AESTamperProof.canonical_for_equal_envelope: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_TamperProof.bend as AESTamperProof
Lines 7-36 of qasim-bend-kit@0.1.0.2/proof/AES_TamperProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TamperProof.bend&start_line=7&end_line=36

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

def canonical_for_equal_envelope(+words: List<&2, U32>,
    +nonce: List<&2, U32>, +tampered_nonce: List<&2, U32>,
    +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
    +tampered_ciphertext: List<&2, U32>, +original: List<&2, U32>,
    canonical: {original == Core.gcm_tag_bytes(Core.gcm_tag_output(words,
        nonce, aad, ciphertext)) : List<&2, U32>},
    same_nonce: {tampered_nonce == nonce : List<&2, U32>},
    same_ciphertext: {tampered_ciphertext == ciphertext : List<&2, U32>}) ->
    {original == Core.gcm_tag_bytes(Core.gcm_tag_output(words,
        tampered_nonce, aad, tampered_ciphertext)) : List<&2, U32>}:
    nonce_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>,
        value => Core.gcm_tag_bytes(Core.gcm_tag_output(words, value, aad,
            ciphertext)), nonce, tampered_nonce,
        Equal.sym(List<&2, U32>, tampered_nonce, nonce, same_nonce))
    ciphertext_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>,
        value => Core.gcm_tag_bytes(Core.gcm_tag_output(words,
            tampered_nonce, aad, value)), ciphertext, tampered_ciphertext,
        Equal.sym(List<&2, U32>, tampered_ciphertext, ciphertext,
            same_ciphertext))
    Equal.trans(List<&2, U32>, original,
        Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, ciphertext)),
        Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce, aad,
            tampered_ciphertext)), canonical,
        Equal.trans(List<&2, U32>,
            Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
                ciphertext)),
            Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce,
                aad, ciphertext)),
            Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce,
                aad, tampered_ciphertext)), nonce_rewrite, ciphertext_rewrite))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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/libs/AES256GCMCore.bend&name=gcm_tag_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_tag_output