def plaintext_valid_same_length

qasim-bend-kit@0.1.0.2 · proof/AES_LengthLimitProof.bend:80

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

80def plaintext_valid_same_length(+ciphertext: List<&2, U32>,
81    +plaintext: List<&2, U32>,
82    ciphertext_bytes_valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
83    plaintext_is_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
84    same_length: {List.length(&2, U32, ciphertext) ==
85        List.length(&2, U32, plaintext) : Nat}) ->
86    {AES.plaintext_valid(ciphertext) == True{} : Bool}:
87    length_limit_eq = bytes_length_limit_same(ciphertext, plaintext,
88        4294967264, 15, same_length)
89    plaintext_limit = bool_and_true_right(AES.bytes_valid(plaintext),
90        AES.bytes_length_limit(plaintext, 4294967264, 15),
91        plaintext_is_valid)
92    ciphertext_limit = Equal.trans(Bool,
93        AES.bytes_length_limit(ciphertext, 4294967264, 15),
94        AES.bytes_length_limit(plaintext, 4294967264, 15), True{},
95        length_limit_eq, plaintext_limit)
96    Equal.trans(Bool, AES.plaintext_valid(ciphertext),
97        Bool.and(True{}, True{}), True{},
98        Equal.trans(Bool,
99            Bool.and(AES.bytes_valid(ciphertext),
100                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
101            Bool.and(True{},
102                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
103            Bool.and(True{}, True{}),
104            Equal.cong(Bool, Bool, valid => Bool.and(valid,
105                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
106                AES.bytes_valid(ciphertext), True{}, ciphertext_bytes_valid),
107            Equal.cong(Bool, Bool, within => Bool.and(True{}, within),
108                AES.bytes_length_limit(ciphertext, 4294967264, 15), True{},
109                ciphertext_limit)),
110        {==})