~/bend-docscommunity

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

raw source on the hub · import bend-collections-laws-math@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> -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8.all_bytes(bs) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.bytes_ok(bs) : Bool}

def seeded_ok source · line 20 · raw

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

def seeded_c source · line 156 · raw

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

def seeded source · line 164 · raw

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

THEOREM (ChaCha8.seeded)