proofs/math/typed/f64addc.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as F64addc
23 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 ./u32laws.bend as LW import ./w64add.bend as WA import ./w64sh.bend as SH import ./natcmp.bend as NC import ./natfuel.bend as NF import ./f64bits.bend as FB import ./f64round.bend as FR import ./f64bl.bend as BL import ./f64rtools.bend as RT
Definitions
def v source · line 28 · raw
@+x:U32 -> Nat
def bz0 source · line 31 · 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}
def bz source · line 39 · raw
@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}a zero pattern with sign s
def max_le source · line 42 · raw
@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.max(a, b) == b : Nat}
def cp_c source · line 52 · raw
@+x:Nat -> @+y:Nat -> @+c:Cmp -> @+hc:{Nat.cmp(x, y) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.cmp_pick(Nat.is_lt(x, y), Nat.is_eq(x, y)) == c : Cmp}X.cmp is the order of the values
def cmpv source · line 61 · raw
@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.cmp(a, b) == Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Cmp}
def addv2 source · line 68 · raw
@+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fb) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(fa, fb)) == Nat.add(Fa, Fb) : Nat}
def shl_v source · line 73 · 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 f53 source · line 76 · 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 r1926 source · line 80 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, m) == True{} : Bool} -> @+u:Nat -> @+hu:{u == 1926n : Nat} -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, 1926n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, Nat.add(m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}a sum below 2^53 at the subnormal exponent is exact
def ame0 source · line 101 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fb) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.pack(s, 0n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(fa, fb)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Fa, Fb), 1926n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}addMags, both subnormal: pack(s, 0, fa + fb)
def swap4 source · line 109 · raw
@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
def c53 source · line 113 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 21n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one) : Nat}
def amen source · line 117 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fb) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 21n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, e), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(fa, fb)), 9n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Nat.add(Fa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)), Nat.add(Fb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))), Nat.add(1925n, e)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}addMags, equal normal exponents e: the 54-bit sum at bit 62