AESNistVectorProof.checkpoint_empty_ghash: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AESNistVectorProof
Lines 35-37 of qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&start_line=35&end_line=37

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

def checkpoint_empty_ghash() ->
    {TagProof.auth_from_hash(Hash.result(), empty_aad(), empty_ciphertext()) == empty_auth() : List<&2, U32>}:
    {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend&name=result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistTagProof.bend&name=auth_from_hash
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=empty_aad
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=empty_auth
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=empty_ciphertext