def ctr_ciphertext_plaintext_valid

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:317

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
import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as LengthLimitProof

317def ctr_ciphertext_plaintext_valid(+plaintext: List<&2, U32>,
318    +stream: List<&2, U32>,
319    same_length: {List.length(&2, U32, plaintext) ==
320        List.length(&2, U32, stream) : Nat},
321    +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
322    {AES.plaintext_valid(Core.gcm_zip_xor(plaintext, stream)) ==
323        True{} : Bool}:
324    +ciphertext = Core.gcm_zip_xor(plaintext, stream)
325    cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
326        same_length)
327    output_bytes_ok = AES.core_bytes_valid_proof(ciphertext,
328        Core.gcm_zip_xor_valid(plaintext, stream))
329    plaintext_limit_ok = bool_and_true_right(AES.bytes_valid(plaintext),
330        AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_ok)
331    output_limit_eq = LengthLimitProof.bytes_length_limit_same(plaintext,
332        ciphertext, 4294967264, 15, Equal.sym(Nat,
333            List.length(&2, U32, ciphertext),
334            List.length(&2, U32, plaintext), cipher_length))
335    output_limit_ok = Equal.trans(Bool,
336        AES.bytes_length_limit(ciphertext, 4294967264, 15),
337        AES.bytes_length_limit(plaintext, 4294967264, 15),
338        True{}, Equal.sym(Bool,
339            AES.bytes_length_limit(plaintext, 4294967264, 15),
340            AES.bytes_length_limit(ciphertext, 4294967264, 15),
341            output_limit_eq), plaintext_limit_ok)
342    Equal.trans(Bool, AES.plaintext_valid(ciphertext),
343        Bool.and(AES.bytes_valid(ciphertext),
344            AES.bytes_length_limit(ciphertext, 4294967264, 15)),
345        True{}, {==},
346        Equal.trans(Bool,
347            Bool.and(AES.bytes_valid(ciphertext),
348                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
349            Bool.and(True{},
350                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
351            True{},
352            Equal.cong(Bool, Bool,
353                byte_ok => Bool.and(byte_ok,
354                    AES.bytes_length_limit(ciphertext, 4294967264, 15)),
355                AES.bytes_valid(ciphertext), True{}, output_bytes_ok),
356            Equal.trans(Bool,
357                Bool.and(True{},
358                    AES.bytes_length_limit(ciphertext, 4294967264, 15)),
359                AES.bytes_length_limit(ciphertext, 4294967264, 15),
360                True{}, {==}, output_limit_ok)))