proofs/crypto/argon2/phc.bend

bend-collections-laws-crypto@1.0.0.0 · 1,358 lines · 45 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
6import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as HH
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH
9# Generated by tools/generators/argon2_phc_gen.py; do not edit by hand.
10
11# The PHC string of an Argon2id hash parses back to its fields: base64 and
12# decimal round trips, and the '$'-separated fields. Every finite fact
13# (a crumb, a base64 digit, a decimal digit) is checked value by value.
14
15# Every byte is below 256.
16def ok(bs: List<&2, U32>) -> Bool:
17  match bs:
18    case Nil{}:
19      True{}
20    case x <> r:
21      Bool.and(Nat.is_lt(U32.to_nat(x), 256n), ok(r))
22
23def ok_head(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}:
24  L.and_left(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)
25
26def ok_tail(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {ok(r) == True{} : Bool}:
27  L.and_right(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)
28
29def u(+n: Nat) -> U32:
30  U32.from_nat(n)
31
32# ---------------------------------------------------------------- base64 digits
33
34def dv_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.value(PH.digit(u(n))) == Some{u(n)} : Maybe<&2, U32>}:
35  match n:
36    case 0n:
37      {==}
38    case 1n:
39      {==}
40    case 2n:
41      {==}
42    case 3n:
43      {==}
44    case 4n:
45      {==}
46    case 5n:
47      {==}
48    case 6n:
49      {==}
50    case 7n:
51      {==}
52    case 8n:
53      {==}
54    case 9n:
55      {==}
56    case 10n:
57      {==}
58    case 11n:
59      {==}
60    case 12n:
61      {==}
62    case 13n:
63      {==}
64    case 14n:
65      {==}
66    case 15n:
67      {==}
68    case 16n:
69      {==}
70    case 17n:
71      {==}
72    case 18n:
73      {==}
74    case 19n:
75      {==}
76    case 20n:
77      {==}
78    case 21n:
79      {==}
80    case 22n:
81      {==}
82    case 23n:
83      {==}
84    case 24n:
85      {==}
86    case 25n:
87      {==}
88    case 26n:
89      {==}
90    case 27n:
91      {==}
92    case 28n:
93      {==}
94    case 29n:
95      {==}
96    case 30n:
97      {==}
98    case 31n:
99      {==}
100    case 32n:
101      {==}
102    case 33n:
103      {==}
104    case 34n:
105      {==}
106    case 35n:
107      {==}
108    case 36n:
109      {==}
110    case 37n:
111      {==}
112    case 38n:
113      {==}
114    case 39n:
115      {==}
116    case 40n:
117      {==}
118    case 41n:
119      {==}
120    case 42n:
121      {==}
122    case 43n:
123      {==}
124    case 44n:
125      {==}
126    case 45n:
127      {==}
128    case 46n:
129      {==}
130    case 47n:
131      {==}
132    case 48n:
133      {==}
134    case 49n:
135      {==}
136    case 50n:
137      {==}
138    case 51n:
139      {==}
140    case 52n:
141      {==}
142    case 53n:
143      {==}
144    case 54n:
145      {==}
146    case 55n:
147      {==}
148    case 56n:
149      {==}
150    case 57n:
151      {==}
152    case 58n:
153      {==}
154    case 59n:
155      {==}
156    case 60n:
157      {==}
158    case 61n:
159      {==}
160    case 62n:
161      {==}
162    case 63n:
163      {==}
164    case 64n+r:
165      Empty.absurd({PH.value(PH.digit(u(64n+r))) == Some{u(64n+r)} : Maybe<&2, U32>}, N.lt_zero_absurd(r, h))
166
167def digit_value(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.value(PH.digit(x)) == Some{x} : Maybe<&2, U32>}:
168  %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>}
169  dv_n(U32.to_nat(x), h)
170
171def nd_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(u(n)), SNil{}}) == False{} : Bool}:
172  match n:
173    case 0n:
174      {==}
175    case 1n:
176      {==}
177    case 2n:
178      {==}
179    case 3n:
180      {==}
181    case 4n:
182      {==}
183    case 5n:
184      {==}
185    case 6n:
186      {==}
187    case 7n:
188      {==}
189    case 8n:
190      {==}
191    case 9n:
192      {==}
193    case 10n:
194      {==}
195    case 11n:
196      {==}
197    case 12n:
198      {==}
199    case 13n:
200      {==}
201    case 14n:
202      {==}
203    case 15n:
204      {==}
205    case 16n:
206      {==}
207    case 17n:
208      {==}
209    case 18n:
210      {==}
211    case 19n:
212      {==}
213    case 20n:
214      {==}
215    case 21n:
216      {==}
217    case 22n:
218      {==}
219    case 23n:
220      {==}
221    case 24n:
222      {==}
223    case 25n:
224      {==}
225    case 26n:
226      {==}
227    case 27n:
228      {==}
229    case 28n:
230      {==}
231    case 29n:
232      {==}
233    case 30n:
234      {==}
235    case 31n:
236      {==}
237    case 32n:
238      {==}
239    case 33n:
240      {==}
241    case 34n:
242      {==}
243    case 35n:
244      {==}
245    case 36n:
246      {==}
247    case 37n:
248      {==}
249    case 38n:
250      {==}
251    case 39n:
252      {==}
253    case 40n:
254      {==}
255    case 41n:
256      {==}
257    case 42n:
258      {==}
259    case 43n:
260      {==}
261    case 44n:
262      {==}
263    case 45n:
264      {==}
265    case 46n:
266      {==}
267    case 47n:
268      {==}
269    case 48n:
270      {==}
271    case 49n:
272      {==}
273    case 50n:
274      {==}
275    case 51n:
276      {==}
277    case 52n:
278      {==}
279    case 53n:
280      {==}
281    case 54n:
282      {==}
283    case 55n:
284      {==}
285    case 56n:
286      {==}
287    case 57n:
288      {==}
289    case 58n:
290      {==}
291    case 59n:
292      {==}
293    case 60n:
294      {==}
295    case 61n:
296      {==}
297    case 62n:
298      {==}
299    case 63n:
300      {==}
301    case 64n+r:
302      Empty.absurd({PH.dollar(SCon{PH.digit(u(64n+r)), SNil{}}) == False{} : Bool}, N.lt_zero_absurd(r, h))
303
304def no_dollar(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(x), SNil{}}) == False{} : Bool}:
305  %LW.rt(x) : {PH.dollar(SCon{PH.digit(_), SNil{}}) == False{} : Bool}
306  nd_n(U32.to_nat(x), h)
307
308# ---------------------------------------------------------------- crumbs
309
310# A value below 4 round-trips through U32.
311def tn(+i: Nat, +h: {Nat.is_lt(i, 4n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
312  U.to_nat_from_nat(i, 2n, {==}, h)
313
314# m < K * 4 gives m / 4 < K.
315def div4_lt(+m: Nat, +k: Nat, +h: {Nat.is_lt(m, Nat.mul(k, 4n)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(m, 4n), k) == True{} : Bool}:
316  N.not_le_lt(k, Nat.div(m, 4n), Equal.trans(Bool, Nat.is_le(k, Nat.div(m, 4n)), Nat.is_le(Nat.mul(k, 4n), m), False{}, NR.le_div(3n, k, m), N.lt_not_le(m, Nat.mul(k, 4n), h)))
317
318def c0_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c0(x)), 4n) == True{} : Bool}:
319  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
320  NR.dm_lt(3n, U32.to_nat(x))
321
322def c1_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c1(x)), 4n) == True{} : Bool}:
323  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
324  NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n))
325
326def c2_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c2(x)), 4n) == True{} : Bool}:
327  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
328  NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n))
329
330def t3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n) == True{} : Bool}:
331  div4_lt(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n, div4_lt(Nat.div(U32.to_nat(x), 4n), 16n, div4_lt(U32.to_nat(x), 64n, h)))
332
333def c3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.c3(x)), 4n) == True{} : Bool}:
334  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {Nat.is_lt(_, 4n) == True{} : Bool}
335  t3_lt(x, h)
336
337# A byte is the byte of its crumbs.
338def byte_rt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {PH.byte_of(PH.c3(x), PH.c2(x), PH.c1(x), PH.c0(x)) == x : U32}:
339  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), U32.to_nat(PH.c2(x))), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
340  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), _), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
341  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), _), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
342  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), _)) == x : U32}
343  %NR.dm_eq(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
344  %NR.dm_eq(3n, Nat.div(U32.to_nat(x), 4n)) : {U32.from_nat(Nat.add(Nat.mul(_, 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
345  %NR.dm_eq(3n, U32.to_nat(x)) : {U32.from_nat(_) == x : U32}
346  LW.rt(x)
347
348# ---------------------------------------------------------------- digit values of crumbs
349
350def su_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.su(PH.sext(u(a), u(b), u(c))) == u(a) : U32}:
351  match a b c:
352    case 0n 0n 0n:
353      {==}
354    case 0n 0n 1n:
355      {==}
356    case 0n 0n 2n:
357      {==}
358    case 0n 0n 3n:
359      {==}
360    case 0n 1n 0n:
361      {==}
362    case 0n 1n 1n:
363      {==}
364    case 0n 1n 2n:
365      {==}
366    case 0n 1n 3n:
367      {==}
368    case 0n 2n 0n:
369      {==}
370    case 0n 2n 1n:
371      {==}
372    case 0n 2n 2n:
373      {==}
374    case 0n 2n 3n:
375      {==}
376    case 0n 3n 0n:
377      {==}
378    case 0n 3n 1n:
379      {==}
380    case 0n 3n 2n:
381      {==}
382    case 0n 3n 3n:
383      {==}
384    case 1n 0n 0n:
385      {==}
386    case 1n 0n 1n:
387      {==}
388    case 1n 0n 2n:
389      {==}
390    case 1n 0n 3n:
391      {==}
392    case 1n 1n 0n:
393      {==}
394    case 1n 1n 1n:
395      {==}
396    case 1n 1n 2n:
397      {==}
398    case 1n 1n 3n:
399      {==}
400    case 1n 2n 0n:
401      {==}
402    case 1n 2n 1n:
403      {==}
404    case 1n 2n 2n:
405      {==}
406    case 1n 2n 3n:
407      {==}
408    case 1n 3n 0n:
409      {==}
410    case 1n 3n 1n:
411      {==}
412    case 1n 3n 2n:
413      {==}
414    case 1n 3n 3n:
415      {==}
416    case 2n 0n 0n:
417      {==}
418    case 2n 0n 1n:
419      {==}
420    case 2n 0n 2n:
421      {==}
422    case 2n 0n 3n:
423      {==}
424    case 2n 1n 0n:
425      {==}
426    case 2n 1n 1n:
427      {==}
428    case 2n 1n 2n:
429      {==}
430    case 2n 1n 3n:
431      {==}
432    case 2n 2n 0n:
433      {==}
434    case 2n 2n 1n:
435      {==}
436    case 2n 2n 2n:
437      {==}
438    case 2n 2n 3n:
439      {==}
440    case 2n 3n 0n:
441      {==}
442    case 2n 3n 1n:
443      {==}
444    case 2n 3n 2n:
445      {==}
446    case 2n 3n 3n:
447      {==}
448    case 3n 0n 0n:
449      {==}
450    case 3n 0n 1n:
451      {==}
452    case 3n 0n 2n:
453      {==}
454    case 3n 0n 3n:
455      {==}
456    case 3n 1n 0n:
457      {==}
458    case 3n 1n 1n:
459      {==}
460    case 3n 1n 2n:
461      {==}
462    case 3n 1n 3n:
463      {==}
464    case 3n 2n 0n:
465      {==}
466    case 3n 2n 1n:
467      {==}
468    case 3n 2n 2n:
469      {==}
470    case 3n 2n 3n:
471      {==}
472    case 3n 3n 0n:
473      {==}
474    case 3n 3n 1n:
475      {==}
476    case 3n 3n 2n:
477      {==}
478    case 3n 3n 3n:
479      {==}
480    case 4n+r _ _:
481      Empty.absurd({PH.su(PH.sext(u(4n+r), u(b), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, ha))
482    case 0n 4n+r _:
483      Empty.absurd({PH.su(PH.sext(u(0n), u(4n+r), u(c))) == u(0n) : U32}, N.lt_zero_absurd(r, hb))
484    case 0n 0n 4n+r:
485      Empty.absurd({PH.su(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
486    case 0n 1n 4n+r:
487      Empty.absurd({PH.su(PH.sext(u(0n), u(1n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
488    case 0n 2n 4n+r:
489      Empty.absurd({PH.su(PH.sext(u(0n), u(2n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
490    case 0n 3n 4n+r:
491      Empty.absurd({PH.su(PH.sext(u(0n), u(3n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
492    case 1n 4n+r _:
493      Empty.absurd({PH.su(PH.sext(u(1n), u(4n+r), u(c))) == u(1n) : U32}, N.lt_zero_absurd(r, hb))
494    case 1n 0n 4n+r:
495      Empty.absurd({PH.su(PH.sext(u(1n), u(0n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
496    case 1n 1n 4n+r:
497      Empty.absurd({PH.su(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
498    case 1n 2n 4n+r:
499      Empty.absurd({PH.su(PH.sext(u(1n), u(2n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
500    case 1n 3n 4n+r:
501      Empty.absurd({PH.su(PH.sext(u(1n), u(3n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
502    case 2n 4n+r _:
503      Empty.absurd({PH.su(PH.sext(u(2n), u(4n+r), u(c))) == u(2n) : U32}, N.lt_zero_absurd(r, hb))
504    case 2n 0n 4n+r:
505      Empty.absurd({PH.su(PH.sext(u(2n), u(0n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
506    case 2n 1n 4n+r:
507      Empty.absurd({PH.su(PH.sext(u(2n), u(1n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
508    case 2n 2n 4n+r:
509      Empty.absurd({PH.su(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
510    case 2n 3n 4n+r:
511      Empty.absurd({PH.su(PH.sext(u(2n), u(3n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
512    case 3n 4n+r _:
513      Empty.absurd({PH.su(PH.sext(u(3n), u(4n+r), u(c))) == u(3n) : U32}, N.lt_zero_absurd(r, hb))
514    case 3n 0n 4n+r:
515      Empty.absurd({PH.su(PH.sext(u(3n), u(0n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
516    case 3n 1n 4n+r:
517      Empty.absurd({PH.su(PH.sext(u(3n), u(1n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
518    case 3n 2n 4n+r:
519      Empty.absurd({PH.su(PH.sext(u(3n), u(2n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
520    case 3n 3n 4n+r:
521      Empty.absurd({PH.su(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
522
523def su_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.su(PH.sext(x, y, z)) == x : U32}:
524  %LW.rt(x) : {PH.su(PH.sext(_, y, z)) == _ : U32}
525  %LW.rt(y) : {PH.su(PH.sext(u(U32.to_nat(x)), _, z)) == u(U32.to_nat(x)) : U32}
526  %LW.rt(z) : {PH.su(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(x)) : U32}
527  su_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
528
529def sv_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sv(PH.sext(u(a), u(b), u(c))) == u(b) : U32}:
530  match a b c:
531    case 0n 0n 0n:
532      {==}
533    case 0n 0n 1n:
534      {==}
535    case 0n 0n 2n:
536      {==}
537    case 0n 0n 3n:
538      {==}
539    case 0n 1n 0n:
540      {==}
541    case 0n 1n 1n:
542      {==}
543    case 0n 1n 2n:
544      {==}
545    case 0n 1n 3n:
546      {==}
547    case 0n 2n 0n:
548      {==}
549    case 0n 2n 1n:
550      {==}
551    case 0n 2n 2n:
552      {==}
553    case 0n 2n 3n:
554      {==}
555    case 0n 3n 0n:
556      {==}
557    case 0n 3n 1n:
558      {==}
559    case 0n 3n 2n:
560      {==}
561    case 0n 3n 3n:
562      {==}
563    case 1n 0n 0n:
564      {==}
565    case 1n 0n 1n:
566      {==}
567    case 1n 0n 2n:
568      {==}
569    case 1n 0n 3n:
570      {==}
571    case 1n 1n 0n:
572      {==}
573    case 1n 1n 1n:
574      {==}
575    case 1n 1n 2n:
576      {==}
577    case 1n 1n 3n:
578      {==}
579    case 1n 2n 0n:
580      {==}
581    case 1n 2n 1n:
582      {==}
583    case 1n 2n 2n:
584      {==}
585    case 1n 2n 3n:
586      {==}
587    case 1n 3n 0n:
588      {==}
589    case 1n 3n 1n:
590      {==}
591    case 1n 3n 2n:
592      {==}
593    case 1n 3n 3n:
594      {==}
595    case 2n 0n 0n:
596      {==}
597    case 2n 0n 1n:
598      {==}
599    case 2n 0n 2n:
600      {==}
601    case 2n 0n 3n:
602      {==}
603    case 2n 1n 0n:
604      {==}
605    case 2n 1n 1n:
606      {==}
607    case 2n 1n 2n:
608      {==}
609    case 2n 1n 3n:
610      {==}
611    case 2n 2n 0n:
612      {==}
613    case 2n 2n 1n:
614      {==}
615    case 2n 2n 2n:
616      {==}
617    case 2n 2n 3n:
618      {==}
619    case 2n 3n 0n:
620      {==}
621    case 2n 3n 1n:
622      {==}
623    case 2n 3n 2n:
624      {==}
625    case 2n 3n 3n:
626      {==}
627    case 3n 0n 0n:
628      {==}
629    case 3n 0n 1n:
630      {==}
631    case 3n 0n 2n:
632      {==}
633    case 3n 0n 3n:
634      {==}
635    case 3n 1n 0n:
636      {==}
637    case 3n 1n 1n:
638      {==}
639    case 3n 1n 2n:
640      {==}
641    case 3n 1n 3n:
642      {==}
643    case 3n 2n 0n:
644      {==}
645    case 3n 2n 1n:
646      {==}
647    case 3n 2n 2n:
648      {==}
649    case 3n 2n 3n:
650      {==}
651    case 3n 3n 0n:
652      {==}
653    case 3n 3n 1n:
654      {==}
655    case 3n 3n 2n:
656      {==}
657    case 3n 3n 3n:
658      {==}
659    case 4n+r _ _:
660      Empty.absurd({PH.sv(PH.sext(u(4n+r), u(b), u(c))) == u(b) : U32}, N.lt_zero_absurd(r, ha))
661    case 0n 4n+r _:
662      Empty.absurd({PH.sv(PH.sext(u(0n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
663    case 0n 0n 4n+r:
664      Empty.absurd({PH.sv(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
665    case 0n 1n 4n+r:
666      Empty.absurd({PH.sv(PH.sext(u(0n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
667    case 0n 2n 4n+r:
668      Empty.absurd({PH.sv(PH.sext(u(0n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
669    case 0n 3n 4n+r:
670      Empty.absurd({PH.sv(PH.sext(u(0n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
671    case 1n 4n+r _:
672      Empty.absurd({PH.sv(PH.sext(u(1n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
673    case 1n 0n 4n+r:
674      Empty.absurd({PH.sv(PH.sext(u(1n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
675    case 1n 1n 4n+r:
676      Empty.absurd({PH.sv(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
677    case 1n 2n 4n+r:
678      Empty.absurd({PH.sv(PH.sext(u(1n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
679    case 1n 3n 4n+r:
680      Empty.absurd({PH.sv(PH.sext(u(1n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
681    case 2n 4n+r _:
682      Empty.absurd({PH.sv(PH.sext(u(2n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
683    case 2n 0n 4n+r:
684      Empty.absurd({PH.sv(PH.sext(u(2n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
685    case 2n 1n 4n+r:
686      Empty.absurd({PH.sv(PH.sext(u(2n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
687    case 2n 2n 4n+r:
688      Empty.absurd({PH.sv(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
689    case 2n 3n 4n+r:
690      Empty.absurd({PH.sv(PH.sext(u(2n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
691    case 3n 4n+r _:
692      Empty.absurd({PH.sv(PH.sext(u(3n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
693    case 3n 0n 4n+r:
694      Empty.absurd({PH.sv(PH.sext(u(3n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
695    case 3n 1n 4n+r:
696      Empty.absurd({PH.sv(PH.sext(u(3n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
697    case 3n 2n 4n+r:
698      Empty.absurd({PH.sv(PH.sext(u(3n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
699    case 3n 3n 4n+r:
700      Empty.absurd({PH.sv(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
701
702def sv_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sv(PH.sext(x, y, z)) == y : U32}:
703  %LW.rt(x) : {PH.sv(PH.sext(_, y, z)) == y : U32}
704  %LW.rt(y) : {PH.sv(PH.sext(u(U32.to_nat(x)), _, z)) == _ : U32}
705  %LW.rt(z) : {PH.sv(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(y)) : U32}
706  sv_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
707
708def sw_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sw(PH.sext(u(a), u(b), u(c))) == u(c) : U32}:
709  match a b c:
710    case 0n 0n 0n:
711      {==}
712    case 0n 0n 1n:
713      {==}
714    case 0n 0n 2n:
715      {==}
716    case 0n 0n 3n:
717      {==}
718    case 0n 1n 0n:
719      {==}
720    case 0n 1n 1n:
721      {==}
722    case 0n 1n 2n:
723      {==}
724    case 0n 1n 3n:
725      {==}
726    case 0n 2n 0n:
727      {==}
728    case 0n 2n 1n:
729      {==}
730    case 0n 2n 2n:
731      {==}
732    case 0n 2n 3n:
733      {==}
734    case 0n 3n 0n:
735      {==}
736    case 0n 3n 1n:
737      {==}
738    case 0n 3n 2n:
739      {==}
740    case 0n 3n 3n:
741      {==}
742    case 1n 0n 0n:
743      {==}
744    case 1n 0n 1n:
745      {==}
746    case 1n 0n 2n:
747      {==}
748    case 1n 0n 3n:
749      {==}
750    case 1n 1n 0n:
751      {==}
752    case 1n 1n 1n:
753      {==}
754    case 1n 1n 2n:
755      {==}
756    case 1n 1n 3n:
757      {==}
758    case 1n 2n 0n:
759      {==}
760    case 1n 2n 1n:
761      {==}
762    case 1n 2n 2n:
763      {==}
764    case 1n 2n 3n:
765      {==}
766    case 1n 3n 0n:
767      {==}
768    case 1n 3n 1n:
769      {==}
770    case 1n 3n 2n:
771      {==}
772    case 1n 3n 3n:
773      {==}
774    case 2n 0n 0n:
775      {==}
776    case 2n 0n 1n:
777      {==}
778    case 2n 0n 2n:
779      {==}
780    case 2n 0n 3n:
781      {==}
782    case 2n 1n 0n:
783      {==}
784    case 2n 1n 1n:
785      {==}
786    case 2n 1n 2n:
787      {==}
788    case 2n 1n 3n:
789      {==}
790    case 2n 2n 0n:
791      {==}
792    case 2n 2n 1n:
793      {==}
794    case 2n 2n 2n:
795      {==}
796    case 2n 2n 3n:
797      {==}
798    case 2n 3n 0n:
799      {==}
800    case 2n 3n 1n:
801      {==}
802    case 2n 3n 2n:
803      {==}
804    case 2n 3n 3n:
805      {==}
806    case 3n 0n 0n:
807      {==}
808    case 3n 0n 1n:
809      {==}
810    case 3n 0n 2n:
811      {==}
812    case 3n 0n 3n:
813      {==}
814    case 3n 1n 0n:
815      {==}
816    case 3n 1n 1n:
817      {==}
818    case 3n 1n 2n:
819      {==}
820    case 3n 1n 3n:
821      {==}
822    case 3n 2n 0n:
823      {==}
824    case 3n 2n 1n:
825      {==}
826    case 3n 2n 2n:
827      {==}
828    case 3n 2n 3n:
829      {==}
830    case 3n 3n 0n:
831      {==}
832    case 3n 3n 1n:
833      {==}
834    case 3n 3n 2n:
835      {==}
836    case 3n 3n 3n:
837      {==}
838    case 4n+r _ _:
839      Empty.absurd({PH.sw(PH.sext(u(4n+r), u(b), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, ha))
840    case 0n 4n+r _:
841      Empty.absurd({PH.sw(PH.sext(u(0n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
842    case 0n 0n 4n+r:
843      Empty.absurd({PH.sw(PH.sext(u(0n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
844    case 0n 1n 4n+r:
845      Empty.absurd({PH.sw(PH.sext(u(0n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
846    case 0n 2n 4n+r:
847      Empty.absurd({PH.sw(PH.sext(u(0n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
848    case 0n 3n 4n+r:
849      Empty.absurd({PH.sw(PH.sext(u(0n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
850    case 1n 4n+r _:
851      Empty.absurd({PH.sw(PH.sext(u(1n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
852    case 1n 0n 4n+r:
853      Empty.absurd({PH.sw(PH.sext(u(1n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
854    case 1n 1n 4n+r:
855      Empty.absurd({PH.sw(PH.sext(u(1n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
856    case 1n 2n 4n+r:
857      Empty.absurd({PH.sw(PH.sext(u(1n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
858    case 1n 3n 4n+r:
859      Empty.absurd({PH.sw(PH.sext(u(1n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
860    case 2n 4n+r _:
861      Empty.absurd({PH.sw(PH.sext(u(2n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
862    case 2n 0n 4n+r:
863      Empty.absurd({PH.sw(PH.sext(u(2n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
864    case 2n 1n 4n+r:
865      Empty.absurd({PH.sw(PH.sext(u(2n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
866    case 2n 2n 4n+r:
867      Empty.absurd({PH.sw(PH.sext(u(2n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
868    case 2n 3n 4n+r:
869      Empty.absurd({PH.sw(PH.sext(u(2n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
870    case 3n 4n+r _:
871      Empty.absurd({PH.sw(PH.sext(u(3n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
872    case 3n 0n 4n+r:
873      Empty.absurd({PH.sw(PH.sext(u(3n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
874    case 3n 1n 4n+r:
875      Empty.absurd({PH.sw(PH.sext(u(3n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
876    case 3n 2n 4n+r:
877      Empty.absurd({PH.sw(PH.sext(u(3n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
878    case 3n 3n 4n+r:
879      Empty.absurd({PH.sw(PH.sext(u(3n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
880
881def sw_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sw(PH.sext(x, y, z)) == z : U32}:
882  %LW.rt(x) : {PH.sw(PH.sext(_, y, z)) == z : U32}
883  %LW.rt(y) : {PH.sw(PH.sext(u(U32.to_nat(x)), _, z)) == z : U32}
884  %LW.rt(z) : {PH.sw(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == _ : U32}
885  sw_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
886
887def sx_lt_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(u(a), u(b), u(c))), 64n) == True{} : Bool}:
888  match a b c:
889    case 0n 0n 0n:
890      {==}
891    case 0n 0n 1n:
892      {==}
893    case 0n 0n 2n:
894      {==}
895    case 0n 0n 3n:
896      {==}
897    case 0n 1n 0n:
898      {==}
899    case 0n 1n 1n:
900      {==}
901    case 0n 1n 2n:
902      {==}
903    case 0n 1n 3n:
904      {==}
905    case 0n 2n 0n:
906      {==}
907    case 0n 2n 1n:
908      {==}
909    case 0n 2n 2n:
910      {==}
911    case 0n 2n 3n:
912      {==}
913    case 0n 3n 0n:
914      {==}
915    case 0n 3n 1n:
916      {==}
917    case 0n 3n 2n:
918      {==}
919    case 0n 3n 3n:
920      {==}
921    case 1n 0n 0n:
922      {==}
923    case 1n 0n 1n:
924      {==}
925    case 1n 0n 2n:
926      {==}
927    case 1n 0n 3n:
928      {==}
929    case 1n 1n 0n:
930      {==}
931    case 1n 1n 1n:
932      {==}
933    case 1n 1n 2n:
934      {==}
935    case 1n 1n 3n:
936      {==}
937    case 1n 2n 0n:
938      {==}
939    case 1n 2n 1n:
940      {==}
941    case 1n 2n 2n:
942      {==}
943    case 1n 2n 3n:
944      {==}
945    case 1n 3n 0n:
946      {==}
947    case 1n 3n 1n:
948      {==}
949    case 1n 3n 2n:
950      {==}
951    case 1n 3n 3n:
952      {==}
953    case 2n 0n 0n:
954      {==}
955    case 2n 0n 1n:
956      {==}
957    case 2n 0n 2n:
958      {==}
959    case 2n 0n 3n:
960      {==}
961    case 2n 1n 0n:
962      {==}
963    case 2n 1n 1n:
964      {==}
965    case 2n 1n 2n:
966      {==}
967    case 2n 1n 3n:
968      {==}
969    case 2n 2n 0n:
970      {==}
971    case 2n 2n 1n:
972      {==}
973    case 2n 2n 2n:
974      {==}
975    case 2n 2n 3n:
976      {==}
977    case 2n 3n 0n:
978      {==}
979    case 2n 3n 1n:
980      {==}
981    case 2n 3n 2n:
982      {==}
983    case 2n 3n 3n:
984      {==}
985    case 3n 0n 0n:
986      {==}
987    case 3n 0n 1n:
988      {==}
989    case 3n 0n 2n:
990      {==}
991    case 3n 0n 3n:
992      {==}
993    case 3n 1n 0n:
994      {==}
995    case 3n 1n 1n:
996      {==}
997    case 3n 1n 2n:
998      {==}
999    case 3n 1n 3n:
1000      {==}
1001    case 3n 2n 0n:
1002      {==}
1003    case 3n 2n 1n:
1004      {==}
1005    case 3n 2n 2n:
1006      {==}
1007    case 3n 2n 3n:
1008      {==}
1009    case 3n 3n 0n:
1010      {==}
1011    case 3n 3n 1n:
1012      {==}
1013    case 3n 3n 2n:
1014      {==}
1015    case 3n 3n 3n:
1016      {==}
1017    case 4n+r _ _:
1018      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(4n+r), u(b), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, ha))
1019    case 0n 4n+r _:
1020      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1021    case 0n 0n 4n+r:
1022      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1023    case 0n 1n 4n+r:
1024      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1025    case 0n 2n 4n+r:
1026      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1027    case 0n 3n 4n+r:
1028      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1029    case 1n 4n+r _:
1030      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1031    case 1n 0n 4n+r:
1032      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1033    case 1n 1n 4n+r:
1034      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1035    case 1n 2n 4n+r:
1036      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1037    case 1n 3n 4n+r:
1038      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1039    case 2n 4n+r _:
1040      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1041    case 2n 0n 4n+r:
1042      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1043    case 2n 1n 4n+r:
1044      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1045    case 2n 2n 4n+r:
1046      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1047    case 2n 3n 4n+r:
1048      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1049    case 3n 4n+r _:
1050      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1051    case 3n 0n 4n+r:
1052      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1053    case 3n 1n 4n+r:
1054      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1055    case 3n 2n 4n+r:
1056      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1057    case 3n 3n 4n+r:
1058      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1059
1060def sx_lt(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(x, y, z)), 64n) == True{} : Bool}:
1061  %LW.rt(x) : {Nat.is_lt(U32.to_nat(PH.sext(_, y, z)), 64n) == True{} : Bool}
1062  %LW.rt(y) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), _, z)), 64n) == True{} : Bool}
1063  %LW.rt(z) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)), 64n) == True{} : Bool}
1064  sx_lt_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
1065
1066# ---------------------------------------------------------------- base64
1067
1068def b64_rt(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {PH.unb64(PH.b64(bs)) == Some{bs} : Maybe<&2, List<&2, U32>>}:
1069  match bs:
1070    case Nil{}:
1071      {==}
1072    case +a <> Nil{}:
1073      +ha = ok_head(a, Nil{}, h)
1074      +ta = ok_tail(a, Nil{}, h)
1075      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec2(_, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0)))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1076      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0))), Some{PH.sext(PH.c0(a), 0, 0)}, digit_value(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {PH.dec2(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1077      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1078      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1079      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1080      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), 0, 0)), PH.c0(a), su_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1081      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), 0, 0)), 0, sv_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(_, 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1082      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), 0, 0)), 0, sw_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(0, 0), U32.is_eq(_, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1083      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec2_fin(_, Bool.and(U32.is_eq(0, 0), U32.is_eq(0, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1084      {==}
1085    case +a <> +b <> Nil{}:
1086      +ha = ok_head(a, b <> Nil{}, h)
1087      +ta = ok_tail(a, b <> Nil{}, h)
1088      +hb = ok_head(b, Nil{}, ta)
1089      +tb = ok_tail(b, Nil{}, ta)
1090      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec3(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1091      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1092      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0))), Some{PH.sext(PH.c1(b), PH.c0(b), 0)}, digit_value(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1093      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1094      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1095      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1096      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1097      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1098      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1099      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1100      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1101      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0, sw_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(_, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1102      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec3_fin(_, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1103      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {PH.dec3_fin(a, _, U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1104      {==}
1105    case +a <> +b <> +c <> +rest:
1106      +ha = ok_head(a, b <> c <> rest, h)
1107      +ta = ok_tail(a, b <> c <> rest, h)
1108      +hb = ok_head(b, c <> rest, ta)
1109      +tb = ok_tail(b, c <> rest, ta)
1110      +hc = ok_head(c, rest, tb)
1111      +tc = ok_tail(c, rest, tb)
1112      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec4(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1113      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1114      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, digit_value(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1115      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, digit_value(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, _, PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1116      %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(rest)), Some{rest}, b64_rt(rest, tc)) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, _) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1117      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1118      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1119      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1120      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1121      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1122      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1123      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1124      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1125      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c3(c), sw_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(_, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1126      %Equal.sym(U32, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c2(c), su_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), _, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1127      %Equal.sym(U32, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c1(c), sv_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), _, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1128      %Equal.sym(U32, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c0(c), sw_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), _) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1129      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {Some{_ <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1130      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {Some{a <> _ <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1131      %Equal.sym(U32, PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)), c, byte_rt(c, hc)) : {Some{a <> b <> _ <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1132      {==}
1133
1134# ---------------------------------------------------------------- the '$' separator
1135
1136# No character is '$'.
1137def nd(s: String) -> Bool:
1138  match s:
1139    case SNil{}:
1140      True{}
1141    case SCon{c, r}:
1142      Bool.and(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r))
1143
1144def dollar_cons(+c: Char, +r: String, +r2: String) -> {PH.dollar(SCon{c, r}) == PH.dollar(SCon{c, r2}) : Bool}:
1145  match c:
1146    case Chr{x}:
1147      {==}
1148
1149def nd_head(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {PH.dollar(SCon{c, SNil{}}) == False{} : Bool}:
1150  +e = L.and_left(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
1151  L.not_true(PH.dollar(SCon{c, SNil{}}), e)
1152
1153def nd_tail(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {nd(r) == True{} : Bool}:
1154  L.and_right(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
1155
1156# A string without '$', then '$': the field before it and the rest.
1157def field_nd(+cs: String, +r: String, +h: {nd(cs) == True{} : Bool}) -> {PH.field_go(String.append(cs, SCon{Chr{36}, r}), PH.dollar(String.append(cs, SCon{Chr{36}, r}))) == Some{PH.Cut{cs, r}} : Maybe<&2, PH.Cut>}:
1158  match cs:
1159    case SNil{}:
1160      {==}
1161    case SCon{Chr{+x}, +t}:
1162      +hd = Equal.trans(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), PH.dollar(SCon{Chr{x}, SNil{}}), False{}, dollar_cons(Chr{x}, String.append(t, SCon{Chr{36}, r}), SNil{}), nd_head(Chr{x}, t, h))
1163      %Equal.sym(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), False{}, hd) : {PH.field_go(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
1164      %Equal.sym(Maybe<&2, PH.Cut>, PH.field_go(String.append(t, SCon{Chr{36}, r}), PH.dollar(String.append(t, SCon{Chr{36}, r}))), Some{PH.Cut{t, r}}, field_nd(t, r, nd_tail(Chr{x}, t, h))) : {PH.field_cons(x, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
1165      {==}
1166
1167def b64_nd(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {nd(PH.b64(bs)) == True{} : Bool}:
1168  match bs:
1169    case Nil{}:
1170      {==}
1171    case +a <> Nil{}:
1172      +ha = ok_head(a, Nil{}, h)
1173      +ta = ok_tail(a, Nil{}, h)
1174      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}})), True{})) == True{} : Bool}
1175      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{})) == True{} : Bool}
1176      {==}
1177    case +a <> +b <> Nil{}:
1178      +ha = ok_head(a, b <> Nil{}, h)
1179      +ta = ok_tail(a, b <> Nil{}, h)
1180      +hb = ok_head(b, Nil{}, ta)
1181      +tb = ok_tail(b, Nil{}, ta)
1182      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
1183      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
1184      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{}))) == True{} : Bool}
1185      {==}
1186    case +a <> +b <> +c <> +rest:
1187      +ha = ok_head(a, b <> c <> rest, h)
1188      +ta = ok_tail(a, b <> c <> rest, h)
1189      +hb = ok_head(b, c <> rest, ta)
1190      +tb = ok_tail(b, c <> rest, ta)
1191      +hc = ok_head(c, rest, tb)
1192      +tc = ok_tail(c, rest, tb)
1193      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1194      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1195      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1196      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), nd(PH.b64(rest)))))) == True{} : Bool}
1197      %Equal.sym(Bool, nd(PH.b64(rest)), True{}, b64_nd(rest, tc)) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), _)))) == True{} : Bool}
1198      {==}
1199
1200def field_b64(+bs: List<&2, U32>, +r: String, +h: {ok(bs) == True{} : Bool}) -> {PH.field(String.append(PH.b64(bs), SCon{Chr{36}, r})) == Some{PH.Cut{PH.b64(bs), r}} : Maybe<&2, PH.Cut>}:
1201  field_nd(PH.b64(bs), r, b64_nd(bs, h))
1202
1203# ---------------------------------------------------------------- decimal
1204
1205def dd_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)) == n : Nat}:
1206  match n:
1207    case 0n:
1208      {==}
1209    case 1n:
1210      {==}
1211    case 2n:
1212      {==}
1213    case 3n:
1214      {==}
1215    case 4n:
1216      {==}
1217    case 5n:
1218      {==}
1219    case 6n:
1220      {==}
1221    case 7n:
1222      {==}
1223    case 8n:
1224      {==}
1225    case 9n:
1226      {==}
1227    case 10n+r:
1228      Empty.absurd({U32.to_nat(U32.sub(U32.add(48, U32.from_nat(10n+r)), 48)) == 10n+r : Nat}, N.lt_zero_absurd(r, h))
1229
1230def di_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {PH.is_digit(U32.add(48, U32.from_nat(n))) == True{} : Bool}:
1231  match n:
1232    case 0n:
1233      {==}
1234    case 1n:
1235      {==}
1236    case 2n:
1237      {==}
1238    case 3n:
1239      {==}
1240    case 4n:
1241      {==}
1242    case 5n:
1243      {==}
1244    case 6n:
1245      {==}
1246    case 7n:
1247      {==}
1248    case 8n:
1249      {==}
1250    case 9n:
1251      {==}
1252    case 10n+r:
1253      Empty.absurd({PH.is_digit(U32.add(48, U32.from_nat(10n+r))) == True{} : Bool}, N.lt_zero_absurd(r, h))
1254
1255def mul10_ge(+k: Nat) -> {Nat.is_le(k, Nat.mul(k, 10n)) == True{} : Bool}:
1256  match k:
1257    case 0n:
1258      {==}
1259    case 1n+ +j:
1260      +x = Nat.mul(j, 10n)
1261      +h1 = N.le_trans(j, x, Nat.add(x, 9n), mul10_ge(j), N.le_add_right(x, 9n))
1262      L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)
1263
1264# m < 9 + 10 m
1265def lt9(+m: Nat) -> {Nat.is_lt(m, Nat.add(9n, Nat.mul(m, 10n))) == True{} : Bool}:
1266  +x = Nat.mul(m, 10n)
1267  +h0 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, 9n)) == True{} : Bool}, Nat.add(x, 0n), x, N.add_zero(x), N.lt_add_left(0n, 9n, x, {==}))
1268  +h1 = N.le_lt_trans(m, x, Nat.add(x, 9n), mul10_ge(m), h0)
1269  L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)
1270
1271# n / 10 < n for n >= 1.
1272def div10_lt(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}:
1273  match n:
1274    case 0n:
1275      Empty.absurd({Nat.is_lt(Nat.div(0n, 10n), 0n) == True{} : Bool}, L.false_true(h))
1276    case 1n+ +m:
1277      +e = NR.le_div(9n, 1n+m, 1n+m)
1278      +f = N.lt_not_le(m, Nat.add(9n, Nat.mul(m, 10n)), lt9(m))
1279      N.not_le_lt(1n+m, Nat.div(1n+m, 10n), Equal.trans(Bool, Nat.is_le(1n+m, Nat.div(1n+m, 10n)), Nat.is_le(Nat.mul(1n+m, 10n), 1n+m), False{}, e, f))
1280
1281def ge10_pos(+n: Nat, +h: {Nat.is_lt(n, 10n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
1282  match n:
1283    case 0n:
1284      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_false(h))
1285    case 1n+ +m:
1286      N.zero_le(m)
1287
1288def sd_dec(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.starts_digit(String.append(PH.dec_go(f, n, acc, last), Y)) == True{} : Bool}:
1289  match f last:
1290    case 0n _:
1291      Empty.absurd({PH.starts_digit(String.append(acc, Y)) == True{} : Bool}, N.lt_zero_absurd(n, hf))
1292    case 1n+ +g True{}:
1293      di_n(n, el)
1294    case 1n+ +g False{}:
1295      +q = Nat.div(n, 10n)
1296      sd_dec(g, q, SCon{PH.dchar(Nat.mod(n, 10n)), acc}, Y, Nat.is_lt(q, 10n), {==}, N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf)))
1297
1298def dec_step(+n: Nat, +ay: String, +hr: {Nat.is_lt(Nat.mod(n, 10n), 10n) == True{} : Bool}) -> {PH.read_go(SCon{PH.dchar(Nat.mod(n, 10n)), ay}, Nat.div(n, 10n), PH.starts_digit(SCon{PH.dchar(Nat.mod(n, 10n)), ay})) == PH.read_go(ay, n, PH.starts_digit(ay)) : PH.Got}:
1299  +q = Nat.div(n, 10n)
1300  +r = Nat.mod(n, 10n)
1301  -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1302  %Equal.sym(Bool, PH.is_digit(U32.add(48, U32.from_nat(r))), True{}, di_n(r, hr)) : {PH.read_go(SCon{PH.dchar(r), ay}, q, _) == rhs : PH.Got}
1303  %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(r)), 48)), r, dd_n(r, hr)) : {PH.read_go(ay, Nat.add(Nat.mul(q, 10n), _), PH.starts_digit(ay)) == rhs : PH.Got}
1304  %NR.dm_eq(9n, n) : {PH.read_go(ay, _, PH.starts_digit(ay)) == rhs : PH.Got}
1305  {==}
1306
1307# Reading the decimal digits of n before acc gives n and acc.
1308def dec_go_rt(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.read_go(String.append(PH.dec_go(f, n, acc, last), Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}:
1309  match f last:
1310    case 0n _:
1311      Empty.absurd({PH.read_go(String.append(acc, Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}, N.lt_zero_absurd(n, hf))
1312    case 1n+ +g True{}:
1313      %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)), n, dd_n(n, el)) : {PH.read_go(String.append(acc, Y), _, PH.starts_digit(String.append(acc, Y))) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}
1314      {==}
1315    case 1n+ +g False{}:
1316      +q = Nat.div(n, 10n)
1317      +r = Nat.mod(n, 10n)
1318      +ay = String.append(acc, Y)
1319      +hr = NR.dm_lt(9n, n)
1320      +hq = N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf))
1321      -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1322      Equal.trans(PH.Got, PH.read_go(String.append(PH.dec_go(g, q, SCon{PH.dchar(r), acc}, Nat.is_lt(q, 10n)), Y), 0n, True{}), PH.read_go(SCon{PH.dchar(r), ay}, q, PH.starts_digit(SCon{PH.dchar(r), ay})), rhs,
1323        dec_go_rt(g, q, SCon{PH.dchar(r), acc}, Y, Nat.is_lt(q, 10n), {==}, hq),
1324        dec_step(n, ay, hr))
1325
1326def got_nd(+n: Nat, +c: Char, +Y: String) -> {Some{PH.read_go(SCon{c, Y}, n, False{})} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
1327  match c:
1328    case Chr{x}:
1329      {==}
1330
1331# A decimal number followed by a non-digit is read back.
1332def dec_rt(+n: Nat, +c: Char, +Y: String, +hc: {PH.starts_digit(SCon{c, Y}) == False{} : Bool}) -> {PH.read(String.append(PH.decimal(n), SCon{c, Y})) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
1333  +s = String.append(PH.dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)), SCon{c, Y})
1334  %Equal.sym(Bool, PH.starts_digit(s), True{}, sd_dec(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {PH.read_check(s, _) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1335  %Equal.sym(PH.Got, PH.read_go(s, 0n, True{}), PH.read_go(SCon{c, Y}, n, PH.starts_digit(SCon{c, Y})), dec_go_rt(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {Some{_} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1336  %Equal.sym(Bool, PH.starts_digit(SCon{c, Y}), False{}, hc) : {Some{PH.read_go(SCon{c, Y}, n, _)} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1337  got_nd(n, c, Y)
1338
1339
1340# ---------------------------------------------------------------- the PHC string
1341
1342def append_nil(+x: String) -> {String.append(x, SNil{}) == x : String}:
1343  match x:
1344    case SNil{}:
1345      {==}
1346    case SCon{+h, +t}:
1347      Equal.cong(String, String, z => SCon{h, z}, String.append(t, SNil{}), t, append_nil(t))
1348
1349# parse(format(x)) == Some{x}, for byte lists of bytes below 256.
1350def parse_format(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, +hash: List<&2, U32>, +hs: {ok(salt) == True{} : Bool}, +hh: {ok(hash) == True{} : Bool}) -> {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}:
1351  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(m), SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{m, SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(m, Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_m(_) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1352  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(t), SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{t, SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(t, Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_t(m, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1353  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(p), SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])})), Some{PH.Got{p, SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])}}}, dec_rt(p, Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)]), {==})) : {PH.parse_p(m, t, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1354  %Equal.sym(Maybe<&2, PH.Cut>, PH.field(String.append(PH.b64(salt), SCon{Chr{36}, String.concat([PH.b64(hash)])})), Some{PH.Cut{PH.b64(salt), String.concat([PH.b64(hash)])}}, field_b64(salt, String.concat([PH.b64(hash)]), hs)) : {PH.parse_salt(m, t, p, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1355  %Equal.sym(String, String.append(PH.b64(hash), SNil{}), PH.b64(hash), append_nil(PH.b64(hash))) : {PH.parse_hash(m, t, p, PH.unb64(PH.b64(salt)), PH.unb64(_)) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1356  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(salt)), Some{salt}, b64_rt(salt, hs)) : {PH.parse_hash(m, t, p, _, PH.unb64(PH.b64(hash))) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1357  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(hash)), Some{hash}, b64_rt(hash, hh)) : {PH.parse_hash(m, t, p, Some{salt}, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1358  {==}