def checkpoint_partial_block_ghash

qasim-bend-kit@0.1.0.2 · proof/AES_NistVectorProof.bend:295

import Base
import qasim-bend-kit@0.1.0.2/proof/AES_NistTagProof.bend as TagProof
import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Hash

295def checkpoint_partial_block_ghash() ->
296    {TagProof.auth_from_hash(Hash.result(), partial_block_aad(), partial_block_ciphertext()) == partial_block_auth() : List<&2, U32>}:
297    {==}