~/bend-docscommunity

proofs/math/typed/f64light.bend checks

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

20 imports
import Base
import ./f64round.bend as FR
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/word.bend as WD
import ../../../src/math/natural.bend as M
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./natcmp.bend as NC
import ./width.bend as WW
import ./w64sh.bend as SH
import ./f64bits.bend as FB
import ./f64rtools.bend as RT
import ./u32laws.bend as LW

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def fval_g source · line 29 · raw

@+xl:U32 -> @+xh:U32 -> @+m:U32 -> @+hm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{xl, U32.and(xh, m)}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def hea source · line 32 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def hfr source · line 35 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def non source · line 38 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(x, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def nfit_mono_c source · line 45 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, x) == False{} : Bool} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, x) == c : Bool} -> {c == False{} : Bool}

def nfit_mono source · line 52 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, x) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, x) == False{} : Bool}

def dm2 source · line 55 · raw

@+l:Bool -> @+r:Bool -> {Bool.or(Bool.not(r), Bool.not(l)) == Bool.not(Bool.and(l, r)) : Bool}

def add_lt2 source · line 66 · raw

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

def add_eq0 source · line 71 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}

def shl_v source · line 78 · 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 orv_c source · line 83 · raw

@+l:U32 -> @+h:U32 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b)) : Nat}

def orv source · line 95 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(b)) : Nat}

def minz source · line 100 · raw

@+r:Nat -> {Nat.min(r, 0n) == 0n : Nat}

def jmin source · line 107 · raw

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

def nlb source · line 114 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(1n+k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == c : Bool} -> {c == True{} : Bool}

def nfit_bl source · line 122 · raw

@+k:Nat -> @+m:Nat -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, m) == False{} : Bool} -> {Nat.is_le(1n+k, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == True{} : Bool}

def hF source · line 126 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == True{} : Bool}

the fraction field has 52 bits (from f64addf, so light roots need not import it)

def nz_le source · line 129 · raw

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

def vb64 source · line 137 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == True{} : Bool}

every U64 value fits 64 bits (u64laws.vb, without u64laws' imports)

def true_ne_false source · line 142 · raw

@+h:{True{} == False{} : Bool} -> Empty