proof_num.bend

lawful-fields@0.1.1.0 · 676 lines · 40 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-fields@0.1.1.0/defs.bend as F
5import lawful-fields@0.1.1.0/fields.bend as C
6import lawful-bytes@0.1.1.0/proof_seq.bend as Q
7import lawful-bytes@0.1.1.0/proof_core.bend as K
8import lawful-bytes@0.1.1.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)