def fin_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:190
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr
import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as QV

190# roundPackToF64 of the root with its sticky bit is the spec's round
191def fin_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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +t: WU.U64, +st: Bool, +ht: {SW.value(t) == M.isqrt(C.shift(64n, SW.value(nh))) : Nat}, +hst: {st == 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)))) : Bool}) -> {F.sq_fin(e, t, st) == 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}:
192  +ev = Equal.trans(Nat, SW.value(X.or_bit(t, st)), SW.jam(SW.value(t), SF.b2n(st)), 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)))))), FL.orv(t, st), Equal.trans(Nat, SW.jam(SW.value(t), SF.b2n(st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(st)), 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)))))), Equal.cong(Nat, Nat, z => SW.jam(z, SF.b2n(st)), SW.value(t), M.isqrt(C.shift(64n, SW.value(nh))), ht), Equal.cong(Bool, Nat, z => SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(z)), st, 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)))), hst)))
193  +s63 = Equal.trans(Bool, C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), True{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(63n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.lt_le_trans(M.isqrt(C.shift(64n, SW.value(nh))), SW.value(WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}), C.shift(63n, one), QV.s_hi(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60)), QV.r0_63(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60))))
194  +s62 = Equal.trans(Bool, C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(62n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.le_not_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one), QV.s62(one, h1, nh, h62, h60)))
195  +j63 = Equal.trans(Bool, C.fits(63n, 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))))))), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), True{}, RT.jam_fits(62n, 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)))))), s63)
196  +j62 = Equal.trans(Bool, C.fits(62n, 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))))))), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), False{}, RT.jam_fits(61n, 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)))))), s62)
197  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, 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)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), 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)))))), ev), j63)
198  +h62b = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, 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)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), 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)))))), ev), j62)
199  +r1 = FR.round_pack(False{}, e, X.or_bit(t, st), x, hx, h62b, h63)
200  Equal.trans(F.F64, F.sq_fin(e, t, st), SF.round(False{}, SW.value(X.or_bit(t, st)), x), 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), r1, Equal.cong(Nat, F.F64, z => SF.round(False{}, z, x), SW.value(X.or_bit(t, st)), 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)))))), ev))
def fin_v

Uses (36)

Used by (3)
