~/bend-docscommunity

proofs/math/typed/w64dm.bend source

proofs/math/typed/w64dm.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/w64.bend as SWimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../lib/word.bend as WDimport ../../lib/u32.bend as Uimport ../../lib/arith.bend as AR2import ../../lib/lemmas/spec/numeric.bend as Simport ../natural/arith.bend as NRimport ../u64/u64.bend as P64import ./w64mul.bend as W64Mimport ./w64div.bend as W64Dimport ./w64add.bend as WAimport ./width.bend as WWimport ./u32laws.bend as LWimport ./natfuel.bend as NF# 64 / 64 division, a * b mod m and the 64-bit square root of# src/math/w64.bend. The quotient loop takes an estimate q with x < (q + 1) b# down while q b > x, so it ends at floor(x / b); w64est.bend shows Knuth's# normalised estimate is never below the quotient (the easy half of Theorem# B; the other half, at most 2 over, only bounds the loop's run time). The# proof is the loop invariant of the Why3 gallery's integer square root and# division examples, closed by the uniqueness of floor(x / b) (Mathlib# Nat.div_add_mod, Nat.div_eq_of_lt_le).def v(+x: U32) -> Nat:  U32.to_nat(x)def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:  LW.true_ne_false(h)def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:  LW.vb(x)def 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}:  +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)  L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, c)) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), h1)# q, bh < 1 + p, p >= 1, lo + hi (1 + p) == q bh: hi + 1 < 1 + pdef 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}:  +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)))  +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))))  +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)))  +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))  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)def P2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, C.shift(32n, one)) == True{} : Bool}:  +h = L.subst(Nat, z => {Nat.is_le(z, C.shift(31n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(31n, one))  N.double_le(1n, C.shift(31n, one), h)# the 96-bit product q b of mul_32_64: low 64 bits + 2^64 * top 32 bitsdef 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}:  +p0 = X.mul32(q, bl)  +p1 = X.mul32(q, bh)  +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))  +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))  +es = WA.acons(X.hi(p0), X.lo(p1))  +PP = C.shift(32n, one)  +pp = Nat.sub(PP, 1n)  +h2 = P2(one, h1)  +eP = N.sub_add(PP, 1n, N.le_trans(1n, 2n, PP, {==}, h2))  +hp = NF.sub_mono_l(2n, PP, 1n, h2)  +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)))  +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)))  +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)  +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)  +cb = U32.is_lt(U32.add(X.hi(p0), X.lo(p1)), X.hi(p0))  +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))))  +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)))))  +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)))  +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))  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)))))))))))))))))))def fit64(+a: WU.U64) -> {C.fits(64n, SW.value(a)) == True{} : Bool}:  match a:    case WU.U64{+l, +h}:      WW.limbs_fit(32n, 32n, v(l), v(h), vb(l), vb(h))# the 96-bit comparison of over96def 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}:  +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))  +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))  +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))  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)))))def X96(+xl: WU.U64, +xh: U32) -> Nat:  Nat.add(SW.value(xl), C.shift(64n, v(xh)))# q b > xdef 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}:  match b:    case WU.U64{+bl, +bh}:      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)))# ---- the quotient loops ----def QB(+b: WU.U64, +q: U32) -> Nat:  Nat.mul(v(q), SW.value(b))# down: q - 1 while q b > x; ends with q b <= xdef 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}:  match fu cb nq:    case 0n _ _:      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))    case 1n+g False{} _:      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))    case 1n+g True{} 0n:      +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)      +h1b = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 0n, hnq, h0)      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))    case 1n+ +g True{} 1n+ +qp:      +q1 = U32.sub(q, 1)      +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)))      +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))      qdn(g, one, h1, xl, xh, b, q1, X.over96(xl, xh, X.mul_32_64(q1, b)), qp, hf1, {==}, e1)# down keeps x < (q + 1) b: a step is taken only when x < q bdef 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}:  match fu cb nq:    case 0n _ _:      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))    case 1n+g False{} _:      hu    case 1n+g True{} 0n:      +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)      +h1b = L.subst(Nat, z => {Nat.is_lt(X96(xl, xh), Nat.mul(z, SW.value(b))) == True{} : Bool}, v(q), 0n, hnq, h0)      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))    case 1n+ +g True{} 1n+ +qp:      +q1 = U32.sub(q, 1)      +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)))      +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))      +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)      +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)      +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)      qup2(g, one, h1, xl, xh, b, q1, X.over96(xl, xh, X.mul_32_64(q1, b)), qp, hf1, {==}, e1, hu1)# r b <= x < (r + 1) b: r == x / b and x - r b == x mod bdef 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}:  +t = Nat.sub(x, Nat.mul(r, 1n+bp))  +ex = N.sub_add(x, Nat.mul(r, 1n+bp), h1)  +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)  +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)  +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)  (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)))def 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}:  (+a, +c) = p  div_uniq(x, r, bp, a, c)def 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}:  (+a, +c) = p  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))def 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}:  (+a, +c) = p  adef QS(+xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +m: U32) -> U32:  X.q_fix(Nat.add(v(q), 1n), xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)))# the down loop from an estimate q with x < (q + 1) b: q' b <= x < (q' + 1) bdef 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}:  (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))def 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}:  {==}# ---- 64 / 64 ----def 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}:  WW.fits_of_lt(k, x, N.le_lt_trans(x, y, C.pow2(k), h, WW.lt_of_fits(k, y, hy)))# a 96-bit value below 2^64 has top word 0: its low 64 bits are the valuedef 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}:  +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)))  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))def pr1(-P: Type, -Q: Type, p: P & Q) -> P:  (a, c) = p  adef pr2(-P: Type, -Q: Type, p: P & Q) -> Q:  (a, c) = p  cdef x96_0(+a: WU.U64) -> {X96(a, 0) == SW.value(a) : Nat}:  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)))def u32_0(+q: U32) -> {SW.value(WU.U64{q, 0}) == v(q) : Nat}:  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)))# a < 2^32 b for b >= 2^32def 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}:  +PP = C.shift(32n, one)  +vbv = SW.value(WU.U64{bl, bh})  +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)))  +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))))  +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))  +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})))  +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))  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)# the big-divisor quotient: q b <= a < (q + 1) bdef 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}:  +vbv = SW.value(WU.U64{bl, bh})  +hX = dm_hx(one, h1, al, ah, bl, bh, hz)  pr = qs_pair(one, h1, WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295, {==}, hX, he)  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)  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)def 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}:  +vbv = SW.value(WU.U64{bl, bh})  +hX = dm_hx(one, h1, al, ah, bl, bh, hz)  pr = qs_pair(one, h1, WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295, {==}, hX, he)  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))