def bytes_length_limit_same
qasim-bend-kit@0.1.0.2 · proof/AES_LengthLimitProof.bend:71
import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as AESLengthLimitProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
71def bytes_length_limit_same(+a: List<&2, U32>, +b: List<&2, U32>,
72 +max_low: U32, +max_high: U32,
73 same_length: {List.length(&2, U32, a) ==
74 List.length(&2, U32, b) : Nat}) ->
75 {AES.bytes_length_limit(a, max_low, max_high) ==
76 AES.bytes_length_limit(b, max_low, max_high) : Bool}:
77 length_limit_go_same(a, b, 0, 0, max_low, max_high, True{},
78 same_length)