proof_core.bend

lawful-bytes@0.1.1.0 · 562 lines · 40 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-words@0.1.0.0/defs.bend as W
5import lawful-words@0.1.0.0/proof_nat.bend as N
6import lawful-words@0.1.0.0/proof_u32.bend as U
7import lawful-words@0.1.0.0/proof_bytes.bend as Y
8import lawful-arrays@0.1.0.0/defs.bend as A
9import lawful-arrays@0.1.0.0/proof_base.bend as AB
10import lawful-arrays@0.1.0.0/proof_tree.bend as P
11import lawful-arrays@0.1.0.0/proof_index.bend as I
12import 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
19def BT(+len: U32, +t: P.Tree<U32>) -> D.Bytes:
20  D.Bytes{len, P.fromT(U32, t)}
21
22# The words of the block.
23def 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.
27def 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.
31def 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.
35def 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
45law 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
51def 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
57law 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
63def 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
72law 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
79def 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.
100law 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
107def 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.
117law 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
122def 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.
127law 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
132def 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
143law 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
150def 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
165law lt32:
166  for +d: Nat
167  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
168  {Nat.is_lt(d, 32n) == True{} : Bool}
169
170def 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.
174law 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
180def 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
188law 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
199def 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.
220def 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
223def 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
227def 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.
233def 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.
237law 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
244def 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
248law 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
255def 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
260law 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
267def 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.
273law 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
282def 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
294def 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).
298law 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
304def 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
315law 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
321def 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
332law 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
338def 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
349law 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
355def 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
366law 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
374def 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.
395law 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
406def 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.
426law 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
435def 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.
451law 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
460def 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.
465law 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
475def 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
483law 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
491def 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).
500law 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
506def 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
512law 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
520def 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
523law 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
528def 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.
532law 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
540def 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
543law 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
549def 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.
554law 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
561def 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))