AESNistObservationProof.finish_auth: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
Lines 208-228 of qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&start_line=208&end_line=228

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

def finish_auth(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope,
    +tag: List<&2, U32>, +flag: Bool, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
    tag_matches: {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>},
    compare_matches: {auth_for_tag(envelope, tag) == flag : Bool},
    branch_matches: {AES.decrypt_auth_result(words, envelope, flag) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
    {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
        decrypt_expanded(words, aad, envelope),
        AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
        result, decrypt_auth_shape(words, aad, envelope),
        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
            AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
            AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)), result,
            Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, actual_tag =>
                AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, actual_tag)),
                envelope_tag_computed(words, aad, envelope), tag, tag_matches),
            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
                AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)),
                AES.decrypt_auth_result(words, envelope, flag), result,
                Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, accepted => AES.decrypt_auth_result(words, envelope, accepted),
                    auth_for_tag(envelope, tag), flag, compare_matches), branch_matches)))

Uses (13):
  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=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=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=decrypt_auth_result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=auth_for_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=decrypt_auth_shape
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=decrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=envelope_tag_computed