~/bend-docscommunity

proofs/math/typed/f64mul.bend checks

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

18 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 ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR2
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64mul.bend as W64M
import ./w64sh.bend as SH
import ./w64m128.bend as M128
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64mulp.bend as MP

Definitions

def fits_mul source · line 25 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), Nat.mul(x, y)) == True{} : Bool}

def nfits_mul source · line 29 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == False{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), Nat.mul(x, y)) == False{} : Bool}

def shl_v source · line 37 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+j:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> @+hj:{Nat.is_le(Nat.add(k, j), 64n) == True{} : Bool} -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(a, k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a)) : Nat}

def m128g source · line 42 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(a, b))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(a, b))))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Nat}

def mc2 source · line 48 · raw

@+s:Bool -> @+e:Nat -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+P:Nat -> @+hp:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == P : Nat} -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, x) == True{} : Bool} -> @+h127:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(127n, P) == True{} : Bool} -> @+h125:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(125n, P) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(ph, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nz(pl))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, P), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, P)), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the 128-bit product jammed to 64 bits and rounded by rp62

def mcore source · line 67 · raw

@+s:Bool -> @+e:Nat -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+P:Nat -> @+hp:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(p)))) == P : Nat} -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, x) == True{} : Bool} -> @+h127:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(127n, P) == True{} : Bool} -> @+h125:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(125n, P) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul_n2(s, e, p) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, P), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, P)), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}