proof_append.bend
lawful-bytes@0.1.0.0 · 398 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-bytes@0.1.0.0/bytes.bend as B
4import lawful-bytes@0.1.0.0/proof_seq.bend as Q
5import lawful-bytes@0.1.0.0/proof_core.bend as C
6import lawful-bytes@0.1.0.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)