proofs/math/typed/f64nrp.bend checks

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

21 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 ../../../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/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./w64clz.bend as CLZ
import ./natcmp.bend as NC
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64bl.bend as BL

Definitions

def shl_v source · line 27 · 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 rq source · line 33 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+q:Nat -> @+xq:Nat -> @+h53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == True{} : Bool} -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> @+hx:{Nat.is_le(1926n, xq) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(Nat.sub(xq, 1926n), 1n), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, q, xq) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, Nat.sub(xq, 1926n)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

a 53-bit q at ulp x' >= 1926 rounds to itself

def tbf source · line 51 · raw

@+k:Nat -> @+V:Nat -> @+J:Nat -> @+ek:{Nat.add(k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(V)) == J : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(J, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, V)) == True{} : Bool}

the top bits of shift(k, V) when k + bit_length(V) = J

def tbn source · line 54 · raw

@+k:Nat -> @+V:Nat -> @+K:Nat -> @+hz:{Nat.is_eq(V, 0n) == False{} : Bool} -> @+ek:{Nat.add(k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(V)) == 1n+K : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(K, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, V)) == False{} : Bool}

def esd source · line 62 · raw

@+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n) == Nat.sub(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig))) : Nat}

def sdb source · line 67 · raw

@+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {Nat.add(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig))) == 63n : Nat}

def sd_le source · line 71 · raw

@+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> {Nat.is_le(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n), 63n) == True{} : Bool}

def nrp_r source · line 75 · 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} -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 0n) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hx63:{Nat.is_le(63n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(s, Nat.sub(e, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(sig, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the rounding branch

def and_l source · line 92 · raw

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

def and_r source · line 99 · raw

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

def nrp_d source · line 107 · 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} -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 0n) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hx63:{Nat.is_le(63n, x) == True{} : Bool} -> @+h10:{Nat.is_le(10n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)) == True{} : Bool} -> @+hoff:{Nat.is_le(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), e) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.sub(e, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 2045n)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.pack(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nrp_exp(e, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(sig)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(sig, Nat.sub(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n), 10n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the exact branch: at most 53 bits, landing in the normal range

def nrp_c source · line 147 · 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} -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 0n) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hx63:{Nat.is_le(63n, x) == True{} : Bool} -> @+d:Bool -> @+hd:{Bool.and(Nat.is_le(10n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 2045n)))) == d : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nrp_pick(s, e, sig, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(sig), 1n), d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def nrp source · line 157 · 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} -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig), 0n) == False{} : Bool} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig)) == True{} : Bool} -> @+hx63:{Nat.is_le(63n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_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 normRoundPackToF64 is round