proofs/math/typed/w64dm.bend

bend-collections-laws-crypto@1.0.0.0 · 220 lines · 30 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR2
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P64
15import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
16import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64div.bend as W64D
17import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
18import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
19import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW
20import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend as NF
21
22# 64 / 64 division, a * b mod m and the 64-bit square root of
23# src/math/w64.bend. The quotient loop takes an estimate q with x < (q + 1) b
24# down while q b > x, so it ends at floor(x / b); w64est.bend shows Knuth's
25# normalised estimate is never below the quotient (the easy half of Theorem
26# B; the other half, at most 2 over, only bounds the loop's run time). The
27# proof is the loop invariant of the Why3 gallery's integer square root and
28# division examples, closed by the uniqueness of floor(x / b) (Mathlib
29# Nat.div_add_mod, Nat.div_eq_of_lt_le).
30
31def v(+x: U32) -> Nat:
32  U32.to_nat(x)
33
34def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
35  LW.true_ne_false(h)
36
37def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
38  LW.vb(x)
39
40def lt_add_pos(+a: Nat, +c: Nat, +h: {Nat.is_lt(0n, c) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, c)) == True{} : Bool}:
41  +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, 0n), Nat.add(a, c)), Nat.is_lt(0n, c), True{}, WW.lt_cancel_l(a, 0n, c), h)
42  L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, c)) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), h1)
43
44# q, bh < 1 + p, p >= 1, lo + hi (1 + p) == q bh: hi + 1 < 1 + p
45def hi_lt(+p: Nat, +q: Nat, +bh: Nat, +lo: Nat, +hi: Nat, +hq: {Nat.is_lt(q, 1n+p) == True{} : Bool}, +hb: {Nat.is_lt(bh, 1n+p) == True{} : Bool}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +e: {Nat.add(lo, Nat.mul(hi, 1n+p)) == Nat.mul(q, bh) : Nat}) -> {Nat.is_lt(Nat.add(hi, 1n), 1n+p) == True{} : Bool}:
46  +h1 = N.le_trans(Nat.mul(q, bh), Nat.mul(p, bh), Nat.mul(p, p), AR2.mul_le(q, p, bh, N.lt_succ_le(q, p, hq)), W64M.le_mul_r(p, bh, p, N.lt_succ_le(bh, p, hb)))
47  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(p, p), z) == True{} : Bool}, Nat.add(p, Nat.mul(p, p)), Nat.mul(p, 1n+p), Equal.sym(Nat, Nat.mul(p, 1n+p), Nat.add(p, Nat.mul(p, p)), NA.mul_succ(p, p)), L.subst(Nat, z => {Nat.is_lt(Nat.mul(p, p), z) == True{} : Bool}, Nat.add(Nat.mul(p, p), p), Nat.add(p, Nat.mul(p, p)), N.add_comm(Nat.mul(p, p), p), lt_add_pos(Nat.mul(p, p), p, N.lt_le_trans(0n, 1n, p, {==}, hp))))
48  +h3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(hi, 1n+p), z) == True{} : Bool}, Nat.add(lo, Nat.mul(hi, 1n+p)), Nat.mul(q, bh), e, L.subst(Nat, z => {Nat.is_le(Nat.mul(hi, 1n+p), z) == True{} : Bool}, Nat.add(Nat.mul(hi, 1n+p), lo), Nat.add(lo, Nat.mul(hi, 1n+p)), N.add_comm(Nat.mul(hi, 1n+p), lo), N.le_add_right(Nat.mul(hi, 1n+p), lo)))
49  +h4 = W64D.lt_cancel_mul(hi, p, 1n+p, N.le_lt_trans(Nat.mul(hi, 1n+p), Nat.mul(p, p), Nat.mul(p, 1n+p), N.le_trans(Nat.mul(hi, 1n+p), Nat.mul(q, bh), Nat.mul(p, p), h3, h1), h2))
50  L.subst(Nat, z => {Nat.is_lt(z, 1n+p) == True{} : Bool}, 1n+hi, Nat.add(hi, 1n), Equal.sym(Nat, Nat.add(hi, 1n), 1n+hi, WA.plus1(hi)), h4)
51
52def P2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, C.shift(32n, one)) == True{} : Bool}:
53  +h = L.subst(Nat, z => {Nat.is_le(z, C.shift(31n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(31n, one))
54  N.double_le(1n, C.shift(31n, one), h)
55
56# the 96-bit product q b of mul_32_64: low 64 bits + 2^64 * top 32 bits
57def mul3264(+one: Nat, +h1: {one == 1n : Nat}, +q: U32, +bl: U32, +bh: U32) -> {Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))))) == Nat.mul(v(q), SW.value(WU.U64{bl, bh})) : Nat}:
58  +p0 = X.mul32(q, bl)
59  +p1 = X.mul32(q, bh)
60  +e0 = Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), SW.value(p0), Nat.mul(v(q), v(bl)), Equal.sym(Nat, SW.value(p0), Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), WA.val_eta(p0)), W64M.mul32_value(q, bl))
61  +e1 = Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), SW.value(p1), Nat.mul(v(q), v(bh)), Equal.sym(Nat, SW.value(p1), Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), WA.val_eta(p1)), W64M.mul32_value(q, bh))
62  +es = WA.acons(X.hi(p0), X.lo(p1))
63  +PP = C.shift(32n, one)
64  +pp = Nat.sub(PP, 1n)
65  +h2 = P2(one, h1)
66  +eP = N.sub_add(PP, 1n, N.le_trans(1n, 2n, PP, {==}, h2))
67  +hp = NF.sub_mono_l(2n, PP, 1n, h2)
68  +hq = L.subst(Nat, z => {Nat.is_lt(v(q), z) == True{} : Bool}, PP, 1n+pp, Equal.sym(Nat, 1n+pp, PP, eP), WW.lt_one(32n, one, h1, v(q), vb(q)))
69  +hbh = L.subst(Nat, z => {Nat.is_lt(v(bh), z) == True{} : Bool}, PP, 1n+pp, Equal.sym(Nat, 1n+pp, PP, eP), WW.lt_one(32n, one, h1, v(bh), vb(bh)))
70  +e1p = Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bh))), Nat.mul(v(X.hi(X.mul32(q, bh))), 1n+pp)), Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), Nat.mul(v(q), v(bh)), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bh))), z), Nat.mul(v(X.hi(X.mul32(q, bh))), 1n+pp), C.shift(32n, v(X.hi(X.mul32(q, bh)))), Equal.sym(Nat, C.shift(32n, v(X.hi(X.mul32(q, bh)))), Nat.mul(v(X.hi(X.mul32(q, bh))), 1n+pp), Equal.trans(Nat, C.shift(32n, v(X.hi(X.mul32(q, bh)))), Nat.mul(v(X.hi(X.mul32(q, bh))), PP), Nat.mul(v(X.hi(X.mul32(q, bh))), 1n+pp), WW.shift_mul_one(32n, one, h1, v(X.hi(X.mul32(q, bh)))), Equal.cong(Nat, Nat, z => Nat.mul(v(X.hi(X.mul32(q, bh))), z), PP, 1n+pp, Equal.sym(Nat, 1n+pp, PP, eP))))), e1)
71  +hh = hi_lt(pp, v(q), v(bh), v(X.lo(X.mul32(q, bh))), v(X.hi(X.mul32(q, bh))), hq, hbh, hp, e1p)
72  +cb = U32.is_lt(U32.add(X.hi(p0), X.lo(p1)), X.hi(p0))
73  +ecb = Equal.trans(Nat, v(X.b32(cb)), S.bit_value(cb), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), W64M.b32_v(cb), Equal.cong(Bool, Nat, z => S.bit_value(z), cb, P64.carry32(X.hi(p0), X.lo(p1)), P64.add_lt(X.hi(p0), X.lo(p1))))
74  +hle = L.subst(Nat, z => {Nat.is_le(Nat.add(v(X.hi(X.mul32(q, bh))), z), Nat.add(v(X.hi(X.mul32(q, bh))), 1n)) == True{} : Bool}, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.b32(cb)), Equal.sym(Nat, v(X.b32(cb)), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), ecb), N.le_add_left(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), 1n, v(X.hi(X.mul32(q, bh))), W64M.bit_le1(P64.carry32(X.hi(p0), X.lo(p1)))))
75  +hfit = WW.fits_one(32n, one, h1, Nat.add(v(X.hi(X.mul32(q, bh))), v(X.b32(cb))), L.subst(Nat, z => {Nat.is_lt(Nat.add(v(X.hi(X.mul32(q, bh))), v(X.b32(cb))), z) == True{} : Bool}, 1n+pp, PP, eP, N.le_lt_trans(Nat.add(v(X.hi(X.mul32(q, bh))), v(X.b32(cb))), Nat.add(v(X.hi(X.mul32(q, bh))), 1n), 1n+pp, hle, hh)))
76  +etop = Equal.trans(Nat, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))), Nat.add(v(X.hi(X.mul32(q, bh))), v(X.b32(cb))), Nat.add(v(X.hi(X.mul32(q, bh))), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), WA.add_exact(one, h1, X.hi(p1), X.b32(cb), hfit), Equal.cong(Nat, Nat, z => Nat.add(v(X.hi(X.mul32(q, bh))), z), v(X.b32(cb)), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), ecb))
77  Equal.sym(Nat, Nat.mul(v(q), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.trans(Nat, Nat.mul(v(q), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.mul(v(q), v(bl)), Nat.mul(v(q), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), NA.mul_add_left(v(q), v(bl), C.shift(32n, v(bh))), Equal.trans(Nat, Nat.add(Nat.mul(v(q), v(bl)), Nat.mul(v(q), C.shift(32n, v(bh)))), Nat.add(Nat.mul(v(q), v(bl)), C.shift(32n, Nat.mul(v(q), v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(q), v(bl)), z), Nat.mul(v(q), C.shift(32n, v(bh))), C.shift(32n, Nat.mul(v(q), v(bh))), WW.shift_mul_r(32n, v(q), v(bh))), Equal.trans(Nat, Nat.add(Nat.mul(v(q), v(bl)), C.shift(32n, Nat.mul(v(q), v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), C.shift(32n, Nat.mul(v(q), v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, Nat.mul(v(q), v(bh)))), Nat.mul(v(q), v(bl)), Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), Equal.sym(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), Nat.mul(v(q), v(bl)), e0)), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), C.shift(32n, Nat.mul(v(q), v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), C.shift(32n, Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), C.shift(32n, z)), Nat.mul(v(q), v(bh)), Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), Equal.sym(Nat, Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), Nat.mul(v(q), v(bh)), e1)), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), C.shift(32n, Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), z), C.shift(32n, Nat.add(v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), WW.shift_add(32n, v(X.lo(X.mul32(q, bh))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl))))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), NA.add_assoc(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(X.hi(X.mul32(q, bl)))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), z), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), Nat.add(C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), NA.add_assoc(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh)))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(z, C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), C.shift(32n, Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh))))), Equal.sym(Nat, C.shift(32n, Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh))))), Nat.add(C.shift(32n, v(X.hi(X.mul32(q, bl)))), C.shift(32n, v(X.lo(X.mul32(q, bh))))), WW.shift_add(32n, v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh)))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, Nat.add(v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, z), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh)))), Nat.add(v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), Equal.sym(Nat, Nat.add(v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), Nat.add(v(X.hi(X.mul32(q, bl))), v(X.lo(X.mul32(q, bh)))), es)), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, Nat.add(v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(z, C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), C.shift(32n, Nat.add(v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), WW.shift_add(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), Nat.add(C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), z), Nat.add(Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), Nat.add(C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), NA.add_assoc(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), Nat.add(C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), z)), Nat.add(C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), C.shift(32n, Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Equal.sym(Nat, C.shift(32n, Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))), Nat.add(C.shift(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, v(X.hi(X.mul32(q, bh)))))), WW.shift_add(32n, C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh))))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh)))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, z))), Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))), Equal.sym(Nat, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))), Nat.add(C.shift(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, v(X.hi(X.mul32(q, bh))))), WW.shift_add(32n, WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))), Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.sym(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))))), Nat.add(v(X.lo(X.mul32(q, bl))), Nat.add(C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))))), NA.add_assoc(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), z), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))), C.shift(64n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))), Equal.sym(Nat, C.shift(64n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))), C.shift(32n, C.shift(32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))), WW.shift_comp(32n, 32n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, Nat.add(v(X.hi(X.mul32(q, bh))), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))))), Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, z)), Nat.add(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh)))), Nat.add(v(X.hi(X.mul32(q, bh))), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), N.add_comm(WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))), v(X.hi(X.mul32(q, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(q, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh)))))), C.shift(64n, z)), Nat.add(v(X.hi(X.mul32(q, bh))), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))), Equal.sym(Nat, v(U32.add(X.hi(X.mul32(q, bh)), X.b32(U32.is_lt(U32.add(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))), X.hi(X.mul32(q, bl)))))), Nat.add(v(X.hi(X.mul32(q, bh))), WA.bv(P64.carry32(X.hi(X.mul32(q, bl)), X.lo(X.mul32(q, bh))))), etop)))))))))))))))))))
78
79def fit64(+a: WU.U64) -> {C.fits(64n, SW.value(a)) == True{} : Bool}:
80  match a:
81    case WU.U64{+l, +h}:
82      WW.limbs_fit(32n, 32n, v(l), v(h), vb(l), vb(h))
83
84# the 96-bit comparison of over96
85def ov96(+xl: WU.U64, +xh: U32, +pl: WU.U64, +ph: U32) -> {X.over96(xl, xh, (pl, ph)) == Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))) : Bool}:
86  +e1 = Equal.cong(Bool, Bool, z => Bool.or(z, Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), U32.is_lt(xh, ph), Nat.is_lt(v(xh), v(ph)), U.is_lt_nat(xh, ph))
87  +e2 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(z, X.lt(xl, pl))), U32.is_eq(xh, ph), Nat.is_eq(v(xh), v(ph)), LW.eq_nat(xh, ph))
88  +e3 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), z)), X.lt(xl, pl), Nat.is_lt(SW.value(xl), SW.value(pl)), WA.lt_value(xl, pl))
89  Equal.trans(Bool, X.over96(xl, xh, (pl, ph)), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e1, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e2, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), Nat.is_lt(SW.value(xl), SW.value(pl)))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e3, WW.lt_limbs(64n, SW.value(xl), v(xh), SW.value(pl), v(ph), fit64(xl), fit64(pl)))))
90
91def X96(+xl: WU.U64, +xh: U32) -> Nat:
92  Nat.add(SW.value(xl), C.shift(64n, v(xh)))
93
94# q b > x
95def ovq(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32) -> {X.over96(xl, xh, X.mul_32_64(q, b)) == Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(b))) : Bool}:
96  match b:
97    case WU.U64{+bl, +bh}:
98      Equal.trans(Bool, X.over96(xl, xh, (X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))), Nat.is_lt(X96(xl, xh), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))))), Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(WU.U64{bl, bh}))), ov96(xl, xh, X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))), Equal.cong(Nat, Bool, z => Nat.is_lt(X96(xl, xh), z), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))))), Nat.mul(v(q), SW.value(WU.U64{bl, bh})), mul3264(one, h1, q, bl, bh)))
99
100# ---- the quotient loops ----
101
102def QB(+b: WU.U64, +q: U32) -> Nat:
103  Nat.mul(v(q), SW.value(b))
104
105# down: q - 1 while q b > x; ends with q b <= x
106def qdn(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +cb: Bool, +nq: Nat, +hf: {Nat.is_lt(v(q), fu) == True{} : Bool}, +hc: {X.over96(xl, xh, X.mul_32_64(q, b)) == cb : Bool}, +hnq: {v(q) == nq : Nat}) -> {Nat.is_le(QB(b, X.q_fix(fu, xl, xh, b, q, cb)), X96(xl, xh)) == True{} : Bool}:
107  match fu cb nq:
108    case 0n _ _:
109      Empty.absurd({Nat.is_le(QB(b, X.q_fix(0n, xl, xh, b, q, cb)), X96(xl, xh)) == True{} : Bool}, N.lt_zero_absurd(v(q), hf))
110    case 1n+g False{} _:
111      N.not_lt_le(X96(xl, xh), QB(b, q), Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), False{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc))
112    case 1n+g True{} 0n:
113      +h0 = Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), True{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc)
114      +h1b = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 0n, hnq, h0)
115      Empty.absurd({Nat.is_le(QB(b, X.q_fix(1n+g, xl, xh, b, q, True{})), X96(xl, xh)) == True{} : Bool}, N.lt_zero_absurd(X96(xl, xh), h1b))
116    case 1n+ +g True{} 1n+ +qp:
117      +q1 = U32.sub(q, 1)
118      +e1 = Equal.trans(Nat, v(q1), Nat.sub(v(q), 1n), qp, U.sub_nat(q, 1, L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+qp, v(q), Equal.sym(Nat, v(q), 1n+qp, hnq), N.zero_le(qp))), Equal.trans(Nat, Nat.sub(v(q), 1n), Nat.sub(1n+qp, 1n), qp, Equal.cong(Nat, Nat, t => Nat.sub(t, 1n), v(q), 1n+qp, hnq), N.sub_zero(qp)))
119      +hf1 = L.subst(Nat, z => {Nat.is_lt(z, g) == True{} : Bool}, qp, v(q1), Equal.sym(Nat, v(q1), qp, e1), L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, v(q), 1n+qp, hnq, hf))
120      qdn(g, one, h1, xl, xh, b, q1, X.over96(xl, xh, X.mul_32_64(q1, b)), qp, hf1, {==}, e1)
121
122# down keeps x < (q + 1) b: a step is taken only when x < q b
123def qup2(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +cb: Bool, +nq: Nat, +hf: {Nat.is_lt(v(q), fu) == True{} : Bool}, +hc: {X.over96(xl, xh, X.mul_32_64(q, b)) == cb : Bool}, +hnq: {v(q) == nq : Nat}, +hu: {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), SW.value(b))) == True{} : Bool}) -> {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(fu, xl, xh, b, q, cb)), SW.value(b))) == True{} : Bool}:
124  match fu cb nq:
125    case 0n _ _:
126      Empty.absurd({Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(0n, xl, xh, b, q, cb)), SW.value(b))) == True{} : Bool}, N.lt_zero_absurd(v(q), hf))
127    case 1n+g False{} _:
128      hu
129    case 1n+g True{} 0n:
130      +h0 = Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), True{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc)
131      +h1b = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 0n, hnq, h0)
132      Empty.absurd({Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(X.q_fix(1n+g, xl, xh, b, q, True{})), SW.value(b))) == True{} : Bool}, N.lt_zero_absurd(X96(xl, xh), h1b))
133    case 1n+ +g True{} 1n+ +qp:
134      +q1 = U32.sub(q, 1)
135      +e1 = Equal.trans(Nat, v(q1), Nat.sub(v(q), 1n), qp, U.sub_nat(q, 1, L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+qp, v(q), Equal.sym(Nat, v(q), 1n+qp, hnq), N.zero_le(qp))), Equal.trans(Nat, Nat.sub(v(q), 1n), Nat.sub(1n+qp, 1n), qp, Equal.cong(Nat, Nat, t => Nat.sub(t, 1n), v(q), 1n+qp, hnq), N.sub_zero(qp)))
136      +hf1 = L.subst(Nat, z => {Nat.is_lt(z, g) == True{} : Bool}, qp, v(q1), Equal.sym(Nat, v(q1), qp, e1), L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, v(q), 1n+qp, hnq, hf))
137      +h0 = Equal.trans(Bool, Nat.is_lt(X96(xl, xh), QB(b, q)), X.over96(xl, xh, X.mul_32_64(q, b)), True{}, Equal.sym(Bool, X.over96(xl, xh, X.mul_32_64(q, b)), Nat.is_lt(X96(xl, xh), QB(b, q)), ovq(one, h1, xl, xh, b, q)), hc)
138      +h2 = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 1n+qp, hnq, h0)
139      +hu1 = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(1n+z, SW.value(b))) == True{} : Bool}, qp, v(q1), Equal.sym(Nat, v(q1), qp, e1), h2)
140      qup2(g, one, h1, xl, xh, b, q1, X.over96(xl, xh, X.mul_32_64(q1, b)), qp, hf1, {==}, e1, hu1)
141
142# r b <= x < (r + 1) b: r == x / b and x - r b == x mod b
143def div_uniq(+x: Nat, +r: Nat, +bp: Nat, +h1: {Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool}, +h2: {Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
144  +t = Nat.sub(x, Nat.mul(r, 1n+bp))
145  +ex = N.sub_add(x, Nat.mul(r, 1n+bp), h1)
146  +h3 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+bp, Nat.mul(r, 1n+bp))) == True{} : Bool}, x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex), h2)
147  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), z) == True{} : Bool}, Nat.add(1n+bp, Nat.mul(r, 1n+bp)), Nat.add(Nat.mul(r, 1n+bp), 1n+bp), N.add_comm(1n+bp, Nat.mul(r, 1n+bp)), h3)
148  +ht = Equal.trans(Bool, Nat.is_lt(t, 1n+bp), Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), Nat.add(Nat.mul(r, 1n+bp), 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), Nat.add(Nat.mul(r, 1n+bp), 1n+bp)), Nat.is_lt(t, 1n+bp), WW.lt_cancel_l(Nat.mul(r, 1n+bp), t, 1n+bp)), h4)
149  (Equal.trans(Nat, Nat.div(x, 1n+bp), Nat.div(Nat.add(Nat.mul(r, 1n+bp), t), 1n+bp), r, Equal.cong(Nat, Nat, z => Nat.div(z, 1n+bp), x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex)), NR.div_of(r, bp, t, ht)), Equal.trans(Nat, Nat.mod(x, 1n+bp), Nat.mod(Nat.add(Nat.mul(r, 1n+bp), t), 1n+bp), t, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex)), NR.mod_of(r, bp, t, ht)))
150
151def qs_fin(+x: Nat, +r: Nat, +bp: Nat, +hB: {SW.value(WU.U64{0, 0}) == 0n : Nat}, p: {Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
152  (+a, +c) = p
153  div_uniq(x, r, bp, a, c)
154
155def qs_fin2(+x: Nat, +r: Nat, +B: Nat, +bp: Nat, +hB: {B == 1n+bp : Nat}, p: {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
156  (+a, +c) = p
157  div_uniq(x, r, bp, L.subst(Nat, z => {Nat.is_le(Nat.mul(r, z), x) == True{} : Bool}, B, 1n+bp, hB, a), L.subst(Nat, z => {Nat.is_lt(x, Nat.mul(1n+r, z)) == True{} : Bool}, B, 1n+bp, hB, c))
158
159def qle_fin(+x: Nat, +r: Nat, +B: Nat, p: {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool}:
160  (+a, +c) = p
161  a
162
163def QS(+xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +m: U32) -> U32:
164  X.q_fix(Nat.add(v(q), 1n), xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)))
165
166# the down loop from an estimate q with x < (q + 1) b: q' b <= x < (q' + 1) b
167def qs_pair(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}, +hX: {Nat.is_lt(X96(xl, xh), Nat.mul(C.shift(32n, one), SW.value(b))) == True{} : Bool}, +hu: {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), SW.value(b))) == True{} : Bool}) -> {Nat.is_le(QB(b, QS(xl, xh, b, q, m)), X96(xl, xh)) == True{} : Bool} & {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(QS(xl, xh, b, q, m)), SW.value(b))) == True{} : Bool}:
168  (qdn(Nat.add(v(q), 1n), one, h1, xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)), v(q), L.subst(Nat, z => {Nat.is_lt(v(q), z) == True{} : Bool}, 1n+v(q), Nat.add(v(q), 1n), Equal.sym(Nat, Nat.add(v(q), 1n), 1n+v(q), WA.plus1(v(q))), N.lt_succ(v(q))), {==}, {==}), qup2(Nat.add(v(q), 1n), one, h1, xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)), v(q), L.subst(Nat, z => {Nat.is_lt(v(q), z) == True{} : Bool}, 1n+v(q), Nat.add(v(q), 1n), Equal.sym(Nat, Nat.add(v(q), 1n), 1n+v(q), WA.plus1(v(q))), N.lt_succ(v(q))), {==}, {==}, hu))
169
170def impl_qs(+xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32) -> {X.q_start(xl, xh, b, q) == QS(xl, xh, b, q, 4294967295) : U32}:
171  {==}
172
173# ---- 64 / 64 ----
174
175def fits_le(+k: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}, +hy: {C.fits(k, y) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
176  WW.fits_of_lt(k, x, N.le_lt_trans(x, y, C.pow2(k), h, WW.lt_of_fits(k, y, hy)))
177
178# a 96-bit value below 2^64 has top word 0: its low 64 bits are the value
179def low_exact(+r: Nat, +t: Nat, +x: Nat, +e: {Nat.add(r, C.shift(64n, t)) == x : Nat}, +hr: {C.fits(64n, r) == True{} : Bool}, +hx: {C.fits(64n, x) == True{} : Bool}) -> {r == x : Nat}:
180  +et = Equal.trans(Nat, t, C.high(64n, Nat.add(r, C.shift(64n, t))), 0n, Equal.sym(Nat, C.high(64n, Nat.add(r, C.shift(64n, t))), t, WW.high_u(64n, r, t, hr)), Equal.trans(Nat, C.high(64n, Nat.add(r, C.shift(64n, t))), C.high(64n, x), 0n, Equal.cong(Nat, Nat, z => C.high(64n, z), Nat.add(r, C.shift(64n, t)), x, e), N.eq_from_is_eq(C.high(64n, x), 0n, hx)))
181  Equal.trans(Nat, r, Nat.add(r, C.shift(64n, 0n)), x, Equal.sym(Nat, Nat.add(r, C.shift(64n, 0n)), r, Equal.trans(Nat, Nat.add(r, C.shift(64n, 0n)), Nat.add(r, 0n), r, Equal.cong(Nat, Nat, z => Nat.add(r, z), C.shift(64n, 0n), 0n, WW.shift_zero(64n)), N.add_zero(r))), Equal.trans(Nat, Nat.add(r, C.shift(64n, 0n)), Nat.add(r, C.shift(64n, t)), x, Equal.cong(Nat, Nat, z => Nat.add(r, C.shift(64n, z)), 0n, t, Equal.sym(Nat, t, 0n, et)), e))
182
183def pr1(-P: Type, -Q: Type, p: P & Q) -> P:
184  (a, c) = p
185  a
186
187def pr2(-P: Type, -Q: Type, p: P & Q) -> Q:
188  (a, c) = p
189  c
190
191def x96_0(+a: WU.U64) -> {X96(a, 0) == SW.value(a) : Nat}:
192  Equal.trans(Nat, Nat.add(SW.value(a), C.shift(64n, 0n)), Nat.add(SW.value(a), 0n), SW.value(a), Equal.cong(Nat, Nat, z => Nat.add(SW.value(a), z), C.shift(64n, 0n), 0n, WW.shift_zero(64n)), N.add_zero(SW.value(a)))
193
194def u32_0(+q: U32) -> {SW.value(WU.U64{q, 0}) == v(q) : Nat}:
195  Equal.trans(Nat, Nat.add(v(q), C.shift(32n, 0n)), Nat.add(v(q), 0n), v(q), Equal.cong(Nat, Nat, z => Nat.add(v(q), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(q)))
196
197# a < 2^32 b for b >= 2^32
198def dm_hx(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +hz: {U32.is_zero(bh) == False{} : Bool}) -> {Nat.is_lt(X96(WU.U64{al, ah}, 0), Nat.mul(C.shift(32n, one), SW.value(WU.U64{bl, bh}))) == True{} : Bool}:
199  +PP = C.shift(32n, one)
200  +vbv = SW.value(WU.U64{bl, bh})
201  +hbh = L.subst(Nat, z => {Nat.is_le(z, v(bh)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), WA.pos_ne(v(bh), Equal.trans(Bool, Nat.is_eq(v(bh), 0n), U32.is_zero(bh), False{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(v(bh), 0n), LW.zero_nat(bh)), hz)))
202  +hPb = N.le_trans(PP, C.shift(32n, v(bh)), vbv, WW.shift_mono(32n, one, v(bh), hbh), L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(bh)), z) == True{} : Bool}, Nat.add(C.shift(32n, v(bh)), v(bl)), vbv, N.add_comm(C.shift(32n, v(bh)), v(bl)), N.le_add_right(C.shift(32n, v(bh)), v(bl))))
203  +eS = Equal.trans(Nat, C.shift(64n, one), C.shift(32n, PP), Nat.mul(PP, PP), WW.shift_comp(32n, 32n, one), WW.shift_mul_one(32n, one, h1, PP))
204  +ha = L.subst(Nat, z => {Nat.is_lt(SW.value(WU.U64{al, ah}), z) == True{} : Bool}, C.shift(64n, one), Nat.mul(PP, PP), eS, WW.lt_one(64n, one, h1, SW.value(WU.U64{al, ah}), fit64(WU.U64{al, ah})))
205  +hX0 = N.lt_le_trans(SW.value(WU.U64{al, ah}), Nat.mul(PP, PP), Nat.mul(PP, vbv), ha, W64M.le_mul_r(PP, PP, vbv, hPb))
206  L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(PP, vbv)) == True{} : Bool}, SW.value(WU.U64{al, ah}), X96(WU.U64{al, ah}, 0), Equal.sym(Nat, X96(WU.U64{al, ah}, 0), SW.value(WU.U64{al, ah}), x96_0(WU.U64{al, ah})), hX0)
207
208# the big-divisor quotient: q b <= a < (q + 1) b
209def dm_pair(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +e: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +he: {Nat.is_lt(X96(WU.U64{al, ah}, 0), Nat.mul(1n+v(e), SW.value(WU.U64{bl, bh}))) == True{} : Bool}, +bp: Nat, +hB: {SW.value(WU.U64{bl, bh}) == 1n+bp : Nat}) -> {Nat.div(SW.value(WU.U64{al, ah}), 1n+bp) == v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)) : Nat} & {Nat.mod(SW.value(WU.U64{al, ah}), 1n+bp) == Nat.sub(SW.value(WU.U64{al, ah}), Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat}:
210  +vbv = SW.value(WU.U64{bl, bh})
211  +hX = dm_hx(one, h1, al, ah, bl, bh, hz)
212  pr = qs_pair(one, h1, WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295, {==}, hX, he)
213  dv = qs_fin2(X96(WU.U64{al, ah}, 0), v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), vbv, bp, hB, pr)
214  L.subst(Nat, z => {Nat.div(z, 1n+bp) == v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)) : Nat} & {Nat.mod(z, 1n+bp) == Nat.sub(z, Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat}, X96(WU.U64{al, ah}, 0), SW.value(WU.U64{al, ah}), x96_0(WU.U64{al, ah}), dv)
215
216def dm_le(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +e: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +he: {Nat.is_lt(X96(WU.U64{al, ah}, 0), Nat.mul(1n+v(e), SW.value(WU.U64{bl, bh}))) == True{} : Bool}) -> {Nat.is_le(Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), SW.value(WU.U64{bl, bh})), SW.value(WU.U64{al, ah})) == True{} : Bool}:
217  +vbv = SW.value(WU.U64{bl, bh})
218  +hX = dm_hx(one, h1, al, ah, bl, bh, hz)
219  pr = qs_pair(one, h1, WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295, {==}, hX, he)
220  L.subst(Nat, z => {Nat.is_le(Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), vbv), z) == True{} : Bool}, X96(WU.U64{al, ah}, 0), SW.value(WU.U64{al, ah}), x96_0(WU.U64{al, ah}), qle_fin(X96(WU.U64{al, ah}, 0), v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), vbv, pr))