AESLengthLimitProof.plaintext_valid_same_length: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as AESLengthLimitProof
Lines 80-110 of qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&start_line=80&end_line=110

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

def plaintext_valid_same_length(+ciphertext: List<&2, U32>,
    +plaintext: List<&2, U32>,
    ciphertext_bytes_valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
    plaintext_is_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
    same_length: {List.length(&2, U32, ciphertext) ==
        List.length(&2, U32, plaintext) : Nat}) ->
    {AES.plaintext_valid(ciphertext) == True{} : Bool}:
    length_limit_eq = bytes_length_limit_same(ciphertext, plaintext,
        4294967264, 15, same_length)
    plaintext_limit = bool_and_true_right(AES.bytes_valid(plaintext),
        AES.bytes_length_limit(plaintext, 4294967264, 15),
        plaintext_is_valid)
    ciphertext_limit = Equal.trans(Bool,
        AES.bytes_length_limit(ciphertext, 4294967264, 15),
        AES.bytes_length_limit(plaintext, 4294967264, 15), True{},
        length_limit_eq, plaintext_limit)
    Equal.trans(Bool, AES.plaintext_valid(ciphertext),
        Bool.and(True{}, True{}), 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)),
            Bool.and(True{}, True{}),
            Equal.cong(Bool, Bool, valid => Bool.and(valid,
                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
                AES.bytes_valid(ciphertext), True{}, ciphertext_bytes_valid),
            Equal.cong(Bool, Bool, within => Bool.and(True{}, within),
                AES.bytes_length_limit(ciphertext, 4294967264, 15), True{},
                ciphertext_limit)),
        {==})

Uses (13):
  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.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=plaintext_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&name=bool_and_true_right
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&name=bytes_length_limit_same