~/bend-docscommunity

proofs/math/typed/f64ofnat.bend checks

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

17 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/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 ../natural/bits.bend as BT
import ../../lib/u32half.bend as UHX
import ./width.bend as WW
import ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64bl.bend as BL

Definitions

def hx source · line 25 · raw

@+bb:Nat -> {Nat.add(Nat.add(2937n, bb), 2180n) == Nat.add(5117n, bb) : Nat}

def jn source · line 28 · raw

@+dd:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.jam_nat(dd, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(dd, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(dd, n)) : Nat}

def on_le source · line 35 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> @+hc:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 63n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(False{}, Nat.add(5117n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.word64(n), Nat.sub(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

b <= 63: an exact shift

def on_gt source · line 61 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> @+hc:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 63n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(False{}, Nat.add(5117n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.word64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.jam_nat(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 63n), n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

b > 63: a sticky jam of n >> (b - 63)

def on_c source · line 88 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 63n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(False{}, Nat.add(5117n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sig63(n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ofz source · line 95 · raw

@+n:Nat -> @+z:Bool -> @+hz:{Nat.is_eq(n, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.of_nat_z(n, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def of_nat_value source · line 102 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.OfNat.value(n)