proof_same.bend
lawful-bytes@0.1.0.0 · 510 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-words@0.1.0.0/defs.bend as W
7import lawful-words@0.1.0.0/proof_nat.bend as N
8import lawful-arrays@0.1.0.0/defs.bend as A
9import lawful-arrays@0.1.0.0/proof_base.bend as AB
10import lawful-arrays@0.1.0.0/proof_tree.bend as P
11import lawful-arrays@0.1.0.0/proof_index.bend as I
12
13# The reading loops: to_list, same and same1, on the mirror C.BT(len, t)
14# (law-shaped, as in proof_ops.bend). Each loop carries the read pair
15# B.at(BT, s) literally: C.at_pair_t turns it into (BT, AT) so the loop steps,
16# and the next call reads B.at(BT, s + 1), the same form one index on.
17
18# List and index facts
19# ====================
20
21def mdisc(m: Maybe<&2, U32>) -> Type:
22 match m:
23 case None{}:
24 Empty
25 case Some{x}:
26 Unit
27
28law none_some:
29 for -x: U32
30 for e: {None{} == Some{x} : Maybe<&2, U32>}
31 Empty
32
33def none_some(x, e):
34 %Equal.sym(Maybe<&2, U32>, None{}, Some{x}, e) : mdisc(_)
35 Unit{}
36
37law drop_zero:
38 for +xs: List<&2, U32>
39 {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>}
40
41def drop_zero(xs):
42 match xs:
43 case Nil{}:
44 {==}
45 case Con{x, t}:
46 {==}
47
48# Dropping j elements, when element j is x: x, then the rest.
49law drop_get:
50 for +xs: List<&2, U32>
51 for +j: Nat
52 for +x: U32
53 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
54 {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}
55
56def drop_get(xs, j, x, h):
57 match xs j:
58 case Nil{} _:
59 Empty.absurd({List.drop(&2, U32, Nil{}, j) == x <> List.drop(&2, U32, Nil{}, Nat.add(j, 1n)) : List<&2, U32>},
60 none_some(x, h))
61 case Con{+y, t} 0n:
62 +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h)
63 %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>}
64 %Equal.sym(U32, y, x, yx) : {_ <> t == x <> t : List<&2, U32>}
65 {==}
66 case Con{y, t} 1n+p:
67 drop_get(t, p, x, h)
68
69law slice_cons:
70 for +xs: List<&2, U32>
71 for +j: Nat
72 for +k: Nat
73 for +x: U32
74 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
75 {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
76
77def slice_cons(xs, j, k, x, h):
78 %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)) :
79 {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
80 {==}
81
82# a + 1 + m <= b gives a < b.
83law lt_of_le:
84 for +a: Nat
85 for +m: Nat
86 for +b: Nat
87 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
88 {Nat.is_lt(a, b) == True{} : Bool}
89
90def lt_of_le(a, m, b, h):
91 +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)
92 +h2 = N.le_trans(1n+a, 1n+Nat.add(a, m), b, N.le_add_r(a, m), h1)
93 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)
94
95# a + 1 + m <= b gives (a + 1) + m <= b.
96law le_step:
97 for +a: Nat
98 for +m: Nat
99 for +b: Nat
100 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
101 {Nat.is_le(Nat.add(Nat.add(a, 1n), m), b) == True{} : Bool}
102
103def le_step(a, m, b, h):
104 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),
105 Equal.sym(Nat, Nat.add(Nat.add(a, 1n), m), Nat.add(a, Nat.add(1n, m)), N.add_assoc(a, 1n, m)), h)
106
107# One step of a read loop at index s with n + 1 left, within a Bytes of size len:
108# byte s is read, s + 1 does not wrap, and the bound holds one index on.
109law step_val:
110 for +len: U32
111 for +t: P.Tree<U32>
112 for +d: Nat
113 for +s: U32
114 for +m: Nat
115 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
116 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
117 {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)) == Some{C.AT(len, t, s)} : Maybe<&2, U32>}
118
119def step_val(len, t, d, s, m, h, hs):
120 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)),
121 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),
122 lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs)))
123
124law step_inc:
125 for +len: U32
126 for +t: P.Tree<U32>
127 for +d: Nat
128 for +s: U32
129 for +m: Nat
130 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
131 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
132 {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat}
133
134def step_inc(len, t, d, s, m, h, hs):
135 C.inc_fits(s, d, C.ok_d(len, t, d, h),
136 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),
137 C.ok_len(len, t, d, h)))
138
139law step_le:
140 for +len: U32
141 for +t: P.Tree<U32>
142 for +d: Nat
143 for +s: U32
144 for +m: Nat
145 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
146 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool}
147 {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), m), U32.to_nat(len)) == True{} : Bool}
148
149def step_le(len, t, d, s, m, h, hs):
150 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)),
151 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)),
152 le_step(U32.to_nat(s), m, U32.to_nat(len), hs))
153
154# to_list
155# =======
156
157law tl_pair:
158 for +n: Nat
159 for +len: U32
160 for +t: P.Tree<U32>
161 for +s: U32
162 {B.to_list.go(n, B.at(C.BT(len, t), s), s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), s), s))) : D.Bytes & List<&2, U32>}
163
164def tl_pair(n, len, t, s):
165 match n:
166 case 0n:
167 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), C.AT(len, t, s)), C.at_pair_t(len, t, s)) :
168 {B.to_list.go(0n, _, s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, s))) : D.Bytes & List<&2, U32>}
169 {==}
170 case 1n+m:
171 +s1 = (s + 1 : U32)
172 +x = C.AT(len, t, s)
173 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), x), C.at_pair_t(len, t, s)) :
174 {B.to_list.go(1n+m, _, s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, s))) : D.Bytes & List<&2, U32>}
175 %Equal.sym(D.Bytes & List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1),
176 (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1))), tl_pair(m, len, t, s1)) :
177 {B.to_list.cons(x, _) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.cons(x, _))) : D.Bytes & List<&2, U32>}
178 {==}
179
180law tl_view:
181 for +n: Nat
182 for +len: U32
183 for +t: P.Tree<U32>
184 for +d: Nat
185 for +s: U32
186 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
187 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), n), U32.to_nat(len)) == True{} : Bool}
188 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), s), s)) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), n) : List<&2, U32>}
189
190def tl_view(n, len, t, d, s, h, hs):
191 match n:
192 case 0n:
193 +X = List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s))
194 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), C.AT(len, t, s)), C.at_pair_t(len, t, s)) :
195 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, s)) == List.take(&2, U32, X, 0n) : List<&2, U32>}
196 Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X))
197 case 1n+m:
198 +s1 = (s + 1 : U32)
199 +x = C.AT(len, t, s)
200 +xs = D.view(C.BT(len, t))
201 +G = Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1))
202 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), x), C.at_pair_t(len, t, s)) :
203 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, s)) == D.slice(xs, U32.to_nat(s), 1n+m) : List<&2, U32>}
204 %Equal.sym(D.Bytes & List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1), (C.BT(len, t), G), tl_pair(m, len, t, s1)) :
205 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.cons(x, _)) == D.slice(xs, U32.to_nat(s), 1n+m) : List<&2, U32>}
206 %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 1n+m), x <> D.slice(xs, Nat.add(U32.to_nat(s), 1n), m),
207 slice_cons(xs, U32.to_nat(s), m, x, step_val(len, t, d, s, m, h, hs))) :
208 {x <> G == _ : List<&2, U32>}
209 %step_inc(len, t, d, s, m, h, hs) : {x <> G == x <> D.slice(xs, _, m) : List<&2, U32>}
210 %tl_view(m, len, t, d, s1, h, step_le(len, t, d, s, m, h, hs)) : {x <> G == x <> _ : List<&2, U32>}
211 {==}
212
213law to_list_pair_t:
214 for +len: U32
215 for +t: P.Tree<U32>
216 for +s: U32
217 for +n: U32
218 {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>}
219
220def to_list_pair_t(len, t, s, n):
221 tl_pair(U32.to_nat(n), len, t, s)
222
223law to_list_view_t:
224 for +len: U32
225 for +t: P.Tree<U32>
226 for +d: Nat
227 for +s: U32
228 for +n: U32
229 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
230 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
231 {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>}
232
233def to_list_view_t(len, t, d, s, n, h, hs):
234 tl_view(U32.to_nat(n), len, t, d, s, h, hs)
235
236# same
237# ====
238
239law and_assoc:
240 for +a: Bool
241 for +b: Bool
242 for +c: Bool
243 {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
244
245def and_assoc(a, b, c):
246 match a:
247 case False{}:
248 {==}
249 case True{}:
250 {==}
251
252# Comparing n more bytes from i of A and from j of B, after an empty prefix:
253# acc and the comparison of the two slices.
254law lists_end:
255 for +acc: Bool
256 for +xs: List<&2, U32>
257 for +ys: List<&2, U32>
258 {acc == Bool.and(acc, D.list_eq(List.take(&2, U32, xs, 0n), List.take(&2, U32, ys, 0n))) : Bool}
259
260def lists_end(acc, xs, ys):
261 %Equal.sym(List<&2, U32>, List.take(&2, U32, xs, 0n), Nil{}, Q.take_zero(xs)) :
262 {acc == Bool.and(acc, D.list_eq(_, List.take(&2, U32, ys, 0n))) : Bool}
263 %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) :
264 {acc == Bool.and(acc, D.list_eq(Nil{}, _)) : Bool}
265 Equal.sym(Bool, Bool.and(acc, True{}), acc, N.and_true_r_id(acc))
266
267# One step of a comparison loop: the two slices from x and y, with the
268# accumulated test rebracketed.
269law lists_step:
270 for +acc: Bool
271 for +xs: List<&2, U32>
272 for +ys: List<&2, U32>
273 for +i: Nat
274 for +j: Nat
275 for +i1: U32
276 for +j1: U32
277 for +k: Nat
278 for +x: U32
279 for +y: U32
280 for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
281 for +hy: {List.get(&2, U32, ys, j) == Some{y} : Maybe<&2, U32>}
282 for +ei: {U32.to_nat(i1) == Nat.add(i, 1n) : Nat}
283 for +ej: {U32.to_nat(j1) == Nat.add(j, 1n) : Nat}
284 {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)))
285 == Bool.and(acc, D.list_eq(D.slice(xs, i, 1n+k), D.slice(ys, j, 1n+k))) : Bool}
286
287def lists_step(acc, xs, ys, i, j, i1, j1, k, x, y, hx, hy, ei, ej):
288 +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)))
289 %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)) :
290 {LHS == Bool.and(acc, D.list_eq(_, D.slice(ys, j, 1n+k))) : Bool}
291 %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)) :
292 {LHS == Bool.and(acc, D.list_eq(x <> D.slice(xs, Nat.add(i, 1n), k), _)) : Bool}
293 %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}
294 %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}
295 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)))
296
297law sm_pair:
298 for +n: Nat
299 for +la: U32
300 for +ta: P.Tree<U32>
301 for +lb: U32
302 for +tb: P.Tree<U32>
303 for +i: U32
304 for +j: U32
305 for +acc: Bool
306 {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),
307 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)}
308
309def sm_pair(n, la, ta, lb, tb, i, j, acc):
310 match n:
311 case 0n:
312 %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)) :
313 {B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
314 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)}
315 %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)) :
316 {B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
317 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)}
318 {==}
319 case 1n+k:
320 %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)) :
321 {B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb),
322 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)}
323 %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)) :
324 {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),
325 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)}
326 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)))
327
328law sm_view:
329 for +n: Nat
330 for +la: U32
331 for +ta: P.Tree<U32>
332 for +lb: U32
333 for +tb: P.Tree<U32>
334 for +d: Nat
335 for +e: Nat
336 for +i: U32
337 for +j: U32
338 for +acc: Bool
339 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool}
340 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool}
341 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(la)) == True{} : Bool}
342 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(lb)) == True{} : Bool}
343 {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)))
344 == 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}
345
346def sm_view(n, la, ta, lb, tb, d, e, i, j, acc, ha, hb, hi, hj):
347 match n:
348 case 0n:
349 +xa = D.view(C.BT(la, ta))
350 +xb = D.view(C.BT(lb, tb))
351 +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 0n), D.slice(xb, U32.to_nat(j), 0n)))
352 %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)) :
353 {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}
354 %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)) :
355 {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}
356 lists_end(acc, List.drop(&2, U32, xa, U32.to_nat(i)), List.drop(&2, U32, xb, U32.to_nat(j)))
357 case 1n+k:
358 +xa = D.view(C.BT(la, ta))
359 +xb = D.view(C.BT(lb, tb))
360 +x = C.AT(la, ta, i)
361 +y = C.AT(lb, tb, j)
362 +i1 = (i + 1 : U32)
363 +j1 = (j + 1 : U32)
364 +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)))
365 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), x), C.at_pair_t(la, ta, i)) :
366 {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}
367 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), y), C.at_pair_t(lb, tb, j)) :
368 {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}
369 %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)))),
370 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))),
371 sm_view(k, la, ta, lb, tb, d, e, i1, j1, acc && U32.is_eq(x, y), ha, hb,
372 step_le(la, ta, d, i, k, ha, hi), step_le(lb, tb, e, j, k, hb, hj))) :
373 {_ == RHS : Bool}
374 lists_step(acc, xa, xb, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y,
375 step_val(la, ta, d, i, k, ha, hi), step_val(lb, tb, e, j, k, hb, hj),
376 step_inc(la, ta, d, i, k, ha, hi), step_inc(lb, tb, e, j, k, hb, hj))
377
378law same_pair_t:
379 for +la: U32
380 for +ta: P.Tree<U32>
381 for +lb: U32
382 for +tb: P.Tree<U32>
383 for +i: U32
384 for +j: U32
385 for +n: U32
386 {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)}
387
388def same_pair_t(la, ta, lb, tb, i, j, n):
389 sm_pair(U32.to_nat(n), la, ta, lb, tb, i, j, True{})
390
391law same_view_t:
392 for +la: U32
393 for +ta: P.Tree<U32>
394 for +lb: U32
395 for +tb: P.Tree<U32>
396 for +d: Nat
397 for +e: Nat
398 for +i: U32
399 for +j: U32
400 for +n: U32
401 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool}
402 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool}
403 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(la, ta))) == True{} : Bool}
404 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(lb, tb))) == True{} : Bool}
405 {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}
406
407def same_view_t(la, ta, lb, tb, d, e, i, j, n, ha, hb, hi, hj):
408 sm_view(U32.to_nat(n), la, ta, lb, tb, d, e, i, j, True{}, ha, hb, hi, hj)
409
410# same1 (two reads of one buffer per step, through at2)
411# =====================================================
412
413law at2_eq:
414 for +len: U32
415 for +t: P.Tree<U32>
416 for +i: U32
417 for +j: U32
418 {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)}
419
420def at2_eq(len, t, i, j):
421 %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)) :
422 {B.at2.fin(j, _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)}
423 %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)) :
424 {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)}
425 {==}
426
427law s1_pair:
428 for +n: Nat
429 for +len: U32
430 for +t: P.Tree<U32>
431 for +i: U32
432 for +j: U32
433 for +acc: Bool
434 {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}
435
436def s1_pair(n, len, t, i, j, acc):
437 match n:
438 case 0n:
439 %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)) :
440 {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}
441 {==}
442 case 1n+m:
443 %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)) :
444 {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}
445 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)))
446
447law s1_view:
448 for +n: Nat
449 for +len: U32
450 for +t: P.Tree<U32>
451 for +d: Nat
452 for +i: U32
453 for +j: U32
454 for +acc: Bool
455 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
456 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(len)) == True{} : Bool}
457 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool}
458 {Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc))
459 == 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}
460
461def s1_view(n, len, t, d, i, j, acc, h, hi, hj):
462 match n:
463 case 0n:
464 +xs = D.view(C.BT(len, t))
465 %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)) :
466 {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}
467 lists_end(acc, List.drop(&2, U32, xs, U32.to_nat(i)), List.drop(&2, U32, xs, U32.to_nat(j)))
468 case 1n+k:
469 +xs = D.view(C.BT(len, t))
470 +x = C.AT(len, t, i)
471 +y = C.AT(len, t, j)
472 +i1 = (i + 1 : U32)
473 +j1 = (j + 1 : U32)
474 +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)))
475 %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)) :
476 {Pair.snd(D.Bytes, Bool, B.same1.go(1n+k, _, i, j, acc)) == RHS : Bool}
477 %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))),
478 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))),
479 s1_view(k, len, t, d, i1, j1, acc && U32.is_eq(x, y), h,
480 step_le(len, t, d, i, k, h, hi), step_le(len, t, d, j, k, h, hj))) :
481 {_ == RHS : Bool}
482 lists_step(acc, xs, xs, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y,
483 step_val(len, t, d, i, k, h, hi), step_val(len, t, d, j, k, h, hj),
484 step_inc(len, t, d, i, k, h, hi), step_inc(len, t, d, j, k, h, hj))
485
486law same1_pair_t:
487 for +len: U32
488 for +t: P.Tree<U32>
489 for +i: U32
490 for +j: U32
491 for +n: U32
492 {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}
493
494def same1_pair_t(len, t, i, j, n):
495 s1_pair(U32.to_nat(n), len, t, i, j, True{})
496
497law same1_view_t:
498 for +len: U32
499 for +t: P.Tree<U32>
500 for +d: Nat
501 for +i: U32
502 for +j: U32
503 for +n: U32
504 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
505 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
506 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool}
507 {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}
508
509def same1_view_t(len, t, d, i, j, n, h, hi, hj):
510 s1_view(U32.to_nat(n), len, t, d, i, j, True{}, h, hi, hj)