proof_fast_append.bend

lawful-bytes@0.1.1.0 · 1,625 lines · 76 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-bytes@0.1.1.0/fast.bend as FA
5import lawful-bytes@0.1.1.0/proof_seq.bend as Q
6import lawful-bytes@0.1.1.0/proof_core.bend as C
7import lawful-bytes@0.1.1.0/proof_ops.bend as O
8import lawful-bytes@0.1.1.0/proof_append.bend as X
9import lawful-bytes@0.1.1.0/proof_shift.bend as H
10import lawful-words@0.1.0.0/defs.bend as W
11import lawful-words@0.1.0.0/proof_nat.bend as N
12import lawful-words@0.1.0.0/proof_u32.bend as U
13import lawful-words@0.1.0.0/proof_bytes.bend as Y
14import lawful-arrays@0.1.0.0/defs.bend as A
15import lawful-arrays@0.1.0.0/proof_base.bend as AB
16import lawful-arrays@0.1.0.0/proof_tree.bend as P
17import lawful-arrays@0.1.0.0/proof_index.bend as I
18
19# fast.bend's append on the mirror. The first bytes go through bytes.bend's
20# append (X.append_*_t), up to dst's next word boundary; then append.words
21# writes whole words, each the merge of two src words. AWT computes the tree
22# append.words leaves (aw_eq), and the view invariant (av) says that after the
23# words written so far the bytes in use are the target's. Up to 3 bytes past
24# the new length come from src bytes past s + n: they are outside the view.
25
26# Lists
27# =====
28
29law drop_drop:
30  for +xs: List<&2, U32>
31  for +a: Nat
32  for +b: Nat
33  {List.drop(&2, U32, List.drop(&2, U32, xs, a), b) == List.drop(&2, U32, xs, Nat.add(a, b)) : List<&2, U32>}
34
35def drop_drop(xs, a, b):
36  match xs a:
37    case Nil{} _:
38      {==}
39    case Con{x, t} 0n:
40      {==}
41    case Con{x, t} 1n+p:
42      drop_drop(t, p, b)
43
44# A list whose first element is b.
45law tcons:
46  for +ys: List<&2, U32>
47  for +b: U32
48  for +m: Nat
49  for +rest: List<&2, U32>
50  for +h: {List.get(&2, U32, ys, 0n) == Some{b} : Maybe<&2, U32>}
51  for +ht: {List.take(&2, U32, List.drop(&2, U32, ys, 1n), m) == rest : List<&2, U32>}
52  {List.take(&2, U32, ys, 1n+m) == b <> rest : List<&2, U32>}
53
54def tcons(ys, b, m, rest, h, ht):
55  match ys:
56    case Nil{}:
57      Empty.absurd({List.take(&2, U32, Nil{}, 1n+m) == b <> rest : List<&2, U32>}, X.none_some(b, h))
58    case Con{+y, t}:
59      %Equal.sym(U32, y, b, X.some_inj(y, b, h)) : {_ <> List.take(&2, U32, t, m) == b <> rest : List<&2, U32>}
60      %Equal.sym(List<&2, U32>, List.take(&2, U32, t, m), rest,
61        AB.subst(List<&2, U32>, z => {List.take(&2, U32, z, m) == rest : List<&2, U32>}, List.drop(&2, U32, t, 0n), t, X.drop_zero(t), ht)) :
62        {b <> _ == b <> rest : List<&2, U32>}
63      {==}
64
65# The first m (<= 4) elements of ys are b0 .. b3, given each one asked for.
66law tg1:
67  for +ys: List<&2, U32>
68  for +m: Nat
69  for +b0: U32
70  for +hm: {Nat.is_le(m, 1n) == True{} : Bool}
71  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
72  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0], m) : List<&2, U32>}
73
74def tg1(ys, m, b0, hm, g0):
75  match m:
76    case 0n:
77      Q.take_zero(ys)
78    case 1n+m1:
79      match m1:
80        case 0n:
81          tcons(ys, b0, 0n, Nil{}, g0({==}), Q.take_zero(List.drop(&2, U32, ys, 1n)))
82        case 1n+m2:
83          Empty.absurd({List.take(&2, U32, ys, 2n+m2) == List.take(&2, U32, [b0], 2n+m2) : List<&2, U32>}, AB.false_ne_true(hm))
84
85law tg2:
86  for +ys: List<&2, U32>
87  for +m: Nat
88  for +b0: U32
89  for +b1: U32
90  for +hm: {Nat.is_le(m, 2n) == True{} : Bool}
91  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
92  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
93  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1], m) : List<&2, U32>}
94
95def tg2(ys, m, b0, b1, hm, g0, g1):
96  match m:
97    case 0n:
98      Q.take_zero(ys)
99    case 1n+m1:
100      tcons(ys, b0, m1, List.take(&2, U32, [b1], m1), g0({==}),
101        tg1(List.drop(&2, U32, ys, 1n), m1, b1, hm,
102          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
103            H.get_drop(ys, 1n, 0n), g1(h))))
104
105law tg3:
106  for +ys: List<&2, U32>
107  for +m: Nat
108  for +b0: U32
109  for +b1: U32
110  for +b2: U32
111  for +hm: {Nat.is_le(m, 3n) == True{} : Bool}
112  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
113  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
114  for g2: {Nat.is_lt(2n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 2n) == Some{b2} : Maybe<&2, U32>}
115  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1, b2], m) : List<&2, U32>}
116
117def tg3(ys, m, b0, b1, b2, hm, g0, g1, g2):
118  match m:
119    case 0n:
120      Q.take_zero(ys)
121    case 1n+m1:
122      tcons(ys, b0, m1, List.take(&2, U32, [b1, b2], m1), g0({==}),
123        tg2(List.drop(&2, U32, ys, 1n), m1, b1, b2, hm,
124          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
125            H.get_drop(ys, 1n, 0n), g1(h)),
126          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 1n), List.get(&2, U32, ys, 2n), Some{b2},
127            H.get_drop(ys, 1n, 1n), g2(h))))
128
129law tg4:
130  for +ys: List<&2, U32>
131  for +m: Nat
132  for +b0: U32
133  for +b1: U32
134  for +b2: U32
135  for +b3: U32
136  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
137  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
138  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
139  for g2: {Nat.is_lt(2n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 2n) == Some{b2} : Maybe<&2, U32>}
140  for g3: {Nat.is_lt(3n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 3n) == Some{b3} : Maybe<&2, U32>}
141  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1, b2, b3], m) : List<&2, U32>}
142
143def tg4(ys, m, b0, b1, b2, b3, hm, g0, g1, g2, g3):
144  match m:
145    case 0n:
146      Q.take_zero(ys)
147    case 1n+m1:
148      tcons(ys, b0, m1, List.take(&2, U32, [b1, b2, b3], m1), g0({==}),
149        tg3(List.drop(&2, U32, ys, 1n), m1, b1, b2, b3, hm,
150          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
151            H.get_drop(ys, 1n, 0n), g1(h)),
152          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 1n), List.get(&2, U32, ys, 2n), Some{b2},
153            H.get_drop(ys, 1n, 1n), g2(h)),
154          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 2n), List.get(&2, U32, ys, 3n), Some{b3},
155            H.get_drop(ys, 1n, 2n), g3(h))))
156
157# Writing word q replaces bytes 4q .. 4q+3 of the unpacked list.
158law us1:
159  for +ws: List<&2, U32>
160  for +q: Nat
161  for +x: U32
162  for +m: Nat
163  for +hq: {Nat.is_lt(q, List.length(&2, U32, ws)) == True{} : Bool}
164  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
165  {List.take(&2, U32, D.unpack(List.set(&2, U32, ws, q, x)), Nat.add(Nat.mul(q, 4n), m)) == List.append(&2, U32, List.take(&2, U32, D.unpack(ws), Nat.mul(q, 4n)), List.take(&2, U32, C.L4(x), m)) : List<&2, U32>}
166
167def us1(ws, q, x, m, hq, hm):
168  match ws q:
169    case Nil{} _:
170      Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(Nat.mul(q, 4n), m)) == List.append(&2, U32, List.take(&2, U32, Nil{}, Nat.mul(q, 4n)), List.take(&2, U32, C.L4(x), m)) : List<&2, U32>},
171        AB.lt_zero_absurd(q, hq))
172    case Con{w0, t} 0n:
173      Q.take_append_l(C.L4(x), D.unpack(t), m, hm)
174    case Con{+w0, t} 1n+p:
175      %us1(t, p, x, m, hq, hm) :
176        {W.byte(w0, 0n) <> W.byte(w0, 1n) <> W.byte(w0, 2n) <> W.byte(w0, 3n) <> List.take(&2, U32, D.unpack(List.set(&2, U32, t, p, x)), Nat.add(Nat.mul(p, 4n), m))
177          == W.byte(w0, 0n) <> W.byte(w0, 1n) <> W.byte(w0, 2n) <> W.byte(w0, 3n) <> _ : List<&2, U32>}
178      {==}
179
180law take_split:
181  for +ys: List<&2, U32>
182  for +a: Nat
183  for +m: Nat
184  {List.append(&2, U32, List.take(&2, U32, ys, a), List.take(&2, U32, List.drop(&2, U32, ys, a), m)) == List.take(&2, U32, ys, Nat.add(a, m)) : List<&2, U32>}
185
186def take_split(ys, a, m):
187  match ys a:
188    case Nil{} _:
189      {==}
190    case Con{y, t} 0n:
191      {==}
192    case Con{+y, t} 1n+p:
193      %take_split(t, p, m) :
194        {y <> List.append(&2, U32, List.take(&2, U32, t, p), List.take(&2, U32, List.drop(&2, U32, t, p), m)) == y <> _ : List<&2, U32>}
195      {==}
196
197law slice_split:
198  for +xs: List<&2, U32>
199  for +s: Nat
200  for +a: Nat
201  for +b: Nat
202  {List.append(&2, U32, D.slice(xs, s, a), D.slice(xs, Nat.add(s, a), b)) == D.slice(xs, s, Nat.add(a, b)) : List<&2, U32>}
203
204def slice_split(xs, s, a, b):
205  %drop_drop(xs, s, a) :
206    {List.append(&2, U32, D.slice(xs, s, a), List.take(&2, U32, _, b)) == D.slice(xs, s, Nat.add(a, b)) : List<&2, U32>}
207  take_split(List.drop(&2, U32, xs, s), a, b)
208
209# A slice of the first l elements, inside them.
210law slice_take:
211  for +xs: List<&2, U32>
212  for +l: Nat
213  for +q: Nat
214  for +n: Nat
215  for +h: {Nat.is_le(Nat.add(q, n), l) == True{} : Bool}
216  {D.slice(List.take(&2, U32, xs, l), q, n) == List.take(&2, U32, List.drop(&2, U32, xs, q), n) : List<&2, U32>}
217
218def slice_take(xs, l, q, n, h):
219  match xs l q n:
220    case Nil{} _ _ _:
221      {==}
222    case Con{x, t} 0n 0n 0n:
223      {==}
224    case Con{x, t} 0n 0n 1n+n1:
225      Empty.absurd({List.take(&2, U32, Nil{}, 1n+n1) == x <> List.take(&2, U32, t, n1) : List<&2, U32>}, AB.false_ne_true(h))
226    case Con{x, t} 0n 1n+q1 _:
227      Empty.absurd({List.take(&2, U32, List.drop(&2, U32, Nil{}, 1n+q1), n) == List.take(&2, U32, List.drop(&2, U32, t, q1), n) : List<&2, U32>},
228        AB.false_ne_true(h))
229    case Con{x, t} 1n+l1 0n _:
230      Q.take_take(x <> t, 1n+l1, n, h)
231    case Con{x, t} 1n+l1 1n+q1 _:
232      slice_take(t, l1, q1, n, h)
233
234law slice_length:
235  for +xs: List<&2, U32>
236  for +s: Nat
237  for +a: Nat
238  for +h: {Nat.is_le(Nat.add(s, a), List.length(&2, U32, xs)) == True{} : Bool}
239  {List.length(&2, U32, D.slice(xs, s, a)) == a : Nat}
240
241def slice_length(xs, s, a, h):
242  Q.take_length(List.drop(&2, U32, xs, s), a,
243    AB.subst(Nat, y => {Nat.is_le(a, y) == True{} : Bool}, Nat.sub(List.length(&2, U32, xs), s), List.length(&2, U32, List.drop(&2, U32, xs, s)),
244      Equal.sym(Nat, List.length(&2, U32, List.drop(&2, U32, xs, s)), Nat.sub(List.length(&2, U32, xs), s), H.drop_length(xs, s)),
245      N.le_sub_r(s, a, List.length(&2, U32, xs), h)))
246
247# Nat
248# ===
249
250law le_antisym:
251  for +a: Nat
252  for +b: Nat
253  for +h1: {Nat.is_le(a, b) == True{} : Bool}
254  for +h2: {Nat.is_le(b, a) == True{} : Bool}
255  {a == b : Nat}
256
257def le_antisym(a, b, h1, h2):
258  match a b:
259    case 0n 0n:
260      {==}
261    case 0n 1n+q:
262      Empty.absurd({0n == 1n+q : Nat}, AB.false_ne_true(h2))
263    case 1n+p 0n:
264      Empty.absurd({1n+p == 0n : Nat}, AB.false_ne_true(h1))
265    case 1n+p 1n+q:
266      %le_antisym(p, q, h1, h2) : {1n+p == 1n+_ : Nat}
267      {==}
268
269law min_l:
270  for +a: Nat
271  for +b: Nat
272  for +h: {Nat.is_lt(a, b) == True{} : Bool}
273  {Nat.min(a, b) == a : Nat}
274
275def min_l(a, b, h):
276  match a b:
277    case 0n _:
278      {==}
279    case 1n+p 0n:
280      Empty.absurd({0n == 1n+p : Nat}, AB.false_ne_true(h))
281    case 1n+p 1n+q:
282      %min_l(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
283      {==}
284
285law min_r:
286  for +a: Nat
287  for +b: Nat
288  for +h: {Nat.is_lt(a, b) == False{} : Bool}
289  {Nat.min(a, b) == b : Nat}
290
291def min_r(a, b, h):
292  match a b:
293    case 0n 0n:
294      {==}
295    case 0n 1n+q:
296      Empty.absurd({0n == 1n+q : Nat}, AB.true_ne_false(h))
297    case 1n+p 0n:
298      {==}
299    case 1n+p 1n+q:
300      %min_r(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
301      {==}
302
303law min_le:
304  for +a: Nat
305  for +b: Nat
306  {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}
307
308def min_le(a, b):
309  match a b:
310    case 0n _:
311      N.le_zero_l(b)
312    case 1n+p 0n:
313      {==}
314    case 1n+p 1n+q:
315      min_le(p, q)
316
317law lt_w:
318  for +w: Nat
319  for +x: Nat
320  for +pp: Nat
321  for +h: {Nat.is_lt(Nat.add(Nat.mul(w, 4n), x), Nat.mul(4n, pp)) == True{} : Bool}
322  {Nat.is_lt(w, pp) == True{} : Bool}
323
324def lt_w(w, x, pp, h):
325  N.lt_mul_cancel(4n, w, pp,
326    AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, pp)) == True{} : Bool}, Nat.mul(w, 4n), Nat.mul(4n, w), N.mul_comm(w, 4n),
327      N.le_lt_trans(Nat.mul(w, 4n), Nat.add(Nat.mul(w, 4n), x), Nat.mul(4n, pp), N.le_add_r(Nat.mul(w, 4n), x), h)))
328
329law lt8:
330  for +r: Nat
331  for +j: Nat
332  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
333  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
334  {Nat.is_lt(Nat.add(r, j), 8n) == True{} : Bool}
335
336def lt8(r, j, hr, hj):
337  match r:
338    case 0n:
339      N.lt_trans(j, 4n, 8n, hj, {==})
340    case 1n+r1:
341      match r1:
342        case 0n:
343          N.lt_trans(j, 4n, 7n, hj, {==})
344        case 1n+r2:
345          match r2:
346            case 0n:
347              N.lt_trans(j, 4n, 6n, hj, {==})
348            case 1n+r3:
349              match r3:
350                case 0n:
351                  N.lt_trans(j, 4n, 5n, hj, {==})
352                case 1n+r4:
353                  Empty.absurd({Nat.is_lt(Nat.add(4n+r4, j), 8n) == True{} : Bool}, AB.lt_zero_absurd(r4, hr))
354
355law sub4_lt:
356  for +x: Nat
357  for +h: {Nat.is_lt(x, 8n) == True{} : Bool}
358  {Nat.is_lt(Nat.sub(x, 4n), 4n) == True{} : Bool}
359
360def sub4_lt(x, h):
361  match x:
362    case 0n:
363      {==}
364    case 1n+x1:
365      match x1:
366        case 0n:
367          {==}
368        case 1n+x2:
369          match x2:
370            case 0n:
371              {==}
372            case 1n+x3:
373              match x3:
374                case 0n:
375                  {==}
376                case 1n+x4:
377                  %Equal.sym(Nat, Nat.sub(x4, 0n), x4, N.sub_zero(x4)) : {Nat.is_lt(_, 4n) == True{} : Bool}
378                  h
379
380# Index 4w + x for x >= 4 is index 4(w + 1) + (x - 4).
381law idx_up:
382  for +w: Nat
383  for +x: Nat
384  for +h: {Nat.is_le(4n, x) == True{} : Bool}
385  {Nat.add(Nat.mul(w, 4n), x) == Nat.add(Nat.mul(1n+w, 4n), Nat.sub(x, 4n)) : Nat}
386
387def idx_up(w, x, h):
388  %Equal.sym(Nat, x, Nat.add(4n, Nat.sub(x, 4n)), Equal.sym(Nat, Nat.add(4n, Nat.sub(x, 4n)), x, N.le_sub_add(4n, x, h))) :
389    {Nat.add(Nat.mul(w, 4n), _) == Nat.add(Nat.mul(1n+w, 4n), Nat.sub(x, 4n)) : Nat}
390  N.add_left_comm(Nat.mul(w, 4n), 4n, Nat.sub(x, 4n))
391
392# Words and shifts
393# ================
394
395# The tree append.words leaves: p is the word read next (hi), lo the word
396# before it, td the dst block, di the dst word written, sh the shift in bits.
397def AWT(n: Nat, +ts: P.Tree<U32>, +p: U32, +lo: U32, +td: P.Tree<U32>, +si: U32, +di: U32, +sh: Nat) -> P.Tree<U32>:
398  match n:
399    case 0n:
400      td
401    case 1n+k:
402      +hi = C.WD(ts, p)
403      AWT(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))), (si + 1 : U32), (di + 1 : U32), sh)
404
405law aw_eq:
406  for +n: Nat
407  for +ts: P.Tree<U32>
408  for +p: U32
409  for +lo: U32
410  for +td: P.Tree<U32>
411  for +si: U32
412  for +di: U32
413  for +sh: Nat
414  {FA.append.words(n, Array.get(U32, P.fromT(U32, ts), p), lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
415
416def aw_eq(n, ts, p, lo, td, si, di, sh):
417  match n:
418    case 0n:
419      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), p), (P.fromT(U32, ts), C.WD(ts, p)), P.get_pair_t(U32, ts, p)) :
420        {FA.append.words(0n, _, lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, td), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
421      {==}
422    case 1n+k:
423      +hi = C.WD(ts, p)
424      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
425      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), p), (P.fromT(U32, ts), hi), P.get_pair_t(U32, ts, p)) :
426        {FA.append.words(1n+k, _, lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, AWT(1n+k, ts, p, lo, td, si, di, sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
427      %Equal.sym(Array<U32>, Array.set(U32, P.fromT(U32, td), di, mw), P.fromT(U32, I.set_tree(U32, td, di, mw)), I.set_tree_eq(U32, td, di, mw)) :
428        {FA.append.words(k, Array.get(U32, P.fromT(U32, ts), (si + 2 : U32)), hi, _, (si + 1 : U32), (di + 1 : U32), sh) == (P.fromT(U32, AWT(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
429      aw_eq(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh)
430
431# The code's shifted pair is lawful-words' merge.
432law mrg2:
433  for +lo: U32
434  for +hi: U32
435  for +r: Nat
436  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
437  {U32.or(U32.shrn(lo, Nat.mul(8n, r)), U32.shln(hi, Nat.sub(32n, Nat.mul(8n, r)))) == W.merge(lo, hi, r) : U32}
438
439def mrg2(lo, hi, r, hr):
440  match r:
441    case 0n:
442      {==}
443    case 1n+r1:
444      match r1:
445        case 0n:
446          {==}
447        case 1n+r2:
448          match r2:
449            case 0n:
450              {==}
451            case 1n+r3:
452              match r3:
453                case 0n:
454                  {==}
455                case 1n+r4:
456                  Empty.absurd({U32.or(U32.shrn(lo, Nat.mul(8n, 4n+r4)), U32.shln(hi, Nat.sub(32n, Nat.mul(8n, 4n+r4)))) == W.merge(lo, hi, 4n+r4) : U32},
457                    AB.lt_zero_absurd(r4, hr))
458
459law mrg:
460  for +lo: U32
461  for +hi: U32
462  for +sh: Nat
463  for +r: Nat
464  for +hsh: {sh == Nat.mul(8n, r) : Nat}
465  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
466  {U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh))) == W.merge(lo, hi, r) : U32}
467
468def mrg(lo, hi, sh, r, hsh, hr):
469  %Equal.sym(Nat, sh, Nat.mul(8n, r), hsh) : {U32.or(U32.shrn(lo, _), U32.shln(hi, Nat.sub(32n, _))) == W.merge(lo, hi, r) : U32}
470  mrg2(lo, hi, r, hr)
471
472law and3_lt:
473  for +q: U32
474  {Nat.is_lt(U32.to_nat((q .&. 3 : U32)), 4n) == True{} : Bool}
475
476def and3_lt(q):
477  AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(U32.to_nat(q), 4n), U32.to_nat((q .&. 3 : U32)),
478    Equal.sym(Nat, U32.to_nat((q .&. 3 : U32)), Nat.mod(U32.to_nat(q), 4n), U.to_nat_and_mask(q, 3, 2n, {==})),
479    N.mod_lt(U32.to_nat(q), 4n, {==}))
480
481law shq2:
482  for +x: U32
483  for +r: Nat
484  for +e: {U32.to_nat(x) == r : Nat}
485  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
486  {U32.to_nat((x << 3n : U32)) == Nat.mul(8n, U32.to_nat(x)) : Nat}
487
488def shq2(x, r, e, hr):
489  match r:
490    case 0n:
491      %Equal.sym(U32, x, 0, U.to_nat_inj(x, 0, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
492      {==}
493    case 1n+r1:
494      match r1:
495        case 0n:
496          %Equal.sym(U32, x, 1, U.to_nat_inj(x, 1, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
497          {==}
498        case 1n+r2:
499          match r2:
500            case 0n:
501              %Equal.sym(U32, x, 2, U.to_nat_inj(x, 2, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
502              {==}
503            case 1n+r3:
504              match r3:
505                case 0n:
506                  %Equal.sym(U32, x, 3, U.to_nat_inj(x, 3, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
507                  {==}
508                case 1n+r4:
509                  Empty.absurd({U32.to_nat((x << 3n : U32)) == Nat.mul(8n, U32.to_nat(x)) : Nat}, AB.lt_zero_absurd(r4, hr))
510
511# The shift of append.w is 8 * (q & 3).
512law shq:
513  for +q: U32
514  {U32.to_nat(((q .&. 3 : U32) << 3n : U32)) == Nat.mul(8n, U32.to_nat((q .&. 3 : U32))) : Nat}
515
516def shq(q):
517  shq2((q .&. 3 : U32), U32.to_nat((q .&. 3 : U32)), {==}, and3_lt(q))
518
519# Bytes of a merged word
520# ======================
521
522def US(+ts: P.Tree<U32>) -> List<&2, U32>:
523  D.unpack(C.WL(ts))
524
525law mb_lo:
526  for +ts: P.Tree<U32>
527  for +e: Nat
528  for +si: U32
529  for +p: U32
530  for +lo: U32
531  for +r: Nat
532  for +j: Nat
533  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
534  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
535  for +hlo: {lo == C.WD(ts, si) : U32}
536  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
537  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == True{} : Bool}
538  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
539
540def mb_lo(ts, e, si, p, lo, r, j, hf, he, hlo, hb, hq):
541  +w = U32.to_nat(si)
542  +hi = C.WD(ts, p)
543  +RHS = {Some{W.byte(W.merge(lo, hi, r), j)} : Maybe<&2, U32>}
544  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, US(ts), Nat.add(Nat.mul(w, 4n), Nat.add(r, j))), C.mb(List.get(&2, U32, C.WL(ts), w), Nat.add(r, j)),
545    C.unpack_get(C.WL(ts), w, Nat.add(r, j), hq)) :
546    {_ == RHS : Maybe<&2, U32>}
547  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, C.WL(ts), w), Some{C.WD(ts, si)}, C.wd_get(ts, e, si, hf, he, lt_w(w, Nat.add(r, j), Nat.pow(2n, e), hb))) :
548    {C.mb(_, Nat.add(r, j)) == RHS : Maybe<&2, U32>}
549  %Equal.sym(U32, W.byte(W.merge(lo, hi, r), j), W.byte(lo, Nat.add(j, r)),
550    Y.byte_merge_lo(lo, hi, r, j, AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.add(r, j), Nat.add(j, r), N.add_comm(r, j), hq))) :
551    {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{_} : Maybe<&2, U32>}
552  %Equal.sym(U32, lo, C.WD(ts, si), hlo) : {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{W.byte(_, Nat.add(j, r))} : Maybe<&2, U32>}
553  %N.add_comm(r, j) : {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{W.byte(C.WD(ts, si), _)} : Maybe<&2, U32>}
554  {==}
555
556law mb_hi:
557  for +ts: P.Tree<U32>
558  for +e: Nat
559  for +si: U32
560  for +p: U32
561  for +lo: U32
562  for +r: Nat
563  for +j: Nat
564  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
565  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
566  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
567  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
568  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
569  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
570  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == False{} : Bool}
571  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
572
573def mb_hi(ts, e, si, p, lo, r, j, hf, he, hp, hr, hj, hb, hq):
574  +w = U32.to_nat(si)
575  +hi = C.WD(ts, p)
576  +x = Nat.add(r, j)
577  +z = Nat.sub(x, 4n)
578  +RHS = {Some{W.byte(W.merge(lo, hi, r), j)} : Maybe<&2, U32>}
579  +h4 = N.not_lt_le(x, 4n, hq)
580  +eu = idx_up(w, x, h4)
581  +hz = sub4_lt(x, lt8(r, j, hr, hj))
582  +ep = Equal.trans(Nat, U32.to_nat(p), Nat.add(w, 1n), 1n+w, hp, N.add_one(w))
583  +hb2 = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(Nat.mul(w, 4n), x), Nat.add(Nat.mul(1n+w, 4n), z), eu, hb)
584  +hpl = AB.subst(Nat, y => {Nat.is_lt(y, Nat.pow(2n, e)) == True{} : Bool}, 1n+w, U32.to_nat(p), Equal.sym(Nat, U32.to_nat(p), 1n+w, ep),
585    lt_w(1n+w, z, Nat.pow(2n, e), hb2))
586  +gp = AB.subst(Nat, y => {List.get(&2, U32, C.WL(ts), y) == Some{hi} : Maybe<&2, U32>}, U32.to_nat(p), 1n+w, ep, C.wd_get(ts, e, p, hf, he, hpl))
587  %Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), x), Nat.add(Nat.mul(1n+w, 4n), z), eu) : {List.get(&2, U32, US(ts), _) == RHS : Maybe<&2, U32>}
588  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, US(ts), Nat.add(Nat.mul(1n+w, 4n), z)), C.mb(List.get(&2, U32, C.WL(ts), 1n+w), z),
589    C.unpack_get(C.WL(ts), 1n+w, z, hz)) :
590    {_ == RHS : Maybe<&2, U32>}
591  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, C.WL(ts), 1n+w), Some{hi}, gp) : {C.mb(_, z) == RHS : Maybe<&2, U32>}
592  %Equal.sym(U32, W.byte(W.merge(lo, hi, r), j), W.byte(hi, Nat.sub(Nat.add(j, r), 4n)),
593    Y.byte_merge_hi(lo, hi, r, j, N.lt_to_le(r, 4n, hr), hj,
594      AB.subst(Nat, y => {Nat.is_le(4n, y) == True{} : Bool}, x, Nat.add(j, r), N.add_comm(r, j), h4))) :
595    {Some{W.byte(hi, z)} == Some{_} : Maybe<&2, U32>}
596  %N.add_comm(r, j) : {Some{W.byte(hi, z)} == Some{W.byte(hi, Nat.sub(_, 4n))} : Maybe<&2, U32>}
597  {==}
598
599law gsel:
600  for +ts: P.Tree<U32>
601  for +e: Nat
602  for +si: U32
603  for +p: U32
604  for +lo: U32
605  for +r: Nat
606  for +j: Nat
607  for +b: Bool
608  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
609  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
610  for +hlo: {lo == C.WD(ts, si) : U32}
611  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
612  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
613  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
614  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
615  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == b : Bool}
616  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
617
618def gsel(ts, e, si, p, lo, r, j, b, hf, he, hlo, hp, hr, hj, hb, hq):
619  match b:
620    case True{}:
621      mb_lo(ts, e, si, p, lo, r, j, hf, he, hlo, hb, hq)
622    case False{}:
623      mb_hi(ts, e, si, p, lo, r, j, hf, he, hp, hr, hj, hb, hq)
624
625# Byte j of the window at 4 si + r, for j below m.
626law gj:
627  for +ts: P.Tree<U32>
628  for +e: Nat
629  for +si: U32
630  for +p: U32
631  for +lo: U32
632  for +r: Nat
633  for +m: Nat
634  for +j: Nat
635  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
636  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
637  for +hlo: {lo == C.WD(ts, si) : U32}
638  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
639  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
640  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
641  for +hb: {Nat.is_le(Nat.add(Nat.add(Nat.mul(U32.to_nat(si), 4n), r), m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
642  for +hjm: {Nat.is_lt(j, m) == True{} : Bool}
643  {List.get(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r)), j) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
644
645def gj(ts, e, si, p, lo, r, m, j, hf, he, hlo, hp, hr, hm, hb, hjm):
646  +X = Nat.mul(U32.to_nat(si), 4n)
647  +ea = N.add_assoc(X, r, j)
648  +hbj = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(Nat.add(X, r), j), Nat.add(X, Nat.add(r, j)), ea,
649    N.lt_le_trans(Nat.add(Nat.add(X, r), j), Nat.add(Nat.add(X, r), m), Nat.mul(4n, Nat.pow(2n, e)), N.lt_add_l(Nat.add(X, r), j, m, hjm), hb))
650  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, US(ts), Nat.add(X, r)), j), List.get(&2, U32, US(ts), Nat.add(Nat.add(X, r), j)), H.get_drop(US(ts), Nat.add(X, r), j)) :
651    {_ == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
652  %Equal.sym(Nat, Nat.add(Nat.add(X, r), j), Nat.add(X, Nat.add(r, j)), ea) : {List.get(&2, U32, US(ts), _) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
653  gsel(ts, e, si, p, lo, r, j, Nat.is_lt(Nat.add(r, j), 4n), hf, he, hlo, hp, hr, N.lt_le_trans(j, m, 4n, hjm, hm), hbj, {==})
654
655# The first m bytes of a merged word are the m src bytes from 4 si + r.
656law win:
657  for +ts: P.Tree<U32>
658  for +e: Nat
659  for +si: U32
660  for +p: U32
661  for +lo: U32
662  for +r: Nat
663  for +m: Nat
664  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
665  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
666  for +hlo: {lo == C.WD(ts, si) : U32}
667  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
668  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
669  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
670  for +hb: {Nat.is_le(Nat.add(Nat.add(Nat.mul(U32.to_nat(si), 4n), r), m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
671  {List.take(&2, U32, C.L4(W.merge(lo, C.WD(ts, p), r)), m) == List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r)), m) : List<&2, U32>}
672
673def win(ts, e, si, p, lo, r, m, hf, he, hlo, hp, hr, hm, hb):
674  +mw = W.merge(lo, C.WD(ts, p), r)
675  +ys = List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r))
676  Equal.sym(List<&2, U32>, List.take(&2, U32, ys, m), List.take(&2, U32, C.L4(mw), m),
677    tg4(ys, m, W.byte(mw, 0n), W.byte(mw, 1n), W.byte(mw, 2n), W.byte(mw, 3n), hm,
678      h => gj(ts, e, si, p, lo, r, m, 0n, hf, he, hlo, hp, hr, hm, hb, h),
679      h => gj(ts, e, si, p, lo, r, m, 1n, hf, he, hlo, hp, hr, hm, hb, h),
680      h => gj(ts, e, si, p, lo, r, m, 2n, hf, he, hlo, hp, hr, hm, hb, h),
681      h => gj(ts, e, si, p, lo, r, m, 3n, hf, he, hlo, hp, hr, hm, hb, h)))
682
683# Nat facts for the word loop
684# ===========================
685
686law lt_w0:
687  for +w: Nat
688  for +pp: Nat
689  for +h: {Nat.is_lt(Nat.mul(w, 4n), Nat.mul(4n, pp)) == True{} : Bool}
690  {Nat.is_lt(w, pp) == True{} : Bool}
691
692def lt_w0(w, pp, h):
693  N.lt_mul_cancel(4n, w, pp, AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, pp)) == True{} : Bool}, Nat.mul(w, 4n), Nat.mul(4n, w), N.mul_comm(w, 4n), h))
694
695law le_x4:
696  for +w: Nat
697  {Nat.is_le(w, Nat.mul(w, 4n)) == True{} : Bool}
698
699def le_x4(w):
700  AB.subst(Nat, y => {Nat.is_le(w, y) == True{} : Bool}, Nat.mul(4n, w), Nat.mul(w, 4n), N.mul_comm(4n, w), N.le_add_r(w, Nat.mul(3n, w)))
701
702law four_alg:
703  for +a: Nat
704  for +b: Nat
705  {Nat.add(4n, Nat.add(a, b)) == Nat.add(a, Nat.add(b, 4n)) : Nat}
706
707def four_alg(a, b):
708  %N.add_comm(4n, b) : {Nat.add(4n, Nat.add(a, b)) == Nat.add(a, _) : Nat}
709  Equal.sym(Nat, Nat.add(a, Nat.add(4n, b)), Nat.add(4n, Nat.add(a, b)), N.add_left_comm(a, 4n, b))
710
711law c4:
712  for +o: Nat
713  for +y: Nat
714  for +np: Nat
715  for +h: {Nat.is_lt(Nat.add(o, Nat.add(4n, y)), Nat.add(np, 4n)) == True{} : Bool}
716  {Nat.is_lt(Nat.add(o, y), np) == True{} : Bool}
717
718def c4(o, y, np, h):
719  +h2 = AB.subst(Nat, z => {Nat.is_lt(z, Nat.add(np, 4n)) == True{} : Bool}, Nat.add(o, Nat.add(4n, y)), Nat.add(4n, Nat.add(o, y)), N.add_left_comm(o, 4n, y), h)
720  AB.subst(Nat, z => {Nat.is_lt(Nat.add(4n, Nat.add(o, y)), z) == True{} : Bool}, Nat.add(np, 4n), Nat.add(4n, np), N.add_comm(np, 4n), h2)
721
722law w2_bound:
723  for +w: Nat
724  for +pp: Nat
725  for +hp: {Nat.is_lt(0n, pp) == True{} : Bool}
726  for +h: {Nat.is_lt(w, pp) == True{} : Bool}
727  {Nat.is_le(Nat.add(w, 2n), Nat.mul(4n, pp)) == True{} : Bool}
728
729def w2_bound(w, pp, hp, h):
730  +R = Nat.add(pp, Nat.add(pp, Nat.add(pp, 0n)))
731  +h1 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(pp, 1n)) == True{} : Bool}, Nat.add(Nat.add(w, 1n), 1n), Nat.add(w, 2n), N.add_assoc(w, 1n, 1n),
732    N.le_add_mono_r(1n, Nat.add(w, 1n), pp, C.succ_le(w, pp, h)))
733  N.le_trans(Nat.add(w, 2n), Nat.add(pp, 1n), Nat.mul(4n, pp), h1,
734    N.le_add_mono_l(pp, 1n, R, Equal.trans(Bool, Nat.is_le(1n, R), Nat.is_lt(0n, R), True{}, N.le_succ_lt(0n, R), N.pos_add_l(pp, Nat.add(pp, Nat.add(pp, 0n)), hp))))
735
736law sub_le_of:
737  for +a: Nat
738  for +b: Nat
739  for +c: Nat
740  for +h: {Nat.is_le(a, Nat.add(b, c)) == True{} : Bool}
741  {Nat.is_le(Nat.sub(a, b), c) == True{} : Bool}
742
743def sub_le_of(a, b, c, h):
744  match a b:
745    case 0n _:
746      N.le_zero_l(c)
747    case 1n+p 0n:
748      h
749    case 1n+p 1n+q:
750      sub_le_of(p, q, c, h)
751
752# One word written
753# ================
754
755law step:
756  for +ts: P.Tree<U32>
757  for +e: Nat
758  for +td: P.Tree<U32>
759  for +d: Nat
760  for +p: U32
761  for +lo: U32
762  for +si: U32
763  for +di: U32
764  for +sh: Nat
765  for +l1: Nat
766  for +qn: Nat
767  for +r: Nat
768  for +o: Nat
769  for +np: Nat
770  for +v1: List<&2, U32>
771  for +m: Nat
772  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
773  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
774  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
775  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
776  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
777  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
778  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
779  for +hlo: {lo == C.WD(ts, si) : U32}
780  for +hsh: {sh == Nat.mul(8n, r) : Nat}
781  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
782  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
783  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
784  for +ho: {Nat.is_lt(o, np) == True{} : Bool}
785  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
786  for +hmv: {Nat.is_le(Nat.add(o, m), np) == True{} : Bool}
787  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
788  {List.take(&2, U32, US(I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh))))), Nat.add(l1, Nat.add(o, m))) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), Nat.add(o, m))) : List<&2, U32>}
789
790def step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, m, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, hm, hmv, hinv):
791  +hi = C.WD(ts, p)
792  +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
793  +dd = U32.to_nat(di)
794  +w = U32.to_nat(si)
795  +ys = List.drop(&2, U32, US(ts), qn)
796  +RHS = List.append(&2, U32, v1, List.take(&2, U32, ys, Nat.add(o, m)))
797  +hdl = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(l1, o), Nat.mul(dd, 4n), Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi),
798    N.lt_le_trans(Nat.add(l1, o), Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d)), N.lt_add_l(l1, o, np, ho), hl))
799  +hD = lt_w0(dd, Nat.pow(2n, d), hdl)
800  +hDl = AB.subst(Nat, y => {Nat.is_lt(dd, y) == True{} : Bool}, Nat.pow(2n, d), List.length(&2, U32, C.WL(td)),
801    Equal.sym(Nat, List.length(&2, U32, C.WL(td)), Nat.pow(2n, d), P.view_length(U32, d, td, hfd)), hD)
802  +eidx = Equal.trans(Nat, Nat.add(Nat.mul(dd, 4n), m), Nat.add(Nat.add(l1, o), m), Nat.add(l1, Nat.add(o, m)),
803    Equal.cong(Nat, Nat, z => Nat.add(z, m), Nat.mul(dd, 4n), Nat.add(l1, o), hdi), N.add_assoc(l1, o, m))
804  +hb = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(qn, o), Nat.add(Nat.mul(w, 4n), r),
805    Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi),
806    AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(qn, Nat.add(o, m)), Nat.add(Nat.add(qn, o), m),
807      Equal.sym(Nat, Nat.add(Nat.add(qn, o), m), Nat.add(qn, Nat.add(o, m)), N.add_assoc(qn, o, m)),
808      N.le_trans(Nat.add(qn, Nat.add(o, m)), Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e)), N.le_add_mono_l(qn, Nat.add(o, m), np, hmv), hq)))
809  +ew = Equal.trans(List<&2, U32>, List.take(&2, U32, C.L4(mw), m), List.take(&2, U32, C.L4(W.merge(lo, hi, r)), m), List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(qn, o)), m),
810    Equal.cong(U32, List<&2, U32>, z => List.take(&2, U32, C.L4(z), m), mw, W.merge(lo, hi, r), mrg(lo, hi, sh, r, hsh, hr)),
811    Equal.trans(List<&2, U32>, List.take(&2, U32, C.L4(W.merge(lo, hi, r)), m), List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(w, 4n), r)), m),
812      List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(qn, o)), m),
813      win(ts, e, si, p, lo, r, m, hfs, hes, hlo, hp, hr, hm, hb),
814      Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, List.drop(&2, U32, US(ts), z), m), Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi)))
815  +ew2 = AB.subst(List<&2, U32>, z => {List.take(&2, U32, C.L4(mw), m) == List.take(&2, U32, z, m) : List<&2, U32>},
816    List.drop(&2, U32, US(ts), Nat.add(qn, o)), List.drop(&2, U32, ys, o),
817    Equal.sym(List<&2, U32>, List.drop(&2, U32, ys, o), List.drop(&2, U32, US(ts), Nat.add(qn, o)), drop_drop(US(ts), qn, o)), ew)
818  %Equal.sym(List<&2, U32>, C.WL(I.set_tree(U32, td, di, mw)), List.set(&2, U32, C.WL(td), dd, mw), C.wl_set(td, d, di, mw, hfd, hdd, hD)) :
819    {List.take(&2, U32, D.unpack(_), Nat.add(l1, Nat.add(o, m))) == RHS : List<&2, U32>}
820  %eidx : {List.take(&2, U32, D.unpack(List.set(&2, U32, C.WL(td), dd, mw)), _) == RHS : List<&2, U32>}
821  %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(List.set(&2, U32, C.WL(td), dd, mw)), Nat.add(Nat.mul(dd, 4n), m)),
822    List.append(&2, U32, List.take(&2, U32, D.unpack(C.WL(td)), Nat.mul(dd, 4n)), List.take(&2, U32, C.L4(mw), m)),
823    us1(C.WL(td), dd, mw, m, hDl, hm)) :
824    {_ == RHS : List<&2, U32>}
825  %Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi) :
826    {List.append(&2, U32, List.take(&2, U32, D.unpack(C.WL(td)), _), List.take(&2, U32, C.L4(mw), m)) == RHS : List<&2, U32>}
827  %Equal.sym(List<&2, U32>, List.take(&2, U32, US(td), Nat.add(l1, o)), List.append(&2, U32, v1, List.take(&2, U32, ys, o)), hinv) :
828    {List.append(&2, U32, _, List.take(&2, U32, C.L4(mw), m)) == RHS : List<&2, U32>}
829  %Equal.sym(List<&2, U32>, List.take(&2, U32, C.L4(mw), m), List.take(&2, U32, List.drop(&2, U32, ys, o), m), ew2) :
830    {List.append(&2, U32, List.append(&2, U32, v1, List.take(&2, U32, ys, o)), _) == RHS : List<&2, U32>}
831  Equal.trans(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, v1, List.take(&2, U32, ys, o)), List.take(&2, U32, List.drop(&2, U32, ys, o), m)),
832    List.append(&2, U32, v1, List.append(&2, U32, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m))), RHS,
833    X.append_assoc(v1, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m)),
834    Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z),
835      List.append(&2, U32, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m)), List.take(&2, U32, ys, Nat.add(o, m)), take_split(ys, o, m)))
836
837# The last word, when fewer than 4 bytes are left.
838law avf:
839  for +k1: Nat
840  for +ts: P.Tree<U32>
841  for +e: Nat
842  for +td: P.Tree<U32>
843  for +d: Nat
844  for +p: U32
845  for +lo: U32
846  for +si: U32
847  for +di: U32
848  for +sh: Nat
849  for +l1: Nat
850  for +qn: Nat
851  for +r: Nat
852  for +o: Nat
853  for +np: Nat
854  for +v1: List<&2, U32>
855  for +hbq: {Nat.is_le(Nat.add(o, 4n), np) == False{} : Bool}
856  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
857  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
858  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
859  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
860  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
861  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
862  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
863  for +hlo: {lo == C.WD(ts, si) : U32}
864  for +hsh: {sh == Nat.mul(8n, r) : Nat}
865  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
866  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
867  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
868  for +hon: {Nat.is_le(o, np) == True{} : Bool}
869  for +hc1: {Nat.is_le(np, Nat.add(o, Nat.mul(1n+k1, 4n))) == True{} : Bool}
870  for +hc2: {Nat.is_lt(Nat.add(o, Nat.mul(1n+k1, 4n)), Nat.add(np, 4n)) == True{} : Bool}
871  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
872  {List.take(&2, U32, US(AWT(1n+k1, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>}
873
874def avf(k1, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv):
875  match k1:
876    case 0n:
877      +hi = C.WD(ts, p)
878      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
879      +ho = N.le_lt_trans(o, Nat.add(o, 0n), np, N.le_add_r(o, 0n), c4(o, 0n, np, hc2))
880      +eo = N.le_sub_add(o, np, N.lt_to_le(o, np, ho))
881      +hm = sub_le_of(np, o, 4n, N.lt_to_le(np, Nat.add(o, 4n), N.not_le_lt(Nat.add(o, 4n), np, hbq)))
882      +hmv = AB.subst(Nat, y => {Nat.is_le(y, np) == True{} : Bool}, np, Nat.add(o, Nat.sub(np, o)), Equal.sym(Nat, Nat.add(o, Nat.sub(np, o)), np, eo), N.le_refl(np))
883      AB.subst(Nat, y => {List.take(&2, U32, US(I.set_tree(U32, td, di, mw)), Nat.add(l1, y)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), y)) : List<&2, U32>},
884        Nat.add(o, Nat.sub(np, o)), np, eo,
885        step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, Nat.sub(np, o), hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, hm, hmv, hinv))
886    case 1n+k2:
887      +X2 = Nat.mul(k2, 4n)
888      +h1 = c4(o, Nat.add(4n, X2), np, hc2)
889      +h2 = N.le_lt_trans(Nat.add(o, 4n), Nat.add(o, Nat.add(4n, X2)), np, N.le_add_mono_l(o, 4n, Nat.add(4n, X2), N.le_add_r(4n, X2)), h1)
890      Empty.absurd({List.take(&2, U32, US(AWT(2n+k2, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>},
891        AB.false_ne_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.add(o, 4n), np), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(o, 4n), np), False{}, hbq),
892          N.lt_to_le(Nat.add(o, 4n), np, h2))))
893
894# The word loop
895# =============
896
897# After the words written so far (o bytes, o <= np), the bytes in use agree
898# with v1 then src from qn; the k words left finish the np bytes.
899law av:
900  for +k: Nat
901  for +b: Bool
902  for +ts: P.Tree<U32>
903  for +e: Nat
904  for +td: P.Tree<U32>
905  for +d: Nat
906  for +p: U32
907  for +lo: U32
908  for +si: U32
909  for +di: U32
910  for +sh: Nat
911  for +l1: Nat
912  for +qn: Nat
913  for +r: Nat
914  for +o: Nat
915  for +np: Nat
916  for +v1: List<&2, U32>
917  for +hbq: {Nat.is_le(Nat.add(o, 4n), np) == b : Bool}
918  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
919  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
920  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
921  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
922  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
923  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
924  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
925  for +hlo: {lo == C.WD(ts, si) : U32}
926  for +hsh: {sh == Nat.mul(8n, r) : Nat}
927  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
928  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
929  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
930  for +hon: {Nat.is_le(o, np) == True{} : Bool}
931  for +hc1: {Nat.is_le(np, Nat.add(o, Nat.mul(k, 4n))) == True{} : Bool}
932  for +hc2: {Nat.is_lt(Nat.add(o, Nat.mul(k, 4n)), Nat.add(np, 4n)) == True{} : Bool}
933  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
934  {List.take(&2, U32, US(AWT(k, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>}
935
936def av(k, b, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv):
937  match k b:
938    case 0n _:
939      +eo = le_antisym(o, np, hon, AB.subst(Nat, y => {Nat.is_le(np, y) == True{} : Bool}, Nat.add(o, 0n), o, N.add_zero(o), hc1))
940      %eo : {List.take(&2, U32, US(td), Nat.add(l1, _)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), _)) : List<&2, U32>}
941      hinv
942    case 1n+k1 True{}:
943      +w = U32.to_nat(si)
944      +dd = U32.to_nat(di)
945      +hi = C.WD(ts, p)
946      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
947      +MD = Nat.mul(4n, Nat.pow(2n, d))
948      +ME = Nat.mul(4n, Nat.pow(2n, e))
949      +X = Nat.mul(k1, 4n)
950      +ho = N.le_lt_trans(o, Nat.add(o, X), np, N.le_add_r(o, X), c4(o, X, np, hc2))
951      +hinv2 = step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, 4n, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, {==}, hbq, hinv)
952      +hdl = AB.subst(Nat, y => {Nat.is_lt(y, MD) == True{} : Bool}, Nat.add(l1, o), Nat.mul(dd, 4n), Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi),
953        N.lt_le_trans(Nat.add(l1, o), Nat.add(l1, np), MD, N.lt_add_l(l1, o, np, ho), hl))
954      +e1 = C.inc_fits(di, d, hdd, N.le_lt_trans(dd, Nat.mul(dd, 4n), MD, le_x4(dd), hdl))
955      +hwl = AB.subst(Nat, y => {Nat.is_lt(y, ME) == True{} : Bool}, Nat.add(qn, o), Nat.add(Nat.mul(w, 4n), r), Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi),
956        N.lt_le_trans(Nat.add(qn, o), Nat.add(qn, np), ME, N.lt_add_l(qn, o, np, ho), hq))
957      +hw4 = N.le_lt_trans(Nat.mul(w, 4n), Nat.add(Nat.mul(w, 4n), r), ME, N.le_add_r(Nat.mul(w, 4n), r), hwl)
958      +e2 = C.inc_fits(si, e, hes, N.le_lt_trans(w, Nat.mul(w, 4n), ME, le_x4(w), hw4))
959      +e3 = C.add_fits(si, 2, e, hes, w2_bound(w, Nat.pow(2n, e), AB.pow_pos(e), lt_w0(w, Nat.pow(2n, e), hw4)))
960      +hdi2 = Equal.trans(Nat, Nat.mul(U32.to_nat((di + 1 : U32)), 4n), Nat.mul(1n+dd, 4n), Nat.add(l1, Nat.add(o, 4n)),
961        Equal.cong(Nat, Nat, z => Nat.mul(z, 4n), U32.to_nat((di + 1 : U32)), 1n+dd, Equal.trans(Nat, U32.to_nat((di + 1 : U32)), Nat.add(dd, 1n), 1n+dd, e1, N.add_one(dd))),
962        Equal.trans(Nat, Nat.add(4n, Nat.mul(dd, 4n)), Nat.add(4n, Nat.add(l1, o)), Nat.add(l1, Nat.add(o, 4n)),
963          Equal.cong(Nat, Nat, z => Nat.add(4n, z), Nat.mul(dd, 4n), Nat.add(l1, o), hdi), four_alg(l1, o)))
964      +hsi2 = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat((si + 1 : U32)), 4n), r), Nat.add(Nat.mul(1n+w, 4n), r), Nat.add(qn, Nat.add(o, 4n)),
965        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 4n), r), U32.to_nat((si + 1 : U32)), 1n+w, Equal.trans(Nat, U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), 1n+w, e2, N.add_one(w))),
966        Equal.trans(Nat, Nat.add(4n, Nat.add(Nat.mul(w, 4n), r)), Nat.add(4n, Nat.add(qn, o)), Nat.add(qn, Nat.add(o, 4n)),
967          Equal.cong(Nat, Nat, z => Nat.add(4n, z), Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi), four_alg(qn, o)))
968      +hp2 = Equal.trans(Nat, U32.to_nat((si + 2 : U32)), Nat.add(w, 2n), Nat.add(U32.to_nat((si + 1 : U32)), 1n), e3,
969        Equal.sym(Nat, Nat.add(U32.to_nat((si + 1 : U32)), 1n), Nat.add(w, 2n),
970          Equal.trans(Nat, Nat.add(U32.to_nat((si + 1 : U32)), 1n), Nat.add(Nat.add(w, 1n), 1n), Nat.add(w, 2n),
971            Equal.cong(Nat, Nat, z => Nat.add(z, 1n), U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), e2), N.add_assoc(w, 1n, 1n))))
972      +hlo2 = Equal.cong(U32, U32, z => C.WD(ts, z), p, (si + 1 : U32),
973        U.to_nat_inj(p, (si + 1 : U32), Equal.trans(Nat, U32.to_nat(p), Nat.add(w, 1n), U32.to_nat((si + 1 : U32)), hp, Equal.sym(Nat, U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), e2))))
974      +ea = Equal.sym(Nat, Nat.add(Nat.add(o, 4n), X), Nat.add(o, Nat.add(4n, X)), N.add_assoc(o, 4n, X))
975      +hc12 = AB.subst(Nat, y => {Nat.is_le(np, y) == True{} : Bool}, Nat.add(o, Nat.add(4n, X)), Nat.add(Nat.add(o, 4n), X), ea, hc1)
976      +hc22 = AB.subst(Nat, y => {Nat.is_lt(y, Nat.add(np, 4n)) == True{} : Bool}, Nat.add(o, Nat.add(4n, X)), Nat.add(Nat.add(o, 4n), X), ea, hc2)
977      av(k1, Nat.is_le(Nat.add(Nat.add(o, 4n), 4n), np), ts, e, I.set_tree(U32, td, di, mw), d, (si + 2 : U32), hi, (si + 1 : U32), (di + 1 : U32), sh, l1, qn, r, Nat.add(o, 4n), np, v1,
978        {==}, hfs, hes, C.full_set(td, d, di, mw, hfd), hdd, hdi2, hsi2, hp2, hlo2, hsh, hr, hq, hl, hbq, hc12, hc22, hinv2)
979    case 1n+k1 False{}:
980      avf(k1, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv)
981
982# Facts for the top level
983# =======================
984
985# The length after the reference append's pushes.
986law ag_size:
987  for +n: Nat
988  for +ld: U32
989  for +td: P.Tree<U32>
990  for +ls: U32
991  for +ts: P.Tree<U32>
992  for +d: Nat
993  for +s: U32
994  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
995  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
996  {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s))) == Nat.add(U32.to_nat(ld), n) : Nat}
997
998def ag_size(n, ld, td, ls, ts, d, s, hd, hc):
999  match n:
1000    case 0n:
1001      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), C.AT(ls, ts, s)), C.at_pair_t(ls, ts, s)) :
1002        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s))) == Nat.add(U32.to_nat(ld), 0n) : Nat}
1003      Equal.sym(Nat, Nat.add(U32.to_nat(ld), 0n), U32.to_nat(ld), N.add_zero(U32.to_nat(ld)))
1004    case 1n+k:
1005      +x = C.AT(ls, ts, s)
1006      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
1007        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s))) == Nat.add(U32.to_nat(ld), 1n+k) : Nat}
1008      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), X.PT(ld, td, x)), O.push_eq_t(ld, td, x)) :
1009        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32)))) == Nat.add(U32.to_nat(ld), 1n+k) : Nat}
1010      Equal.trans(Nat, D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, C.BT((ld + 1 : U32), X.PT(ld, td, x)), B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32)))),
1011        Nat.add(U32.to_nat((ld + 1 : U32)), k), Nat.add(U32.to_nat(ld), 1n+k),
1012        ag_size(k, (ld + 1 : U32), X.PT(ld, td, x), ls, ts, d, (s + 1 : U32), X.step_ok(ld, td, d, x, k, hd, hc), X.step_cap(ld, td, d, x, k, hd, hc)),
1013        Equal.trans(Nat, Nat.add(U32.to_nat((ld + 1 : U32)), k), Nat.add(Nat.add(U32.to_nat(ld), 1n), k), Nat.add(U32.to_nat(ld), 1n+k),
1014          Equal.cong(Nat, Nat, z => Nat.add(z, k), U32.to_nat((ld + 1 : U32)), Nat.add(U32.to_nat(ld), 1n),
1015            C.inc_fits(ld, d, C.ok_d(ld, td, d, hd), X.step_room(ld, td, d, k, hd, hc))),
1016          N.add_assoc(U32.to_nat(ld), 1n, k)))
1017
1018law aw_full:
1019  for +n: Nat
1020  for +ts: P.Tree<U32>
1021  for +p: U32
1022  for +lo: U32
1023  for +td: P.Tree<U32>
1024  for +si: U32
1025  for +di: U32
1026  for +sh: Nat
1027  for +d: Nat
1028  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
1029  {A.full(U32, P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), d) == True{} : Bool}
1030
1031def aw_full(n, ts, p, lo, td, si, di, sh, d, hfd):
1032  match n:
1033    case 0n:
1034      hfd
1035    case 1n+k:
1036      +mw = U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh)))
1037      aw_full(k, ts, (si + 2 : U32), C.WD(ts, p), I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh, d, C.full_set(td, d, di, mw, hfd))
1038
1039law mul4div:
1040  for +z: Nat
1041  for +y: Nat
1042  for +e: {z == Nat.mul(y, 4n) : Nat}
1043  {Nat.mul(Nat.div(z, 4n), 4n) == z : Nat}
1044
1045def mul4div(z, y, e):
1046  %Equal.sym(Nat, z, Nat.mul(y, 4n), e) : {Nat.mul(Nat.div(_, 4n), 4n) == _ : Nat}
1047  Equal.cong(Nat, Nat, w => Nat.mul(w, 4n), Nat.div(Nat.mul(y, 4n), 4n), y,
1048    AB.subst(Nat, w => {Nat.div(w, 4n) == y : Nat}, Nat.add(Nat.mul(y, 4n), 0n), Nat.mul(y, 4n), N.add_zero(Nat.mul(y, 4n)), N.div_mul_add(y, 4n, 0n, {==})))
1049
1050# x = 4a + k with k + h = 4 gives x + h = 4(a + 1).
1051law al_k:
1052  for +x: Nat
1053  for +a: Nat
1054  for +k: Nat
1055  for +h: Nat
1056  for +ex: {x == Nat.add(Nat.mul(a, 4n), k) : Nat}
1057  for +ek: {Nat.add(k, h) == 4n : Nat}
1058  {Nat.add(x, h) == Nat.mul(1n+a, 4n) : Nat}
1059
1060def al_k(x, a, k, h, ex, ek):
1061  %Equal.sym(Nat, x, Nat.add(Nat.mul(a, 4n), k), ex) : {Nat.add(_, h) == Nat.mul(1n+a, 4n) : Nat}
1062  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(a, 4n), k), h), Nat.add(Nat.mul(a, 4n), Nat.add(k, h)), N.add_assoc(Nat.mul(a, 4n), k, h)) : {_ == Nat.mul(1n+a, 4n) : Nat}
1063  %Equal.sym(Nat, Nat.add(k, h), 4n, ek) : {Nat.add(Nat.mul(a, 4n), _) == Nat.mul(1n+a, 4n) : Nat}
1064  N.add_comm(Nat.mul(a, 4n), 4n)
1065
1066def H0(+ld: U32) -> U32:
1067  U32.and(U32.sub(4, U32.and(ld, 3)), 3)
1068
1069law exk:
1070  for +ld: U32
1071  for +k: Nat
1072  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1073  {U32.to_nat(ld) == Nat.add(Nat.mul(Nat.div(U32.to_nat(ld), 4n), 4n), k) : Nat}
1074
1075def exk(ld, k, ek):
1076  +x = U32.to_nat(ld)
1077  +a = Nat.div(x, 4n)
1078  +ex0 = Equal.sym(Nat, Nat.add(Nat.mul(a, 4n), U32.to_nat((ld .&. 3 : U32))), x,
1079    AB.subst(Nat, z => {Nat.add(Nat.mul(a, 4n), z) == x : Nat}, Nat.mod(x, 4n), U32.to_nat((ld .&. 3 : U32)),
1080      Equal.sym(Nat, U32.to_nat((ld .&. 3 : U32)), Nat.mod(x, 4n), U.to_nat_and_mask(ld, 3, 2n, {==})), N.div_mod(x, 4n)))
1081  AB.subst(Nat, z => {x == Nat.add(Nat.mul(a, 4n), z) : Nat}, U32.to_nat((ld .&. 3 : U32)), k, ek, ex0)
1082
1083law align2:
1084  for +ld: U32
1085  for +k: Nat
1086  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1087  for +hk: {Nat.is_lt(k, 4n) == True{} : Bool}
1088  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}
1089
1090def align2(ld, k, ek, hk):
1091  match k:
1092    case 0n:
1093      +x = U32.to_nat(ld)
1094      +a = Nat.div(x, 4n)
1095      +ex = exk(ld, 0n, ek)
1096      +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 0, U.to_nat_inj((ld .&. 3 : U32), 0, ek))
1097      mul4div(Nat.add(x, U32.to_nat(H0(ld))), a,
1098        Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 0n), Nat.mul(a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 0n, eh),
1099          Equal.trans(Nat, Nat.add(x, 0n), x, Nat.mul(a, 4n), N.add_zero(x),
1100            Equal.trans(Nat, x, Nat.add(Nat.mul(a, 4n), 0n), Nat.mul(a, 4n), ex, N.add_zero(Nat.mul(a, 4n))))))
1101    case 1n+k1:
1102      match k1:
1103        case 0n:
1104          +x = U32.to_nat(ld)
1105          +a = Nat.div(x, 4n)
1106          +ex = exk(ld, 1n, ek)
1107          +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 1, U.to_nat_inj((ld .&. 3 : U32), 1, ek))
1108          mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1109            Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 3n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 3n, eh),
1110              al_k(x, a, 1n, 3n, ex, {==})))
1111        case 1n+k2:
1112          match k2:
1113            case 0n:
1114              +x = U32.to_nat(ld)
1115              +a = Nat.div(x, 4n)
1116              +ex = exk(ld, 2n, ek)
1117              +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 2, U.to_nat_inj((ld .&. 3 : U32), 2, ek))
1118              mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1119                Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 2n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 2n, eh),
1120                  al_k(x, a, 2n, 2n, ex, {==})))
1121            case 1n+k3:
1122              match k3:
1123                case 0n:
1124                  +x = U32.to_nat(ld)
1125                  +a = Nat.div(x, 4n)
1126                  +ex = exk(ld, 3n, ek)
1127                  +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 3, U.to_nat_inj((ld .&. 3 : U32), 3, ek))
1128                  mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1129                    Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 1n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 1n, eh),
1130                      al_k(x, a, 3n, 1n, ex, {==})))
1131                case 1n+k4:
1132                  Empty.absurd({Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}, AB.lt_zero_absurd(k4, hk))
1133
1134# dst's length after the first h0 bytes is a multiple of 4.
1135law align:
1136  for +ld: U32
1137  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}
1138
1139def align(ld):
1140  align2(ld, U32.to_nat((ld .&. 3 : U32)), {==}, and3_lt(ld))
1141
1142# x + y < 2^e for x <= 4 * 2^d and y <= 3, when d + 2 < e (e a variable:
1143# the callers put 32n only in the final type).
1144law x3_lt_e:
1145  for +x: Nat
1146  for +y: Nat
1147  for +d: Nat
1148  for +e: Nat
1149  for +hy: {Nat.is_le(y, 3n) == True{} : Bool}
1150  for +hx: {Nat.is_le(x, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
1151  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
1152  {Nat.is_lt(Nat.add(x, y), Nat.pow(2n, e)) == True{} : Bool}
1153
1154def x3_lt_e(x, y, d, e, hy, hx, he):
1155  +pp = Nat.pow(2n, d)
1156  +q = Nat.pow(2n, Nat.add(2n, d))
1157  +eq = N.mul_assoc(2n, 2n, pp)
1158  +hxq = AB.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.mul(Nat.mul(2n, 2n), pp), Nat.mul(2n, Nat.mul(2n, pp)), eq, hx)
1159  +h1 = N.le_trans(Nat.add(x, y), Nat.add(q, y), Nat.add(q, 3n), N.le_add_mono_r(y, x, q, hxq), N.le_add_mono_l(q, y, 3n, hy))
1160  +h41 = N.le_mul_l(4n, 1n, pp, Equal.trans(Bool, Nat.is_le(1n, pp), Nat.is_lt(0n, pp), True{}, N.le_succ_lt(0n, pp), AB.pow_pos(d)))
1161  +h4q = AB.subst(Nat, z => {Nat.is_le(4n, z) == True{} : Bool}, Nat.mul(Nat.mul(2n, 2n), pp), Nat.mul(2n, Nat.mul(2n, pp)), eq, h41)
1162  +h4 = Equal.trans(Bool, Nat.is_lt(3n, q), Nat.is_le(4n, q), True{}, Equal.sym(Bool, Nat.is_le(4n, q), Nat.is_lt(3n, q), N.le_succ_lt(3n, q)), h4q)
1163  +h2 = AB.subst(Nat, z => {Nat.is_lt(Nat.add(q, 3n), z) == True{} : Bool}, Nat.add(q, q), Nat.add(q, Nat.add(q, 0n)),
1164    Equal.cong(Nat, Nat, z => Nat.add(q, z), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), N.lt_add_l(q, 3n, q, h4))
1165  +h3 = N.pow_le(Nat.add(3n, d), e, Equal.trans(Bool, Nat.is_le(Nat.add(3n, d), e), Nat.is_lt(Nat.add(2n, d), e), True{}, N.le_succ_lt(Nat.add(2n, d), e), he))
1166  N.le_lt_trans(Nat.add(x, y), Nat.add(q, 3n), Nat.pow(2n, e), h1, N.lt_le_trans(Nat.add(q, 3n), Nat.pow(2n, Nat.add(3n, d)), Nat.pow(2n, e), h2, h3))
1167
1168# The word count (np + 3) >> 2 covers np bytes with less than one word left.
1169law cnt1:
1170  for +np: Nat
1171  {Nat.is_le(np, Nat.mul(Nat.div(Nat.add(np, 3n), 4n), 4n)) == True{} : Bool}
1172
1173def cnt1(np):
1174  +xx = Nat.add(np, 3n)
1175  +q = Nat.div(xx, 4n)
1176  +rm = Nat.mod(xx, 4n)
1177  +h1 = AB.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.mul(q, 4n), 3n)) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), rm), xx, N.div_mod(xx, 4n),
1178    N.le_add_mono_l(Nat.mul(q, 4n), rm, 3n, Equal.trans(Bool, Nat.is_le(rm, 3n), Nat.is_lt(rm, 4n), True{}, Equal.sym(Bool, Nat.is_lt(rm, 4n), Nat.is_le(rm, 3n), N.lt_succ_iff(rm, 3n)), N.mod_lt(xx, 4n, {==}))))
1179  +h2 = AB.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.mul(q, 4n), 3n)) == True{} : Bool}, xx, Nat.add(3n, np), N.add_comm(np, 3n), h1)
1180  AB.subst(Nat, z => {Nat.is_le(Nat.add(3n, np), z) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), 3n), Nat.add(3n, Nat.mul(q, 4n)), N.add_comm(Nat.mul(q, 4n), 3n), h2)
1181
1182law cnt2:
1183  for +np: Nat
1184  {Nat.is_lt(Nat.mul(Nat.div(Nat.add(np, 3n), 4n), 4n), Nat.add(np, 4n)) == True{} : Bool}
1185
1186def cnt2(np):
1187  +xx = Nat.add(np, 3n)
1188  +q = Nat.div(xx, 4n)
1189  +rm = Nat.mod(xx, 4n)
1190  N.le_lt_trans(Nat.mul(q, 4n), xx, Nat.add(np, 4n),
1191    AB.subst(Nat, z => {Nat.is_le(Nat.mul(q, 4n), z) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), rm), xx, N.div_mod(xx, 4n), N.le_add_r(Nat.mul(q, 4n), rm)),
1192    N.lt_add_l(np, 3n, 4n, {==}))
1193
1194# The fast append on mirrors
1195# ==========================
1196
1197# The bytes done one at a time, the bytes left, and where they start.
1198def HH(+ld: U32, +n: U32) -> U32:
1199  U32.min(H0(ld), n)
1200
1201def NPw(+ld: U32, +n: U32) -> U32:
1202  U32.sub(n, HH(ld, n))
1203
1204def QQ(+ld: U32, +s: U32, +n: U32) -> U32:
1205  U32.add(s, HH(ld, n))
1206
1207def NW(+ld: U32, +n: U32) -> Nat:
1208  U32.to_nat(U32.shrn(U32.add(NPw(ld, n), 3), 2n))
1209
1210def SH(+q: U32) -> Nat:
1211  U32.to_nat(U32.shln(U32.and(q, 3), 3n))
1212
1213def TF(+ld: U32, +ts: P.Tree<U32>, +s: U32, +n: U32, +l1: U32, +t1: P.Tree<U32>) -> P.Tree<U32>:
1214  AWT(NW(ld, n), ts, U32.add(U32.shrn(QQ(ld, s, n), 2n), 1), C.WD(ts, U32.shrn(QQ(ld, s, n), 2n)), t1, U32.shrn(QQ(ld, s, n), 2n), U32.shrn(l1, 2n), SH(QQ(ld, s, n)))
1215
1216# With BT(l1, t1) the result of the first bytes, fast append is these mirrors.
1217law fa_eq:
1218  for +ld: U32
1219  for +td: P.Tree<U32>
1220  for +ls: U32
1221  for +ts: P.Tree<U32>
1222  for +s: U32
1223  for +n: U32
1224  for +l1: U32
1225  for +t1: P.Tree<U32>
1226  for +e1: {C.BT(l1, t1) == Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, HH(ld, n))) : D.Bytes}
1227  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1228
1229def fa_eq(ld, td, ls, ts, s, n, l1, t1, e1):
1230  +h = HH(ld, n)
1231  +q = QQ(ld, s, n)
1232  +qw = U32.shrn(q, 2n)
1233  %Equal.sym(D.Bytes & D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, h), (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, h)), C.BT(ls, ts)),
1234    X.append_pair_t(ld, td, ls, ts, s, h)) :
1235    {FA.append.k(NPw(ld, n), q, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1236  %e1 : {FA.append.k(NPw(ld, n), q, (_, C.BT(ls, ts))) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1237  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), qw), (P.fromT(U32, ts), C.WD(ts, qw)), P.get_pair_t(U32, ts, qw)) :
1238    {FA.append.w(l1, NPw(ld, n), q, P.fromT(U32, t1), ls, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1239  %Equal.sym(Array<U32> & Array<U32>,
1240    FA.append.words(NW(ld, n), Array.get(U32, P.fromT(U32, ts), U32.add(qw, 1)), C.WD(ts, qw), P.fromT(U32, t1), qw, U32.shrn(l1, 2n), SH(q)),
1241    (P.fromT(U32, TF(ld, ts, s, n, l1, t1)), P.fromT(U32, ts)),
1242    aw_eq(NW(ld, n), ts, U32.add(qw, 1), C.WD(ts, qw), t1, qw, U32.shrn(l1, 2n), SH(q))) :
1243    {FA.append.fin(U32.add(l1, NPw(ld, n)), ls, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1244  {==}
1245
1246# The last list step: the bytes of the prefix and of the words make the slice.
1247law fin_eq:
1248  for +v1: List<&2, U32>
1249  for +vd: List<&2, U32>
1250  for +us: List<&2, U32>
1251  for +ls: Nat
1252  for +s: Nat
1253  for +hh: Nat
1254  for +qn: Nat
1255  for +np: Nat
1256  for +nn: Nat
1257  for +hv: {v1 == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, hh)) : List<&2, U32>}
1258  for +hq: {qn == Nat.add(s, hh) : Nat}
1259  for +hnp: {np == Nat.sub(nn, hh) : Nat}
1260  for +hhn: {Nat.is_le(hh, nn) == True{} : Bool}
1261  for +hb: {Nat.is_le(Nat.add(s, nn), ls) == True{} : Bool}
1262  {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, qn), np)) == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, nn)) : List<&2, U32>}
1263
1264def fin_eq(v1, vd, us, ls, s, hh, qn, np, nn, hv, hq, hnp, hhn, hb):
1265  +xs = List.take(&2, U32, us, ls)
1266  +rest = Nat.sub(nn, hh)
1267  +RHS = List.append(&2, U32, vd, D.slice(xs, s, nn))
1268  +esum = Equal.trans(Nat, Nat.add(Nat.add(s, hh), rest), Nat.add(s, Nat.add(hh, rest)), Nat.add(s, nn), N.add_assoc(s, hh, rest),
1269    Equal.cong(Nat, Nat, z => Nat.add(s, z), Nat.add(hh, rest), nn, N.le_sub_add(hh, nn, hhn)))
1270  %Equal.sym(Nat, np, rest, hnp) : {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, qn), _)) == RHS : List<&2, U32>}
1271  %Equal.sym(Nat, qn, Nat.add(s, hh), hq) : {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, _), rest)) == RHS : List<&2, U32>}
1272  %Equal.sym(List<&2, U32>, v1, List.append(&2, U32, vd, D.slice(xs, s, hh)), hv) :
1273    {List.append(&2, U32, _, List.take(&2, U32, List.drop(&2, U32, us, Nat.add(s, hh)), rest)) == RHS : List<&2, U32>}
1274  %slice_take(us, ls, Nat.add(s, hh), rest,
1275    AB.subst(Nat, z => {Nat.is_le(z, ls) == True{} : Bool}, Nat.add(s, nn), Nat.add(Nat.add(s, hh), rest), Equal.sym(Nat, Nat.add(Nat.add(s, hh), rest), Nat.add(s, nn), esum), hb)) :
1276    {List.append(&2, U32, List.append(&2, U32, vd, D.slice(xs, s, hh)), _) == RHS : List<&2, U32>}
1277  Equal.trans(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, vd, D.slice(xs, s, hh)), D.slice(xs, Nat.add(s, hh), rest)),
1278    List.append(&2, U32, vd, List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest))), RHS,
1279    X.append_assoc(vd, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)),
1280    Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, vd, z),
1281      List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)), D.slice(xs, s, nn),
1282      Equal.trans(List<&2, U32>, List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)), D.slice(xs, s, Nat.add(hh, rest)), D.slice(xs, s, nn),
1283        slice_split(xs, s, hh, rest), Equal.cong(Nat, List<&2, U32>, z => D.slice(xs, s, z), Nat.add(hh, rest), nn, N.le_sub_add(hh, nn, hhn)))))
1284
1285# Facts shared by the three laws
1286# ==============================
1287
1288def D1(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +s: U32, +n: U32) -> D.Bytes:
1289  Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, HH(ld, n)))
1290
1291law hh_le:
1292  for +ld: U32
1293  for +n: U32
1294  {Nat.is_le(U32.to_nat(HH(ld, n)), U32.to_nat(n)) == True{} : Bool}
1295
1296def hh_le(ld, n):
1297  AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(n)) == True{} : Bool}, Nat.min(U32.to_nat(H0(ld)), U32.to_nat(n)), U32.to_nat(HH(ld, n)),
1298    Equal.sym(Nat, U32.to_nat(HH(ld, n)), Nat.min(U32.to_nat(H0(ld)), U32.to_nat(n)), U.to_nat_min(H0(ld), n)),
1299    min_le(U32.to_nat(H0(ld)), U32.to_nat(n)))
1300
1301law hc_h:
1302  for +ld: U32
1303  for +td: P.Tree<U32>
1304  for +n: U32
1305  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1306  {Nat.is_le(Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))), D.cap(C.BT(ld, td))) == True{} : Bool}
1307
1308def hc_h(ld, td, n, hc):
1309  N.le_trans(Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))), Nat.add(U32.to_nat(ld), U32.to_nat(n)), D.cap(C.BT(ld, td)),
1310    N.le_add_mono_l(U32.to_nat(ld), U32.to_nat(HH(ld, n)), U32.to_nat(n), hh_le(ld, n)), hc)
1311
1312law ok1:
1313  for +ld: U32
1314  for +td: P.Tree<U32>
1315  for +ls: U32
1316  for +ts: P.Tree<U32>
1317  for +d: Nat
1318  for +s: U32
1319  for +n: U32
1320  for +l1: U32
1321  for +t1: P.Tree<U32>
1322  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1323  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1324  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1325  {D.ok(C.BT(l1, t1), d) == True{} : Bool}
1326
1327def ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc):
1328  AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1329    X.append_ok_t(ld, td, ls, ts, d, s, HH(ld, n), hd, hc_h(ld, td, n, hc)))
1330
1331law el1:
1332  for +ld: U32
1333  for +td: P.Tree<U32>
1334  for +ls: U32
1335  for +ts: P.Tree<U32>
1336  for +d: Nat
1337  for +s: U32
1338  for +n: U32
1339  for +l1: U32
1340  for +t1: P.Tree<U32>
1341  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1342  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1343  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1344  {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1345
1346def el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc):
1347  Equal.trans(Nat, U32.to_nat(l1), D.size(D1(ld, td, ls, ts, s, n)), Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))),
1348    Equal.cong(D.Bytes, Nat, b => D.size(b), C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1349    ag_size(U32.to_nat(HH(ld, n)), ld, td, ls, ts, d, s, hd, hc_h(ld, td, n, hc)))
1350
1351law enp:
1352  for +ld: U32
1353  for +n: U32
1354  {U32.to_nat(NPw(ld, n)) == Nat.sub(U32.to_nat(n), U32.to_nat(HH(ld, n))) : Nat}
1355
1356def enp(ld, n):
1357  U.to_nat_sub_le(n, HH(ld, n), Equal.trans(Bool, U32.is_le(HH(ld, n), n), Nat.is_le(U32.to_nat(HH(ld, n)), U32.to_nat(n)), True{}, U.is_le_to_nat(HH(ld, n), n), hh_le(ld, n)))
1358
1359# l1 + (n - h) = ld + n.
1360law esum:
1361  for +ld: U32
1362  for +l1: U32
1363  for +n: U32
1364  for +el: {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1365  {Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))) == Nat.add(U32.to_nat(ld), U32.to_nat(n)) : Nat}
1366
1367def esum(ld, l1, n, el):
1368  +a = U32.to_nat(ld)
1369  +h = U32.to_nat(HH(ld, n))
1370  +nn = U32.to_nat(n)
1371  %Equal.sym(Nat, U32.to_nat(l1), Nat.add(a, h), el) : {Nat.add(_, U32.to_nat(NPw(ld, n))) == Nat.add(a, nn) : Nat}
1372  %Equal.sym(Nat, U32.to_nat(NPw(ld, n)), Nat.sub(nn, h), enp(ld, n)) : {Nat.add(Nat.add(a, h), _) == Nat.add(a, nn) : Nat}
1373  Equal.trans(Nat, Nat.add(Nat.add(a, h), Nat.sub(nn, h)), Nat.add(a, Nat.add(h, Nat.sub(nn, h))), Nat.add(a, nn), N.add_assoc(a, h, Nat.sub(nn, h)),
1374    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(h, Nat.sub(nn, h)), nn, N.le_sub_add(h, nn, hh_le(ld, n))))
1375
1376law hlen0:
1377  for +ld: U32
1378  for +td: P.Tree<U32>
1379  for +l1: U32
1380  for +d: Nat
1381  for +n: U32
1382  for +el: {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1383  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1384  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1385  {Nat.is_le(Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
1386
1387def hlen0(ld, td, l1, d, n, el, hd, hc):
1388  AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(ld), U32.to_nat(n)), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))),
1389    Equal.sym(Nat, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), Nat.add(U32.to_nat(ld), U32.to_nat(n)), esum(ld, l1, n, el)),
1390    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), U32.to_nat(n)), y) == True{} : Bool}, D.cap(C.BT(ld, td)), Nat.mul(4n, Nat.pow(2n, d)), O.cap_ok_t(ld, td, d, hd), hc))
1391
1392# The pair law
1393# ============
1394
1395def fap.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +s: U32, +n: U32, m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1396  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}:
1397  (+l1, m2) = m
1398  (+t1, +e1) = m2
1399  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1400    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1401    {_ == (Pair.fst(D.Bytes, D.Bytes, _), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1402  {==}
1403
1404law fast_append_pair_t:
1405  for +ld: U32
1406  for +td: P.Tree<U32>
1407  for +ls: U32
1408  for +ts: P.Tree<U32>
1409  for +s: U32
1410  for +n: U32
1411  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1412
1413def fast_append_pair_t(ld, td, ls, ts, s, n):
1414  fap.go(ld, td, ls, ts, s, n, C.bmirror(D1(ld, td, ls, ts, s, n)))
1415
1416# The ok law
1417# ==========
1418
1419def fao.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +s: U32, +n: U32,
1420  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1421  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1422  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1423  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}:
1424  (+l1, m2) = m
1425  (+t1, +e1) = m2
1426  +q = QQ(ld, s, n)
1427  +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1428  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1429  +hdd = C.ok_d(ld, td, d, hd)
1430  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1431  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1432    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1433    {D.ok(Pair.fst(D.Bytes, D.Bytes, _), d) == True{} : Bool}
1434  C.ok_mk(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1), d,
1435    aw_full(NW(ld, n), ts, U32.add(U32.shrn(q, 2n), 1), C.WD(ts, U32.shrn(q, 2n)), t1, U32.shrn(q, 2n), U32.shrn(l1, 2n), SH(q), d, C.ok_full(l1, t1, d, hk1)),
1436    hdd,
1437    AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), U32.to_nat(U32.add(l1, NPw(ld, n))),
1438      Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), C.add_fits(l1, NPw(ld, n), d, hdd, hl0)), hl0))
1439
1440law fast_append_ok_t:
1441  for +ld: U32
1442  for +td: P.Tree<U32>
1443  for +ls: U32
1444  for +ts: P.Tree<U32>
1445  for +d: Nat
1446  for +s: U32
1447  for +n: U32
1448  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1449  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1450  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}
1451
1452def fast_append_ok_t(ld, td, ls, ts, d, s, n, hd, hc):
1453  fao.go(ld, td, ls, ts, d, s, n, hd, hc, C.bmirror(D1(ld, td, ls, ts, s, n)))
1454
1455# The view law
1456# ============
1457
1458law esum_n:
1459  for +a: Nat
1460  for +h: Nat
1461  for +nn: Nat
1462  for +hle: {Nat.is_le(h, nn) == True{} : Bool}
1463  {Nat.add(Nat.add(a, h), Nat.sub(nn, h)) == Nat.add(a, nn) : Nat}
1464
1465def esum_n(a, h, nn, hle):
1466  Equal.trans(Nat, Nat.add(Nat.add(a, h), Nat.sub(nn, h)), Nat.add(a, Nat.add(h, Nat.sub(nn, h))), Nat.add(a, nn), N.add_assoc(a, h, Nat.sub(nn, h)),
1467    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(h, Nat.sub(nn, h)), nn, N.le_sub_add(h, nn, hle)))
1468
1469# What the word loop leaves: the bytes in use after the prefix, then src from q.
1470law avc:
1471  for +b0: Bool
1472  for +ld: U32
1473  for +td: P.Tree<U32>
1474  for +ls: U32
1475  for +ts: P.Tree<U32>
1476  for +d: Nat
1477  for +e: Nat
1478  for +s: U32
1479  for +n: U32
1480  for +l1: U32
1481  for +t1: P.Tree<U32>
1482  for +hb0: {Nat.is_lt(U32.to_nat(H0(ld)), U32.to_nat(n)) == b0 : Bool}
1483  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1484  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1485  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
1486  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
1487  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1488  {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n)))) == List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), U32.to_nat(NPw(ld, n)))) : List<&2, U32>}
1489
1490def avc(b0, ld, td, ls, ts, d, e, s, n, l1, t1, hb0, e1, hd, he, hs, hc):
1491  match b0:
1492    case True{}:
1493      +q = QQ(ld, s, n)
1494      +qw = U32.shrn(q, 2n)
1495      +L1 = U32.to_nat(l1)
1496      +NP = U32.to_nat(NPw(ld, n))
1497      +qn = U32.to_nat(q)
1498      +sn = U32.to_nat(s)
1499      +nn = U32.to_nat(n)
1500      +hhn = U32.to_nat(HH(ld, n))
1501      +h0n = U32.to_nat(H0(ld))
1502      +r0 = U32.to_nat((q .&. 3 : U32))
1503      +ME = Nat.mul(4n, Nat.pow(2n, e))
1504      +MD = Nat.mul(4n, Nat.pow(2n, d))
1505      +v1 = D.view(C.BT(l1, t1))
1506      +hfs = C.ok_full(ls, ts, e, he)
1507      +hes = C.ok_d(ls, ts, e, he)
1508      +hdd = C.ok_d(ld, td, d, hd)
1509      +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1510      +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1511      +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1512      +hsl = N.le_trans(Nat.add(sn, nn), U32.to_nat(ls), ME, hs, C.ok_len(ls, ts, e, he))
1513      +ehh = Equal.trans(Nat, hhn, Nat.min(h0n, nn), h0n, U.to_nat_min(H0(ld), n), min_l(h0n, nn, hb0))
1514      +eL = Equal.trans(Nat, L1, Nat.add(U32.to_nat(ld), hhn), Nat.add(U32.to_nat(ld), h0n), el, Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(ld), z), hhn, h0n, ehh))
1515      +hdi0 = Equal.trans(Nat, Nat.mul(U32.to_nat(U32.shrn(l1, 2n)), 4n), Nat.mul(Nat.div(L1, 4n), 4n), Nat.add(L1, 0n),
1516        Equal.cong(Nat, Nat, z => Nat.mul(z, 4n), U32.to_nat(U32.shrn(l1, 2n)), Nat.div(L1, 4n), U.to_nat_shrn(l1, 2n)),
1517        Equal.trans(Nat, Nat.mul(Nat.div(L1, 4n), 4n), Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), h0n), 4n), 4n), Nat.add(L1, 0n),
1518          Equal.cong(Nat, Nat, z => Nat.mul(Nat.div(z, 4n), 4n), L1, Nat.add(U32.to_nat(ld), h0n), eL),
1519          Equal.trans(Nat, Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), h0n), 4n), 4n), Nat.add(U32.to_nat(ld), h0n), Nat.add(L1, 0n), align(ld),
1520            Equal.trans(Nat, Nat.add(U32.to_nat(ld), h0n), L1, Nat.add(L1, 0n), Equal.sym(Nat, L1, Nat.add(U32.to_nat(ld), h0n), eL),
1521              Equal.sym(Nat, Nat.add(L1, 0n), L1, N.add_zero(L1))))))
1522      +hsi0 = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(qw), 4n), r0), Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), Nat.add(qn, 0n),
1523        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 4n), r0), U32.to_nat(qw), Nat.div(qn, 4n), U.to_nat_shrn(q, 2n)),
1524        Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), qn, Nat.add(qn, 0n), Equal.sym(Nat, qn, Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), exk(q, r0, {==})),
1525          Equal.sym(Nat, Nat.add(qn, 0n), qn, N.add_zero(qn))))
1526      +hbq = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), ME, N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hsl)
1527      +eq = C.add_fits(s, HH(ld, n), e, hes, hbq)
1528      +hhl = AB.subst(Nat, z => {Nat.is_lt(z, nn) == True{} : Bool}, h0n, hhn, Equal.sym(Nat, hhn, h0n, ehh), hb0)
1529      +hq4 = AB.subst(Nat, z => {Nat.is_lt(z, ME) == True{} : Bool}, Nat.add(sn, hhn), qn, Equal.sym(Nat, qn, Nat.add(sn, hhn), eq),
1530        N.lt_le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), ME, N.lt_add_l(sn, hhn, nn, hhl), hsl))
1531      +hdq = AB.subst(Nat, z => {Nat.is_lt(z, Nat.pow(2n, e)) == True{} : Bool}, Nat.div(qn, 4n), U32.to_nat(qw), Equal.sym(Nat, U32.to_nat(qw), Nat.div(qn, 4n), U.to_nat_shrn(q, 2n)),
1532        N.div_lt(qn, 4n, Nat.pow(2n, e), {==}, hq4))
1533      +hp0 = C.inc_fits(qw, e, hes, N.lt_le_trans(U32.to_nat(qw), Nat.pow(2n, e), ME, hdq, N.le_add_r(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), 0n))))))
1534      +eqs = Equal.trans(Nat, Nat.add(qn, NP), Nat.add(Nat.add(sn, hhn), NP), Nat.add(sn, nn), Equal.cong(Nat, Nat, z => Nat.add(z, NP), qn, Nat.add(sn, hhn), eq),
1535        Equal.trans(Nat, Nat.add(Nat.add(sn, hhn), NP), Nat.add(Nat.add(sn, hhn), Nat.sub(nn, hhn)), Nat.add(sn, nn), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sn, hhn), z), NP, Nat.sub(nn, hhn), enp(ld, n)),
1536          esum_n(sn, hhn, nn, hh_le(ld, n))))
1537      +hq0 = AB.subst(Nat, z => {Nat.is_le(z, ME) == True{} : Bool}, Nat.add(sn, nn), Nat.add(qn, NP), Equal.sym(Nat, Nat.add(qn, NP), Nat.add(sn, nn), eqs), hsl)
1538      +hnp = N.le_trans(NP, Nat.add(L1, NP), MD, N.le_add_l(NP, L1), hl0)
1539      +efit = U.to_nat_add_fits_p(NPw(ld, n), 3, x3_lt_e(NP, U32.to_nat(3), d, 32n, {==}, hnp, C.he32(d, hdd)))
1540      +enw = Equal.trans(Nat, NW(ld, n), Nat.div(U32.to_nat(U32.add(NPw(ld, n), 3)), 4n), Nat.div(Nat.add(NP, 3n), 4n), U.to_nat_shrn(U32.add(NPw(ld, n), 3), 2n),
1541        Equal.cong(Nat, Nat, z => Nat.div(z, 4n), U32.to_nat(U32.add(NPw(ld, n), 3)), Nat.add(NP, 3n), efit))
1542      +hc10 = AB.subst(Nat, z => {Nat.is_le(NP, Nat.mul(z, 4n)) == True{} : Bool}, Nat.div(Nat.add(NP, 3n), 4n), NW(ld, n), Equal.sym(Nat, NW(ld, n), Nat.div(Nat.add(NP, 3n), 4n), enw), cnt1(NP))
1543      +hc20 = AB.subst(Nat, z => {Nat.is_lt(Nat.mul(z, 4n), Nat.add(NP, 4n)) == True{} : Bool}, Nat.div(Nat.add(NP, 3n), 4n), NW(ld, n), Equal.sym(Nat, NW(ld, n), Nat.div(Nat.add(NP, 3n), 4n), enw), cnt2(NP))
1544      +hinv0 = Equal.trans(List<&2, U32>, List.take(&2, U32, US(t1), Nat.add(L1, 0n)), List.take(&2, U32, US(t1), L1), List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)),
1545        Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, US(t1), z), Nat.add(L1, 0n), L1, N.add_zero(L1)),
1546        Equal.sym(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), v1,
1547          Equal.trans(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), List.append(&2, U32, v1, Nil{}), v1,
1548            Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z), List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n), Nil{}, Q.take_zero(List.drop(&2, U32, US(ts), qn))),
1549            X.append_nil(v1))))
1550      av(NW(ld, n), Nat.is_le(Nat.add(0n, 4n), NP), ts, e, t1, d, U32.add(qw, 1), C.WD(ts, qw), qw, U32.shrn(l1, 2n), SH(q), L1, qn, r0, 0n, NP, v1,
1551        {==}, hfs, hes, C.ok_full(l1, t1, d, hk1), hdd, hdi0, hsi0, hp0, {==}, shq(q), and3_lt(q), hq0, hl0, N.le_zero_l(NP), hc10, hc20, hinv0)
1552    case False{}:
1553      +q = QQ(ld, s, n)
1554      +qw = U32.shrn(q, 2n)
1555      +L1 = U32.to_nat(l1)
1556      +NP = U32.to_nat(NPw(ld, n))
1557      +qn = U32.to_nat(q)
1558      +nn = U32.to_nat(n)
1559      +hhn = U32.to_nat(HH(ld, n))
1560      +v1 = D.view(C.BT(l1, t1))
1561      +ehh = Equal.trans(Nat, hhn, Nat.min(U32.to_nat(H0(ld)), nn), nn, U.to_nat_min(H0(ld), n), min_r(U32.to_nat(H0(ld)), nn, hb0))
1562      +enp0 = Equal.trans(Nat, NP, Nat.sub(nn, hhn), 0n, enp(ld, n),
1563        Equal.trans(Nat, Nat.sub(nn, hhn), Nat.sub(nn, nn), 0n, Equal.cong(Nat, Nat, z => Nat.sub(nn, z), hhn, nn, ehh), H.sub_self(nn)))
1564      +enw0 = Equal.cong(U32, Nat, z => U32.to_nat(U32.shrn(U32.add(z, 3), 2n)), NPw(ld, n), 0, U.to_nat_inj(NPw(ld, n), 0, enp0))
1565      %Equal.sym(Nat, NW(ld, n), U32.to_nat(U32.shrn(U32.add(0, 3), 2n)), enw0) :
1566        {List.take(&2, U32, US(AWT(_, ts, U32.add(qw, 1), C.WD(ts, qw), t1, qw, U32.shrn(l1, 2n), SH(q))), Nat.add(L1, NP)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), NP)) : List<&2, U32>}
1567      %Equal.sym(Nat, NP, 0n, enp0) :
1568        {List.take(&2, U32, US(t1), Nat.add(L1, _)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), _)) : List<&2, U32>}
1569      Equal.trans(List<&2, U32>, List.take(&2, U32, US(t1), Nat.add(L1, 0n)), List.take(&2, U32, US(t1), L1), List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)),
1570        Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, US(t1), z), Nat.add(L1, 0n), L1, N.add_zero(L1)),
1571        Equal.sym(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), v1,
1572          Equal.trans(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), List.append(&2, U32, v1, Nil{}), v1,
1573            Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z), List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n), Nil{}, Q.take_zero(List.drop(&2, U32, US(ts), qn))),
1574            X.append_nil(v1))))
1575
1576def fav.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +e: Nat, +s: U32, +n: U32,
1577  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1578  +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool},
1579  +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool},
1580  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1581  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1582  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
1583  (+l1, m2) = m
1584  (+t1, +e1) = m2
1585  +sn = U32.to_nat(s)
1586  +nn = U32.to_nat(n)
1587  +hhn = U32.to_nat(HH(ld, n))
1588  +L1 = U32.to_nat(l1)
1589  +NP = U32.to_nat(NPw(ld, n))
1590  +RHS = List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, nn))
1591  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1592  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1593  +hss = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), U32.to_nat(ls), N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hs)
1594  +vd1 = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, hhn)) : List<&2, U32>},
1595    D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1596    X.append_view_t(ld, td, ls, ts, d, e, s, HH(ld, n), hd, he, hss, hc_h(ld, td, n, hc)))
1597  +eq = C.add_fits(s, HH(ld, n), e, C.ok_d(ls, ts, e, he),
1598    N.le_trans(Nat.add(sn, hhn), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), hss, C.ok_len(ls, ts, e, he)))
1599  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1600    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1601    {D.view(Pair.fst(D.Bytes, D.Bytes, _)) == RHS : List<&2, U32>}
1602  %Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(L1, NP), C.add_fits(l1, NPw(ld, n), d, C.ok_d(ld, td, d, hd), hl0)) :
1603    {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), _) == RHS : List<&2, U32>}
1604  Equal.trans(List<&2, U32>, List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(L1, NP)),
1605    List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), NP)), RHS,
1606    avc(Nat.is_lt(U32.to_nat(H0(ld)), nn), ld, td, ls, ts, d, e, s, n, l1, t1, {==}, e1, hd, he, hs, hc),
1607    fin_eq(D.view(C.BT(l1, t1)), D.view(C.BT(ld, td)), US(ts), U32.to_nat(ls), sn, hhn, U32.to_nat(QQ(ld, s, n)), NP, nn, vd1, eq, enp(ld, n), hh_le(ld, n), hs))
1608
1609law fast_append_view_t:
1610  for +ld: U32
1611  for +td: P.Tree<U32>
1612  for +ls: U32
1613  for +ts: P.Tree<U32>
1614  for +d: Nat
1615  for +e: Nat
1616  for +s: U32
1617  for +n: U32
1618  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1619  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
1620  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
1621  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1622  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
1623
1624def fast_append_view_t(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc):
1625  fav.go(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc, C.bmirror(D1(ld, td, ls, ts, s, n)))