~/bend-docscommunity

proofs/math/random/float.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float

21 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/random.bend as SR
import ../../../src/math/random/rand.bend as R
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/f64.bend as F
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ../natural/bits.bend as NB
import ../typed/width.bend as WW
import ../typed/u32laws.bend as LW
import ../typed/w64sh.bend as SH
import ../typed/w64clz.bend as WC
import ../typed/w64add.bend as WA
import ../typed/f64bits.bend as FB
import ./fround.bend as FR

Definitions

def v source · line 32 · raw

@+x:U32 -> Nat

def sub63 source · line 38 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.sub(63n, j) == Nat.add(11n, Nat.sub(52n, j)) : Nat}

63 - j = 11 + (52 - j)

def shift_amt source · line 46 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.sub(Nat.sub(63n, j), 11n) == Nat.sub(52n, j) : Nat}

the shift of the implementation: clz - 11 = 52 - j

def exp_amt0 source · line 51 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(970n, j) : Nat}

the exponent field of the implementation: 1033 - clz = 970 + j

def exp_amt source · line 59 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(j, 970n) : Nat}

def fits0 source · line 64 · raw

@+a:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, 0n) == True{} : Bool}

def fits_up source · line 68 · raw

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

def fits_shift source · line 75 · raw

@+a:Nat -> @+k:Nat -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(a, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, x)) == True{} : Bool}

x < 2^k gives x 2^a < 2^(a + k)

def fits_lt11 source · line 78 · raw

@+e:Nat -> @+h:{Nat.is_lt(e, 2048n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, e) == True{} : Bool}

def hw source · line 85 · raw

@+e:Nat -> @+qh:U32 -> U32

the high word the implementation builds: exponent field e, and the top 20 fraction bits of qh

def bits source · line 88 · raw

@+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def f12 source · line 91 · raw

@+e:Nat -> @+he:{Nat.is_lt(e, 2048n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(12n, e) == True{} : Bool}

def hw_value source · line 95 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+e:Nat -> @+qh:U32 -> @+he:{Nat.is_lt(e, 2048n) == True{} : Bool} -> {v(hw(e, qh)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(20n, v(qh)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, e)) : Nat}

its value: 2^20 e + (qh mod 2^20), for e < 2^11

def value_eta source · line 111 · raw

@+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q) == Nat.add(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(q)))) : Nat}

def enc source · line 118 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+Q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:Nat -> @+he:{Nat.is_lt(e, 2048n) == True{} : Bool} -> @+q:Nat -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(Q) == q : Nat} -> @+f53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == True{} : Bool} -> {bits(Q, e) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(False{}, e, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the implementation's bits are encode(False, e, q mod 2^52) for the value q < 2^53 of the shifted significand

def bl_le source · line 144 · raw

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

def x0 source · line 163 · raw

Nat

def max_l source · line 166 · raw

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

def sub_add53 source · line 177 · raw

@+X:Nat -> {Nat.sub(Nat.add(X, 53n), 53n) == X : Nat}

def ex source · line 182 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.add(Nat.add(j, 2895n), Nat.sub(52n, j)) == x0 : Nat}

X + r = 2947 for X = j + 2895, r = 52 - j

def round_q source · line 194 · raw

@+q:Nat -> @+j:Nat -> @+bq:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(q) == 53n : Nat} -> @+hz:{Nat.is_eq(q, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, q, Nat.add(j, 2895n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(False{}, q, Nat.add(j, 2895n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round(q, X) for 2^52 <= q < 2^53 at the scale X = j + 2895 is pack(q, X)

def pack_q source · line 209 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> @+f53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == True{} : Bool} -> @+n52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(False{}, q, Nat.add(j, 2895n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(False{}, Nat.add(j, 970n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

pack(q, X) is the pattern with exponent field j + 970 and fraction q mod 2^52

def J source · line 240 · raw

@+np:Nat -> Nat

the bit length of 1 + np is 1 + J(np)

def j52 source · line 243 · raw

@+np:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+np) == True{} : Bool} -> {Nat.is_le(J(np), 52n) == True{} : Bool}

def r52 source · line 246 · raw

@+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> {Nat.is_lt(Nat.sub(52n, j), 64n) == True{} : Bool}

def impl_eq source · line 254 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+np : Nat} -> @+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> @+hbl:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 1n+j : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.f53(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(m)) == bits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the implementation: shift by 52 - j, exponent field j + 970, for the bit length 1 + j of the significand (j a variable, so no bit length is ever evaluated inside a comparison)

def hj_of source · line 268 · raw

@+np:Nat -> @+j:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+np) == True{} : Bool} -> @+hbl:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 1n+j : Nat} -> {Nat.is_le(j, 52n) == True{} : Bool}

j <= 52 from the bit length 1 + j <= 53

def main_g source · line 271 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+np : Nat} -> @+j:Nat -> @+hj:{Nat.is_le(j, 52n) == True{} : Bool} -> @+hbl:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 1n+j : Nat} -> {bits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 1n+np, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def main_j source · line 295 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+np : Nat} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+np) == True{} : Bool} -> @+j:Nat -> @+hbl:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 1n+j : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.f53(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 1n+np, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bl_nz source · line 301 · raw

@+np:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == 0n : Nat} -> Empty

def main_b source · line 304 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+np : Nat} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+np) == True{} : Bool} -> @+b:Nat -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(1n+np) == b : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.f53(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 1n+np, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def main_v source · line 311 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+np : Nat} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+np) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.f53(m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 1n+np, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def mm source · line 317 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

the low 53 bits of the source output

def m_val source · line 320 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) : Nat}

def iz source · line 333 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+vm:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == vm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(m) == Nat.is_eq(vm, 0n) : Bool}

def hl_of source · line 336 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+vm:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == vm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == vm : Nat}

def round0 source · line 339 · raw

@+xv:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0n, xv) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(False{}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def value_z source · line 342 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == n : Nat} -> @+xv:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == 0n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def value_s source · line 348 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == n : Nat} -> @+np:Nat -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == 1n+np : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def value_c source · line 356 · raw

@+vm:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == vm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, n, xv) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def value source · line 364 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)) == n : Nat} -> @+xv:Nat -> @+hx:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 53n) == xv : Nat} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Float64.value(x, n, hn, xv, hx)

THEOREM (Float64.value)

def and_f source · line 373 · raw

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

def hv_one source · line 382 · raw

@+H:U32 -> @+K:U32 -> @+k:Nat -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(12n, k) == True{} : Bool} -> @+hH:{U32.and(H, 2147483647) == U32.mul(K, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(20n)) : U32} -> @+hK:{U32.to_nat(K) == k : Nat} -> {v(U32.and(H, 2147483647)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, k) : Nat}

the value of the high word of 1.0 without its sign bit: k * 2^20 (k = 1023, kept a variable so no 30-bit constant is ever expanded)

def below_one source · line 393 · raw

@+l:U32 -> @+qh:U32 -> @+E:Nat -> @+H:U32 -> @+K:U32 -> @+k:Nat -> @+hE:{Nat.is_lt(E, k) == True{} : Bool} -> @+hk:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(11n, k) == True{} : Bool} -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, H}) == False{} : Bool} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, H}) == False{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, H}) == False{} : Bool} -> @+hH:{U32.and(H, 2147483647) == U32.mul(K, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(20n)) : U32} -> @+hK:{U32.to_nat(K) == k : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, hw(E, qh)}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{0, H}) == True{} : Bool}

a double Bits{l, hw(E, qh)} with E < k <= 2047 is below Bits{0, H} whose high word (without sign) is k * 2^20

def lt_z_case source · line 437 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == 0n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.one) == True{} : Bool}

def lt_s_case source · line 441 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+np:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == 1n+np : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.one) == True{} : Bool}

def lt_c source · line 451 · raw

@+vm:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mm(x)) == vm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.to_float(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.one) == True{} : Bool}

def lt_one source · line 459 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Float64.lt_one(x)

THEOREM (Float64.lt_one)