~/bend-docscommunity

proofs/math/typed/f64mulc.bend checks

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

11 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./u32laws.bend as LW
import ./f64bits.bend as FB
import ./f64round.bend as FR

Definitions

def v source · line 15 · raw

@+x:U32 -> Nat

def hea source · line 20 · 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 mimpl source · line 23 · raw

@+s:Bool -> @+a1:Bool -> @+b1:Bool -> @+c1:Bool -> @+a2:Bool -> @+b2:Bool -> @+c2:Bool -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def mspec source · line 26 · raw

@+s:Bool -> @+a1:Bool -> @+b1:Bool -> @+c1:Bool -> @+a2:Bool -> @+b2:Bool -> @+c2:Bool -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def ion source · line 29 · raw

@+s:Bool -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf_or_nan(s, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def zero_v source · line 36 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ne2047 source · line 43 · raw

@+E:Nat -> {Bool.and(Nat.is_eq(E, 2047n), Nat.is_eq(E, 0n)) == False{} : Bool}

def sh3 source · line 50 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_z(s, ea, fa, eb, fb, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, z, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sh2 source · line 57 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_b(s, ea, fa, eb, fb, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sh1 source · line 64 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_cls(s, ea, fa, eb, fb, t) == mimpl(s, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa), Nat.is_eq(ea, 0n), Nat.is_eq(eb, 2047n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb), Nat.is_eq(eb, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def mant0 source · line 71 · raw

@+xl:U32 -> @+xh:U32 -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == 0n : Nat}

def zx source · line 75 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s) == 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}

def zy source · line 78 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n) == True{} : Bool} -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s) == 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}

def mcase source · line 82 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+r1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+a1:Bool -> @+ha1:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == a1 : Bool} -> @+b1:Bool -> @+hb1:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == b1 : Bool} -> @+c1:Bool -> @+hc1:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == c1 : Bool} -> @+a2:Bool -> @+ha2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n) == a2 : Bool} -> @+b2:Bool -> @+hb2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n) == b2 : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n) == c2 : Bool} -> @+hR:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.and(c1, b1), Bool.and(c2, b2))), r2, r1) == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> @+hZ:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.or(a1, a2), Bool.not(Bool.or(Bool.and(c1, b1), Bool.and(c2, b2)))), r2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s)) == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> {mimpl(s, a1, b1, c1, a2, b2, c2, r1) == mspec(s, a1, b1, c1, a2, b2, c2, r2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}