start working on proof involving SHA (admitting lemmas as necessary). how to compose + how to deal with hash_blocks_terminate?