proofs/crypto/argon2/memory.bend

bend-collections-laws-crypto@1.0.0.0 · 606 lines · 62 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/u32.bend as U
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/src/crypto/blake/blake2b/types.bend as T
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend as SB
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
13import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
14import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
15
16# The implementation's memory (a packed Array<U32> of 2^d words, block b at
17# words 256 b .. 256 b + 255) against the specification's (a list of blocks).
18#
19# Arrays are linear, so the relation is stated through proofs/lib/array.bend's
20# mirror trees: the memory of the list mem is thaw(mt(d, mem)), the perfect
21# tree of depth d whose words are mem's blocks one after the other, then
22# zeros. Reading block b with 256 Array.get and writing it with 256
23# Array.set (Base's own algorithms, proved in proofs/lib/array.bend) is then
24# get and update on mem.
25
26# ---------------------------------------------------------------- lists
27
28def nthv(ws: List<&2, U32>, i: Nat) -> U32:
29  Maybe.default(&2, U32, SC.nth(U32, ws, i), 0)
30
31def take_drop(+xs: List<&2, U32>, +n: Nat) -> {SC.append(U32, SC.take(U32, xs, n), SC.drop(U32, xs, n)) == xs : List<&2, U32>}:
32  match xs n:
33    case Nil{} _:
34      {==}
35    case Con{h, t} 0n:
36      {==}
37    case Con{+h, +t} 1n+ +p:
38      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{h, z}, SC.append(U32, SC.take(U32, t, p), SC.drop(U32, t, p)), t, take_drop(t, p))
39
40def zsub(+n: Nat) -> {Nat.sub(0n, n) == 0n : Nat}:
41  match n:
42    case 0n:
43      {==}
44    case 1n+p:
45      {==}
46
47def length_drop(+xs: List<&2, U32>, +n: Nat) -> {SC.length(U32, SC.drop(U32, xs, n)) == Nat.sub(SC.length(U32, xs), n) : Nat}:
48  match xs n:
49    case Nil{} _:
50      Equal.sym(Nat, Nat.sub(0n, n), 0n, zsub(n))
51    case Con{h, t} 0n:
52      {==}
53    case Con{+h, +t} 1n+ +p:
54      length_drop(t, p)
55
56def take_all(+xs: List<&2, U32>, +n: Nat, +h: {SC.length(U32, xs) == n : Nat}) -> {SC.take(U32, xs, n) == xs : List<&2, U32>}:
57  match xs n:
58    case Nil{} _:
59      {==}
60    case Con{h1, t} 0n:
61      Empty.absurd({SC.take(U32, Con{h1, t}, 0n) == Con{h1, t} : List<&2, U32>}, N.succ_zero(SC.length(U32, t), h))
62    case Con{+h1, +t} 1n+ +p:
63      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{h1, z}, SC.take(U32, t, p), t, take_all(t, p, N.succ_inj(SC.length(U32, t), p, h)))
64
65def drop_zero(+ys: List<&2, U32>) -> {SC.drop(U32, ys, 0n) == ys : List<&2, U32>}:
66  match ys:
67    case Nil{}:
68      {==}
69    case Con{h, t}:
70      {==}
71
72def drop_all(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +h: {SC.length(U32, xs) == n : Nat}) -> {SC.drop(U32, SC.append(U32, xs, ys), n) == ys : List<&2, U32>}:
73  match xs n:
74    case Nil{} 0n:
75      drop_zero(ys)
76    case Nil{} 1n+p:
77      Empty.absurd({SC.drop(U32, ys, 1n+p) == ys : List<&2, U32>}, N.zero_succ(p, h))
78    case Con{h1, t} 0n:
79      Empty.absurd({SC.drop(U32, SC.append(U32, Con{h1, t}, ys), 0n) == ys : List<&2, U32>}, N.succ_zero(SC.length(U32, t), h))
80    case Con{+h1, +t} 1n+ +p:
81      drop_all(t, ys, p, N.succ_inj(SC.length(U32, t), p, h))
82
83# ---------------------------------------------------------------- mirror trees of word lists
84
85# The perfect tree of depth d holding ws (padded by zeros, truncated at 2^d).
86def tree(d: Nat, +ws: List<&2, U32>) -> AR.Tree<U32>:
87  match d:
88    case 0n:
89      AR.TLeaf{nthv(ws, 0n)}
90    case 1n+ +p:
91      AR.TNode{tree(p, SC.take(U32, ws, SC.pow2(p))), tree(p, SC.drop(U32, ws, SC.pow2(p)))}
92
93def tree_perfect(+d: Nat, +ws: List<&2, U32>) -> {AR.perfect(U32, d, tree(d, ws)) == True{} : Bool}:
94  match d:
95    case 0n:
96      {==}
97    case 1n+ +p:
98      L.and_intro(AR.perfect(U32, p, tree(p, SC.take(U32, ws, SC.pow2(p)))), AR.perfect(U32, p, tree(p, SC.drop(U32, ws, SC.pow2(p)))), tree_perfect(p, SC.take(U32, ws, SC.pow2(p))), tree_perfect(p, SC.drop(U32, ws, SC.pow2(p))))
99
100def leaf_slots(+ws: List<&2, U32>, +h: {SC.length(U32, ws) == 1n : Nat}) -> {Con{nthv(ws, 0n), Nil{}} == ws : List<&2, U32>}:
101  match ws:
102    case Nil{}:
103      Empty.absurd({Con{nthv(Nil{}, 0n), Nil{}} == Nil{} : List<&2, U32>}, N.zero_succ(0n, h))
104    case Con{x, Nil{}}:
105      {==}
106    case Con{x, Con{y, r}}:
107      Empty.absurd({Con{nthv(Con{x, Con{y, r}}, 0n), Nil{}} == Con{x, Con{y, r}} : List<&2, U32>}, N.succ_zero(SC.length(U32, r), N.succ_inj(1n+SC.length(U32, r), 0n, h)))
108
109def double_sub(+x: Nat) -> {Nat.sub(Nat.double(x), x) == x : Nat}:
110  %Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)) : {Nat.sub(_, x) == x : Nat}
111  N.add_sub_cancel(x, x)
112
113def pow2_le_succ(+p: Nat) -> {Nat.is_le(SC.pow2(p), SC.pow2(1n+p)) == True{} : Bool}:
114  N.lt_le(SC.pow2(p), SC.pow2(1n+p), N.pow2_lt_succ(p))
115
116# The words of tree(d, ws) are ws, for 2^d words.
117def tree_slots(+d: Nat, +ws: List<&2, U32>, +h: {SC.length(U32, ws) == SC.pow2(d) : Nat}) -> {AR.slots(U32, tree(d, ws)) == ws : List<&2, U32>}:
118  match d:
119    case 0n:
120      leaf_slots(ws, h)
121    case 1n+ +p:
122      +k = SC.pow2(p)
123      +ht = LL.sc_length_take(U32, ws, k, L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, SC.pow2(1n+p), SC.length(U32, ws), Equal.sym(Nat, SC.length(U32, ws), SC.pow2(1n+p), h), pow2_le_succ(p)))
124      +hd = Equal.trans(Nat, SC.length(U32, SC.drop(U32, ws, k)), Nat.sub(SC.length(U32, ws), k), k, length_drop(ws, k),
125        Equal.trans(Nat, Nat.sub(SC.length(U32, ws), k), Nat.sub(Nat.double(k), k), k, Equal.cong(Nat, Nat, z => Nat.sub(z, k), SC.length(U32, ws), Nat.double(k), h), double_sub(k)))
126      Equal.trans(List<&2, U32>, SC.append(U32, AR.slots(U32, tree(p, SC.take(U32, ws, k))), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), SC.drop(U32, ws, k)), ws,
127        Equal.trans(List<&2, U32>, SC.append(U32, AR.slots(U32, tree(p, SC.take(U32, ws, k))), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), SC.drop(U32, ws, k)),
128          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), AR.slots(U32, tree(p, SC.take(U32, ws, k))), SC.take(U32, ws, k), tree_slots(p, SC.take(U32, ws, k), ht)),
129          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, SC.take(U32, ws, k), z), AR.slots(U32, tree(p, SC.drop(U32, ws, k))), SC.drop(U32, ws, k), tree_slots(p, SC.drop(U32, ws, k), hd))),
130        take_drop(ws, k))
131
132# A perfect tree is the tree of its words.
133def tree_ext(+d: Nat, +t: AR.Tree<U32>, +pf: {AR.perfect(U32, d, t) == True{} : Bool}) -> {t == tree(d, AR.slots(U32, t)) : AR.Tree<U32>}:
134  match d t:
135    case 0n AR.TLeaf{x}:
136      {==}
137    case 0n AR.TNode{l, r}:
138      Empty.absurd({AR.TNode{l, r} == tree(0n, AR.slots(U32, AR.TNode{l, r})) : AR.Tree<U32>}, L.false_true(pf))
139    case 1n+p AR.TLeaf{x}:
140      Empty.absurd({AR.TLeaf{x} == tree(1n+p, AR.slots(U32, AR.TLeaf{x})) : AR.Tree<U32>}, L.false_true(pf))
141    case 1n+ +p AR.TNode{+l, +r}:
142      +pl = AR.pf_left(U32, p, l, r, pf)
143      +pr = AR.pf_right(U32, p, l, r, pf)
144      +sl = AR.slots(U32, l)
145      +sr = AR.slots(U32, r)
146      +hl = AR.slots_length(U32, p, l, pl)
147      +et = Equal.trans(List<&2, U32>, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p)), SC.take(U32, sl, SC.pow2(p)), sl,
148        LL.sc_take_append_left(U32, sl, sr, SC.pow2(p), N.eq_le(SC.pow2(p), SC.length(U32, sl), Equal.sym(Nat, SC.length(U32, sl), SC.pow2(p), hl))),
149        take_all(sl, SC.pow2(p), hl))
150      +ed = drop_all(sl, sr, SC.pow2(p), hl)
151      Equal.trans(AR.Tree<U32>, AR.TNode{l, r}, AR.TNode{tree(p, sl), tree(p, sr)}, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))},
152        Equal.trans(AR.Tree<U32>, AR.TNode{l, r}, AR.TNode{tree(p, sl), r}, AR.TNode{tree(p, sl), tree(p, sr)},
153          Equal.cong(AR.Tree<U32>, AR.Tree<U32>, z => AR.TNode{z, r}, l, tree(p, sl), tree_ext(p, l, pl)),
154          Equal.cong(AR.Tree<U32>, AR.Tree<U32>, z => AR.TNode{tree(p, sl), z}, r, tree(p, sr), tree_ext(p, r, pr))),
155        Equal.sym(AR.Tree<U32>, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, sr)},
156          Equal.trans(AR.Tree<U32>, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, sr)},
157            Equal.cong(List<&2, U32>, AR.Tree<U32>, z => AR.TNode{tree(p, z), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p)), sl, et),
158            Equal.cong(List<&2, U32>, AR.Tree<U32>, z => AR.TNode{tree(p, sl), tree(p, z)}, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)), sr, ed))))
159
160# ---------------------------------------------------------------- one word
161
162def nth_some(+xs: List<&2, U32>, +j: Nat, +h: {Nat.is_lt(j, SC.length(U32, xs)) == True{} : Bool}) -> {SC.nth(U32, xs, j) == Some{nthv(xs, j)} : Maybe<&2, U32>}:
163  match xs j:
164    case Nil{} _:
165      Empty.absurd({SC.nth(U32, Nil{}, j) == Some{nthv(Nil{}, j)} : Maybe<&2, U32>}, N.lt_zero_absurd(j, h))
166    case Con{x, t} 0n:
167      {==}
168    case Con{x, +t} 1n+ +p:
169      nth_some(t, p, h)
170
171def le32(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {Nat.is_le(d, 32n) == True{} : Bool}:
172  N.lt_le(d, 32n, hd)
173
174# Array.get at word j of the tree of ws.
175def get_word(+d: Nat, +ws: List<&2, U32>, +j: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hl: {SC.length(U32, ws) == SC.pow2(d) : Nat}, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, tree(d, ws)), U32.from_nat(j)) == (AR.thaw(U32, tree(d, ws)), nthv(ws, j)) : Array<U32> & U32}:
176  +t = tree(d, ws)
177  +ej = U.to_nat_from_nat(j, d, le32(d, hd), hj)
178  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej), hj)
179  +hn = nth_some(ws, j, L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.pow2(d), SC.length(U32, ws), Equal.sym(Nat, SC.length(U32, ws), SC.pow2(d), hl), hj))
180  +hx = L.subst(List<&2, U32>, z => {SC.nth(U32, z, U32.to_nat(U32.from_nat(j))) == Some{nthv(ws, j)} : Maybe<&2, U32>}, ws, AR.slots(U32, t), Equal.sym(List<&2, U32>, AR.slots(U32, t), ws, tree_slots(d, ws, hl)),
181    L.subst(Nat, z => {SC.nth(U32, ws, z) == Some{nthv(ws, j)} : Maybe<&2, U32>}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej), hn))
182  AR.get(U32, d, t, U32.from_nat(j), nthv(ws, j), hd, hi, hx, tree_perfect(d, ws))
183
184# ---------------------------------------------------------------- reading a run of words
185
186def slice(ws: List<&2, U32>, +base: Nat, n: Nat) -> List<&2, U32>:
187  SC.take(U32, SC.drop(U32, ws, base), n)
188
189def nth_drop(+ws: List<&2, U32>, +base: Nat, +k: Nat) -> {nthv(SC.drop(U32, ws, base), k) == nthv(ws, Nat.add(base, k)) : U32}:
190  match ws base:
191    case Nil{} _:
192      {==}
193    case Con{h, t} 0n:
194      {==}
195    case Con{h, +t} 1n+ +b:
196      nth_drop(t, b, k)
197
198def take_snoc(+ys: List<&2, U32>, +k: Nat, +h: {Nat.is_lt(k, SC.length(U32, ys)) == True{} : Bool}) -> {SC.take(U32, ys, 1n+k) == SC.append(U32, SC.take(U32, ys, k), Con{nthv(ys, k), Nil{}}) : List<&2, U32>}:
199  match ys k:
200    case Nil{} _:
201      Empty.absurd({SC.take(U32, Nil{}, 1n+k) == SC.append(U32, SC.take(U32, Nil{}, k), Con{nthv(Nil{}, k), Nil{}}) : List<&2, U32>}, N.lt_zero_absurd(k, h))
202    case Con{+x, +t} 0n:
203      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, SC.take(U32, t, 0n), Nil{}, LL.sc_take_zero(U32, t))
204    case Con{+x, +t} 1n+ +p:
205      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, SC.take(U32, t, 1n+p), SC.append(U32, SC.take(U32, t, p), Con{nthv(t, p), Nil{}}), take_snoc(t, p, h))
206
207def lt_sub(+base: Nat, +k: Nat, +n: Nat, +h: {Nat.is_lt(Nat.add(base, k), n) == True{} : Bool}) -> {Nat.is_lt(k, Nat.sub(n, base)) == True{} : Bool}:
208  match base n:
209    case 0n _:
210      L.subst(Nat, z => {Nat.is_lt(k, z) == True{} : Bool}, n, Nat.sub(n, 0n), Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)), h)
211    case 1n+b 0n:
212      Empty.absurd({Nat.is_lt(k, Nat.sub(0n, 1n+b)) == True{} : Bool}, N.lt_zero_absurd(Nat.add(1n+b, k), h))
213    case 1n+ +b 1n+ +m:
214      lt_sub(b, k, m, h)
215
216# slice(ws, base, k + 1) is slice(ws, base, k) and word base + k.
217def slice_snoc(+ws: List<&2, U32>, +base: Nat, +k: Nat, +h: {Nat.is_lt(Nat.add(base, k), SC.length(U32, ws)) == True{} : Bool}) -> {slice(ws, base, 1n+k) == SC.append(U32, slice(ws, base, k), Con{nthv(ws, Nat.add(base, k)), Nil{}}) : List<&2, U32>}:
218  +ys = SC.drop(U32, ws, base)
219  +hk = L.subst(Nat, z => {Nat.is_lt(k, z) == True{} : Bool}, Nat.sub(SC.length(U32, ws), base), SC.length(U32, ys), Equal.sym(Nat, SC.length(U32, ys), Nat.sub(SC.length(U32, ws), base), length_drop(ws, base)), lt_sub(base, k, SC.length(U32, ws), h))
220  Equal.trans(List<&2, U32>, SC.take(U32, ys, 1n+k), SC.append(U32, SC.take(U32, ys, k), Con{nthv(ys, k), Nil{}}), SC.append(U32, SC.take(U32, ys, k), Con{nthv(ws, Nat.add(base, k)), Nil{}}),
221    take_snoc(ys, k, hk),
222    Equal.cong(U32, List<&2, U32>, z => SC.append(U32, SC.take(U32, ys, k), Con{z, Nil{}}), nthv(ys, k), nthv(ws, Nat.add(base, k)), nth_drop(ws, base, k)))
223
224def slice_one(+ws: List<&2, U32>, +base: Nat, +h: {Nat.is_lt(base, SC.length(U32, ws)) == True{} : Bool}) -> {slice(ws, base, 1n) == Con{nthv(ws, base), Nil{}} : List<&2, U32>}:
225  match ws base:
226    case Nil{} _:
227      Empty.absurd({slice(Nil{}, base, 1n) == Con{nthv(Nil{}, base), Nil{}} : List<&2, U32>}, N.lt_zero_absurd(base, h))
228    case Con{+x, +t} 0n:
229      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, SC.take(U32, t, 0n), Nil{}, LL.sc_take_zero(U32, t))
230    case Con{x, +t} 1n+ +b:
231      slice_one(t, b, h)
232
233def append_cons(+xs: List<&2, U32>, +w: U32, +acc: List<&2, U32>) -> {SC.append(U32, SC.append(U32, xs, Con{w, Nil{}}), acc) == SC.append(U32, xs, Con{w, acc}) : List<&2, U32>}:
234  LL.append_assoc(U32, xs, Con{w, Nil{}}, acc)
235
236def lt_pred(+base: Nat, +p: Nat, +n: Nat, +h: {Nat.is_lt(Nat.add(base, 1n+p), n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(base, p), n) == True{} : Bool}:
237  N.lt_trans(Nat.add(base, p), Nat.add(base, 1n+p), n, L.subst(Nat, z => {Nat.is_lt(Nat.add(base, p), z) == True{} : Bool}, 1n+Nat.add(base, p), Nat.add(base, 1n+p), Equal.sym(Nat, Nat.add(base, 1n+p), 1n+Nat.add(base, p), N.add_succ(base, p)), N.lt_succ(Nat.add(base, p))), h)
238
239def pred_add(+base: Nat, +p: Nat) -> {Nat.sub(Nat.add(base, 1n+p), 1n) == Nat.add(base, p) : Nat}:
240  %Equal.sym(Nat, Nat.add(base, 1n+p), 1n+Nat.add(base, p), N.add_succ(base, p)) : {Nat.sub(_, 1n) == Nat.add(base, p) : Nat}
241  N.sub_zero(Nat.add(base, p))
242
243# M.rd reads words base + n down to base (onto acc), leaving the memory unchanged.
244def rd_words(+d: Nat, +ws: List<&2, U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hl: {SC.length(U32, ws) == SC.pow2(d) : Nat}, +n: Nat, +base: Nat, +acc: List<&2, U32>, +h: {Nat.is_lt(Nat.add(base, n), SC.pow2(d)) == True{} : Bool}) -> {M.rd(n, Nat.add(base, n), acc, (AR.thaw(U32, tree(d, ws)), nthv(ws, Nat.add(base, n)))) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 1n+n), acc)) : Array<U32> & List<&2, U32>}:
245  match n:
246    case 0n:
247      +hw = L.subst(Nat, z => {Nat.is_lt(Nat.add(base, 0n), z) == True{} : Bool}, SC.pow2(d), SC.length(U32, ws), Equal.sym(Nat, SC.length(U32, ws), SC.pow2(d), hl), h)
248      %Equal.sym(Nat, Nat.add(base, 0n), base, N.add_zero(base)) : {(AR.thaw(U32, tree(d, ws)), Con{nthv(ws, _), acc}) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 1n), acc)) : Array<U32> & List<&2, U32>}
249      %Equal.sym(List<&2, U32>, slice(ws, base, 1n), Con{nthv(ws, base), Nil{}}, slice_one(ws, base, L.subst(Nat, z => {Nat.is_lt(z, SC.length(U32, ws)) == True{} : Bool}, Nat.add(base, 0n), base, N.add_zero(base), hw))) : {(AR.thaw(U32, tree(d, ws)), Con{nthv(ws, base), acc}) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, _, acc)) : Array<U32> & List<&2, U32>}
250      {==}
251    case 1n+ +p:
252      +hw = L.subst(Nat, z => {Nat.is_lt(Nat.add(base, 1n+p), z) == True{} : Bool}, SC.pow2(d), SC.length(U32, ws), Equal.sym(Nat, SC.length(U32, ws), SC.pow2(d), hl), h)
253      +w = nthv(ws, Nat.add(base, 1n+p))
254      +j = Nat.add(base, p)
255      +hj = lt_pred(base, p, SC.pow2(d), h)
256      %Equal.sym(Nat, Nat.sub(Nat.add(base, 1n+p), 1n), Nat.add(base, p), pred_add(base, p)) : {M.rd(p, _, Con{w, acc}, Array.get(U32, AR.thaw(U32, tree(d, ws)), U32.from_nat(_))) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 2n+p), acc)) : Array<U32> & List<&2, U32>}
257      %Equal.sym(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tree(d, ws)), U32.from_nat(j)), (AR.thaw(U32, tree(d, ws)), nthv(ws, j)), get_word(d, ws, j, hd, hl, hj)) : {M.rd(p, j, Con{w, acc}, _) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 2n+p), acc)) : Array<U32> & List<&2, U32>}
258      %Equal.sym(Array<U32> & List<&2, U32>, M.rd(p, j, Con{w, acc}, (AR.thaw(U32, tree(d, ws)), nthv(ws, j))), (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 1n+p), Con{w, acc})), rd_words(d, ws, hd, hl, p, base, Con{w, acc}, hj)) : {_ == (AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 2n+p), acc)) : Array<U32> & List<&2, U32>}
259      %Equal.sym(List<&2, U32>, slice(ws, base, 2n+p), SC.append(U32, slice(ws, base, 1n+p), Con{w, Nil{}}), slice_snoc(ws, base, 1n+p, hw)) : {(AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 1n+p), Con{w, acc})) == (AR.thaw(U32, tree(d, ws)), SC.append(U32, _, acc)) : Array<U32> & List<&2, U32>}
260      %Equal.sym(List<&2, U32>, SC.append(U32, SC.append(U32, slice(ws, base, 1n+p), Con{w, Nil{}}), acc), SC.append(U32, slice(ws, base, 1n+p), Con{w, acc}), append_cons(slice(ws, base, 1n+p), w, acc)) : {(AR.thaw(U32, tree(d, ws)), SC.append(U32, slice(ws, base, 1n+p), Con{w, acc})) == (AR.thaw(U32, tree(d, ws)), _) : Array<U32> & List<&2, U32>}
261      {==}
262
263# ---------------------------------------------------------------- the memory of a list of blocks
264
265def flat(mem: List<&2, A.Block>) -> List<&2, U32>:
266  match mem:
267    case Nil{}:
268      Nil{}
269    case b <> rest:
270      SC.append(U32, SB.words(b), flat(rest))
271
272def pad(+d: Nat, +n: Nat) -> List<&2, U32>:
273  SC.replicate(U32, Nat.sub(SC.pow2(d), Nat.mul(n, 256n)), 0)
274
275# The words of the memory mem in an array of 2^d words.
276def W(+d: Nat, +mem: List<&2, A.Block>) -> List<&2, U32>:
277  SC.append(U32, flat(mem), pad(d, SC.length(A.Block, mem)))
278
279def mt(+d: Nat, +mem: List<&2, A.Block>) -> AR.Tree<U32>:
280  tree(d, W(d, mem))
281
282def rw_len(+v: T.State) -> {SC.length(U32, SB.row_words(v)) == 32n : Nat}:
283  match v:
284    case T.V{T.W{l0, h0}, T.W{l1, h1}, T.W{l2, h2}, T.W{l3, h3}, T.W{l4, h4}, T.W{l5, h5}, T.W{l6, h6}, T.W{l7, h7}, T.W{l8, h8}, T.W{l9, h9}, T.W{l10, h10}, T.W{l11, h11}, T.W{l12, h12}, T.W{l13, h13}, T.W{l14, h14}, T.W{l15, h15}}:
285      {==}
286
287def len_app(+a: List<&2, U32>, +b: List<&2, U32>) -> {SC.length(U32, SB.app(a, b)) == Nat.add(SC.length(U32, a), SC.length(U32, b)) : Nat}:
288  match a:
289    case Nil{}:
290      {==}
291    case +x <> +r:
292      Equal.cong(Nat, Nat, z => 1n+z, SC.length(U32, SB.app(r, b)), Nat.add(SC.length(U32, r), SC.length(U32, b)), len_app(r, b))
293
294# One more row: 32 more words.
295def len_row(+v: T.State, +rest: List<&2, U32>) -> {SC.length(U32, SB.app(SB.row_words(v), rest)) == Nat.add(32n, SC.length(U32, rest)) : Nat}:
296  %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(v), rest)), Nat.add(SC.length(U32, SB.row_words(v)), SC.length(U32, rest)), len_app(SB.row_words(v), rest)) : {_ == Nat.add(32n, SC.length(U32, rest)) : Nat}
297  %Equal.sym(Nat, SC.length(U32, SB.row_words(v)), 32n, rw_len(v)) : {Nat.add(_, SC.length(U32, rest)) == Nat.add(32n, SC.length(U32, rest)) : Nat}
298  {==}
299
300def words_len(+b: A.Block) -> {SC.length(U32, SB.words(b)) == 256n : Nat}:
301  match b:
302    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
303      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r0), SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), len_row(r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))) : {_ == 256n : Nat}
304      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), len_row(r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))) : {Nat.add(32n, _) == 256n : Nat}
305      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), len_row(r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))) : {Nat.add(32n, Nat.add(32n, _)) == 256n : Nat}
306      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), len_row(r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, _))) == 256n : Nat}
307      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), len_row(r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _)))) == 256n : Nat}
308      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), len_row(r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _))))) == 256n : Nat}
309      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r7), Nil{}))), len_row(r6, SB.app(SB.row_words(r7), Nil{}))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _)))))) == 256n : Nat}
310      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r7), Nil{})), Nat.add(32n, SC.length(U32, Nil{})), len_row(r7, Nil{})) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _))))))) == 256n : Nat}
311      {==}
312
313def row_rw(+v: T.State, +rest: List<&2, U32>) -> {SB.row(SB.app(SB.row_words(v), rest)) == (v, rest) : T.State & List<&2, U32>}:
314  match v:
315    case T.V{T.W{l0, h0}, T.W{l1, h1}, T.W{l2, h2}, T.W{l3, h3}, T.W{l4, h4}, T.W{l5, h5}, T.W{l6, h6}, T.W{l7, h7}, T.W{l8, h8}, T.W{l9, h9}, T.W{l10, h10}, T.W{l11, h11}, T.W{l12, h12}, T.W{l13, h13}, T.W{l14, h14}, T.W{l15, h15}}:
316      {==}
317
318def rows8_words(+b: A.Block) -> {SB.rows8(SB.words(b)) == b : A.Block}:
319  match b:
320    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
321      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r0), SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), (r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), row_rw(r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))) : {SB.rows8_0(_) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
322      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), (r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), row_rw(r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))) : {SB.rows8_1(r0, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
323      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), (r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), row_rw(r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))) : {SB.rows8_2(r0, r1, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
324      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), (r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), row_rw(r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))) : {SB.rows8_3(r0, r1, r2, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
325      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), (r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), row_rw(r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))) : {SB.rows8_4(r0, r1, r2, r3, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
326      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), (r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), row_rw(r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))) : {SB.rows8_5(r0, r1, r2, r3, r4, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
327      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), (r6, SB.app(SB.row_words(r7), Nil{})), row_rw(r6, SB.app(SB.row_words(r7), Nil{}))) : {SB.rows8_6(r0, r1, r2, r3, r4, r5, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
328      %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r7), Nil{})), (r7, Nil{}), row_rw(r7, Nil{})) : {SB.rows8_7(r0, r1, r2, r3, r4, r5, r6, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
329      {==}
330
331def flat_len(+mem: List<&2, A.Block>) -> {SC.length(U32, flat(mem)) == Nat.mul(SC.length(A.Block, mem), 256n) : Nat}:
332  match mem:
333    case Nil{}:
334      {==}
335    case +b <> +rest:
336      Equal.trans(Nat, SC.length(U32, SC.append(U32, SB.words(b), flat(rest))), Nat.add(SC.length(U32, SB.words(b)), SC.length(U32, flat(rest))), Nat.add(256n, Nat.mul(SC.length(A.Block, rest), 256n)),
337        LL.length_append(U32, SB.words(b), flat(rest)),
338        Equal.trans(Nat, Nat.add(SC.length(U32, SB.words(b)), SC.length(U32, flat(rest))), Nat.add(256n, SC.length(U32, flat(rest))), Nat.add(256n, Nat.mul(SC.length(A.Block, rest), 256n)),
339          Equal.cong(Nat, Nat, z => Nat.add(z, SC.length(U32, flat(rest))), SC.length(U32, SB.words(b)), 256n, words_len(b)),
340          Equal.cong(Nat, Nat, z => Nat.add(256n, z), SC.length(U32, flat(rest)), Nat.mul(SC.length(A.Block, rest), 256n), flat_len(rest))))
341
342def W_len(+d: Nat, +mem: List<&2, A.Block>, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}) -> {SC.length(U32, W(d, mem)) == SC.pow2(d) : Nat}:
343  +n = Nat.mul(SC.length(A.Block, mem), 256n)
344  Equal.trans(Nat, SC.length(U32, W(d, mem)), Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), SC.pow2(d),
345    LL.length_append(U32, flat(mem), pad(d, SC.length(A.Block, mem))),
346    Equal.trans(Nat, Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, Nat.sub(SC.pow2(d), n)), SC.pow2(d),
347      Equal.trans(Nat, Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, Nat.sub(SC.pow2(d), n)),
348        Equal.cong(Nat, Nat, z => Nat.add(z, SC.length(U32, pad(d, SC.length(A.Block, mem)))), SC.length(U32, flat(mem)), n, flat_len(mem)),
349        Equal.cong(Nat, Nat, z => Nat.add(n, z), SC.length(U32, pad(d, SC.length(A.Block, mem))), Nat.sub(SC.pow2(d), n), LL.length_replicate(U32, Nat.sub(SC.pow2(d), n), 0))),
350      N.sub_add(SC.pow2(d), n, hc)))
351
352# ---------------------------------------------------------------- reading block b
353
354def drop_append_add(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +k: Nat, +h: {SC.length(U32, xs) == n : Nat}) -> {SC.drop(U32, SC.append(U32, xs, ys), Nat.add(n, k)) == SC.drop(U32, ys, k) : List<&2, U32>}:
355  match xs n:
356    case Nil{} 0n:
357      {==}
358    case Nil{} 1n+p:
359      Empty.absurd({SC.drop(U32, ys, Nat.add(1n+p, k)) == SC.drop(U32, ys, k) : List<&2, U32>}, N.zero_succ(p, h))
360    case Con{x, t} 0n:
361      Empty.absurd({SC.drop(U32, SC.append(U32, Con{x, t}, ys), k) == SC.drop(U32, ys, k) : List<&2, U32>}, N.succ_zero(SC.length(U32, t), h))
362    case Con{x, +t} 1n+ +p:
363      drop_append_add(t, ys, p, k, N.succ_inj(SC.length(U32, t), p, h))
364
365def drop_append_le(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +h: {Nat.is_le(n, SC.length(U32, xs)) == True{} : Bool}) -> {SC.drop(U32, SC.append(U32, xs, ys), n) == SC.append(U32, SC.drop(U32, xs, n), ys) : List<&2, U32>}:
366  match xs n:
367    case Nil{} 0n:
368      Equal.trans(List<&2, U32>, SC.drop(U32, ys, 0n), ys, SC.append(U32, SC.drop(U32, Nil{}, 0n), ys), drop_zero(ys), {==})
369    case Nil{} 1n+p:
370      Empty.absurd({SC.drop(U32, ys, 1n+p) == SC.append(U32, SC.drop(U32, Nil{}, 1n+p), ys) : List<&2, U32>}, L.false_true(h))
371    case Con{x, t} 0n:
372      {==}
373    case Con{x, +t} 1n+ +p:
374      drop_append_le(t, ys, p, h)
375
376# The 256 words of block b of the flattened blocks.
377def flat_slice(+mem: List<&2, A.Block>, +b: Nat, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {slice(flat(mem), Nat.mul(b, 256n), 256n) == SB.words(SA.get(mem, b)) : List<&2, U32>}:
378  match mem b:
379    case Nil{} _:
380      Empty.absurd({slice(Nil{}, Nat.mul(b, 256n), 256n) == SB.words(SA.get(Nil{}, b)) : List<&2, U32>}, N.lt_zero_absurd(b, hb))
381    case +x <> +rest 0n:
382      +e1 = drop_zero(SC.append(U32, SB.words(x), flat(rest)))
383      +e2 = LL.sc_take_append_left(U32, SB.words(x), flat(rest), 256n, N.eq_le(256n, SC.length(U32, SB.words(x)), Equal.sym(Nat, SC.length(U32, SB.words(x)), 256n, words_len(x))))
384      +e3 = take_all(SB.words(x), 256n, words_len(x))
385      Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), 0n), 256n), SC.take(U32, SC.append(U32, SB.words(x), flat(rest)), 256n), SB.words(x),
386        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), 0n), SC.append(U32, SB.words(x), flat(rest)), e1),
387        Equal.trans(List<&2, U32>, SC.take(U32, SC.append(U32, SB.words(x), flat(rest)), 256n), SC.take(U32, SB.words(x), 256n), SB.words(x), e2, e3))
388    case +x <> +rest 1n+ +c:
389      Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), Nat.add(256n, Nat.mul(c, 256n))), 256n), slice(flat(rest), Nat.mul(c, 256n), 256n), SB.words(SA.get(rest, c)),
390        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, SB.words(x), flat(rest)), Nat.add(256n, Nat.mul(c, 256n))), SC.drop(U32, flat(rest), Nat.mul(c, 256n)), drop_append_add(SB.words(x), flat(rest), 256n, Nat.mul(c, 256n), words_len(x))),
391        flat_slice(rest, c, hb))
392
393def mul_lt(+b: Nat, +n: Nat, +hb: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_le(Nat.add(Nat.mul(b, 256n), 256n), Nat.mul(n, 256n)) == True{} : Bool}:
394  match b n:
395    case _ 0n:
396      Empty.absurd({Nat.is_le(Nat.add(Nat.mul(b, 256n), 256n), 0n) == True{} : Bool}, N.lt_zero_absurd(b, hb))
397    case 0n 1n+m:
398      N.le_add_right(256n, Nat.mul(m, 256n))
399    case 1n+ +c 1n+ +m:
400      %Equal.sym(Nat, Nat.add(Nat.add(256n, Nat.mul(c, 256n)), 256n), Nat.add(256n, Nat.add(Nat.mul(c, 256n), 256n)), NA.add_assoc(256n, Nat.mul(c, 256n), 256n)) : {Nat.is_le(_, Nat.add(256n, Nat.mul(m, 256n))) == True{} : Bool}
401      N.le_add_left(Nat.add(Nat.mul(c, 256n), 256n), Nat.mul(m, 256n), 256n, mul_lt(c, m, hb))
402
403def le_sub(+base: Nat, +k: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(base, k), n) == True{} : Bool}) -> {Nat.is_le(k, Nat.sub(n, base)) == True{} : Bool}:
404  match base n:
405    case 0n _:
406      L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, n, Nat.sub(n, 0n), Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)), h)
407    case 1n+b 0n:
408      Empty.absurd({Nat.is_le(k, Nat.sub(0n, 1n+b)) == True{} : Bool}, L.false_true(h))
409    case 1n+ +b 1n+ +m:
410      le_sub(b, k, m, h)
411
412def slice_W(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {slice(W(d, mem), Nat.mul(b, 256n), 256n) == SB.words(SA.get(mem, b)) : List<&2, U32>}:
413  +F = flat(mem)
414  +P = pad(d, SC.length(A.Block, mem))
415  +base = Nat.mul(b, 256n)
416  +hn = mul_lt(b, SC.length(A.Block, mem), hb)
417  +hfl = Equal.sym(Nat, SC.length(U32, F), Nat.mul(SC.length(A.Block, mem), 256n), flat_len(mem))
418  +hle = N.le_trans(base, Nat.add(base, 256n), SC.length(U32, F), N.le_add_right(base, 256n), L.subst(Nat, z => {Nat.is_le(Nat.add(base, 256n), z) == True{} : Bool}, Nat.mul(SC.length(A.Block, mem), 256n), SC.length(U32, F), hfl, hn))
419  +h256 = L.subst(Nat, z => {Nat.is_le(256n, z) == True{} : Bool}, Nat.sub(SC.length(U32, F), base), SC.length(U32, SC.drop(U32, F, base)), Equal.sym(Nat, SC.length(U32, SC.drop(U32, F, base)), Nat.sub(SC.length(U32, F), base), length_drop(F, base)),
420    le_sub(base, 256n, SC.length(U32, F), L.subst(Nat, z => {Nat.is_le(Nat.add(base, 256n), z) == True{} : Bool}, Nat.mul(SC.length(A.Block, mem), 256n), SC.length(U32, F), hfl, hn)))
421  Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, F, P), base), 256n), SC.take(U32, SC.drop(U32, F, base), 256n), SB.words(SA.get(mem, b)),
422    Equal.trans(List<&2, U32>, SC.take(U32, SC.drop(U32, SC.append(U32, F, P), base), 256n), SC.take(U32, SC.append(U32, SC.drop(U32, F, base), P), 256n), SC.take(U32, SC.drop(U32, F, base), 256n),
423      Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, 256n), SC.drop(U32, SC.append(U32, F, P), base), SC.append(U32, SC.drop(U32, F, base), P), drop_append_le(F, P, base, hle)),
424      LL.sc_take_append_left(U32, SC.drop(U32, F, base), P, 256n, h256)),
425    flat_slice(mem, b, hb))
426
427def lt_last(+base: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(base, 256n), n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(base, 255n), n) == True{} : Bool}:
428  N.lt_le_trans(Nat.add(base, 255n), Nat.add(base, 256n), n, N.lt_add_left(255n, 256n, base, {==}), h)
429
430# Reading block b of the memory of mem.
431def get_block(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +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}, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {M.get(b, AR.thaw(U32, mt(d, mem))) == (AR.thaw(U32, mt(d, mem)), SA.get(mem, b)) : Array<U32> & A.Block}:
432  +ws = W(d, mem)
433  +hl = W_len(d, mem, hc)
434  +base = Nat.mul(b, 256n)
435  +last = Nat.add(base, 255n)
436  -ar = AR.thaw(U32, mt(d, mem))
437  +hlast = lt_last(base, SC.pow2(d), N.le_trans(Nat.add(base, 256n), Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d), mul_lt(b, SC.length(A.Block, mem), hb), hc))
438  +g = SA.get(mem, b)
439  %Equal.sym(Array<U32> & U32, Array.get(U32, ar, U32.from_nat(last)), (ar, nthv(ws, last)), get_word(d, ws, last, hd, hl, hlast)) : {M.read_fin(M.rd(255n, last, Nil{}, _)) == (ar, g) : Array<U32> & A.Block}
440  %Equal.sym(Array<U32> & List<&2, U32>, M.rd(255n, last, Nil{}, (ar, nthv(ws, last))), (ar, SC.append(U32, slice(ws, base, 256n), Nil{})), rd_words(d, ws, hd, hl, 255n, base, Nil{}, hlast)) : {M.read_fin(_) == (ar, g) : Array<U32> & A.Block}
441  %Equal.sym(List<&2, U32>, SC.append(U32, slice(ws, base, 256n), Nil{}), slice(ws, base, 256n), LL.append_nil(U32, slice(ws, base, 256n))) : {M.read_fin((ar, _)) == (ar, g) : Array<U32> & A.Block}
442  %Equal.sym(List<&2, U32>, slice(ws, base, 256n), SB.words(g), slice_W(d, mem, b, hb)) : {M.read_fin((ar, _)) == (ar, g) : Array<U32> & A.Block}
443  Equal.cong(A.Block, Array<U32> & A.Block, z => (ar, z), SB.rows8(SB.words(g)), g, rows8_words(g))
444
445# ---------------------------------------------------------------- writing block b
446
447# Words ws stored from index i on.
448def splice(ws: List<&2, U32>, +i: Nat, V: List<&2, U32>) -> List<&2, U32>:
449  match ws:
450    case Nil{}:
451      V
452    case w <> rest:
453      splice(rest, Nat.add(i, 1n), SC.update(U32, V, i, w))
454
455def lt_add_succ(+i: Nat, +r: Nat) -> {Nat.is_lt(i, Nat.add(i, 1n+r)) == True{} : Bool}:
456  %Equal.sym(Nat, Nat.add(i, 1n+r), 1n+Nat.add(i, r), N.add_succ(i, r)) : {Nat.is_lt(i, _) == True{} : Bool}
457  N.le_lt_succ(i, Nat.add(i, r), N.le_add_right(i, r))
458
459def add_one_assoc(+i: Nat, +r: Nat) -> {Nat.add(Nat.add(i, 1n), r) == Nat.add(i, 1n+r) : Nat}:
460  NA.add_assoc(i, 1n, r)
461
462# M.wr stores the words ws from word i on.
463def wr_words(+d: Nat, +ws: List<&2, U32>, +i: Nat, +V: List<&2, U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hl: {SC.length(U32, V) == SC.pow2(d) : Nat}, +hi: {Nat.is_le(Nat.add(i, SC.length(U32, ws)), SC.pow2(d)) == True{} : Bool}) -> {M.wr(ws, i, AR.thaw(U32, tree(d, V))) == AR.thaw(U32, tree(d, splice(ws, i, V))) : Array<U32>}:
464  match ws:
465    case Nil{}:
466      {==}
467    case +w <> +rest:
468      +t = tree(d, V)
469      +hi1 = N.lt_le_trans(i, Nat.add(i, 1n+SC.length(U32, rest)), SC.pow2(d), lt_add_succ(i, SC.length(U32, rest)), hi)
470      +ei = U.to_nat_from_nat(i, d, le32(d, hd), hi1)
471      +hin = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), hi1)
472      +hn = nth_some(V, i, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.pow2(d), SC.length(U32, V), Equal.sym(Nat, SC.length(U32, V), SC.pow2(d), hl), hi1))
473      +hx = L.subst(List<&2, U32>, z => {SC.nth(U32, z, U32.to_nat(U32.from_nat(i))) == Some{nthv(V, i)} : Maybe<&2, U32>}, V, AR.slots(U32, t), Equal.sym(List<&2, U32>, AR.slots(U32, t), V, tree_slots(d, V, hl)),
474        L.subst(Nat, z => {SC.nth(U32, V, z) == Some{nthv(V, i)} : Maybe<&2, U32>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), hn))
475      +es = AR.set(U32, d, t, U32.from_nat(i), w, nthv(V, i), hd, hin, hx, tree_perfect(d, V))
476      +t2 = AR.upd(U32, d, t, i, w)
477      +V2 = SC.update(U32, V, i, w)
478      +e_slots = Equal.trans(List<&2, U32>, AR.slots(U32, t2), SC.update(U32, AR.slots(U32, t), i, w), V2,
479        AR.upd_slots(U32, d, t, i, w, hi1, tree_perfect(d, V)),
480        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, i, w), AR.slots(U32, t), V, tree_slots(d, V, hl)))
481      +e_ext = Equal.trans(AR.Tree<U32>, t2, tree(d, AR.slots(U32, t2)), tree(d, V2), tree_ext(d, t2, AR.upd_perfect(U32, d, t, i, w, tree_perfect(d, V))), Equal.cong(List<&2, U32>, AR.Tree<U32>, z => tree(d, z), AR.slots(U32, t2), V2, e_slots))
482      +hl2 = Equal.trans(Nat, SC.length(U32, V2), SC.length(U32, V), SC.pow2(d), LL.length_update(U32, V, i, w), hl)
483      +hi2 = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest))), hi)
484      %Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, t), U32.from_nat(i), w), AR.thaw(U32, AR.upd(U32, d, t, U32.to_nat(U32.from_nat(i)), w)), es) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
485      %Equal.sym(Array<U32>, AR.thaw(U32, AR.upd(U32, d, t, U32.to_nat(U32.from_nat(i)), w)), AR.thaw(U32, t2), Equal.cong(Nat, Array<U32>, z => AR.thaw(U32, AR.upd(U32, d, t, z, w)), U32.to_nat(U32.from_nat(i)), i, ei)) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
486      %Equal.sym(Array<U32>, AR.thaw(U32, t2), AR.thaw(U32, tree(d, V2)), Equal.cong(AR.Tree<U32>, Array<U32>, z => AR.thaw(U32, z), t2, tree(d, V2), e_ext)) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
487      wr_words(d, rest, Nat.add(i, 1n), V2, hd, hl2, hi2)
488
489def splice_app_left(+ws: List<&2, U32>, +i: Nat, +X: List<&2, U32>, +P: List<&2, U32>, +h: {Nat.is_le(Nat.add(i, SC.length(U32, ws)), SC.length(U32, X)) == True{} : Bool}) -> {splice(ws, i, SC.append(U32, X, P)) == SC.append(U32, splice(ws, i, X), P) : List<&2, U32>}:
490  match ws:
491    case Nil{}:
492      {==}
493    case +w <> +rest:
494      +hi = N.lt_le_trans(i, Nat.add(i, 1n+SC.length(U32, rest)), SC.length(U32, X), lt_add_succ(i, SC.length(U32, rest)), h)
495      +X2 = SC.update(U32, X, i, w)
496      +h2 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), z) == True{} : Bool}, SC.length(U32, X), SC.length(U32, X2), Equal.sym(Nat, SC.length(U32, X2), SC.length(U32, X), LL.length_update(U32, X, i, w)),
497        L.subst(Nat, z => {Nat.is_le(z, SC.length(U32, X)) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest))), h))
498      %Equal.sym(List<&2, U32>, SC.update(U32, SC.append(U32, X, P), i, w), SC.append(U32, X2, P), LL.update_append_left(U32, X, P, i, w, hi)) : {splice(rest, Nat.add(i, 1n), _) == SC.append(U32, splice(rest, Nat.add(i, 1n), X2), P) : List<&2, U32>}
499      splice_app_left(rest, Nat.add(i, 1n), X2, P, h2)
500
501def splice_app_right(+ws: List<&2, U32>, +n: Nat, +k: Nat, +X: List<&2, U32>, +Y: List<&2, U32>, +hX: {SC.length(U32, X) == n : Nat}) -> {splice(ws, Nat.add(n, k), SC.append(U32, X, Y)) == SC.append(U32, X, splice(ws, k, Y)) : List<&2, U32>}:
502  match ws:
503    case Nil{}:
504      {==}
505    case +w <> +rest:
506      +hle = L.subst(Nat, z => {Nat.is_le(z, Nat.add(n, k)) == True{} : Bool}, n, SC.length(U32, X), Equal.sym(Nat, SC.length(U32, X), n, hX), N.le_add_right(n, k))
507      +ek = Equal.trans(Nat, Nat.sub(Nat.add(n, k), SC.length(U32, X)), Nat.sub(Nat.add(n, k), n), k, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(n, k), z), SC.length(U32, X), n, hX), N.add_sub_cancel(n, k))
508      +Y2 = SC.update(U32, Y, k, w)
509      %Equal.sym(List<&2, U32>, SC.update(U32, SC.append(U32, X, Y), Nat.add(n, k), w), SC.append(U32, X, SC.update(U32, Y, Nat.sub(Nat.add(n, k), SC.length(U32, X)), w)), LL.update_append_right(U32, X, Y, Nat.add(n, k), w, hle)) : {splice(rest, Nat.add(Nat.add(n, k), 1n), _) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
510      %Equal.sym(Nat, Nat.sub(Nat.add(n, k), SC.length(U32, X)), k, ek) : {splice(rest, Nat.add(Nat.add(n, k), 1n), SC.append(U32, X, SC.update(U32, Y, _, w))) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
511      %Equal.sym(Nat, Nat.add(Nat.add(n, k), 1n), Nat.add(n, Nat.add(k, 1n)), NA.add_assoc(n, k, 1n)) : {splice(rest, _, SC.append(U32, X, Y2)) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
512      splice_app_right(rest, n, Nat.add(k, 1n), X, Y2, hX)
513
514def take_upd(+V: List<&2, U32>, +i: Nat, +w: U32, +h: {Nat.is_lt(i, SC.length(U32, V)) == True{} : Bool}) -> {SC.take(U32, SC.update(U32, V, i, w), 1n+i) == SC.append(U32, SC.take(U32, V, i), Con{w, Nil{}}) : List<&2, U32>}:
515  match V i:
516    case Nil{} _:
517      Empty.absurd({SC.take(U32, SC.update(U32, Nil{}, i, w), 1n+i) == SC.append(U32, SC.take(U32, Nil{}, i), Con{w, Nil{}}) : List<&2, U32>}, N.lt_zero_absurd(i, h))
518    case Con{x, +r} 0n:
519      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{w, z}, SC.take(U32, r, 0n), Nil{}, LL.sc_take_zero(U32, r))
520    case Con{+x, +r} 1n+ +j:
521      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, SC.take(U32, SC.update(U32, r, j, w), 1n+j), SC.append(U32, SC.take(U32, r, j), Con{w, Nil{}}), take_upd(r, j, w, h))
522
523# Storing ws from word i over V, when V ends exactly there: the first i words of V, then ws.
524def splice_self(+ws: List<&2, U32>, +i: Nat, +V: List<&2, U32>, +h: {SC.length(U32, V) == Nat.add(i, SC.length(U32, ws)) : Nat}) -> {splice(ws, i, V) == SC.append(U32, SC.take(U32, V, i), ws) : List<&2, U32>}:
525  match ws:
526    case Nil{}:
527      +hv = Equal.trans(Nat, SC.length(U32, V), Nat.add(i, 0n), i, h, N.add_zero(i))
528      Equal.trans(List<&2, U32>, V, SC.take(U32, V, i), SC.append(U32, SC.take(U32, V, i), Nil{}), Equal.sym(List<&2, U32>, SC.take(U32, V, i), V, take_all(V, i, hv)), Equal.sym(List<&2, U32>, SC.append(U32, SC.take(U32, V, i), Nil{}), SC.take(U32, V, i), LL.append_nil(U32, SC.take(U32, V, i))))
529    case +w <> +rest:
530      +V2 = SC.update(U32, V, i, w)
531      +hi = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), SC.length(U32, V), Equal.sym(Nat, SC.length(U32, V), Nat.add(i, 1n+SC.length(U32, rest)), h), lt_add_succ(i, SC.length(U32, rest)))
532      +h2 = Equal.trans(Nat, SC.length(U32, V2), SC.length(U32, V), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), LL.length_update(U32, V, i, w), Equal.trans(Nat, SC.length(U32, V), Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), h, Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest)))))
533      %Equal.sym(List<&2, U32>, splice(rest, Nat.add(i, 1n), V2), SC.append(U32, SC.take(U32, V2, Nat.add(i, 1n)), rest), splice_self(rest, Nat.add(i, 1n), V2, h2)) : {_ == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
534      %Equal.sym(Nat, Nat.add(i, 1n), 1n+i, Equal.trans(Nat, Nat.add(i, 1n), 1n+Nat.add(i, 0n), 1n+i, N.add_succ(i, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(i, 0n), i, N.add_zero(i)))) : {SC.append(U32, SC.take(U32, V2, _), rest) == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
535      %Equal.sym(List<&2, U32>, SC.take(U32, V2, 1n+i), SC.append(U32, SC.take(U32, V, i), Con{w, Nil{}}), take_upd(V, i, w, hi)) : {SC.append(U32, _, rest) == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
536      LL.append_assoc(U32, SC.take(U32, V, i), Con{w, Nil{}}, rest)
537
538def splice_full(+b: A.Block, +v: A.Block) -> {splice(SB.words(v), 0n, SB.words(b)) == SB.words(v) : List<&2, U32>}:
539  Equal.trans(List<&2, U32>, splice(SB.words(v), 0n, SB.words(b)), SC.append(U32, SC.take(U32, SB.words(b), 0n), SB.words(v)), SB.words(v),
540    splice_self(SB.words(v), 0n, SB.words(b), Equal.trans(Nat, SC.length(U32, SB.words(b)), 256n, SC.length(U32, SB.words(v)), words_len(b), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v)))),
541    Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, SB.words(v)), SC.take(U32, SB.words(b), 0n), Nil{}, LL.sc_take_zero(U32, SB.words(b))))
542
543def flat_splice(+mem: List<&2, A.Block>, +b: Nat, +v: A.Block, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {splice(SB.words(v), Nat.mul(b, 256n), flat(mem)) == flat(SA.set(mem, b, v)) : List<&2, U32>}:
544  match mem b:
545    case Nil{} _:
546      Empty.absurd({splice(SB.words(v), Nat.mul(b, 256n), Nil{}) == flat(SA.set(Nil{}, b, v)) : List<&2, U32>}, N.lt_zero_absurd(b, hb))
547    case +x <> +rest 0n:
548      Equal.trans(List<&2, U32>, splice(SB.words(v), 0n, SC.append(U32, SB.words(x), flat(rest))), SC.append(U32, splice(SB.words(v), 0n, SB.words(x)), flat(rest)), SC.append(U32, SB.words(v), flat(rest)),
549        splice_app_left(SB.words(v), 0n, SB.words(x), flat(rest), L.subst(Nat, z => {Nat.is_le(z, SC.length(U32, SB.words(x))) == True{} : Bool}, SC.length(U32, SB.words(x)), SC.length(U32, SB.words(v)), Equal.trans(Nat, SC.length(U32, SB.words(x)), 256n, SC.length(U32, SB.words(v)), words_len(x), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v))), N.le_refl(SC.length(U32, SB.words(x))))),
550        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, flat(rest)), splice(SB.words(v), 0n, SB.words(x)), SB.words(v), splice_full(x, v)))
551    case +x <> +rest 1n+ +c:
552      Equal.trans(List<&2, U32>, splice(SB.words(v), Nat.add(256n, Nat.mul(c, 256n)), SC.append(U32, SB.words(x), flat(rest))), SC.append(U32, SB.words(x), splice(SB.words(v), Nat.mul(c, 256n), flat(rest))), SC.append(U32, SB.words(x), flat(SA.set(rest, c, v))),
553        splice_app_right(SB.words(v), 256n, Nat.mul(c, 256n), SB.words(x), flat(rest), words_len(x)),
554        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, SB.words(x), z), splice(SB.words(v), Nat.mul(c, 256n), flat(rest)), flat(SA.set(rest, c, v)), flat_splice(rest, c, v, hb)))
555
556def W_splice(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +v: A.Block, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {splice(SB.words(v), Nat.mul(b, 256n), W(d, mem)) == W(d, SA.set(mem, b, v)) : List<&2, U32>}:
557  +F = flat(mem)
558  +hn = mul_lt(b, SC.length(A.Block, mem), hb)
559  +hfl = Equal.sym(Nat, SC.length(U32, F), Nat.mul(SC.length(A.Block, mem), 256n), flat_len(mem))
560  +h = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(b, 256n), z), SC.length(U32, F)) == True{} : Bool}, 256n, SC.length(U32, SB.words(v)), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v)), L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(b, 256n), 256n), z) == True{} : Bool}, Nat.mul(SC.length(A.Block, mem), 256n), SC.length(U32, F), hfl, hn))
561  +P = pad(d, SC.length(A.Block, mem))
562  Equal.trans(List<&2, U32>, splice(SB.words(v), Nat.mul(b, 256n), SC.append(U32, F, P)), SC.append(U32, splice(SB.words(v), Nat.mul(b, 256n), F), P), W(d, SA.set(mem, b, v)),
563    splice_app_left(SB.words(v), Nat.mul(b, 256n), F, P, h),
564    Equal.trans(List<&2, U32>, SC.append(U32, splice(SB.words(v), Nat.mul(b, 256n), F), P), SC.append(U32, flat(SA.set(mem, b, v)), P), W(d, SA.set(mem, b, v)),
565      Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, P), splice(SB.words(v), Nat.mul(b, 256n), F), flat(SA.set(mem, b, v)), flat_splice(mem, b, v, hb)),
566      Equal.cong(Nat, List<&2, U32>, z => SC.append(U32, flat(SA.set(mem, b, v)), pad(d, z)), SC.length(A.Block, mem), SC.length(A.Block, SA.set(mem, b, v)), Equal.sym(Nat, SC.length(A.Block, SA.set(mem, b, v)), SC.length(A.Block, mem), LL.length_update(A.Block, mem, b, v)))))
567
568# Writing block b of the memory of mem.
569def set_block(+d: Nat, +mem: List<&2, A.Block>, +b: Nat, +v: 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}, +hb: {Nat.is_lt(b, SC.length(A.Block, mem)) == True{} : Bool}) -> {M.set(b, v, AR.thaw(U32, mt(d, mem))) == AR.thaw(U32, mt(d, SA.set(mem, b, v))) : Array<U32>}:
570  +hi = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(b, 256n), z), SC.pow2(d)) == True{} : Bool}, 256n, SC.length(U32, SB.words(v)), Equal.sym(Nat, SC.length(U32, SB.words(v)), 256n, words_len(v)), N.le_trans(Nat.add(Nat.mul(b, 256n), 256n), Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d), mul_lt(b, SC.length(A.Block, mem), hb), hc))
571  Equal.trans(Array<U32>, M.wr(SB.words(v), Nat.mul(b, 256n), AR.thaw(U32, tree(d, W(d, mem)))), AR.thaw(U32, tree(d, splice(SB.words(v), Nat.mul(b, 256n), W(d, mem)))), AR.thaw(U32, mt(d, SA.set(mem, b, v))),
572    wr_words(d, SB.words(v), Nat.mul(b, 256n), W(d, mem), hd, W_len(d, mem, hc), hi),
573    Equal.cong(List<&2, U32>, Array<U32>, z => AR.thaw(U32, tree(d, z)), splice(SB.words(v), Nat.mul(b, 256n), W(d, mem)), W(d, SA.set(mem, b, v)), W_splice(d, mem, b, v, hb)))
574
575# ---------------------------------------------------------------- the zero memory
576
577def zero_words() -> {SB.words(SG.zero()) == SC.replicate(U32, 256n, 0) : List<&2, U32>}:
578  {==}
579
580def flat_zero(+n: Nat) -> {flat(SC.replicate(A.Block, n, SG.zero())) == SC.replicate(U32, Nat.mul(n, 256n), 0) : List<&2, U32>}:
581  match n:
582    case 0n:
583      {==}
584    case 1n+ +k:
585      Equal.trans(List<&2, U32>, SC.append(U32, SB.words(SG.zero()), flat(SC.replicate(A.Block, k, SG.zero()))), SC.append(U32, SC.replicate(U32, 256n, 0), SC.replicate(U32, Nat.mul(k, 256n), 0)), SC.replicate(U32, Nat.add(256n, Nat.mul(k, 256n)), 0),
586        Equal.trans(List<&2, U32>, SC.append(U32, SB.words(SG.zero()), flat(SC.replicate(A.Block, k, SG.zero()))), SC.append(U32, SC.replicate(U32, 256n, 0), flat(SC.replicate(A.Block, k, SG.zero()))), SC.append(U32, SC.replicate(U32, 256n, 0), SC.replicate(U32, Nat.mul(k, 256n), 0)),
587          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, flat(SC.replicate(A.Block, k, SG.zero()))), SB.words(SG.zero()), SC.replicate(U32, 256n, 0), zero_words()),
588          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, SC.replicate(U32, 256n, 0), z), flat(SC.replicate(A.Block, k, SG.zero())), SC.replicate(U32, Nat.mul(k, 256n), 0), flat_zero(k))),
589        LL.replicate_add(U32, 256n, Nat.mul(k, 256n), 0))
590
591# The zeroed array is the memory of mm zero blocks.
592def new_mem(+d: Nat, +mm: Nat, +hc: {Nat.is_le(Nat.mul(mm, 256n), SC.pow2(d)) == True{} : Bool}) -> {Array.new(U32, d, 0) == AR.thaw(U32, mt(d, SC.replicate(A.Block, mm, SG.zero()))) : Array<U32>}:
593  +z = SC.replicate(A.Block, mm, SG.zero())
594  +n = Nat.mul(mm, 256n)
595  +t = AR.trep(U32, d, 0)
596  +ew = Equal.trans(List<&2, U32>, W(d, z), SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)), SC.replicate(U32, SC.pow2(d), 0),
597    Equal.trans(List<&2, U32>, W(d, z), SC.append(U32, SC.replicate(U32, n, 0), pad(d, SC.length(A.Block, z))), SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)),
598      Equal.cong(List<&2, U32>, List<&2, U32>, x => SC.append(U32, x, pad(d, SC.length(A.Block, z))), flat(z), SC.replicate(U32, n, 0), flat_zero(mm)),
599      Equal.cong(Nat, List<&2, U32>, x => SC.append(U32, SC.replicate(U32, n, 0), pad(d, x)), SC.length(A.Block, z), mm, LL.length_replicate(A.Block, mm, SG.zero()))),
600    Equal.trans(List<&2, U32>, SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)), SC.replicate(U32, Nat.add(n, Nat.sub(SC.pow2(d), n)), 0), SC.replicate(U32, SC.pow2(d), 0),
601      LL.replicate_add(U32, n, Nat.sub(SC.pow2(d), n), 0),
602      Equal.cong(Nat, List<&2, U32>, x => SC.replicate(U32, x, 0), Nat.add(n, Nat.sub(SC.pow2(d), n)), SC.pow2(d), N.sub_add(SC.pow2(d), n, hc))))
603  +et = Equal.trans(AR.Tree<U32>, t, tree(d, AR.slots(U32, t)), tree(d, W(d, z)),
604    tree_ext(d, t, AR.trep_perfect(U32, d, 0)),
605    Equal.cong(List<&2, U32>, AR.Tree<U32>, x => tree(d, x), AR.slots(U32, t), W(d, z), Equal.trans(List<&2, U32>, AR.slots(U32, t), SC.replicate(U32, SC.pow2(d), 0), W(d, z), AR.trep_slots(U32, d, 0), Equal.sym(List<&2, U32>, W(d, z), SC.replicate(U32, SC.pow2(d), 0), ew))))
606  Equal.trans(Array<U32>, Array.new(U32, d, 0), AR.thaw(U32, t), AR.thaw(U32, mt(d, z)), AR.new(U32, d, 0), Equal.cong(AR.Tree<U32>, Array<U32>, x => AR.thaw(U32, x), t, tree(d, W(d, z)), et))