~/bend-docscommunity

proofs/math/typed/f64tools.bend checks

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

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 ../../../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 ./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 ./f64rtools.bend as RT
import ./f64norm.bend as NM
import ./f64nrp.bend as NR
import ./f64cmp.bend as FC
import ./natcmp.bend as NC
import ../../lib/word.bend as WD

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def dz source · line 36 · raw

@+E:Nat -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp_z(E, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, z, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n)) : Nat}

def dexp_value source · line 43 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x) : Nat}

def dmf source · line 49 · raw

@+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant_z(f, False{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(f, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 1048576})) : Nat}

def dm source · line 52 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(f) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant_z(f, z)) == Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(z)))) : Nat}

def dmant_value source · line 71 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x) : Nat}

def b2n_fits source · line 77 · raw

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

def mant_fits source · line 85 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x)) == True{} : Bool}

the significand has at most 53 bits

def zero_eq source · line 92 · raw

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

def nz_mono source · line 99 · raw

@+h:Nat -> @+J:Nat -> @+hle:{Nat.is_le(h, J) == True{} : Bool} -> @+hz:{Nat.is_eq(h, 0n) == False{} : Bool} -> {Nat.is_eq(J, 0n) == False{} : Bool}

def le_jam source · line 108 · raw

@+h:Nat -> @+l:Nat -> {Nat.is_le(h, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l)) == True{} : Bool}

h <= jam(h, l)

def rw_hi source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hx:{Nat.is_le(63n, x) == True{} : Bool} -> @+hnf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rw_top(s, x, w, True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

top bit set: a sticky shift by one, then normRoundPack at the next scale

def top_eq source · line 138 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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}, w) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w))) : Bool}

the top value 2^63 of the test in rw_z (the word c = 2^31 kept abstract, so the checker never expands 2^31 in unary)

def rw_f source · line 148 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hx:{Nat.is_le(63n, x) == True{} : Bool} -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 0n) == False{} : Bool} -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == f : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rw_top(s, x, w, Bool.not(f)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rw_c source · line 155 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hx:{Nat.is_le(63n, x) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rw_z(s, x, w, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rw_value source · line 165 · raw

@+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hx:{Nat.is_le(63n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_w(s, x, w) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round_w is the spec's round

def ea source · line 171 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x) : Nat}

def fz source · line 176 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x), 0n) : Bool}

def dge_z source · line 182 · raw

@+e:Nat -> @+z:Bool -> {Nat.is_le(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp_z(e, z)) == True{} : Bool}

the scale of a finite double is at least 1926 (the subnormal scale)

def dexp_ge source · line 189 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_le(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)) == True{} : Bool}

def xexp_ge source · line 192 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_le(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) == True{} : Bool}

def zero_v source · line 195 · raw

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

def mw53 source · line 198 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x))) == True{} : Bool}

def subsub source · line 201 · raw

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

def bzc source · line 205 · raw

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

def and_comm source · line 212 · raw

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

def mant_z source · line 224 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) : Bool}

the significand is zero exactly for the zeros

def dmz source · line 231 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)), 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) : Bool}