def successful_encrypt_preserves_length

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

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

197def successful_encrypt_preserves_length(+key: AES.SecretKey,
198    +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
199    +envelope: AES.Envelope,
200    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
201        Result<&2, &2, AES.Error, AES.Envelope>}) ->
202    {List.length(&2, U32, AES.ciphertext(envelope)) ==
203     List.length(&2, U32, plaintext) : Nat}:
204    +aad_flag = AES.aad_valid(aad)
205    +plaintext_flag = AES.plaintext_valid(plaintext)
206    aad_is_true = successful_encrypt_aad_valid(key, nonce, aad, plaintext,
207        aad_flag, plaintext_flag, {==}, {==}, envelope, encrypted)
208    plaintext_is_true = successful_encrypt_plaintext_valid(key, nonce,
209        aad, plaintext, aad_flag, plaintext_flag, {==}, {==},
210        envelope, encrypted)
211    checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
212        True{}, True{}, aad_is_true, plaintext_is_true, envelope, encrypted)
213    output_length = valid_output_ciphertext_length(key, nonce, aad, plaintext)
214    Equal.trans(Nat,
215        List.length(&2, U32, AES.ciphertext(envelope)),
216        result_ciphertext_length(
217            AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})),
218        List.length(&2, U32, plaintext),
219        Equal.sym(Nat,
220            result_ciphertext_length(
221                AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})),
222            result_ciphertext_length(Done{envelope}),
223            Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Nat,
224                result => result_ciphertext_length(result),
225                AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}),
226                Done{envelope}, checked)),
227        output_length)