~/bend-docscommunity

proofs/math/typed/f64adda.bend checks

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

22 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 ../../../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 ../../lib/word.bend as WD
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64mulp.bend as MP
import ./f64addp.bend as AP

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def shl_v source · line 30 · 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 c61 source · line 35 · raw

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

def top9 source · line 39 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(f) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 29n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(f, 9n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(9n, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) : Nat}

f << 9 plus the hidden bit at 61: the significand at bit 61

def nlb source · line 48 · 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 51 · 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 amb_core source · line 56 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+S:Nat -> @+d:Nat -> @+x0:Nat -> @+hsig:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, S), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, S)), Nat.double(t)) : Nat} -> @+he:{Nat.add(Nat.add(x0, d), 2180n) == e : Nat} -> @+hx1:{Nat.is_le(1n, Nat.add(x0, d)) == True{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, S) == True{} : Bool} -> @+ht62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.double(t)) == True{} : Bool} -> @+ht61:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(61n, Nat.double(t)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, e, sig) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(S, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.double(t))), x0) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def addc source · line 78 · raw

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

def n52 source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+Fr:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) == False{} : Bool}

def f53 source · line 87 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+Fr:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) == True{} : Bool}

def sh9 source · line 90 · raw

@+k:Nat -> @+m:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(9n, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(9n, m)) == True{} : Bool}

def shc source · line 93 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, m)) : Nat}

def sigv source · line 97 · raw

@+tw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+sw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+S:Nat -> @+d:Nat -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tw) == T : Nat} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sw) == S : Nat} -> @+hT:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, T) == True{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, S) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(tw, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(sw, d))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, S), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, S)), T) : Nat}

the aligned sum value: T + jam(S >> d)

def amb1 source · line 109 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+p:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(1n+p, el) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, el), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 536870912}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 9n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_small(1n+p, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 9n)), Nat.sub(el, 1n+p)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Nat.add(Fs, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(el, 1n+p), Nat.add(Fl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)))), Nat.add(1925n, 1n+p)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

addMags, larger exponent el, smaller exponent es = 1 + p

def amb0 source · line 131 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(0n, el) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, el), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 536870912}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 9n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_small(0n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 9n)), Nat.sub(el, 0n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Fs, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(el, 1n), Nat.add(Fl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)))), 1926n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

addMags, larger exponent el, the smaller operand subnormal (es = 0)