1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/w64.bend as SW 4 import ../../../src/math/w64.bend as X 5 import ../../../src/math/u64.bend as WU 6 import ../../../src/math/natural.bend as M 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as L 9 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 10 import ../natural/arith.bend as NR 11 import ./width.bend as WW 12 import ./natcmp.bend as NC 13 import ./u32laws.bend as LW 14 import ./w64add.bend as WA 15 import ./w64isq.bend as ISQ 16 import ./f64round.bend as FR 17 import ./f64sqa.bend as AQ 18 import ./f64sqw.bend as QW 19 import ./w64mul.bend as W64M 20 import ./w64div.bend as W64D 21 import ../natural/sqrtn.bend as SQ2 22 23 # Facts about s = isqrt(nh) for 2^60 <= nh < 2^62 and the Karatsuba step's 24 # words (r = nh - s^2, 2 s, the quotient digit) used by f64sqr.bend. 25 26 def v(+x: U32) -> Nat: 27 U32.to_nat(x) 28 29 def mone(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(one, one) == one : Nat}: 30 L.subst(Nat, z => {Nat.mul(z, z) == z : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}) 31 32 def one_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n, one) == True{} : Bool}: 33 L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}) 34 35 # (2^k)^2 as one shift 36 def psq(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.mul(C.shift(k, one), C.shift(k, one)) == C.shift(Nat.add(k, k), one) : Nat}: 37 Equal.trans(Nat, Nat.mul(C.shift(k, one), C.shift(k, one)), C.shift(k, C.shift(k, Nat.mul(one, one))), C.shift(Nat.add(k, k), one), AQ.sh_sq(k, one), Equal.trans(Nat, C.shift(k, C.shift(k, Nat.mul(one, one))), C.shift(k, C.shift(k, one)), C.shift(Nat.add(k, k), one), Equal.cong(Nat, Nat, z => C.shift(k, C.shift(k, z)), Nat.mul(one, one), one, mone(one, h1)), Equal.sym(Nat, C.shift(Nat.add(k, k), one), C.shift(k, C.shift(k, one)), WW.shift_comp(k, k, one)))) 38 39 def lo_val(+w: WU.U64, +h: {C.fits(32n, SW.value(w)) == True{} : Bool}) -> {v(X.lo(w)) == SW.value(w) : Nat}: 40 match w: 41 case WU.U64{+l, +hh}: 42 Equal.trans(Nat, v(l), C.low(32n, SW.value(WU.U64{l, hh})), SW.value(WU.U64{l, hh}), Equal.sym(Nat, C.low(32n, SW.value(WU.U64{l, hh})), v(l), WW.low_u(32n, v(l), v(hh), LW.vb(l))), WW.low_fit(32n, SW.value(WU.U64{l, hh}), h)) 43 44 def shmk(+a: Nat, +b: Nat, +x: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(C.shift(a, x), C.shift(b, x)) == True{} : Bool}: 45 +h0 = WW.shift_mono(a, x, C.shift(Nat.sub(b, a), x), WW.shift_ge(Nat.sub(b, a), x)) 46 L.subst(Nat, z => {Nat.is_le(C.shift(a, x), z) == True{} : Bool}, C.shift(a, C.shift(Nat.sub(b, a), x)), C.shift(b, x), Equal.sym(Nat, C.shift(b, x), C.shift(a, C.shift(Nat.sub(b, a), x)), NC.sh_split(b, a, x, h)), h0) 47 48 def p_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.is_lt(C.shift(k, one), C.shift(1n+k, one)) == True{} : Bool}: 49 +g = N.le_trans(1n, one, C.shift(k, one), one_le(one, h1), WW.shift_ge(k, one)) 50 +l = N.lt_add_left(0n, C.shift(k, one), C.shift(k, one), N.lt_le_trans(0n, 1n, C.shift(k, one), {==}, g)) 51 L.subst(Nat, z => {Nat.is_lt(C.shift(k, one), z) == True{} : Bool}, Nat.add(C.shift(k, one), C.shift(k, one)), C.shift(1n+k, one), Equal.sym(Nat, Nat.double(C.shift(k, one)), Nat.add(C.shift(k, one), C.shift(k, one)), NA.double_self(C.shift(k, one))), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(C.shift(k, one), C.shift(k, one))) == True{} : Bool}, Nat.add(C.shift(k, one), 0n), C.shift(k, one), N.add_zero(C.shift(k, one)), l)) 52 53 def vn62(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}) -> {Nat.is_lt(SW.value(nh), C.shift(62n, one)) == True{} : Bool}: 54 Equal.trans(Bool, Nat.is_lt(SW.value(nh), C.shift(62n, one)), C.fits(62n, SW.value(nh)), True{}, FR.lt_fit(62n, one, h1, SW.value(nh)), h62) 55 56 def vn60(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_le(C.shift(60n, one), SW.value(nh)) == True{} : Bool}: 57 N.not_lt_le(SW.value(nh), C.shift(60n, one), Equal.trans(Bool, Nat.is_lt(SW.value(nh), C.shift(60n, one)), C.fits(60n, SW.value(nh)), False{}, FR.lt_fit(60n, one, h1, SW.value(nh)), h60)) 58 59 def iv31(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_lt(M.isqrt(SW.value(nh)), C.shift(31n, one)) == True{} : Bool}: 60 AQ.isqrt_lt(SW.value(nh), C.shift(31n, one), L.subst(Nat, z => {Nat.is_lt(SW.value(nh), z) == True{} : Bool}, C.shift(62n, one), Nat.mul(C.shift(31n, one), C.shift(31n, one)), Equal.sym(Nat, Nat.mul(C.shift(31n, one), C.shift(31n, one)), C.shift(62n, one), psq(one, h1, 31n)), vn62(one, h1, nh, h62))) 61 62 def iw_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {SW.value(X.isqrt(nh)) == M.isqrt(SW.value(nh)) : Nat}: 63 ISQ.isqrt_value(nh) 64 65 def iw32(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {C.fits(32n, SW.value(X.isqrt(nh))) == True{} : Bool}: 66 +l = N.lt_trans(M.isqrt(SW.value(nh)), C.shift(31n, one), C.shift(32n, one), iv31(one, h1, nh, h62, h60), p_lt(one, h1, 31n)) 67 WW.fits_one(32n, one, h1, SW.value(X.isqrt(nh)), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, M.isqrt(SW.value(nh)), SW.value(X.isqrt(nh)), Equal.sym(Nat, SW.value(X.isqrt(nh)), M.isqrt(SW.value(nh)), iw_v(one, h1, nh, h62, h60)), l)) 68 69 def lo_iv(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {v(X.lo(X.isqrt(nh))) == M.isqrt(SW.value(nh)) : Nat}: 70 Equal.trans(Nat, v(X.lo(X.isqrt(nh))), SW.value(X.isqrt(nh)), M.isqrt(SW.value(nh)), lo_val(X.isqrt(nh), iw32(one, h1, nh, h62, h60)), iw_v(one, h1, nh, h62, h60)) 71 72 def plus1(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.add(v(X.lo(X.isqrt(nh))), v(1)) == 1n+M.isqrt(SW.value(nh)) : Nat}: 73 Equal.trans(Nat, Nat.add(v(X.lo(X.isqrt(nh))), 1n), Nat.add(M.isqrt(SW.value(nh)), 1n), 1n+M.isqrt(SW.value(nh)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), lo_iv(one, h1, nh, h62, h60)), Equal.trans(Nat, Nat.add(M.isqrt(SW.value(nh)), 1n), 1n+Nat.add(M.isqrt(SW.value(nh)), 0n), 1n+M.isqrt(SW.value(nh)), N.add_succ(M.isqrt(SW.value(nh)), 0n), N.succ_cong(Nat.add(M.isqrt(SW.value(nh)), 0n), M.isqrt(SW.value(nh)), N.add_zero(M.isqrt(SW.value(nh)))))) 74 75 def add1_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {v(U32.add(X.lo(X.isqrt(nh)), 1)) == 1n+M.isqrt(SW.value(nh)) : Nat}: 76 +l = N.le_lt_trans(1n+M.isqrt(SW.value(nh)), C.shift(31n, one), C.shift(32n, one), N.lt_succ_le_succ(M.isqrt(SW.value(nh)), C.shift(31n, one), iv31(one, h1, nh, h62, h60)), p_lt(one, h1, 31n)) 77 +f = WW.fits_one(32n, one, h1, Nat.add(v(X.lo(X.isqrt(nh))), v(1)), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, 1n+M.isqrt(SW.value(nh)), Nat.add(v(X.lo(X.isqrt(nh))), v(1)), Equal.sym(Nat, Nat.add(v(X.lo(X.isqrt(nh))), v(1)), 1n+M.isqrt(SW.value(nh)), plus1(one, h1, nh, h62, h60)), l)) 78 Equal.trans(Nat, v(U32.add(X.lo(X.isqrt(nh)), 1)), Nat.add(v(X.lo(X.isqrt(nh))), v(1)), 1n+M.isqrt(SW.value(nh)), WA.add_exact(one, h1, X.lo(X.isqrt(nh)), 1, f), plus1(one, h1, nh, h62, h60)) 79 80 # r0 = (isqrt(nh) + 1) * 2^32 81 def r0_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {SW.value(WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}) == C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))) : Nat}: 82 +e0 = L.subst(Nat, z => {v(U32.add(X.lo(X.isqrt(nh)), 1)) == Nat.add(z, M.isqrt(SW.value(nh))) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), add1_v(one, h1, nh, h62, h60)) 83 Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.add(X.lo(X.isqrt(nh)), 1)), Nat.add(one, M.isqrt(SW.value(nh))), e0) 84 85 def nn_eq(+nh: WU.U64) -> {C.shift(64n, SW.value(nh)) == C.shift(32n, C.shift(32n, SW.value(nh))) : Nat}: 86 WW.shift_comp(32n, 32n, SW.value(nh)) 87 88 def s_lo(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_le(C.shift(32n, M.isqrt(SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))) == True{} : Bool}: 89 AQ.isqrt_ge(C.shift(64n, SW.value(nh)), C.shift(32n, M.isqrt(SW.value(nh))), L.subst(Nat, z => {Nat.is_le(z, C.shift(64n, SW.value(nh))) == True{} : Bool}, C.shift(32n, C.shift(32n, Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.mul(C.shift(32n, M.isqrt(SW.value(nh))), C.shift(32n, M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.mul(C.shift(32n, M.isqrt(SW.value(nh))), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(32n, C.shift(32n, Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), AQ.sh_sq(32n, M.isqrt(SW.value(nh)))), L.subst(Nat, z => {Nat.is_le(C.shift(32n, C.shift(32n, Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), z) == True{} : Bool}, C.shift(32n, C.shift(32n, SW.value(nh))), C.shift(64n, SW.value(nh)), Equal.sym(Nat, C.shift(64n, SW.value(nh)), C.shift(32n, C.shift(32n, SW.value(nh))), nn_eq(nh)), AQ.le_sh2(32n, Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), SW.value(nh), AQ.isl(SW.value(nh)))))) 90 91 # shift(32, isqrt nh) <= S < r0 92 def ilt1(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_lt(SW.value(nh), Nat.mul(Nat.add(one, M.isqrt(SW.value(nh))), Nat.add(one, M.isqrt(SW.value(nh))))) == True{} : Bool}: 93 L.subst(Nat, z => {Nat.is_lt(SW.value(nh), Nat.mul(Nat.add(z, M.isqrt(SW.value(nh))), Nat.add(z, M.isqrt(SW.value(nh))))) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), AQ.ilt(SW.value(nh))) 94 95 def s_hi(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +r0w: WU.U64, +hR0: {SW.value(r0w) == C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))) : Nat}, +hhi: {U32.is_zero(X.hi(r0w)) == False{} : Bool}) -> {Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), SW.value(r0w)) == True{} : Bool}: 96 +l1 = AQ.lt_sh2(32n, SW.value(nh), Nat.mul(Nat.add(one, M.isqrt(SW.value(nh))), Nat.add(one, M.isqrt(SW.value(nh)))), ilt1(one, h1, nh, h62, h60)) 97 +e1 = Equal.trans(Nat, Nat.mul(SW.value(r0w), SW.value(r0w)), Nat.mul(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh))))), C.shift(32n, C.shift(32n, Nat.mul(Nat.add(one, M.isqrt(SW.value(nh))), Nat.add(one, M.isqrt(SW.value(nh)))))), Equal.trans(Nat, Nat.mul(SW.value(r0w), SW.value(r0w)), Nat.mul(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), SW.value(r0w)), Nat.mul(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.mul(z, SW.value(r0w)), SW.value(r0w), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), hR0), Equal.cong(Nat, Nat, z => Nat.mul(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), z), SW.value(r0w), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), hR0)), AQ.sh_sq(32n, Nat.add(one, M.isqrt(SW.value(nh))))) 98 AQ.isqrt_lt(C.shift(64n, SW.value(nh)), SW.value(r0w), L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(SW.value(r0w), SW.value(r0w))) == True{} : Bool}, C.shift(32n, C.shift(32n, SW.value(nh))), C.shift(64n, SW.value(nh)), Equal.sym(Nat, C.shift(64n, SW.value(nh)), C.shift(32n, C.shift(32n, SW.value(nh))), nn_eq(nh)), L.subst(Nat, z => {Nat.is_lt(C.shift(32n, C.shift(32n, SW.value(nh))), z) == True{} : Bool}, C.shift(32n, C.shift(32n, Nat.mul(Nat.add(one, M.isqrt(SW.value(nh))), Nat.add(one, M.isqrt(SW.value(nh)))))), Nat.mul(SW.value(r0w), SW.value(r0w)), Equal.sym(Nat, Nat.mul(SW.value(r0w), SW.value(r0w)), C.shift(32n, C.shift(32n, Nat.mul(Nat.add(one, M.isqrt(SW.value(nh))), Nat.add(one, M.isqrt(SW.value(nh)))))), e1), l1))) 99 100 # S >= 2^62 101 def s62(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_le(C.shift(62n, one), M.isqrt(C.shift(64n, SW.value(nh)))) == True{} : Bool}: 102 +e1 = Equal.trans(Nat, Nat.mul(C.shift(62n, one), C.shift(62n, one)), C.shift(Nat.add(62n, 62n), one), C.shift(64n, C.shift(60n, one)), psq(one, h1, 62n), WW.shift_comp(64n, 60n, one)) 103 AQ.isqrt_ge(C.shift(64n, SW.value(nh)), C.shift(62n, one), L.subst(Nat, z => {Nat.is_le(z, C.shift(64n, SW.value(nh))) == True{} : Bool}, C.shift(64n, C.shift(60n, one)), Nat.mul(C.shift(62n, one), C.shift(62n, one)), Equal.sym(Nat, Nat.mul(C.shift(62n, one), C.shift(62n, one)), C.shift(64n, C.shift(60n, one)), e1), WW.shift_mono(64n, C.shift(60n, one), SW.value(nh), vn60(one, h1, nh, h62, h60)))) 104 105 def r0_sd(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +r0w: WU.U64, +hR0: {SW.value(r0w) == C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))) : Nat}, +hhi: {U32.is_zero(X.hi(r0w)) == False{} : Bool}) -> {Nat.add(M.isqrt(C.shift(64n, SW.value(nh))), Nat.sub(SW.value(r0w), M.isqrt(C.shift(64n, SW.value(nh))))) == SW.value(r0w) : Nat}: 106 N.sub_add(SW.value(r0w), M.isqrt(C.shift(64n, SW.value(nh))), N.lt_le(M.isqrt(C.shift(64n, SW.value(nh))), SW.value(r0w), s_hi(one, h1, nh, h62, h60, r0w, hR0, hhi))) 107 108 def r0_hi(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {U32.is_zero(X.hi(WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)})) == False{} : Bool}: 109 Equal.trans(Bool, U32.is_zero(U32.add(X.lo(X.isqrt(nh)), 1)), Nat.is_eq(v(U32.add(X.lo(X.isqrt(nh)), 1)), 0n), False{}, LW.zero_nat(U32.add(X.lo(X.isqrt(nh)), 1)), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(U32.add(X.lo(X.isqrt(nh)), 1)), 1n+M.isqrt(SW.value(nh)), add1_v(one, h1, nh, h62, h60))) 110 111 def r0_63(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +r0w: WU.U64, +hR0: {SW.value(r0w) == C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))) : Nat}, +hhi: {U32.is_zero(X.hi(r0w)) == False{} : Bool}) -> {Nat.is_le(SW.value(r0w), C.shift(63n, one)) == True{} : Bool}: 112 +l0 = N.lt_succ_le_succ(M.isqrt(SW.value(nh)), C.shift(31n, one), iv31(one, h1, nh, h62, h60)) 113 +l1 = L.subst(Nat, z => {Nat.is_le(Nat.add(z, M.isqrt(SW.value(nh))), C.shift(31n, one)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), l0) 114 +l2 = WW.shift_mono(32n, Nat.add(one, M.isqrt(SW.value(nh))), C.shift(31n, one), l1) 115 L.subst(Nat, z => {Nat.is_le(z, C.shift(63n, one)) == True{} : Bool}, C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), SW.value(r0w), Equal.sym(Nat, SW.value(r0w), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), hR0), L.subst(Nat, z => {Nat.is_le(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), z) == True{} : Bool}, C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one)), l2)) 116 117 # the quotient digits give Q = floor(nh * 2^64 / r0) 118 119 # ---- the Karatsuba (SqrtRem) step: s = isqrt(nh), r = nh - s^2, D = 2 s ---- 120 121 def not_t(+x: Bool, +h: {Bool.not(x) == True{} : Bool}) -> {x == False{} : Bool}: 122 match x: 123 case True{}: 124 Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h))) 125 case False{}: 126 {==} 127 128 # q D <= x < (q + 1) D for q = x / D 129 def dq_le(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_le(Nat.mul(Nat.div(x, D), D), x) == True{} : Bool}: 130 match D: 131 case 0n: 132 Empty.absurd({Nat.is_le(Nat.mul(Nat.div(x, 0n), 0n), x) == True{} : Bool}, N.lt_zero_absurd(0n, hD)) 133 case 1n+ +dp: 134 L.subst(Nat, z => {Nat.is_le(Nat.mul(Nat.div(x, 1n+dp), 1n+dp), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.div(x, 1n+dp), 1n+dp), Nat.mod(x, 1n+dp)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 1n+dp), 1n+dp), Nat.mod(x, 1n+dp)), NR.dm_eq(dp, x)), N.le_add_right(Nat.mul(Nat.div(x, 1n+dp), 1n+dp), Nat.mod(x, 1n+dp))) 135 136 def dq_lt(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_lt(x, Nat.mul(1n+Nat.div(x, D), D)) == True{} : Bool}: 137 match D: 138 case 0n: 139 Empty.absurd({Nat.is_lt(x, Nat.mul(1n+Nat.div(x, 0n), 0n)) == True{} : Bool}, N.lt_zero_absurd(0n, hD)) 140 case 1n+ +dp: 141 +m = Nat.mul(Nat.div(x, 1n+dp), 1n+dp) 142 +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(m, Nat.mod(x, 1n+dp)), Nat.add(m, 1n+dp)), Nat.is_lt(Nat.mod(x, 1n+dp), 1n+dp), True{}, WW.lt_cancel_l(m, Nat.mod(x, 1n+dp), 1n+dp), NR.dm_lt(dp, x)) 143 +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(m, 1n+dp)) == True{} : Bool}, Nat.add(m, Nat.mod(x, 1n+dp)), x, Equal.sym(Nat, x, Nat.add(m, Nat.mod(x, 1n+dp)), NR.dm_eq(dp, x)), h1) 144 L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, Nat.add(m, 1n+dp), Nat.add(1n+dp, m), NA.add_comm(m, 1n+dp), h2) 145 146 def s_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {v(X.lo(X.isqrt(nh))) == M.isqrt(SW.value(nh)) : Nat}: 147 lo_iv(one, h1, nh, h62, h60) 148 149 def hn_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.add(Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) == SW.value(nh) : Nat}: 150 N.sub_add(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), AQ.isl(SW.value(nh))) 151 152 def mm_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))) == Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))) : Nat}: 153 Equal.trans(Nat, SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.mul(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), W64M.mul32_value(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), Equal.trans(Nat, Nat.mul(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Nat.mul(M.isqrt(SW.value(nh)), v(X.lo(X.isqrt(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Equal.cong(Nat, Nat, z => Nat.mul(z, v(X.lo(X.isqrt(nh)))), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), s_v(one, h1, nh, h62, h60)), Equal.cong(Nat, Nat, z => Nat.mul(M.isqrt(SW.value(nh)), z), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), s_v(one, h1, nh, h62, h60)))) 154 155 def w_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))) == Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}: 156 +h = L.subst(Nat, z => {Nat.is_le(z, SW.value(nh)) == True{} : Bool}, Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Equal.sym(Nat, SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), mm_v(one, h1, nh, h62, h60)), AQ.isl(SW.value(nh))) 157 Equal.trans(Nat, SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.sub(SW.value(nh), SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), WA.sub_value(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), h), Equal.cong(Nat, Nat, z => Nat.sub(SW.value(nh), z), SW.value(X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), mm_v(one, h1, nh, h62, h60))) 158 159 # r <= 2 s, as nh < (s + 1)^2 160 def r_le(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_le(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}: 161 +e1 = Equal.trans(Nat, Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), SW.value(nh), NA.add_comm(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hn_v(one, h1, nh, h62, h60)) 162 +h1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(1n+M.isqrt(SW.value(nh)), 1n+M.isqrt(SW.value(nh)))) == True{} : Bool}, SW.value(nh), Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), e1), AQ.ilt(SW.value(nh))) 163 +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z) == True{} : Bool}, Nat.mul(1n+M.isqrt(SW.value(nh)), 1n+M.isqrt(SW.value(nh))), 1n+Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SQ2.succ_mul_succ(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), h1) 164 +h3 = Equal.trans(Bool, Nat.is_lt(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.is_lt(Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(1n+Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(1n+Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.is_lt(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), WW.lt_cancel_r(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), h2) 165 N.lt_succ_le(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), h3) 166 167 # 2 s < 2^32 168 def d_lt(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_lt(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)) == True{} : Bool}: 169 +h = iv31(one, h1, nh, h62, h60) 170 +S31 = C.shift(31n, one) 171 +l2 = N.lt_le_trans(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.add(S31, M.isqrt(SW.value(nh))), Nat.add(S31, S31), N.lt_add_r2(M.isqrt(SW.value(nh)), S31, M.isqrt(SW.value(nh)), h), N.le_add_left(M.isqrt(SW.value(nh)), S31, S31, N.lt_le(M.isqrt(SW.value(nh)), S31, h))) 172 L.subst(Nat, z => {Nat.is_lt(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), z) == True{} : Bool}, Nat.add(C.shift(31n, one), C.shift(31n, one)), C.shift(32n, one), Equal.sym(Nat, C.shift(32n, one), Nat.add(C.shift(31n, one), C.shift(31n, one)), NA.double_self(C.shift(31n, one))), l2) 173 174 def dw_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))) == Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))) : Nat}: 175 +e = Equal.trans(Nat, Nat.add(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), v(X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Equal.cong(Nat, Nat, z => Nat.add(z, v(X.lo(X.isqrt(nh)))), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), s_v(one, h1, nh, h62, h60)), Equal.cong(Nat, Nat, z => Nat.add(M.isqrt(SW.value(nh)), z), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), s_v(one, h1, nh, h62, h60))) 176 +f = WW.fits_one(32n, one, h1, Nat.add(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.add(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Equal.sym(Nat, Nat.add(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), e), d_lt(one, h1, nh, h62, h60))) 177 Equal.trans(Nat, v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(v(X.lo(X.isqrt(nh))), v(X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), WA.add_exact(one, h1, X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)), f), e) 178 179 # 2 s > 0, as nh >= 2^60 180 def d_pos(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_lt(0n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}: 181 +h1n = N.le_trans(1n, C.shift(60n, one), SW.value(nh), L.subst(Nat, o => {Nat.is_le(o, C.shift(60n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(60n, one)), vn60(one, h1, nh, h62, h60)) 182 +hs = AQ.isqrt_ge(SW.value(nh), 1n, h1n) 183 N.lt_le_trans(0n, 1n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), {==}, N.le_trans(1n, M.isqrt(SW.value(nh)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), hs, N.le_add_right(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) 184 185 def dw_nz(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {U32.is_zero(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))) == False{} : Bool}: 186 +e = Equal.trans(Bool, U32.is_zero(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.is_eq(v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), 0n), Nat.is_eq(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), 0n), LW.zero_nat(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), dw_v(one, h1, nh, h62, h60))) 187 +h = Equal.trans(Bool, Bool.not(Nat.is_eq(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), 0n)), Nat.is_lt(0n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), True{}, Equal.sym(Bool, Nat.is_lt(0n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Bool.not(Nat.is_eq(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), 0n)), QW.ltz(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), d_pos(one, h1, nh, h62, h60)) 188 Equal.trans(Bool, U32.is_zero(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.is_eq(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), 0n), False{}, e, not_t(Nat.is_eq(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), 0n), h)) 189 190 def lo_w(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))) == Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}: 191 +hr = N.le_lt_trans(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one), r_le(one, h1, nh, h62, h60), d_lt(one, h1, nh, h62, h60)) 192 +f = WW.fits_one(32n, one, h1, SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Equal.sym(Nat, SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), w_v(one, h1, nh, h62, h60)), hr)) 193 Equal.trans(Nat, v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), SW.value(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), lo_val(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), f), w_v(one, h1, nh, h62, h60)) 194 195 def q_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {SW.value(X.fst_q(X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}: 196 Equal.trans(Nat, SW.value(X.fst_q(X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.div(C.shift(32n, v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), W64D.div32_quot(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), dw_nz(one, h1, nh, h62, h60)), Equal.trans(Nat, Nat.div(C.shift(32n, v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), lo_w(one, h1, nh, h62, h60)), Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), dw_v(one, h1, nh, h62, h60)))) 197 198 def hq_le(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}) -> {Nat.is_le(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}: 199 dq_le(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), d_pos(one, h1, nh, h62, h60))