AESTamperProof.reject_authenticated: 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 38-67 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=38&end_line=67

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_TagRejectProof.bend as Reject

def reject_authenticated(+key: AES.SecretKey, +aad: List<&2, U32>,
    +envelope: AES.Envelope, +tampered: AES.Envelope,
    canonical: {AES.tag_bytes(AES.envelope_tag(envelope)) ==
        Core.gcm_tag_bytes(Core.gcm_tag_output(
            Core.aes256_expand(AES.secret_key_bytes(key)),
            AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad,
            AES.ciphertext(envelope))) : List<&2, U32>},
    same_nonce: {AES.raw_nonce_bytes(AES.envelope_nonce(tampered)) ==
        AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) : List<&2, U32>},
    same_ciphertext: {AES.ciphertext(tampered) == AES.ciphertext(envelope) :
        List<&2, U32>},
    changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
        AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}) ->
    {AES.decrypt_authenticated(key, aad, tampered) ==
     Fail{AES.AuthenticationFailed{}} :
        Result<&2, &2, AES.Error, List<&2, U32>>}:
    match key envelope tampered:
        case AES.SecretKey{+key_bytes, _, _}
             AES.Envelope{nonce, ciphertext, tag, _}
             AES.Envelope{tampered_nonce, tampered_ciphertext, tampered_tag, _}:
            +words = Core.aes256_expand(key_bytes)
            +tampered_nonce_bytes = AES.raw_nonce_bytes(tampered_nonce)
            +original = AES.tag_bytes(tag)
            canonical_tampered = canonical_for_equal_envelope(words,
                AES.raw_nonce_bytes(nonce), tampered_nonce_bytes, aad,
                ciphertext, tampered_ciphertext, original, canonical,
                same_nonce, same_ciphertext)
            Reject.rejects_tag(words, tampered_nonce_bytes, aad,
                tampered_ciphertext, tampered, tampered_tag, original,
                canonical_tampered, changed_tag)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  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=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt_authenticated
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=envelope_nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=envelope_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=raw_nonce_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=secret_key_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=tag_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes256_expand
  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
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TagRejectProof.bend&name=rejects_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TamperProof.bend&name=canonical_for_equal_envelope