spec/crypto/random.bend checks

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

12 imports

import Base
import ../../src/math/u64.bend as W
import ../../src/math/w64.bend as X
import ../../src/math/random/chacha8.bend as C8
import ../../src/math/random/chacha8/block.bend as B
import ../../src/math/random/rand.bend as R
import ../../src/crypto/random.bend as CR
import ../math/w64.bend as SW
import ../math/random/source.bend as SRC
import ../math/random/chacha8rand.bend as SC
import ../math/random/rand.bend as SR
import ../math/random.bend as SRM

Definitions

def byte_of source · line 34 · raw

@+w:U32 -> @+k:Nat -> U32

Go's byte(v >> k)

def le_bytes source · line 38 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> List<&2, U32>

Go's binary.LittleEndian.PutUint64

def append source · line 43 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

def flat source · line 51 · raw

@xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64> -> List<&2, U32>

the bytes of consecutive outputs

def take source · line 58 · raw

@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>

def below256 source · line 67 · raw

@xs:List<&2, U32> -> Bool

def fst_bytes source · line 74 · raw

@-G:Data -> @r:Pair(List<&2, U32>, G) -> List<&2, U32>

def map_outputs source · line 78 · raw

@+n:Nat -> @m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen> -> Maybe<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>>

def Random.stream source · line 85 · raw

@+n:Nat -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> Type

def Random.seeded source · line 88 · raw

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

def Random.bytes source · line 91 · raw

@+n:Nat -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8 -> @+p:List<&2, U32> -> Type

def Random.bytes_lt source · line 94 · raw

@+n:Nat -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8 -> @+p:List<&2, U32> -> @+hp:{below256(p) == True{} : Bool} -> Type

def Random.uint_below source · line 97 · raw

@+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen -> @+n:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+hn:{0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.is_zero(n) == False{} : Bool} -> Type

Templates

template Random.shuffle source · line 100 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen -> @+items:List<&2, A> -> @+v:V -> Type