spec/math/random.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as Random

15 imports

import Base
import ../lib/common.bend as C
import ../../src/math/u64.bend as W
import ../../src/math/w64.bend as X
import ../../src/math/f64.bend as F
import ../../src/math/random/rand.bend as R
import ../../src/math/random/chacha8.bend as C8
import ../../src/math/random/chacha8/block.bend as B
import ../../src/math/random/pcg.bend as P
import ./w64.bend as SW
import ./f64.bend as SF
import ./random/source.bend as SRC
import ./random/chacha8rand.bend as SC
import ./random/pcg.bend as SP
import ./random/rand.bend as SR

Definitions

def map_outputs source · line 63 · raw

@+n:Nat -> @m:Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8.ChaCha8> -> Maybe<&2, List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>>

def map_stream source · line 70 · raw

@+n:Nat -> @m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>>

def ChaCha8.stream source · line 77 · raw

@+n:Nat -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Key -> Type

def ChaCha8.seeded source · line 80 · raw

@+n:Nat -> @+seed:List<&2, U32> -> Type

def value128 source · line 83 · raw

@p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.PCG -> Nat

def PCG.step source · line 88 · raw

@+mh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ml:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ih:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+il:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.PCG -> Type

def PCG.output source · line 94 · raw

@+cm:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+ht:{t == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.dxsm1(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(cm), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(hi)) : Nat} -> Type

stated through the intermediate value t of the first half (so the checker never compares two copies of the nested 64-bit recursion); t = dxsm1(cm, hi) gives output == dxsm(cm, hi, lo)

def PCG.constants source · line 97 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.PCG -> Type

def val_pair source · line 100 · raw

@-S:Data -> @r:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> Pair(Nat, S)

def Lemire.unbiased source · line 110 · raw

@+w:Nat -> @+n:Nat -> @+k:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w, n) == True{} : Bool} -> @+hk:{Nat.is_lt(k, n) == True{} : Bool} -> Type

def Float64.value source · line 122 · 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} -> Type

the exact double m * 2^-53 for m = the low 53 bits of x (m and the exponent zb - 53 given as variables n, xv with their equations, so the checker never compares two expansions of the rounding)

def Float64.lt_one source · line 125 · raw

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

Templates

template Uint64n.value source · line 104 · raw

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

template Uint64n.lt source · line 107 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> Type

template Shuffle.permutation source · line 113 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+xs:List<&2, A> -> @+v:V -> Type

template Perm.permutation source · line 116 · raw

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

template x0 source · line 131 · raw

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

template Uint32.value source · line 134 · raw

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

template Int64.value source · line 137 · raw

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

template Int32.value source · line 140 · raw

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

template Uint32n.lt source · line 143 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:U32 -> @+hn:{U32.is_zero(n) == False{} : Bool} -> Type

template Intn.lt source · line 146 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool} -> Type

template IntRange.bounds source · line 149 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(lo, hi) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.sub(hi, lo)) == True{} : Bool} -> Type