~/bend-docscommunity

spec/math/random/chacha8rand.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8rand

3 imports
import Base
import ../../../src/math/u64.bend as W
import ../../../src/math/random/chacha8/block.bend as B

Definitions

def key_list source · line 31 · raw

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

the key record as the list of its eight little-endian words

def get source · line 36 · raw

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

def put source · line 45 · raw

@xs:List<&2, U32> -> @i:Nat -> @y:U32 -> List<&2, U32>

def rotl source · line 55 · raw

@+x:U32 -> @+n:Nat -> U32

x <<< n, 0 < n < 32

def quarter source · line 60 · raw

@+x:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> List<&2, U32>

RFC 8439 2.1: a += b; d ^= a; d <<<= 16; c += d; b ^= c; b <<<= 12; a += b; d ^= a; d <<<= 8; c += d; b ^= c; b <<<= 7 (2.2: on x[a..d])

def double_round source · line 72 · raw

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

RFC 8439 2.3 inner_block (on the sixteen words of a state)

def double_rounds source · line 86 · raw

@n:Nat -> @x:List<&2, U32> -> List<&2, U32>

def append source · line 93 · raw

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

def initial source · line 101 · raw

@key:List<&2, U32> -> @+ctr:U32 -> List<&2, U32>

RFC 8439 2.3: constants, key (eight words), block counter, nonce (here zero)

def add_words source · line 108 · raw

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

def chacha8 source · line 116 · raw

@+key:List<&2, U32> -> @+ctr:U32 -> List<&2, U32>

the ChaCha8 block function: eight rounds, then the input added back

def sub_at source · line 119 · raw

@+x:List<&2, U32> -> @+i:Nat -> @+c:U32 -> List<&2, U32>

def subtract source · line 124 · raw

@+b:List<&2, U32> -> @+i:U32 -> List<&2, U32>

C2SP: for each block, subtract the constants from words 0..3 and the block counter from word 12

def c2sp_block source · line 127 · raw

@+key:List<&2, U32> -> @+i:U32 -> List<&2, U32>

def interleave source · line 132 · raw

@k:Nat -> @+i:Nat -> @+b0:List<&2, U32> -> @+b1:List<&2, U32> -> @+b2:List<&2, U32> -> @+b3:List<&2, U32> -> List<&2, U32>

C2SP: "for each sequence of four blocks, first we output the first four bytes of each block, then the next four bytes of each block, and so on"

def group source · line 140 · raw

@+key:List<&2, U32> -> @+g:U32 -> List<&2, U32>

the blocks g, g + 1, g + 2, g + 3, permuted

def iteration source · line 144 · raw

@+key:List<&2, U32> -> List<&2, U32>

one iteration: the sixteen blocks 0..15, permuted, as 256 words

def take source · line 147 · raw

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

def drop source · line 156 · raw

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

def output source · line 166 · raw

@+key:List<&2, U32> -> List<&2, U32>

the first 992 bytes are output, the last 32 bytes key the next iteration

def next_key source · line 169 · raw

@+key:List<&2, U32> -> List<&2, U32>

def words64 source · line 173 · raw

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

consecutive little-endian word pairs as 64-bit words

def tail source · line 187 · raw

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

def stream_go source · line 196 · raw

@n:Nat -> @buf:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+key:List<&2, U32> -> List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

n outputs: the words left of the current iteration, then the next iterations, each keyed by the last 32 bytes of the one before

def stream source · line 206 · raw

@n:Nat -> @+key:List<&2, U32> -> List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

the first n 64-bit outputs of ChaCha8Rand keyed by key (eight words)

def le32 source · line 210 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> U32

Go's byteorder.LEUint32: b0 | b1 << 8 | b2 << 16 | b3 << 24

def bytes_ok source · line 213 · raw

@bs:List<&2, U32> -> Bool

def words_of source · line 220 · raw

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

def length source · line 227 · raw

@bs:List<&2, U32> -> Nat

def key_if source · line 234 · raw

@+bs:List<&2, U32> -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def key_of_seed source · line 242 · raw

@+seed:List<&2, U32> -> Maybe<&2, List<&2, U32>>

the key of a seed: 32 bytes, each below 256