proofs/crypto/chacha/core.bend source
proofs/crypto/chacha/core.bend on the hub · documented module
# 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).import Baseimport ../../../src/crypto/chacha/core.bend as Cimport ../../../spec/crypto/chacha.bend as Rdef p0(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0def p1(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1def p2(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2def p3(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3def p4(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4def p5(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5def p6(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6def p7(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7def p8(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8def p9(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9def p10(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10def p11(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11def p12(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12def p13(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13def p14(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14def p15(s: C.State) -> U32: match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15def vec(+s: C.State) -> List<&2, U32>: [p0(s), p1(s), p2(s), p3(s), p4(s), p5(s), p6(s), p7(s), p8(s), p9(s), p10(s), p11(s), p12(s), p13(s), p14(s), p15(s)]law double_round_correct: for +s: C.State {vec(C.double_round(s)) == R.inner_block(vec(s)) : List<&2, U32>}def double_round_correct(s): match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}law rounds_correct: for +n: Nat for +s: C.State {vec(C.rounds(n, s)) == R.inner_blocks(n, vec(s)) : List<&2, U32>}def rounds_correct(n, s): match n: case 0n: {==} case 1n+p: Equal.trans(List<&2, U32>, vec(C.rounds(p, C.double_round(s))), R.inner_blocks(p, vec(C.double_round(s))), R.inner_blocks(p, R.inner_block(vec(s))), rounds_correct(p, C.double_round(s)), Equal.cong(List<&2, U32>, List<&2, U32>, l => R.inner_blocks(p, l), vec(C.double_round(s)), R.inner_block(vec(s)), double_round_correct(s)))law add_correct: for +a: C.State for +b: C.State {vec(C.add(a, b)) == R.add_words(vec(a), vec(b)) : List<&2, U32>}def add_correct(a, b): match a b: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} C.S{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15}: {==}law bytes_correct: for +s: C.State {C.bytes(s) == R.serialize(vec(s)) : List<&2, U32>}def bytes_correct(s): match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}# The block function with n double rounds, serialized, is the RFC's.law block_correct: for +n: Nat for +s: C.State {C.bytes(C.block(n, s)) == R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))) : List<&2, U32>}def block_correct(n, s): Equal.trans(List<&2, U32>, C.bytes(C.block(n, s)), R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))), bytes_correct(C.add(s, C.rounds(n, s))), Equal.trans(List<&2, U32>, R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), vec(C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))), Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(l), vec(C.add(s, C.rounds(n, s))), R.add_words(vec(s), vec(C.rounds(n, s))), add_correct(s, C.rounds(n, s))), Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(R.add_words(vec(s), l)), vec(C.rounds(n, s)), R.inner_blocks(n, vec(s)), rounds_correct(n, s))))law init_correct: for +k0: U32 for +k1: U32 for +k2: U32 for +k3: U32 for +k4: U32 for +k5: U32 for +k6: U32 for +k7: U32 for +c: U32 for +n0: U32 for +n1: U32 for +n2: U32 {vec(C.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == R.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}def init_correct(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2): {==}law hinit_correct: for +k0: U32 for +k1: U32 for +k2: U32 for +k3: U32 for +k4: U32 for +k5: U32 for +k6: U32 for +k7: U32 for +n0: U32 for +n1: U32 for +n2: U32 for +n3: U32 {vec(C.hinit(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3)) == R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3]) : List<&2, U32>}def hinit_correct(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3): {==}law hbytes_correct: for +s: C.State {C.hbytes(s) == R.serialize([R.get(vec(s), 0n), R.get(vec(s), 1n), R.get(vec(s), 2n), R.get(vec(s), 3n), R.get(vec(s), 12n), R.get(vec(s), 13n), R.get(vec(s), 14n), R.get(vec(s), 15n)]) : List<&2, U32>}def hbytes_correct(s): match s: case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}