proofs/crypto/random/bytes.bend checks

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

12 imports

import Base
import ../../../src/math/u64.bend as W
import ../../../src/math/random/chacha8.bend as C8
import ../../../src/crypto/random.bend as CR
import ../../../spec/math/random/source.bend as SRC
import ../../../spec/crypto/random.bend as SCR
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ../../../spec/math/random/rand.bend as SR
import ../../math/random/bits.bend as BI
import ../../math/random/below.bend as BL

Definitions

def rev source · line 18 · raw

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

def app_nil source · line 21 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(xs, []) == xs : List<&2, U32>}

def app_assoc source · line 28 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+zs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(xs, ys), zs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(ys, zs)) : List<&2, U32>}

def rgo source · line 36 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {List.reverse.go(&2, U32, xs, ys) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(xs), ys) : List<&2, U32>}

reverse.go(xs, ys) = reverse(xs) ++ ys

def rev_cons source · line 48 · raw

@+b:U32 -> @+acc:List<&2, U32> -> @+ts:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(b <> acc), ts) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(acc), b <> ts) : List<&2, U32>}

rev(b :: acc) ++ ts = rev(acc) ++ (b :: ts)

def b0 source · line 54 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> U32

the eight bytes of a word, split at the first

def b7 source · line 59 · raw

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

def le_split source · line 64 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.le_bytes(x) == b0(x) <> b7(x) : List<&2, U32>}

def outs source · line 69 · raw

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

def prefix source · line 73 · raw

@+j:Nat -> @+r:List<&2, U32> -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8 -> @+d:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(r, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(Nat.add(j, d), c)))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(r, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(j, c)))) : List<&2, U32>}

taking j bytes never looks past the first j outputs

def facc source · line 93 · raw

@f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> List<&2, U32>

def fsrc source · line 98 · raw

@f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8

def fpend source · line 103 · raw

@f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> List<&2, U32>

def step_nil source · line 108 · raw

@+j:Nat -> @+acc:List<&2, U32> -> @q:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(facc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.split(acc, q))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(fpend(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.split(acc, q)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(j, fsrc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.split(acc, q))))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(acc), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(1n+j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.fst64(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, q) <> outs(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.snd64(0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.ChaCha8, q))))) : List<&2, U32>}

def step source · line 117 · raw

@+j:Nat -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(facc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.take1(f))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(fpend(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.take1(f)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(j, fsrc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.take1(f))))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(facc(f)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(1n+j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(fpend(f), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(1n+j, fsrc(f)))))) : List<&2, U32>}

one byte of the loop against the byte stream

def fill_inv source · line 133 · raw

@+k:Nat -> @+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> {rev(facc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.fill(k, f))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(rev(facc(f)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(fpend(f), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(outs(k, fsrc(f)))))) : List<&2, U32>}

THEOREM: after k bytes the accumulator, read back, is the old one followed by the first k bytes of the pending bytes and the stream

def done_bytes source · line 142 · raw

@+f:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Fill -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.fst_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.Gen, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.done(f)) == rev(facc(f)) : List<&2, U32>}

def bytes source · line 148 · raw

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

THEOREM (Random.bytes)

def and_true_r source · line 155 · raw

@+b:Bool -> {Bool.and(b, True{}) == b : Bool}

def below_take source · line 162 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.take(n, xs)) == True{} : Bool}

def below_app source · line 172 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(xs) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(ys) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.append(xs, ys)) == True{} : Bool}

def byte_lt source · line 181 · raw

@+y:U32 -> {U32.is_lt(U32.and(y, 255), 256) == True{} : Bool}

y & 255 < 256

def byte_of_lt source · line 187 · raw

@+w:U32 -> @+k:Nat -> {U32.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.byte_of(w, k), 256) == True{} : Bool}

def le_below source · line 190 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.le_bytes(x)) == True{} : Bool}

def flat_below source · line 203 · raw

@+os:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.below256(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.flat(os)) == True{} : Bool}

def bytes_lt source · line 211 · 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)

THEOREM (Random.bytes_lt)