~/bend-docscommunity

proofs/crypto/chacha/core.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as Core

Generated by tools/generators/chacha_gen.py; do not edit. The unrolled ChaCha core refines the list-based RFC 8439 specification.

vec(s) is the RFC state list of a record state, one projection per entry, so that the list has its shape even when the state is abstract. One double round is compared with inner_block on a destructured state (both sides normalize to the same sixteen words); the round count is then an induction, so the theorems hold for every number of double rounds (ChaCha20, ChaCha8, ChaCha12 alike).

3 imports
import Base
import ../../../src/crypto/chacha/core.bend as C
import ../../../spec/crypto/chacha.bend as R

Laws

law double_round_correct provedsource · line 81 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.double_round(s)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.inner_block(vec(s)) : List<&2, U32>}

law rounds_correct provedsource · line 89 · raw

@+n:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.rounds(n, s)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.inner_blocks(n, vec(s)) : List<&2, U32>}

law add_correct provedsource · line 105 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.add(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.add_words(vec(a), vec(b)) : List<&2, U32>}

law bytes_correct provedsource · line 114 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.bytes(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.serialize(vec(s)) : List<&2, U32>}

law block_correct provedsource · line 123 · raw

@+n:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.block(n, s)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.serialize(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.add_words(vec(s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.inner_blocks(n, vec(s)))) : List<&2, U32>}

The block function with n double rounds, serialized, is the RFC's.

law init_correct provedsource · line 135 · raw

@+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+c:U32 -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}

law hinit_correct provedsource · line 153 · raw

@+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.hinit(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3]) : List<&2, U32>}

law hbytes_correct provedsource · line 171 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.hbytes(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.serialize([0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 3n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 12n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 13n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 14n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(vec(s), 15n)]) : List<&2, U32>}

Definitions

def p0 source · line 14 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p1 source · line 18 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p2 source · line 22 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p3 source · line 26 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p4 source · line 30 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p5 source · line 34 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p6 source · line 38 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p7 source · line 42 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p8 source · line 46 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p9 source · line 50 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p10 source · line 54 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p11 source · line 58 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p12 source · line 62 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p13 source · line 66 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p14 source · line 70 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def p15 source · line 74 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> U32

def vec source · line 78 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> List<&2, U32>