proof_find.bend

lawful-bytes@0.1.1.0 · 448 lines · 20 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# find and find2 on the mirror C.BT(len, t). The loops read one byte ahead:
15# r holds byte j + 1 while hit says whether byte j matched. Each lemma takes r
16# as a literal pair (C.BT(len, t), byte) so the loop's destructuring computes;
17# the next read is rewritten into that form with C.at_pair_t.
18
19# Small facts
20# ===========
21
22def is_some_t(m: Maybe<&2, U32>) -> Type:
23  match m:
24    case None{}:
25      Unit
26    case Some{x}:
27      Empty
28
29law none_ne_some:
30  for -x: U32
31  for e: {None{} == Some{x} : Maybe<&2, U32>}
32  Empty
33
34def none_ne_some(x, e):
35  AB.subst(Maybe<&2, U32>, m => is_some_t(m), None{}, Some{x}, e, 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 from a list with x at j leaves x in front.
49law drop_cons:
50  for +xs: List<&2, U32>
51  for +j: Nat
52  for +x: U32
53  for +hx: {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_cons(xs, j, x, hx):
57  match xs j:
58    case Nil{} _:
59      Empty.absurd({Nil{} == x <> Nil{} : List<&2, U32>}, none_ne_some(x, hx))
60    case Con{+y, t} 0n:
61      +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, hx)
62      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>}
63      %yx : {y <> t == _ <> t : List<&2, U32>}
64      {==}
65    case Con{y, t} 1n+p:
66      drop_cons(t, p, x, hx)
67
68law slice_cons:
69  for +xs: List<&2, U32>
70  for +j: Nat
71  for +k: Nat
72  for +x: U32
73  for +hx: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
74  {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
75
76def slice_cons(xs, j, k, x, hx):
77  %Equal.sym(List<&2, U32>, List.drop(&2, U32, xs, j), x <> List.drop(&2, U32, xs, Nat.add(j, 1n)), drop_cons(xs, j, x, hx)) :
78    {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
79  {==}
80
81law lt_add_succ:
82  for +a: Nat
83  for +k: Nat
84  {Nat.is_lt(a, Nat.add(a, 1n+k)) == True{} : Bool}
85
86def lt_add_succ(a, k):
87  match a:
88    case 0n:
89      {==}
90    case 1n+p:
91      lt_add_succ(p, k)
92
93# (j + 1) + 1 is j + 2, for every word j (no range needed: through from_nat).
94law add11:
95  for +j: U32
96  {U32.add(U32.add(j, 1), 1) == U32.add(j, 2) : U32}
97
98def add11(j):
99  +tj = U32.to_nat(j)
100  %U.from_nat_to_nat(j) : {U32.add(U32.add(_, 1), 1) == U32.add(j, 2) : U32}
101  %U.from_nat_add(tj, 1n) : {U32.add(_, 1) == U32.add(j, 2) : U32}
102  %U.from_nat_add(Nat.add(tj, 1n), 1n) : {_ == U32.add(j, 2) : U32}
103  %Equal.sym(Nat, Nat.add(Nat.add(tj, 1n), 1n), Nat.add(tj, Nat.add(1n, 1n)), N.add_assoc(tj, 1n, 1n)) :
104    {U32.from_nat(_) == U32.add(j, 2) : U32}
105  %U.from_nat_to_nat(j) : {U32.from_nat(Nat.add(tj, 2n)) == U32.add(_, 2) : U32}
106  U.from_nat_add(tj, 2n)
107
108# The loops hand the buffer back
109# ==============================
110
111law fgo_pair:
112  for n: Nat
113  for +hit: Bool
114  for +len: U32
115  for +t: P.Tree<U32>
116  for +x: U32
117  for +j: U32
118  for +to: U32
119  for +c: U32
120  {B.find.go(n, hit, (C.BT(len, t), x), j, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(n, hit, (C.BT(len, t), x), j, to, c))) : D.Bytes & U32}
121
122def fgo_pair(n, hit, len, t, x, j, to, c):
123  match n hit:
124    case 0n _:
125      {==}
126    case 1n+k True{}:
127      {==}
128    case 1n+k False{}:
129      +H = U32.is_eq(x, c)
130      +j2 = (j + 2 : U32)
131      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j2), (C.BT(len, t), C.AT(len, t, j2)), C.at_pair_t(len, t, j2)) :
132        {B.find.go(k, H, _, (j + 1 : U32), to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(k, H, _, (j + 1 : U32), to, c))) : D.Bytes & U32}
133      fgo_pair(k, H, len, t, C.AT(len, t, j2), (j + 1 : U32), to, c)
134
135law find_pair_t:
136  for +len: U32
137  for +t: P.Tree<U32>
138  for +from: U32
139  for +to: U32
140  for +c: U32
141  {B.find(C.BT(len, t), from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))) : D.Bytes & U32}
142
143def find_pair_t(len, t, from, to, c):
144  +n = Nat.sub(U32.to_nat(to), U32.to_nat(from))
145  +f1 = (from + 1 : U32)
146  +H = U32.is_eq(C.AT(len, t, from), c)
147  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
148    {B.find.start(n, _, from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.start(n, _, from, to, c))) : D.Bytes & U32}
149  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
150    {B.find.go(n, H, _, from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(n, H, _, from, to, c))) : D.Bytes & U32}
151  fgo_pair(n, H, len, t, C.AT(len, t, f1), from, to, c)
152
153law fgo2_pair:
154  for n: Nat
155  for +hit: Bool
156  for +len: U32
157  for +t: P.Tree<U32>
158  for +x: U32
159  for +j: U32
160  for +to: U32
161  for +c1: U32
162  for +c2: U32
163  {B.find2.go(n, hit, (C.BT(len, t), x), j, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(n, hit, (C.BT(len, t), x), j, to, c1, c2))) : D.Bytes & U32}
164
165def fgo2_pair(n, hit, len, t, x, j, to, c1, c2):
166  match n hit:
167    case 0n _:
168      {==}
169    case 1n+k True{}:
170      {==}
171    case 1n+k False{}:
172      +H = U32.is_eq(x, c1) || U32.is_eq(x, c2)
173      +j2 = (j + 2 : U32)
174      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j2), (C.BT(len, t), C.AT(len, t, j2)), C.at_pair_t(len, t, j2)) :
175        {B.find2.go(k, H, _, (j + 1 : U32), to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(k, H, _, (j + 1 : U32), to, c1, c2))) : D.Bytes & U32}
176      fgo2_pair(k, H, len, t, C.AT(len, t, j2), (j + 1 : U32), to, c1, c2)
177
178law find2_pair_t:
179  for +len: U32
180  for +t: P.Tree<U32>
181  for +from: U32
182  for +to: U32
183  for +c1: U32
184  for +c2: U32
185  {B.find2(C.BT(len, t), from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))) : D.Bytes & U32}
186
187def find2_pair_t(len, t, from, to, c1, c2):
188  +n = Nat.sub(U32.to_nat(to), U32.to_nat(from))
189  +f1 = (from + 1 : U32)
190  +x0 = C.AT(len, t, from)
191  +H = U32.is_eq(x0, c1) || U32.is_eq(x0, c2)
192  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), x0), C.at_pair_t(len, t, from)) :
193    {B.find2.start(n, _, from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.start(n, _, from, to, c1, c2))) : D.Bytes & U32}
194  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
195    {B.find2.go(n, H, _, from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(n, H, _, from, to, c1, c2))) : D.Bytes & U32}
196  fgo2_pair(n, H, len, t, C.AT(len, t, f1), from, to, c1, c2)
197
198# Index steps
199# ===========
200
201# With j + 1 + k = to <= len, byte j is in range.
202law step_lt:
203  for +len: U32
204  for +j: U32
205  for +to: U32
206  for +k: Nat
207  for +hn: {Nat.add(U32.to_nat(j), 1n+k) == U32.to_nat(to) : Nat}
208  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
209  {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
210
211def step_lt(len, j, to, k, hn, hto):
212  +tj = U32.to_nat(j)
213  N.lt_le_trans(tj, U32.to_nat(to), U32.to_nat(len),
214    AB.subst(Nat, x => {Nat.is_lt(tj, x) == True{} : Bool}, Nat.add(tj, 1n+k), U32.to_nat(to), hn, lt_add_succ(tj, k)),
215    hto)
216
217law step_lt4:
218  for +len: U32
219  for +t: P.Tree<U32>
220  for +d: Nat
221  for +j: U32
222  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
223  for +hj: {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
224  {Nat.is_lt(U32.to_nat(j), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
225
226def step_lt4(len, t, d, j, h, hj):
227  N.lt_le_trans(U32.to_nat(j), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hj, C.ok_len(len, t, d, h))
228
229law step_get:
230  for +len: U32
231  for +t: P.Tree<U32>
232  for +d: Nat
233  for +j: U32
234  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
235  for +hj: {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
236  {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)) == Some{C.AT(len, t, j)} : Maybe<&2, U32>}
237
238def step_get(len, t, d, j, h, hj):
239  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)),
240    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), hj))
241
242law step_n:
243  for +j: U32
244  for +k: Nat
245  for +to: U32
246  for +d: Nat
247  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
248  for +hj4: {Nat.is_lt(U32.to_nat(j), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
249  for +hn: {Nat.add(U32.to_nat(j), 1n+k) == U32.to_nat(to) : Nat}
250  {Nat.add(U32.to_nat((j + 1 : U32)), k) == U32.to_nat(to) : Nat}
251
252def step_n(j, k, to, d, hd, hj4, hn):
253  +tj = U32.to_nat(j)
254  %Equal.sym(Nat, U32.to_nat((j + 1 : U32)), Nat.add(tj, 1n), C.inc_fits(j, d, hd, hj4)) :
255    {Nat.add(_, k) == U32.to_nat(to) : Nat}
256  %Equal.sym(Nat, Nat.add(Nat.add(tj, 1n), k), Nat.add(tj, Nat.add(1n, k)), N.add_assoc(tj, 1n, k)) :
257    {_ == U32.to_nat(to) : Nat}
258  hn
259
260# find
261# ====
262
263# hit says byte j is c, r holds byte j + 1, j + n = to.
264law fgo_view:
265  for +n: Nat
266  for +hit: Bool
267  for +len: U32
268  for +t: P.Tree<U32>
269  for +d: Nat
270  for +j: U32
271  for +to: U32
272  for +c: U32
273  for +hh: {U32.is_eq(C.AT(len, t, j), c) == hit : Bool}
274  for +hn: {Nat.add(U32.to_nat(j), n) == U32.to_nat(to) : Nat}
275  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
276  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
277  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(n, hit, (C.BT(len, t), C.AT(len, t, (j + 1 : U32))), j, to, c))) == Nat.add(U32.to_nat(j), D.run_len(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n), c)) : Nat}
278
279def fgo_view(n, hit, len, t, d, j, to, c, hh, hn, hto, h):
280  match n hit:
281    case 0n _:
282      +tj = U32.to_nat(j)
283      %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), tj), 0n), Nil{},
284        Q.take_zero(List.drop(&2, U32, D.view(C.BT(len, t)), tj))) :
285        {U32.to_nat(to) == Nat.add(tj, D.run_len(_, c)) : Nat}
286      Equal.sym(Nat, Nat.add(tj, 0n), U32.to_nat(to), hn)
287    case 1n+k True{}:
288      +tj = U32.to_nat(j)
289      +VW = D.view(C.BT(len, t))
290      +x = C.AT(len, t, j)
291      +S = D.slice(VW, Nat.add(tj, 1n), k)
292      +hj = step_lt(len, j, to, k, hn, hto)
293      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
294        {tj == Nat.add(tj, D.run_len(_, c)) : Nat}
295      %Equal.sym(Bool, U32.is_eq(x, c), True{}, hh) :
296        {tj == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(S, c)))) : Nat}
297      Equal.sym(Nat, Nat.add(tj, 0n), tj, AB.add_zero(tj))
298    case 1n+k False{}:
299      +tj = U32.to_nat(j)
300      +VW = D.view(C.BT(len, t))
301      +x = C.AT(len, t, j)
302      +S = D.slice(VW, Nat.add(tj, 1n), k)
303      +j1 = (j + 1 : U32)
304      +j11 = (j1 + 1 : U32)
305      +H1 = U32.is_eq(C.AT(len, t, j1), c)
306      +RHS = Nat.add(tj, D.run_len(D.slice(VW, tj, 1n+k), c))
307      +hd = C.ok_d(len, t, d, h)
308      +hj = step_lt(len, j, to, k, hn, hto)
309      +hj4 = step_lt4(len, t, d, j, h, hj)
310      %add11(j) : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, B.at(C.BT(len, t), _), j1, to, c))) == RHS : Nat}
311      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j11), (C.BT(len, t), C.AT(len, t, j11)), C.at_pair_t(len, t, j11)) :
312        {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, _, j1, to, c))) == RHS : Nat}
313      +G = U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, (C.BT(len, t), C.AT(len, t, j11)), j1, to, c)))
314      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
315        {G == Nat.add(tj, D.run_len(_, c)) : Nat}
316      %Equal.sym(Bool, U32.is_eq(x, c), False{}, hh) :
317        {G == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(S, c)))) : Nat}
318      %N.add_assoc(tj, 1n, D.run_len(S, c)) : {G == _ : Nat}
319      %C.inc_fits(j, d, hd, hj4) : {G == Nat.add(_, D.run_len(D.slice(VW, _, k), c)) : Nat}
320      fgo_view(k, H1, len, t, d, j1, to, c, {==}, step_n(j, k, to, d, hd, hj4, hn), hto, h)
321
322# from <= to as numbers.
323law le_ft:
324  for +from: U32
325  for +to: U32
326  for +hft: {U32.is_le(from, to) == True{} : Bool}
327  {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
328
329def le_ft(from, to, hft):
330  Equal.trans(Bool, Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U32.is_le(from, to), True{},
331    Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U.is_le_to_nat(from, to)), hft)
332
333law find_view_t:
334  for +len: U32
335  for +t: P.Tree<U32>
336  for +d: Nat
337  for +from: U32
338  for +to: U32
339  for +c: U32
340  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
341  for +hft: {U32.is_le(from, to) == True{} : Bool}
342  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
343  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
344  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
345
346def find_view_t(len, t, d, from, to, c, h, hft, ht, hc):
347  +tf = U32.to_nat(from)
348  +tt = U32.to_nat(to)
349  +n = Nat.sub(tt, tf)
350  +f1 = (from + 1 : U32)
351  +H = U32.is_eq(C.AT(len, t, from), c)
352  +RHS = D.first(D.view(C.BT(len, t)), tf, tt, c)
353  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
354    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.start(n, _, from, to, c))) == RHS : Nat}
355  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
356    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(n, H, _, from, to, c))) == RHS : Nat}
357  fgo_view(n, H, len, t, d, from, to, c, {==}, N.le_sub_add(tf, tt, le_ft(from, to, hft)), ht, h)
358
359# find2
360# =====
361
362# hit says byte j is c1 or c2, r holds byte j + 1, j + n = to.
363law fgo2_view:
364  for +n: Nat
365  for +hit: Bool
366  for +len: U32
367  for +t: P.Tree<U32>
368  for +d: Nat
369  for +j: U32
370  for +to: U32
371  for +c1: U32
372  for +c2: U32
373  for +hh: {(U32.is_eq(C.AT(len, t, j), c1) || U32.is_eq(C.AT(len, t, j), c2)) == hit : Bool}
374  for +hn: {Nat.add(U32.to_nat(j), n) == U32.to_nat(to) : Nat}
375  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
376  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
377  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(n, hit, (C.BT(len, t), C.AT(len, t, (j + 1 : U32))), j, to, c1, c2))) == Nat.add(U32.to_nat(j), D.run_len2(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n), c1, c2)) : Nat}
378
379def fgo2_view(n, hit, len, t, d, j, to, c1, c2, hh, hn, hto, h):
380  match n hit:
381    case 0n _:
382      +tj = U32.to_nat(j)
383      %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), tj), 0n), Nil{},
384        Q.take_zero(List.drop(&2, U32, D.view(C.BT(len, t)), tj))) :
385        {U32.to_nat(to) == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
386      Equal.sym(Nat, Nat.add(tj, 0n), U32.to_nat(to), hn)
387    case 1n+k True{}:
388      +tj = U32.to_nat(j)
389      +VW = D.view(C.BT(len, t))
390      +x = C.AT(len, t, j)
391      +S = D.slice(VW, Nat.add(tj, 1n), k)
392      +hj = step_lt(len, j, to, k, hn, hto)
393      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
394        {tj == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
395      %Equal.sym(Bool, U32.is_eq(x, c1) || U32.is_eq(x, c2), True{}, hh) :
396        {tj == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(S, c1, c2)))) : Nat}
397      Equal.sym(Nat, Nat.add(tj, 0n), tj, AB.add_zero(tj))
398    case 1n+k False{}:
399      +tj = U32.to_nat(j)
400      +VW = D.view(C.BT(len, t))
401      +x = C.AT(len, t, j)
402      +S = D.slice(VW, Nat.add(tj, 1n), k)
403      +j1 = (j + 1 : U32)
404      +j11 = (j1 + 1 : U32)
405      +H1 = U32.is_eq(C.AT(len, t, j1), c1) || U32.is_eq(C.AT(len, t, j1), c2)
406      +RHS = Nat.add(tj, D.run_len2(D.slice(VW, tj, 1n+k), c1, c2))
407      +hd = C.ok_d(len, t, d, h)
408      +hj = step_lt(len, j, to, k, hn, hto)
409      +hj4 = step_lt4(len, t, d, j, h, hj)
410      %add11(j) : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, B.at(C.BT(len, t), _), j1, to, c1, c2))) == RHS : Nat}
411      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j11), (C.BT(len, t), C.AT(len, t, j11)), C.at_pair_t(len, t, j11)) :
412        {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, _, j1, to, c1, c2))) == RHS : Nat}
413      +G = U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, (C.BT(len, t), C.AT(len, t, j11)), j1, to, c1, c2)))
414      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
415        {G == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
416      %Equal.sym(Bool, U32.is_eq(x, c1) || U32.is_eq(x, c2), False{}, hh) :
417        {G == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(S, c1, c2)))) : Nat}
418      %N.add_assoc(tj, 1n, D.run_len2(S, c1, c2)) : {G == _ : Nat}
419      %C.inc_fits(j, d, hd, hj4) : {G == Nat.add(_, D.run_len2(D.slice(VW, _, k), c1, c2)) : Nat}
420      fgo2_view(k, H1, len, t, d, j1, to, c1, c2, {==}, step_n(j, k, to, d, hd, hj4, hn), hto, h)
421
422law find2_view_t:
423  for +len: U32
424  for +t: P.Tree<U32>
425  for +d: Nat
426  for +from: U32
427  for +to: U32
428  for +c1: U32
429  for +c2: U32
430  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
431  for +hft: {U32.is_le(from, to) == True{} : Bool}
432  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
433  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
434  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
435  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
436
437def find2_view_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
438  +tf = U32.to_nat(from)
439  +tt = U32.to_nat(to)
440  +n = Nat.sub(tt, tf)
441  +f1 = (from + 1 : U32)
442  +H = U32.is_eq(C.AT(len, t, from), c1) || U32.is_eq(C.AT(len, t, from), c2)
443  +RHS = D.first2(D.view(C.BT(len, t)), tf, tt, c1, c2)
444  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
445    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.start(n, _, from, to, c1, c2))) == RHS : Nat}
446  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
447    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(n, H, _, from, to, c1, c2))) == RHS : Nat}
448  fgo2_view(n, H, len, t, d, from, to, c1, c2, {==}, N.le_sub_add(tf, tt, le_ft(from, to, hft)), ht, h)