proof_grow.bend

lawful-bytes@0.1.1.0 · 511 lines · 26 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/proof_seq.bend as Q
5import lawful-bytes@0.1.1.0/proof_core.bend as C
6import lawful-bytes@0.1.1.0/proof_ops.bend as O
7import lawful-words@0.1.0.0/defs.bend as W
8import lawful-words@0.1.0.0/proof_nat.bend as N
9import lawful-arrays@0.1.0.0/defs.bend as A
10import lawful-arrays@0.1.0.0/proof_base.bend as AB
11import lawful-arrays@0.1.0.0/proof_tree.bend as P
12import lawful-arrays@0.1.0.0/proof_index.bend as I
13
14# The laws about making Bytes: empty, of_list (a loop of pushes) and grow (a
15# loop copying words into a new block). Blocks made by Array.new are mirrored
16# by tnew, so every loop runs on mirrors C.BT(len, t).
17
18# A new block as a tree.
19def tnew(+d: Nat, +v: U32) -> P.Tree<U32>:
20  match d:
21    case 0n:
22      P.TLeaf{v}
23    case 1n+p:
24      P.TNode{tnew(p, v), tnew(p, v)}
25
26law tnew_eq:
27  for +d: Nat
28  for +v: U32
29  {P.fromT(U32, tnew(d, v)) == Array.new(U32, d, v) : Array<U32>}
30
31def tnew_eq(d, v):
32  match d:
33    case 0n:
34      {==}
35    case 1n+p:
36      P.anode_eq(U32, P.fromT(U32, tnew(p, v)), P.fromT(U32, tnew(p, v)), Array.new(U32, p, v), Array.new(U32, p, v),
37        tnew_eq(p, v), tnew_eq(p, v))
38
39law tnew_full:
40  for +d: Nat
41  for +v: U32
42  {A.full(U32, P.fromT(U32, tnew(d, v)), d) == True{} : Bool}
43
44def tnew_full(d, v):
45  %Equal.sym(Array<U32>, P.fromT(U32, tnew(d, v)), Array.new(U32, d, v), tnew_eq(d, v)) : {A.full(U32, _, d) == True{} : Bool}
46  P.new_full(U32, d, v)
47
48law empty_eq:
49  for +d: Nat
50  {B.empty(d) == C.BT(0, tnew(d, 0)) : D.Bytes}
51
52def empty_eq(d):
53  %tnew_eq(d, 0) : {D.Bytes{0, _} == C.BT(0, tnew(d, 0)) : D.Bytes}
54  {==}
55
56# Empty
57# =====
58
59law empty_view:
60  for +d: Nat
61  {D.view(B.empty(d)) == Nil{} : List<&2, U32>}
62
63def empty_view(d):
64  Q.take_zero(D.unpack(A.view(U32, Array.new(U32, d, 0))))
65
66law empty_ok:
67  for +d: Nat
68  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
69  {D.ok(B.empty(d), d) == True{} : Bool}
70
71def empty_ok(d, hd):
72  %Equal.sym(D.Bytes, B.empty(d), C.BT(0, tnew(d, 0)), empty_eq(d)) : {D.ok(_, d) == True{} : Bool}
73  C.ok_mk(0, tnew(d, 0), d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d))))
74
75# Lists
76# =====
77
78law append_nil:
79  for +xs: List<&2, U32>
80  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
81
82def append_nil(xs):
83  match xs:
84    case Nil{}:
85      {==}
86    case Con{x, t}:
87      %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>}
88      {==}
89
90law app_snoc:
91  for +xs: List<&2, U32>
92  for +x: U32
93  for +r: List<&2, U32>
94  {List.append(&2, U32, List.append(&2, U32, xs, [x]), r) == List.append(&2, U32, xs, x <> r) : List<&2, U32>}
95
96def app_snoc(xs, x, r):
97  match xs:
98    case Nil{}:
99      {==}
100    case Con{y, t}:
101      %app_snoc(t, x, r) : {y <> List.append(&2, U32, List.append(&2, U32, t, [x]), r) == y <> _ : List<&2, U32>}
102      {==}
103
104# of_list
105# =======
106
107# Room for one more byte when the rest of the list still fits.
108law ol_room:
109  for +len: U32
110  for +r: Nat
111  for +m: Nat
112  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), m) == True{} : Bool}
113  {Nat.is_lt(U32.to_nat(len), m) == True{} : Bool}
114
115def ol_room(len, r, m, hn):
116  +L = U32.to_nat(len)
117  +h1 = AB.subst(Nat, x => {Nat.is_le(x, m) == True{} : Bool}, Nat.add(L, 1n+r), 1n+Nat.add(L, r), N.add_succ(L, r), hn)
118  +h2 = Equal.trans(Bool, Nat.is_lt(Nat.add(L, r), m), Nat.is_le(1n+Nat.add(L, r), m), True{},
119    Equal.sym(Bool, Nat.is_le(1n+Nat.add(L, r), m), Nat.is_lt(Nat.add(L, r), m), N.le_succ_lt(Nat.add(L, r), m)), h1)
120  N.le_lt_trans(L, Nat.add(L, r), m, N.le_add_r(L, r), h2)
121
122# The rest still fits after the push.
123law ol_rest:
124  for +len: U32
125  for +d: Nat
126  for +r: Nat
127  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
128  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
129  {Nat.is_le(Nat.add(U32.to_nat((len + 1 : U32)), r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
130
131def ol_rest(len, d, r, hd, hn):
132  +L = U32.to_nat(len)
133  +M = Nat.mul(4n, Nat.pow(2n, d))
134  %Equal.sym(Nat, U32.to_nat((len + 1 : U32)), Nat.add(L, 1n), C.inc_fits(len, d, hd, ol_room(len, r, M, hn))) :
135    {Nat.is_le(Nat.add(_, r), M) == True{} : Bool}
136  %Equal.sym(Nat, Nat.add(Nat.add(L, 1n), r), Nat.add(L, Nat.add(1n, r)), N.add_assoc(L, 1n, r)) : {Nat.is_le(_, M) == True{} : Bool}
137  hn
138
139law ol_go_view:
140  for +xs: List<&2, U32>
141  for +len: U32
142  for +t: P.Tree<U32>
143  for +d: Nat
144  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
145  for +hb: {D.all_bytes(xs) == True{} : Bool}
146  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, xs)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
147  {D.view(B.of_list.go(xs, C.BT(len, t))) == List.append(&2, U32, D.view(C.BT(len, t)), xs) : List<&2, U32>}
148
149def ol_go_view(xs, len, t, d, h, hb, hn):
150  match xs:
151    case Nil{}:
152      Equal.sym(List<&2, U32>, List.append(&2, U32, D.view(C.BT(len, t)), Nil{}), D.view(C.BT(len, t)), append_nil(D.view(C.BT(len, t))))
153    case Con{+x, rest}:
154      +k = (len >> 2n : U32)
155      +t2 = I.set_tree(U32, t, k, W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), x))
156      +l2 = (len + 1 : U32)
157      +M = Nat.mul(4n, Nat.pow(2n, d))
158      +hd = C.ok_d(len, t, d, h)
159      +hr = ol_room(len, List.length(&2, U32, rest), M, hn)
160      +hc = AB.subst(Nat, y => {Nat.is_lt(U32.to_nat(len), y) == True{} : Bool}, M, D.cap(C.BT(len, t)),
161        Equal.sym(Nat, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h)), hr)
162      +pe = O.push_eq_t(len, t, x)
163      +hv = AB.and_true_l(U32.is_lt(x, 256), D.all_bytes(rest), hb)
164      +h2 = AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(len, t), x), C.BT(l2, t2), pe,
165        O.push_ok_t(len, t, d, x, h, hc))
166      +pv = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(len, t)), [x]) : List<&2, U32>},
167        B.push(C.BT(len, t), x), C.BT(l2, t2), pe, O.push_view_t(len, t, d, x, h, hc, hv))
168      +RHS = List.append(&2, U32, D.view(C.BT(len, t)), x <> rest)
169      %Equal.sym(D.Bytes, B.push(C.BT(len, t), x), C.BT(l2, t2), pe) : {D.view(B.of_list.go(rest, _)) == RHS : List<&2, U32>}
170      %Equal.sym(List<&2, U32>, D.view(B.of_list.go(rest, C.BT(l2, t2))), List.append(&2, U32, D.view(C.BT(l2, t2)), rest),
171        ol_go_view(rest, l2, t2, d, h2, AB.and_true_r(U32.is_lt(x, 256), D.all_bytes(rest), hb),
172          ol_rest(len, d, List.length(&2, U32, rest), hd, hn))) :
173        {_ == RHS : List<&2, U32>}
174      %Equal.sym(List<&2, U32>, D.view(C.BT(l2, t2)), List.append(&2, U32, D.view(C.BT(len, t)), [x]), pv) :
175        {List.append(&2, U32, _, rest) == RHS : List<&2, U32>}
176      app_snoc(D.view(C.BT(len, t)), x, rest)
177
178law ol_go_ok:
179  for +xs: List<&2, U32>
180  for +len: U32
181  for +t: P.Tree<U32>
182  for +d: Nat
183  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
184  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, xs)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
185  {D.ok(B.of_list.go(xs, C.BT(len, t)), d) == True{} : Bool}
186
187def ol_go_ok(xs, len, t, d, h, hn):
188  match xs:
189    case Nil{}:
190      h
191    case Con{+x, rest}:
192      +k = (len >> 2n : U32)
193      +t2 = I.set_tree(U32, t, k, W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), x))
194      +l2 = (len + 1 : U32)
195      +M = Nat.mul(4n, Nat.pow(2n, d))
196      +hd = C.ok_d(len, t, d, h)
197      +hr = ol_room(len, List.length(&2, U32, rest), M, hn)
198      +hc = AB.subst(Nat, y => {Nat.is_lt(U32.to_nat(len), y) == True{} : Bool}, M, D.cap(C.BT(len, t)),
199        Equal.sym(Nat, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h)), hr)
200      +pe = O.push_eq_t(len, t, x)
201      +h2 = AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(len, t), x), C.BT(l2, t2), pe,
202        O.push_ok_t(len, t, d, x, h, hc))
203      %Equal.sym(D.Bytes, B.push(C.BT(len, t), x), C.BT(l2, t2), pe) : {D.ok(B.of_list.go(rest, _), d) == True{} : Bool}
204      ol_go_ok(rest, l2, t2, d, h2, ol_rest(len, d, List.length(&2, U32, rest), hd, hn))
205
206law of_list_view:
207  for +d: Nat
208  for +xs: List<&2, U32>
209  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
210  for +hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
211  for +hb: {D.all_bytes(xs) == True{} : Bool}
212  {D.view(B.of_list(d, xs)) == xs : List<&2, U32>}
213
214def of_list_view(d, xs, hd, hn, hb):
215  +t0 = tnew(d, 0)
216  %Equal.sym(D.Bytes, B.empty(d), C.BT(0, t0), empty_eq(d)) : {D.view(B.of_list.go(xs, _)) == xs : List<&2, U32>}
217  %Equal.sym(List<&2, U32>, D.view(B.of_list.go(xs, C.BT(0, t0))), List.append(&2, U32, D.view(C.BT(0, t0)), xs),
218    ol_go_view(xs, 0, t0, d, C.ok_mk(0, t0, d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d)))), hb, hn)) :
219    {_ == xs : List<&2, U32>}
220  %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(C.WL(t0)), 0n), Nil{}, Q.take_zero(D.unpack(C.WL(t0)))) :
221    {List.append(&2, U32, _, xs) == xs : List<&2, U32>}
222  {==}
223
224law of_list_ok:
225  for +d: Nat
226  for +xs: List<&2, U32>
227  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
228  for +hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
229  {D.ok(B.of_list(d, xs), d) == True{} : Bool}
230
231def of_list_ok(d, xs, hd, hn):
232  +t0 = tnew(d, 0)
233  %Equal.sym(D.Bytes, B.empty(d), C.BT(0, t0), empty_eq(d)) : {D.ok(B.of_list.go(xs, _), d) == True{} : Bool}
234  ol_go_ok(xs, 0, t0, d, C.ok_mk(0, t0, d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d)))), hn)
235
236# grow
237# ====
238
239# The tree grow.go builds from td: words i .. i+n-1 of t written in.
240def gtree(n: Nat, +t: P.Tree<U32>, +td: P.Tree<U32>, +i: U32) -> P.Tree<U32>:
241  match n:
242    case 0n:
243      td
244    case 1n+k:
245      gtree(k, t, I.set_tree(U32, td, i, C.WD(t, i)), (i + 1 : U32))
246
247law ggo:
248  for +n: Nat
249  for +t: P.Tree<U32>
250  for +td: P.Tree<U32>
251  for +i: U32
252  {B.grow.go(n, Array.get(U32, P.fromT(U32, t), i), P.fromT(U32, td), i) == P.fromT(U32, gtree(n, t, td, i)) : Array<U32>}
253
254def ggo(n, t, td, i):
255  match n:
256    case 0n:
257      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), i), (P.fromT(U32, t), C.WD(t, i)), P.get_pair_t(U32, t, i)) :
258        {B.grow.go(0n, _, P.fromT(U32, td), i) == P.fromT(U32, td) : Array<U32>}
259      {==}
260    case 1n+k:
261      +w = C.WD(t, i)
262      +i1 = (i + 1 : U32)
263      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), i), (P.fromT(U32, t), w), P.get_pair_t(U32, t, i)) :
264        {B.grow.go(1n+k, _, P.fromT(U32, td), i) == P.fromT(U32, gtree(1n+k, t, td, i)) : Array<U32>}
265      %Equal.sym(Array<U32>, Array.set(U32, P.fromT(U32, td), i, w), P.fromT(U32, I.set_tree(U32, td, i, w)), I.set_tree_eq(U32, td, i, w)) :
266        {B.grow.go(k, Array.get(U32, P.fromT(U32, t), i1), _, i1) == P.fromT(U32, gtree(k, t, I.set_tree(U32, td, i, w), i1)) : Array<U32>}
267      ggo(k, t, I.set_tree(U32, td, i, w), i1)
268
269law grow_eq:
270  for +len: U32
271  for +t: P.Tree<U32>
272  for +d: Nat
273  for +e: Nat
274  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
275  {B.grow(C.BT(len, t), e) == C.BT(len, gtree(U32.to_nat(U32.shln(1, d)), t, tnew(e, 0), 0)) : D.Bytes}
276
277def grow_eq(len, t, d, e, hf):
278  +N0 = U32.to_nat(U32.shln(1, d))
279  %Equal.sym(Array<U32> & U32, Array.size(U32, P.fromT(U32, t)), (P.fromT(U32, t), U32.shln(1, d)), P.size_tree(U32, d, t, hf)) :
280    {B.grow.fin(len, e, _) == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes}
281  %tnew_eq(e, 0) : {D.Bytes{len, B.grow.go(N0, Array.get(U32, P.fromT(U32, t), 0), _, 0)} == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes}
282  %Equal.sym(Array<U32>, B.grow.go(N0, Array.get(U32, P.fromT(U32, t), 0), P.fromT(U32, tnew(e, 0)), 0),
283    P.fromT(U32, gtree(N0, t, tnew(e, 0), 0)), ggo(N0, t, tnew(e, 0), 0)) :
284    {D.Bytes{len, _} == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes}
285  {==}
286
287law gfull:
288  for +n: Nat
289  for +t: P.Tree<U32>
290  for +td: P.Tree<U32>
291  for +i: U32
292  for +e: Nat
293  for +hf: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool}
294  {A.full(U32, P.fromT(U32, gtree(n, t, td, i)), e) == True{} : Bool}
295
296def gfull(n, t, td, i, e, hf):
297  match n:
298    case 0n:
299      hf
300    case 1n+k:
301      gfull(k, t, I.set_tree(U32, td, i, C.WD(t, i)), (i + 1 : U32), e, C.full_set(td, e, i, C.WD(t, i), hf))
302
303def mtag(m: Maybe<&2, U32>) -> Bool:
304  match m:
305    case None{}:
306      False{}
307    case Some{x}:
308      True{}
309
310law take_succ_get:
311  for +xs: List<&2, U32>
312  for +j: Nat
313  for +w: U32
314  for +hg: {List.get(&2, U32, xs, j) == Some{w} : Maybe<&2, U32>}
315  {List.take(&2, U32, xs, Nat.add(j, 1n)) == List.append(&2, U32, List.take(&2, U32, xs, j), [w]) : List<&2, U32>}
316
317def take_succ_get(xs, j, w, hg):
318  match xs j:
319    case Nil{} _:
320      Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(j, 1n)) == List.append(&2, U32, Nil{}, [w]) : List<&2, U32>},
321        AB.false_ne_true(Equal.cong(Maybe<&2, U32>, Bool, m => mtag(m), None{}, Some{w}, hg)))
322    case Con{+x, r} 0n:
323      +xw = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, x, m), Some{x}, Some{w}, hg)
324      %Equal.sym(List<&2, U32>, List.take(&2, U32, r, 0n), Nil{}, Q.take_zero(r)) : {x <> _ == [w] : List<&2, U32>}
325      %Equal.sym(U32, x, w, xw) : {_ <> Nil{} == [w] : List<&2, U32>}
326      {==}
327    case Con{+x, r} 1n+p:
328      %take_succ_get(r, p, w, hg) : {x <> List.take(&2, U32, r, Nat.add(p, 1n)) == x <> _ : List<&2, U32>}
329      {==}
330
331law take_all:
332  for +xs: List<&2, U32>
333  {List.take(&2, U32, xs, List.length(&2, U32, xs)) == xs : List<&2, U32>}
334
335def take_all(xs):
336  match xs:
337    case Nil{}:
338      {==}
339    case Con{x, r}:
340      %take_all(r) : {x <> List.take(&2, U32, r, List.length(&2, U32, r)) == x <> _ : List<&2, U32>}
341      {==}
342
343# Only the first q words matter for the first m <= 4q bytes.
344law ut:
345  for +ws: List<&2, U32>
346  for +q: Nat
347  for +m: Nat
348  for +h: {Nat.is_le(m, Nat.mul(q, 4n)) == True{} : Bool}
349  {List.take(&2, U32, D.unpack(ws), m) == List.take(&2, U32, D.unpack(List.take(&2, U32, ws, q)), m) : List<&2, U32>}
350
351def ut(ws, q, m, h):
352  match ws q m:
353    case Nil{} _ _:
354      {==}
355    case Con{w, r} 0n 0n:
356      {==}
357    case Con{w, r} 0n 1n+m1:
358      Empty.absurd({List.take(&2, U32, D.unpack(w <> r), 1n+m1) == Nil{} : List<&2, U32>}, AB.false_ne_true(h))
359    case Con{+w, r} 1n+p 0n:
360      {==}
361    case Con{+w, r} 1n+p 1n+m1:
362      match m1:
363        case 0n:
364          {==}
365        case 1n+m2:
366          match m2:
367            case 0n:
368              {==}
369            case 1n+m3:
370              match m3:
371                case 0n:
372                  {==}
373                case 1n+m4:
374                  %ut(r, p, m4, h) :
375                    {W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> List.take(&2, U32, D.unpack(r), m4) ==
376                      W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> _ : List<&2, U32>}
377                  {==}
378
379# Writing word i keeps the copied prefix and extends it by one word.
380law ginv:
381  for +t: P.Tree<U32>
382  for +td: P.Tree<U32>
383  for +i: U32
384  for +d: Nat
385  for +e: Nat
386  for +hft: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
387  for +hfd: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool}
388  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
389  for +he29: {Nat.is_le(e, 29n) == True{} : Bool}
390  for +hjd: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
391  for +hje: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, e)) == True{} : Bool}
392  for +ei1: {U32.to_nat((i + 1 : U32)) == Nat.add(U32.to_nat(i), 1n) : Nat}
393  for +hinv: {List.take(&2, U32, C.WL(td), U32.to_nat(i)) == List.take(&2, U32, C.WL(t), U32.to_nat(i)) : List<&2, U32>}
394  {List.take(&2, U32, C.WL(I.set_tree(U32, td, i, C.WD(t, i))), U32.to_nat((i + 1 : U32))) == List.take(&2, U32, C.WL(t), U32.to_nat((i + 1 : U32))) : List<&2, U32>}
395
396def ginv(t, td, i, d, e, hft, hfd, hd, he29, hjd, hje, ei1, hinv):
397  +j = U32.to_nat(i)
398  +w = C.WD(t, i)
399  +td2 = I.set_tree(U32, td, i, w)
400  %Equal.sym(Nat, U32.to_nat((i + 1 : U32)), Nat.add(j, 1n), ei1) :
401    {List.take(&2, U32, C.WL(td2), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>}
402  %Equal.sym(List<&2, U32>, C.WL(td2), List.set(&2, U32, C.WL(td), j, w), C.wl_set(td, e, i, w, hfd, he29, hje)) :
403    {List.take(&2, U32, _, Nat.add(j, 1n)) == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>}
404  +hlen = AB.subst(Nat, x => {Nat.is_lt(j, x) == True{} : Bool}, Nat.pow(2n, e), List.length(&2, U32, C.WL(td)),
405    Equal.sym(Nat, List.length(&2, U32, C.WL(td)), Nat.pow(2n, e), P.view_length(U32, e, td, hfd)), hje)
406  %Equal.sym(List<&2, U32>, List.take(&2, U32, List.set(&2, U32, C.WL(td), j, w), Nat.add(j, 1n)),
407    List.append(&2, U32, List.take(&2, U32, C.WL(td), j), [w]), Q.take_set_succ(C.WL(td), j, w, hlen)) :
408    {_ == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>}
409  %Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(td), j), List.take(&2, U32, C.WL(t), j), hinv) :
410    {List.append(&2, U32, _, [w]) == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>}
411  Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(t), Nat.add(j, 1n)), List.append(&2, U32, List.take(&2, U32, C.WL(t), j), [w]),
412    take_succ_get(C.WL(t), j, w, C.wd_get(t, d, i, hft, hd, hjd)))
413
414# The loop copies words i .. i+n-1 of t.
415law gtake:
416  for +n: Nat
417  for +t: P.Tree<U32>
418  for +td: P.Tree<U32>
419  for +i: U32
420  for +d: Nat
421  for +e: Nat
422  for +hft: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
423  for +hfd: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool}
424  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
425  for +he: {Nat.is_le(d, e) == True{} : Bool}
426  for +he29: {Nat.is_le(e, 29n) == True{} : Bool}
427  for +hn: {Nat.is_le(Nat.add(U32.to_nat(i), n), Nat.pow(2n, d)) == True{} : Bool}
428  for +hinv: {List.take(&2, U32, C.WL(td), U32.to_nat(i)) == List.take(&2, U32, C.WL(t), U32.to_nat(i)) : List<&2, U32>}
429  {List.take(&2, U32, C.WL(gtree(n, t, td, i)), Nat.add(U32.to_nat(i), n)) == List.take(&2, U32, C.WL(t), Nat.add(U32.to_nat(i), n)) : List<&2, U32>}
430
431def gtake(n, t, td, i, d, e, hft, hfd, hd, he, he29, hn, hinv):
432  match n:
433    case 0n:
434      +j = U32.to_nat(i)
435      %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) :
436        {List.take(&2, U32, C.WL(td), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>}
437      hinv
438    case 1n+k:
439      +j = U32.to_nat(i)
440      +w = C.WD(t, i)
441      +i1 = (i + 1 : U32)
442      +td2 = I.set_tree(U32, td, i, w)
443      +Pd = Nat.pow(2n, d)
444      +hjd = ol_room(i, k, Pd, hn)
445      +hje = N.lt_le_trans(j, Pd, Nat.pow(2n, e), hjd, N.pow_le(d, e, he))
446      +hj4 = N.lt_le_trans(j, Pd, Nat.mul(4n, Pd), hjd, N.le_add_r(Pd, Nat.mul(3n, Pd)))
447      +ei1 = C.inc_fits(i, d, hd, hj4)
448      +ek = Equal.trans(Nat, Nat.add(U32.to_nat(i1), k), Nat.add(Nat.add(j, 1n), k), Nat.add(j, 1n+k),
449        Equal.cong(Nat, Nat, x => Nat.add(x, k), U32.to_nat(i1), Nat.add(j, 1n), ei1), N.add_assoc(j, 1n, k))
450      %ek : {List.take(&2, U32, C.WL(gtree(k, t, td2, i1)), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>}
451      gtake(k, t, td2, i1, d, e, hft, C.full_set(td, e, i, w, hfd), hd, he, he29,
452        AB.subst(Nat, x => {Nat.is_le(x, Pd) == True{} : Bool}, Nat.add(j, 1n+k), Nat.add(U32.to_nat(i1), k),
453          Equal.sym(Nat, Nat.add(U32.to_nat(i1), k), Nat.add(j, 1n+k), ek), hn),
454        ginv(t, td, i, d, e, hft, hfd, hd, he29, hjd, hje, ei1, hinv))
455
456law grow_view_t:
457  for +len: U32
458  for +t: P.Tree<U32>
459  for +d: Nat
460  for +e: Nat
461  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
462  for +he: {Nat.is_le(d, e) == True{} : Bool}
463  for +he29: {Nat.is_le(e, 29n) == True{} : Bool}
464  {D.view(B.grow(C.BT(len, t), e)) == D.view(C.BT(len, t)) : List<&2, U32>}
465
466def grow_view_t(len, t, d, e, h, he, he29):
467  +hf = C.ok_full(len, t, d, h)
468  +hd = C.ok_d(len, t, d, h)
469  +L = U32.to_nat(len)
470  +N0 = U32.to_nat(U32.shln(1, d))
471  +Pd = Nat.pow(2n, d)
472  +t0 = tnew(e, 0)
473  +GTR = gtree(N0, t, t0, 0)
474  +RHS = D.view(C.BT(len, t))
475  +hl4 = AB.subst(Nat, x => {Nat.is_le(L, x) == True{} : Bool}, Nat.mul(4n, Pd), Nat.mul(Pd, 4n), N.mul_comm(4n, Pd),
476    C.ok_len(len, t, d, h))
477  +hn0 = AB.subst(Nat, x => {Nat.is_le(x, Pd) == True{} : Bool}, Pd, N0,
478    Equal.sym(Nat, N0, Pd, I.size_n(d, C.lt32(d, hd))), N.le_refl(Pd))
479  +hinv0 = Equal.trans(List<&2, U32>, List.take(&2, U32, C.WL(t0), 0n), Nil{}, List.take(&2, U32, C.WL(t), 0n),
480    Q.take_zero(C.WL(t0)), Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(t), 0n), Nil{}, Q.take_zero(C.WL(t))))
481  +g1 = AB.subst(Nat, x => {List.take(&2, U32, C.WL(GTR), x) == List.take(&2, U32, C.WL(t), x) : List<&2, U32>}, N0, Pd,
482    I.size_n(d, C.lt32(d, hd)), gtake(N0, t, t0, 0, d, e, hf, tnew_full(e, 0), hd, he, he29, hn0, hinv0))
483  +tall = AB.subst(Nat, x => {List.take(&2, U32, C.WL(t), x) == C.WL(t) : List<&2, U32>}, List.length(&2, U32, C.WL(t)), Pd,
484    P.view_length(U32, d, t, hf), take_all(C.WL(t)))
485  +e1 = Equal.trans(List<&2, U32>, List.take(&2, U32, C.WL(GTR), Pd), List.take(&2, U32, C.WL(t), Pd), C.WL(t), g1, tall)
486  %Equal.sym(D.Bytes, B.grow(C.BT(len, t), e), C.BT(len, GTR), grow_eq(len, t, d, e, hf)) : {D.view(_) == RHS : List<&2, U32>}
487  %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(C.WL(GTR)), L), List.take(&2, U32, D.unpack(List.take(&2, U32, C.WL(GTR), Pd)), L),
488    ut(C.WL(GTR), Pd, L, hl4)) :
489    {_ == RHS : List<&2, U32>}
490  %Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(GTR), Pd), C.WL(t), e1) :
491    {List.take(&2, U32, D.unpack(_), L) == RHS : List<&2, U32>}
492  {==}
493
494law grow_ok_t:
495  for +len: U32
496  for +t: P.Tree<U32>
497  for +d: Nat
498  for +e: Nat
499  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
500  for +he: {Nat.is_le(d, e) == True{} : Bool}
501  for +he29: {Nat.is_le(e, 29n) == True{} : Bool}
502  {D.ok(B.grow(C.BT(len, t), e), e) == True{} : Bool}
503
504def grow_ok_t(len, t, d, e, h, he, he29):
505  +hf = C.ok_full(len, t, d, h)
506  +N0 = U32.to_nat(U32.shln(1, d))
507  +GTR = gtree(N0, t, tnew(e, 0), 0)
508  %Equal.sym(D.Bytes, B.grow(C.BT(len, t), e), C.BT(len, GTR), grow_eq(len, t, d, e, hf)) : {D.ok(_, e) == True{} : Bool}
509  C.ok_mk(len, GTR, e, gfull(N0, t, tnew(e, 0), 0, e, tnew_full(e, 0)), he29,
510    N.le_trans(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), Nat.mul(4n, Nat.pow(2n, e)), C.ok_len(len, t, d, h),
511      N.le_mul_l(4n, Nat.pow(2n, d), Nat.pow(2n, e), N.pow_le(d, e, he))))