proofs/math/typed/f64addb.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addb.bend as F64addb
20 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/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 ./f64bits.bend as FB import ./f64round.bend as FR import ./f64rtools.bend as RT import ./f64adda.bend as AA import ./f64addp.bend as AP import ./f64adds.bend as AS
Definitions
def v source · line 24 · raw
@+x:U32 -> Nat
def c62 source · line 27 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one) : Nat}
def top10 source · line 31 · 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, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(f, 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) : Nat}f << 10 plus the hidden bit at 62, with the constant on either side
def subv source · line 40 · 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) == Nat.double(t) : Nat} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sw) == S : Nat} -> @+hle:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, S), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, S)), Nat.double(t)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(tw, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(sw, d))) == Nat.sub(Nat.double(t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, S), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, S))) : Nat}the value of T - jam(S >> d) as a U64 subtraction
def hlt2 source · line 48 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+t:Nat -> @+S1:Nat -> @+d:Nat -> @+hd1:{Nat.is_le(1n, d) == True{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)) == True{} : Bool} -> @+hT62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.double(t)) == False{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1))), Nat.double(t)) == True{} : Bool}
def f63s source · line 55 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+Fr:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hk:{Nat.is_le(Nat.add(k, 53n), 63n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)))) == True{} : Bool}
def ms_le source · line 58 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+Fl:Nat -> @+m:Nat -> @+d:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, m) == True{} : Bool} -> @+hd:{Nat.is_le(1n, d) == True{} : Bool} -> {Nat.is_le(m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.add(Fl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)))) == True{} : Bool}
def smb1 source · line 65 · 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.norm_round_pack(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(el, 1n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 1073741824}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_small(1n+p, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 10n)), Nat.sub(el, 1n+p)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(el, 1n+p), Nat.add(Fl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))), Nat.add(Fs, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))), Nat.add(1925n, 1n+p)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}subMags, larger exponent el, smaller exponent es = 1 + p
def smb0 source · line 90 · 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.norm_round_pack(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(el, 1n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 1073741824}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_small(0n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 10n)), Nat.sub(el, 0n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(el, 1n), Nat.add(Fl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))), Fs), 1926n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}subMags, the smaller operand subnormal (es = 0)