~/bend-docscommunity

proofs/math/typed/f64cmp.bend checks

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

17 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 ../../lib/u32.bend as U
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./f64bits.bend as FB
import ./natcmp.bend as NC

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def shmk source · line 32 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, x)) == True{} : Bool}

shift(a, x) <= shift(b, x) for a <= b

def gub source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+E:Nat -> @+b:Bool -> @+hb:{Nat.is_eq(E, 0n) == b : Bool} -> @+c:Nat -> @+hc:{c == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b)) : Nat} -> @+F:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b, 1n, E), Nat.add(F, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) == True{} : Bool}

G < 2^(1+E) * 2^52

def glb source · line 55 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+E:Nat -> @+c:Nat -> @+hc:{c == 1n : Nat} -> @+F:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(E, Nat.add(F, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c)))) == True{} : Bool}

a normal G is at least 2^E * 2^52

def gcmp_lt source · line 62 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+E1:Nat -> @+b1:Bool -> @+hb1:{Nat.is_eq(E1, 0n) == b1 : Bool} -> @+c1:Nat -> @+hc1:{c1 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b1)) : Nat} -> @+F1:Nat -> @+hF1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F1) == True{} : Bool} -> @+E2:Nat -> @+c2:Nat -> @+hc2:{c2 == 1n : Nat} -> @+F2:Nat -> @+hlt:{Nat.is_lt(E1, E2) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b1, 1n, E1), Nat.add(F1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, False{}, 1n, E2), Nat.add(F2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c2)))) == True{} : Bool}

def gcmp_c source · line 71 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+E1:Nat -> @+b1:Bool -> @+hb1:{Nat.is_eq(E1, 0n) == b1 : Bool} -> @+c1:Nat -> @+hc1:{c1 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b1)) : Nat} -> @+F1:Nat -> @+hF1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F1) == True{} : Bool} -> @+E2:Nat -> @+b2:Bool -> @+hb2:{Nat.is_eq(E2, 0n) == b2 : Bool} -> @+c2:Nat -> @+hc2:{c2 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b2)) : Nat} -> @+F2:Nat -> @+hF2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F2) == True{} : Bool} -> @+d:Cmp -> @+hd:{Nat.cmp(E1, E2) == d : Cmp} -> {Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b1, 1n, E1), Nat.add(F1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b2, 1n, E2), Nat.add(F2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c2)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(d, Nat.cmp(F1, F2)) : Cmp}

G orders like (E, F) lexicographically

def gcmp source · line 96 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+E1:Nat -> @+b1:Bool -> @+hb1:{Nat.is_eq(E1, 0n) == b1 : Bool} -> @+c1:Nat -> @+hc1:{c1 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b1)) : Nat} -> @+F1:Nat -> @+hF1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F1) == True{} : Bool} -> @+E2:Nat -> @+b2:Bool -> @+hb2:{Nat.is_eq(E2, 0n) == b2 : Bool} -> @+c2:Nat -> @+hc2:{c2 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b2)) : Nat} -> @+F2:Nat -> @+hF2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, F2) == True{} : Bool} -> {Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b1, 1n, E1), Nat.add(F1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b2, 1n, E2), Nat.add(F2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, c2)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(Nat.cmp(E1, E2), Nat.cmp(F1, F2)) : Cmp}

def hF source · line 101 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == True{} : Bool}

def esub source · line 104 · raw

@+E:Nat -> {Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n) == Nat.add(1925n, E) : Nat}

def xsh source · line 108 · raw

@+E:Nat -> @+b:Bool -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n)), m) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1925n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b, 1n, E), m)) : Nat}

2^xexp = 2^1925 * 2^e' with e' = max(E, 1)

def xshx source · line 123 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1925n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0n), 1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x))) : Nat}

xsh at a double, stated with SF.xexp as mcf uses it (the unfolding of xexp is a small step here, so no conversion walks C.shift(1925n, _))

def mcf source · line 128 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> {Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))) == Nat.cmp(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) : Cmp}

the finite branch of mag_cmp compares K

def and_l source · line 140 · raw

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

def and_r source · line 147 · raw

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

def or_l source · line 154 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {a == False{} : Bool}

def or_r source · line 161 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {b == False{} : Bool}

def nl source · line 169 · raw

@+a:Bool -> @+d:Bool -> @+hi:{Bool.and(a, d) == False{} : Bool} -> @+hn:{Bool.and(a, Bool.not(d)) == False{} : Bool} -> {a == False{} : Bool}

neither infinite nor NaN: the exponent field is not 2047

def lt2047 source · line 178 · raw

@+xl:U32 -> @+xh:U32 -> @+hi:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == True{} : Bool}

def magc_c source · line 182 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+nx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+ny:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == False{} : Bool} -> @+ix:Bool -> @+hix:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == ix : Bool} -> @+iy:Bool -> @+hiy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == iy : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, ix, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, iy, EQ{}, GT{}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, iy, LT{}, Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))))) == Nat.cmp(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) : Cmp}

def magc source · line 207 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+nx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+ny:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == Nat.cmp(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) : Cmp}

mag_cmp is the order of K on doubles that are not NaN

def magQ source · line 211 · raw

@+xl:U32 -> @+xh:U32 -> {Nat.add(v(xl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(xh)))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}))) : Nat}

the magnitude word is K

def magv source · line 217 · raw

@+xl:U32 -> @+xh:U32 -> @+m31:U32 -> @+hm31:{m31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{xl, U32.and(xh, m31)}) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}))) : Nat}

def hm source · line 222 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+nx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+ny:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) : Bool}

def hm2 source · line 228 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+nx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+ny:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))) : Bool}

def lts source · line 235 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+sa:Bool -> @+sb:Bool -> @+mc:Cmp -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == Cmp.is_lt(mc) : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(mc)) : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt_s(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, sa, sb) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(sa, sb)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(mc), mc), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, LT{}, GT{}))) : Bool}

def nlf source · line 246 · raw

@+c:Cmp -> {Bool.not(Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(c))) == Cmp.is_le(c) : Bool}

def nlc source · line 255 · raw

@+c:Cmp -> {Bool.not(Cmp.is_lt(c)) == Cmp.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(c)) : Bool}

def eqflip source · line 264 · raw

@+c:Cmp -> {Cmp.is_eq(c) == Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(c)) : Bool}

def andff source · line 273 · raw

@+a:Bool -> @+b:Bool -> {Bool.and(a, Bool.and(b, False{})) == False{} : Bool}

def les source · line 282 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+sa:Bool -> @+sb:Bool -> @+mc:Cmp -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == Cmp.is_lt(mc) : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(mc)) : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.le_s(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, sa, sb) == Cmp.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(sa, sb)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(mc), mc), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, LT{}, GT{}))) : Bool}

def eqs source · line 293 · raw

@+eL:Bool -> @+eW:Bool -> @+sa:Bool -> @+sb:Bool -> @+mc:Cmp -> @+h:{Bool.and(eL, eW) == Cmp.is_eq(mc) : Bool} -> {Bool.and(eL, Bool.and(eW, Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(sa), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(sb)))) == Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(sa, sb)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(mc), mc), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, sa, LT{}, GT{}))) : Bool}

def lt_gen source · line 304 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+bad:Bool -> @+hbad:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == bad : Bool} -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, bad, z) == Bool.and(Bool.not(bad), Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, z, EQ{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), LT{}, GT{}))))) : Bool}

def le_gen source · line 316 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+bad:Bool -> @+hbad:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == bad : Bool} -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.le_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, bad, z) == Bool.and(Bool.not(bad), Cmp.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, z, EQ{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), LT{}, GT{}))))) : Bool}

def hq source · line 328 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+nx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == False{} : Bool} -> @+ny:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == False{} : Bool} -> {Bool.and(Nat.is_eq(v(xl), v(yl)), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(xh)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(yh)))) == Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) : Bool}

def hw source · line 335 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> {U32.is_eq(xh, yh) == Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(xh)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(yh))), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) : Bool}

the high words are equal when sign and the low 31 bits are

def eq_gen source · line 342 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+bad:Bool -> @+hbad:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) == bad : Bool} -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.eq_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, bad, z) == Bool.and(Bool.not(bad), Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, z, EQ{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, Bool.not(Bool.xor(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mag_cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Cmp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), LT{}, GT{}))))) : Bool}

def lt_value source · line 354 · raw

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

def le_value source · line 362 · raw

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

def eq_value source · line 370 · raw

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