~/bend-docscommunity

proofs/math/typed/f64round.bend checks

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

23 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 ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./f64bits.bend as FB
import ./natcmp.bend as NC
import ./w64sh.bend as SH
import ../../lib/u32.bend as U
import ../../lib/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ../../lib/word.bend as WD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../../src/math/natural.bend as M
import ../natural/bits.bend as BT

Definitions

def pk_t source · line 37 · raw

@-T:Data -> @+a:T -> @+b:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(T, True{}, a, b) == a : T}

SF.pick on a known Bool, as lemmas: rewriting with these keeps a conversion syntactic instead of unfolding (and normalizing) both branches

def pk_f source · line 40 · raw

@-T:Data -> @+a:T -> @+b:T -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(T, False{}, a, b) == b : T}

def v source · line 43 · raw

@+x:U32 -> Nat

def bits source · line 48 · raw

@+s:Bool -> @+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def enc_bits source · line 51 · raw

@+s:Bool -> @+ef:Nat -> @+f:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, ef, f) == bits(s, Nat.add(f, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, ef))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rne_c source · line 64 · raw

@+q:Nat -> @+c:Cmp -> Nat

def rne_cmp source · line 67 · raw

@+q:Nat -> @+r:Nat -> @+h:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne_up(q, r, h) == rne_c(q, Nat.cmp(r, h)) : Nat}

def lex_assoc source · line 70 · raw

@+x:Cmp -> @+y:Cmp -> @+z:Cmp -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(x, y), z) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(x, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(y, z)) : Cmp}

def fz source · line 79 · raw

@+d:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(d, 0n) == True{} : Bool}

def small source · line 86 · raw

@+t:Nat -> @+ht:{Nat.is_le(t, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, t) == True{} : Bool}

def bit_small source · line 95 · raw

@+t:Nat -> @+ht:{Nat.is_le(t, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(t) == t : Nat}

def half_small source · line 104 · raw

@+t:Nat -> @+ht:{Nat.is_le(t, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(t) == 0n : Nat}

def max_le1 source · line 113 · raw

@+b:Nat -> @+l:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> {Nat.is_le(Nat.max(b, Nat.min(l, 1n)), 1n) == True{} : Bool}

def tl source · line 135 · raw

@+b:Nat -> @+l:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natcmp.lex(Nat.cmp(b, 0n), Nat.cmp(l, 0n)) == Nat.cmp(Nat.max(b, Nat.min(l, 1n)), 0n) : Cmp}

the sticky bit merges the parity bit with "some lower bit is set"

def jam_form source · line 149 · raw

@+h:Nat -> @+l:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l) == Nat.add(Nat.max(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(h), Nat.min(l, 1n)), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(h))) : Nat}

jam(H, L) is H with bit 0 replaced by t = max(bit H, [L > 0])

def sticky source · line 158 · raw

@+i:Nat -> @+D:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, Nat.add(2n+i, D)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(D, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(D, m)), 2n+i) : Nat}

rounding m by K + D bits is rounding jam(m >> D, m mod 2^D) by K bits, K >= 2

def fits_add1 source · line 182 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == True{} : Bool} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, b) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, Nat.add(a, b)) == True{} : Bool}

def bit_le_self source · line 190 · raw

@+n:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n), n) == True{} : Bool}

def sub_add_r source · line 199 · raw

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

def cvb source · line 204 · raw

@+l:U32 -> @+h:U32 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clear0(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}), Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}), 2n)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) : Nat}

the value of clear0(r, b): r, or r with bit 0 cleared

def cv source · line 225 · raw

@+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clear0(r, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, b, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 2n)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r)) : Nat}

def tie_v source · line 231 · raw

@+l:U32 -> @+h:U32 -> {U32.is_eq(U32.and(l, 1023), 512) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(10n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})), 512n) : Bool}

the tie test reads the low 10 bits

def parq source · line 237 · raw

@+q:Nat -> {Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(q), 1n))) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(Nat.add(q, 1n))) : Nat}

def subm source · line 246 · raw

@+n:Nat -> {Nat.sub(n, Nat.mod(n, 2n)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n)) : Nat}

def rp_c source · line 249 · raw

@+q0:Nat -> @+r0:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(10n, r0) == True{} : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(r0, 512n) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne_up(q0, r0, 512n) : Nat}

def rpv source · line 282 · raw

@+l:U32 -> @+h:U32 -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clear0(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}), 10n) : Nat}

the rounded significand of roundPackToF64 is rne(sig, 10)

def bits_of source · line 296 · raw

@+s:Bool -> @+n:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w) == Nat.add(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(s))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.pack64(w) == bits(s, n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sgn_pick source · line 309 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sgn(s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(U32, s, 2147483648, 0) : U32}

def pb source · line 316 · raw

@+s:Bool -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, s, one, 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(s) : Nat}

def sgv0 source · line 323 · raw

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

def sgv source · line 330 · raw

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

def b2n_le source · line 333 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(s)) == True{} : Bool}

def mulv source · line 341 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+c:U32 -> @+h:{Nat.is_lt(Nat.mul(v(a), v(c)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {v(U32.mul(a, c)) == Nat.mul(v(a), v(c)) : Nat}

a product below 2^32 is exact

def hwv source · line 353 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+he:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, e) == True{} : Bool} -> @+c31:U32 -> @+hc31:{c31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> {v(U32.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, e)) : Nat}

the high word of packToF64's addend: 2^31 s + 2^20 e

def pack_g source · line 369 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+he:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, e) == True{} : Bool} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, e))) == True{} : Bool} -> @+c31:U32 -> @+hc31:{c31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.pack64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, U32.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}, m)) == bits(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, e))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

SoftFloat's packToF64: the pattern of (s, e, m) is bits(s, m + 2^52 e)

def pack_v source · line 377 · raw

@+s:Bool -> @+e:Nat -> @+he:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, e) == True{} : Bool} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, e))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.pack(s, e, m) == bits(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, e))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def inf_v source · line 381 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.inf(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bl_gt source · line 390 · raw

@+k:Nat -> @+n:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) == False{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, n) == True{} : Bool} -> @+hg:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(2n+k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == 1n+k : Nat}

def bl_c source · line 400 · raw

@+k:Nat -> @+n:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) == False{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, n) == True{} : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 1n+k) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == 1n+k : Nat}

def bl63 source · line 412 · raw

@+m:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, m) == False{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m) == 63n : Nat}

def nz_of source · line 415 · raw

@+k:Nat -> @+m:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == False{} : Bool} -> {Nat.is_eq(m, 0n) == False{} : Bool}

def fits_hc source · line 423 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(a, b), n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(a, n)) : Bool}

fits(a + b, n) is fits(b, n >> a)

def b2n_le1 source · line 426 · raw

@+c:Bool -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(c), 1n) == True{} : Bool}

def rne_lb source · line 433 · raw

@+m:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 10n)) == True{} : Bool}

def rne_ub source · line 436 · raw

@+m:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 10n), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 1n)) == True{} : Bool}

def succ_le source · line 439 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, 1n), b) == True{} : Bool}

def rne_top source · line 443 · raw

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

a 63-bit m rounds to at most 2^53

def nfit_c source · line 447 · raw

@+k:Nat -> @+a:Nat -> @+r:Nat -> @+hle:{Nat.is_le(a, r) == True{} : Bool} -> @+f:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == False{} : Bool} -> @+b:Bool -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == b : Bool} -> {b == False{} : Bool}

def nfit source · line 454 · raw

@+k:Nat -> @+a:Nat -> @+r:Nat -> @+hle:{Nat.is_le(a, r) == True{} : Bool} -> @+f:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == False{} : Bool}

def rne_norm source · line 458 · raw

@+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, m) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 10n)) == False{} : Bool}

a normalized m (bit 62 set) rounds to a normal significand

def lt_fit source · line 464 · raw

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

n < 2^k as fits

def efv source · line 472 · raw

@+u:Nat -> @+EF:Nat -> @+hu:{Nat.add(EF, 1926n) == u : Nat} -> {Nat.sub(Nat.add(u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) == 1n+EF : Nat}

def ef2v source · line 478 · raw

@+u:Nat -> @+EF:Nat -> @+hu:{Nat.add(EF, 1926n) == u : Nat} -> {Nat.sub(Nat.add(1n+u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) == 2n+EF : Nat}

def add1c source · line 484 · raw

@+a:Nat -> @+k:Nat -> {Nat.add(a, k) == Nat.add(k, a) : Nat}

def hi_one source · line 488 · raw

@+H0:Nat -> @+a:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(H0), 0n) == True{} : Bool} -> @+b:{Nat.is_eq(H0, 0n) == False{} : Bool} -> {H0 == 1n : Nat}

the high part of a q in [2^52, 2^53) is 1

def f53h source · line 497 · raw

@+q:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(52n, q)), 0n) : Bool}

def top_q source · line 500 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == False{} : Bool} -> {q == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, Nat.double(one)) : Nat}

def pkg_c source · line 505 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+f53:Bool -> @+h53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == f53 : Bool} -> @+f52:Bool -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == f52 : Bool} -> @+h0:{Bool.or(Bool.not(f52), Nat.is_eq(EF, 0n)) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, f53, 1n, 2n)), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, f53, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, f52, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0n, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0n)) == bits(s, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def pkg source · line 532 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+h0:{Bool.or(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q)), Nat.is_eq(EF, 0n)) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, q, u) == bits(s, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def pko_c source · line 535 · raw

@+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+f53:Bool -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, f53, 1n, 2n)), 2047n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, f53, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0n, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.inf(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def pko source · line 547 · raw

@+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q), 1n, 2n)), 2047n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, q, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.inf(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def hsp source · line 552 · raw

@+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(m, 512n)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(10n, m), 512n))) : Nat}

def mod_sh source · line 555 · raw

@+k:Nat -> @+x:Nat -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+k, x), 2n) == 0n : Nat}

def fsub_c source · line 558 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+R0:Nat -> @+hR:{Nat.is_le(R0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+k, one)) == True{} : Bool} -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, R0) == f : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))) == f : Bool}

def fpk source · line 569 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+R0:Nat -> @+hR:{Nat.is_le(R0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, t, Nat.sub(R0, Nat.mod(R0, 2n)), R0)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, R0) : Bool}

def le1 source · line 576 · raw

@+t:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, t) == True{} : Bool} -> {Nat.is_le(t, 1n) == True{} : Bool}

def R_le source · line 585 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {Nat.is_le(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(10n, m), 512n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool}

def p2 source · line 592 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 10n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(m, 512n)) : Bool}

the rounded significand overflows 53 bits exactly when m + 2^9 overflows 63

def ovle source · line 600 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(sig, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{512, 0})) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 512n))) : Bool}

SoftFloat's carry test: 2^63 <= sig + 2^9

def ze0 source · line 612 · raw

@+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero_e(0n, z) == 0n : Nat}

def rpw source · line 619 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clear0(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(w, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{512, 0}), 10n), U32.is_eq(U32.and(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(w), 1023), 512))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n) : Nat}

def max_r source · line 624 · raw

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

def max_l source · line 633 · raw

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

def ge_or source · line 644 · raw

@+c:Nat -> @+n:Nat -> {Bool.or(Nat.is_lt(c, n), Nat.is_eq(n, c)) == Nat.is_le(c, n) : Bool}

def le_succ_lt source · line 655 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}

def and_f source · line 670 · raw

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

def or_f source · line 677 · raw

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

def or_t source · line 684 · raw

@+b:Bool -> {Bool.or(b, True{}) == True{} : Bool}

def not_t source · line 691 · raw

@+b:Bool -> @+h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def not_f source · line 698 · raw

@+b:Bool -> @+h:{Bool.not(b) == False{} : Bool} -> {b == True{} : Bool}

def pick_lt source · line 705 · raw

@+c:Bool -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c, 1n, 2n), 2047n) == True{} : Bool}

def ov_c source · line 713 · raw

@+EF:Nat -> @+f:Bool -> {Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), Bool.not(f))) == Bool.not(Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, f, 1n, 2n)), 2047n)) : Bool}

the overflow test of roundPackToF64 against the spec's exponent field

def eq_cancel_r source · line 724 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.is_eq(Nat.add(a, c), Nat.add(b, c)) == Nat.is_eq(a, b) : Bool}

def sub_cancel_r source · line 727 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.sub(Nat.add(a, c), Nat.add(b, c)) == Nat.sub(a, b) : Nat}

def sub_add_l source · line 734 · raw

@+a:Nat -> @+x:Nat -> {Nat.sub(Nat.add(a, x), x) == a : Nat}

def half_le source · line 737 · raw

@+n:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n), n) == True{} : Bool}

def fit54 source · line 747 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(54n, q) == True{} : Bool}

q < 2^53 + 1 fits 54 bits

def hpick_c source · line 754 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == f : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(52n, q) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, f, 1n, 2n) : Nat}

the high part of a normal q <= 2^53 is the spec's 1 or 2

def qsplit source · line 763 · raw

@+q:Nat -> @+EF:Nat -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(52n, q), EF))) == Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF)) : Nat}

def qfit source · line 767 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+EF:Nat -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF))) == True{} : Bool}

a normal q with its exponent field below 2047 fits the 63-bit pattern

def ef11 source · line 775 · raw

@+EF:Nat -> @+c:Nat -> @+hov:{Nat.is_lt(Nat.add(EF, c), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, EF) == True{} : Bool}

def rpfE source · line 780 · raw

@+s:Bool -> @+E:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> @+hE:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, E) == True{} : Bool} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n)) == False{} : Bool} -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, E))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_fin(s, E, w) == bits(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, E))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rpf0 source · line 792 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0n))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_fin(s, 0n, w) == bits(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def esub63 source · line 805 · raw

@+x:Nat -> {Nat.sub(Nat.add(x, 63n), 53n) == Nat.add(10n, x) : Nat}

def sr source · line 808 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, m) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, m, x, Nat.max(Nat.add(10n, x), 1926n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def lt_sub_pos source · line 814 · raw

@+x:Nat -> @+n:Nat -> @+h:{Nat.is_lt(x, n) == True{} : Bool} -> {Nat.is_le(1n, Nat.sub(n, x)) == True{} : Bool}

def sub_add_a source · line 825 · raw

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

def le_cancel_r source · line 828 · raw

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

def jfit source · line 831 · raw

@+d:Nat -> @+m:Nat -> @+hd:{Nat.is_le(1n, d) == True{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, m))) == True{} : Bool}

def rp_sub source · line 841 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hb:{Nat.is_lt(x, 1916n) == True{} : Bool} -> @+u:Nat -> @+hu:{Nat.max(Nat.add(10n, x), 1926n) == u : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_neg(s, e, sig, True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x, u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ov_eq source · line 867 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+hge:{Nat.is_le(1916n, x) == True{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {Bool.or(Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 2045n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 2147483648}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(sig, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{512, 0})))) == Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 10n)), 1n, 2n)), 2047n)) : Bool}

def rp_nc source · line 879 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+u:Nat -> @+hEF:{Nat.add(Nat.sub(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1926n) == u : Nat} -> @+o:Bool -> @+ho:{Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 10n)), 1n, 2n)), 2047n)) == o : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_over(s, e, sig, o) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 10n), u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rp_norm source · line 893 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hb:{Nat.is_lt(x, 1916n) == False{} : Bool} -> @+u:Nat -> @+hu:{Nat.max(Nat.add(10n, x), 1926n) == u : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_neg(s, e, sig, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x, u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rp_c2 source · line 910 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(x, 1916n) == b : Bool} -> @+u:Nat -> @+hu:{Nat.max(Nat.add(10n, x), 1926n) == u : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp_neg(s, e, sig, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x, u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def round_pack source · line 919 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(s, e, sig) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

SoftFloat's roundPackToF64(s, e, sig), sig with its top bit at 62 and e the biased exponent minus one plus OFF, is Flocq's round_NE of s * sig * 2^(e - 2180 - Z)