proofs/math/typed/f64mulp.bend checks

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

19 imports

import Base
import ./f64light.bend as FL
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/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64bits.bend as FB
import ./f64round.bend as FR
import ./f64rtools.bend as RT

Definitions

def v source · line 25 · raw

@+x:U32 -> Nat

def orv_c source · line 29 · raw

@+l:U32 -> @+h:U32 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b)) : Nat}

or_bit(a, b) is jam(a, b)

def orv source · line 32 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b)) : Nat}

def minz source · line 35 · raw

@+r:Nat -> {Nat.min(r, 0n) == 0n : Nat}

def jmin source · line 39 · raw

@+q:Nat -> @+r:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(r, 0n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(q, r) : Nat}

jam reads only whether r is zero

def lt62 source · line 44 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(sig, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) : Bool}

def rp62_c source · line 49 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, x) == True{} : Bool} -> @+h61:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(61n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == f : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62_pick(s, e, sig, f) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rp62_g source · line 70 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, x) == True{} : Bool} -> @+h61:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(61n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62_pick(s, e, sig, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(sig, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rp62 source · line 75 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, x) == True{} : Bool} -> @+h61:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(61n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, e, sig) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

SoftFloat's rp62(s, e, sig) for sig in [2^61, 2^63) is round(s, sig, e - 2180)