def successful_encrypt_ciphertext_matches_gcm

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

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_CoreTagProof.bend as CoreTagProof

229def successful_encrypt_ciphertext_matches_gcm(+key: AES.SecretKey,
230    +nonce: AES.Nonce, +aad: List<&2, U32>,
231    +plaintext: List<&2, U32>, +envelope: AES.Envelope,
232    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
233    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
234    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
235        Result<&2, &2, AES.Error, AES.Envelope>}) ->
236    {AES.ciphertext(envelope) ==
237     CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce,
238        aad, plaintext)) : List<&2, U32>}:
239    checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
240        True{}, True{}, aad_valid, plaintext_valid, envelope, encrypted)
241    +output = AES.encrypt_valid_output(key, nonce, aad, plaintext)
242    constructed_matches = Equal.cong(
243        Result<&2, &2, AES.Error, AES.Envelope>, List<&2, U32>,
244        result => result_ciphertext(AES.ciphertext(envelope), result),
245        AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}),
246        Done{envelope}, checked)
247    Equal.trans(List<&2, U32>,
248        AES.ciphertext(envelope),
249        AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)),
250        CoreTagProof.output_ciphertext(output),
251        Equal.sym(List<&2, U32>,
252            AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)),
253            AES.ciphertext(envelope), constructed_matches),
254        CoreTagProof.envelope_gcm_ciphertext(nonce, output))