# 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 Base
import ../../../src/crypto/chacha/core.bend as C
import ../../../spec/crypto/chacha.bend as R

def 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}: a0

def 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}: a1

def 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}: a2

def 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}: a3

def 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}: a4

def 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}: a5

def 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}: a6

def 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}: a7

def 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}: a8

def 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}: a9

def 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}: a10

def 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}: a11

def 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}: a12

def 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}: a13

def 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}: a14

def 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}: a15

def 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}: {==}