def mant_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:84

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/src/math/f64.bend as F
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/f64light.bend as FL

84# the significand has at most 53 bits
85def mant_fits(+x: F.F64) -> {C.fits(53n, SF.mant(x)) == True{} : Bool}:
86  match x:
87    case F.Bits{+xl, +xh}:
88      WW.limbs_fit(52n, 1n, SF.frac(F.Bits{xl, xh}), SF.b2n(Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n))), FL.hF(xl, xh), b2n_fits(Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n))))