proofs/crypto/argon2/fill.bend

bend-collections-laws-crypto@1.0.0.0 · 361 lines · 42 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR2
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
14import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
15import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
16import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as MEM
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as IX
20
21# Filling the memory: every segment, slice, lane and pass of the
22# implementation (on the packed array) equals the specification's (on the
23# list of blocks), as the array thaw(mt(d, mem)) of the specification's list.
24
25# ---------------------------------------------------------------- arithmetic
26
27def mod_lt(+v: Nat, +q: Nat, +hq: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(v, q), q) == True{} : Bool}:
28  match q:
29    case 0n:
30      Empty.absurd({Nat.is_lt(Nat.mod(v, 0n), 0n) == True{} : Bool}, L.false_true(hq))
31    case 1n+ +b:
32      NR.dm_lt(b, v)
33
34# a < p and b < q give a * q + b < p * q.
35def lt_mul_add(+a: Nat, +p: Nat, +b: Nat, +q: Nat, +ha: {Nat.is_lt(a, p) == True{} : Bool}, +hb: {Nat.is_lt(b, q) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(a, q), b), Nat.mul(p, q)) == True{} : Bool}:
36  +h1 = N.lt_add_left(b, q, Nat.mul(a, q), hb)
37  +h2 = AR2.mul_le(1n+a, p, q, N.lt_succ_le_succ(a, p, ha))
38  N.lt_le_trans(Nat.add(Nat.mul(a, q), b), Nat.add(Nat.mul(a, q), q), Nat.mul(p, q), h1,
39    L.subst(Nat, z => {Nat.is_le(z, Nat.mul(p, q)) == True{} : Bool}, Nat.mul(1n+a, q), Nat.add(Nat.mul(a, q), q), NA.add_comm(q, Nat.mul(a, q)), h2))
40
41# s < 4 and idx < sl give s * sl + idx < 4 sl.
42def seg_lt(+s: Nat, +sl: Nat, +idx: Nat, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(s, sl), idx), Nat.mul(4n, sl)) == True{} : Bool}:
43  lt_mul_add(s, 4n, idx, sl, hs, hi)
44
45def le_of_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
46  N.lt_le(a, b, h)
47
48def other_le(+base: Nat, +z: Bool) -> {Nat.is_le(SA.area_other(base, z), base) == True{} : Bool}:
49  match z:
50    case True{}:
51      AR2.sub_le2(base, 1n)
52    case False{}:
53      N.le_refl(base)
54
55# The size of the reference area is below the base plus the index.
56def area_le(+base: Nat, +idx: Nat, +same: Bool) -> {Nat.is_le(SA.area(base, idx, same), Nat.add(base, idx)) == True{} : Bool}:
57  match same:
58    case True{}:
59      AR2.sub_le2(Nat.add(base, idx), 1n)
60    case False{}:
61      N.le_trans(SA.area_other(base, Nat.is_eq(idx, 0n)), base, Nat.add(base, idx), other_le(base, Nat.is_eq(idx, 0n)), N.le_add_right(base, idx))
62
63# The base of the reference area plus the index stays below q = 4 sl.
64def base_lt(+r0: Bool, +s: Nat, +sl: Nat, +idx: Nat, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}) -> {Nat.is_lt(Nat.add(SA.area_base(r0, s, sl, Nat.mul(4n, sl)), idx), Nat.mul(4n, sl)) == True{} : Bool}:
65  match r0:
66    case True{}:
67      seg_lt(s, sl, idx, hs, hi)
68    case False{}:
69      +q = Nat.mul(4n, sl)
70      +hsq = N.le_trans(sl, Nat.add(sl, Nat.mul(3n, sl)), q, N.le_add_right(sl, Nat.mul(3n, sl)), N.le_refl(q))
71      +e = N.sub_add(q, sl, hsq)
72      +h1 = N.lt_add_left(idx, sl, Nat.sub(q, sl), hi)
73      L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(q, sl), idx), z) == True{} : Bool}, Nat.add(Nat.sub(q, sl), sl), q,
74        Equal.trans(Nat, Nat.add(Nat.sub(q, sl), sl), Nat.add(sl, Nat.sub(q, sl)), q, NA.add_comm(Nat.sub(q, sl), sl), e), h1)
75
76# ---------------------------------------------------------------- one block
77
78def store_eq(+d: Nat, +mem: List<&2, A.Block>, +r0: Bool, +cur: Nat, +prev: A.Block, +refb: A.Block, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hcur: {Nat.is_lt(cur, SC.length(A.Block, mem)) == True{} : Bool}) -> {I.store(r0, cur, prev, refb, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.store(r0, cur, prev, refb, mem))) : Array<U32>}:
79  match r0:
80    case True{}:
81      %Equal.sym(A.Block, G.compress(prev, refb), SG.G(prev, refb), BL.compress_correct(prev, refb)) : {M.set(cur, _, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.set(mem, cur, SG.G(prev, refb)))) : Array<U32>}
82      MEM.set_block(d, mem, cur, SG.G(prev, refb), hd, hc, hcur)
83    case False{}:
84      +old = SA.get(mem, cur)
85      %Equal.sym(Array<U32> & A.Block, M.get(cur, AR.thaw(U32, MEM.mt(d, mem))), (AR.thaw(U32, MEM.mt(d, mem)), old), MEM.get_block(d, mem, cur, hd, hc, hcur)) : {I.store_xor(cur, prev, refb, _) == AR.thaw(U32, MEM.mt(d, SA.set(mem, cur, SG.xor(SG.G(prev, refb), old)))) : Array<U32>}
86      %Equal.sym(A.Block, G.compress_xor(prev, refb, old), SG.xor(SG.G(prev, refb), old), BL.compress_xor_correct(prev, refb, old)) : {M.set(cur, _, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.set(mem, cur, SG.xor(SG.G(prev, refb), old)))) : Array<U32>}
87      MEM.set_block(d, mem, cur, SG.xor(SG.G(prev, refb), old), hd, hc, hcur)
88
89def store_len(+r0: Bool, +cur: Nat, +prev: A.Block, +refb: A.Block, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.store(r0, cur, prev, refb, mem)) == SC.length(A.Block, mem) : Nat}:
90  match r0:
91    case True{}:
92      LL.length_update(A.Block, mem, cur, SG.G(prev, refb))
93    case False{}:
94      LL.length_update(A.Block, mem, cur, SG.xor(SG.G(prev, refb), SA.get(mem, cur)))
95
96# The reference block index from the pseudo-random lane pr, as the implementation computes it.
97def ixi(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +pr: T.Lane) -> Nat:
98  +rl = I.ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, I.hi(pr), p)
99  +w = I.area(I.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l))
100  Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(I.start(r0, s, sl), I.rel(w, G.lo(pr))), q))
101
102# The same after the reference lane, and as the specification computes it.
103def ixi_mid(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +rl: Nat) -> Nat:
104  Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(I.start(r0, s, sl), I.rel(I.area(I.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), G.lo(pr))), q))
105
106def ixs_mid(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +rl: Nat) -> Nat:
107  Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(SA.start(r0, s, sl), SA.rel(SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), SA.lo(pr))), q))
108
109def ixs(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +pr: T.Lane) -> Nat:
110  +rl = SA.ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, SA.hi(pr), p)
111  +w = SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l))
112  Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(SA.start(r0, s, sl), SA.rel(w, SA.lo(pr))), q))
113
114def le_mul256(+n: Nat) -> {Nat.is_le(n, Nat.mul(n, 256n)) == True{} : Bool}:
115  %Equal.sym(Nat, Nat.mul(n, 256n), Nat.mul(256n, n), NA.mul_comm(n, 256n)) : {Nat.is_le(n, _) == True{} : Bool}
116  N.le_add_right(n, Nat.mul(255n, n))
117
118# |W| < 2^d.
119def area_bound(+d: Nat, +n: Nat, +r0: Bool, +s: Nat, +sl: Nat, +q: Nat, +idx: Nat, +same: Bool, +hq: {q == Nat.mul(4n, sl) : Nat}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hqn: {Nat.is_le(q, n) == True{} : Bool}, +hn: {Nat.is_le(Nat.mul(n, 256n), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(SA.area(SA.area_base(r0, s, sl, q), idx, same), SC.pow2(d)) == True{} : Bool}:
120  +base = SA.area_base(r0, s, sl, q)
121  +h1 = area_le(base, idx, same)
122  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(SA.area_base(r0, s, sl, z), idx), z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), base_lt(r0, s, sl, idx, hs, hi))
123  +h3 = N.le_trans(n, Nat.mul(n, 256n), SC.pow2(d), le_mul256(n), hn)
124  N.le_lt_trans(SA.area(base, idx, same), Nat.add(base, idx), SC.pow2(d), h1, N.lt_le_trans(Nat.add(base, idx), q, SC.pow2(d), h2, N.le_trans(q, n, SC.pow2(d), hqn, h3)))
125
126def mid_eq(+d: Nat, +n: Nat, +r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +rl: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hqn: {Nat.is_le(q, n) == True{} : Bool}, +hn: {Nat.is_le(Nat.mul(n, 256n), SC.pow2(d)) == True{} : Bool}) -> {ixi_mid(r0, s, l, idx, q, sl, pr, rl) == ixs_mid(r0, s, l, idx, q, sl, pr, rl) : Nat}:
127  +same = Nat.is_eq(rl, l)
128  +wi = I.area(I.area_base(r0, s, sl, q), idx, same)
129  +ws = SA.area(SA.area_base(r0, s, sl, q), idx, same)
130  +ew = Equal.trans(Nat, wi, I.area(SA.area_base(r0, s, sl, q), idx, same), ws,
131    Equal.cong(Nat, Nat, z => I.area(z, idx, same), I.area_base(r0, s, sl, q), SA.area_base(r0, s, sl, q), IX.area_base_eq(r0, s, sl, q)),
132    IX.area_eq(SA.area_base(r0, s, sl, q), idx, same))
133  +erel = Equal.trans(Nat, I.rel(wi, G.lo(pr)), I.rel(ws, G.lo(pr)), SA.rel(ws, SA.lo(pr)),
134    Equal.cong(Nat, Nat, z => I.rel(z, G.lo(pr)), wi, ws, ew),
135    Equal.trans(Nat, I.rel(ws, G.lo(pr)), I.rel(ws, SA.lo(pr)), SA.rel(ws, SA.lo(pr)),
136      Equal.cong(U32, Nat, z => I.rel(ws, z), G.lo(pr), SA.lo(pr), IX.lo_eq(pr)),
137      IX.rel_eq(ws, SA.lo(pr), d, N.lt_le(d, 32n, hd), area_bound(d, n, r0, s, sl, q, idx, same, hq, hs, hi, hqn, hn))))
138  Equal.trans(Nat, ixi_mid(r0, s, l, idx, q, sl, pr, rl), Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(SA.start(r0, s, sl), I.rel(wi, G.lo(pr))), q)), ixs_mid(r0, s, l, idx, q, sl, pr, rl),
139    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(z, I.rel(wi, G.lo(pr))), q)), I.start(r0, s, sl), SA.start(r0, s, sl), IX.start_eq(r0, s, sl)),
140    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(rl, q), Nat.mod(Nat.add(SA.start(r0, s, sl), z), q)), I.rel(wi, G.lo(pr)), SA.rel(ws, SA.lo(pr)), erel))
141
142def ix_eq(+d: Nat, +n: Nat, +r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hqn: {Nat.is_le(q, n) == True{} : Bool}, +hn: {Nat.is_le(Nat.mul(n, 256n), SC.pow2(d)) == True{} : Bool}) -> {ixi(r0, s, l, idx, p, q, sl, pr) == ixs(r0, s, l, idx, p, q, sl, pr) : Nat}:
143  +f = Bool.and(r0, Nat.is_eq(s, 0n))
144  +rli = I.ref_lane(f, l, I.hi(pr), p)
145  +rls = SA.ref_lane(f, l, SA.hi(pr), p)
146  +erl = Equal.trans(Nat, rli, SA.ref_lane(f, l, I.hi(pr), p), rls,
147    IX.ref_lane_eq(f, l, I.hi(pr), p),
148    Equal.cong(U32, Nat, z => SA.ref_lane(f, l, z, p), I.hi(pr), SA.hi(pr), IX.hi_eq(pr)))
149  Equal.trans(Nat, ixi_mid(r0, s, l, idx, q, sl, pr, rli), ixi_mid(r0, s, l, idx, q, sl, pr, rls), ixs_mid(r0, s, l, idx, q, sl, pr, rls),
150    Equal.cong(Nat, Nat, z => ixi_mid(r0, s, l, idx, q, sl, pr, z), rli, rls, erl),
151    mid_eq(d, n, r0, s, l, idx, q, sl, pr, rls, hd, hq, hs, hi, hqn, hn))
152
153def ref_lane_lt(+f: Bool, +l: Nat, +j2: U32, +p: Nat, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.is_lt(SA.ref_lane(f, l, j2, p), p) == True{} : Bool}:
154  match f:
155    case True{}:
156      hl
157    case False{}:
158      mod_lt(U32.to_nat(j2), p, hp)
159
160def q_pos(+q: Nat, +sl: Nat, +hq: {q == Nat.mul(4n, sl) : Nat}, +hsl: {Nat.is_le(1n, sl) == True{} : Bool}) -> {Nat.is_le(1n, q) == True{} : Bool}:
161  L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), N.le_trans(1n, sl, Nat.mul(4n, sl), hsl, N.le_add_right(sl, Nat.mul(3n, sl))))
162
163# The reference block is in the memory.
164def ix_lt(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(ixs(r0, s, l, idx, p, q, sl, pr), Nat.mul(p, q)) == True{} : Bool}:
165  +rl = SA.ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, SA.hi(pr), p)
166  lt_mul_add(rl, p, Nat.mod(Nat.add(SA.start(r0, s, sl), SA.rel(SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), SA.lo(pr))), q), q, ref_lane_lt(Bool.and(r0, Nat.is_eq(s, 0n)), l, SA.hi(pr), p, hl, hp), mod_lt(Nat.add(SA.start(r0, s, sl), SA.rel(SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), SA.lo(pr))), q, hq1))
167
168def le_mul_left(+p: Nat, +q: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.is_le(q, Nat.mul(p, q)) == True{} : Bool}:
169  match p:
170    case 0n:
171      Empty.absurd({Nat.is_le(q, 0n) == True{} : Bool}, L.false_true(hp))
172    case 1n+k:
173      N.le_add_right(q, Nat.mul(k, q))
174
175# One block of a segment.
176def step_eq(+d: Nat, +mem: List<&2, A.Block>, +r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +pb: A.Block, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(1n, sl) == True{} : Bool}, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hcur: {Nat.is_lt(cur, SC.length(A.Block, mem)) == True{} : Bool}) -> {I.step(r, l, s, idx, p, q, sl, cur, indep, addr, (AR.thaw(U32, MEM.mt(d, mem)), pb)) == AR.thaw(U32, MEM.mt(d, SA.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem))) : Array<U32>}:
177  +r0 = Nat.is_eq(r, 0n)
178  +pri = I.pick(indep, addr, idx, pb)
179  +prs = SA.pick(indep, addr, idx, pb)
180  +n = SC.length(A.Block, mem)
181  +hq1 = q_pos(q, sl, hq, hsl)
182  +hqn = L.subst(Nat, z => {Nat.is_le(q, z) == True{} : Bool}, Nat.mul(p, q), n, Equal.sym(Nat, n, Nat.mul(p, q), hlen), le_mul_left(p, q, hp))
183  +ei = Equal.trans(Nat, ixi(r0, s, l, idx, p, q, sl, pri), ixi(r0, s, l, idx, p, q, sl, prs), ixs(r0, s, l, idx, p, q, sl, prs),
184    Equal.cong(T.Lane, Nat, z => ixi(r0, s, l, idx, p, q, sl, z), pri, prs, IX.pick_eq(indep, addr, idx, pb)),
185    ix_eq(d, n, r0, s, l, idx, p, q, sl, prs, hd, hq, hs, hi, hqn, hc))
186  +ix = ixs(r0, s, l, idx, p, q, sl, prs)
187  +hix = L.subst(Nat, z => {Nat.is_lt(ix, z) == True{} : Bool}, Nat.mul(p, q), n, Equal.sym(Nat, n, Nat.mul(p, q), hlen), ix_lt(r0, s, l, idx, p, q, sl, prs, hl, hp, hq1))
188  %Equal.sym(Nat, ixi(r0, s, l, idx, p, q, sl, pri), ix, ei) : {I.with_ref(r0, cur, pb, M.get(_, AR.thaw(U32, MEM.mt(d, mem)))) == AR.thaw(U32, MEM.mt(d, SA.store(r0, cur, pb, SA.get(mem, ix), mem))) : Array<U32>}
189  %Equal.sym(Array<U32> & A.Block, M.get(ix, AR.thaw(U32, MEM.mt(d, mem))), (AR.thaw(U32, MEM.mt(d, mem)), SA.get(mem, ix)), MEM.get_block(d, mem, ix, hd, hc, hix)) : {I.with_ref(r0, cur, pb, _) == AR.thaw(U32, MEM.mt(d, SA.store(r0, cur, pb, SA.get(mem, ix), mem))) : Array<U32>}
190  store_eq(d, mem, r0, cur, pb, SA.get(mem, ix), hd, hc, hcur)
191
192# ---------------------------------------------------------------- segments
193
194def step_len(+r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +pb: A.Block, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem)) == SC.length(A.Block, mem) : Nat}:
195  +r0 = Nat.is_eq(r, 0n)
196  store_len(r0, cur, pb, SA.get(mem, ixs(r0, s, l, idx, p, q, sl, SA.pick(indep, addr, idx, pb))), mem)
197
198def sub1_lt(+q: Nat, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(q, 1n), q) == True{} : Bool}:
199  match q:
200    case 0n:
201      Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n), 0n) == True{} : Bool}, L.false_true(hq1))
202    case 1n+ +k:
203      %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) : {Nat.is_lt(_, 1n+k) == True{} : Bool}
204      N.lt_succ(k)
205
206# The previous block is in the memory.
207def prev_lt(+l: Nat, +p: Nat, +q: Nat, +j: Nat, +b: Bool, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hj: {Nat.is_lt(j, q) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(SA.prev_index(l, q, j, b), Nat.mul(p, q)) == True{} : Bool}:
208  match b:
209    case True{}:
210      lt_mul_add(l, p, Nat.sub(q, 1n), q, hl, sub1_lt(q, hq1))
211    case False{}:
212      N.le_lt_trans(Nat.sub(Nat.add(Nat.mul(l, q), j), 1n), Nat.add(Nat.mul(l, q), j), Nat.mul(p, q), AR2.sub_le2(Nat.add(Nat.mul(l, q), j), 1n), lt_mul_add(l, p, j, q, hl, hj))
213
214def lt_of_add_succ(+a: Nat, +r: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(a, 1n+r), n) == True{} : Bool}) -> {Nat.is_lt(a, n) == True{} : Bool}:
215  N.lt_le_trans(a, Nat.add(a, 1n+r), n, MEM.lt_add_succ(a, r), h)
216
217def le_shift(+a: Nat, +r: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(a, 1n+r), n) == True{} : Bool}) -> {Nat.is_le(Nat.add(Nat.add(a, 1n), r), n) == True{} : Bool}:
218  L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(a, 1n+r), Nat.add(Nat.add(a, 1n), r), Equal.sym(Nat, Nat.add(Nat.add(a, 1n), r), Nat.add(a, 1n+r), MEM.add_one_assoc(a, r)), h)
219
220def lt_q(+q: Nat, +sl: Nat, +x: Nat, +hq: {q == Nat.mul(4n, sl) : Nat}, +h: {Nat.is_lt(x, Nat.mul(4n, sl)) == True{} : Bool}) -> {Nat.is_lt(x, q) == True{} : Bool}:
221  L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), h)
222
223def lt_len(+x: Nat, +mem: List<&2, A.Block>, +p: Nat, +q: Nat, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +h: {Nat.is_lt(x, Nat.mul(p, q)) == True{} : Bool}) -> {Nat.is_lt(x, SC.length(A.Block, mem)) == True{} : Bool}:
224  L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, Nat.mul(p, q), SC.length(A.Block, mem), Equal.sym(Nat, SC.length(A.Block, mem), Nat.mul(p, q), hlen), h)
225
226def seg_len(+n: Nat, +idx: Nat, +first: Bool, +addr: A.Block, +mem: List<&2, A.Block>, +r: Nat, +l: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +indep: Bool) -> {SC.length(A.Block, SA.seg_go(n, idx, first, addr, mem, r, l, s, p, q, sl, mm, t, indep)) == SC.length(A.Block, mem) : Nat}:
227  match n:
228    case 0n:
229      {==}
230    case 1n+ +rest:
231      +a2 = SA.regen(Bool.and(indep, Bool.or(first, Nat.is_eq(Nat.mod(idx, 128n), 0n))), addr, r, l, s, mm, t, idx)
232      +j = Nat.add(Nat.mul(s, sl), idx)
233      +m2 = SA.step(r, l, s, idx, p, q, sl, Nat.add(Nat.mul(l, q), j), indep, a2, SA.get(mem, SA.prev_index(l, q, j, Nat.is_eq(j, 0n))), mem)
234      Equal.trans(Nat, SC.length(A.Block, SA.seg_go(rest, Nat.add(idx, 1n), False{}, a2, m2, r, l, s, p, q, sl, mm, t, indep)), SC.length(A.Block, m2), SC.length(A.Block, mem),
235        seg_len(rest, Nat.add(idx, 1n), False{}, a2, m2, r, l, s, p, q, sl, mm, t, indep),
236        step_len(r, l, s, idx, p, q, sl, Nat.add(Nat.mul(l, q), j), indep, a2, SA.get(mem, SA.prev_index(l, q, j, Nat.is_eq(j, 0n))), mem))
237
238# Positions idx .. idx + n - 1 of a segment.
239def seg_eq(+d: Nat, +n: Nat, +idx: Nat, +first: Bool, +addr: A.Block, +mem: List<&2, A.Block>, +r: Nat, +l: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +indep: Bool, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(1n, sl) == True{} : Bool}, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hidx: {Nat.is_le(Nat.add(idx, n), sl) == True{} : Bool}) -> {I.seg_go(n, idx, first, addr, AR.thaw(U32, MEM.mt(d, mem)), r, l, s, p, q, sl, mm, t, indep) == AR.thaw(U32, MEM.mt(d, SA.seg_go(n, idx, first, addr, mem, r, l, s, p, q, sl, mm, t, indep))) : Array<U32>}:
240  match n:
241    case 0n:
242      {==}
243    case 1n+ +rest:
244      +need = Bool.and(indep, Bool.or(first, Nat.is_eq(Nat.mod(idx, 128n), 0n)))
245      +a2i = I.regen(need, addr, r, l, s, mm, t, idx)
246      +a2s = SA.regen(need, addr, r, l, s, mm, t, idx)
247      +j = Nat.add(Nat.mul(s, sl), idx)
248      +cur = Nat.add(Nat.mul(l, q), j)
249      +b0 = Nat.is_eq(j, 0n)
250      +pvi = I.prev_index(l, q, j, b0)
251      +pvs = SA.prev_index(l, q, j, b0)
252      +hi = lt_of_add_succ(idx, rest, sl, hidx)
253      +hq1 = q_pos(q, sl, hq, hsl)
254      +hj = lt_q(q, sl, j, hq, seg_lt(s, sl, idx, hs, hi))
255      +hcur = lt_len(cur, mem, p, q, hlen, lt_mul_add(l, p, j, q, hl, hj))
256      +hpv = lt_len(pvs, mem, p, q, hlen, prev_lt(l, p, q, j, b0, hl, hj, hq1))
257      +pb = SA.get(mem, pvs)
258      +m2 = SA.step(r, l, s, idx, p, q, sl, cur, indep, a2s, pb, mem)
259      +hl2 = step_len(r, l, s, idx, p, q, sl, cur, indep, a2s, pb, mem)
260      +hc2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, 256n), SC.pow2(d)) == True{} : Bool}, SC.length(A.Block, mem), SC.length(A.Block, m2), Equal.sym(Nat, SC.length(A.Block, m2), SC.length(A.Block, mem), hl2), hc)
261      +hlen2 = Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, mem), Nat.mul(p, q), hl2, hlen)
262      -ar = AR.thaw(U32, MEM.mt(d, mem))
263      -goal = AR.thaw(U32, MEM.mt(d, SA.seg_go(rest, Nat.add(idx, 1n), False{}, a2s, m2, r, l, s, p, q, sl, mm, t, indep)))
264      %Equal.sym(A.Block, a2i, a2s, IX.regen_eq(need, addr, r, l, s, mm, t, idx)) : {I.seg_go(rest, Nat.add(idx, 1n), False{}, _, I.step(r, l, s, idx, p, q, sl, cur, indep, _, M.get(pvi, ar)), r, l, s, p, q, sl, mm, t, indep) == goal : Array<U32>}
265      %Equal.sym(Nat, pvi, pvs, IX.prev_index_eq(l, q, j, b0)) : {I.seg_go(rest, Nat.add(idx, 1n), False{}, a2s, I.step(r, l, s, idx, p, q, sl, cur, indep, a2s, M.get(_, ar)), r, l, s, p, q, sl, mm, t, indep) == goal : Array<U32>}
266      %Equal.sym(Array<U32> & A.Block, M.get(pvs, ar), (ar, pb), MEM.get_block(d, mem, pvs, hd, hc, hpv)) : {I.seg_go(rest, Nat.add(idx, 1n), False{}, a2s, I.step(r, l, s, idx, p, q, sl, cur, indep, a2s, _), r, l, s, p, q, sl, mm, t, indep) == goal : Array<U32>}
267      %Equal.sym(Array<U32>, I.step(r, l, s, idx, p, q, sl, cur, indep, a2s, (ar, pb)), AR.thaw(U32, MEM.mt(d, m2)), step_eq(d, mem, r, l, s, idx, p, q, sl, cur, indep, a2s, pb, hd, hc, hlen, hq, hp, hsl, hl, hs, hi, hcur)) : {I.seg_go(rest, Nat.add(idx, 1n), False{}, a2s, _, r, l, s, p, q, sl, mm, t, indep) == goal : Array<U32>}
268      seg_eq(d, rest, Nat.add(idx, 1n), False{}, a2s, m2, r, l, s, p, q, sl, mm, t, indep, hd, hc2, hlen2, hq, hp, hsl, hl, hs, le_shift(idx, rest, sl, hidx))
269
270def start_index_le(+f: Bool, +sl: Nat, +h2: {Nat.is_le(2n, sl) == True{} : Bool}) -> {Nat.is_le(SA.start_index(f), sl) == True{} : Bool}:
271  match f:
272    case True{}:
273      h2
274    case False{}:
275      N.zero_le(sl)
276
277def segment_len(+r: Nat, +s: Nat, +l: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.segment(r, s, l, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
278  +r0 = Nat.is_eq(r, 0n)
279  +st = SA.start_index(Bool.and(r0, Nat.is_eq(s, 0n)))
280  seg_len(Nat.sub(sl, st), st, True{}, SG.zero(), mem, r, l, s, p, q, sl, mm, t, Bool.and(r0, Nat.is_lt(s, 2n)))
281
282# One segment.
283def segment_eq(+d: Nat, +r: Nat, +s: Nat, +l: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}) -> {I.segment(r, s, l, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.segment(r, s, l, p, q, sl, mm, t, mem))) : Array<U32>}:
284  +r0 = Nat.is_eq(r, 0n)
285  +f = Bool.and(r0, Nat.is_eq(s, 0n))
286  +ind = Bool.and(r0, Nat.is_lt(s, 2n))
287  +sti = I.start_index(f)
288  +sts = SA.start_index(f)
289  +hsl1 = N.le_trans(1n, 2n, sl, {==}, hsl)
290  +hidx = N.eq_le(Nat.add(sts, Nat.sub(sl, sts)), sl, N.sub_add(sl, sts, start_index_le(f, sl, hsl)))
291  -ar = AR.thaw(U32, MEM.mt(d, mem))
292  -goal = AR.thaw(U32, MEM.mt(d, SA.segment(r, s, l, p, q, sl, mm, t, mem)))
293  %Equal.sym(Nat, sti, sts, IX.start_index_eq(f)) : {I.seg_go(Nat.sub(sl, _), _, True{}, G.zero(), ar, r, l, s, p, q, sl, mm, t, ind) == goal : Array<U32>}
294  %Equal.sym(A.Block, G.zero(), SG.zero(), BL.zero_correct()) : {I.seg_go(Nat.sub(sl, sts), sts, True{}, _, ar, r, l, s, p, q, sl, mm, t, ind) == goal : Array<U32>}
295  seg_eq(d, Nat.sub(sl, sts), sts, True{}, SG.zero(), mem, r, l, s, p, q, sl, mm, t, ind, hd, hc, hlen, hq, hp, hsl1, hl, hs, hidx)
296
297def lanes_len(+n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.lanes_go(n, l, r, s, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
298  match n:
299    case 0n:
300      {==}
301    case 1n+ +rest:
302      +m2 = SA.segment(r, s, l, p, q, sl, mm, t, mem)
303      Equal.trans(Nat, SC.length(A.Block, SA.lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
304        lanes_len(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2), segment_len(r, s, l, p, q, sl, mm, t, mem))
305
306def keep_c(+d: Nat, +m1: List<&2, A.Block>, +m2: List<&2, A.Block>, +e: {SC.length(A.Block, m2) == SC.length(A.Block, m1) : Nat}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, m1), 256n), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(SC.length(A.Block, m2), 256n), SC.pow2(d)) == True{} : Bool}:
307  L.subst(Nat, z => {Nat.is_le(Nat.mul(z, 256n), SC.pow2(d)) == True{} : Bool}, SC.length(A.Block, m1), SC.length(A.Block, m2), Equal.sym(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), e), hc)
308
309def keep_len(+m1: List<&2, A.Block>, +m2: List<&2, A.Block>, +x: Nat, +e: {SC.length(A.Block, m2) == SC.length(A.Block, m1) : Nat}, +h: {SC.length(A.Block, m1) == x : Nat}) -> {SC.length(A.Block, m2) == x : Nat}:
310  Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), x, e, h)
311
312# The lanes l .. l + n - 1 of a slice.
313def lanes_eq(+d: Nat, +n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hln: {Nat.is_le(Nat.add(l, n), p) == True{} : Bool}) -> {I.lanes_go(n, l, r, s, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.lanes_go(n, l, r, s, p, q, sl, mm, t, mem))) : Array<U32>}:
314  match n:
315    case 0n:
316      {==}
317    case 1n+ +rest:
318      +m2 = SA.segment(r, s, l, p, q, sl, mm, t, mem)
319      +e = segment_len(r, s, l, p, q, sl, mm, t, mem)
320      %Equal.sym(Array<U32>, I.segment(r, s, l, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m2)), segment_eq(d, r, s, l, p, q, sl, mm, t, mem, hd, hc, hlen, hq, hp, hsl, lt_of_add_succ(l, rest, p, hln), hs)) : {I.lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2))) : Array<U32>}
321      lanes_eq(d, rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2, hd, keep_c(d, mem, m2, e, hc), keep_len(mem, m2, Nat.mul(p, q), e, hlen), hq, hp, hsl, hs, le_shift(l, rest, p, hln))
322
323def slices_len(+n: Nat, +s: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.slices_go(n, s, r, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
324  match n:
325    case 0n:
326      {==}
327    case 1n+ +rest:
328      +m2 = SA.lanes_go(p, 0n, r, s, p, q, sl, mm, t, mem)
329      Equal.trans(Nat, SC.length(A.Block, SA.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
330        slices_len(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2), lanes_len(p, 0n, r, s, p, q, sl, mm, t, mem))
331
332# Slices s .. s + n - 1 of a pass.
333def slices_eq(+d: Nat, +n: Nat, +s: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}, +hsn: {Nat.is_le(Nat.add(s, n), 4n) == True{} : Bool}) -> {I.slices_go(n, s, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.slices_go(n, s, r, p, q, sl, mm, t, mem))) : Array<U32>}:
334  match n:
335    case 0n:
336      {==}
337    case 1n+ +rest:
338      +m2 = SA.lanes_go(p, 0n, r, s, p, q, sl, mm, t, mem)
339      +e = lanes_len(p, 0n, r, s, p, q, sl, mm, t, mem)
340      %Equal.sym(Array<U32>, I.lanes_go(p, 0n, r, s, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m2)), lanes_eq(d, p, 0n, r, s, p, q, sl, mm, t, mem, hd, hc, hlen, hq, hp, hsl, lt_of_add_succ(s, rest, 4n, hsn), N.le_refl(p))) : {I.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2))) : Array<U32>}
341      slices_eq(d, rest, Nat.add(s, 1n), r, p, q, sl, mm, t, m2, hd, keep_c(d, mem, m2, e, hc), keep_len(mem, m2, Nat.mul(p, q), e, hlen), hq, hp, hsl, le_shift(s, rest, 4n, hsn))
342
343def passes_len(+n: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.passes_go(n, r, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
344  match n:
345    case 0n:
346      {==}
347    case 1n+ +rest:
348      +m2 = SA.slices_go(4n, 0n, r, p, q, sl, mm, t, mem)
349      Equal.trans(Nat, SC.length(A.Block, SA.passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
350        passes_len(rest, Nat.add(r, 1n), p, q, sl, mm, t, m2), slices_len(4n, 0n, r, p, q, sl, mm, t, mem))
351
352# Passes r .. r + n - 1.
353def passes_eq(+d: Nat, +n: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}) -> {I.passes_go(n, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.passes_go(n, r, p, q, sl, mm, t, mem))) : Array<U32>}:
354  match n:
355    case 0n:
356      {==}
357    case 1n+ +rest:
358      +m2 = SA.slices_go(4n, 0n, r, p, q, sl, mm, t, mem)
359      +e = slices_len(4n, 0n, r, p, q, sl, mm, t, mem)
360      %Equal.sym(Array<U32>, I.slices_go(4n, 0n, r, p, q, sl, mm, t, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m2)), slices_eq(d, 4n, 0n, r, p, q, sl, mm, t, mem, hd, hc, hlen, hq, hp, hsl, N.le_refl(4n))) : {I.passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, m2))) : Array<U32>}
361      passes_eq(d, rest, Nat.add(r, 1n), p, q, sl, mm, t, m2, hd, keep_c(d, mem, m2, e, hc), keep_len(mem, m2, Nat.mul(p, q), e, hlen), hq, hp, hsl)