~/bend-docscommunity

proofs/crypto/random/proof.bend checks

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

15 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/crypto/random.bend as CR
import ../../../spec/math/random/source.bend as SRC
import ../../../spec/math/random/chacha8rand.bend as SC
import ../../../spec/math/random.bend as SRM
import ../../../spec/crypto/random.bend as SCR
import ../../math/random/chacha8/stream.bend as CS
import ../../math/random/chacha8/seed.bend as SEED
import ../../math/random/bounded.bend as BD
import ../../math/random/shuffle.bend as SH
import ./bytes.bend as BY

Definitions

def kp_fst source · line 22 · raw

@+p:List<&2, U32> -> @q:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.fst64(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.keep_pending(p, q)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.fst64(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, q) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

def kp_snd source · line 27 · raw

@+p:List<&2, U32> -> @q:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.snd64(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.keep_pending(p, q)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.G{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.snd64(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, q), p} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen}

def gen_outputs source · line 33 · raw

@+n:Nat -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8 -> @+p:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.outputs(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.next, n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.G{c, p}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.outputs(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.next, n, c) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>}

the generator's outputs are its ChaCha8's; pending bytes are only for bytes

def Random.stream source · line 42 · raw

@+n:Nat -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.Random.stream(n, k0, k1, k2, k3, k4, k5, k6, k7)

def wrap_map source · line 48 · raw

@+n:Nat -> @m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.map_outputs(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.wrap(m)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.map_outputs(n, m) : Maybe<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>>}

def Random.seeded source · line 55 · raw

@+n:Nat -> @+seed:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.Random.seeded(n, seed)

def Random.bytes source · line 60 · raw

@+n:Nat -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8 -> @+p:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.Random.bytes(n, c, p)

def Random.bytes_lt source · line 63 · raw

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

def Random.uint_below source · line 66 · raw

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

Templates

template Random.shuffle source · line 69 · raw

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