AESMaskedXorProof.ctr_ciphertext_plaintext_valid: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as AESMaskedXorProof
Lines 317-360 of qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&start_line=317&end_line=360

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

def ctr_ciphertext_plaintext_valid(+plaintext: List<&2, U32>,
    +stream: List<&2, U32>,
    same_length: {List.length(&2, U32, plaintext) ==
        List.length(&2, U32, stream) : Nat},
    +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
    {AES.plaintext_valid(Core.gcm_zip_xor(plaintext, stream)) ==
        True{} : Bool}:
    +ciphertext = Core.gcm_zip_xor(plaintext, stream)
    cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
        same_length)
    output_bytes_ok = AES.core_bytes_valid_proof(ciphertext,
        Core.gcm_zip_xor_valid(plaintext, stream))
    plaintext_limit_ok = bool_and_true_right(AES.bytes_valid(plaintext),
        AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_ok)
    output_limit_eq = LengthLimitProof.bytes_length_limit_same(plaintext,
        ciphertext, 4294967264, 15, Equal.sym(Nat,
            List.length(&2, U32, ciphertext),
            List.length(&2, U32, plaintext), cipher_length))
    output_limit_ok = Equal.trans(Bool,
        AES.bytes_length_limit(ciphertext, 4294967264, 15),
        AES.bytes_length_limit(plaintext, 4294967264, 15),
        True{}, Equal.sym(Bool,
            AES.bytes_length_limit(plaintext, 4294967264, 15),
            AES.bytes_length_limit(ciphertext, 4294967264, 15),
            output_limit_eq), plaintext_limit_ok)
    Equal.trans(Bool, AES.plaintext_valid(ciphertext),
        Bool.and(AES.bytes_valid(ciphertext),
            AES.bytes_length_limit(ciphertext, 4294967264, 15)),
        True{}, {==},
        Equal.trans(Bool,
            Bool.and(AES.bytes_valid(ciphertext),
                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
            Bool.and(True{},
                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
            True{},
            Equal.cong(Bool, Bool,
                byte_ok => Bool.and(byte_ok,
                    AES.bytes_length_limit(ciphertext, 4294967264, 15)),
                AES.bytes_valid(ciphertext), True{}, output_bytes_ok),
            Equal.trans(Bool,
                Bool.and(True{},
                    AES.bytes_length_limit(ciphertext, 4294967264, 15)),
                AES.bytes_length_limit(ciphertext, 4294967264, 15),
                True{}, {==}, output_limit_ok)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_length_limit
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=core_bytes_valid_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&name=bytes_length_limit_same
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=bool_and_true_right
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=zip_length_equal