~/bend-docscommunity

proofs/math/typed/f64rint.bend checks

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

18 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/word.bend as WD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64bits.bend as FB
import ./f64light.bend as FL
import ./f64round.bend as FR
import ./f64tools.bend as T

Definitions

def upn source · line 32 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+q:Nat -> @+r:Nat -> @+h:Nat -> Bool

def up_v source · line 43 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_up(m, s, q, r, h) == upn(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h)) : Bool}

def b64v source · line 62 · raw

@+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.b64(b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b) : Nat}

def b2n63 source · line 69 · raw

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

def addb source · line 76 · raw

@+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Bool -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.b64(b))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b)) : Nat}

def G source · line 84 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+a:Nat -> @+b:Nat -> @+c:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def riq source · line 87 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_q(m, s, q, r, h) == G(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def g3 source · line 95 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+a:Nat -> @+a2:Nat -> @+ha:{a == a2 : Nat} -> @+b:Nat -> @+b2:Nat -> @+hb:{b == b2 : Nat} -> @+c:Nat -> @+c2:Nat -> @+hc:{c == c2 : Nat} -> {G(m, s, a, b, c) == G(m, s, a2, b2, c2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def integ source · line 102 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+n:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.integral(m, s, n, 1n+j), 3000n) == G(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+j, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(1n+j, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 1n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the spec's integral at k = 1 + j, in the same shape

def le64 source · line 115 · raw

@+j:Nat -> {Nat.is_le(64n, Nat.add(1n+j, 63n)) == True{} : Bool}

def hfit source · line 118 · raw

@+j:Nat -> @+V:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, V) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+j, V)) == True{} : Bool}

def half_v source · line 123 · raw

@+j:Nat -> @+hb:{Nat.is_lt(1n+j, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0}, Nat.sub(1n+j, 1n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 1n) : Nat}

2^(k-1) as a word

def small_case source · line 130 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+j:Nat -> @+hb:{Nat.is_lt(1n+j, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_k(m, s, w, 1n+j, True{}) == G(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(1n+j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 1n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def c63 source · line 166 · raw

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

def nlt source · line 170 · raw

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

V < 2^k is not above 2^k

def upn_big source · line 174 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+V:Nat -> @+a:Nat -> @+b:Nat -> @+la:{Nat.is_lt(a, V) == False{} : Bool} -> @+lb:{Nat.is_lt(b, V) == False{} : Bool} -> {upn(m, s, 0n, V, a) == upn(m, s, 0n, V, b) : Bool}

def large_case source · line 187 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+j:Nat -> @+hb:{Nat.is_le(64n, 1n+j) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_q(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0}, w, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.integral(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 1n+j), 3000n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rik_c source · line 205 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+j:Nat -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(1n+j, 64n) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_k(m, s, w, 1n+j, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.integral(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 1n+j), 3000n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rik source · line 213 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hk:{Nat.is_le(1n, k) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_k(m, s, w, k, Nat.is_lt(k, 64n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.integral(m, s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), k), 3000n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def RI source · line 222 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def ti_fin source · line 225 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> @+hc:{Nat.is_le(3000n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_fin(m, x, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, c, x, RI(m, x)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ti_c source · line 242 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+t:Bool -> @+z:Bool -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ri_cls(m, x, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(t, Bool.not(z)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.and(t, z), Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x))), x, RI(m, x))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ti_value source · line 253 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.to_integral(m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.to_integral(m, x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def trunc_value source · line 257 · raw

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

def floor_value source · line 260 · raw

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

def ceil_value source · line 263 · raw

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

def round_value source · line 266 · raw

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