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

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

Generated by tools/generators/chacha8rand_gen.py; do not edit. The unrolled ChaCha8 pieces of src/math/random/chacha8/block.bend against the list-based RFC 8439 / C2SP specification spec/math/random/chacha8rand.bend, for every state and key: one double round (both sides symbolic in the sixteen words, so the checker compares one double round at a time), the initial state, the final additions with C2SP's subtractions, and the four-block interleaving.

5 imports

import Base
import ../../../../src/math/u64.bend as W
import ../../../../src/math/random/chacha8/block.bend as B
import ../../../../spec/math/random/chacha8rand.bend as S
import ../../../lib/u32alg.bend as A

Definitions

def vec source · line 17 · raw

@v:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> List<&2, U32>

the state as the RFC list x[0..15]; like S.key_list on a key, it is stuck on an abstract state, so the checker never unfolds rounds of symbolic words it does not have to compare

def dr_correct source · line 22 · raw

@+v:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> {vec(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.dr(v)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.double_round(vec(v)) : List<&2, U32>}

one double round is RFC 8439's inner_block

def init_correct source · line 26 · raw

@+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Key -> @+ctr:U32 -> {vec(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.init(k, ctr)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.initial(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.key_list(k), ctr) : List<&2, U32>}

def cancel source · line 31 · raw

@+x:U32 -> @+c:U32 -> {U32.sub(U32.add(x, c), c) == x : U32}

x + c - c = x

def finish_correct source · line 37 · raw

@+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Key -> @+v:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> @+ctr:U32 -> {vec(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.finish(k, v)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.subtract(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.add_words(vec(v), vec(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.init(k, ctr))), ctr) : List<&2, U32>}

the key words added back, C2SP's subtractions of the constants and the counter, and the zero nonce words: the words the implementation keeps

def interleave_correct source · line 51 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> @+c:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.interleave(a, b, c, d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.words64(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.interleave(16n, 0n, vec(a), vec(b), vec(c), vec(d))) : List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

the interleaving is C2SP's permutation read as little-endian 64-bit words