~/bend-docscommunity

proofs/math/typed/f64conv.bend checks

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

25 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/num.bend as NE
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 ./w64clz.bend as CZ
import ./u32laws.bend as LW
import ./f64bits.bend as FB
import ./f64light.bend as FL
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64nrp.bend as NR
import ./f64bl.bend as BL
import ./f64tools.bend as T
import ./f64rint.bend as RI

Definitions

def v source · line 36 · raw

@+x:U32 -> Nat

def TN source · line 40 · raw

@+s:Bool -> @+n:Nat -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

the spec's verdict on a nonnegative-or-zero integer part n with sign s

def TS source · line 43 · raw

@+s:Bool -> @+n:Nat -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def tn source · line 46 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_neg(w, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>, b, Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Overflow{}}, Done{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)}) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def tuint_v source · line 53 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_int(s, w)) == TS(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def tn_fit source · line 58 · raw

@+s:Bool -> @+n:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool} -> {TS(s, n) == TN(s, n) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

TN is TS when n fits 64 bits

def le_k64 source · line 66 · raw

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

def small_nat source · line 69 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_int(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(w, k))) == TN(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def subsub source · line 79 · raw

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

def big_c source · line 83 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 0n) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(Nat.add(k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w))), 64n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_big(s, w, k, c)) == TN(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def big_nat source · line 113 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w), 0n) == False{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_big(s, w, k, Nat.is_le(Nat.add(k, Nat.sub(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(w))), 64n))) == TN(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def mz source · line 126 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0n) == b : Bool} -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0n) == Nat.is_eq(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(b)))), 0n) : Bool}

a double with scale at least Z is normal, so its significand is not zero the significand at an abstract exponent-is-zero bit b: instantiated at False, the hidden bit 2^52 is never evaluated

def bnz_c source · line 129 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+z:Bool -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(x), 0n) == z : Bool} -> @+h:{Nat.is_le(3000n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp_z(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(x), z)) == True{} : Bool} -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0n) == False{} : Bool}

def big_nz source · line 143 · raw

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

def hw53 source · line 146 · 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 IPc source · line 149 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> Nat

def tu_fin_c source · line 152 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> @+hc:{Nat.is_le(3000n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_fin(x, c)) == TN(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), IPc(x, c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def TNR source · line 175 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> @+n:Nat -> @+f:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def tu_c source · line 178 · raw

@+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/spec/math/f64.rv64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu_cls(x, t)) == TNR(Bool.and(t, Bool.not(z)), Bool.and(t, z), Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.int_part(x), 0n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.int_part(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.int_part(x))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def to_u64_value source · line 189 · raw

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

def f32r source · line 195 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def t32_c source · line 202 · raw

@+l:U32 -> @+h:U32 -> @+c:Bool -> @+hc:{U32.is_zero(h) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu32_w(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>, c, Done{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})}, Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Overflow{}}) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def t32w source · line 212 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu32_w(w, U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(w)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), Done{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)}, Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Overflow{}}) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def t32 source · line 220 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.tu32(r)) == f32r(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rv64(r)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def pn source · line 227 · raw

@+b:Bool -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>, b, Done{n}, Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Overflow{}}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>, Bool.not(b), Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Overflow{}}, Done{n}) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def s32_c source · line 234 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> @+n:Nat -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == f : Bool} -> {f32r(TNR(a, b, c, n, f)) == TNR(a, b, c, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def to_u32_value source · line 248 · raw

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

def floor_u64_value source · line 258 · raw

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

def ceil_u64_value source · line 261 · raw

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

def round_u64_value source · line 264 · raw

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