# Generated by tools/generators/sha512_gen.py; do not edit by hand.
import Base
import ../../../src/crypto/sha512/types.bend as T
import ../../../src/crypto/sha512/core.bend as C
import ../../../spec/crypto/sha512.bend as F

# src/crypto/sha512/core.bend refines spec/crypto/sha512.bend, the structure
# of proofs/crypto/sha/conformance.bend (SHA-256) at 64-bit words: one round
# and the feedforward are equal after opening every word into its halves;
# the rolling window computes the spec's recurrence over the reverse history;
# a block's rounds, the blocks, the parsing and the padding follow by
# induction, each short tail by enumeration.

law step_correct:
  for +s: T.State
  for +k: T.Lane
  for +w: T.Lane
  {C.step(s, k, w) == F.step(s, k, w) : T.State}

def step_correct(s, k, w):
  match s k w:
    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.W{kh, kl} T.W{wh, wl}:
      {==}

law feedforward_correct:
  for +x: T.State
  for +y: T.State
  {C.feedforward(x, y) == F.feedforward(x, y) : T.State}

def feedforward_correct(x, y):
  match x y:
    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.H{T.W{ih, il}, T.W{jh, jl}, T.W{kh, kl}, T.W{lh, ll}, T.W{mh, ml}, T.W{nh, nl}, T.W{oh, ol}, T.W{ph, pl}}:
      {==}

law next_correct:
  for +a: T.Lane
  for +b: T.Lane
  for +c: T.Lane
  for +d: T.Lane
  for +e: T.Lane
  for +f: T.Lane
  for +g: T.Lane
  for +h: T.Lane
  for +i: T.Lane
  for +j: T.Lane
  for +k: T.Lane
  for +l: T.Lane
  for +m: T.Lane
  for +n: T.Lane
  for +o: T.Lane
  for +p: T.Lane
  for +rest: List<&2, T.Lane>
  {C.next(b, g, o, p) == F.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : T.Lane}

def next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest):
  match b g o p:
    case T.W{bh, bl} T.W{gh, gl} T.W{oh, ol} T.W{ph, pl}:
      {==}

law window_rounds_correct:
  for +q: Nat
  for +a: T.Lane
  for +b: T.Lane
  for +c: T.Lane
  for +d: T.Lane
  for +e: T.Lane
  for +f: T.Lane
  for +g: T.Lane
  for +h: T.Lane
  for +i: T.Lane
  for +j: T.Lane
  for +k: T.Lane
  for +l: T.Lane
  for +m: T.Lane
  for +n: T.Lane
  for +o: T.Lane
  for +p: T.Lane
  for +rest: List<&2, T.Lane>
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}

def window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
  match q ks:
    case 0n Nil{}:
      {==}
    case 0n x <> xt:
      {==}
    case 1n+r Nil{}:
      {==}
    case 1n+r x <> xt:
      %next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest) :
        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
          F.rounds(xt, F.extension(r, _ <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(F.step(s, x, _)) : T.State}
      %step_correct(s, x, C.next(b, g, o, p)) :
        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
          F.rounds(xt, F.extension(r, C.next(b, g, o, p) <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(_) : T.State}
      window_rounds_correct(r, C.next(b, g, o, p), a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p <> rest, xt,
        C.step(s, x, C.next(b, g, o, p)))

law block_rounds_correct:
  for +ws: List<&2, T.Lane>
  for +q: Nat
  for +a: T.Lane
  for +b: T.Lane
  for +c: T.Lane
  for +d: T.Lane
  for +e: T.Lane
  for +f: T.Lane
  for +g: T.Lane
  for +h: T.Lane
  for +i: T.Lane
  for +j: T.Lane
  for +k: T.Lane
  for +l: T.Lane
  for +m: T.Lane
  for +n: T.Lane
  for +o: T.Lane
  for +p: T.Lane
  for +rest: List<&2, T.Lane>
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {C.block_rounds(ws, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) ==
    F.rounds(ks, List.append(&2, T.Lane, ws, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(s) : T.State}

def block_rounds_correct(ws, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
  match ws ks:
    case Nil{} _:
      window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s)
    case w <> wt Nil{}:
      {==}
    case w <> wt x <> xt:
      %step_correct(s, x, w) :
        {C.block_rounds(w <> wt, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
          F.rounds(xt, List.append(&2, T.Lane, wt, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(_) : T.State}
      block_rounds_correct(wt, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, xt, C.step(s, x, w))

law compress16_correct:
  for +a: T.Lane
  for +b: T.Lane
  for +c: T.Lane
  for +d: T.Lane
  for +e: T.Lane
  for +f: T.Lane
  for +g: T.Lane
  for +h: T.Lane
  for +i: T.Lane
  for +j: T.Lane
  for +k: T.Lane
  for +l: T.Lane
  for +m: T.Lane
  for +n: T.Lane
  for +o: T.Lane
  for +p: T.Lane
  for +q: Nat
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == F.compress(F.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : T.State}

def compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s):
  +r = F.rounds(ks, List.append(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], F.extension(q, List.reverse(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]))))(s)
  %feedforward_correct(s, r) : {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == _ : T.State}
  Equal.cong(T.State, T.State, t => C.feedforward(s, t),
    C.block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, C.Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s), r,
    block_rounds_correct([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a, Nil{}, ks, s))

law blocks_correct:
  for +ws: List<&2, T.Lane>
  for +q: Nat
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {C.blocks(ws, q, ks, s) == F.blocks(F.schedules(ws, q), ks)(s) : T.State}

def blocks_correct(ws, q, ks, s):
  match ws:
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
      %compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) :
        {C.blocks(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, q, ks, s) == F.blocks(F.schedules(rest, q), ks)(_) : T.State}
      blocks_correct(rest, q, ks, C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s))
    case Nil{}:
      {==}
    case a <> Nil{}:
      {==}
    case a <> b <> Nil{}:
      {==}
    case a <> b <> c <> Nil{}:
      {==}
    case a <> b <> c <> d <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> Nil{}:
      {==}
    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> Nil{}:
      {==}

law lanes_correct:
  for +bytes: List<&2, U32>
  {C.lanes(bytes) == F.words(bytes) : List<&2, T.Lane>}

def lanes_correct(bytes):
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      %lanes_correct(rest) :
        {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.decode(b0, b1, b2, b3), F.decode(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>}
      {==}
    case Nil{}:
      {==}
    case b0 <> Nil{}:
      {==}
    case b0 <> b1 <> Nil{}:
      {==}
    case b0 <> b1 <> b2 <> Nil{}:
      {==}
    case b0 <> b1 <> b2 <> b3 <> Nil{}:
      {==}
    case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}:
      {==}
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}:
      {==}
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}:
      {==}

law zeros_correct:
  for +r: Nat
  for +fits: Bool
  {C.zeros_if(r, fits) == F.zero_count_if(r, fits) : Nat}

def zeros_correct(r, fits):
  match fits:
    case True{}:
      {==}
    case False{}:
      {==}

law suffix_correct:
  for +n: Nat
  {C.suffix(n) == F.padding_suffix(n) : List<&2, U32>}

def suffix_correct(n):
  %zeros_correct(Nat.mod(n, 128n), Nat.is_le(Nat.mod(n, 128n), 111n)) :
    {C.suffix(n) == 128 <> List.append(&2, U32, List.replicate(U32, _, 0), F.length_field(n)) : List<&2, U32>}
  {==}

law digest_correct:
  for +s: T.State
  {C.digest_bytes(s) == F.digest_octets(F.digest(s)) : List<&2, U32>}

def digest_correct(s):
  match s:
    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
      {==}

law digest_length:
  for +s: T.State
  {List.length(&2, U32, C.digest_bytes(s)) == 64n : Nat}

def digest_length(s):
  match s:
    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
      {==}

law constants_correct:
  {C.round_constants() == F.constants() : List<&2, T.Lane>}

def constants_correct():
  {==}

law initial_correct:
  {C.initial() == F.initial() : T.State}

def initial_correct():
  {==}

law sha512_correct:
  for +bytes: List<&2, U32>
  {C.sha512(bytes) == F.sha512_bytes(bytes) : List<&2, U32>}

def sha512_correct(bytes):
  +n = List.length(&2, U32, bytes)
  %suffix_correct(n) :
    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(F.words(
      List.append(&2, U32, bytes, _)), 64n), F.constants())(F.initial()))) : List<&2, U32>}
  +padded = List.append(&2, U32, bytes, C.suffix(n))
  %lanes_correct(padded) :
    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(_, 64n), F.constants())(F.initial()))) : List<&2, U32>}
  %Equal.sym(List<&2, T.Lane>, C.round_constants(), F.constants(), constants_correct()) :
    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), _)(F.initial()))) : List<&2, U32>}
  %Equal.sym(T.State, C.initial(), F.initial(), initial_correct()) :
    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), C.round_constants())(_))) : List<&2, U32>}
  %blocks_correct(C.lanes(padded), 64n, C.round_constants(), C.initial()) :
    {C.sha512(bytes) == F.digest_octets(F.digest(_)) : List<&2, U32>}
  digest_correct(C.blocks(C.lanes(padded), 64n, C.round_constants(), C.initial()))