AESKnownAnswerProof.output_matches: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend as AESKnownAnswerProof
Lines 61-95 of qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&start_line=61&end_line=95

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
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 Fields

def output_matches(+nonce: AES.Nonce, +output: Core.GcmOutput,
    +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
    ciphertext_matches: {Fields.output_ciphertext(output) == ciphertext :
        List<&2, U32>},
    tag_matches: {Fields.output_tag(output) == tag_bytes : List<&2, U32>}) ->
    @+tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat} ->
    @+tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool} ->
    @+ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool} ->
    {AES.encrypt_output_from_gcm(nonce, output) ==
     Done{AES.Envelope{nonce, ciphertext,
        AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
        Result<&2, &2, AES.Error, AES.Envelope>}:
    match output:
        case Core.GcmOutput{+actual_ciphertext, actual_ciphertext_valid,
            +actual_tag, actual_tag_valid, actual_tag_size, _, _, _, _}:
            tag_size => tag_valid => ciphertext_valid =>
                +actual_valid = AES.core_bytes_valid_proof(actual_ciphertext,
                    actual_ciphertext_valid)
                +actual_tag_value = {AES.Tag{actual_tag, actual_tag_size,
                    AES.core_bytes_valid_proof(actual_tag, actual_tag_valid)} :
                    AES.Tag}
                +expected_tag_value = {AES.Tag{tag_bytes, tag_size, tag_valid} :
                    AES.Tag}
                tag_eq = tag_equal(actual_tag, actual_tag_size,
                    AES.core_bytes_valid_proof(actual_tag, actual_tag_valid),
                    tag_bytes, tag_matches, tag_size, tag_valid)
                envelope_eq = envelope_equal(nonce, actual_ciphertext,
                    actual_tag_value, actual_valid, ciphertext,
                    expected_tag_value, ciphertext_matches, tag_eq,
                    ciphertext_valid)
                Equal.cong(AES.Envelope,
                    Result<&2, &2, AES.Error, AES.Envelope>, value => Done{value},
                    AES.envelope_from_gcm_checked(nonce, output),
                    AES.Envelope{nonce, ciphertext, expected_tag_value,
                        ciphertext_valid}, envelope_eq)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  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/AES256GCM.bend&name=Envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=core_bytes_valid_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt_output_from_gcm
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=envelope_from_gcm_checked
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=GcmOutput
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CoreTagProof.bend&name=output_ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CoreTagProof.bend&name=output_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&name=envelope_equal
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&name=tag_equal