AESEncryptProof.successful_encrypt_decrypt_authenticated: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend as AESEncryptProof
Lines 515-563 of qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&start_line=515&end_line=563

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

def successful_encrypt_decrypt_authenticated(+key: AES.SecretKey,
    +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
    +envelope: AES.Envelope,
    +aad_ok: {AES.aad_valid(aad) == True{} : Bool},
    +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
        Result<&2, &2, AES.Error, AES.Envelope>}) ->
    {AES.decrypt_authenticated(key, aad, envelope) == Done{plaintext} :
        Result<&2, &2, AES.Error, List<&2, U32>>}:
    match key envelope:
        case AES.SecretKey{+key_bytes, _, _}
             AES.Envelope{envelope_nonce, ciphertext, tag, _}:
            +words = Core.aes256_expand(key_bytes)
            +nonce_bytes = AES.raw_nonce_bytes(envelope_nonce)
            canonical = successful_encrypt_envelope_tag_canonical(key,
                nonce, aad, plaintext, envelope, aad_ok, plaintext_ok,
                encrypted)
            authenticated = decrypt_auth_tag_canonical(words, nonce_bytes,
                aad, ciphertext, envelope, tag, canonical)
            nonce_matches = Equal.cong(AES.Nonce, List<&2, U32>,
                AES.raw_nonce_bytes, envelope_nonce, nonce,
                preserves_nonce(key, nonce, aad, plaintext, envelope,
                    encrypted))
            ctr_roundtrip = successful_encrypt_ctr_decrypts(key, nonce, aad,
                plaintext, envelope, aad_ok, plaintext_ok, encrypted)
            expanded_nonce = Equal.cong(List<&2, U32>, List<&2, U32>,
                value => Core.gcm_decrypt_expanded(words, value, ciphertext),
                nonce_bytes, AES.raw_nonce_bytes(nonce), nonce_matches)
            expanded_to_raw = Equal.trans(List<&2, U32>,
                Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
                Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(nonce),
                    ciphertext),
                Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
                    AES.raw_nonce_bytes(nonce), ciphertext),
                expanded_nonce, {==})
            expanded_roundtrip = Equal.trans(List<&2, U32>,
                Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
                Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
                    AES.raw_nonce_bytes(nonce), ciphertext), plaintext,
                expanded_to_raw, ctr_roundtrip)
            payload = Equal.cong(List<&2, U32>,
                Result<&2, &2, AES.Error, List<&2, U32>>,
                value => Done{value},
                Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
                plaintext, expanded_roundtrip)
            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
                AES.decrypt_authenticated(key, aad, envelope),
                AES.decrypt_auth_result(words, envelope, True{}),
                Done{plaintext}, authenticated, payload)

Uses (24):
  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=Nonce
  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=aad_valid
  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/libs/AES256GCM.bend&name=decrypt_authenticated
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid
  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/AES256GCMCore.bend&name=aes256_expand
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_decrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_decrypt_raw
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=decrypt_auth_tag_canonical
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=preserves_nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_ctr_decrypts
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_envelope_tag_canonical