proof_same.bend

lawful-bytes@0.1.1.0 · 668 lines · 34 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-words@0.1.0.0/defs.bend as W
7import lawful-words@0.1.0.0/proof_nat.bend as N
8import lawful-words@0.1.0.0/proof_u32.bend as U
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 reading loops: to_list, same and same1, on the mirror C.BT(len, t)
15# (law-shaped, as in proof_ops.bend). Each loop carries the read pair
16# B.at(BT, s) literally: C.at_pair_t turns it into (BT, AT) so the loop steps,
17# and the next call reads B.at(BT, s + 1), the same form one index on.
18
19# List and index facts
20# ====================
21
22def mdisc(m: Maybe<&2, U32>) -> Type:
23  match m:
24    case None{}:
25      Empty
26    case Some{x}:
27      Unit
28
29law none_some:
30  for -x: U32
31  for e: {None{} == Some{x} : Maybe<&2, U32>}
32  Empty
33
34def none_some(x, e):
35  %Equal.sym(Maybe<&2, U32>, None{}, Some{x}, e) : mdisc(_)
36  Unit{}
37
38law drop_zero:
39  for +xs: List<&2, U32>
40  {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>}
41
42def drop_zero(xs):
43  match xs:
44    case Nil{}:
45      {==}
46    case Con{x, t}:
47      {==}
48
49# Dropping j elements, when element j is x: x, then the rest.
50law drop_get:
51  for +xs: List<&2, U32>
52  for +j: Nat
53  for +x: U32
54  for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
55  {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}
56
57def drop_get(xs, j, x, h):
58  match xs j:
59    case Nil{} _:
60      Empty.absurd({List.drop(&2, U32, Nil{}, j) == x <> List.drop(&2, U32, Nil{}, Nat.add(j, 1n)) : List<&2, U32>},
61        none_some(x, h))
62    case Con{+y, t} 0n:
63      +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h)
64      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>}
65      %Equal.sym(U32, y, x, yx) : {_ <> t == x <> t : List<&2, U32>}
66      {==}
67    case Con{y, t} 1n+p:
68      drop_get(t, p, x, h)
69
70law slice_cons:
71  for +xs: List<&2, U32>
72  for +j: Nat
73  for +k: Nat
74  for +x: U32
75  for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
76  {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
77
78def slice_cons(xs, j, k, x, h):
79  %Equal.sym(List<&2, U32>, List.drop(&2, U32, xs, j), x <> List.drop(&2, U32, xs, Nat.add(j, 1n)), drop_get(xs, j, x, h)) :
80    {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
81  {==}
82
83# a + 1 + m <= b gives a < b.
84law lt_of_le:
85  for +a: Nat
86  for +m: Nat
87  for +b: Nat
88  for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
89  {Nat.is_lt(a, b) == True{} : Bool}
90
91def lt_of_le(a, m, b, h):
92  +h1 = AB.subst(Nat, x => {Nat.is_le(x, b) == True{} : Bool}, Nat.add(a, 1n+m), 1n+Nat.add(a, m), AB.add_succ(a, m), h)
93  +h2 = N.le_trans(1n+a, 1n+Nat.add(a, m), b, N.le_add_r(a, m), h1)
94  Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), True{}, Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), N.le_succ_lt(a, b)), h2)
95
96# a + 1 + m <= b gives (a + 1) + m <= b.
97law le_step:
98  for +a: Nat
99  for +m: Nat
100  for +b: Nat
101  for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
102  {Nat.is_le(Nat.add(Nat.add(a, 1n), m), b) == True{} : Bool}
103
104def le_step(a, m, b, h):
105  AB.subst(Nat, x => {Nat.is_le(x, b) == True{} : Bool}, Nat.add(a, Nat.add(1n, m)), Nat.add(Nat.add(a, 1n), m),
106    Equal.sym(Nat, Nat.add(Nat.add(a, 1n), m), Nat.add(a, Nat.add(1n, m)), N.add_assoc(a, 1n, m)), h)
107
108# One step of a read loop at index s with n + 1 left, within a Bytes of size len:
109# byte s is read, s + 1 does not wrap, and the bound holds one index on.
110law step_val:
111  for +len: U32
112  for +t: P.Tree<U32>
113  for +d: Nat
114  for +s: U32
115  for +m: Nat
116  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
117  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
118  {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)) == Some{C.AT(len, t, s)} : Maybe<&2, U32>}
119
120def step_val(len, t, d, s, m, h, hs):
121  Equal.sym(Maybe<&2, U32>, Some{C.AT(len, t, s)}, List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)),
122    C.at_view_t(len, t, d, s, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h),
123      lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs)))
124
125law step_inc:
126  for +len: U32
127  for +t: P.Tree<U32>
128  for +d: Nat
129  for +s: U32
130  for +m: Nat
131  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
132  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
133  {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat}
134
135def step_inc(len, t, d, s, m, h, hs):
136  C.inc_fits(s, d, C.ok_d(len, t, d, h),
137    N.lt_le_trans(U32.to_nat(s), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs),
138      C.ok_len(len, t, d, h)))
139
140law step_le:
141  for +len: U32
142  for +t: P.Tree<U32>
143  for +d: Nat
144  for +s: U32
145  for +m: Nat
146  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
147  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
148  {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), m), U32.to_nat(len)) == True{} : Bool}
149
150def step_le(len, t, d, s, m, h, hs):
151  AB.subst(Nat, x => {Nat.is_le(Nat.add(x, m), U32.to_nat(len)) == True{} : Bool}, Nat.add(U32.to_nat(s), 1n), U32.to_nat((s + 1 : U32)),
152    Equal.sym(Nat, U32.to_nat((s + 1 : U32)), Nat.add(U32.to_nat(s), 1n), step_inc(len, t, d, s, m, h, hs)),
153    le_step(U32.to_nat(s), m, U32.to_nat(len), hs))
154
155# to_list
156# =======
157
158# to_list reads from the last byte back, putting each in front of acc, so its
159# loop is a tail call. The invariant: reading at j = m + s with 1 + m bytes
160# left gives slice(view, s, 1 + m) followed by acc.
161
162law tl_pair:
163  for +n: Nat
164  for +len: U32
165  for +t: P.Tree<U32>
166  for +j: U32
167  for +acc: List<&2, U32>
168  {B.to_list.go(n, B.at(C.BT(len, t), j), j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), j), j, acc))) : D.Bytes & List<&2, U32>}
169
170def tl_pair(n, len, t, j, acc):
171  match n:
172    case 0n:
173      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) :
174        {B.to_list.go(0n, _, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, j, acc))) : D.Bytes & List<&2, U32>}
175      {==}
176    case 1n+m:
177      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) :
178        {B.to_list.go(1n+m, _, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, j, acc))) : D.Bytes & List<&2, U32>}
179      tl_pair(m, len, t, (j - 1 : U32), C.AT(len, t, j) <> acc)
180
181law append_nil:
182  for +xs: List<&2, U32>
183  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
184
185def append_nil(xs):
186  match xs:
187    case Nil{}:
188      {==}
189    case Con{+x, t}:
190      Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, List.append(&2, U32, t, Nil{}), t, append_nil(t))
191
192law get_drop:
193  for +xs: List<&2, U32>
194  for +i: Nat
195  for +k: Nat
196  {List.get(&2, U32, List.drop(&2, U32, xs, i), k) == List.get(&2, U32, xs, Nat.add(i, k)) : Maybe<&2, U32>}
197
198def get_drop(xs, i, k):
199  match xs i:
200    case Nil{} _:
201      {==}
202    case Con{x, t} 0n:
203      {==}
204    case Con{x, t} 1n+p:
205      get_drop(t, p, k)
206
207# Taking k + 1 elements then acc is taking k then element k, then acc.
208law take_snoc:
209  for +ys: List<&2, U32>
210  for +k: Nat
211  for +x: U32
212  for +acc: List<&2, U32>
213  for +h: {List.get(&2, U32, ys, k) == Some{x} : Maybe<&2, U32>}
214  {List.append(&2, U32, List.take(&2, U32, ys, 1n+k), acc) == List.append(&2, U32, List.take(&2, U32, ys, k), x <> acc) : List<&2, U32>}
215
216def take_snoc(ys, k, x, acc, h):
217  match ys k:
218    case Nil{} _:
219      Empty.absurd({List.append(&2, U32, List.take(&2, U32, Nil{}, 1n+k), acc) == List.append(&2, U32, List.take(&2, U32, Nil{}, k), x <> acc) : List<&2, U32>},
220        none_some(x, h))
221    case Con{+y, t} 0n:
222      +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h)
223      %Equal.sym(List<&2, U32>, List.take(&2, U32, t, 0n), Nil{}, Q.take_zero(t)) : {y <> List.append(&2, U32, _, acc) == x <> acc : List<&2, U32>}
224      %Equal.sym(U32, y, x, yx) : {_ <> acc == x <> acc : List<&2, U32>}
225      {==}
226    case Con{+y, t} 1n+p:
227      Equal.cong(List<&2, U32>, List<&2, U32>, z => y <> z, List.append(&2, U32, List.take(&2, U32, t, 1n+p), acc),
228        List.append(&2, U32, List.take(&2, U32, t, p), x <> acc), take_snoc(t, p, x, acc, h))
229
230law slice_snoc:
231  for +xs: List<&2, U32>
232  for +i: Nat
233  for +k: Nat
234  for +x: U32
235  for +acc: List<&2, U32>
236  for +h: {List.get(&2, U32, xs, Nat.add(k, i)) == Some{x} : Maybe<&2, U32>}
237  {List.append(&2, U32, D.slice(xs, i, 1n+k), acc) == List.append(&2, U32, D.slice(xs, i, k), x <> acc) : List<&2, U32>}
238
239def slice_snoc(xs, i, k, x, acc, h):
240  +ys = List.drop(&2, U32, xs, i)
241  +g = AB.subst(Nat, z => {List.get(&2, U32, ys, k) == List.get(&2, U32, xs, z) : Maybe<&2, U32>}, Nat.add(i, k), Nat.add(k, i),
242    N.add_comm(i, k), get_drop(xs, i, k))
243  take_snoc(ys, k, x, acc, Equal.trans(Maybe<&2, U32>, List.get(&2, U32, ys, k), List.get(&2, U32, xs, Nat.add(k, i)), Some{x}, g, h))
244
245# Byte j, for j = m + s below len, is element m + s of the view.
246law tl_val:
247  for +m: Nat
248  for +len: U32
249  for +t: P.Tree<U32>
250  for +d: Nat
251  for +s: U32
252  for +j: U32
253  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
254  for +hj: {U32.to_nat(j) == Nat.add(m, U32.to_nat(s)) : Nat}
255  for +hs: {Nat.is_lt(Nat.add(m, U32.to_nat(s)), U32.to_nat(len)) == True{} : Bool}
256  {List.get(&2, U32, D.view(C.BT(len, t)), Nat.add(m, U32.to_nat(s))) == Some{C.AT(len, t, j)} : Maybe<&2, U32>}
257
258def tl_val(m, len, t, d, s, j, h, hj, hs):
259  +a = Nat.add(m, U32.to_nat(s))
260  +hi = AB.subst(Nat, z => {Nat.is_lt(z, U32.to_nat(len)) == True{} : Bool}, a, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), a, hj), hs)
261  +e = Equal.sym(Maybe<&2, U32>, Some{C.AT(len, t, j)}, List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)),
262    C.at_view_t(len, t, d, j, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h), hi))
263  AB.subst(Nat, z => {List.get(&2, U32, D.view(C.BT(len, t)), z) == Some{C.AT(len, t, j)} : Maybe<&2, U32>}, U32.to_nat(j), a, hj, e)
264
265# j - 1 for j = 1 + m + s.
266law tl_dec:
267  for +m: Nat
268  for +s: U32
269  for +j: U32
270  for +hj: {U32.to_nat(j) == 1n+Nat.add(m, U32.to_nat(s)) : Nat}
271  {U32.to_nat((j - 1 : U32)) == Nat.add(m, U32.to_nat(s)) : Nat}
272
273def tl_dec(m, s, j, hj):
274  +a = Nat.add(m, U32.to_nat(s))
275  +hle = Equal.trans(Bool, U32.is_le(1, j), Nat.is_le(U32.to_nat(1), U32.to_nat(j)), True{}, U.is_le_to_nat(1, j),
276    AB.subst(Nat, z => {Nat.is_le(U32.to_nat(1), z) == True{} : Bool}, 1n+a, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), 1n+a, hj), N.le_zero_l(a)))
277  %Equal.sym(Nat, U32.to_nat((j - 1 : U32)), Nat.sub(U32.to_nat(j), U32.to_nat(1)), U.to_nat_sub_le(j, 1, hle)) : {_ == a : Nat}
278  %Equal.sym(Nat, U32.to_nat(j), 1n+a, hj) : {Nat.sub(_, U32.to_nat(1)) == a : Nat}
279  N.sub_zero(a)
280
281law tl_lt:
282  for +a: Nat
283  for +b: Nat
284  for +h: {Nat.is_lt(1n+a, b) == True{} : Bool}
285  {Nat.is_lt(a, b) == True{} : Bool}
286
287def tl_lt(a, b, h):
288  Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), True{}, Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), N.le_succ_lt(a, b)),
289    N.lt_to_le(1n+a, b, h))
290
291law tl_view:
292  for +m: Nat
293  for +len: U32
294  for +t: P.Tree<U32>
295  for +d: Nat
296  for +s: U32
297  for +j: U32
298  for +acc: List<&2, U32>
299  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
300  for +hj: {U32.to_nat(j) == Nat.add(m, U32.to_nat(s)) : Nat}
301  for +hs: {Nat.is_lt(Nat.add(m, U32.to_nat(s)), U32.to_nat(len)) == True{} : Bool}
302  {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, B.at(C.BT(len, t), j), j, acc)) == List.append(&2, U32, D.slice(D.view(C.BT(len, t)), U32.to_nat(s), 1n+m), acc) : List<&2, U32>}
303
304def tl_view(m, len, t, d, s, j, acc, h, hj, hs):
305  match m:
306    case 0n:
307      +x = C.AT(len, t, j)
308      +j1 = (j - 1 : U32)
309      +xs = D.view(C.BT(len, t))
310      +ys = List.drop(&2, U32, xs, U32.to_nat(s))
311      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) :
312        {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n, _, j, acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc) : List<&2, U32>}
313      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j1), (C.BT(len, t), C.AT(len, t, j1)), C.at_pair_t(len, t, j1)) :
314        {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, j1, x <> acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc) : List<&2, U32>}
315      %Equal.sym(List<&2, U32>, List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc), List.append(&2, U32, D.slice(xs, U32.to_nat(s), 0n), x <> acc),
316        slice_snoc(xs, U32.to_nat(s), 0n, x, acc, tl_val(0n, len, t, d, s, j, h, hj, hs))) :
317        {x <> acc == _ : List<&2, U32>}
318      %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {x <> acc == List.append(&2, U32, _, x <> acc) : List<&2, U32>}
319      {==}
320    case 1n+p:
321      +x = C.AT(len, t, j)
322      +j1 = (j - 1 : U32)
323      +xs = D.view(C.BT(len, t))
324      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) :
325        {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+(1n+p), _, j, acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+(1n+p)), acc) : List<&2, U32>}
326      %Equal.sym(List<&2, U32>, List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+(1n+p)), acc), List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+p), x <> acc),
327        slice_snoc(xs, U32.to_nat(s), 1n+p, x, acc, tl_val(1n+p, len, t, d, s, j, h, hj, hs))) :
328        {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+p, B.at(C.BT(len, t), j1), j1, x <> acc)) == _ : List<&2, U32>}
329      tl_view(p, len, t, d, s, j1, x <> acc, h, tl_dec(p, s, j, hj), tl_lt(Nat.add(p, U32.to_nat(s)), U32.to_nat(len), hs))
330
331# to_list(BT, s, n) with k = n bytes: none, or 1 + p read from s + n - 1.
332law tl_view_k:
333  for +k: Nat
334  for +len: U32
335  for +t: P.Tree<U32>
336  for +d: Nat
337  for +s: U32
338  for +n: U32
339  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
340  for +hk: {U32.to_nat(n) == k : Nat}
341  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), U32.to_nat(len)) == True{} : Bool}
342  {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(k, B.at(C.BT(len, t), ((s + n : U32) - 1 : U32)), ((s + n : U32) - 1 : U32), Nil{})) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), k) : List<&2, U32>}
343
344def tl_view_k(k, len, t, d, s, n, h, hk, hs):
345  match k:
346    case 0n:
347      +e = ((s + n : U32) - 1 : U32)
348      +xs = D.view(C.BT(len, t))
349      +ys = List.drop(&2, U32, xs, U32.to_nat(s))
350      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), e), (C.BT(len, t), C.AT(len, t, e)), C.at_pair_t(len, t, e)) :
351        {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, e, Nil{})) == D.slice(xs, U32.to_nat(s), 0n) : List<&2, U32>}
352      Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys))
353    case 1n+p:
354      +e = ((s + n : U32) - 1 : U32)
355      +xs = D.view(C.BT(len, t))
356      +a = Nat.add(p, U32.to_nat(s))
357      +sn = Nat.add(U32.to_nat(s), U32.to_nat(n))
358      +E = Equal.trans(Nat, sn, Nat.add(U32.to_nat(s), 1n+p), 1n+a,
359        Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(s), z), U32.to_nat(n), 1n+p, hk),
360        Equal.trans(Nat, Nat.add(U32.to_nat(s), 1n+p), 1n+Nat.add(U32.to_nat(s), p), 1n+a, N.add_succ(U32.to_nat(s), p),
361          Equal.cong(Nat, Nat, z => 1n+z, Nat.add(U32.to_nat(s), p), a, N.add_comm(U32.to_nat(s), p))))
362      +hsum = C.add_fits(s, n, d, C.ok_d(len, t, d, h), N.le_trans(sn, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hs, C.ok_len(len, t, d, h)))
363      +hj = tl_dec(p, s, (s + n : U32), Equal.trans(Nat, U32.to_nat((s + n : U32)), sn, 1n+a, hsum, E))
364      +hlt = Equal.trans(Bool, Nat.is_lt(a, U32.to_nat(len)), Nat.is_le(1n+a, U32.to_nat(len)), True{},
365        Equal.sym(Bool, Nat.is_le(1n+a, U32.to_nat(len)), Nat.is_lt(a, U32.to_nat(len)), N.le_succ_lt(a, U32.to_nat(len))),
366        AB.subst(Nat, z => {Nat.is_le(z, U32.to_nat(len)) == True{} : Bool}, sn, 1n+a, E, hs))
367      +sl = D.slice(xs, U32.to_nat(s), 1n+p)
368      Equal.trans(List<&2, U32>, Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+p, B.at(C.BT(len, t), e), e, Nil{})), List.append(&2, U32, sl, Nil{}), sl,
369        tl_view(p, len, t, d, s, e, Nil{}, h, hj, hlt), append_nil(sl))
370
371law to_list_pair_t:
372  for +len: U32
373  for +t: P.Tree<U32>
374  for +s: U32
375  for +n: U32
376  {B.to_list(C.BT(len, t), s, n) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list(C.BT(len, t), s, n))) : D.Bytes & List<&2, U32>}
377
378def to_list_pair_t(len, t, s, n):
379  tl_pair(U32.to_nat(n), len, t, ((s + n : U32) - 1 : U32), Nil{})
380
381law to_list_view_t:
382  for +len: U32
383  for +t: P.Tree<U32>
384  for +d: Nat
385  for +s: U32
386  for +n: U32
387  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
388  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
389  {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(C.BT(len, t), s, n)) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}
390
391def to_list_view_t(len, t, d, s, n, h, hs):
392  tl_view_k(U32.to_nat(n), len, t, d, s, n, h, {==}, hs)
393
394# same
395# ====
396
397law and_assoc:
398  for +a: Bool
399  for +b: Bool
400  for +c: Bool
401  {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
402
403def and_assoc(a, b, c):
404  match a:
405    case False{}:
406      {==}
407    case True{}:
408      {==}
409
410# Comparing n more bytes from i of A and from j of B, after an empty prefix:
411# acc and the comparison of the two slices.
412law lists_end:
413  for +acc: Bool
414  for +xs: List<&2, U32>
415  for +ys: List<&2, U32>
416  {acc == Bool.and(acc, D.list_eq(List.take(&2, U32, xs, 0n), List.take(&2, U32, ys, 0n))) : Bool}
417
418def lists_end(acc, xs, ys):
419  %Equal.sym(List<&2, U32>, List.take(&2, U32, xs, 0n), Nil{}, Q.take_zero(xs)) :
420    {acc == Bool.and(acc, D.list_eq(_, List.take(&2, U32, ys, 0n))) : Bool}
421  %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) :
422    {acc == Bool.and(acc, D.list_eq(Nil{}, _)) : Bool}
423  Equal.sym(Bool, Bool.and(acc, True{}), acc, N.and_true_r_id(acc))
424
425# One step of a comparison loop: the two slices from x and y, with the
426# accumulated test rebracketed.
427law lists_step:
428  for +acc: Bool
429  for +xs: List<&2, U32>
430  for +ys: List<&2, U32>
431  for +i: Nat
432  for +j: Nat
433  for +i1: U32
434  for +j1: U32
435  for +k: Nat
436  for +x: U32
437  for +y: U32
438  for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
439  for +hy: {List.get(&2, U32, ys, j) == Some{y} : Maybe<&2, U32>}
440  for +ei: {U32.to_nat(i1) == Nat.add(i, 1n) : Nat}
441  for +ej: {U32.to_nat(j1) == Nat.add(j, 1n) : Nat}
442  {Bool.and(Bool.and(acc, U32.is_eq(x, y)), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k)))
443    == Bool.and(acc, D.list_eq(D.slice(xs, i, 1n+k), D.slice(ys, j, 1n+k))) : Bool}
444
445def lists_step(acc, xs, ys, i, j, i1, j1, k, x, y, hx, hy, ei, ej):
446  +LHS = Bool.and(Bool.and(acc, U32.is_eq(x, y)), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k)))
447  %Equal.sym(List<&2, U32>, D.slice(xs, i, 1n+k), x <> D.slice(xs, Nat.add(i, 1n), k), slice_cons(xs, i, k, x, hx)) :
448    {LHS == Bool.and(acc, D.list_eq(_, D.slice(ys, j, 1n+k))) : Bool}
449  %Equal.sym(List<&2, U32>, D.slice(ys, j, 1n+k), y <> D.slice(ys, Nat.add(j, 1n), k), slice_cons(ys, j, k, y, hy)) :
450    {LHS == Bool.and(acc, D.list_eq(x <> D.slice(xs, Nat.add(i, 1n), k), _)) : Bool}
451  %ei : {LHS == Bool.and(acc, Bool.and(U32.is_eq(x, y), D.list_eq(D.slice(xs, _, k), D.slice(ys, Nat.add(j, 1n), k)))) : Bool}
452  %ej : {LHS == Bool.and(acc, Bool.and(U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, _, k)))) : Bool}
453  and_assoc(acc, U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k)))
454
455law sm_pair:
456  for +n: Nat
457  for +la: U32
458  for +ta: P.Tree<U32>
459  for +lb: U32
460  for +tb: P.Tree<U32>
461  for +i: U32
462  for +j: U32
463  for +acc: Bool
464  {B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
465    Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)}
466
467def sm_pair(n, la, ta, lb, tb, i, j, acc):
468  match n:
469    case 0n:
470      %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) :
471        {B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
472          Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)}
473      %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) :
474        {B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
475          Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))))) : D.Bytes & (D.Bytes & Bool)}
476      {==}
477    case 1n+k:
478      %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) :
479        {B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
480          Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)}
481      %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) :
482        {B.same.go(1n+k, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
483          Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))))) : D.Bytes & (D.Bytes & Bool)}
484      sm_pair(k, la, ta, lb, tb, (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(C.AT(la, ta, i), C.AT(lb, tb, j)))
485
486law sm_view:
487  for +n: Nat
488  for +la: U32
489  for +ta: P.Tree<U32>
490  for +lb: U32
491  for +tb: P.Tree<U32>
492  for +d: Nat
493  for +e: Nat
494  for +i: U32
495  for +j: U32
496  for +acc: Bool
497  for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool}
498  for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool}
499  for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(la)) == True{} : Bool}
500  for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(lb)) == True{} : Bool}
501  {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc)))
502    == Bool.and(acc, D.list_eq(D.slice(D.view(C.BT(la, ta)), U32.to_nat(i), n), D.slice(D.view(C.BT(lb, tb)), U32.to_nat(j), n))) : Bool}
503
504def sm_view(n, la, ta, lb, tb, d, e, i, j, acc, ha, hb, hi, hj):
505  match n:
506    case 0n:
507      +xa = D.view(C.BT(la, ta))
508      +xb = D.view(C.BT(lb, tb))
509      +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 0n), D.slice(xb, U32.to_nat(j), 0n)))
510      %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) :
511        {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc))) == RHS : Bool}
512      %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) :
513        {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))) == RHS : Bool}
514      lists_end(acc, List.drop(&2, U32, xa, U32.to_nat(i)), List.drop(&2, U32, xb, U32.to_nat(j)))
515    case 1n+k:
516      +xa = D.view(C.BT(la, ta))
517      +xb = D.view(C.BT(lb, tb))
518      +x = C.AT(la, ta, i)
519      +y = C.AT(lb, tb, j)
520      +i1 = (i + 1 : U32)
521      +j1 = (j + 1 : U32)
522      +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 1n+k), D.slice(xb, U32.to_nat(j), 1n+k)))
523      %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), x), C.at_pair_t(la, ta, i)) :
524        {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc))) == RHS : Bool}
525      %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), y), C.at_pair_t(lb, tb, j)) :
526        {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, (C.BT(la, ta), x), _, i, j, acc))) == RHS : Bool}
527      %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(k, B.at(C.BT(la, ta), i1), B.at(C.BT(lb, tb), j1), i1, j1, acc && U32.is_eq(x, y)))),
528        Bool.and(acc && U32.is_eq(x, y), D.list_eq(D.slice(xa, U32.to_nat(i1), k), D.slice(xb, U32.to_nat(j1), k))),
529        sm_view(k, la, ta, lb, tb, d, e, i1, j1, acc && U32.is_eq(x, y), ha, hb,
530          step_le(la, ta, d, i, k, ha, hi), step_le(lb, tb, e, j, k, hb, hj))) :
531        {_ == RHS : Bool}
532      lists_step(acc, xa, xb, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y,
533        step_val(la, ta, d, i, k, ha, hi), step_val(lb, tb, e, j, k, hb, hj),
534        step_inc(la, ta, d, i, k, ha, hi), step_inc(lb, tb, e, j, k, hb, hj))
535
536law same_pair_t:
537  for +la: U32
538  for +ta: P.Tree<U32>
539  for +lb: U32
540  for +tb: P.Tree<U32>
541  for +i: U32
542  for +j: U32
543  for +n: U32
544  {B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n) == (C.BT(la, ta), (C.BT(lb, tb), Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n))))) : D.Bytes & (D.Bytes & Bool)}
545
546def same_pair_t(la, ta, lb, tb, i, j, n):
547  sm_pair(U32.to_nat(n), la, ta, lb, tb, i, j, True{})
548
549law same_view_t:
550  for +la: U32
551  for +ta: P.Tree<U32>
552  for +lb: U32
553  for +tb: P.Tree<U32>
554  for +d: Nat
555  for +e: Nat
556  for +i: U32
557  for +j: U32
558  for +n: U32
559  for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool}
560  for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool}
561  for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(la, ta))) == True{} : Bool}
562  for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(lb, tb))) == True{} : Bool}
563  {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n))) == D.list_eq(D.slice(D.view(C.BT(la, ta)), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(C.BT(lb, tb)), U32.to_nat(j), U32.to_nat(n))) : Bool}
564
565def same_view_t(la, ta, lb, tb, d, e, i, j, n, ha, hb, hi, hj):
566  sm_view(U32.to_nat(n), la, ta, lb, tb, d, e, i, j, True{}, ha, hb, hi, hj)
567
568# same1 (two reads of one buffer per step, through at2)
569# =====================================================
570
571law at2_eq:
572  for +len: U32
573  for +t: P.Tree<U32>
574  for +i: U32
575  for +j: U32
576  {B.at2(C.BT(len, t), i, j) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)}
577
578def at2_eq(len, t, i, j):
579  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), i), (C.BT(len, t), C.AT(len, t, i)), C.at_pair_t(len, t, i)) :
580    {B.at2.fin(j, _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)}
581  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) :
582    {B.at2.fin2(C.AT(len, t, i), _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)}
583  {==}
584
585law s1_pair:
586  for +n: Nat
587  for +len: U32
588  for +t: P.Tree<U32>
589  for +i: U32
590  for +j: U32
591  for +acc: Bool
592  {B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc))) : D.Bytes & Bool}
593
594def s1_pair(n, len, t, i, j, acc):
595  match n:
596    case 0n:
597      %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) :
598        {B.same1.go(0n, _, i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(0n, _, i, j, acc))) : D.Bytes & Bool}
599      {==}
600    case 1n+m:
601      %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) :
602        {B.same1.go(1n+m, _, i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(1n+m, _, i, j, acc))) : D.Bytes & Bool}
603      s1_pair(m, len, t, (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(C.AT(len, t, i), C.AT(len, t, j)))
604
605law s1_view:
606  for +n: Nat
607  for +len: U32
608  for +t: P.Tree<U32>
609  for +d: Nat
610  for +i: U32
611  for +j: U32
612  for +acc: Bool
613  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
614  for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(len)) == True{} : Bool}
615  for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool}
616  {Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc))
617    == Bool.and(acc, D.list_eq(D.slice(D.view(C.BT(len, t)), U32.to_nat(i), n), D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n))) : Bool}
618
619def s1_view(n, len, t, d, i, j, acc, h, hi, hj):
620  match n:
621    case 0n:
622      +xs = D.view(C.BT(len, t))
623      %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) :
624        {Pair.snd(D.Bytes, Bool, B.same1.go(0n, _, i, j, acc)) == Bool.and(acc, D.list_eq(D.slice(xs, U32.to_nat(i), 0n), D.slice(xs, U32.to_nat(j), 0n))) : Bool}
625      lists_end(acc, List.drop(&2, U32, xs, U32.to_nat(i)), List.drop(&2, U32, xs, U32.to_nat(j)))
626    case 1n+k:
627      +xs = D.view(C.BT(len, t))
628      +x = C.AT(len, t, i)
629      +y = C.AT(len, t, j)
630      +i1 = (i + 1 : U32)
631      +j1 = (j + 1 : U32)
632      +RHS = Bool.and(acc, D.list_eq(D.slice(xs, U32.to_nat(i), 1n+k), D.slice(xs, U32.to_nat(j), 1n+k)))
633      %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (x, y)), at2_eq(len, t, i, j)) :
634        {Pair.snd(D.Bytes, Bool, B.same1.go(1n+k, _, i, j, acc)) == RHS : Bool}
635      %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, B.same1.go(k, B.at2(C.BT(len, t), i1, j1), i1, j1, acc && U32.is_eq(x, y))),
636        Bool.and(acc && U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(xs, U32.to_nat(j1), k))),
637        s1_view(k, len, t, d, i1, j1, acc && U32.is_eq(x, y), h,
638          step_le(len, t, d, i, k, h, hi), step_le(len, t, d, j, k, h, hj))) :
639        {_ == RHS : Bool}
640      lists_step(acc, xs, xs, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y,
641        step_val(len, t, d, i, k, h, hi), step_val(len, t, d, j, k, h, hj),
642        step_inc(len, t, d, i, k, h, hi), step_inc(len, t, d, j, k, h, hj))
643
644law same1_pair_t:
645  for +len: U32
646  for +t: P.Tree<U32>
647  for +i: U32
648  for +j: U32
649  for +n: U32
650  {B.same1(C.BT(len, t), i, j, n) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1(C.BT(len, t), i, j, n))) : D.Bytes & Bool}
651
652def same1_pair_t(len, t, i, j, n):
653  s1_pair(U32.to_nat(n), len, t, i, j, True{})
654
655law same1_view_t:
656  for +len: U32
657  for +t: P.Tree<U32>
658  for +d: Nat
659  for +i: U32
660  for +j: U32
661  for +n: U32
662  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
663  for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
664  for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
665  {Pair.snd(D.Bytes, Bool, B.same1(C.BT(len, t), i, j, n)) == D.list_eq(D.slice(D.view(C.BT(len, t)), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(C.BT(len, t)), U32.to_nat(j), U32.to_nat(n))) : Bool}
666
667def same1_view_t(len, t, d, i, j, n, h, hi, hj):
668  s1_view(U32.to_nat(n), len, t, d, i, j, True{}, h, hi, hj)