~/bend-docscommunity

proofs/math/random/uint64n.bend checks

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

20 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../spec/math/random/rand.bend as SR
import ../../../spec/math/random/source.bend as SRC
import ../../../src/math/u64.bend as WU
import ../../../src/math/w64.bend as X
import ../../../src/math/random/rand.bend as R
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as LA
import ../typed/width.bend as WI
import ../typed/w64add.bend as WA
import ../typed/w64m128.bend as M128
import ../typed/w64dmrem.bend as DMR
import ../natural/arith.bend as AR
import ./bits.bend as BI
import ./lemire.bend as LE
import ../../../spec/math/random.bend as SRM
import ../../lib/u32alg.bend as UA

Definitions

def Z source · line 26 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def one64 source · line 29 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def q_one source · line 34 · raw

@+q:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:Bool -> @+hc:{Nat.is_eq(q, 0n) == c : Bool} -> @+hq0:{c == False{} : Bool} -> @+hq1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, q) == True{} : Bool} -> {q == one : Nat}

def add_eq0_r source · line 43 · raw

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

def q_nz_c source · line 50 · raw

@+q:Nat -> @+s:Nat -> @+vn:Nat -> @+hn:{Nat.is_eq(vn, 0n) == False{} : Bool} -> @+e:{Nat.add(s, vn) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, q) : Nat} -> @+c:Bool -> @+hc:{Nat.is_eq(q, 0n) == c : Bool} -> {c == False{} : Bool}

def q_nz source · line 60 · raw

@+q:Nat -> @+s:Nat -> @+vn:Nat -> @+hn:{Nat.is_eq(vn, 0n) == False{} : Bool} -> @+e:{Nat.add(s, vn) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, q) : Nat} -> {Nat.is_eq(q, 0n) == False{} : Bool}

def neg_sum source · line 64 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hn:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), 0n) == False{} : Bool} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(Z, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat}

a nonzero word and its negation add up to 2^64

def pm_one source · line 76 · raw

@+w:Nat -> @+m:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(w, 1n+m) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, one), 1n+m) : Nat}

pow2mod through a symbolic one (2^64 is never a closed term)

def thresh_m source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.thresh(n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat}

def pred_value source · line 95 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(n, one64)) == m : Nat}

n - 1 for a nonzero n

def pow2_value source · line 102 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.is_pow2(n) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) : Bool}

the power-of-two test is n & (n - 1) == 0

def mask_value source · line 111 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.and64(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(n, one64))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), m) : Nat}

the mask is x & (n - 1)

def m128_lo source · line 117 · raw

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

the halves of the 128-bit product

def m128_hi source · line 125 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n))) : Nat}

def dec source · line 151 · raw

@+x:Nat -> @+m:Nat -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(x, 1n+m)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.draw(64n, x, 1n+m) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.accept(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, Nat.mul(x, 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}

Lemire's decision of the specification: accept unless lo < 2^64 mod n

def pm_lt source · line 164 · raw

@+m:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}

def lt_low source · line 170 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), t) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+m)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m)) : Bool}

the implementation's rejection test is the specification's

def hi_value source · line 178 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+m)) : Nat}

def hd_of source · line 182 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), t) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.draw(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+m) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.accept(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}

def lt_low_n source · line 220 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), n) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+m)), 1n+m) : Bool}

def mask_pair source · line 249 · raw

@-S:Data -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.mask(S, n, p)) == (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, p)), m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, p)) : Pair(Nat, S)}

def all1 source · line 254 · raw

@n:Nat -> Word(n)

def and_true source · line 261 · raw

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

def and_all1 source · line 268 · raw

@+n:Nat -> @+w:Word(n) -> {Word.and(n, w, all1(n)) == w : Word(n)}

def uand_all source · line 276 · raw

@+y:U32 -> @+M:U32 -> @+hM:{M == U32{all1(32n)} : U32} -> {U32.and(y, M) == y : U32}

def zero_pair source · line 283 · raw

@-S:Data -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.mask(S, Z, p)) == (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, p)) : Pair(Nat, S)}

n == 0 is read as 2^64: the whole word

def zero_word source · line 312 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == True{} : Bool} -> {n == Z : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64}

Templates

template cont source · line 136 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @f:Nat -> @+n:Nat -> @+x:Nat -> @+s:S -> Pair(Nat, S)

the specification's bounded draw after a draw of x with state s

template below_cont source · line 139 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+f:Nat -> @+n:Nat -> @+s:S -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.below(S, next, f, n, s) == cont(S, next, f, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, next(s))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, next(s))) : Pair(Nat, S)}

template fixpoint source · line 142 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+f:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:S -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(lo, t) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, f, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.D{hi, lo, s}) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.D{hi, lo, s} : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.Draw<S>}

template last_acc source · line 156 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+h:Nat -> @+ok:Bool -> @+x:Nat -> @+n:Nat -> @+s:S -> @+hh:{h == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, Nat.mul(x, n)) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.below_go(S, next, 0n, n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.accept(h, ok), x, s) == (h, s) : Pair(Nat, S)}

template step_false source · line 186 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+g:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:S -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), t) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, g, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.again(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), s1, False{})))) == cont(S, next, 1n+g, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), s1) : Pair(Nat, S)}

one retry step, accepted

template step_true source · line 195 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+g:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:S -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), t) == True{} : Bool} -> @+rec:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, g, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.draw(S, n, next(s1))))) == cont(S, next, g, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, next(s1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, next(s1))) : Pair(Nat, S)} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, g, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.again(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), s1, True{})))) == cont(S, next, 1n+g, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), s1) : Pair(Nat, S)}

one retry step, rejected: the next draw

template step_case source · line 200 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+g:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:S -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), t) == c : Bool} -> @+rec:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, g, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.draw(S, n, next(s1))))) == cont(S, next, g, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, next(s1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, next(s1))) : Pair(Nat, S)} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, g, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.again(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), s1, c)))) == cont(S, next, 1n+g, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), s1) : Pair(Nat, S)}

template loop source · line 209 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+f:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.result(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.retry(S, next, f, n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.draw(S, n, p)))) == cont(S, next, f, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, p)) : Pair(Nat, S)}

THEOREM (the rejection loop): f retries from the draw p follow the specification's draws

template first_false source · line 228 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:S -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.lemire_small(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), s1, False{})) == cont(S, next, 127n, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), s1) : Pair(Nat, S)}

lo >= n: the first draw is accepted by the specification too

template first_case source · line 240 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:S -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> @+htn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.lemire_small(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(x, n)), s1, c)) == cont(S, next, 127n, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), s1) : Pair(Nat, S)}

the first draw: accepted at once when lo >= n, else the loop

template top_first source · line 294 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> @+hp:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.lemire_first(S, next, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.draw(S, n, p))) == cont(S, next, 127n, 1n+m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.fst64(S, p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/source.snd64(S, p)) : Pair(Nat, S)}

template value_nz source · line 299 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == 1n+m : Nat} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 1n+m, m), 0n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.uint64n_pick(S, next, s, n, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.below(S, next, 127n, 1n+m, s) : Pair(Nat, S)}

template value_vn source · line 321 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+vn:Nat -> @+hv:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n) == vn : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.uint64n(S, next, s, n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.below(S, next, 127n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(n), s) : Pair(Nat, S)}

template uint64n_value source · line 334 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Uint64n.value(S, next, s, n)

THEOREM (Uint64n.value)