proof_fast_find.bend

lawful-bytes@0.1.1.0 · 1,064 lines · 52 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/fast.bend as FA
5import lawful-bytes@0.1.1.0/proof_seq.bend as Q
6import lawful-bytes@0.1.1.0/proof_core.bend as C
7import lawful-bytes@0.1.1.0/proof_find.bend as F
8import lawful-bytes@0.1.1.0/proof_append.bend as X
9import lawful-bytes@0.1.1.0/proof_shift.bend as H
10import lawful-bytes@0.1.1.0/proof_fast_word.bend as FW
11import lawful-words@0.1.0.0/defs.bend as W
12import lawful-words@0.1.0.0/proof_nat.bend as N
13import lawful-words@0.1.0.0/proof_u32.bend as U
14import lawful-arrays@0.1.0.0/proof_base.bend as AB
15import lawful-arrays@0.1.0.0/proof_tree.bend as P
16import lawful-arrays@0.1.0.0/defs.bend as A
17
18# fast.bend's find on the mirror C.BT(len, t). FG is find.go as a function of
19# the tree (fg_eq): the word loop answers the offset of the first flagged byte,
20# or 4294967295; find.fin takes the min with to. The word facts (what the
21# flags and bidx say) are in proof_fast_word.bend.
22
23def FG(n: Nat, z: Bool, +wi: U32, +m: U32, +rc: U32, +t: P.Tree<U32>) -> U32:
24  match n z:
25    case 0n _:
26      4294967295
27    case 1n+k True{}:
28      +m2 = FA.zb((C.WD(t, (wi + 1 : U32)) .^. rc : U32))
29      FG(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)
30    case 1n+k False{}:
31      ((wi << 2n : U32) + FA.bidx(m) : U32)
32
33law fg_eq:
34  for +n: Nat
35  for +z: Bool
36  for +wi: U32
37  for +m: U32
38  for +rc: U32
39  for +t: P.Tree<U32>
40  {FA.find.go(n, z, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), wi, m, rc) == (P.fromT(U32, t), FG(n, z, wi, m, rc, t)) : Array<U32> & U32}
41
42def fg_eq(n, z, wi, m, rc, t):
43  match n z:
44    case 0n _:
45      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
46        {FA.find.go(0n, z, _, wi, m, rc) == (P.fromT(U32, t), FG(0n, z, wi, m, rc, t)) : Array<U32> & U32}
47      {==}
48    case 1n+k True{}:
49      +m2 = FA.zb((C.WD(t, (wi + 1 : U32)) .^. rc : U32))
50      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
51        {FA.find.go(1n+k, True{}, _, wi, m, rc) == (P.fromT(U32, t), FG(1n+k, True{}, wi, m, rc, t)) : Array<U32> & U32}
52      %F.add11(wi) :
53        {FA.find.go(k, U32.is_zero(m2), Array.get(U32, P.fromT(U32, t), _), (wi + 1 : U32), m2, rc) == (P.fromT(U32, t), FG(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)) : Array<U32> & U32}
54      fg_eq(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)
55    case 1n+k False{}:
56      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
57        {FA.find.go(1n+k, False{}, _, wi, m, rc) == (P.fromT(U32, t), FG(1n+k, False{}, wi, m, rc, t)) : Array<U32> & U32}
58      {==}
59
60# The mask of the first word.
61def M0(+t: P.Tree<U32>, +from: U32, +rc: U32) -> U32:
62  FA.zb(((C.WD(t, (from >> 2n : U32)) .^. rc : U32) .|. U32.not(FA.low(from)) : U32))
63
64# fast find on the mirror: the same Bytes, and the min of the loop's answer with to.
65law fast_eq:
66  for +len: U32
67  for +t: P.Tree<U32>
68  for +from: U32
69  for +to: U32
70  for +c: U32
71  {FA.find(C.BT(len, t), from, to, c) == (C.BT(len, t), U32.min(FG(FA.words(from, to), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) : D.Bytes & U32}
72
73def fast_eq(len, t, from, to, c):
74  +k = (from >> 2n : U32)
75  +rc = FA.rep(c)
76  +n = FA.words(from, to)
77  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), C.WD(t, k)), P.get_pair_t(U32, t, k)) :
78    {FA.find.k(len, FA.find.fin(to, FA.find.start(n, _, from, rc))) == (C.BT(len, t), U32.min(FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t), to)) : D.Bytes & U32}
79  %Equal.sym(Array<U32> & U32, FA.find.go(n, U32.is_zero(M0(t, from, rc)), Array.get(U32, P.fromT(U32, t), (k + 1 : U32)), k, M0(t, from, rc), rc),
80    (P.fromT(U32, t), FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t)), fg_eq(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t)) :
81    {FA.find.k(len, FA.find.fin(to, _)) == (C.BT(len, t), U32.min(FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t), to)) : D.Bytes & U32}
82  {==}
83
84# Lists
85# =====
86
87law drop_append_l:
88  for +xs: List<&2, U32>
89  for +ys: List<&2, U32>
90  for +o: Nat
91  for +h: {Nat.is_le(o, List.length(&2, U32, xs)) == True{} : Bool}
92  {List.drop(&2, U32, List.append(&2, U32, xs, ys), o) == List.append(&2, U32, List.drop(&2, U32, xs, o), ys) : List<&2, U32>}
93
94def drop_append_l(xs, ys, o, h):
95  match xs o:
96    case Nil{} 0n:
97      X.drop_zero(ys)
98    case Nil{} 1n+p:
99      Empty.absurd({List.drop(&2, U32, ys, 1n+p) == ys : List<&2, U32>}, AB.false_ne_true(h))
100    case Con{x, t} 0n:
101      {==}
102    case Con{x, t} 1n+p:
103      drop_append_l(t, ys, p, h)
104
105law drop_unpack:
106  for +ws: List<&2, U32>
107  for +q: Nat
108  {List.drop(&2, U32, D.unpack(ws), Nat.mul(q, 4n)) == D.unpack(List.drop(&2, U32, ws, q)) : List<&2, U32>}
109
110def drop_unpack(ws, q):
111  match ws q:
112    case Nil{} _:
113      {==}
114    case Con{x, t} 0n:
115      X.drop_zero(D.unpack(Con{x, t}))
116    case Con{x, t} 1n+p:
117      drop_unpack(t, p)
118
119# Byte 4q + o onwards: the rest of word q, then the words after it.
120law drop_word:
121  for +ws: List<&2, U32>
122  for +q: Nat
123  for +o: Nat
124  for +w: U32
125  for +hw: {List.get(&2, U32, ws, q) == Some{w} : Maybe<&2, U32>}
126  for +ho: {Nat.is_le(o, 4n) == True{} : Bool}
127  {List.drop(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), o)) == List.append(&2, U32, List.drop(&2, U32, C.L4(w), o), D.unpack(List.drop(&2, U32, ws, Nat.add(q, 1n)))) : List<&2, U32>}
128
129def drop_word(ws, q, o, w, hw, ho):
130  match ws q:
131    case Nil{} _:
132      Empty.absurd({List.drop(&2, U32, D.unpack(Nil{}), Nat.add(Nat.mul(q, 4n), o)) == List.append(&2, U32, List.drop(&2, U32, C.L4(w), o), D.unpack(List.drop(&2, U32, Nil{}, Nat.add(q, 1n)))) : List<&2, U32>},
133        X.none_some(w, hw))
134    case Con{+x, t} 0n:
135      %X.some_inj(x, w, hw) :
136        {List.drop(&2, U32, List.append(&2, U32, C.L4(x), D.unpack(t)), o) == List.append(&2, U32, List.drop(&2, U32, C.L4(_), o), D.unpack(List.drop(&2, U32, t, 0n))) : List<&2, U32>}
137      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, X.drop_zero(t)) :
138        {List.drop(&2, U32, List.append(&2, U32, C.L4(x), D.unpack(t)), o) == List.append(&2, U32, List.drop(&2, U32, C.L4(x), o), D.unpack(_)) : List<&2, U32>}
139      drop_append_l(C.L4(x), D.unpack(t), o, ho)
140    case Con{x, t} 1n+p:
141      drop_word(t, p, o, w, hw, ho)
142
143# Whether the head of a list is c.
144def hd_eq(xs: List<&2, U32>, +c: U32) -> Bool:
145  match xs:
146    case Nil{}:
147      False{}
148    case Con{x, t}:
149      U32.is_eq(x, c)
150
151# A hit inside xs: the first c of take(xs ++ ys, n) is at min(run, n).
152law run_hit:
153  for +xs: List<&2, U32>
154  for +ys: List<&2, U32>
155  for +n: Nat
156  for +c: U32
157  for +b: Bool
158  for +hb: {hd_eq(xs, c) == b : Bool}
159  for +h: {Nat.is_lt(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}
160  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == Nat.min(D.run_len(xs, c), n) : Nat}
161
162def run_hit(xs, ys, n, c, b, hb, h):
163  match xs n b:
164    case Nil{} _ _:
165      Empty.absurd({D.run_len(List.take(&2, U32, ys, n), c) == Nat.min(0n, n) : Nat}, AB.lt_zero_absurd(0n, h))
166    case Con{x, t} 0n True{}:
167      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 0n) : Nat}
168      {==}
169    case Con{x, t} 0n False{}:
170      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 0n) : Nat}
171      {==}
172    case Con{x, t} 1n+p True{}:
173      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) :
174        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+p) : Nat}
175      {==}
176    case Con{x, t} 1n+p False{}:
177      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
178        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+p) : Nat}
179      +h2 = AB.subst(Bool, y => {Nat.is_lt(Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool},
180        hd_eq(x <> t, c), False{}, hb, h)
181      %run_hit(t, ys, p, c, hd_eq(t, c), {==}, h2) :
182        {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
183      {==}
184
185# No c in xs, and n reaches past it: the search goes on in ys.
186law run_skip:
187  for +xs: List<&2, U32>
188  for +ys: List<&2, U32>
189  for +n: Nat
190  for +c: U32
191  for +b: Bool
192  for +hb: {hd_eq(xs, c) == b : Bool}
193  for +h: {D.run_len(xs, c) == List.length(&2, U32, xs) : Nat}
194  for +hn: {Nat.is_le(List.length(&2, U32, xs), n) == True{} : Bool}
195  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == Nat.add(List.length(&2, U32, xs), D.run_len(List.take(&2, U32, ys, Nat.sub(n, List.length(&2, U32, xs))), c)) : Nat}
196
197def run_skip(xs, ys, n, c, b, hb, h, hn):
198  match xs n b:
199    case Nil{} _ _:
200      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) :
201        {D.run_len(List.take(&2, U32, ys, n), c) == D.run_len(List.take(&2, U32, ys, _), c) : Nat}
202      {==}
203    case Con{x, t} _ True{}:
204      Empty.absurd({D.run_len(List.take(&2, U32, List.append(&2, U32, x <> t, ys), n), c) == Nat.add(1n+List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(n, 1n+List.length(&2, U32, t))), c)) : Nat},
205        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat},
206          hd_eq(x <> t, c), True{}, hb, h)))
207    case Con{x, t} 0n False{}:
208      Empty.absurd({0n == Nat.add(1n+List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(0n, 1n+List.length(&2, U32, t))), c)) : Nat},
209        AB.false_ne_true(hn))
210    case Con{x, t} 1n+p False{}:
211      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
212        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == 1n+Nat.add(List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(p, List.length(&2, U32, t))), c)) : Nat}
213      +h2 = N.succ_inj(D.run_len(t, c), List.length(&2, U32, t),
214        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat}, hd_eq(x <> t, c), False{}, hb, h))
215      %run_skip(t, ys, p, c, hd_eq(t, c), {==}, h2, hn) :
216        {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
217      {==}
218
219# No c in xs, and n stays within it.
220law run_none:
221  for +xs: List<&2, U32>
222  for +ys: List<&2, U32>
223  for +n: Nat
224  for +c: U32
225  for +b: Bool
226  for +hb: {hd_eq(xs, c) == b : Bool}
227  for +h: {D.run_len(xs, c) == List.length(&2, U32, xs) : Nat}
228  for +hn: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
229  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == n : Nat}
230
231def run_none(xs, ys, n, c, b, hb, h, hn):
232  match xs n b:
233    case Nil{} 0n _:
234      %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {D.run_len(_, c) == 0n : Nat}
235      {==}
236    case Nil{} 1n+p _:
237      Empty.absurd({D.run_len(List.take(&2, U32, ys, 1n+p), c) == 1n+p : Nat}, AB.false_ne_true(hn))
238    case Con{x, t} 0n _:
239      {==}
240    case Con{x, t} 1n+p True{}:
241      Empty.absurd({D.run_len(List.take(&2, U32, List.append(&2, U32, x <> t, ys), 1n+p), c) == 1n+p : Nat},
242        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat},
243          hd_eq(x <> t, c), True{}, hb, h)))
244    case Con{x, t} 1n+p False{}:
245      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
246        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == 1n+p : Nat}
247      +h2 = N.succ_inj(D.run_len(t, c), List.length(&2, U32, t),
248        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat}, hd_eq(x <> t, c), False{}, hb, h))
249      %run_none(t, ys, p, c, hd_eq(t, c), {==}, h2, hn) : {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
250      {==}
251
252law run_le:
253  for +xs: List<&2, U32>
254  for +c: U32
255  for +b: Bool
256  for +hb: {hd_eq(xs, c) == b : Bool}
257  {Nat.is_le(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}
258
259def run_le(xs, c, b, hb):
260  match xs b:
261    case Nil{} _:
262      {==}
263    case Con{x, t} True{}:
264      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) :
265        {Nat.is_le(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool}
266      {==}
267    case Con{x, t} False{}:
268      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
269        {Nat.is_le(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool}
270      run_le(t, c, hd_eq(t, c), {==})
271
272# Nat
273# ===
274
275law min_shift:
276  for +s: Nat
277  for +r: Nat
278  for +tt: Nat
279  for +h: {Nat.is_le(s, tt) == True{} : Bool}
280  {Nat.min(Nat.add(s, r), tt) == Nat.add(s, Nat.min(r, Nat.sub(tt, s))) : Nat}
281
282def min_shift(s, r, tt, h):
283  match s tt:
284    case 0n 0n:
285      {==}
286    case 0n 1n+q:
287      {==}
288    case 1n+p 0n:
289      Empty.absurd({Nat.min(1n+Nat.add(p, r), 0n) == 1n+Nat.add(p, Nat.min(r, 0n)) : Nat}, AB.false_ne_true(h))
290    case 1n+p 1n+q:
291      %min_shift(p, r, q, h) : {1n+Nat.min(Nat.add(p, r), q) == 1n+_ : Nat}
292      {==}
293
294law le_cancel:
295  for +a: Nat
296  for +x: Nat
297  for +y: Nat
298  for +h: {Nat.is_le(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
299  {Nat.is_le(x, y) == True{} : Bool}
300
301def le_cancel(a, x, y, h):
302  match a:
303    case 0n:
304      h
305    case 1n+p:
306      le_cancel(p, x, y, h)
307
308law lt_cancel:
309  for +a: Nat
310  for +x: Nat
311  for +y: Nat
312  for +h: {Nat.is_lt(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
313  {Nat.is_lt(x, y) == True{} : Bool}
314
315def lt_cancel(a, x, y, h):
316  match a:
317    case 0n:
318      h
319    case 1n+p:
320      lt_cancel(p, x, y, h)
321
322law sub_sub:
323  for +tt: Nat
324  for +s: Nat
325  for +l: Nat
326  {Nat.sub(Nat.sub(tt, s), l) == Nat.sub(tt, Nat.add(s, l)) : Nat}
327
328def sub_sub(tt, s, l):
329  match tt s:
330    case 0n _:
331      match l:
332        case 0n:
333          {==}
334        case 1n+q:
335          {==}
336    case 1n+p 0n:
337      {==}
338    case 1n+p 1n+q:
339      sub_sub(p, q, l)
340
341law mul4s:
342  for +w: Nat
343  {Nat.mul(Nat.add(w, 1n), 4n) == Nat.add(Nat.mul(w, 4n), 4n) : Nat}
344
345def mul4s(w):
346  match w:
347    case 0n:
348      {==}
349    case 1n+p:
350      %mul4s(p) : {Nat.add(4n, Nat.mul(Nat.add(p, 1n), 4n)) == Nat.add(4n, _) : Nat}
351      {==}
352
353# Word index bounds: the words searched lie inside the block.
354law wlt:
355  for +w: Nat
356  for +k: Nat
357  for +tt: Nat
358  for +ll: Nat
359  for +pp: Nat
360  for +h1: {Nat.is_lt(Nat.mul(Nat.add(w, k), 4n), tt) == True{} : Bool}
361  for +h2: {Nat.is_le(tt, ll) == True{} : Bool}
362  for +h3: {Nat.is_le(ll, Nat.mul(4n, pp)) == True{} : Bool}
363  {Nat.is_lt(w, pp) == True{} : Bool}
364
365def wlt(w, k, tt, ll, pp, h1, h2, h3):
366  +a = N.le_lt_trans(Nat.mul(w, 4n), Nat.mul(Nat.add(w, k), 4n), Nat.mul(4n, pp), N.le_mul_r(w, Nat.add(w, k), 4n, N.le_add_r(w, k)),
367    N.lt_le_trans(Nat.mul(Nat.add(w, k), 4n), tt, Nat.mul(4n, pp), h1, N.le_trans(tt, ll, Nat.mul(4n, pp), h2, h3)))
368  N.lt_mul_cancel(4n, w, pp, AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, pp)) == True{} : Bool}, Nat.mul(w, 4n), Nat.mul(4n, w), N.mul_comm(w, 4n), a))
369
370law wb4:
371  for +w: Nat
372  for +pp: Nat
373  for +h: {Nat.is_lt(w, pp) == True{} : Bool}
374  {Nat.is_le(Nat.add(Nat.mul(w, 4n), 4n), Nat.mul(4n, pp)) == True{} : Bool}
375
376def wb4(w, pp, h):
377  +a = N.le_mul_r(1n+w, pp, 4n, Equal.trans(Bool, Nat.is_le(1n+w, pp), Nat.is_lt(w, pp), True{}, N.le_succ_lt(w, pp), h))
378  %Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), 4n), Nat.add(4n, Nat.mul(w, 4n)), N.add_comm(Nat.mul(w, 4n), 4n)) : {Nat.is_le(_, Nat.mul(4n, pp)) == True{} : Bool}
379  %Equal.sym(Nat, Nat.mul(4n, pp), Nat.mul(pp, 4n), N.mul_comm(4n, pp)) : {Nat.is_le(Nat.add(4n, Nat.mul(w, 4n)), _) == True{} : Bool}
380  a
381
382# The loop's "no hit" answer 4294967295 is above every length.
383law not0:
384  {U32.not(0) == 4294967295 : U32}
385
386def not0():
387  {==}
388
389law min_r:
390  for +a: U32
391  for +b: U32
392  for +h: {U32.is_lt(a, b) == False{} : Bool}
393  {U32.min(a, b) == b : U32}
394
395def min_r(a, b, h):
396  match a b:
397    case U32{x} U32{y}:
398      %Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), False{}, h) : {Bool.pick(U32, _, U32{x}, U32{y}) == U32{y} : U32}
399      {==}
400
401def gtop.go(+tt: Nat, +m: Nat, +ht: {Nat.is_lt(tt, m) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(Nat.sub(m, 1n), 0n), tt) == False{} : Bool}:
402  match m:
403    case 0n:
404      Empty.absurd({Nat.is_lt(0n, tt) == False{} : Bool}, AB.lt_zero_absurd(tt, ht))
405    case 1n+p:
406      %Equal.sym(Nat, Nat.sub(Nat.sub(p, 0n), 0n), Nat.sub(p, 0n), N.sub_zero(Nat.sub(p, 0n))) : {Nat.is_lt(_, tt) == False{} : Bool}
407      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, tt) == False{} : Bool}
408      N.le_not_lt(tt, p, Equal.trans(Bool, Nat.is_le(tt, p), Nat.is_lt(tt, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(tt, 1n+p), Nat.is_le(tt, p), N.lt_succ_iff(tt, p)), ht))
409
410# With the bound m abstract (m stands for 2^32).
411law gtop:
412  for +x: Nat
413  for +tt: Nat
414  for +m: Nat
415  for +hx: {x == Nat.sub(Nat.sub(m, 1n), U32.to_nat(0)) : Nat}
416  for +ht: {Nat.is_lt(tt, m) == True{} : Bool}
417  {Nat.is_lt(x, tt) == False{} : Bool}
418
419def gtop(x, tt, m, hx, ht):
420  %Equal.sym(Nat, x, Nat.sub(Nat.sub(m, 1n), U32.to_nat(0)), hx) : {Nat.is_lt(_, tt) == False{} : Bool}
421  gtop.go(tt, m, ht)
422
423
424law top_nat:
425  {U32.to_nat(4294967295) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(0)) : Nat}
426
427def top_nat():
428  %not0() : {U32.to_nat(_) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(0)) : Nat}
429  U.to_nat_not_p(0)
430
431law is_lt_top:
432  for +to: U32
433  for +d: Nat
434  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
435  for +ht: {Nat.is_le(U32.to_nat(to), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
436  {U32.is_lt(4294967295, to) == False{} : Bool}
437
438def is_lt_top(to, d, hd, ht):
439  %Equal.sym(Bool, U32.is_lt(4294967295, to), Nat.is_lt(U32.to_nat(4294967295), U32.to_nat(to)), U.is_lt_to_nat(4294967295, to)) :
440    {_ == False{} : Bool}
441  gtop(U32.to_nat(4294967295), U32.to_nat(to), Nat.pow(2n, 32n), top_nat(), C.fits_e(U32.to_nat(to), d, 32n, C.he32(d, hd), ht))
442
443law min_top:
444  for +to: U32
445  for +d: Nat
446  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
447  for +ht: {Nat.is_le(U32.to_nat(to), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
448  {U32.min(4294967295, to) == to : U32}
449
450def min_top(to, d, hd, ht):
451  min_r(4294967295, to, is_lt_top(to, d, hd, ht))
452
453# The word loop
454# =============
455
456# All the block's bytes, the start of a search inside word wi (o bytes in),
457# the rest of that word, and the bytes from the next word on.
458def UB(+t: P.Tree<U32>) -> List<&2, U32>:
459  D.unpack(C.WL(t))
460
461def SS(+wi: U32, +o: Nat) -> Nat:
462  Nat.add(Nat.mul(U32.to_nat(wi), 4n), o)
463
464def AW(+t: P.Tree<U32>, +wi: U32, +o: Nat) -> List<&2, U32>:
465  List.drop(&2, U32, C.L4(C.WD(t, wi)), o)
466
467def BW(+t: P.Tree<U32>, +wi: U32) -> List<&2, U32>:
468  List.drop(&2, U32, UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n))
469
470law shl2:
471  for +wi: U32
472  for +d: Nat
473  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
474  for +hx: {Nat.is_le(Nat.mul(U32.to_nat(wi), 4n), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
475  {U32.to_nat((wi << 2n : U32)) == Nat.mul(U32.to_nat(wi), 4n) : Nat}
476
477def shl2(wi, d, hd, hx):
478  U.to_nat_shln_fits_p(wi, 2n, C.fits_e(Nat.mul(U32.to_nat(wi), Nat.pow(2n, 2n)), d, 32n, C.he32(d, hd), hx))
479
480law dw:
481  for +t: P.Tree<U32>
482  for +d: Nat
483  for +wi: U32
484  for +o: Nat
485  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
486  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
487  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
488  for +ho: {Nat.is_le(o, 4n) == True{} : Bool}
489  {List.drop(&2, U32, UB(t), SS(wi, o)) == List.append(&2, U32, AW(t, wi, o), BW(t, wi)) : List<&2, U32>}
490
491def dw(t, d, wi, o, hf, hd, hk, ho):
492  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)), D.unpack(List.drop(&2, U32, C.WL(t), Nat.add(U32.to_nat(wi), 1n))),
493    drop_unpack(C.WL(t), Nat.add(U32.to_nat(wi), 1n))) :
494    {List.drop(&2, U32, UB(t), SS(wi, o)) == List.append(&2, U32, AW(t, wi, o), _) : List<&2, U32>}
495  drop_word(C.WL(t), U32.to_nat(wi), o, C.WD(t, wi), C.wd_get(t, d, wi, hf, hd, hk), ho)
496
497law awl:
498  for +t: P.Tree<U32>
499  for +wi: U32
500  for +o: Nat
501  {List.length(&2, U32, AW(t, wi, o)) == Nat.sub(4n, o) : Nat}
502
503def awl(t, wi, o):
504  H.drop_length(C.L4(C.WD(t, wi)), o)
505
506# The flagged word: the answer is the first c from the start, or to.
507law fhit:
508  for +len: U32
509  for +t: P.Tree<U32>
510  for +d: Nat
511  for +to: U32
512  for +c: U32
513  for +wi: U32
514  for +o: Nat
515  for +v: U32
516  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
517  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
518  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
519  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
520  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
521  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
522  for +hz: {U32.is_zero(FA.zb(v)) == False{} : Bool}
523  {U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
524
525def fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs, hk, hv, hz):
526  +W = U32.to_nat(wi)
527  +T = U32.to_nat(to)
528  +r = D.run_len(AW(t, wi, o), c)
529  +M4 = Nat.mul(4n, Nat.pow(2n, d))
530  +hd = C.ok_d(len, t, d, h)
531  +hf = C.ok_full(len, t, d, h)
532  +hp4 = run_le(C.L4(v), 0, hd_eq(C.L4(v), 0), {==})
533  +hne = Equal.trans(Bool, Nat.is_eq(FW.P0(v), 4n), U32.is_zero(FA.zb(v)), False{}, Equal.sym(Bool, U32.is_zero(FA.zb(v)), Nat.is_eq(FW.P0(v), 4n), FW.zb_none(v)), hz)
534  +hlt = Equal.trans(Bool, Nat.is_lt(FW.P0(v), 4n), Nat.is_le(1n+FW.P0(v), 4n), True{}, Equal.sym(Bool, Nat.is_le(1n+FW.P0(v), 4n), Nat.is_lt(FW.P0(v), 4n), N.le_succ_lt(FW.P0(v), 4n)),
535    N.le_ne(FW.P0(v), 4n, hp4, hne))
536  +hlt2 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, FW.P0(v), Nat.add(o, r), hv, hlt)
537  +eo = N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))
538  +hrl0 = lt_cancel(o, r, Nat.sub(4n, o), AB.subst(Nat, y => {Nat.is_lt(Nat.add(o, r), y) == True{} : Bool}, 4n, Nat.add(o, Nat.sub(4n, o)), Equal.sym(Nat, Nat.add(o, Nat.sub(4n, o)), 4n, eo), hlt2))
539  +hrl = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, AW(t, wi, o)), Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)), hrl0)
540  +eb = Equal.trans(Nat, U32.to_nat(FA.bidx(FA.zb(v))), FW.P0(v), Nat.add(o, r), FW.zb_bidx(v, hlt), hv)
541  +hw4 = wb4(W, Nat.pow(2n, d), hk)
542  +esh = shl2(wi, d, hd, N.le_trans(Nat.mul(W, 4n), Nat.add(Nat.mul(W, 4n), 4n), M4, N.le_add_r(Nat.mul(W, 4n), 4n), hw4))
543  +b1 = N.le_trans(Nat.add(Nat.mul(W, 4n), Nat.add(o, r)), Nat.add(Nat.mul(W, 4n), 4n), M4,
544    N.le_add_mono_l(Nat.mul(W, 4n), Nat.add(o, r), 4n, N.lt_to_le(Nat.add(o, r), 4n, hlt2)), hw4)
545  +b2 = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, Nat.add(o, r)), M4) == True{} : Bool}, Nat.mul(W, 4n), U32.to_nat((wi << 2n : U32)), Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh), b1)
546  +b3 = AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat((wi << 2n : U32)), y), M4) == True{} : Bool}, Nat.add(o, r), U32.to_nat(FA.bidx(FA.zb(v))),
547    Equal.sym(Nat, U32.to_nat(FA.bidx(FA.zb(v))), Nat.add(o, r), eb), b2)
548  +ej = C.add_fits((wi << 2n : U32), FA.bidx(FA.zb(v)), d, hd, b3)
549  +RHS = D.first(UB(t), SS(wi, o), T, c)
550  %Equal.sym(Nat, U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)), Nat.min(U32.to_nat(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32)), T),
551    U.to_nat_min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)) :
552    {_ == RHS : Nat}
553  %Equal.sym(Nat, U32.to_nat(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32)), Nat.add(U32.to_nat((wi << 2n : U32)), U32.to_nat(FA.bidx(FA.zb(v)))), ej) :
554    {Nat.min(_, T) == RHS : Nat}
555  %Equal.sym(Nat, U32.to_nat(FA.bidx(FA.zb(v))), Nat.add(o, r), eb) :
556    {Nat.min(Nat.add(U32.to_nat((wi << 2n : U32)), _), T) == RHS : Nat}
557  %Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh) :
558    {Nat.min(Nat.add(_, Nat.add(o, r)), T) == RHS : Nat}
559  %N.add_assoc(Nat.mul(W, 4n), o, r) :
560    {Nat.min(_, T) == RHS : Nat}
561  %Equal.sym(Nat, Nat.min(Nat.add(SS(wi, o), r), T), Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))), min_shift(SS(wi, o), r, T, hs)) :
562    {_ == RHS : Nat}
563  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), SS(wi, o)), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
564    {Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))) == Nat.add(SS(wi, o), D.run_len(List.take(&2, U32, _, Nat.sub(T, SS(wi, o))), c)) : Nat}
565  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), Nat.sub(T, SS(wi, o))), c), Nat.min(r, Nat.sub(T, SS(wi, o))),
566    run_hit(AW(t, wi, o), BW(t, wi), Nat.sub(T, SS(wi, o)), c, hd_eq(AW(t, wi, o), c), {==}, hrl)) :
567    {Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))) == Nat.add(SS(wi, o), _) : Nat}
568  {==}
569
570# An unflagged word has no c from the start on.
571law nohit_run:
572  for +t: P.Tree<U32>
573  for +wi: U32
574  for +o: Nat
575  for +v: U32
576  for +c: U32
577  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
578  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
579  {D.run_len(AW(t, wi, o), c) == List.length(&2, U32, AW(t, wi, o)) : Nat}
580
581def nohit_run(t, wi, o, v, c, hv, hz):
582  +r = D.run_len(AW(t, wi, o), c)
583  +e4 = N.eq_sound(FW.P0(v), 4n, Equal.trans(Bool, Nat.is_eq(FW.P0(v), 4n), U32.is_zero(FA.zb(v)), True{},
584    Equal.sym(Bool, U32.is_zero(FA.zb(v)), Nat.is_eq(FW.P0(v), 4n), FW.zb_none(v)), hz))
585  +e5 = Equal.trans(Nat, Nat.add(o, r), FW.P0(v), 4n, Equal.sym(Nat, FW.P0(v), Nat.add(o, r), hv), e4)
586  %Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)) : {r == _ : Nat}
587  %e5 : {r == Nat.sub(_, o) : Nat}
588  Equal.sym(Nat, Nat.sub(Nat.add(o, r), o), r, N.sub_add_l(o, r))
589
590law pow_le4:
591  for +p: Nat
592  {Nat.is_le(p, Nat.mul(4n, p)) == True{} : Bool}
593
594def pow_le4(p):
595  N.le_add_r(p, Nat.mul(3n, p))
596
597# The last word, unflagged: the answer is to.
598law fnone0:
599  for +len: U32
600  for +t: P.Tree<U32>
601  for +d: Nat
602  for +to: U32
603  for +c: U32
604  for +wi: U32
605  for +o: Nat
606  for +v: U32
607  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
608  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
609  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
610  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
611  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
612  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
613  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
614  for +he: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)) == True{} : Bool}
615  {U32.to_nat(U32.min(4294967295, to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
616
617def fnone0(len, t, d, to, c, wi, o, v, h, ht, ho, hs, hk, hv, hz, he):
618  +W = U32.to_nat(wi)
619  +T = U32.to_nat(to)
620  +X = Nat.sub(T, SS(wi, o))
621  +hd = C.ok_d(len, t, d, h)
622  +hf = C.ok_full(len, t, d, h)
623  +a1 = AB.subst(Nat, y => {Nat.is_le(T, y) == True{} : Bool}, Nat.mul(Nat.add(W, 1n), 4n), Nat.add(Nat.mul(W, 4n), 4n), mul4s(W), he)
624  +a2 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, T, Nat.add(SS(wi, o), X),
625    Equal.sym(Nat, Nat.add(SS(wi, o), X), T, N.le_sub_add(SS(wi, o), T, hs)), a1)
626  +a3 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(W, 4n), o), X), Nat.add(Nat.mul(W, 4n), Nat.add(o, X)),
627    N.add_assoc(Nat.mul(W, 4n), o, X), a2)
628  +a4 = N.le_sub_r(o, X, 4n, le_cancel(Nat.mul(W, 4n), Nat.add(o, X), 4n, a3))
629  +hn = AB.subst(Nat, y => {Nat.is_le(X, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, AW(t, wi, o)),
630    Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)), a4)
631  +RHS = D.first(UB(t), SS(wi, o), T, c)
632  %Equal.sym(U32, U32.min(4294967295, to), to, min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
633    {U32.to_nat(_) == RHS : Nat}
634  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), SS(wi, o)), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
635    {T == Nat.add(SS(wi, o), D.run_len(List.take(&2, U32, _, X), c)) : Nat}
636  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), X), c), X,
637    run_none(AW(t, wi, o), BW(t, wi), X, c, hd_eq(AW(t, wi, o), c), {==}, nohit_run(t, wi, o, v, c, hv, hz), hn)) :
638    {T == Nat.add(SS(wi, o), _) : Nat}
639  Equal.sym(Nat, Nat.add(SS(wi, o), X), T, N.le_sub_add(SS(wi, o), T, hs))
640
641# An unflagged word that is not the last: the search goes on at the next word.
642law fskip:
643  for +len: U32
644  for +t: P.Tree<U32>
645  for +d: Nat
646  for +to: U32
647  for +c: U32
648  for +wi: U32
649  for +o: Nat
650  for +v: U32
651  for +k: Nat
652  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
653  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
654  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
655  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
656  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
657  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
658  for +hs1: {Nat.is_le(Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to)) == True{} : Bool}
659  {D.first(UB(t), SS(wi, o), U32.to_nat(to), c) == D.first(UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to), c) : Nat}
660
661def fskip(len, t, d, to, c, wi, o, v, k, h, ho, hs, hk, hv, hz, hs1):
662  +W = U32.to_nat(wi)
663  +T = U32.to_nat(to)
664  +S = SS(wi, o)
665  +S1 = Nat.mul(Nat.add(W, 1n), 4n)
666  +L = Nat.sub(4n, o)
667  +hd = C.ok_d(len, t, d, h)
668  +hf = C.ok_full(len, t, d, h)
669  +eS = Equal.trans(Nat, Nat.add(S, L), Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), S1, N.add_assoc(Nat.mul(W, 4n), o, L),
670    Equal.trans(Nat, Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), Nat.add(Nat.mul(W, 4n), 4n), S1,
671      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(W, 4n), y), Nat.add(o, L), 4n, N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))),
672      Equal.sym(Nat, S1, Nat.add(Nat.mul(W, 4n), 4n), mul4s(W))))
673  +hl0 = N.le_sub_r(S, L, T, AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, Nat.add(S, L), Equal.sym(Nat, Nat.add(S, L), S1, eS), hs1))
674  +hn = AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, S)) == True{} : Bool}, L, List.length(&2, U32, AW(t, wi, o)),
675    Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), L, awl(t, wi, o)), hl0)
676  +RHS = D.first(UB(t), S1, T, c)
677  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), S), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
678    {Nat.add(S, D.run_len(List.take(&2, U32, _, Nat.sub(T, S)), c)) == RHS : Nat}
679  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), Nat.sub(T, S)), c),
680    Nat.add(List.length(&2, U32, AW(t, wi, o)), D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(Nat.sub(T, S), List.length(&2, U32, AW(t, wi, o)))), c)),
681    run_skip(AW(t, wi, o), BW(t, wi), Nat.sub(T, S), c, hd_eq(AW(t, wi, o), c), {==}, nohit_run(t, wi, o, v, c, hv, hz), hn)) :
682    {Nat.add(S, _) == RHS : Nat}
683  %Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), L, awl(t, wi, o)) :
684    {Nat.add(S, Nat.add(_, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(Nat.sub(T, S), _)), c))) == RHS : Nat}
685  %Equal.sym(Nat, Nat.sub(Nat.sub(T, S), L), Nat.sub(T, Nat.add(S, L)), sub_sub(T, S, L)) :
686    {Nat.add(S, Nat.add(L, D.run_len(List.take(&2, U32, BW(t, wi), _), c))) == RHS : Nat}
687  %N.add_assoc(S, L, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(T, Nat.add(S, L))), c)) :
688    {_ == RHS : Nat}
689  %Equal.sym(Nat, Nat.add(S, L), S1, eS) :
690    {Nat.add(_, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(T, _)), c)) == RHS : Nat}
691  {==}
692
693# The first byte of the next word starts a fresh search.
694law hv0:
695  for +t: P.Tree<U32>
696  for +wi: U32
697  for +c: U32
698  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
699  {FW.P0(U32.xor(C.WD(t, wi), FA.rep(c))) == Nat.add(0n, D.run_len(AW(t, wi, 0n), c)) : Nat}
700
701def hv0(t, wi, c, hc):
702  %Equal.sym(List<&2, U32>, List.drop(&2, U32, C.L4(C.WD(t, wi)), 0n), C.L4(C.WD(t, wi)), X.drop_zero(C.L4(C.WD(t, wi)))) :
703    {FW.P0(U32.xor(C.WD(t, wi), FA.rep(c))) == Nat.add(0n, D.run_len(_, c)) : Nat}
704  FW.p0_xor(C.WD(t, wi), c, hc)
705
706# The loop invariant, for 1 + k words left (wi's included): the answer, capped
707# at to, is the first c from the start o bytes into word wi.
708law fi:
709  for +k: Nat
710  for +z: Bool
711  for +len: U32
712  for +t: P.Tree<U32>
713  for +d: Nat
714  for +to: U32
715  for +c: U32
716  for +wi: U32
717  for +o: Nat
718  for +v: U32
719  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
720  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
721  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
722  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
723  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
724  for +he1: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n+k), 4n)) == True{} : Bool}
725  for +he2: {Nat.is_lt(Nat.mul(Nat.add(U32.to_nat(wi), k), 4n), U32.to_nat(to)) == True{} : Bool}
726  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
727  for +hz: {U32.is_zero(FA.zb(v)) == z : Bool}
728  {U32.to_nat(U32.min(FG(1n+k, z, wi, FA.zb(v), FA.rep(c), t), to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
729
730def fi(k, z, len, t, d, to, c, wi, o, v, h, ht, hc, ho, hs, he1, he2, hv, hz):
731  match k z:
732    case 0n False{}:
733      fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
734        wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
735    case 1n+q False{}:
736      fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
737        wlt(U32.to_nat(wi), 1n+q, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
738    case 0n True{}:
739      fnone0(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
740        wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz, he1)
741    case 1n+q True{}:
742      +W = U32.to_nat(wi)
743      +T = U32.to_nat(to)
744      +j1 = (wi + 1 : U32)
745      +v1 = U32.xor(C.WD(t, j1), FA.rep(c))
746      +S1 = Nat.mul(Nat.add(W, 1n), 4n)
747      +hk = wlt(W, 1n+q, T, U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h))
748      +ej1 = C.inc_fits(wi, d, C.ok_d(len, t, d, h), N.lt_le_trans(W, Nat.pow(2n, d), Nat.mul(4n, Nat.pow(2n, d)), hk, pow_le4(Nat.pow(2n, d))))
749      +hs1 = N.lt_to_le(S1, T, N.le_lt_trans(S1, Nat.mul(Nat.add(W, 1n+q), 4n), T,
750        N.le_mul_r(Nat.add(W, 1n), Nat.add(W, 1n+q), 4n, N.le_add_mono_l(W, 1n, 1n+q, N.le_zero_l(q))), he2))
751      +ea = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(j1), 4n), 0n), Nat.mul(U32.to_nat(j1), 4n), S1, N.add_zero(Nat.mul(U32.to_nat(j1), 4n)),
752        Equal.cong(Nat, Nat, y => Nat.mul(y, 4n), U32.to_nat(j1), Nat.add(W, 1n), ej1))
753      +hsi = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, SS(j1, 0n), Equal.sym(Nat, SS(j1, 0n), S1, ea), hs1)
754      +e1 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(Nat.add(W, 1n), 1n+q), Nat.add(W, 1n+(1n+q)),
755        Equal.cong(Nat, Nat, y => Nat.add(y, 1n+q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, 1n+q))
756      +he1i = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(W, 1n+(1n+q)), Nat.add(U32.to_nat(j1), 1n+q),
757        Equal.sym(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(W, 1n+(1n+q)), e1), he1)
758      +e2 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(Nat.add(W, 1n), q), Nat.add(W, 1n+q),
759        Equal.cong(Nat, Nat, y => Nat.add(y, q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, q))
760      +he2i = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.add(W, 1n+q), Nat.add(U32.to_nat(j1), q),
761        Equal.sym(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(W, 1n+q), e2), he2)
762      +ih = fi(q, U32.is_zero(FA.zb(v1)), len, t, d, to, c, j1, 0n, v1, h, ht, hc, {==}, hsi, he1i, he2i, hv0(t, j1, c, hc), {==})
763      +sk = fskip(len, t, d, to, c, wi, o, v, q, h, ho, hs, hk, hv, hz, hs1)
764      Equal.trans(Nat, U32.to_nat(U32.min(FG(1n+q, U32.is_zero(FA.zb(v1)), j1, FA.zb(v1), FA.rep(c), t), to)), D.first(UB(t), SS(j1, 0n), T, c), D.first(UB(t), SS(wi, o), T, c),
765        ih, Equal.sym(Nat, D.first(UB(t), SS(wi, o), T, c), D.first(UB(t), SS(j1, 0n), T, c),
766          Equal.trans(Nat, D.first(UB(t), SS(wi, o), T, c), D.first(UB(t), S1, T, c), D.first(UB(t), SS(j1, 0n), T, c), sk,
767            Equal.cong(Nat, Nat, y => D.first(UB(t), y, T, c), S1, SS(j1, 0n), Equal.sym(Nat, SS(j1, 0n), S1, ea)))))
768
769# The top level
770# =============
771
772law slice_take:
773  for +xs: List<&2, U32>
774  for +l: Nat
775  for +f: Nat
776  for +n: Nat
777  for +h: {Nat.is_le(Nat.add(f, n), l) == True{} : Bool}
778  {D.slice(List.take(&2, U32, xs, l), f, n) == D.slice(xs, f, n) : List<&2, U32>}
779
780def slice_take(xs, l, f, n, h):
781  match xs l f:
782    case Nil{} _ _:
783      {==}
784    case Con{x, t} 0n 0n:
785      match n:
786        case 0n:
787          {==}
788        case 1n+q:
789          Empty.absurd({D.slice(Nil{}, 0n, 1n+q) == D.slice(x <> t, 0n, 1n+q) : List<&2, U32>}, AB.false_ne_true(h))
790    case Con{x, t} 0n 1n+g:
791      Empty.absurd({D.slice(Nil{}, 1n+g, n) == D.slice(x <> t, 1n+g, n) : List<&2, U32>}, AB.false_ne_true(h))
792    case Con{+x, t} 1n+p 0n:
793      match n:
794        case 0n:
795          {==}
796        case 1n+q:
797          Equal.cong(List<&2, U32>, List<&2, U32>, y => x <> y, List.take(&2, U32, List.take(&2, U32, t, p), q), List.take(&2, U32, t, q), Q.take_take(t, p, q, h))
798    case Con{x, t} 1n+p 1n+g:
799      slice_take(t, p, g, n, h)
800
801law le_antisym:
802  for +a: Nat
803  for +b: Nat
804  for +h1: {Nat.is_le(a, b) == True{} : Bool}
805  for +h2: {Nat.is_le(b, a) == True{} : Bool}
806  {a == b : Nat}
807
808def le_antisym(a, b, h1, h2):
809  match a b:
810    case 0n 0n:
811      {==}
812    case 0n 1n+q:
813      Empty.absurd({0n == 1n+q : Nat}, AB.false_ne_true(h2))
814    case 1n+p 0n:
815      Empty.absurd({1n+p == 0n : Nat}, AB.false_ne_true(h1))
816    case 1n+p 1n+q:
817      %le_antisym(p, q, h1, h2) : {1n+p == 1n+_ : Nat}
818      {==}
819
820law lt_add_l:
821  for +c: Nat
822  for +a: Nat
823  for +b: Nat
824  for +h: {Nat.is_lt(a, b) == True{} : Bool}
825  {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
826
827def lt_add_l(c, a, b, h):
828  match c:
829    case 0n:
830      h
831    case 1n+p:
832      lt_add_l(p, a, b, h)
833
834law div_le4:
835  for +a: Nat
836  for +b: Nat
837  for +h: {Nat.is_le(a, b) == True{} : Bool}
838  {Nat.is_le(Nat.div(a, 4n), Nat.div(b, 4n)) == True{} : Bool}
839
840def div_le4(a, b, h):
841  +qb = Nat.div(b, 4n)
842  +rb = Nat.mod(b, 4n)
843  +hb = AB.subst(Nat, y => {Nat.is_le(a, y) == True{} : Bool}, b, Nat.add(Nat.mul(qb, 4n), rb), Equal.sym(Nat, Nat.add(Nat.mul(qb, 4n), rb), b, N.div_mod(b, 4n)), h)
844  +h1 = N.le_lt_trans(a, Nat.add(Nat.mul(qb, 4n), rb), Nat.add(Nat.mul(qb, 4n), 4n), hb, lt_add_l(Nat.mul(qb, 4n), rb, 4n, N.mod_lt(b, 4n, {==})))
845  +h2 = AB.subst(Nat, y => {Nat.is_lt(a, y) == True{} : Bool}, Nat.add(Nat.mul(qb, 4n), 4n), Nat.mul(4n, 1n+qb),
846    Equal.trans(Nat, Nat.add(Nat.mul(qb, 4n), 4n), Nat.mul(1n+qb, 4n), Nat.mul(4n, 1n+qb),
847      Equal.trans(Nat, Nat.add(Nat.mul(qb, 4n), 4n), Nat.add(4n, Nat.mul(qb, 4n)), Nat.mul(1n+qb, 4n), N.add_comm(Nat.mul(qb, 4n), 4n), {==}),
848      N.mul_comm(1n+qb, 4n)), h1)
849  Equal.trans(Bool, Nat.is_le(Nat.div(a, 4n), qb), Nat.is_lt(Nat.div(a, 4n), 1n+qb), True{},
850    Equal.sym(Bool, Nat.is_lt(Nat.div(a, 4n), 1n+qb), Nat.is_le(Nat.div(a, 4n), qb), N.lt_succ_iff(Nat.div(a, 4n), qb)),
851    N.div_lt(a, 4n, 1n+qb, {==}, h2))
852
853# The last word holds byte to - 1: 4E < to <= 4E + 4 for E = (to - 1) / 4.
854law last_lt:
855  for +tt: Nat
856  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
857  {Nat.is_lt(Nat.mul(Nat.div(Nat.sub(tt, 1n), 4n), 4n), tt) == True{} : Bool}
858
859def last_lt(tt, h):
860  match tt:
861    case 0n:
862      Empty.absurd({Nat.is_lt(Nat.mul(Nat.div(Nat.sub(0n, 1n), 4n), 4n), 0n) == True{} : Bool}, AB.false_ne_true(h))
863    case 1n+p:
864      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(Nat.mul(Nat.div(_, 4n), 4n), 1n+p) == True{} : Bool}
865      Equal.trans(Bool, Nat.is_lt(Nat.mul(Nat.div(p, 4n), 4n), 1n+p), Nat.is_le(Nat.mul(Nat.div(p, 4n), 4n), p), True{},
866        N.lt_succ_iff(Nat.mul(Nat.div(p, 4n), 4n), p),
867        AB.subst(Nat, y => {Nat.is_le(Nat.mul(Nat.div(p, 4n), 4n), y) == True{} : Bool}, Nat.add(Nat.mul(Nat.div(p, 4n), 4n), Nat.mod(p, 4n)), p, N.div_mod(p, 4n),
868          N.le_add_r(Nat.mul(Nat.div(p, 4n), 4n), Nat.mod(p, 4n))))
869
870law last_le:
871  for +tt: Nat
872  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
873  {Nat.is_le(tt, Nat.mul(Nat.add(Nat.div(Nat.sub(tt, 1n), 4n), 1n), 4n)) == True{} : Bool}
874
875def last_le(tt, h):
876  match tt:
877    case 0n:
878      Empty.absurd({Nat.is_le(0n, Nat.mul(Nat.add(Nat.div(Nat.sub(0n, 1n), 4n), 1n), 4n)) == True{} : Bool}, AB.false_ne_true(h))
879    case 1n+p:
880      +q = Nat.div(p, 4n)
881      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_le(1n+p, Nat.mul(Nat.add(Nat.div(_, 4n), 1n), 4n)) == True{} : Bool}
882      %Equal.sym(Nat, Nat.mul(Nat.add(q, 1n), 4n), Nat.add(Nat.mul(q, 4n), 4n), mul4s(q)) : {Nat.is_le(1n+p, _) == True{} : Bool}
883      %N.div_mod(p, 4n) : {Nat.is_le(1n+_, Nat.add(Nat.mul(q, 4n), 4n)) == True{} : Bool}
884      %N.add_succ(Nat.mul(q, 4n), Nat.mod(p, 4n)) : {Nat.is_le(_, Nat.add(Nat.mul(q, 4n), 4n)) == True{} : Bool}
885      N.le_add_mono_l(Nat.mul(q, 4n), 1n+Nat.mod(p, 4n), 4n,
886        Equal.trans(Bool, Nat.is_le(1n+Nat.mod(p, 4n), 4n), Nat.is_lt(Nat.mod(p, 4n), 4n), True{}, N.le_succ_lt(Nat.mod(p, 4n), 4n), N.mod_lt(p, 4n, {==})))
887
888law lt_sub1:
889  for +f: Nat
890  for +tt: Nat
891  for +h: {Nat.is_lt(f, tt) == True{} : Bool}
892  {Nat.is_le(f, Nat.sub(tt, 1n)) == True{} : Bool}
893
894def lt_sub1(f, tt, h):
895  match tt:
896    case 0n:
897      Empty.absurd({Nat.is_le(f, 0n) == True{} : Bool}, AB.lt_zero_absurd(f, h))
898    case 1n+p:
899      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_le(f, _) == True{} : Bool}
900      Equal.trans(Bool, Nat.is_le(f, p), Nat.is_lt(f, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(f, 1n+p), Nat.is_le(f, p), N.lt_succ_iff(f, p)), h)
901
902law div_self_le:
903  for +a: Nat
904  {Nat.is_le(Nat.div(a, 4n), a) == True{} : Bool}
905
906def div_self_le(a):
907  +h = Equal.trans(Bool, Nat.is_lt(a, 1n+Nat.add(a, Nat.mul(3n, 1n+a))), Nat.is_le(a, Nat.add(a, Nat.mul(3n, 1n+a))), True{},
908    N.lt_succ_iff(a, Nat.add(a, Nat.mul(3n, 1n+a))), N.le_add_r(a, Nat.mul(3n, 1n+a)))
909  Equal.trans(Bool, Nat.is_le(Nat.div(a, 4n), a), Nat.is_lt(Nat.div(a, 4n), 1n+a), True{},
910    Equal.sym(Bool, Nat.is_lt(Nat.div(a, 4n), 1n+a), Nat.is_le(Nat.div(a, 4n), a), N.lt_succ_iff(Nat.div(a, 4n), a)),
911    N.div_lt(a, 4n, 1n+a, {==}, h))
912
913law sub1_lt:
914  for +tt: Nat
915  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
916  {Nat.is_lt(Nat.sub(tt, 1n), tt) == True{} : Bool}
917
918def sub1_lt(tt, h):
919  match tt:
920    case 0n:
921      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, AB.false_ne_true(h))
922    case 1n+p:
923      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, 1n+p) == True{} : Bool}
924      Equal.trans(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), True{}, N.lt_succ_iff(p, p), N.le_refl(p))
925
926# from < to: the loop runs 1 + k0 words, from word from >> 2 to word (to - 1) >> 2.
927law fview_lt:
928  for +len: U32
929  for +t: P.Tree<U32>
930  for +d: Nat
931  for +from: U32
932  for +to: U32
933  for +c: U32
934  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
935  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
936  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
937  for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
938  {U32.to_nat(U32.min(FG(U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
939
940def fview_lt(len, t, d, from, to, c, h, ht, hc, hlt):
941  +F = U32.to_nat(from)
942  +T = U32.to_nat(to)
943  +wi0 = (from >> 2n : U32)
944  +W0 = U32.to_nat(wi0)
945  +o0 = U32.to_nat((from .&. 3 : U32))
946  +ee = ((to - 1 : U32) >> 2n : U32)
947  +E = U32.to_nat(ee)
948  +rc = FA.rep(c)
949  +hd = C.ok_d(len, t, d, h)
950  +M4 = Nat.mul(4n, Nat.pow(2n, d))
951  +hTM = N.le_trans(T, U32.to_nat(len), M4, ht, C.ok_len(len, t, d, h))
952  +h0T = N.le_lt_trans(0n, F, T, N.le_zero_l(F), hlt)
953  +eW0 = U.to_nat_shrn(from, 2n)
954  +eo = U.to_nat_and_mask(from, 3, 2n, {==})
955  +et1 = U.to_nat_sub_le(to, 1, Equal.trans(Bool, U32.is_le(1, to), Nat.is_le(U32.to_nat(1), T), True{}, U.is_le_to_nat(1, to),
956    Equal.trans(Bool, Nat.is_le(1n, T), Nat.is_lt(0n, T), True{}, N.le_succ_lt(0n, T), h0T)))
957  +eE = Equal.trans(Nat, E, Nat.div(U32.to_nat((to - 1 : U32)), 4n), Nat.div(Nat.sub(T, 1n), 4n), U.to_nat_shrn((to - 1 : U32), 2n),
958    Equal.cong(Nat, Nat, y => Nat.div(y, 4n), U32.to_nat((to - 1 : U32)), Nat.sub(T, 1n), et1))
959  +hWE = AB.subst(Nat, y => {Nat.is_le(W0, y) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE),
960    AB.subst(Nat, y => {Nat.is_le(y, Nat.div(Nat.sub(T, 1n), 4n)) == True{} : Bool}, Nat.div(F, 4n), W0, Equal.sym(Nat, W0, Nat.div(F, 4n), eW0),
961      div_le4(F, Nat.sub(T, 1n), lt_sub1(F, T, hlt))))
962  +k0 = Nat.sub(E, W0)
963  +esub = U.to_nat_sub_le(ee, wi0, Equal.trans(Bool, U32.is_le(wi0, ee), Nat.is_le(W0, E), True{}, U.is_le_to_nat(wi0, ee), hWE))
964  +hET = N.le_lt_trans(E, Nat.sub(T, 1n), T,
965    AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, 1n)) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE), div_self_le(Nat.sub(T, 1n))),
966    sub1_lt(T, h0T))
967  +ek = C.inc_fits((ee - wi0 : U32), d, hd,
968    AB.subst(Nat, y => {Nat.is_lt(y, M4) == True{} : Bool}, k0, U32.to_nat((ee - wi0 : U32)), Equal.sym(Nat, U32.to_nat((ee - wi0 : U32)), k0, esub),
969      N.le_lt_trans(k0, E, M4, H.sub_le(E, W0), N.lt_le_trans(E, T, M4, hET, hTM))))
970  +en = Equal.trans(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), 1n+k0, ek,
971    Equal.trans(Nat, Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), Nat.add(k0, 1n), 1n+k0, Equal.cong(Nat, Nat, y => Nat.add(y, 1n), U32.to_nat((ee - wi0 : U32)), k0, esub), N.add_one(k0)))
972  +eSF = Equal.trans(Nat, SS(wi0, o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)), F,
973    Equal.trans(Nat, Nat.add(Nat.mul(W0, 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)),
974      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(y, 4n), o0), W0, Nat.div(F, 4n), eW0),
975      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(Nat.div(F, 4n), 4n), y), o0, Nat.mod(F, 4n), eo)),
976    N.div_mod(F, 4n))
977  +ho0 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(F, 4n), o0, Equal.sym(Nat, o0, Nat.mod(F, 4n), eo), N.mod_lt(F, 4n, {==}))
978  +hs0 = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, F, SS(wi0, o0), Equal.sym(Nat, SS(wi0, o0), F, eSF), N.lt_to_le(F, T, hlt))
979  +eWk = N.le_sub_add(W0, E, hWE)
980  +eA = Equal.trans(Nat, Nat.add(W0, 1n+k0), 1n+Nat.add(W0, k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), N.add_succ(W0, k0),
981    Equal.trans(Nat, 1n+Nat.add(W0, k0), 1n+E, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.cong(Nat, Nat, y => 1n+y, Nat.add(W0, k0), E, eWk),
982      Equal.trans(Nat, 1n+E, Nat.add(E, 1n), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.sym(Nat, Nat.add(E, 1n), 1n+E, N.add_one(E)),
983        Equal.cong(Nat, Nat, y => Nat.add(y, 1n), E, Nat.div(Nat.sub(T, 1n), 4n), eE))))
984  +he1 = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Nat.add(W0, 1n+k0),
985    Equal.sym(Nat, Nat.add(W0, 1n+k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), eA), last_le(T, h0T))
986  +eB = Equal.trans(Nat, Nat.add(W0, k0), E, Nat.div(Nat.sub(T, 1n), 4n), eWk, eE)
987  +he2 = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), Nat.add(W0, k0),
988    Equal.sym(Nat, Nat.add(W0, k0), Nat.div(Nat.sub(T, 1n), 4n), eB), last_lt(T, h0T))
989  +fiv = fi(k0, U32.is_zero(M0(t, from, rc)), len, t, d, to, c, wi0, o0, U32.or(U32.xor(C.WD(t, wi0), rc), U32.not(FA.low(from))),
990    h, ht, hc, ho0, hs0, he1, he2, FW.p0_low(C.WD(t, wi0), c, from, hc), {==})
991  +hh = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, T, Nat.add(F, Nat.sub(T, F)),
992    Equal.sym(Nat, Nat.add(F, Nat.sub(T, F)), T, N.le_sub_add(F, T, N.lt_to_le(F, T, hlt))), ht)
993  +E2 = Equal.trans(Nat, D.first(UB(t), SS(wi0, o0), T, c), D.first(UB(t), F, T, c), D.first(D.view(C.BT(len, t)), F, T, c),
994    Equal.cong(Nat, Nat, y => D.first(UB(t), y, T, c), SS(wi0, o0), F, eSF),
995    Equal.sym(Nat, D.first(D.view(C.BT(len, t)), F, T, c), D.first(UB(t), F, T, c),
996      Equal.cong(List<&2, U32>, Nat, y => Nat.add(F, D.run_len(y, c)), D.slice(List.take(&2, U32, UB(t), U32.to_nat(len)), F, Nat.sub(T, F)), D.slice(UB(t), F, Nat.sub(T, F)),
997        slice_take(UB(t), U32.to_nat(len), F, Nat.sub(T, F), hh))))
998  %Equal.sym(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), 1n+k0, en) :
999    {U32.to_nat(U32.min(FG(_, U32.is_zero(M0(t, from, rc)), wi0, M0(t, from, rc), rc, t), to)) == D.first(D.view(C.BT(len, t)), F, T, c) : Nat}
1000  Equal.trans(Nat, U32.to_nat(U32.min(FG(1n+k0, U32.is_zero(M0(t, from, rc)), wi0, M0(t, from, rc), rc, t), to)), D.first(UB(t), SS(wi0, o0), T, c),
1001    D.first(D.view(C.BT(len, t)), F, T, c), fiv, E2)
1002
1003# The answer as a number, split on to <= from (no words: the answer is to = from).
1004law fview_go:
1005  for +b: Bool
1006  for +len: U32
1007  for +t: P.Tree<U32>
1008  for +d: Nat
1009  for +from: U32
1010  for +to: U32
1011  for +c: U32
1012  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
1013  for +hft: {U32.is_le(from, to) == True{} : Bool}
1014  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
1015  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
1016  for +hb: {U32.is_le(to, from) == b : Bool}
1017  {U32.to_nat(U32.min(FG(Bool.pick(Nat, b, 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32))), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
1018
1019def fview_go(b, len, t, d, from, to, c, h, hft, ht, hc, hb):
1020  match b:
1021    case True{}:
1022      +F = U32.to_nat(from)
1023      +T = U32.to_nat(to)
1024      +xs = D.view(C.BT(len, t))
1025      +hd = C.ok_d(len, t, d, h)
1026      +eTF = le_antisym(T, F, Equal.trans(Bool, Nat.is_le(T, F), U32.is_le(to, from), True{}, Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(T, F), U.is_le_to_nat(to, from)), hb),
1027        Equal.trans(Bool, Nat.is_le(F, T), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(F, T), U.is_le_to_nat(from, to)), hft))
1028      %Equal.sym(U32, U32.min(4294967295, to), to, min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
1029        {U32.to_nat(_) == D.first(xs, F, T, c) : Nat}
1030      %Equal.sym(Nat, T, F, eTF) : {_ == D.first(xs, F, _, c) : Nat}
1031      %Equal.sym(Nat, Nat.sub(F, F), 0n, H.sub_self(F)) : {F == Nat.add(F, D.run_len(D.slice(xs, F, _), c)) : Nat}
1032      %Equal.sym(List<&2, U32>, D.slice(xs, F, 0n), Nil{}, X.slice_zero(xs, F)) : {F == Nat.add(F, D.run_len(_, c)) : Nat}
1033      Equal.sym(Nat, Nat.add(F, 0n), F, N.add_zero(F))
1034    case False{}:
1035      fview_lt(len, t, d, from, to, c, h, ht, hc,
1036        N.not_le_lt(U32.to_nat(to), U32.to_nat(from), Equal.trans(Bool, Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U32.is_le(to, from), False{},
1037          Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U.is_le_to_nat(to, from)), hb)))
1038
1039# fast find equals the reference find, Bytes included.
1040law fast_find_t:
1041  for +len: U32
1042  for +t: P.Tree<U32>
1043  for +d: Nat
1044  for +from: U32
1045  for +to: U32
1046  for +c: U32
1047  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
1048  for +hft: {U32.is_le(from, to) == True{} : Bool}
1049  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
1050  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
1051  {FA.find(C.BT(len, t), from, to, c) == B.find(C.BT(len, t), from, to, c) : D.Bytes & U32}
1052
1053def fast_find_t(len, t, d, from, to, c, h, hft, ht, hc):
1054  +rc = FA.rep(c)
1055  +MN = U32.min(FG(FA.words(from, to), U32.is_zero(M0(t, from, rc)), (from >> 2n : U32), M0(t, from, rc), rc, t), to)
1056  +SN = Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))
1057  %Equal.sym(D.Bytes & U32, FA.find(C.BT(len, t), from, to, c), (C.BT(len, t), MN), fast_eq(len, t, from, to, c)) :
1058    {_ == B.find(C.BT(len, t), from, to, c) : D.Bytes & U32}
1059  %Equal.sym(D.Bytes & U32, B.find(C.BT(len, t), from, to, c), (C.BT(len, t), SN), F.find_pair_t(len, t, from, to, c)) :
1060    {(C.BT(len, t), MN) == _ : D.Bytes & U32}
1061  Equal.cong(U32, D.Bytes & U32, y => (C.BT(len, t), y), MN, SN,
1062    U.to_nat_inj(MN, SN, Equal.trans(Nat, U32.to_nat(MN), D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c), U32.to_nat(SN),
1063      fview_go(U32.is_le(to, from), len, t, d, from, to, c, h, hft, ht, hc, {==}),
1064      Equal.sym(Nat, U32.to_nat(SN), D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c), F.find_view_t(len, t, d, from, to, c, h, hft, ht, hc)))))