def cl_t

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:343

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64E
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as QV

343# q < 2^32: the digit as it is
344def cl_t(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == 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}, +hu: {v(uu) == Nat.mod(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}, +hz: {U32.is_zero(X.hi(qq)) == True{} : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, True{}) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:
345  +eq1 = Equal.trans(Nat, v(X.lo(qq)), SW.value(qq), 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)))), W64E.lo_hi0(qq, hz), hq)
346  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(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)))), Nat.mod(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))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(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)))), v(uu)), Nat.add(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)))), Nat.mod(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.add(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), v(X.lo(qq)), 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)))), eq1), Equal.cong(Nat, Nat, z => Nat.add(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)))), z), v(uu), Nat.mod(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)))), hu)), dmq(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))), QV.d_pos(one, h1, nh, h62, h60)))
347  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.mod(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)))), v(uu), Equal.sym(Nat, v(uu), Nat.mod(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)))), hu), N.lt_le(Nat.mod(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))), dml(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))), QV.d_pos(one, h1, nh, h62, h60))))
348  +hQ = WW.lt_one(32n, one, h1, v(X.lo(qq)), LW.vb(X.lo(qq)))
349  qu_v(one, h1, nh, h62, h60, e, x, hx, X.lo(qq), uu, hc, hU, hQ)