proof_fast_find2.bend
lawful-bytes@0.1.0.0 · 704 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/fast.bend as FA
5import lawful-bytes@0.1.0.0/proof_seq.bend as Q
6import lawful-bytes@0.1.0.0/proof_core.bend as C
7import lawful-bytes@0.1.0.0/proof_find.bend as F
8import lawful-bytes@0.1.0.0/proof_append.bend as X
9import lawful-bytes@0.1.0.0/proof_shift.bend as H
10import lawful-bytes@0.1.0.0/proof_fast_word.bend as FW
11import lawful-bytes@0.1.0.0/proof_fast_find.bend as FF
12import lawful-words@0.1.0.0/defs.bend as W
13import lawful-words@0.1.0.0/proof_nat.bend as N
14import lawful-words@0.1.0.0/proof_u32.bend as U
15import lawful-arrays@0.1.0.0/proof_base.bend as AB
16import lawful-arrays@0.1.0.0/proof_tree.bend as P
17import lawful-arrays@0.1.0.0/defs.bend as A
18
19# fast.bend's find2 on the mirror, the same way as find (proof_fast_find.bend,
20# whose word and list lemmas are reused): the mask is the or of two flag
21# words, its place the min of their places, and the spec run_len2/first2.
22
23# Whether the head of a list is c1 or c2.
24def hd2(xs: List<&2, U32>, +c1: U32, +c2: U32) -> Bool:
25 match xs:
26 case Nil{}:
27 False{}
28 case Con{+x, t}:
29 U32.is_eq(x, c1) || U32.is_eq(x, c2)
30
31def FG2(n: Nat, z: Bool, +wi: U32, +m: U32, +r1: U32, +r2: U32, +t: P.Tree<U32>) -> U32:
32 match n z:
33 case 0n _:
34 4294967295
35 case 1n+k True{}:
36 +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
37 FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
38 case 1n+k False{}:
39 ((wi << 2n : U32) + FA.bidx(m) : U32)
40
41law fg2_eq:
42 for +n: Nat
43 for +z: Bool
44 for +wi: U32
45 for +m: U32
46 for +r1: U32
47 for +r2: U32
48 for +t: P.Tree<U32>
49 {FA.find2.go(n, z, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), wi, m, r1, r2) == (P.fromT(U32, t), FG2(n, z, wi, m, r1, r2, t)) : Array<U32> & U32}
50
51def fg2_eq(n, z, wi, m, r1, r2, t):
52 match n z:
53 case 0n _:
54 %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))) :
55 {FA.find2.go(0n, z, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(0n, z, wi, m, r1, r2, t)) : Array<U32> & U32}
56 {==}
57 case 1n+k True{}:
58 +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
59 %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))) :
60 {FA.find2.go(1n+k, True{}, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(1n+k, True{}, wi, m, r1, r2, t)) : Array<U32> & U32}
61 %F.add11(wi) :
62 {FA.find2.go(k, U32.is_zero(m2), Array.get(U32, P.fromT(U32, t), _), (wi + 1 : U32), m2, r1, r2) == (P.fromT(U32, t), FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)) : Array<U32> & U32}
63 fg2_eq(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
64 case 1n+k False{}:
65 %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))) :
66 {FA.find2.go(1n+k, False{}, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(1n+k, False{}, wi, m, r1, r2, t)) : Array<U32> & U32}
67 {==}
68
69def M02(+t: P.Tree<U32>, +from: U32, +r1: U32, +r2: U32) -> U32:
70 (FA.zb(((C.WD(t, (from >> 2n : U32)) .^. r1 : U32) .|. U32.not(FA.low(from)) : U32)) .|. FA.zb(((C.WD(t, (from >> 2n : U32)) .^. r2 : U32) .|. U32.not(FA.low(from)) : U32)) : U32)
71
72law fast2_eq:
73 for +len: U32
74 for +t: P.Tree<U32>
75 for +from: U32
76 for +to: U32
77 for +c1: U32
78 for +c2: U32
79 {FA.find2(C.BT(len, t), from, to, c1, c2) == (C.BT(len, t), U32.min(FG2(FA.words(from, to), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) : D.Bytes & U32}
80
81def fast2_eq(len, t, from, to, c1, c2):
82 +k = (from >> 2n : U32)
83 +r1 = FA.rep(c1)
84 +r2 = FA.rep(c2)
85 +n = FA.words(from, to)
86 %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)) :
87 {FA.find.k(len, FA.find.fin(to, FA.find2.start(n, _, from, r1, r2))) == (C.BT(len, t), U32.min(FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t), to)) : D.Bytes & U32}
88 %Equal.sym(Array<U32> & U32, FA.find2.go(n, U32.is_zero(M02(t, from, r1, r2)), Array.get(U32, P.fromT(U32, t), (k + 1 : U32)), k, M02(t, from, r1, r2), r1, r2),
89 (P.fromT(U32, t), FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t)), fg2_eq(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t)) :
90 {FA.find.k(len, FA.find.fin(to, _)) == (C.BT(len, t), U32.min(FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t), to)) : D.Bytes & U32}
91 {==}
92
93# Two runs and their min
94# ======================
95
96law min_le_l:
97 for +a: Nat
98 for +b: Nat
99 {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}
100
101def min_le_l(a, b):
102 match a b:
103 case 0n _:
104 {==}
105 case 1n+p 0n:
106 {==}
107 case 1n+p 1n+q:
108 min_le_l(p, q)
109
110law min_le4:
111 for +v1: U32
112 for +v2: U32
113 {Nat.is_le(Nat.min(FW.P0(v1), FW.P0(v2)), 4n) == True{} : Bool}
114
115def min_le4(v1, v2):
116 N.le_trans(Nat.min(FW.P0(v1), FW.P0(v2)), FW.P0(v1), 4n, min_le_l(FW.P0(v1), FW.P0(v2)), FF.run_le(C.L4(v1), 0, FF.hd_eq(C.L4(v1), 0), {==}))
117
118law min_add:
119 for +o: Nat
120 for +a: Nat
121 for +b: Nat
122 {Nat.min(Nat.add(o, a), Nat.add(o, b)) == Nat.add(o, Nat.min(a, b)) : Nat}
123
124def min_add(o, a, b):
125 match o:
126 case 0n:
127 {==}
128 case 1n+p:
129 %min_add(p, a, b) : {1n+Nat.min(Nat.add(p, a), Nat.add(p, b)) == 1n+_ : Nat}
130 {==}
131
132# The first c1 or c2 is the earlier of the first c1 and the first c2.
133law min_run:
134 for +xs: List<&2, U32>
135 for +c1: U32
136 for +c2: U32
137 for +b1: Bool
138 for +b2: Bool
139 for +hb1: {FF.hd_eq(xs, c1) == b1 : Bool}
140 for +hb2: {FF.hd_eq(xs, c2) == b2 : Bool}
141 {Nat.min(D.run_len(xs, c1), D.run_len(xs, c2)) == D.run_len2(xs, c1, c2) : Nat}
142
143def min_run(xs, c1, c2, b1, b2, hb1, hb2):
144 match xs b1 b2:
145 case Nil{} _ _:
146 {==}
147 case Con{x, t} True{} _:
148 %Equal.sym(Bool, FF.hd_eq(x <> t, c1), True{}, hb1) :
149 {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
150 {==}
151 case Con{x, t} False{} True{}:
152 %Equal.sym(Bool, FF.hd_eq(x <> t, c1), False{}, hb1) :
153 {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
154 %Equal.sym(Bool, FF.hd_eq(x <> t, c2), True{}, hb2) :
155 {Nat.min(1n+D.run_len(t, c1), Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(False{}, _), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
156 {==}
157 case Con{x, t} False{} False{}:
158 %Equal.sym(Bool, FF.hd_eq(x <> t, c1), False{}, hb1) :
159 {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
160 %Equal.sym(Bool, FF.hd_eq(x <> t, c2), False{}, hb2) :
161 {Nat.min(1n+D.run_len(t, c1), Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(False{}, _), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
162 %min_run(t, c1, c2, FF.hd_eq(t, c1), FF.hd_eq(t, c2), {==}, {==}) : {1n+Nat.min(D.run_len(t, c1), D.run_len(t, c2)) == 1n+_ : Nat}
163 {==}
164
165# The first word of a search, for two values.
166law p0_low2:
167 for +w: U32
168 for +c1: U32
169 for +c2: U32
170 for +i: U32
171 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
172 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
173 {Nat.min(FW.P0(U32.or(U32.xor(w, FA.rep(c1)), U32.not(FA.low(i)))), FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i))))) == Nat.add(U32.to_nat((i .&. 3 : U32)), D.run_len2(List.drop(&2, U32, C.L4(w), U32.to_nat((i .&. 3 : U32))), c1, c2)) : Nat}
174
175def p0_low2(w, c1, c2, i, hc1, hc2):
176 +o = U32.to_nat((i .&. 3 : U32))
177 +ys = List.drop(&2, U32, C.L4(w), o)
178 %Equal.sym(Nat, FW.P0(U32.or(U32.xor(w, FA.rep(c1)), U32.not(FA.low(i)))), Nat.add(o, D.run_len(ys, c1)), FW.p0_low(w, c1, i, hc1)) :
179 {Nat.min(_, FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i))))) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
180 %Equal.sym(Nat, FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i)))), Nat.add(o, D.run_len(ys, c2)), FW.p0_low(w, c2, i, hc2)) :
181 {Nat.min(Nat.add(o, D.run_len(ys, c1)), _) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
182 %Equal.sym(Nat, Nat.min(Nat.add(o, D.run_len(ys, c1)), Nat.add(o, D.run_len(ys, c2))), Nat.add(o, Nat.min(D.run_len(ys, c1), D.run_len(ys, c2))), min_add(o, D.run_len(ys, c1), D.run_len(ys, c2))) :
183 {_ == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
184 %Equal.sym(Nat, Nat.min(D.run_len(ys, c1), D.run_len(ys, c2)), D.run_len2(ys, c1, c2), min_run(ys, c1, c2, FF.hd_eq(ys, c1), FF.hd_eq(ys, c2), {==}, {==})) :
185 {Nat.add(o, _) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
186 {==}
187
188# The next word starts a fresh search.
189law hv02:
190 for +t: P.Tree<U32>
191 for +wi: U32
192 for +c1: U32
193 for +c2: U32
194 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
195 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
196 {Nat.min(FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == Nat.add(0n, D.run_len2(FF.AW(t, wi, 0n), c1, c2)) : Nat}
197
198def hv02(t, wi, c1, c2, hc1, hc2):
199 +ws = C.L4(C.WD(t, wi))
200 %Equal.sym(List<&2, U32>, List.drop(&2, U32, ws, 0n), ws, X.drop_zero(ws)) :
201 {Nat.min(FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == Nat.add(0n, D.run_len2(_, c1, c2)) : Nat}
202 %Equal.sym(Nat, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), D.run_len(ws, c1), FW.p0_xor(C.WD(t, wi), c1, hc1)) :
203 {Nat.min(_, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == D.run_len2(ws, c1, c2) : Nat}
204 %Equal.sym(Nat, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2))), D.run_len(ws, c2), FW.p0_xor(C.WD(t, wi), c2, hc2)) :
205 {Nat.min(D.run_len(ws, c1), _) == D.run_len2(ws, c1, c2) : Nat}
206 min_run(ws, c1, c2, FF.hd_eq(ws, c1), FF.hd_eq(ws, c2), {==}, {==})
207
208# The word loop (from proof_fast_find.bend, for two values)
209# =========================================================
210
211law run_hit2:
212 for +xs: List<&2, U32>
213 for +ys: List<&2, U32>
214 for +n: Nat
215 for +c1: U32
216 for +c2: U32
217 for +b: Bool
218 for +hb: {hd2(xs, c1, c2) == b : Bool}
219 for +h: {Nat.is_lt(D.run_len2(xs, c1, c2), List.length(&2, U32, xs)) == True{} : Bool}
220 {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == Nat.min(D.run_len2(xs, c1, c2), n) : Nat}
221
222def run_hit2(xs, ys, n, c1, c2, b, hb, h):
223 match xs n b:
224 case Nil{} _ _:
225 Empty.absurd({D.run_len2(List.take(&2, U32, ys, n), c1, c2) == Nat.min(0n, n) : Nat}, AB.lt_zero_absurd(0n, h))
226 case Con{x, t} 0n True{}:
227 %Equal.sym(Bool, hd2(x <> t, c1, c2), True{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 0n) : Nat}
228 {==}
229 case Con{x, t} 0n False{}:
230 %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 0n) : Nat}
231 {==}
232 case Con{x, t} 1n+p True{}:
233 %Equal.sym(Bool, hd2(x <> t, c1, c2), True{}, hb) :
234 {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+p) : Nat}
235 {==}
236 case Con{x, t} 1n+p False{}:
237 %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
238 {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+p) : Nat}
239 +h2 = AB.subst(Bool, y => {Nat.is_lt(Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+List.length(&2, U32, t)) == True{} : Bool},
240 hd2(x <> t, c1, c2), False{}, hb, h)
241 %run_hit2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2) :
242 {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
243 {==}
244
245law run_skip2:
246 for +xs: List<&2, U32>
247 for +ys: List<&2, U32>
248 for +n: Nat
249 for +c1: U32
250 for +c2: U32
251 for +b: Bool
252 for +hb: {hd2(xs, c1, c2) == b : Bool}
253 for +h: {D.run_len2(xs, c1, c2) == List.length(&2, U32, xs) : Nat}
254 for +hn: {Nat.is_le(List.length(&2, U32, xs), n) == True{} : Bool}
255 {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == Nat.add(List.length(&2, U32, xs), D.run_len2(List.take(&2, U32, ys, Nat.sub(n, List.length(&2, U32, xs))), c1, c2)) : Nat}
256
257def run_skip2(xs, ys, n, c1, c2, b, hb, h, hn):
258 match xs n b:
259 case Nil{} _ _:
260 %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) :
261 {D.run_len2(List.take(&2, U32, ys, n), c1, c2) == D.run_len2(List.take(&2, U32, ys, _), c1, c2) : Nat}
262 {==}
263 case Con{x, t} _ True{}:
264 Empty.absurd({D.run_len2(List.take(&2, U32, List.append(&2, U32, x <> t, ys), n), c1, c2) == Nat.add(1n+List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(n, 1n+List.length(&2, U32, t))), c1, c2)) : Nat},
265 N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat},
266 hd2(x <> t, c1, c2), True{}, hb, h)))
267 case Con{x, t} 0n False{}:
268 Empty.absurd({0n == Nat.add(1n+List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(0n, 1n+List.length(&2, U32, t))), c1, c2)) : Nat},
269 AB.false_ne_true(hn))
270 case Con{x, t} 1n+p False{}:
271 %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
272 {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == 1n+Nat.add(List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(p, List.length(&2, U32, t))), c1, c2)) : Nat}
273 +h2 = N.succ_inj(D.run_len2(t, c1, c2), List.length(&2, U32, t),
274 AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat}, hd2(x <> t, c1, c2), False{}, hb, h))
275 %run_skip2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2, hn) :
276 {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
277 {==}
278
279law run_none2:
280 for +xs: List<&2, U32>
281 for +ys: List<&2, U32>
282 for +n: Nat
283 for +c1: U32
284 for +c2: U32
285 for +b: Bool
286 for +hb: {hd2(xs, c1, c2) == b : Bool}
287 for +h: {D.run_len2(xs, c1, c2) == List.length(&2, U32, xs) : Nat}
288 for +hn: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
289 {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == n : Nat}
290
291def run_none2(xs, ys, n, c1, c2, b, hb, h, hn):
292 match xs n b:
293 case Nil{} 0n _:
294 %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {D.run_len2(_, c1, c2) == 0n : Nat}
295 {==}
296 case Nil{} 1n+p _:
297 Empty.absurd({D.run_len2(List.take(&2, U32, ys, 1n+p), c1, c2) == 1n+p : Nat}, AB.false_ne_true(hn))
298 case Con{x, t} 0n _:
299 {==}
300 case Con{x, t} 1n+p True{}:
301 Empty.absurd({D.run_len2(List.take(&2, U32, List.append(&2, U32, x <> t, ys), 1n+p), c1, c2) == 1n+p : Nat},
302 N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat},
303 hd2(x <> t, c1, c2), True{}, hb, h)))
304 case Con{x, t} 1n+p False{}:
305 %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
306 {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == 1n+p : Nat}
307 +h2 = N.succ_inj(D.run_len2(t, c1, c2), List.length(&2, U32, t),
308 AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat}, hd2(x <> t, c1, c2), False{}, hb, h))
309 %run_none2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2, hn) : {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
310 {==}
311
312law fhit2:
313 for +len: U32
314 for +t: P.Tree<U32>
315 for +d: Nat
316 for +to: U32
317 for +c1: U32
318 for +c2: U32
319 for +wi: U32
320 for +o: Nat
321 for +v1: U32
322 for +v2: U32
323 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
324 for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
325 for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
326 for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
327 for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
328 for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
329 for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == False{} : Bool}
330 {U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
331
332def fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs, hk, hv, hz):
333 +W = U32.to_nat(wi)
334 +T = U32.to_nat(to)
335 +r = D.run_len2(FF.AW(t, wi, o), c1, c2)
336 +M4 = Nat.mul(4n, Nat.pow(2n, d))
337 +hd = C.ok_d(len, t, d, h)
338 +hf = C.ok_full(len, t, d, h)
339 +hp4 = min_le4(v1, v2)
340 +hne = Equal.trans(Bool, Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), False{}, Equal.sym(Bool, U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), FW.zb2_none(v1, v2)), hz)
341 +hlt = Equal.trans(Bool, Nat.is_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), Nat.is_le(1n+Nat.min(FW.P0(v1), FW.P0(v2)), 4n), True{}, Equal.sym(Bool, Nat.is_le(1n+Nat.min(FW.P0(v1), FW.P0(v2)), 4n), Nat.is_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), N.le_succ_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n)),
342 N.le_ne(Nat.min(FW.P0(v1), FW.P0(v2)), 4n, hp4, hne))
343 +hlt2 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), hv, hlt)
344 +eo = N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))
345 +hrl0 = FF.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))
346 +hrl = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, FF.AW(t, wi, o)), Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)), hrl0)
347 +eb = Equal.trans(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), FW.zb2_bidx(v1, v2, hlt), hv)
348 +hw4 = FF.wb4(W, Nat.pow(2n, d), hk)
349 +esh = FF.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))
350 +b1 = N.le_trans(Nat.add(Nat.mul(W, 4n), Nat.add(o, r)), Nat.add(Nat.mul(W, 4n), 4n), M4,
351 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)
352 +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)
353 +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(U32.or(FA.zb(v1), FA.zb(v2)))),
354 Equal.sym(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.add(o, r), eb), b2)
355 +ej = C.add_fits((wi << 2n : U32), FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))), d, hd, b3)
356 +RHS = D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2)
357 %Equal.sym(Nat, U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)), Nat.min(U32.to_nat(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32)), T),
358 U.to_nat_min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)) :
359 {_ == RHS : Nat}
360 %Equal.sym(Nat, U32.to_nat(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32)), Nat.add(U32.to_nat((wi << 2n : U32)), U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))))), ej) :
361 {Nat.min(_, T) == RHS : Nat}
362 %Equal.sym(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.add(o, r), eb) :
363 {Nat.min(Nat.add(U32.to_nat((wi << 2n : U32)), _), T) == RHS : Nat}
364 %Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh) :
365 {Nat.min(Nat.add(_, Nat.add(o, r)), T) == RHS : Nat}
366 %N.add_assoc(Nat.mul(W, 4n), o, r) :
367 {Nat.min(_, T) == RHS : Nat}
368 %Equal.sym(Nat, Nat.min(Nat.add(FF.SS(wi, o), r), T), Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))), FF.min_shift(FF.SS(wi, o), r, T, hs)) :
369 {_ == RHS : Nat}
370 %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), FF.SS(wi, o)), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
371 {Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))) == Nat.add(FF.SS(wi, o), D.run_len2(List.take(&2, U32, _, Nat.sub(T, FF.SS(wi, o))), c1, c2)) : Nat}
372 %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), Nat.sub(T, FF.SS(wi, o))), c1, c2), Nat.min(r, Nat.sub(T, FF.SS(wi, o))),
373 run_hit2(FF.AW(t, wi, o), FF.BW(t, wi), Nat.sub(T, FF.SS(wi, o)), c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, hrl)) :
374 {Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))) == Nat.add(FF.SS(wi, o), _) : Nat}
375 {==}
376
377law nohit2:
378 for +t: P.Tree<U32>
379 for +wi: U32
380 for +o: Nat
381 for +v1: U32
382 for +v2: U32
383 for +c1: U32
384 for +c2: U32
385 for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
386 for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
387 {D.run_len2(FF.AW(t, wi, o), c1, c2) == List.length(&2, U32, FF.AW(t, wi, o)) : Nat}
388
389def nohit2(t, wi, o, v1, v2, c1, c2, hv, hz):
390 +r = D.run_len2(FF.AW(t, wi, o), c1, c2)
391 +e4 = N.eq_sound(Nat.min(FW.P0(v1), FW.P0(v2)), 4n, Equal.trans(Bool, Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), True{},
392 Equal.sym(Bool, U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), FW.zb2_none(v1, v2)), hz))
393 +e5 = Equal.trans(Nat, Nat.add(o, r), Nat.min(FW.P0(v1), FW.P0(v2)), 4n, Equal.sym(Nat, Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), hv), e4)
394 %Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)) : {r == _ : Nat}
395 %e5 : {r == Nat.sub(_, o) : Nat}
396 Equal.sym(Nat, Nat.sub(Nat.add(o, r), o), r, N.sub_add_l(o, r))
397
398law fnone2:
399 for +len: U32
400 for +t: P.Tree<U32>
401 for +d: Nat
402 for +to: U32
403 for +c1: U32
404 for +c2: U32
405 for +wi: U32
406 for +o: Nat
407 for +v1: U32
408 for +v2: U32
409 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
410 for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
411 for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
412 for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
413 for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
414 for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
415 for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
416 for +he: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)) == True{} : Bool}
417 {U32.to_nat(U32.min(4294967295, to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
418
419def fnone2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs, hk, hv, hz, he):
420 +W = U32.to_nat(wi)
421 +T = U32.to_nat(to)
422 +X = Nat.sub(T, FF.SS(wi, o))
423 +hd = C.ok_d(len, t, d, h)
424 +hf = C.ok_full(len, t, d, h)
425 +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), FF.mul4s(W), he)
426 +a2 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, T, Nat.add(FF.SS(wi, o), X),
427 Equal.sym(Nat, Nat.add(FF.SS(wi, o), X), T, N.le_sub_add(FF.SS(wi, o), T, hs)), a1)
428 +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)),
429 N.add_assoc(Nat.mul(W, 4n), o, X), a2)
430 +a4 = N.le_sub_r(o, X, 4n, FF.le_cancel(Nat.mul(W, 4n), Nat.add(o, X), 4n, a3))
431 +hn = AB.subst(Nat, y => {Nat.is_le(X, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, FF.AW(t, wi, o)),
432 Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)), a4)
433 +RHS = D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2)
434 %Equal.sym(U32, U32.min(4294967295, to), to, FF.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)))) :
435 {U32.to_nat(_) == RHS : Nat}
436 %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), FF.SS(wi, o)), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
437 {T == Nat.add(FF.SS(wi, o), D.run_len2(List.take(&2, U32, _, X), c1, c2)) : Nat}
438 %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), X), c1, c2), X,
439 run_none2(FF.AW(t, wi, o), FF.BW(t, wi), X, c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, nohit2(t, wi, o, v1, v2, c1, c2, hv, hz), hn)) :
440 {T == Nat.add(FF.SS(wi, o), _) : Nat}
441 Equal.sym(Nat, Nat.add(FF.SS(wi, o), X), T, N.le_sub_add(FF.SS(wi, o), T, hs))
442
443law fskip2:
444 for +len: U32
445 for +t: P.Tree<U32>
446 for +d: Nat
447 for +to: U32
448 for +c1: U32
449 for +c2: U32
450 for +wi: U32
451 for +o: Nat
452 for +v1: U32
453 for +v2: U32
454 for +k: Nat
455 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
456 for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
457 for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
458 for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
459 for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
460 for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
461 for +hs1: {Nat.is_le(Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to)) == True{} : Bool}
462 {D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) == D.first2(FF.UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to), c1, c2) : Nat}
463
464def fskip2(len, t, d, to, c1, c2, wi, o, v1, v2, k, h, ho, hs, hk, hv, hz, hs1):
465 +W = U32.to_nat(wi)
466 +T = U32.to_nat(to)
467 +S = FF.SS(wi, o)
468 +S1 = Nat.mul(Nat.add(W, 1n), 4n)
469 +L = Nat.sub(4n, o)
470 +hd = C.ok_d(len, t, d, h)
471 +hf = C.ok_full(len, t, d, h)
472 +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),
473 Equal.trans(Nat, Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), Nat.add(Nat.mul(W, 4n), 4n), S1,
474 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))),
475 Equal.sym(Nat, S1, Nat.add(Nat.mul(W, 4n), 4n), FF.mul4s(W))))
476 +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))
477 +hn = AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, S)) == True{} : Bool}, L, List.length(&2, U32, FF.AW(t, wi, o)),
478 Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), L, FF.awl(t, wi, o)), hl0)
479 +RHS = D.first2(FF.UB(t), S1, T, c1, c2)
480 %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), S), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
481 {Nat.add(S, D.run_len2(List.take(&2, U32, _, Nat.sub(T, S)), c1, c2)) == RHS : Nat}
482 %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), Nat.sub(T, S)), c1, c2),
483 Nat.add(List.length(&2, U32, FF.AW(t, wi, o)), D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(Nat.sub(T, S), List.length(&2, U32, FF.AW(t, wi, o)))), c1, c2)),
484 run_skip2(FF.AW(t, wi, o), FF.BW(t, wi), Nat.sub(T, S), c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, nohit2(t, wi, o, v1, v2, c1, c2, hv, hz), hn)) :
485 {Nat.add(S, _) == RHS : Nat}
486 %Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), L, FF.awl(t, wi, o)) :
487 {Nat.add(S, Nat.add(_, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(Nat.sub(T, S), _)), c1, c2))) == RHS : Nat}
488 %Equal.sym(Nat, Nat.sub(Nat.sub(T, S), L), Nat.sub(T, Nat.add(S, L)), FF.sub_sub(T, S, L)) :
489 {Nat.add(S, Nat.add(L, D.run_len2(List.take(&2, U32, FF.BW(t, wi), _), c1, c2))) == RHS : Nat}
490 %N.add_assoc(S, L, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(T, Nat.add(S, L))), c1, c2)) :
491 {_ == RHS : Nat}
492 %Equal.sym(Nat, Nat.add(S, L), S1, eS) :
493 {Nat.add(_, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(T, _)), c1, c2)) == RHS : Nat}
494 {==}
495
496law fi2:
497 for +k: Nat
498 for +z: Bool
499 for +len: U32
500 for +t: P.Tree<U32>
501 for +d: Nat
502 for +to: U32
503 for +c1: U32
504 for +c2: U32
505 for +wi: U32
506 for +o: Nat
507 for +v1: U32
508 for +v2: U32
509 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
510 for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
511 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
512 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
513 for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
514 for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
515 for +he1: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n+k), 4n)) == True{} : Bool}
516 for +he2: {Nat.is_lt(Nat.mul(Nat.add(U32.to_nat(wi), k), 4n), U32.to_nat(to)) == True{} : Bool}
517 for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
518 for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == z : Bool}
519 {U32.to_nat(U32.min(FG2(1n+k, z, wi, U32.or(FA.zb(v1), FA.zb(v2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
520
521def fi2(k, z, len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, hc1, hc2, ho, hs, he1, he2, hv, hz):
522 match k z:
523 case 0n False{}:
524 fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
525 FF.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)
526 case 1n+q False{}:
527 fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
528 FF.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)
529 case 0n True{}:
530 fnone2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
531 FF.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)
532 case 1n+q True{}:
533 +W = U32.to_nat(wi)
534 +T = U32.to_nat(to)
535 +j1 = (wi + 1 : U32)
536 +n1 = U32.xor(C.WD(t, j1), FA.rep(c1))
537 +n2 = U32.xor(C.WD(t, j1), FA.rep(c2))
538 +S1 = Nat.mul(Nat.add(W, 1n), 4n)
539 +hk = FF.wlt(W, 1n+q, T, U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h))
540 +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, FF.pow_le4(Nat.pow(2n, d))))
541 +hs1 = N.lt_to_le(S1, T, N.le_lt_trans(S1, Nat.mul(Nat.add(W, 1n+q), 4n), T,
542 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))
543 +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)),
544 Equal.cong(Nat, Nat, y => Nat.mul(y, 4n), U32.to_nat(j1), Nat.add(W, 1n), ej1))
545 +hsi = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, FF.SS(j1, 0n), Equal.sym(Nat, FF.SS(j1, 0n), S1, ea), hs1)
546 +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)),
547 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))
548 +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),
549 Equal.sym(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(W, 1n+(1n+q)), e1), he1)
550 +e2 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(Nat.add(W, 1n), q), Nat.add(W, 1n+q),
551 Equal.cong(Nat, Nat, y => Nat.add(y, q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, q))
552 +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),
553 Equal.sym(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(W, 1n+q), e2), he2)
554 +ih = fi2(q, U32.is_zero(U32.or(FA.zb(n1), FA.zb(n2))), len, t, d, to, c1, c2, j1, 0n, n1, n2, h, ht, hc1, hc2, {==}, hsi, he1i, he2i, hv02(t, j1, c1, c2, hc1, hc2), {==})
555 +sk = fskip2(len, t, d, to, c1, c2, wi, o, v1, v2, q, h, ho, hs, hk, hv, hz, hs1)
556 Equal.trans(Nat, U32.to_nat(U32.min(FG2(1n+q, U32.is_zero(U32.or(FA.zb(n1), FA.zb(n2))), j1, U32.or(FA.zb(n1), FA.zb(n2)), FA.rep(c1), FA.rep(c2), t), to)), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2), D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2),
557 ih, Equal.sym(Nat, D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2),
558 Equal.trans(Nat, D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2), D.first2(FF.UB(t), S1, T, c1, c2), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2), sk,
559 Equal.cong(Nat, Nat, y => D.first2(FF.UB(t), y, T, c1, c2), S1, FF.SS(j1, 0n), Equal.sym(Nat, FF.SS(j1, 0n), S1, ea)))))
560
561law fview2_lt:
562 for +len: U32
563 for +t: P.Tree<U32>
564 for +d: Nat
565 for +from: U32
566 for +to: U32
567 for +c1: U32
568 for +c2: U32
569 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
570 for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
571 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
572 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
573 for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
574 {U32.to_nat(U32.min(FG2(U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
575
576def fview2_lt(len, t, d, from, to, c1, c2, h, ht, hc1, hc2, hlt):
577 +F = U32.to_nat(from)
578 +T = U32.to_nat(to)
579 +wi0 = (from >> 2n : U32)
580 +W0 = U32.to_nat(wi0)
581 +o0 = U32.to_nat((from .&. 3 : U32))
582 +ee = ((to - 1 : U32) >> 2n : U32)
583 +E = U32.to_nat(ee)
584 +rc1 = FA.rep(c1)
585 +rc2 = FA.rep(c2)
586 +hd = C.ok_d(len, t, d, h)
587 +M4 = Nat.mul(4n, Nat.pow(2n, d))
588 +hTM = N.le_trans(T, U32.to_nat(len), M4, ht, C.ok_len(len, t, d, h))
589 +h0T = N.le_lt_trans(0n, F, T, N.le_zero_l(F), hlt)
590 +eW0 = U.to_nat_shrn(from, 2n)
591 +eo = U.to_nat_and_mask(from, 3, 2n, {==})
592 +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),
593 Equal.trans(Bool, Nat.is_le(1n, T), Nat.is_lt(0n, T), True{}, N.le_succ_lt(0n, T), h0T)))
594 +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),
595 Equal.cong(Nat, Nat, y => Nat.div(y, 4n), U32.to_nat((to - 1 : U32)), Nat.sub(T, 1n), et1))
596 +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),
597 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),
598 FF.div_le4(F, Nat.sub(T, 1n), FF.lt_sub1(F, T, hlt))))
599 +k0 = Nat.sub(E, W0)
600 +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))
601 +hET = N.le_lt_trans(E, Nat.sub(T, 1n), T,
602 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), FF.div_self_le(Nat.sub(T, 1n))),
603 FF.sub1_lt(T, h0T))
604 +ek = C.inc_fits((ee - wi0 : U32), d, hd,
605 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),
606 N.le_lt_trans(k0, E, M4, H.sub_le(E, W0), N.lt_le_trans(E, T, M4, hET, hTM))))
607 +en = Equal.trans(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), 1n+k0, ek,
608 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)))
609 +eSF = Equal.trans(Nat, FF.SS(wi0, o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)), F,
610 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)),
611 Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(y, 4n), o0), W0, Nat.div(F, 4n), eW0),
612 Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(Nat.div(F, 4n), 4n), y), o0, Nat.mod(F, 4n), eo)),
613 N.div_mod(F, 4n))
614 +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, {==}))
615 +hs0 = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, F, FF.SS(wi0, o0), Equal.sym(Nat, FF.SS(wi0, o0), F, eSF), N.lt_to_le(F, T, hlt))
616 +eWk = N.le_sub_add(W0, E, hWE)
617 +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),
618 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),
619 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)),
620 Equal.cong(Nat, Nat, y => Nat.add(y, 1n), E, Nat.div(Nat.sub(T, 1n), 4n), eE))))
621 +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),
622 Equal.sym(Nat, Nat.add(W0, 1n+k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), eA), FF.last_le(T, h0T))
623 +eB = Equal.trans(Nat, Nat.add(W0, k0), E, Nat.div(Nat.sub(T, 1n), 4n), eWk, eE)
624 +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),
625 Equal.sym(Nat, Nat.add(W0, k0), Nat.div(Nat.sub(T, 1n), 4n), eB), FF.last_lt(T, h0T))
626 +fiv = fi2(k0, U32.is_zero(M02(t, from, rc1, rc2)), len, t, d, to, c1, c2, wi0, o0, U32.or(U32.xor(C.WD(t, wi0), rc1), U32.not(FA.low(from))), U32.or(U32.xor(C.WD(t, wi0), rc2), U32.not(FA.low(from))),
627 h, ht, hc1, hc2, ho0, hs0, he1, he2, p0_low2(C.WD(t, wi0), c1, c2, from, hc1, hc2), {==})
628 +hh = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, T, Nat.add(F, Nat.sub(T, F)),
629 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)
630 +E2 = Equal.trans(Nat, D.first2(FF.UB(t), FF.SS(wi0, o0), T, c1, c2), D.first2(FF.UB(t), F, T, c1, c2), D.first2(D.view(C.BT(len, t)), F, T, c1, c2),
631 Equal.cong(Nat, Nat, y => D.first2(FF.UB(t), y, T, c1, c2), FF.SS(wi0, o0), F, eSF),
632 Equal.sym(Nat, D.first2(D.view(C.BT(len, t)), F, T, c1, c2), D.first2(FF.UB(t), F, T, c1, c2),
633 Equal.cong(List<&2, U32>, Nat, y => Nat.add(F, D.run_len2(y, c1, c2)), D.slice(List.take(&2, U32, FF.UB(t), U32.to_nat(len)), F, Nat.sub(T, F)), D.slice(FF.UB(t), F, Nat.sub(T, F)),
634 FF.slice_take(FF.UB(t), U32.to_nat(len), F, Nat.sub(T, F), hh))))
635 %Equal.sym(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), 1n+k0, en) :
636 {U32.to_nat(U32.min(FG2(_, U32.is_zero(M02(t, from, rc1, rc2)), wi0, M02(t, from, rc1, rc2), rc1, rc2, t), to)) == D.first2(D.view(C.BT(len, t)), F, T, c1, c2) : Nat}
637 Equal.trans(Nat, U32.to_nat(U32.min(FG2(1n+k0, U32.is_zero(M02(t, from, rc1, rc2)), wi0, M02(t, from, rc1, rc2), rc1, rc2, t), to)), D.first2(FF.UB(t), FF.SS(wi0, o0), T, c1, c2),
638 D.first2(D.view(C.BT(len, t)), F, T, c1, c2), fiv, E2)
639
640law fview2_go:
641 for +b: Bool
642 for +len: U32
643 for +t: P.Tree<U32>
644 for +d: Nat
645 for +from: U32
646 for +to: U32
647 for +c1: U32
648 for +c2: U32
649 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
650 for +hft: {U32.is_le(from, to) == True{} : Bool}
651 for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
652 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
653 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
654 for +hb: {U32.is_le(to, from) == b : Bool}
655 {U32.to_nat(U32.min(FG2(Bool.pick(Nat, b, 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32))), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
656
657def fview2_go(b, len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2, hb):
658 match b:
659 case True{}:
660 +F = U32.to_nat(from)
661 +T = U32.to_nat(to)
662 +xs = D.view(C.BT(len, t))
663 +hd = C.ok_d(len, t, d, h)
664 +eTF = FF.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),
665 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))
666 %Equal.sym(U32, U32.min(4294967295, to), to, FF.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)))) :
667 {U32.to_nat(_) == D.first2(xs, F, T, c1, c2) : Nat}
668 %Equal.sym(Nat, T, F, eTF) : {_ == D.first2(xs, F, _, c1, c2) : Nat}
669 %Equal.sym(Nat, Nat.sub(F, F), 0n, H.sub_self(F)) : {F == Nat.add(F, D.run_len2(D.slice(xs, F, _), c1, c2)) : Nat}
670 %Equal.sym(List<&2, U32>, D.slice(xs, F, 0n), Nil{}, X.slice_zero(xs, F)) : {F == Nat.add(F, D.run_len2(_, c1, c2)) : Nat}
671 Equal.sym(Nat, Nat.add(F, 0n), F, N.add_zero(F))
672 case False{}:
673 fview2_lt(len, t, d, from, to, c1, c2, h, ht, hc1, hc2,
674 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{},
675 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)))
676
677law fast_find2_t:
678 for +len: U32
679 for +t: P.Tree<U32>
680 for +d: Nat
681 for +from: U32
682 for +to: U32
683 for +c1: U32
684 for +c2: U32
685 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
686 for +hft: {U32.is_le(from, to) == True{} : Bool}
687 for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
688 for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
689 for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
690 {FA.find2(C.BT(len, t), from, to, c1, c2) == B.find2(C.BT(len, t), from, to, c1, c2) : D.Bytes & U32}
691
692def fast_find2_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
693 +rc1 = FA.rep(c1)
694 +rc2 = FA.rep(c2)
695 +MN = U32.min(FG2(FA.words(from, to), U32.is_zero(M02(t, from, rc1, rc2)), (from >> 2n : U32), M02(t, from, rc1, rc2), rc1, rc2, t), to)
696 +SN = Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))
697 %Equal.sym(D.Bytes & U32, FA.find2(C.BT(len, t), from, to, c1, c2), (C.BT(len, t), MN), fast2_eq(len, t, from, to, c1, c2)) :
698 {_ == B.find2(C.BT(len, t), from, to, c1, c2) : D.Bytes & U32}
699 %Equal.sym(D.Bytes & U32, B.find2(C.BT(len, t), from, to, c1, c2), (C.BT(len, t), SN), F.find2_pair_t(len, t, from, to, c1, c2)) :
700 {(C.BT(len, t), MN) == _ : D.Bytes & U32}
701 Equal.cong(U32, D.Bytes & U32, y => (C.BT(len, t), y), MN, SN,
702 U.to_nat_inj(MN, SN, Equal.trans(Nat, U32.to_nat(MN), D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2), U32.to_nat(SN),
703 fview2_go(U32.is_le(to, from), len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2, {==}),
704 Equal.sym(Nat, U32.to_nat(SN), D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2), F.find2_view_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2)))))