proofs/math/random/proof.bend checks

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

9 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../src/math/u64.bend as W
import ../../../src/math/random/chacha8/block.bend as B
import ../../../spec/math/random.bend as SRM
import ./chacha8/stream.bend as CS
import ./chacha8/seed.bend as SEED
import ./lemire.bend as LE
import ./shuffle.bend as SH

Definitions

def ChaCha8.stream source · line 20 · raw

@+n:Nat -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Key -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.ChaCha8.stream(n, k)

def ChaCha8.seeded source · line 23 · raw

@+n:Nat -> @+seed:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.ChaCha8.seeded(n, seed)

def Lemire.unbiased source · line 26 · 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} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Lemire.unbiased(w, n, k, hn, hw, hk)

Templates

template Shuffle.permutation source · line 29 · 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 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Shuffle.permutation(A, V, rel, S, next, s, xs, v)

template Perm.permutation source · line 32 · raw

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