proof_num.bend
lawful-fields@0.1.0.0 · 676 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-fields@0.1.0.0/defs.bend as F
5import lawful-fields@0.1.0.0/fields.bend as C
6import lawful-bytes@0.1.0.0/proof_seq.bend as Q
7import lawful-bytes@0.1.0.0/proof_core.bend as K
8import lawful-bytes@0.1.0.0/proof_append.bend as X
9import lawful-words@0.1.0.0/proof_nat.bend as N
10import lawful-words@0.1.0.0/proof_u32.bend as U
11import lawful-arrays@0.1.0.0/proof_base.bend as AB
12import lawful-arrays@0.1.0.0/proof_tree.bend as P
13
14# num on the mirror K.BT(len, t). The checker normalizes both sides of any
15# conversion that is not a syntactic identity, and normalizing 2^32, or
16# U32.to_nat of a large word such as 429496729, overflows. So the lemmas take
17# the bound M (with hm : 2^32 == M) and q = to_nat(429496729) as variables,
18# and only num_view_t instantiates them, in a type that matches syntactically.
19
20# 2^32 and the overflow constant, kept abstract
21# =============================================
22
23# A bound below M gives the bound below 2^32 that lawful-words' lemmas want.
24law lift:
25 for +x: Nat
26 for +M: Nat
27 for +hm: {Nat.pow(2n, 32n) == M : Nat}
28 for +h: {Nat.is_lt(x, M) == True{} : Bool}
29 {Nat.is_lt(x, Nat.pow(2n, 32n)) == True{} : Bool}
30
31def lift(x, M, hm, h):
32 %Equal.sym(Nat, Nat.pow(2n, 32n), M, hm) : {Nat.is_lt(x, _) == True{} : Bool}
33 h
34
35law posM:
36 for +M: Nat
37 for +hm: {Nat.pow(2n, 32n) == M : Nat}
38 {Nat.is_lt(0n, M) == True{} : Bool}
39
40def posM(M, hm):
41 %hm : {Nat.is_lt(0n, _) == True{} : Bool}
42 AB.pow_pos(32n)
43
44law notM:
45 for +M: Nat
46 for +hm: {Nat.pow(2n, 32n) == M : Nat}
47 {U32.to_nat(U32.not(0)) == Nat.sub(Nat.sub(M, 1n), U32.to_nat(0)) : Nat}
48
49def notM(M, hm):
50 %hm : {U32.to_nat(U32.not(0)) == Nat.sub(Nat.sub(_, 1n), U32.to_nat(0)) : Nat}
51 U.to_nat_not_p(0)
52
53law ED:
54 {U32.div(U32.not(0), 10) == 429496729 : U32}
55
56def ED():
57 {==}
58
59law EM:
60 {U32.mod(U32.not(0), 10) == 5 : U32}
61
62def EM():
63 {==}
64
65law QD:
66 {Nat.div(U32.to_nat(U32.not(0)), U32.to_nat(10)) == U32.to_nat(429496729) : Nat}
67
68def QD():
69 %ED() : {Nat.div(U32.to_nat(U32.not(0)), U32.to_nat(10)) == U32.to_nat(_) : Nat}
70 Equal.sym(Nat, U32.to_nat(U32.div(U32.not(0), 10)), Nat.div(U32.to_nat(U32.not(0)), U32.to_nat(10)), U.to_nat_div(U32.not(0), 10))
71
72law QR:
73 {Nat.mod(U32.to_nat(U32.not(0)), U32.to_nat(10)) == U32.to_nat(5) : Nat}
74
75def QR():
76 %EM() : {Nat.mod(U32.to_nat(U32.not(0)), U32.to_nat(10)) == U32.to_nat(_) : Nat}
77 Equal.sym(Nat, U32.to_nat(U32.mod(U32.not(0), 10)), Nat.mod(U32.to_nat(U32.not(0)), U32.to_nat(10)), U.to_nat_mod(U32.not(0), 10))
78
79law succ_pred:
80 for +M: Nat
81 for +h: {Nat.is_lt(0n, M) == True{} : Bool}
82 {1n+Nat.sub(M, 1n) == M : Nat}
83
84def succ_pred(M, h):
85 match M:
86 case 0n:
87 Empty.absurd({1n+Nat.sub(0n, 1n) == 0n : Nat}, AB.false_ne_true(h))
88 case 1n+p:
89 %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {1n+_ == 1n+p : Nat}
90 {==}
91
92law qg1:
93 for +N1: Nat
94 for +Qn: Nat
95 for +R: Nat
96 for +T: Nat
97 for +M: Nat
98 for +hdm: {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == N1 : Nat}
99 for +hd: {Nat.div(N1, T) == Qn : Nat}
100 for +hr: {Nat.mod(N1, T) == R : Nat}
101 for +hT: {T == 10n : Nat}
102 for +hR: {R == 5n : Nat}
103 for +eN: {N1 == Nat.sub(M, 1n) : Nat}
104 {Nat.add(Nat.mul(Qn, 10n), 5n) == Nat.sub(M, 1n) : Nat}
105
106def qg1(N1, Qn, R, T, M, hdm, hd, hr, hT, hR, eN):
107 %hd : {Nat.add(Nat.mul(_, 10n), 5n) == Nat.sub(M, 1n) : Nat}
108 %hT : {Nat.add(Nat.mul(Nat.div(N1, T), _), 5n) == Nat.sub(M, 1n) : Nat}
109 %Equal.trans(Nat, Nat.mod(N1, T), R, 5n, hr, hR) : {Nat.add(Nat.mul(Nat.div(N1, T), T), _) == Nat.sub(M, 1n) : Nat}
110 %eN : {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == _ : Nat}
111 hdm
112
113# M = 10 q + 6, from 2^32 - 1 = 10 q + 5 with every number abstract.
114law QG:
115 for +N1: Nat
116 for +Qn: Nat
117 for +R: Nat
118 for +T: Nat
119 for +Z: Nat
120 for +M: Nat
121 for +hdm: {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == N1 : Nat}
122 for +hd: {Nat.div(N1, T) == Qn : Nat}
123 for +hr: {Nat.mod(N1, T) == R : Nat}
124 for +hT: {T == 10n : Nat}
125 for +hR: {R == 5n : Nat}
126 for +hZ: {Z == 0n : Nat}
127 for +hN: {N1 == Nat.sub(Nat.sub(M, 1n), Z) : Nat}
128 for +hM: {Nat.is_lt(0n, M) == True{} : Bool}
129 {Nat.add(Nat.mul(Qn, 10n), 6n) == M : Nat}
130
131def QG(N1, Qn, R, T, Z, M, hdm, hd, hr, hT, hR, hZ, hN, hM):
132 +eN = Equal.trans(Nat, N1, Nat.sub(Nat.sub(M, 1n), 0n), Nat.sub(M, 1n),
133 Equal.trans(Nat, N1, Nat.sub(Nat.sub(M, 1n), Z), Nat.sub(Nat.sub(M, 1n), 0n), hN,
134 Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(M, 1n), z), Z, 0n, hZ)),
135 N.sub_zero(Nat.sub(M, 1n)))
136 +e1 = qg1(N1, Qn, R, T, M, hdm, hd, hr, hT, hR, eN)
137 %Equal.sym(Nat, Nat.add(Nat.mul(Qn, 10n), 1n+5n), 1n+Nat.add(Nat.mul(Qn, 10n), 5n), N.add_succ(Nat.mul(Qn, 10n), 5n)) :
138 {_ == M : Nat}
139 %Equal.sym(Nat, Nat.add(Nat.mul(Qn, 10n), 5n), Nat.sub(M, 1n), e1) : {1n+_ == M : Nat}
140 succ_pred(M, hM)
141
142law QM:
143 for +M: Nat
144 for +hm: {Nat.pow(2n, 32n) == M : Nat}
145 {Nat.add(Nat.mul(U32.to_nat(429496729), 10n), 6n) == M : Nat}
146
147def QM(M, hm):
148 QG(U32.to_nat(U32.not(0)), U32.to_nat(429496729), U32.to_nat(5), U32.to_nat(10), U32.to_nat(0), M,
149 N.div_mod(U32.to_nat(U32.not(0)), U32.to_nat(10)), QD(), QR(), {==}, {==}, {==}, notM(M, hm), posM(M, hm))
150
151# The overflow test, as numbers
152# =============================
153
154# a < q, or a = q and k <= 5, exactly when 10a + k < 10q + 6 (k a digit).
155law FITS0:
156 for +a: Nat
157 for +q: Nat
158 for +k: Nat
159 for +hk: {Nat.is_le(k, 9n) == True{} : Bool}
160 {Bool.or(Nat.is_lt(a, q), Bool.and(Nat.is_eq(a, q), Nat.is_le(k, 5n))) == Nat.is_lt(Nat.add(Nat.mul(a, 10n), k), Nat.add(Nat.mul(q, 10n), 6n)) : Bool}
161
162def FITS0(a, q, k, hk):
163 match a q:
164 case 0n 0n:
165 Equal.sym(Bool, Nat.is_lt(k, 1n+5n), Nat.is_le(k, 5n), N.lt_succ_iff(k, 5n))
166 case 0n 1n+p:
167 +B = Nat.add(Nat.mul(1n+p, 10n), 6n)
168 Equal.sym(Bool, Nat.is_lt(k, B), True{},
169 N.lt_le_trans(k, 10n, B, Equal.trans(Bool, Nat.is_lt(k, 1n+9n), Nat.is_le(k, 9n), True{}, N.lt_succ_iff(k, 9n), hk),
170 N.le_add_r(10n, Nat.add(Nat.mul(p, 10n), 6n))))
171 case 1n+b 0n:
172 {==}
173 case 1n+b 1n+p:
174 FITS0(b, p, k, hk)
175
176law sub_mono:
177 for +a: Nat
178 for +b: Nat
179 for +c: Nat
180 for +h: {Nat.is_le(a, b) == True{} : Bool}
181 {Nat.is_le(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}
182
183def sub_mono(a, b, c, h):
184 match a b c:
185 case 0n _ _:
186 N.le_zero_l(Nat.sub(b, c))
187 case 1n+p 0n _:
188 Empty.absurd({Nat.is_le(Nat.sub(1n+p, c), Nat.sub(0n, c)) == True{} : Bool}, AB.false_ne_true(h))
189 case 1n+p 1n+r 0n:
190 h
191 case 1n+p 1n+r 1n+s:
192 sub_mono(p, r, s, h)
193
194# A digit byte: x - 48 does not wrap, and its value is at most 9.
195law le48:
196 for +x: U32
197 for +hge: {U32.is_ge(x, 48) == True{} : Bool}
198 {U32.is_le(48, x) == True{} : Bool}
199
200def le48(x, hge):
201 %Equal.sym(Bool, U32.is_le(48, x), Nat.is_le(U32.to_nat(48), U32.to_nat(x)), U.is_le_to_nat(48, x)) : {_ == True{} : Bool}
202 %U.ge_le(U32.to_nat(x), U32.to_nat(48)) : {_ == True{} : Bool}
203 Equal.trans(Bool, Nat.is_ge(U32.to_nat(x), U32.to_nat(48)), U32.is_ge(x, 48), True{},
204 Equal.sym(Bool, U32.is_ge(x, 48), Nat.is_ge(U32.to_nat(x), U32.to_nat(48)), U.is_ge_to_nat(x, 48)), hge)
205
206law ed48:
207 for +x: U32
208 for +hge: {U32.is_ge(x, 48) == True{} : Bool}
209 {U32.to_nat(U32.sub(x, 48)) == Nat.sub(U32.to_nat(x), 48n) : Nat}
210
211def ed48(x, hge):
212 U.to_nat_sub_le(x, 48, le48(x, hge))
213
214law k9:
215 for +x: U32
216 for +hle: {U32.is_le(x, 57) == True{} : Bool}
217 {Nat.is_le(Nat.sub(U32.to_nat(x), 48n), 9n) == True{} : Bool}
218
219def k9(x, hle):
220 sub_mono(U32.to_nat(x), 57n, 48n,
221 Equal.trans(Bool, Nat.is_le(U32.to_nat(x), U32.to_nat(57)), U32.is_le(x, 57), True{},
222 Equal.sym(Bool, U32.is_le(x, 57), Nat.is_le(U32.to_nat(x), U32.to_nat(57)), U.is_le_to_nat(x, 57)), hle))
223
224# num's test on words is the test on numbers (c the constant, q its value).
225law FITSU:
226 for +acc: U32
227 for +x: U32
228 for +c: U32
229 for +q: Nat
230 for +M: Nat
231 for +hcq: {U32.to_nat(c) == q : Nat}
232 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
233 for +hge: {U32.is_ge(x, 48) == True{} : Bool}
234 for +hle: {U32.is_le(x, 57) == True{} : Bool}
235 {Bool.or(U32.is_lt(acc, c), Bool.and(U32.is_eq(acc, c), U32.is_le(U32.sub(x, 48), 5))) == Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) : Bool}
236
237def FITSU(acc, x, c, q, M, hcq, hq, hge, hle):
238 +A = U32.to_nat(acc)
239 +KK = Nat.sub(U32.to_nat(x), 48n)
240 +RHS = Nat.is_lt(Nat.add(Nat.mul(A, 10n), KK), M)
241 %Equal.sym(Bool, U32.is_lt(acc, c), Nat.is_lt(A, U32.to_nat(c)), U.is_lt_to_nat(acc, c)) :
242 {Bool.or(_, Bool.and(U32.is_eq(acc, c), U32.is_le(U32.sub(x, 48), 5))) == RHS : Bool}
243 %Equal.sym(Bool, U32.is_eq(acc, c), Nat.is_eq(A, U32.to_nat(c)), U.is_eq_to_nat(acc, c)) :
244 {Bool.or(Nat.is_lt(A, U32.to_nat(c)), Bool.and(_, U32.is_le(U32.sub(x, 48), 5))) == RHS : Bool}
245 %Equal.sym(Bool, U32.is_le(U32.sub(x, 48), 5), Nat.is_le(U32.to_nat(U32.sub(x, 48)), U32.to_nat(5)), U.is_le_to_nat(U32.sub(x, 48), 5)) :
246 {Bool.or(Nat.is_lt(A, U32.to_nat(c)), Bool.and(Nat.is_eq(A, U32.to_nat(c)), _)) == RHS : Bool}
247 %Equal.sym(Nat, U32.to_nat(U32.sub(x, 48)), KK, ed48(x, hge)) :
248 {Bool.or(Nat.is_lt(A, U32.to_nat(c)), Bool.and(Nat.is_eq(A, U32.to_nat(c)), Nat.is_le(_, U32.to_nat(5)))) == RHS : Bool}
249 %Equal.sym(Nat, U32.to_nat(c), q, hcq) :
250 {Bool.or(Nat.is_lt(A, _), Bool.and(Nat.is_eq(A, _), Nat.is_le(KK, U32.to_nat(5)))) == RHS : Bool}
251 %hq : {Bool.or(Nat.is_lt(A, q), Bool.and(Nat.is_eq(A, q), Nat.is_le(KK, U32.to_nat(5)))) == Nat.is_lt(Nat.add(Nat.mul(A, 10n), KK), _) : Bool}
252 FITS0(A, q, KK, k9(x, hle))
253
254# The loop state
255# ==============
256
257# One step of num.go on byte x: the digit test, the overflow test, the new value.
258def DG(+x: U32) -> Bool:
259 U32.is_ge(x, 48) && U32.is_le(x, 57)
260
261def FT(+acc: U32, +x: U32) -> Bool:
262 U32.is_lt(acc, 429496729) || (U32.is_eq(acc, 429496729) && U32.is_le((x - 48 : U32), 5))
263
264def NA(+acc: U32, +x: U32) -> U32:
265 ((acc * 10 : U32) + (x - 48 : U32) : U32)
266
267# The value dec has so far can no longer give a number below M.
268def Bad(m: Maybe<&2, Nat>, +M: Nat) -> Data:
269 match m:
270 case None{}:
271 Unit
272 case Some{v}:
273 {Nat.is_lt(v, M) == False{} : Bool}
274
275# How num.go's (ok, acc) stands for dec.go's value m.
276def Inv(ok: Bool, +acc: U32, +m: Maybe<&2, Nat>, +M: Nat) -> Data:
277 match ok:
278 case True{}:
279 Sigma<&2, &2, {m == Some{U32.to_nat(acc)} : Maybe<&2, Nat>}, e => {Nat.is_lt(U32.to_nat(acc), M) == True{} : Bool}>
280 case False{}:
281 Bad(m, M)
282
283law le_mul10:
284 for +v: Nat
285 {Nat.is_le(v, Nat.mul(v, 10n)) == True{} : Bool}
286
287def le_mul10(v):
288 match v:
289 case 0n:
290 {==}
291 case 1n+p:
292 N.le_trans(p, Nat.mul(p, 10n), Nat.add(9n, Nat.mul(p, 10n)), le_mul10(p), N.le_add_l(Nat.mul(p, 10n), 9n))
293
294law bad_step:
295 for +m: Maybe<&2, Nat>
296 for +dx: Maybe<&2, Nat>
297 for +M: Nat
298 for +hb: Bad(m, M)
299 Bad(F.dec.push(m, dx), M)
300
301def bad_step(m, dx, M, hb):
302 match m dx:
303 case None{} None{}:
304 Unit{}
305 case None{} Some{k}:
306 Unit{}
307 case Some{v} None{}:
308 Unit{}
309 case Some{+v} Some{+k}:
310 +S = Nat.add(Nat.mul(v, 10n), k)
311 N.le_not_lt(M, S,
312 N.le_trans(M, v, S, N.not_lt_le(v, M, hb),
313 N.le_trans(v, Nat.mul(v, 10n), S, le_mul10(v), N.le_add_r(Nat.mul(v, 10n), k))))
314
315law bad_none:
316 for +m: Maybe<&2, Nat>
317 for +M: Nat
318 for +hb: Bad(m, M)
319 {F.decb.of(m, M) == None{} : Maybe<&2, Nat>}
320
321def bad_none(m, M, hb):
322 match m:
323 case None{}:
324 {==}
325 case Some{+v}:
326 %Equal.sym(Bool, Nat.is_lt(v, M), False{}, hb) : {F.decb.if(v, _) == None{} : Maybe<&2, Nat>}
327 {==}
328
329law ena_add:
330 for +acc: U32
331 for +x: U32
332 for +M: Nat
333 for +emul: {U32.to_nat(U32.mul(acc, 10)) == Nat.mul(U32.to_nat(acc), U32.to_nat(10)) : Nat}
334 for +ed: {U32.to_nat(U32.sub(x, 48)) == Nat.sub(U32.to_nat(x), 48n) : Nat}
335 for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == True{} : Bool}
336 {Nat.is_lt(Nat.add(U32.to_nat(U32.mul(acc, 10)), U32.to_nat(U32.sub(x, 48))), M) == True{} : Bool}
337
338def ena_add(acc, x, M, emul, ed, hb):
339 %Equal.sym(Nat, U32.to_nat(U32.mul(acc, 10)), Nat.mul(U32.to_nat(acc), U32.to_nat(10)), emul) :
340 {Nat.is_lt(Nat.add(_, U32.to_nat(U32.sub(x, 48))), M) == True{} : Bool}
341 %Equal.sym(Nat, U32.to_nat(U32.sub(x, 48)), Nat.sub(U32.to_nat(x), 48n), ed) :
342 {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), U32.to_nat(10)), _), M) == True{} : Bool}
343 hb
344
345# The new value when the test passes (no wrap).
346law ena:
347 for +acc: U32
348 for +x: U32
349 for +M: Nat
350 for +hm: {Nat.pow(2n, 32n) == M : Nat}
351 for +hge: {U32.is_ge(x, 48) == True{} : Bool}
352 for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == True{} : Bool}
353 {U32.to_nat(NA(acc, x)) == Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)) : Nat}
354
355def ena(acc, x, M, hm, hge, hb):
356 +A = U32.to_nat(acc)
357 +KK = Nat.sub(U32.to_nat(x), 48n)
358 +S = Nat.add(Nat.mul(A, 10n), KK)
359 +hmul = N.le_lt_trans(Nat.mul(A, U32.to_nat(10)), S, M, N.le_add_r(Nat.mul(A, 10n), KK), hb)
360 +emul = U.to_nat_mul_fits_p(acc, 10, lift(Nat.mul(U32.to_nat(acc), U32.to_nat(10)), M, hm, hmul))
361 +ed = ed48(x, hge)
362 +hadd = ena_add(acc, x, M, emul, ed, hb)
363 +eadd = U.to_nat_add_fits_p(U32.mul(acc, 10), U32.sub(x, 48), lift(Nat.add(U32.to_nat(U32.mul(acc, 10)), U32.to_nat(U32.sub(x, 48))), M, hm, hadd))
364 %Equal.sym(Nat, U32.to_nat(U32.add(U32.mul(acc, 10), U32.sub(x, 48))), Nat.add(U32.to_nat(U32.mul(acc, 10)), U32.to_nat(U32.sub(x, 48))), eadd) :
365 {_ == S : Nat}
366 %Equal.sym(Nat, U32.to_nat(U32.mul(acc, 10)), Nat.mul(A, U32.to_nat(10)), emul) : {Nat.add(_, U32.to_nat(U32.sub(x, 48))) == S : Nat}
367 %Equal.sym(Nat, U32.to_nat(U32.sub(x, 48)), KK, ed) : {Nat.add(Nat.mul(A, U32.to_nat(10)), _) == S : Nat}
368 {==}
369
370# After a digit, by the overflow test (b).
371law step_fb:
372 for +acc: U32
373 for +x: U32
374 for +M: Nat
375 for +b: Bool
376 for +hm: {Nat.pow(2n, 32n) == M : Nat}
377 for +hge: {U32.is_ge(x, 48) == True{} : Bool}
378 for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == b : Bool}
379 Inv(b, NA(acc, x), Some{Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n))}, M)
380
381def step_fb(acc, x, M, b, hm, hge, hb):
382 match b:
383 case True{}:
384 +S = Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n))
385 +e = Equal.sym(Nat, U32.to_nat(NA(acc, x)), S, ena(acc, x, M, hm, hge, hb))
386 (Equal.cong(Nat, Maybe<&2, Nat>, v => Some{v}, S, U32.to_nat(NA(acc, x)), e),
387 AB.subst(Nat, y => {Nat.is_lt(y, M) == True{} : Bool}, S, U32.to_nat(NA(acc, x)), e, hb))
388 case False{}:
389 hb
390
391# After byte x, from value a, by the digit test (dg).
392law step_dg:
393 for +acc: U32
394 for +x: U32
395 for +M: Nat
396 for +q: Nat
397 for +dg: Bool
398 for +hdg: {DG(x) == dg : Bool}
399 for +hm: {Nat.pow(2n, 32n) == M : Nat}
400 for +hcq: {U32.to_nat(429496729) == q : Nat}
401 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
402 Inv(Bool.and(dg, FT(acc, x)), NA(acc, x), F.dec.push(Some{U32.to_nat(acc)}, F.digit.if(x, dg)), M)
403
404def step_dg(acc, x, M, q, dg, hdg, hm, hcq, hq):
405 match dg:
406 case False{}:
407 Unit{}
408 case True{}:
409 +hge = AB.and_true_l(U32.is_ge(x, 48), U32.is_le(x, 57), hdg)
410 +hle = AB.and_true_r(U32.is_ge(x, 48), U32.is_le(x, 57), hdg)
411 +S = Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n))
412 %Equal.sym(Bool, Bool.or(U32.is_lt(acc, 429496729), Bool.and(U32.is_eq(acc, 429496729), U32.is_le(U32.sub(x, 48), 5))), Nat.is_lt(S, M),
413 FITSU(acc, x, 429496729, q, M, hcq, hq, hge, hle)) :
414 Inv(_, NA(acc, x), Some{S}, M)
415 step_fb(acc, x, M, Nat.is_lt(S, M), hm, hge, {==})
416
417law inv_step:
418 for +ok: Bool
419 for +acc: U32
420 for +m: Maybe<&2, Nat>
421 for +x: U32
422 for +M: Nat
423 for +q: Nat
424 for +hm: {Nat.pow(2n, 32n) == M : Nat}
425 for +hcq: {U32.to_nat(429496729) == q : Nat}
426 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
427 for +hi: Inv(ok, acc, m, M)
428 Inv(Bool.and(ok, Bool.and(DG(x), FT(acc, x))), NA(acc, x), F.dec.push(m, F.digit(x)), M)
429
430def inv_step(ok, acc, m, x, M, q, hm, hcq, hq, hi):
431 match ok:
432 case False{}:
433 bad_step(m, F.digit(x), M, hi)
434 case True{}:
435 (e1, e2) = hi
436 %Equal.sym(Maybe<&2, Nat>, m, Some{U32.to_nat(acc)}, e1) :
437 Inv(Bool.and(DG(x), FT(acc, x)), NA(acc, x), F.dec.push(_, F.digit(x)), M)
438 step_dg(acc, x, M, q, DG(x), {==}, hm, hcq, hq)
439
440law base:
441 for +ok: Bool
442 for +acc: U32
443 for +m: Maybe<&2, Nat>
444 for +M: Nat
445 for +hi: Inv(ok, acc, m, M)
446 {F.nat_of(C.num.fin(acc, ok)) == F.decb.of(m, M) : Maybe<&2, Nat>}
447
448def base(ok, acc, m, M, hi):
449 match ok:
450 case True{}:
451 (+e1, +e2) = hi
452 %Equal.sym(Maybe<&2, Nat>, m, Some{U32.to_nat(acc)}, e1) : {F.nat_of(C.num.fin(acc, True{})) == F.decb.of(_, M) : Maybe<&2, Nat>}
453 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(acc), M), True{}, e2) : {Some{U32.to_nat(acc)} == F.decb.if(U32.to_nat(acc), _) : Maybe<&2, Nat>}
454 {==}
455 case False{}:
456 Equal.sym(Maybe<&2, Nat>, F.decb.of(m, M), None{}, bad_none(m, M, hi))
457
458# The loop
459# ========
460
461law np:
462 for +n: Nat
463 for +len: U32
464 for +t: P.Tree<U32>
465 for +j: U32
466 for +acc: U32
467 for +ok: Bool
468 {C.num.go(n, B.at(K.BT(len, t), j), j, acc, ok) == (K.BT(len, t), Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(n, B.at(K.BT(len, t), j), j, acc, ok))) : D.Bytes & Maybe<&2, U32>}
469
470def np(n, len, t, j, acc, ok):
471 match n:
472 case 0n:
473 %Equal.sym(D.Bytes & U32, B.at(K.BT(len, t), j), (K.BT(len, t), K.AT(len, t, j)), K.at_pair_t(len, t, j)) :
474 {C.num.go(0n, _, j, acc, ok) == (K.BT(len, t), Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(0n, _, j, acc, ok))) : D.Bytes & Maybe<&2, U32>}
475 {==}
476 case 1n+k:
477 +x = K.AT(len, t, j)
478 %Equal.sym(D.Bytes & U32, B.at(K.BT(len, t), j), (K.BT(len, t), x), K.at_pair_t(len, t, j)) :
479 {C.num.go(1n+k, _, j, acc, ok) == (K.BT(len, t), Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(1n+k, _, j, acc, ok))) : D.Bytes & Maybe<&2, U32>}
480 np(k, len, t, (j + 1 : U32), NA(acc, x), Bool.and(ok, Bool.and(DG(x), FT(acc, x))))
481
482law num_pair_t:
483 for +len: U32
484 for +t: P.Tree<U32>
485 for +from: U32
486 for +to: U32
487 {C.num(K.BT(len, t), from, to) == (K.BT(len, t), Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(K.BT(len, t), from, to))) : D.Bytes & Maybe<&2, U32>}
488
489def num_pair_t(len, t, from, to):
490 np(Nat.sub(U32.to_nat(to), U32.to_nat(from)), len, t, from, 0, U32.is_lt(from, to))
491
492law nv:
493 for +n: Nat
494 for +len: U32
495 for +t: P.Tree<U32>
496 for +d: Nat
497 for +j: U32
498 for +ok: Bool
499 for +acc: U32
500 for +m: Maybe<&2, Nat>
501 for +M: Nat
502 for +q: Nat
503 for +hm: {Nat.pow(2n, 32n) == M : Nat}
504 for +hcq: {U32.to_nat(429496729) == q : Nat}
505 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
506 for +h: {D.ok(K.BT(len, t), d) == True{} : Bool}
507 for +hjn: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool}
508 for +hi: Inv(ok, acc, m, M)
509 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(n, B.at(K.BT(len, t), j), j, acc, ok))) == F.decb.of(F.dec.go(D.slice(D.view(K.BT(len, t)), U32.to_nat(j), n), m), M) : Maybe<&2, Nat>}
510
511def nv(n, len, t, d, j, ok, acc, m, M, q, hm, hcq, hq, h, hjn, hi):
512 match n:
513 case 0n:
514 +xs = D.view(K.BT(len, t))
515 %Equal.sym(D.Bytes & U32, B.at(K.BT(len, t), j), (K.BT(len, t), K.AT(len, t, j)), K.at_pair_t(len, t, j)) :
516 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(0n, _, j, acc, ok))) == F.decb.of(F.dec.go(D.slice(xs, U32.to_nat(j), 0n), m), M) : Maybe<&2, Nat>}
517 %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(j), 0n), Nil{}, X.slice_zero(xs, U32.to_nat(j))) :
518 {F.nat_of(C.num.fin(acc, ok)) == F.decb.of(F.dec.go(_, m), M) : Maybe<&2, Nat>}
519 base(ok, acc, m, M, hi)
520 case 1n+k:
521 +xs = D.view(K.BT(len, t))
522 +JJ = U32.to_nat(j)
523 +x = K.AT(len, t, j)
524 +j1 = (j + 1 : U32)
525 +ok1 = Bool.and(ok, Bool.and(DG(x), FT(acc, x)))
526 +hx = Equal.sym(Maybe<&2, U32>, Some{x}, List.get(&2, U32, xs, JJ),
527 K.at_view_t(len, t, d, j, K.ok_full(len, t, d, h), K.ok_d(len, t, d, h), K.ok_len(len, t, d, h), X.read_lt(len, j, k, hjn)))
528 %Equal.sym(D.Bytes & U32, B.at(K.BT(len, t), j), (K.BT(len, t), x), K.at_pair_t(len, t, j)) :
529 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(1n+k, _, j, acc, ok))) == F.decb.of(F.dec.go(D.slice(xs, JJ, 1n+k), m), M) : Maybe<&2, Nat>}
530 %Equal.sym(List<&2, U32>, D.slice(xs, JJ, 1n+k), x <> D.slice(xs, Nat.add(JJ, 1n), k), X.slice_cons(xs, JJ, k, x, hx)) :
531 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(k, B.at(K.BT(len, t), j1), j1, NA(acc, x), ok1))) == F.decb.of(F.dec.go(_, m), M) : Maybe<&2, Nat>}
532 %X.read_inc(len, t, d, j, k, h, hjn) :
533 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(k, B.at(K.BT(len, t), j1), j1, NA(acc, x), ok1))) == F.decb.of(F.dec.go(D.slice(xs, _, k), F.dec.push(m, F.digit(x))), M) : Maybe<&2, Nat>}
534 nv(k, len, t, d, j1, ok1, NA(acc, x), F.dec.push(m, F.digit(x)), M, q, hm, hcq, hq, h, X.read_next(len, t, d, j, k, h, hjn),
535 inv_step(ok, acc, m, x, M, q, hm, hcq, hq, hi))
536
537# Entering the loop
538# =================
539
540law sub0_nlt:
541 for +a: Nat
542 for +b: Nat
543 for +h: {Nat.sub(b, a) == 0n : Nat}
544 {Nat.is_lt(a, b) == False{} : Bool}
545
546def sub0_nlt(a, b, h):
547 match a b:
548 case 0n 0n:
549 {==}
550 case 0n 1n+r:
551 Empty.absurd({Nat.is_lt(0n, 1n+r) == False{} : Bool}, AB.succ_ne_zero(r, h))
552 case 1n+p 0n:
553 {==}
554 case 1n+p 1n+r:
555 sub0_nlt(p, r, h)
556
557law subs_lt:
558 for +a: Nat
559 for +b: Nat
560 for +k: Nat
561 for +h: {Nat.sub(b, a) == 1n+k : Nat}
562 {Nat.is_lt(a, b) == True{} : Bool}
563
564def subs_lt(a, b, k, h):
565 match a b:
566 case 0n 0n:
567 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, AB.succ_ne_zero(k, Equal.sym(Nat, 0n, 1n+k, h)))
568 case 0n 1n+r:
569 {==}
570 case 1n+p 0n:
571 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, AB.succ_ne_zero(k, Equal.sym(Nat, 0n, 1n+k, h)))
572 case 1n+p 1n+r:
573 subs_lt(p, r, k, h)
574
575law decs:
576 for +xs: List<&2, U32>
577 for +i: Nat
578 for +k: Nat
579 for +x: U32
580 for +M: Nat
581 for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
582 {F.decb(D.slice(xs, i, 1n+k), M) == F.decb.of(F.dec.go(D.slice(xs, i, 1n+k), Some{0n}), M) : Maybe<&2, Nat>}
583
584def decs(xs, i, k, x, M, hx):
585 %Equal.sym(List<&2, U32>, D.slice(xs, i, 1n+k), x <> D.slice(xs, Nat.add(i, 1n), k), X.slice_cons(xs, i, k, x, hx)) :
586 {F.decb(_, M) == F.decb.of(F.dec.go(_, Some{0n}), M) : Maybe<&2, Nat>}
587 {==}
588
589law nvt2:
590 for +n: Nat
591 for +len: U32
592 for +t: P.Tree<U32>
593 for +d: Nat
594 for +from: U32
595 for +to: U32
596 for +M: Nat
597 for +q: Nat
598 for +hm: {Nat.pow(2n, 32n) == M : Nat}
599 for +hcq: {U32.to_nat(429496729) == q : Nat}
600 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
601 for +h: {D.ok(K.BT(len, t), d) == True{} : Bool}
602 for +hft: {U32.is_le(from, to) == True{} : Bool}
603 for +ht: {Nat.is_le(U32.to_nat(to), D.size(K.BT(len, t))) == True{} : Bool}
604 for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat}
605 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(K.BT(len, t), from, to))) == F.decb(D.slice(D.view(K.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), M) : Maybe<&2, Nat>}
606
607def nvt2(n, len, t, d, from, to, M, q, hm, hcq, hq, h, hft, ht, hn):
608 match n:
609 case 0n:
610 +xs = D.view(K.BT(len, t))
611 +FF = U32.to_nat(from)
612 +TT = U32.to_nat(to)
613 +nlt = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), False{}, U.is_lt_to_nat(from, to), sub0_nlt(FF, TT, hn))
614 %Equal.sym(Nat, Nat.sub(TT, FF), 0n, hn) :
615 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(_, B.at(K.BT(len, t), from), from, 0, U32.is_lt(from, to)))) == F.decb(D.slice(xs, FF, _), M) : Maybe<&2, Nat>}
616 %Equal.sym(D.Bytes & U32, B.at(K.BT(len, t), from), (K.BT(len, t), K.AT(len, t, from)), K.at_pair_t(len, t, from)) :
617 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(0n, _, from, 0, U32.is_lt(from, to)))) == F.decb(D.slice(xs, FF, 0n), M) : Maybe<&2, Nat>}
618 %Equal.sym(Bool, U32.is_lt(from, to), False{}, nlt) :
619 {F.nat_of(C.num.fin(0, _)) == F.decb(D.slice(xs, FF, 0n), M) : Maybe<&2, Nat>}
620 %Equal.sym(List<&2, U32>, D.slice(xs, FF, 0n), Nil{}, X.slice_zero(xs, FF)) :
621 {F.nat_of(C.num.fin(0, False{})) == F.decb(_, M) : Maybe<&2, Nat>}
622 {==}
623 case 1n+k:
624 +xs = D.view(K.BT(len, t))
625 +FF = U32.to_nat(from)
626 +TT = U32.to_nat(to)
627 +LL = U32.to_nat(len)
628 +hlt = subs_lt(FF, TT, k, hn)
629 +lt1 = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), True{}, U.is_lt_to_nat(from, to), hlt)
630 +hFT = Equal.trans(Bool, Nat.is_le(FF, TT), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(FF, TT), U.is_le_to_nat(from, to)), hft)
631 +eT = Equal.trans(Nat, Nat.add(FF, 1n+k), Nat.add(FF, Nat.sub(TT, FF)), TT,
632 Equal.cong(Nat, Nat, y => Nat.add(FF, y), 1n+k, Nat.sub(TT, FF), Equal.sym(Nat, Nat.sub(TT, FF), 1n+k, hn)), N.le_sub_add(FF, TT, hFT))
633 +hjn = AB.subst(Nat, y => {Nat.is_le(y, LL) == True{} : Bool}, TT, Nat.add(FF, 1n+k), Equal.sym(Nat, Nat.add(FF, 1n+k), TT, eT), ht)
634 +hx = Equal.sym(Maybe<&2, U32>, Some{K.AT(len, t, from)}, List.get(&2, U32, xs, FF),
635 K.at_view_t(len, t, d, from, K.ok_full(len, t, d, h), K.ok_d(len, t, d, h), K.ok_len(len, t, d, h), N.lt_le_trans(FF, TT, LL, hlt, ht)))
636 %Equal.sym(Nat, Nat.sub(TT, FF), 1n+k, hn) :
637 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(_, B.at(K.BT(len, t), from), from, 0, U32.is_lt(from, to)))) == F.decb(D.slice(xs, FF, _), M) : Maybe<&2, Nat>}
638 %Equal.sym(Bool, U32.is_lt(from, to), True{}, lt1) :
639 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(1n+k, B.at(K.BT(len, t), from), from, 0, _))) == F.decb(D.slice(xs, FF, 1n+k), M) : Maybe<&2, Nat>}
640 %Equal.sym(Maybe<&2, Nat>, F.decb(D.slice(xs, FF, 1n+k), M), F.decb.of(F.dec.go(D.slice(xs, FF, 1n+k), Some{0n}), M), decs(xs, FF, k, K.AT(len, t, from), M, hx)) :
641 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(1n+k, B.at(K.BT(len, t), from), from, 0, True{}))) == _ : Maybe<&2, Nat>}
642 nv(1n+k, len, t, d, from, True{}, 0, Some{U32.to_nat(0)}, M, q, hm, hcq, hq, h, hjn, ({==}, posM(M, hm)))
643
644law nvt:
645 for +len: U32
646 for +t: P.Tree<U32>
647 for +d: Nat
648 for +from: U32
649 for +to: U32
650 for +M: Nat
651 for +q: Nat
652 for +hm: {Nat.pow(2n, 32n) == M : Nat}
653 for +hcq: {U32.to_nat(429496729) == q : Nat}
654 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
655 for +h: {D.ok(K.BT(len, t), d) == True{} : Bool}
656 for +hft: {U32.is_le(from, to) == True{} : Bool}
657 for +ht: {Nat.is_le(U32.to_nat(to), D.size(K.BT(len, t))) == True{} : Bool}
658 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(K.BT(len, t), from, to))) == F.decb(D.slice(D.view(K.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), M) : Maybe<&2, Nat>}
659
660def nvt(len, t, d, from, to, M, q, hm, hcq, hq, h, hft, ht):
661 nvt2(Nat.sub(U32.to_nat(to), U32.to_nat(from)), len, t, d, from, to, M, q, hm, hcq, hq, h, hft, ht, {==})
662
663# The law, with the bound 2^32 and the constant's value put in only here.
664law num_view_t:
665 for +len: U32
666 for +t: P.Tree<U32>
667 for +d: Nat
668 for +from: U32
669 for +to: U32
670 for +h: {D.ok(K.BT(len, t), d) == True{} : Bool}
671 for +hft: {U32.is_le(from, to) == True{} : Bool}
672 for +ht: {Nat.is_le(U32.to_nat(to), D.size(K.BT(len, t))) == True{} : Bool}
673 {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(K.BT(len, t), from, to))) == F.decb(D.slice(D.view(K.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}
674
675def num_view_t(len, t, d, from, to, h, hft, ht):
676 nvt(len, t, d, from, to, Nat.pow(2n, 32n), U32.to_nat(429496729), {==}, {==}, QM(Nat.pow(2n, 32n), {==}), h, hft, ht)