src/math/random/chacha8/block.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as Block

Generated by tools/generators/chacha8rand_gen.py; do not edit. The ChaCha8 core of ChaCha8Rand (C2SP chacha8rand; Go's internal/chacha8rand block_generic). One double round is fully unrolled (four column and four diagonal quarter rounds, RFC 8439 section 2.1-2.3, constant rotations); a block is four double rounds (eight rounds). As C2SP specifies, only the key words 4..11 are added back after the rounds: the constants and the counter are not (the standard ChaCha output minus them). A group is four consecutive blocks interleaved word by word, read as 32 little-endian 64-bit words: word 2w of the group is word w of the first block (low half) and of the second (high half), word 2w + 1 the same for the third and fourth block.

Proved equal to spec/math/random/chacha8rand.bend for every key and counter (proofs/math/random/chacha8/).

2 imports

import Base
import ../../u64.bend as W

Types

type Key source · line 19 · raw

Data

the 256-bit key as eight little-endian words

K

@k0:U32 -> @k1:U32 -> @k2:U32 -> @k3:U32 -> @k4:U32 -> @k5:U32 -> @k6:U32 -> @k7:U32 -> Key

type Vector source · line 23 · raw

Data

the ChaCha state x[0..15]

V

@v0:U32 -> @v1:U32 -> @v2:U32 -> @v3:U32 -> @v4:U32 -> @v5:U32 -> @v6:U32 -> @v7:U32 -> @v8:U32 -> @v9:U32 -> @v10:U32 -> @v11:U32 -> @v12:U32 -> @v13:U32 -> @v14:U32 -> @v15:U32 -> Vector

Definitions

def init source · line 27 · raw

@k:Key -> @+ctr:U32 -> Vector

the initial state: constants, key, 32-bit block counter, zero nonce

def dr source · line 33 · raw

@v:Vector -> Vector

one double round: four column quarter rounds, then four diagonal ones

def finish source · line 135 · raw

@k:Key -> @v:Vector -> Vector

the key words added back to words 4..11

def block source · line 141 · raw

@+k:Key -> @+ctr:U32 -> Vector

the ChaCha8Rand block with counter ctr: eight rounds

def interleave source · line 145 · raw

@a:Vector -> @b:Vector -> @c:Vector -> @d:Vector -> List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

four blocks interleaved word by word, as 32 little-endian 64-bit words

def group source · line 151 · raw

@+k:Key -> @+ctr:U32 -> List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

the group of the blocks ctr, ctr + 1, ctr + 2, ctr + 3