def valid_output_ciphertext_length

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:69

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_ZipLengthProof.bend as ZipLengthProof

69def valid_output_ciphertext_length(+key: AES.SecretKey,
70    +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>) ->
71    {List.length(&2, U32,
72        AES.ciphertext(AES.envelope_from_gcm_checked(nonce,
73            AES.encrypt_valid_output(key, nonce, aad, plaintext)))) ==
74     List.length(&2, U32, plaintext) : Nat}:
75    ZipLengthProof.ctr_encrypt_ciphertext_length(
76        Core.aes256_expand(AES.secret_key_bytes(key)),
77        AES.raw_nonce_bytes(nonce), plaintext)