def length_limit_go_same

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

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

22def length_limit_go_same(+a: List<&2, U32>, +b: List<&2, U32>,
23    +low: U32, +high: U32, +max_low: U32, +max_high: U32,
24    +within: Bool,
25    same_length: {List.length(&2, U32, a) ==
26        List.length(&2, U32, b) : Nat}) ->
27    {AES.bytes_length_limit.go(List.length(&2, U32, a), a,
28        low, high, max_low, max_high, within) ==
29     AES.bytes_length_limit.go(List.length(&2, U32, b), b,
30        low, high, max_low, max_high, within) : Bool}:
31    match a b within:
32        case Nil{} Nil{} _: {==}
33        case Nil{} y <> ys _:
34            mismatch = Equal.cong(Nat, Bool,
35                n => Nat.is_eq(0n, n),
36                List.length(&2, U32, Nil{}),
37                List.length(&2, U32, y <> ys), same_length)
38            Empty.absurd(
39                {AES.bytes_length_limit.go(0n, Nil{}, low, high,
40                    max_low, max_high, within) ==
41                 AES.bytes_length_limit.go(
42                    List.length(&2, U32, y <> ys), y <> ys,
43                    low, high, max_low, max_high, within) : Bool},
44                ZipLengthProof.false_true(Equal.sym(Bool,
45                    True{}, False{}, mismatch)))
46        case x <> xs Nil{} _:
47            mismatch = Equal.cong(Nat, Bool,
48                n => Nat.is_eq(n, 0n),
49                List.length(&2, U32, x <> xs),
50                List.length(&2, U32, Nil{}), same_length)
51            Empty.absurd(
52                {AES.bytes_length_limit.go(
53                    List.length(&2, U32, x <> xs), x <> xs,
54                    low, high, max_low, max_high, within) ==
55                 AES.bytes_length_limit.go(0n, Nil{}, low, high,
56                    max_low, max_high, within) : Bool},
57                ZipLengthProof.false_true(mismatch))
58        case x <> xs y <> ys False{}: {==}
59        case x <> xs y <> ys True{}:
60            tail_length = Equal.cong(Nat, Nat, predecessor,
61                List.length(&2, U32, x <> xs),
62                List.length(&2, U32, y <> ys), same_length)
63            +next_low = U32.add(low, 1)
64            +next_high = Bool.pick(U32, U32.is_eq(next_low, 0),
65                U32.add(high, 1), high)
66            next_within = AES.length_pair_within(next_low, next_high,
67                max_low, max_high)
68            length_limit_go_same(xs, ys, next_low, next_high,
69                max_low, max_high, next_within, tail_length)