1	import Base
2	import ../../../spec/lib/common.bend as SC
3	import ../../lib/array.bend as AR
4	import ../../lib/list.bend as LL
5	import ../../lib/nat.bend as N
6	import ../../lib/logic.bend as L
7	import ../../lib/u32.bend as U
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../../src/crypto/blake/blake2b/types.bend as T
10	import ../../../src/crypto/argon2/types.bend as A
11	import ../../../src/crypto/argon2/sub.bend as SB
12	import ../../../src/crypto/argon2/memory.bend as M
13	import ../../../spec/crypto/argon2/blamka.bend as SG
14	import ../../../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	
28	def nthv(ws: List<&2, U32>, i: Nat) -> U32:
29	  Maybe.default(&2, U32, SC.nth(U32, ws, i), 0)
30	
31	def 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	
40	def zsub(+n: Nat) -> {Nat.sub(0n, n) == 0n : Nat}:
41	  match n:
42	    case 0n:
43	      {==}
44	    case 1n+p:
45	      {==}
46	
47	def 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	
56	def 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	
65	def 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	
72	def 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).
86	def 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	
93	def 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	
100	def 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	
109	def 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	
113	def 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.
117	def 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.
133	def 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	
162	def 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	
171	def 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.
175	def 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	
186	def slice(ws: List<&2, U32>, +base: Nat, n: Nat) -> List<&2, U32>:
187	  SC.take(U32, SC.drop(U32, ws, base), n)
188	
189	def 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	
198	def 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	
207	def 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.
217	def 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	
224	def 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	
233	def 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	
236	def 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	
239	def 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.
244	def 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	
265	def 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	
272	def 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.
276	def 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	
279	def mt(+d: Nat, +mem: List<&2, A.Block>) -> AR.Tree<U32>:
280	  tree(d, W(d, mem))
281	
282	def 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	
287	def 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.
295	def 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	
300	def 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	
313	def 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	
318	def 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	
331	def 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	
342	def 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	
354	def 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	
365	def 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.
377	def 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	
393	def 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	
403	def 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	
412	def 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	
427	def 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.
431	def 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.
448	def 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	
455	def 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	
459	def 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.
463	def 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	
489	def 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	
501	def 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	
514	def 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.
524	def 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	
538	def 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	
543	def 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	
556	def 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.
569	def 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	
577	def zero_words() -> {SB.words(SG.zero()) == SC.replicate(U32, 256n, 0) : List<&2, U32>}:
578	  {==}
579	
580	def 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.
592	def 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))