~/bend-docscommunity

proofs/math/typed/f64norm.bend checks

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

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 ../../lib/u32half.bend as UH
import ../../lib/word.bend as WD
import ../natural/bits.bend as BT
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./w64clz.bend as CLZ
import ./f64bits.bend as FB
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64bl.bend as BL
import ./f64cmp.bend as FC

Definitions

def v source · line 29 · raw

@+x:U32 -> Nat

def sa source · line 32 · raw

@+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

def hid source · line 40 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa)) == True{} : Bool} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(fa, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c})) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)) : Nat}

the hidden bit: f + 2^52 for a fraction below 2^52

def clz_t source · line 49 · raw

@+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hb:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(Fr), 52n) == True{} : Bool} -> {Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(fa), 11n) == Nat.sub(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(Fr)) : Nat}

def sub_fit source · line 56 · raw

@+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hz:{Nat.is_eq(Fr, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(fa), 11n), Fr)) == True{} : Bool}

def sub_nfit source · line 66 · raw

@+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hz:{Nat.is_eq(Fr, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(fa), 11n), Fr)) == False{} : Bool}

def sub_val source · line 81 · raw

@+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fr:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hz:{Nat.is_eq(Fr, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fa, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(fa), 11n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(fa), 11n), Fr) : Nat}

def sub_sum source · line 88 · raw

@+A:Nat -> @+t:Nat -> @+B:Nat -> @+hB:{Nat.is_le(B, t) == True{} : Bool} -> @+hA:{Nat.is_le(t, A) == True{} : Bool} -> {Nat.add(Nat.sub(A, t), Nat.sub(t, B)) == Nat.sub(A, B) : Nat}

def ez0 source · line 96 · raw

@+E:Nat -> @+hea:{0n == E : Nat} -> {Nat.is_eq(E, 0n) == True{} : Bool}

def ezs source · line 99 · raw

@+p:Nat -> @+E:Nat -> @+hea:{1n+p == E : Nat} -> {Nat.is_eq(E, 0n) == False{} : Bool}

def n1 source · line 103 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+E:Nat -> @+Fr:Nat -> @+hea:{ea == E : Nat} -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hnz:{Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sa(ea, fa), Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(E, 0n)))))) : Nat}

the normalized significand

def n2 source · line 118 · raw

@+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+E:Nat -> @+Fr:Nat -> @+hea:{ea == E : Nat} -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hnz:{Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), sa(ea, fa)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n)), 2171n) : Nat}

the exponent: norm_e + sa = xexp + 2171

def n3a source · line 140 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+E:Nat -> @+Fr:Nat -> @+hea:{ea == E : Nat} -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hnz:{Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa))) == True{} : Bool}

the normalized significand has its top bit at 52

def n3b source · line 151 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+E:Nat -> @+Fr:Nat -> @+hea:{ea == E : Nat} -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fa) == Fr : Nat} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+hnz:{Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa))) == False{} : Bool}