def successful_encrypt_ciphertext_valid

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

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

350def successful_encrypt_ciphertext_valid(+key: AES.SecretKey,
351    +nonce: AES.Nonce, +aad: List<&2, U32>,
352    +plaintext: List<&2, U32>, +envelope: AES.Envelope,
353    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
354    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
355    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
356        Result<&2, &2, AES.Error, AES.Envelope>}) ->
357    {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool}:
358    length_eq = successful_encrypt_preserves_length(key, nonce, aad,
359        plaintext, envelope, encrypted)
360    LengthLimitProof.plaintext_valid_same_length(
361        AES.ciphertext(envelope), plaintext,
362        AES.envelope_ciphertext_valid(envelope), plaintext_valid, length_eq)