~/bend-docscommunity

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

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

7 imports
import Base
import ../../../../src/math/u64.bend as W
import ../../../../src/math/random/chacha8/block.bend as B
import ../../../../src/math/random/chacha8.bend as C8
import ../../../../spec/math/random/chacha8rand.bend as S
import ../../../../spec/math/random/source.bend as SRC
import ./block.bend as PB

Definitions

def app source · line 14 · raw

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

def drop64 source · line 21 · raw

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

def rest source · line 31 · raw

@+kl:List<&2, U32> -> @p:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.Phase -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>

the outputs of the current iteration after the groups already produced

def nk source · line 43 · raw

@+kl:List<&2, U32> -> @p:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.Phase -> List<&2, U32>

the key of the iteration after them

def gw source · line 54 · raw

@+k:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8/block.Key -> @+c:U32 -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>

def inv source · line 59 · raw

@+n:Nat -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8/block.Key -> @+buf:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64> -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.Phase -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.outputs(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.next, n, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.C{k, p, buf}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.stream_go(n, app(buf, rest(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.key_list(k), p)), nk(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.key_list(k), p)) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>}

the invariant: from state C{k, p, buf} the generator outputs buf, the rest of the iteration keyed by k, then C2SP's stream from the next key

def stream source · line 84 · raw

@+n:Nat -> @+k:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8/block.Key -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.outputs(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.next, n, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.of_key(k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.stream(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.key_list(k)) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64>}

THEOREM: the generator keyed by k outputs C2SP's ChaCha8Rand stream keyed by k's eight words, for every key and every number of outputs