~/bend-docscommunity

proofs/math/random/chacha8/seed.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/seed.bend as Seed

8 imports
import Base
import ../../../../src/math/u64.bend as W
import ../../../../src/math/random/chacha8.bend as C8
import ../../../../src/math/random/chacha8/block.bend as B
import ../../../../spec/math/random/chacha8rand.bend as S
import ../../../../spec/math/random.bend as SRM
import ./stream.bend as CS
import ../../../../spec/math/random/source.bend as SRC

Definitions

def bytes_eq source · line 13 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.all_bytes(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.bytes_ok(bs) : Bool}

def seeded_ok source · line 20 · raw

@+n:Nat -> @+seed:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.map_outputs(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.lift(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.key_of(seed))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.map_stream(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.key_if(seed, Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.length(seed), 32n))) : Maybe<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>>}

def seeded_c source · line 156 · raw

@+n:Nat -> @+seed:List<&2, U32> -> @+b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.map_outputs(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.seed_ok(seed, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.map_stream(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.key_if(seed, Bool.and(b, Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.length(seed), 32n)))) : Maybe<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>>}

def seeded source · line 164 · raw

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

THEOREM (ChaCha8.seeded)