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

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

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 ./rounds.bend as R

Definitions

def drs source · line 11 · raw

@n:Nat -> @v:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector

n double rounds, the model of the implementation's dr(dr(dr(dr(x))))

def drs_correct source · line 18 · raw

@+n:Nat -> @+v:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/chacha8/block.Vector -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/rounds.vec(drs(n, v)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/chacha8rand.double_rounds(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/chacha8/rounds.vec(v)) : List<&2, U32>}

def rounds_correct source · line 28 · raw

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

the eight rounds on the initial state

def block_correct source · line 34 · raw

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

THEOREM: the implementation's block is C2SP's block ctr

def group_correct source · line 44 · raw

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

THEOREM: the implementation's group is C2SP's four permuted blocks ctr .. ctr + 3, read as little-endian 64-bit words