~/bend-docscommunity

proofs/math/typed/f64exp.bend checks

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

21 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/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./w64sh.bend as SH
import ./w64clz.bend as CZ
import ./f64bits.bend as FB
import ./f64round.bend as FR
import ./u32laws.bend as LW
import ../../lib/word.bend as WD
import ./f64bl.bend as BL
import ./f64rtools.bend as RT
import ./f64tools.bend as T
import ./f64rint.bend as RI

Definitions

def sub_le_self source · line 33 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}

def rne_zero source · line 45 · raw

@+m:Nat -> @+j:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, m) == True{} : Bool} -> @+hj:{Nat.is_le(53n, j) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 1n+j) == 0n : Nat}

m < 2^53 divided by 2^(1+j) >= 2^54 rounds to 0

def max_le source · line 61 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.max(a, b) == b : Nat}

def bz0 source · line 71 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, U32.from_nat(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, s, one, 0n)))} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, 0}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

a zero pattern with sign s (as f64addc.bz)

def bz source · line 78 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ru source · line 83 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+u:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, m, x, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_le(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), m)), u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round_u unfolded at an abstract ulp u: instantiated at a literal u, the checker never evaluates pack's closed exponent arithmetic

def tiny_c source · line 86 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, m) == True{} : Bool} -> @+hx:{Nat.is_lt(x, 63n) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def tiny source · line 121 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, m) == True{} : Bool} -> @+hx:{Nat.is_lt(x, 63n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ee_c source · line 126 · raw

@+t:Nat -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_pick(t, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp, c, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{False{}, Nat.sub(t, 3000n)}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{True{}, Nat.sub(3000n, t)}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp}

def exp_eq source · line 133 · raw

@+t:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_of(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.exp_of(t) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp}

def FIN source · line 136 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp)

def fx_nz source · line 139 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fx_fin(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x), Nat.sub(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)))) == FIN(x) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp)}

def fxz_c source · line 167 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+iz:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fx_z(x, iz) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp), iz, (x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{False{}, 0n}), FIN(x)) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp)}

def fx_c source · line 174 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+t:Bool -> @+z:Bool -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fx_cls(x, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp), Bool.and(t, Bool.not(z)), (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{False{}, 0n}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp), Bool.or(Bool.and(t, z), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x)), (x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{False{}, 0n}), FIN(x))) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp)}

def frexp_value source · line 184 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Frexp.value(x)

def LD source · line 190 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def rwx source · line 194 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+u:Nat -> @+hu:{Nat.is_le(63n, u) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_w(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), u, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the round_w of the significand at scale u is the spec's round at u

def slt source · line 201 · raw

@+a:Nat -> @+k:Nat -> @+h:{Nat.is_lt(a, Nat.add(k, 63n)) == True{} : Bool} -> {Nat.is_lt(Nat.sub(a, k), 63n) == True{} : Bool}

a - k < 63 when a < k + 63

def ldn_c source · line 212 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+k:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), Nat.add(k, 63n)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ld_neg(x, k, c) == LD(x, True{}, k) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ldf_c source · line 227 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ld_fin(x, neg, k) == LD(x, neg, k) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ldz_c source · line 237 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> @+iz:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ld_z(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{neg, k}, iz) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, iz, x, LD(x, neg, k)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ld_c source · line 244 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> @+t:Bool -> @+z:Bool -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ld_cls(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp{neg, k}, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(t, Bool.not(z)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.and(t, z), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x)), x, LD(x, neg, k))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ldexp_value source · line 254 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Ldexp.value(x, neg, k)