proofs/math/typed/f64mulf.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulf.bend as F64mulf

20 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ./width.bend as WW
import ../../lib/word.bend as WD
import ./w64sh.bend as SH
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64rtools.bend as RT
import ./f64norm.bend as NM
import ./f64mexp.bend as EX
import ./f64mul.bend as MU

Definitions

def v source · line 24 · raw

@+x:U32 -> Nat

def hea source · line 29 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def fval_g source · line 32 · raw

@+xl:U32 -> @+xh:U32 -> @+m:U32 -> @+hm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{xl, U32.and(xh, m)}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def hfa source · line 35 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def nlb source · line 38 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(1n+k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == c : Bool} -> {c == True{} : Bool}

def nfit_bl source · line 46 · raw

@+k:Nat -> @+m:Nat -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == False{} : Bool} -> {Nat.is_le(1n+k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == True{} : Bool}

def smul source · line 49 · raw

@+k:Nat -> @+j:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.add(k, j), Nat.mul(x, y)) : Nat}

def mfin source · line 54 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+hzx:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n)) == False{} : Bool} -> @+hzy:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), Nat.sub(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}