AESEncryptProof.successful_encrypt_ciphertext_matches_ctr: 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 323-348 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=323&end_line=348

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 CoreTagProof

def successful_encrypt_ciphertext_matches_ctr(+key: AES.SecretKey,
    +nonce: AES.Nonce, +aad: List<&2, U32>,
    +plaintext: List<&2, U32>, +envelope: AES.Envelope,
    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
        Result<&2, &2, AES.Error, AES.Envelope>}) ->
    {AES.ciphertext(envelope) ==
     Core.gcm_zip_xor(plaintext,
        Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
            Core.aes256_expand(AES.secret_key_bytes(key)),
            Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))) :
        List<&2, U32>}:
    Equal.trans(List<&2, U32>,
        AES.ciphertext(envelope),
        CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce,
            aad, plaintext)),
        Core.gcm_zip_xor(plaintext,
            Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
                Core.aes256_expand(AES.secret_key_bytes(key)),
                Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))),
        successful_encrypt_ciphertext_matches_gcm(key, nonce, aad,
            plaintext, envelope, aad_valid, plaintext_valid, encrypted),
        CoreTagProof.raw_encrypt_output_ciphertext(
            AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), aad,
            plaintext))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=List.length
  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=ciphertext
  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=encrypt_valid_output
  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_ctr_stream_exact
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_inc32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_j0
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor
  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=raw_encrypt_output_ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_ciphertext_matches_gcm