1	import Base
2	import ./defs.bend as D
3	import ./bytes.bend as B
4	import lawful-words@0.1.0.0/defs.bend as W
5	import lawful-words@0.1.0.0/proof_nat.bend as N
6	import lawful-words@0.1.0.0/proof_u32.bend as U
7	import lawful-words@0.1.0.0/proof_bytes.bend as Y
8	import lawful-arrays@0.1.0.0/defs.bend as A
9	import lawful-arrays@0.1.0.0/proof_base.bend as AB
10	import lawful-arrays@0.1.0.0/proof_tree.bend as P
11	import lawful-arrays@0.1.0.0/proof_index.bend as I
12	import lawful-arrays@0.1.0.0/proof_shape.bend as S
13	
14	# The core of the Bytes proofs. A Bytes is a Type (it holds an Array), so a
15	# proof may use one only once. Every lemma here is about BT(len, t): a Bytes
16	# whose block is the mirror P.fromT(t) of a Tree<U32> t (Data), so len and t
17	# may be used freely. A law first takes its Bytes apart and mirrors the block.
18	
19	def BT(+len: U32, +t: P.Tree<U32>) -> D.Bytes:
20	  D.Bytes{len, P.fromT(U32, t)}
21	
22	# The words of the block.
23	def WL(+t: P.Tree<U32>) -> List<&2, U32>:
24	  A.view(U32, P.fromT(U32, t))
25	
26	# Word k of the block, as Array.get reads it.
27	def WD(+t: P.Tree<U32>, +k: U32) -> U32:
28	  Pair.snd(Array<U32>, U32, Array.get(U32, P.fromT(U32, t), k))
29	
30	# Byte i, as B.at reads it.
31	def AT(+len: U32, +t: P.Tree<U32>, +i: U32) -> U32:
32	  Pair.snd(D.Bytes, U32, B.at(BT(len, t), i))
33	
34	# What a Maybe word gives for byte r.
35	def mb(m: Maybe<&2, U32>, +r: Nat) -> Maybe<&2, U32>:
36	  match m:
37	    case None{}:
38	      None{}
39	    case Some{w}:
40	      Some{W.byte(w, r)}
41	
42	# Reading a byte
43	# ==============
44	
45	law at_pair_t:
46	  for +len: U32
47	  for +t: P.Tree<U32>
48	  for +i: U32
49	  {B.at(BT(len, t), i) == (BT(len, t), AT(len, t, i)) : D.Bytes & U32}
50	
51	def at_pair_t(len, t, i):
52	  +k = (i >> 2n : U32)
53	  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), WD(t, k)), P.get_pair_t(U32, t, k)) :
54	    {B.at.fin(len, i, _) == (BT(len, t), Pair.snd(D.Bytes, U32, B.at.fin(len, i, _))) : D.Bytes & U32}
55	  {==}
56	
57	law at_val:
58	  for +len: U32
59	  for +t: P.Tree<U32>
60	  for +i: U32
61	  {AT(len, t, i) == W.byte(WD(t, (i >> 2n : U32)), U32.to_nat((i .&. 3 : U32))) : U32}
62	
63	def at_val(len, t, i):
64	  +k = (i >> 2n : U32)
65	  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), WD(t, k)), P.get_pair_t(U32, t, k)) :
66	    {Pair.snd(D.Bytes, U32, B.at.fin(len, i, _)) == W.byte(WD(t, k), U32.to_nat((i .&. 3 : U32))) : U32}
67	  {==}
68	
69	# The bytes of a word list
70	# ========================
71	
72	law unpack_get0:
73	  for +w: U32
74	  for +t: List<&2, U32>
75	  for +r: Nat
76	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
77	  {List.get(&2, U32, D.unpack(w <> t), r) == Some{W.byte(w, r)} : Maybe<&2, U32>}
78	
79	def unpack_get0(w, t, r, hr):
80	  match r:
81	    case 0n:
82	      {==}
83	    case 1n+r1:
84	      match r1:
85	        case 0n:
86	          {==}
87	        case 1n+r2:
88	          match r2:
89	            case 0n:
90	              {==}
91	            case 1n+r3:
92	              match r3:
93	                case 0n:
94	                  {==}
95	                case 1n+r4:
96	                  Empty.absurd({List.get(&2, U32, D.unpack(w <> t), 4n+r4) == Some{W.byte(w, 4n+r4)} : Maybe<&2, U32>},
97	                    AB.lt_zero_absurd(r4, hr))
98	
99	# Byte r of word q is byte 4q + r.
100	law unpack_get:
101	  for +ws: List<&2, U32>
102	  for +q: Nat
103	  for +r: Nat
104	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
105	  {List.get(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), r)) == mb(List.get(&2, U32, ws, q), r) : Maybe<&2, U32>}
106	
107	def unpack_get(ws, q, r, hr):
108	  match ws q:
109	    case Nil{} _:
110	      {==}
111	    case Con{w, t} 0n:
112	      unpack_get0(w, t, r, hr)
113	    case Con{w, t} 1n+p:
114	      unpack_get(t, p, r, hr)
115	
116	# Byte n of the word list: byte n % 4 of word n / 4.
117	law unpack_get_n:
118	  for +ws: List<&2, U32>
119	  for +n: Nat
120	  {List.get(&2, U32, D.unpack(ws), n) == mb(List.get(&2, U32, ws, Nat.div(n, 4n)), Nat.mod(n, 4n)) : Maybe<&2, U32>}
121	
122	def unpack_get_n(ws, n):
123	  %N.div_mod(n, 4n) : {List.get(&2, U32, D.unpack(ws), _) == mb(List.get(&2, U32, ws, Nat.div(n, 4n)), Nat.mod(n, 4n)) : Maybe<&2, U32>}
124	  unpack_get(ws, Nat.div(n, 4n), Nat.mod(n, 4n), N.mod_lt(n, 4n, {==}))
125	
126	# The same for a U32 index: word i >> 2, byte i & 3.
127	law unpack_get_i:
128	  for +ws: List<&2, U32>
129	  for +i: U32
130	  {List.get(&2, U32, D.unpack(ws), U32.to_nat(i)) == mb(List.get(&2, U32, ws, U32.to_nat((i >> 2n : U32))), U32.to_nat((i .&. 3 : U32))) : Maybe<&2, U32>}
131	
132	def unpack_get_i(ws, i):
133	  +n = U32.to_nat(i)
134	  %Equal.sym(Nat, U32.to_nat((i >> 2n : U32)), Nat.div(n, 4n), U.to_nat_shrn(i, 2n)) :
135	    {List.get(&2, U32, D.unpack(ws), n) == mb(List.get(&2, U32, ws, _), U32.to_nat((i .&. 3 : U32))) : Maybe<&2, U32>}
136	  %Equal.sym(Nat, U32.to_nat((i .&. 3 : U32)), Nat.mod(n, 4n), U.to_nat_and_mask(i, 3, 2n, {==})) :
137	    {List.get(&2, U32, D.unpack(ws), n) == mb(List.get(&2, U32, ws, Nat.div(n, 4n)), _) : Maybe<&2, U32>}
138	  unpack_get_n(ws, n)
139	
140	# Lists
141	# =====
142	
143	law take_get:
144	  for +xs: List<&2, U32>
145	  for +n: Nat
146	  for +i: Nat
147	  for +h: {Nat.is_lt(i, n) == True{} : Bool}
148	  {List.get(&2, U32, List.take(&2, U32, xs, n), i) == List.get(&2, U32, xs, i) : Maybe<&2, U32>}
149	
150	def take_get(xs, n, i, h):
151	  match xs n i:
152	    case Nil{} _ _:
153	      {==}
154	    case Con{x, t} 0n _:
155	      Empty.absurd({List.get(&2, U32, Nil{}, i) == List.get(&2, U32, x <> t, i) : Maybe<&2, U32>},
156	        AB.lt_zero_absurd(i, h))
157	    case Con{x, t} 1n+p 0n:
158	      {==}
159	    case Con{x, t} 1n+p 1n+j:
160	      take_get(t, p, j, h)
161	
162	# Index facts
163	# ===========
164	
165	law lt32:
166	  for +d: Nat
167	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
168	  {Nat.is_lt(d, 32n) == True{} : Bool}
169	
170	def lt32(d, hd):
171	  N.le_lt_trans(d, 29n, 32n, hd, {==})
172	
173	# A byte index below 4 * 2^d has its word index below 2^d.
174	law word_lt:
175	  for +i: U32
176	  for +d: Nat
177	  for +h: {Nat.is_lt(U32.to_nat(i), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
178	  {Nat.is_lt(U32.to_nat((i >> 2n : U32)), Nat.pow(2n, d)) == True{} : Bool}
179	
180	def word_lt(i, d, h):
181	  %Equal.sym(Nat, U32.to_nat((i >> 2n : U32)), Nat.div(U32.to_nat(i), 4n), U.to_nat_shrn(i, 2n)) :
182	    {Nat.is_lt(_, Nat.pow(2n, d)) == True{} : Bool}
183	  N.div_lt(U32.to_nat(i), 4n, Nat.pow(2n, d), {==}, h)
184	
185	# Reading a byte
186	# ==============
187	
188	law at_view_t:
189	  for +len: U32
190	  for +t: P.Tree<U32>
191	  for +d: Nat
192	  for +i: U32
193	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
194	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
195	  for +hl: {Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
196	  for +hi: {Nat.is_lt(U32.to_nat(i), U32.to_nat(len)) == True{} : Bool}
197	  {Some{AT(len, t, i)} == List.get(&2, U32, D.view(BT(len, t)), U32.to_nat(i)) : Maybe<&2, U32>}
198	
199	def at_view_t(len, t, d, i, hf, hd, hl, hi):
200	  +k = (i >> 2n : U32)
201	  +r = U32.to_nat((i .&. 3 : U32))
202	  +n = U32.to_nat(i)
203	  %Equal.sym(U32, AT(len, t, i), W.byte(WD(t, k), r), at_val(len, t, i)) :
204	    {Some{_} == List.get(&2, U32, D.view(BT(len, t)), n) : Maybe<&2, U32>}
205	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.take(&2, U32, D.unpack(WL(t)), U32.to_nat(len)), n),
206	    List.get(&2, U32, D.unpack(WL(t)), n), take_get(D.unpack(WL(t)), U32.to_nat(len), n, hi)) :
207	    {Some{W.byte(WD(t, k), r)} == _ : Maybe<&2, U32>}
208	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, D.unpack(WL(t)), n), mb(List.get(&2, U32, WL(t), U32.to_nat(k)), r),
209	    unpack_get_i(WL(t), i)) :
210	    {Some{W.byte(WD(t, k), r)} == _ : Maybe<&2, U32>}
211	  +hk = word_lt(i, d, N.lt_le_trans(n, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hi, hl))
212	  %I.slot_small_t(k, d, hk) : {Some{W.byte(WD(t, k), r)} == mb(List.get(&2, U32, WL(t), _), r) : Maybe<&2, U32>}
213	  %I.get_view_t(U32, t, d, k, hf, lt32(d, hd)) : {Some{W.byte(WD(t, k), r)} == mb(_, r) : Maybe<&2, U32>}
214	  {==}
215	
216	# The mirror of a Bytes
217	# =====================
218	
219	# Every Bytes is BT(len, t) for some len and tree t.
220	def BMirror(-b: D.Bytes) -> Data:
221	  Sigma<&2, &2, U32, len => Sigma<&2, &2, P.Tree<U32>, t => {BT(len, t) == b : D.Bytes}>>
222	
223	def bmirror.go(+len: U32, -buf: Array<U32>, m: P.Mirror(U32, buf)) -> BMirror(D.Bytes{len, buf}):
224	  (t, e) = m
225	  (len, (t, Equal.cong(Array<U32>, D.Bytes, x => D.Bytes{len, x}, P.fromT(U32, t), buf, e)))
226	
227	def bmirror(b: D.Bytes) -> BMirror(b):
228	  match b:
229	    case D.Bytes{+len, buf}:
230	      bmirror.go(len, buf, P.mirror(U32, buf))
231	
232	# Transport of a hypothesis about b to its mirror.
233	def tr(-H: D.Bytes -> Type, -b: D.Bytes, +len: U32, +t: P.Tree<U32>, e: {BT(len, t) == b : D.Bytes}, h: H(b)) -> H(BT(len, t)):
234	  AB.subst(D.Bytes, H, b, BT(len, t), Equal.sym(D.Bytes, BT(len, t), b, e), h)
235	
236	# The three parts of ok.
237	law ok_full:
238	  for +len: U32
239	  for +t: P.Tree<U32>
240	  for +d: Nat
241	  for +h: {D.ok(BT(len, t), d) == True{} : Bool}
242	  {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
243	
244	def ok_full(len, t, d, h):
245	  AB.and_true_l(A.full(U32, P.fromT(U32, t), d),
246	    Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))), h)
247	
248	law ok_d:
249	  for +len: U32
250	  for +t: P.Tree<U32>
251	  for +d: Nat
252	  for +h: {D.ok(BT(len, t), d) == True{} : Bool}
253	  {Nat.is_le(d, 29n) == True{} : Bool}
254	
255	def ok_d(len, t, d, h):
256	  AB.and_true_l(Nat.is_le(d, 29n), Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))),
257	    AB.and_true_r(A.full(U32, P.fromT(U32, t), d),
258	      Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))), h))
259	
260	law ok_len:
261	  for +len: U32
262	  for +t: P.Tree<U32>
263	  for +d: Nat
264	  for +h: {D.ok(BT(len, t), d) == True{} : Bool}
265	  {Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
266	
267	def ok_len(len, t, d, h):
268	  AB.and_true_r(Nat.is_le(d, 29n), Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))),
269	    AB.and_true_r(A.full(U32, P.fromT(U32, t), d),
270	      Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))), h))
271	
272	# ok from its three parts.
273	law ok_mk:
274	  for +len: U32
275	  for +t: P.Tree<U32>
276	  for +d: Nat
277	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
278	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
279	  for +hl: {Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
280	  {D.ok(BT(len, t), d) == True{} : Bool}
281	
282	def ok_mk(len, t, d, hf, hd, hl):
283	  %Equal.sym(Bool, A.full(U32, P.fromT(U32, t), d), True{}, hf) :
284	    {Bool.and(_, Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)))) == True{} : Bool}
285	  %Equal.sym(Bool, Nat.is_le(d, 29n), True{}, hd) :
286	    {Bool.and(True{}, Bool.and(_, Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))))) == True{} : Bool}
287	  %Equal.sym(Bool, Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))), True{}, hl) :
288	    {Bool.and(True{}, Bool.and(True{}, _)) == True{} : Bool}
289	  {==}
290	
291	# Writing a byte
292	# ==============
293	
294	def L4(+w: U32) -> List<&2, U32>:
295	  [W.byte(w, 0n), W.byte(w, 1n), W.byte(w, 2n), W.byte(w, 3n)]
296	
297	# The four bytes of a word with byte k set to v (k a literal).
298	law wbp0:
299	  for +w: U32
300	  for +v: U32
301	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
302	  {L4(W.put_byte(w, 0n, v)) == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}
303	
304	def wbp0(w, v, hv):
305	  %Equal.sym(U32, W.byte(W.put_byte(w, 0n, v), 0n), v, Y.byte_put_same(w, 0n, v, {==}, hv)) :
306	    {[_, W.byte(W.put_byte(w, 0n, v), 1n), W.byte(W.put_byte(w, 0n, v), 2n), W.byte(W.put_byte(w, 0n, v), 3n)] == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}
307	  %Equal.sym(U32, W.byte(W.put_byte(w, 0n, v), 1n), W.byte(w, 1n), Y.byte_put_other(w, 1n, 0n, v, hv, {==})) :
308	    {[v, _, W.byte(W.put_byte(w, 0n, v), 2n), W.byte(W.put_byte(w, 0n, v), 3n)] == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}
309	  %Equal.sym(U32, W.byte(W.put_byte(w, 0n, v), 2n), W.byte(w, 2n), Y.byte_put_other(w, 2n, 0n, v, hv, {==})) :
310	    {[v, W.byte(w, 1n), _, W.byte(W.put_byte(w, 0n, v), 3n)] == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}
311	  %Equal.sym(U32, W.byte(W.put_byte(w, 0n, v), 3n), W.byte(w, 3n), Y.byte_put_other(w, 3n, 0n, v, hv, {==})) :
312	    {[v, W.byte(w, 1n), W.byte(w, 2n), _] == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}
313	  {==}
314	
315	law wbp1:
316	  for +w: U32
317	  for +v: U32
318	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
319	  {L4(W.put_byte(w, 1n, v)) == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}
320	
321	def wbp1(w, v, hv):
322	  %Equal.sym(U32, W.byte(W.put_byte(w, 1n, v), 0n), W.byte(w, 0n), Y.byte_put_other(w, 0n, 1n, v, hv, {==})) :
323	    {[_, W.byte(W.put_byte(w, 1n, v), 1n), W.byte(W.put_byte(w, 1n, v), 2n), W.byte(W.put_byte(w, 1n, v), 3n)] == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}
324	  %Equal.sym(U32, W.byte(W.put_byte(w, 1n, v), 1n), v, Y.byte_put_same(w, 1n, v, {==}, hv)) :
325	    {[W.byte(w, 0n), _, W.byte(W.put_byte(w, 1n, v), 2n), W.byte(W.put_byte(w, 1n, v), 3n)] == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}
326	  %Equal.sym(U32, W.byte(W.put_byte(w, 1n, v), 2n), W.byte(w, 2n), Y.byte_put_other(w, 2n, 1n, v, hv, {==})) :
327	    {[W.byte(w, 0n), v, _, W.byte(W.put_byte(w, 1n, v), 3n)] == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}
328	  %Equal.sym(U32, W.byte(W.put_byte(w, 1n, v), 3n), W.byte(w, 3n), Y.byte_put_other(w, 3n, 1n, v, hv, {==})) :
329	    {[W.byte(w, 0n), v, W.byte(w, 2n), _] == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}
330	  {==}
331	
332	law wbp2:
333	  for +w: U32
334	  for +v: U32
335	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
336	  {L4(W.put_byte(w, 2n, v)) == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}
337	
338	def wbp2(w, v, hv):
339	  %Equal.sym(U32, W.byte(W.put_byte(w, 2n, v), 0n), W.byte(w, 0n), Y.byte_put_other(w, 0n, 2n, v, hv, {==})) :
340	    {[_, W.byte(W.put_byte(w, 2n, v), 1n), W.byte(W.put_byte(w, 2n, v), 2n), W.byte(W.put_byte(w, 2n, v), 3n)] == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}
341	  %Equal.sym(U32, W.byte(W.put_byte(w, 2n, v), 1n), W.byte(w, 1n), Y.byte_put_other(w, 1n, 2n, v, hv, {==})) :
342	    {[W.byte(w, 0n), _, W.byte(W.put_byte(w, 2n, v), 2n), W.byte(W.put_byte(w, 2n, v), 3n)] == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}
343	  %Equal.sym(U32, W.byte(W.put_byte(w, 2n, v), 2n), v, Y.byte_put_same(w, 2n, v, {==}, hv)) :
344	    {[W.byte(w, 0n), W.byte(w, 1n), _, W.byte(W.put_byte(w, 2n, v), 3n)] == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}
345	  %Equal.sym(U32, W.byte(W.put_byte(w, 2n, v), 3n), W.byte(w, 3n), Y.byte_put_other(w, 3n, 2n, v, hv, {==})) :
346	    {[W.byte(w, 0n), W.byte(w, 1n), v, _] == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}
347	  {==}
348	
349	law wbp3:
350	  for +w: U32
351	  for +v: U32
352	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
353	  {L4(W.put_byte(w, 3n, v)) == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}
354	
355	def wbp3(w, v, hv):
356	  %Equal.sym(U32, W.byte(W.put_byte(w, 3n, v), 0n), W.byte(w, 0n), Y.byte_put_other(w, 0n, 3n, v, hv, {==})) :
357	    {[_, W.byte(W.put_byte(w, 3n, v), 1n), W.byte(W.put_byte(w, 3n, v), 2n), W.byte(W.put_byte(w, 3n, v), 3n)] == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}
358	  %Equal.sym(U32, W.byte(W.put_byte(w, 3n, v), 1n), W.byte(w, 1n), Y.byte_put_other(w, 1n, 3n, v, hv, {==})) :
359	    {[W.byte(w, 0n), _, W.byte(W.put_byte(w, 3n, v), 2n), W.byte(W.put_byte(w, 3n, v), 3n)] == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}
360	  %Equal.sym(U32, W.byte(W.put_byte(w, 3n, v), 2n), W.byte(w, 2n), Y.byte_put_other(w, 2n, 3n, v, hv, {==})) :
361	    {[W.byte(w, 0n), W.byte(w, 1n), _, W.byte(W.put_byte(w, 3n, v), 3n)] == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}
362	  %Equal.sym(U32, W.byte(W.put_byte(w, 3n, v), 3n), v, Y.byte_put_same(w, 3n, v, {==}, hv)) :
363	    {[W.byte(w, 0n), W.byte(w, 1n), W.byte(w, 2n), _] == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}
364	  {==}
365	
366	law wbp:
367	  for +w: U32
368	  for +r: Nat
369	  for +v: U32
370	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
371	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
372	  {L4(W.put_byte(w, r, v)) == List.set(&2, U32, L4(w), r, v) : List<&2, U32>}
373	
374	def wbp(w, r, v, hr, hv):
375	  match r:
376	    case 0n:
377	      wbp0(w, v, hv)
378	    case 1n+r1:
379	      match r1:
380	        case 0n:
381	          wbp1(w, v, hv)
382	        case 1n+r2:
383	          match r2:
384	            case 0n:
385	              wbp2(w, v, hv)
386	            case 1n+r3:
387	              match r3:
388	                case 0n:
389	                  wbp3(w, v, hv)
390	                case 1n+r4:
391	                  Empty.absurd({L4(W.put_byte(w, 4n+r4, v)) == List.set(&2, U32, L4(w), 4n+r4, v) : List<&2, U32>},
392	                    AB.lt_zero_absurd(r4, hr))
393	
394	# Byte 4q + r of the word list after word q is written with its byte r set.
395	law unpack_set:
396	  for +ws: List<&2, U32>
397	  for +q: Nat
398	  for +r: Nat
399	  for +w: U32
400	  for +v: U32
401	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
402	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
403	  for +hw: {List.get(&2, U32, ws, q) == Some{w} : Maybe<&2, U32>}
404	  {D.unpack(List.set(&2, U32, ws, q, W.put_byte(w, r, v))) == List.set(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), r), v) : List<&2, U32>}
405	
406	def unpack_set(ws, q, r, w, v, hr, hv, hw):
407	  match ws q:
408	    case Nil{} _:
409	      {==}
410	    case Con{+x, t} 0n:
411	      +xw = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, x, m), Some{x}, Some{w}, hw)
412	      +U = D.unpack(t)
413	      %Equal.sym(U32, x, w, xw) :
414	        {List.append(&2, U32, L4(W.put_byte(w, r, v)), U) == List.set(&2, U32, List.append(&2, U32, L4(_), U), r, v) : List<&2, U32>}
415	      %Equal.sym(List<&2, U32>, List.set(&2, U32, List.append(&2, U32, L4(w), U), r, v),
416	        List.append(&2, U32, List.set(&2, U32, L4(w), r, v), U), AB.set_append_l(U32, L4(w), U, r, v, hr)) :
417	        {List.append(&2, U32, L4(W.put_byte(w, r, v)), U) == _ : List<&2, U32>}
418	      %wbp(w, r, v, hr, hv) : {List.append(&2, U32, L4(W.put_byte(w, r, v)), U) == List.append(&2, U32, _, U) : List<&2, U32>}
419	      {==}
420	    case Con{+x, t} 1n+p:
421	      %unpack_set(t, p, r, w, v, hr, hv, hw) :
422	        {List.append(&2, U32, L4(x), D.unpack(List.set(&2, U32, t, p, W.put_byte(w, r, v)))) == List.append(&2, U32, L4(x), _) : List<&2, U32>}
423	      {==}
424	
425	# The same for a U32 index.
426	law unpack_set_i:
427	  for +ws: List<&2, U32>
428	  for +i: U32
429	  for +w: U32
430	  for +v: U32
431	  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
432	  for +hw: {List.get(&2, U32, ws, U32.to_nat((i >> 2n : U32))) == Some{w} : Maybe<&2, U32>}
433	  {D.unpack(List.set(&2, U32, ws, U32.to_nat((i >> 2n : U32)), W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v))) == List.set(&2, U32, D.unpack(ws), U32.to_nat(i), v) : List<&2, U32>}
434	
435	def unpack_set_i(ws, i, w, v, hv, hw):
436	  +n = U32.to_nat(i)
437	  +eq = U.to_nat_shrn(i, 2n)
438	  %Equal.sym(Nat, U32.to_nat((i >> 2n : U32)), Nat.div(n, 4n), eq) :
439	    {D.unpack(List.set(&2, U32, ws, _, W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v))) == List.set(&2, U32, D.unpack(ws), n, v) : List<&2, U32>}
440	  %Equal.sym(Nat, U32.to_nat((i .&. 3 : U32)), Nat.mod(n, 4n), U.to_nat_and_mask(i, 3, 2n, {==})) :
441	    {D.unpack(List.set(&2, U32, ws, Nat.div(n, 4n), W.put_byte(w, _, v))) == List.set(&2, U32, D.unpack(ws), n, v) : List<&2, U32>}
442	  %N.div_mod(n, 4n) :
443	    {D.unpack(List.set(&2, U32, ws, Nat.div(n, 4n), W.put_byte(w, Nat.mod(n, 4n), v))) == List.set(&2, U32, D.unpack(ws), _, v) : List<&2, U32>}
444	  unpack_set(ws, Nat.div(n, 4n), Nat.mod(n, 4n), w, v, N.mod_lt(n, 4n, {==}), hv,
445	    AB.subst(Nat, x => {List.get(&2, U32, ws, x) == Some{w} : Maybe<&2, U32>}, U32.to_nat((i >> 2n : U32)), Nat.div(n, 4n), eq, hw))
446	
447	# Words of the block
448	# ==================
449	
450	# Word k (in range) is the k-th of the word list.
451	law wd_get:
452	  for +t: P.Tree<U32>
453	  for +d: Nat
454	  for +k: U32
455	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
456	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
457	  for +hk: {Nat.is_lt(U32.to_nat(k), Nat.pow(2n, d)) == True{} : Bool}
458	  {List.get(&2, U32, WL(t), U32.to_nat(k)) == Some{WD(t, k)} : Maybe<&2, U32>}
459	
460	def wd_get(t, d, k, hf, hd, hk):
461	  %I.slot_small_t(k, d, hk) : {List.get(&2, U32, WL(t), _) == Some{WD(t, k)} : Maybe<&2, U32>}
462	  Equal.sym(Maybe<&2, U32>, Some{WD(t, k)}, List.get(&2, U32, WL(t), A.slot(k, d)), I.get_view_t(U32, t, d, k, hf, lt32(d, hd)))
463	
464	# Writing word k (in range) sets the k-th of the word list.
465	law wl_set:
466	  for +t: P.Tree<U32>
467	  for +d: Nat
468	  for +k: U32
469	  for +w: U32
470	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
471	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
472	  for +hk: {Nat.is_lt(U32.to_nat(k), Nat.pow(2n, d)) == True{} : Bool}
473	  {WL(I.set_tree(U32, t, k, w)) == List.set(&2, U32, WL(t), U32.to_nat(k), w) : List<&2, U32>}
474	
475	def wl_set(t, d, k, w, hf, hd, hk):
476	  %I.set_tree_eq(U32, t, k, w) : {A.view(U32, _) == List.set(&2, U32, WL(t), U32.to_nat(k), w) : List<&2, U32>}
477	  %Equal.sym(List<&2, U32>, A.view(U32, Array.set(U32, P.fromT(U32, t), k, w)), List.set(&2, U32, WL(t), A.slot(k, d), w),
478	    I.set_view_t(U32, t, d, k, w, hf, lt32(d, hd))) :
479	    {_ == List.set(&2, U32, WL(t), U32.to_nat(k), w) : List<&2, U32>}
480	  %I.slot_small_t(k, d, hk) : {List.set(&2, U32, WL(t), A.slot(k, d), w) == List.set(&2, U32, WL(t), _, w) : List<&2, U32>}
481	  {==}
482	
483	law full_set:
484	  for +t: P.Tree<U32>
485	  for +d: Nat
486	  for +k: U32
487	  for +w: U32
488	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
489	  {A.full(U32, P.fromT(U32, I.set_tree(U32, t, k, w)), d) == True{} : Bool}
490	
491	def full_set(t, d, k, w, hf):
492	  %I.set_tree_eq(U32, t, k, w) : {A.full(U32, _, d) == True{} : Bool}
493	  S.set_full(U32, P.fromT(U32, t), d, k, w, hf)
494	
495	# Bounds: every length is at most 4 * 2^d <= 2^31, so sums of two fit in a U32
496	# ===========================================================================
497	
498	# 4 * 2^d < 2^e for d + 2 < e (e stays a variable here: 2^32 must never be
499	# unfolded, so the callers instantiate e = 32n only in the final type).
500	law four_lt_e:
501	  for +d: Nat
502	  for +e: Nat
503	  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
504	  {Nat.is_lt(Nat.mul(4n, Nat.pow(2n, d)), Nat.pow(2n, e)) == True{} : Bool}
505	
506	def four_lt_e(d, e, he):
507	  +P = Nat.pow(2n, d)
508	  %Equal.sym(Nat, Nat.mul(Nat.mul(2n, 2n), P), Nat.mul(2n, Nat.mul(2n, P)), N.mul_assoc(2n, 2n, P)) :
509	    {Nat.is_lt(_, Nat.pow(2n, e)) == True{} : Bool}
510	  AB.pow_lt(Nat.add(2n, d), e, he)
511	
512	law fits_e:
513	  for +x: Nat
514	  for +d: Nat
515	  for +e: Nat
516	  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
517	  for +hx: {Nat.is_le(x, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
518	  {Nat.is_lt(x, Nat.pow(2n, e)) == True{} : Bool}
519	
520	def fits_e(x, d, e, he, hx):
521	  N.le_lt_trans(x, Nat.mul(4n, Nat.pow(2n, d)), Nat.pow(2n, e), hx, four_lt_e(d, e, he))
522	
523	law he32:
524	  for +d: Nat
525	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
526	  {Nat.is_lt(Nat.add(2n, d), 32n) == True{} : Bool}
527	
528	def he32(d, hd):
529	  Equal.trans(Bool, Nat.is_lt(Nat.add(2n, d), 32n), Nat.is_le(d, 29n), True{}, N.lt_succ_iff(d, 29n), hd)
530	
531	# A sum of two words that stays within 4 * 2^d does not wrap.
532	law add_fits:
533	  for +a: U32
534	  for +b: U32
535	  for +d: Nat
536	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
537	  for +h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
538	  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
539	
540	def add_fits(a, b, d, hd, h):
541	  U.to_nat_add_fits_p(a, b, fits_e(Nat.add(U32.to_nat(a), U32.to_nat(b)), d, 32n, he32(d, hd), h))
542	
543	law succ_le:
544	  for +x: Nat
545	  for +m: Nat
546	  for +h: {Nat.is_lt(x, m) == True{} : Bool}
547	  {Nat.is_le(Nat.add(x, 1n), m) == True{} : Bool}
548	
549	def succ_le(x, m, h):
550	  %Equal.sym(Nat, Nat.add(x, 1n), 1n+x, N.add_one(x)) : {Nat.is_le(_, m) == True{} : Bool}
551	  Equal.trans(Bool, Nat.is_le(1n+x, m), Nat.is_lt(x, m), True{}, N.le_succ_lt(x, m), h)
552	
553	# An index below 4 * 2^d steps up by one.
554	law inc_fits:
555	  for +a: U32
556	  for +d: Nat
557	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
558	  for +h: {Nat.is_lt(U32.to_nat(a), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
559	  {U32.to_nat((a + 1 : U32)) == Nat.add(U32.to_nat(a), 1n) : Nat}
560	
561	def inc_fits(a, d, hd, h):
562	  add_fits(a, 1, d, hd, succ_le(U32.to_nat(a), Nat.mul(4n, Nat.pow(2n, d)), h))