proof_append.bend

lawful-bytes@0.1.1.0 · 398 lines · 24 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-words@0.1.0.0/proof_bytes.bend as Y
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# append: n pushes onto dst of bytes s.. of src, and shift, laws on the mirror
15# (named as in proof_ops.bend). The loop lemmas take dst as a mirror that changes
16# at every push (O.push_eq_t names the new one) and src as a fixed mirror.
17
18# Lists
19# =====
20
21law append_nil:
22  for +xs: List<&2, U32>
23  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
24
25def append_nil(xs):
26  match xs:
27    case Nil{}:
28      {==}
29    case Con{+x, t}:
30      %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>}
31      {==}
32
33law append_assoc:
34  for +xs: List<&2, U32>
35  for +ys: List<&2, U32>
36  for +zs: List<&2, U32>
37  {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}
38
39def append_assoc(xs, ys, zs):
40  match xs:
41    case Nil{}:
42      {==}
43    case Con{+x, t}:
44      %append_assoc(t, ys, zs) :
45        {x <> List.append(&2, U32, List.append(&2, U32, t, ys), zs) == x <> _ : List<&2, U32>}
46      {==}
47
48law drop_zero:
49  for +xs: List<&2, U32>
50  {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>}
51
52def drop_zero(xs):
53  match xs:
54    case Nil{}:
55      {==}
56    case Con{x, t}:
57      {==}
58
59def is_some_t(m: Maybe<&2, U32>) -> Type:
60  match m:
61    case None{}:
62      Unit
63    case Some{x}:
64      Empty
65
66law none_some:
67  for -x: U32
68  for e: {None{} == Some{x} : Maybe<&2, U32>}
69  Empty
70
71def none_some(x, e):
72  %e : is_some_t(_)
73  Unit{}
74
75law some_inj:
76  for +x: U32
77  for +y: U32
78  for +e: {Some{x} == Some{y} : Maybe<&2, U32>}
79  {x == y : U32}
80
81def some_inj(x, y, e):
82  Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, x, m), Some{x}, Some{y}, e)
83
84law slice_zero:
85  for +xs: List<&2, U32>
86  for +i: Nat
87  {D.slice(xs, i, 0n) == Nil{} : List<&2, U32>}
88
89def slice_zero(xs, i):
90  Q.take_zero(List.drop(&2, U32, xs, i))
91
92# A slice of 1 + k from i starts with element i.
93law slice_cons:
94  for +xs: List<&2, U32>
95  for +i: Nat
96  for +k: Nat
97  for +x: U32
98  for +h: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
99  {D.slice(xs, i, 1n+k) == x <> D.slice(xs, Nat.add(i, 1n), k) : List<&2, U32>}
100
101def slice_cons(xs, i, k, x, h):
102  match xs i:
103    case Nil{} _:
104      Empty.absurd({D.slice(Nil{}, i, 1n+k) == x <> D.slice(Nil{}, Nat.add(i, 1n), k) : List<&2, U32>}, none_some(x, h))
105    case Con{+y, t} 0n:
106      %some_inj(y, x, h) : {y <> List.take(&2, U32, t, k) == _ <> List.take(&2, U32, List.drop(&2, U32, t, 0n), k) : List<&2, U32>}
107      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) :
108        {y <> List.take(&2, U32, t, k) == y <> List.take(&2, U32, _, k) : List<&2, U32>}
109      {==}
110    case Con{y, t} 1n+p:
111      slice_cons(t, p, k, x, h)
112
113# Nat order
114# =========
115
116law le_split:
117  for +a: Nat
118  for +k: Nat
119  for +m: Nat
120  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
121  {Nat.is_lt(a, m) == True{} : Bool}
122
123def le_split(a, k, m, h):
124  +h2 = AB.subst(Nat, y => {Nat.is_le(y, m) == True{} : Bool}, Nat.add(a, 1n+k), 1n+Nat.add(a, k), N.add_succ(a, k), h)
125  N.le_lt_trans(a, Nat.add(a, k), m, N.le_add_r(a, k),
126    Equal.trans(Bool, Nat.is_lt(Nat.add(a, k), m), Nat.is_le(1n+Nat.add(a, k), m), True{},
127      Equal.sym(Bool, Nat.is_le(1n+Nat.add(a, k), m), Nat.is_lt(Nat.add(a, k), m), N.le_succ_lt(Nat.add(a, k), m)), h2))
128
129law le_shift:
130  for +a: Nat
131  for +k: Nat
132  for +m: Nat
133  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
134  {Nat.is_le(Nat.add(Nat.add(a, 1n), k), m) == True{} : Bool}
135
136def le_shift(a, k, m, h):
137  %Equal.sym(Nat, Nat.add(Nat.add(a, 1n), k), Nat.add(a, Nat.add(1n, k)), N.add_assoc(a, 1n, k)) : {Nat.is_le(_, m) == True{} : Bool}
138  h
139
140# One push
141# ========
142
143# The tree after pushing x onto BT(ld, td).
144def PT(+ld: U32, +td: P.Tree<U32>, +x: U32) -> P.Tree<U32>:
145  I.set_tree(U32, td, (ld >> 2n : U32), W.put_byte(C.WD(td, (ld >> 2n : U32)), U32.to_nat((ld .&. 3 : U32)), x))
146
147law step_room:
148  for +ld: U32
149  for +td: P.Tree<U32>
150  for +d: Nat
151  for +k: Nat
152  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
153  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
154  {Nat.is_lt(U32.to_nat(ld), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
155
156def step_room(ld, td, d, k, hd, hc):
157  +M = Nat.mul(4n, Nat.pow(2n, d))
158  le_split(U32.to_nat(ld), k, M,
159    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), y) == True{} : Bool}, D.cap(C.BT(ld, td)), M, O.cap_ok_t(ld, td, d, hd), hc))
160
161law step_lt:
162  for +ld: U32
163  for +td: P.Tree<U32>
164  for +d: Nat
165  for +k: Nat
166  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
167  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
168  {Nat.is_lt(D.size(C.BT(ld, td)), D.cap(C.BT(ld, td))) == True{} : Bool}
169
170def step_lt(ld, td, d, k, hd, hc):
171  le_split(U32.to_nat(ld), k, D.cap(C.BT(ld, td)), hc)
172
173law step_ok:
174  for +ld: U32
175  for +td: P.Tree<U32>
176  for +d: Nat
177  for +x: U32
178  for +k: Nat
179  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
180  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
181  {D.ok(C.BT((ld + 1 : U32), PT(ld, td, x)), d) == True{} : Bool}
182
183def step_ok(ld, td, d, x, k, hd, hc):
184  AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), PT(ld, td, x)),
185    O.push_eq_t(ld, td, x), O.push_ok_t(ld, td, d, x, hd, step_lt(ld, td, d, k, hd, hc)))
186
187law step_cap:
188  for +ld: U32
189  for +td: P.Tree<U32>
190  for +d: Nat
191  for +x: U32
192  for +k: Nat
193  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
194  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
195  {Nat.is_le(Nat.add(U32.to_nat((ld + 1 : U32)), k), D.cap(C.BT((ld + 1 : U32), PT(ld, td, x)))) == True{} : Bool}
196
197def step_cap(ld, td, d, x, k, hd, hc):
198  +M = Nat.mul(4n, Nat.pow(2n, d))
199  +hr = step_room(ld, td, d, k, hd, hc)
200  %Equal.sym(Nat, D.cap(C.BT((ld + 1 : U32), PT(ld, td, x))), M, O.cap_ok_t((ld + 1 : U32), PT(ld, td, x), d, step_ok(ld, td, d, x, k, hd, hc))) :
201    {Nat.is_le(Nat.add(U32.to_nat((ld + 1 : U32)), k), _) == True{} : Bool}
202  %Equal.sym(Nat, U32.to_nat((ld + 1 : U32)), Nat.add(U32.to_nat(ld), 1n), C.inc_fits(ld, d, C.ok_d(ld, td, d, hd), hr)) :
203    {Nat.is_le(Nat.add(_, k), M) == True{} : Bool}
204  le_shift(U32.to_nat(ld), k, M,
205    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), y) == True{} : Bool}, D.cap(C.BT(ld, td)), M, O.cap_ok_t(ld, td, d, hd), hc))
206
207# One read of src
208# ===============
209
210law read_lt:
211  for +ls: U32
212  for +s: U32
213  for +k: Nat
214  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
215  {Nat.is_lt(U32.to_nat(s), U32.to_nat(ls)) == True{} : Bool}
216
217def read_lt(ls, s, k, hs):
218  le_split(U32.to_nat(s), k, U32.to_nat(ls), hs)
219
220law read_inc:
221  for +ls: U32
222  for +ts: P.Tree<U32>
223  for +e: Nat
224  for +s: U32
225  for +k: Nat
226  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
227  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
228  {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat}
229
230def read_inc(ls, ts, e, s, k, he, hs):
231  C.inc_fits(s, e, C.ok_d(ls, ts, e, he),
232    N.lt_le_trans(U32.to_nat(s), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), read_lt(ls, s, k, hs), C.ok_len(ls, ts, e, he)))
233
234law read_next:
235  for +ls: U32
236  for +ts: P.Tree<U32>
237  for +e: Nat
238  for +s: U32
239  for +k: Nat
240  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
241  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
242  {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), k), U32.to_nat(ls)) == True{} : Bool}
243
244def read_next(ls, ts, e, s, k, he, hs):
245  %Equal.sym(Nat, U32.to_nat((s + 1 : U32)), Nat.add(U32.to_nat(s), 1n), read_inc(ls, ts, e, s, k, he, hs)) :
246    {Nat.is_le(Nat.add(_, k), U32.to_nat(ls)) == True{} : Bool}
247  le_shift(U32.to_nat(s), k, U32.to_nat(ls), hs)
248
249# append
250# ======
251
252law append_go_pair:
253  for +n: Nat
254  for -dst: D.Bytes
255  for +ls: U32
256  for +ts: P.Tree<U32>
257  for +s: U32
258  {B.append.go(n, dst, B.at(C.BT(ls, ts), s), s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(n, dst, B.at(C.BT(ls, ts), s), s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
259
260def append_go_pair(n, dst, ls, ts, s):
261  match n:
262    case 0n:
263      %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)) :
264        {B.append.go(0n, dst, _, s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, dst, _, s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
265      {==}
266    case 1n+k:
267      %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)) :
268        {B.append.go(1n+k, dst, _, s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, dst, _, s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
269      append_go_pair(k, B.push(dst, C.AT(ls, ts, s)), ls, ts, (s + 1 : U32))
270
271law append_pair_t:
272  for +ld: U32
273  for +td: P.Tree<U32>
274  for +ls: U32
275  for +ts: P.Tree<U32>
276  for +s: U32
277  for +n: U32
278  {B.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
279
280def append_pair_t(ld, td, ls, ts, s, n):
281  append_go_pair(U32.to_nat(n), C.BT(ld, td), ls, ts, s)
282
283law append_go_ok:
284  for +n: Nat
285  for +ld: U32
286  for +td: P.Tree<U32>
287  for +ls: U32
288  for +ts: P.Tree<U32>
289  for +d: Nat
290  for +s: U32
291  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
292  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
293  {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s)), d) == True{} : Bool}
294
295def append_go_ok(n, ld, td, ls, ts, d, s, hd, hc):
296  match n:
297    case 0n:
298      %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)) :
299        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s)), d) == True{} : Bool}
300      hd
301    case 1n+k:
302      +x = C.AT(ls, ts, s)
303      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
304        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s)), d) == True{} : Bool}
305      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), PT(ld, td, x)), O.push_eq_t(ld, td, x)) :
306        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32))), d) == True{} : Bool}
307      append_go_ok(k, (ld + 1 : U32), PT(ld, td, x), ls, ts, d, (s + 1 : U32), step_ok(ld, td, d, x, k, hd, hc), step_cap(ld, td, d, x, k, hd, hc))
308
309law append_ok_t:
310  for +ld: U32
311  for +td: P.Tree<U32>
312  for +ls: U32
313  for +ts: P.Tree<U32>
314  for +d: Nat
315  for +s: U32
316  for +n: U32
317  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
318  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}
319  {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}
320
321def append_ok_t(ld, td, ls, ts, d, s, n, hd, hc):
322  append_go_ok(U32.to_nat(n), ld, td, ls, ts, d, s, hd, hc)
323
324law append_go_view:
325  for +n: Nat
326  for +ld: U32
327  for +td: P.Tree<U32>
328  for +ls: U32
329  for +ts: P.Tree<U32>
330  for +d: Nat
331  for +e: Nat
332  for +s: U32
333  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
334  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
335  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), n), U32.to_nat(ls)) == True{} : Bool}
336  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
337  {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), n)) : List<&2, U32>}
338
339def append_go_view(n, ld, td, ls, ts, d, e, s, hd, he, hs, hc):
340  match n:
341    case 0n:
342      +V = D.view(C.BT(ld, td))
343      +xs = D.view(C.BT(ls, ts))
344      %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)) :
345        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s))) == List.append(&2, U32, V, D.slice(xs, U32.to_nat(s), 0n)) : List<&2, U32>}
346      %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 0n), Nil{}, slice_zero(xs, U32.to_nat(s))) :
347        {V == List.append(&2, U32, V, _) : List<&2, U32>}
348      Equal.sym(List<&2, U32>, List.append(&2, U32, V, Nil{}), V, append_nil(V))
349    case 1n+k:
350      +x = C.AT(ls, ts, s)
351      +s1 = (s + 1 : U32)
352      +ld1 = (ld + 1 : U32)
353      +td1 = PT(ld, td, x)
354      +V = D.view(C.BT(ld, td))
355      +xs = D.view(C.BT(ls, ts))
356      +RHS = List.append(&2, U32, V, D.slice(xs, U32.to_nat(s), 1n+k))
357      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
358        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s))) == RHS : List<&2, U32>}
359      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT(ld1, td1), O.push_eq_t(ld, td, x)) :
360        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), s1), s1))) == RHS : List<&2, U32>}
361      +hd1 = step_ok(ld, td, d, x, k, hd, hc)
362      %Equal.sym(List<&2, U32>, D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, C.BT(ld1, td1), B.at(C.BT(ls, ts), s1), s1))),
363        List.append(&2, U32, D.view(C.BT(ld1, td1)), D.slice(xs, U32.to_nat(s1), k)),
364        append_go_view(k, ld1, td1, ls, ts, d, e, s1, hd1, he, read_next(ls, ts, e, s, k, he, hs), step_cap(ld, td, d, x, k, hd, hc))) :
365        {_ == RHS : List<&2, U32>}
366      +hv = AB.subst(U32, y => {U32.is_lt(y, 256) == True{} : Bool}, W.byte(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))), x,
367        Equal.sym(U32, x, W.byte(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))), C.at_val(ls, ts, s)),
368        Y.byte_lt(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))))
369      +pv = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, V, [x]) : List<&2, U32>}, B.push(C.BT(ld, td), x), C.BT(ld1, td1),
370        O.push_eq_t(ld, td, x), O.push_view_t(ld, td, d, x, hd, step_lt(ld, td, d, k, hd, hc), hv))
371      %Equal.sym(List<&2, U32>, D.view(C.BT(ld1, td1)), List.append(&2, U32, V, [x]), pv) :
372        {List.append(&2, U32, _, D.slice(xs, U32.to_nat(s1), k)) == RHS : List<&2, U32>}
373      %Equal.sym(Nat, U32.to_nat(s1), Nat.add(U32.to_nat(s), 1n), read_inc(ls, ts, e, s, k, he, hs)) :
374        {List.append(&2, U32, List.append(&2, U32, V, [x]), D.slice(xs, _, k)) == RHS : List<&2, U32>}
375      +hx = Equal.sym(Maybe<&2, U32>, Some{x}, List.get(&2, U32, xs, U32.to_nat(s)),
376        C.at_view_t(ls, ts, e, s, C.ok_full(ls, ts, e, he), C.ok_d(ls, ts, e, he), C.ok_len(ls, ts, e, he), read_lt(ls, s, k, hs)))
377      %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 1n+k), x <> D.slice(xs, Nat.add(U32.to_nat(s), 1n), k),
378        slice_cons(xs, U32.to_nat(s), k, x, hx)) :
379        {List.append(&2, U32, List.append(&2, U32, V, [x]), D.slice(xs, Nat.add(U32.to_nat(s), 1n), k)) == List.append(&2, U32, V, _) : List<&2, U32>}
380      append_assoc(V, [x], D.slice(xs, Nat.add(U32.to_nat(s), 1n), k))
381
382law append_view_t:
383  for +ld: U32
384  for +td: P.Tree<U32>
385  for +ls: U32
386  for +ts: P.Tree<U32>
387  for +d: Nat
388  for +e: Nat
389  for +s: U32
390  for +n: U32
391  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
392  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
393  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
394  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}
395  {D.view(Pair.fst(D.Bytes, D.Bytes, B.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>}
396
397def append_view_t(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc):
398  append_go_view(U32.to_nat(n), ld, td, ls, ts, d, e, s, hd, he, hs, hc)