def output_tag_matches_context

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:36

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

36def output_tag_matches_context(+output: Core.GcmOutput) ->
37    {CoreTagProof.output_tag(output) ==
38     tag_for_context(output_tag_context(output)) : List<&2, U32>}:
39    match output:
40        case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
41            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
42            tag_matches