# Generated by tools/generators/hash_gen.py; do not edit by hand.
import Base
import ./sha/state.bend as S256
import ./sha/core.bend as C256
import ./sha/sha256.bend as SHA256
import ./sha512/types.bend as T512
import ./sha512/core.bend as C512
import ./keccak/types.bend as TK
import ./keccak/permutation.bend as P
import ./sha3/core.bend as C3

# Hash functions: one-shot and incremental.
#
#   sha256(bytes), sha512(bytes), sha3_256(bytes)       the digest (32, 64, 32 bytes)
#   new_sha256(), new_sha512(), new_sha3_256()          an empty Hasher
#   update(h, bytes)                                    h with bytes appended
#   update_all(h, chunks)                               update with each chunk in turn
#   digest(h)                                           the digest of everything appended
#
# Bytes are U32 values, each < 256 (List<&2, U32>). A Hasher keeps the chaining
# state, the bytes of the unfinished block (fewer than one block) and the total
# length; update compresses every block it completes, and digest pads the
# buffered tail with the total length. Proved (proofs/crypto/hash/laws.bend):
# each one-shot function equals its executable specification, and for every
# list of chunks, digest(update_all(new_X(), chunks)) == X(concat(chunks)).
# Hashers are values: update returns a new one, the old one is unchanged.

# A chaining state and the buffered bytes of the unfinished block.
type Sha256State is Data:
  St256{s: S256.State, buf: List<&2, U32>}

type Sha512State is Data:
  St512{s: T512.State, buf: List<&2, U32>}

type Sha3State is Data:
  St3{s: TK.State, buf: List<&2, U32>}

type Hasher is Data:
  Sha256H{st: Sha256State, len: Nat}
  Sha512H{st: Sha512State, len: Nat}
  Sha3H{st: Sha3State, len: Nat}

# ---------------------------------------------------------------- one-shot

# SHA-256 (FIPS 180-4), 32 bytes.
def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
  SHA256.sha256_bytes(bytes)

# SHA-512 (FIPS 180-4), 64 bytes.
def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
  C512.sha512(bytes)

# SHA3-256 (FIPS 202), 32 bytes.
def sha3_256(bytes: List<&2, U32>) -> List<&2, U32>:
  C3.sha3_256(bytes)

# ---------------------------------------------------------------- SHA-256 (FIPS 180-4)

# One block read 4 bytes at a time into its 16 words, or Short when
# fewer than 64 bytes are left.
type Read256 is Data:
  Blk256{w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, rest: List<&2, U32>}
  Short256{}

def read256_16(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32) -> Read256:
  Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}

def read256_15(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_14(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_13(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_12(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_11(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_10(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_9(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_8(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_7(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_8(rest, w0, w1, w2, w3, w4, w5, w6, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_6(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_7(rest, w0, w1, w2, w3, w4, w5, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_5(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_6(rest, w0, w1, w2, w3, w4, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_4(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_5(rest, w0, w1, w2, w3, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_3(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_4(rest, w0, w1, w2, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_2(bytes: List<&2, U32>, w0: U32, w1: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_3(rest, w0, w1, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_1(bytes: List<&2, U32>, w0: U32) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_2(rest, w0, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

def read256_0(bytes: List<&2, U32>) -> Read256:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> rest:
      read256_1(rest, C256.pack(b0, b1, b2, b3))
    case _:
      Short256{}

# Compress every whole block (fuel bounds the count: any fuel >= the number of
# blocks reads them all; fewer leaves the rest buffered, still correct). The
# chaining state and the unread bytes; orig is the list the read r started at.
# q is the algorithm's round parameter (48n), kept a variable for the proofs.
def absorb256(fuel: Nat, r: Read256, orig: List<&2, U32>, +q: Nat, s: S256.State) -> Sha256State:
  match fuel r:
    case 0n _:
      St256{s, orig}
    case 1n+p Short256{}:
      St256{s, orig}
    case 1n+p Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
      absorb256(p, read256_0(rest), rest, q, C256.fips_compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, s))

def step256(st: Sha256State, xs: List<&2, U32>, +q: Nat) -> Sha256State:
  match st:
    case St256{s, buf}:
      +bytes = List.append(&2, U32, buf, xs)
      absorb256(List.length(&2, U32, bytes), read256_0(bytes), bytes, q, s)

def finish256(st: Sha256State, +len: Nat, +q: Nat) -> List<&2, U32>:
  match st:
    case St256{s, buf}:
      SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, buf, C256.suffix(len)), q, C256.round_constants(), s)))

# ---------------------------------------------------------------- SHA-512 (FIPS 180-4)

# One block read 8 bytes at a time into its 16 words, or Short when
# fewer than 128 bytes are left.
type Read512 is Data:
  Blk512{w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane, rest: List<&2, U32>}
  Short512{}

def read512_16(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane) -> Read512:
  Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}

def read512_15(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_14(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_13(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_12(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_11(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_10(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_9(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_8(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_7(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_8(rest, w0, w1, w2, w3, w4, w5, w6, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_6(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_7(rest, w0, w1, w2, w3, w4, w5, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_5(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_6(rest, w0, w1, w2, w3, w4, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_4(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_5(rest, w0, w1, w2, w3, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_3(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_4(rest, w0, w1, w2, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_2(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_3(rest, w0, w1, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_1(bytes: List<&2, U32>, w0: T512.Lane) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_2(rest, w0, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

def read512_0(bytes: List<&2, U32>) -> Read512:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read512_1(rest, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
    case _:
      Short512{}

# Compress every whole block (fuel bounds the count: any fuel >= the number of
# blocks reads them all; fewer leaves the rest buffered, still correct). The
# chaining state and the unread bytes; orig is the list the read r started at.
# q is the algorithm's round parameter (64n), kept a variable for the proofs.
def absorb512(fuel: Nat, r: Read512, orig: List<&2, U32>, +q: Nat, s: T512.State) -> Sha512State:
  match fuel r:
    case 0n _:
      St512{s, orig}
    case 1n+p Short512{}:
      St512{s, orig}
    case 1n+p Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
      absorb512(p, read512_0(rest), rest, q, C512.compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, C512.round_constants(), s))

def step512(st: Sha512State, xs: List<&2, U32>, +q: Nat) -> Sha512State:
  match st:
    case St512{s, buf}:
      +bytes = List.append(&2, U32, buf, xs)
      absorb512(List.length(&2, U32, bytes), read512_0(bytes), bytes, q, s)

def finish512(st: Sha512State, +len: Nat, +q: Nat) -> List<&2, U32>:
  match st:
    case St512{s, buf}:
      C512.digest_bytes(C512.blocks(C512.lanes(List.append(&2, U32, buf, C512.suffix(len))), q, C512.round_constants(), s))

# ---------------------------------------------------------------- SHA3-256 (FIPS 202)

# One block read 8 bytes at a time into its 17 words, or Short when
# fewer than 136 bytes are left.
type Read3 is Data:
  Blk3{w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane, rest: List<&2, U32>}
  Short3{}

def read3_17(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane) -> Read3:
  Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, bytes}

def read3_16(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_17(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_15(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_14(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_13(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_12(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_11(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_10(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_9(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_8(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_7(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_8(rest, w0, w1, w2, w3, w4, w5, w6, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_6(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_7(rest, w0, w1, w2, w3, w4, w5, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_5(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_6(rest, w0, w1, w2, w3, w4, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_4(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_5(rest, w0, w1, w2, w3, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_3(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_4(rest, w0, w1, w2, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_2(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_3(rest, w0, w1, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_1(bytes: List<&2, U32>, w0: TK.Lane) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_2(rest, w0, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

def read3_0(bytes: List<&2, U32>) -> Read3:
  match bytes:
    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
      read3_1(rest, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
    case _:
      Short3{}

# Compress every whole block (fuel bounds the count: any fuel >= the number of
# blocks reads them all; fewer leaves the rest buffered, still correct). The
# chaining state and the unread bytes; orig is the list the read r started at.
# q is the algorithm's round parameter (24n), kept a variable for the proofs.
def absorb3(fuel: Nat, r: Read3, orig: List<&2, U32>, +q: Nat, s: TK.State) -> Sha3State:
  match fuel r:
    case 0n _:
      St3{s, orig}
    case 1n+p Short3{}:
      St3{s, orig}
    case 1n+p Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, +rest}:
      absorb3(p, read3_0(rest), rest, q, P.rounds(q, 0n, C3.inject(s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16)))

def step3(st: Sha3State, xs: List<&2, U32>, +q: Nat) -> Sha3State:
  match st:
    case St3{s, buf}:
      +bytes = List.append(&2, U32, buf, xs)
      absorb3(List.length(&2, U32, bytes), read3_0(bytes), bytes, q, s)

def finish3(st: Sha3State, +len: Nat, +q: Nat) -> List<&2, U32>:
  match st:
    case St3{s, buf}:
      C3.digest_bytes(C3.absorb(C3.lanes(List.append(&2, U32, buf, C3.suffix(len))), q, s))

# ---------------------------------------------------------------- the Hasher

def new_sha256() -> Hasher:
  Sha256H{St256{C256.initial(), Nil{}}, 0n}

def new_sha512() -> Hasher:
  Sha512H{St512{C512.initial(), Nil{}}, 0n}

def new_sha3_256() -> Hasher:
  Sha3H{St3{C3.zero(), Nil{}}, 0n}

def update(h: Hasher, +bytes: List<&2, U32>) -> Hasher:
  match h:
    case Sha256H{st, len}:
      Sha256H{step256(st, bytes, 48n), Nat.add(len, List.length(&2, U32, bytes))}
    case Sha512H{st, len}:
      Sha512H{step512(st, bytes, 64n), Nat.add(len, List.length(&2, U32, bytes))}
    case Sha3H{st, len}:
      Sha3H{step3(st, bytes, 24n), Nat.add(len, List.length(&2, U32, bytes))}

def fold(chunks: List<&2, List<&2, U32>>, h: Hasher) -> Hasher:
  match chunks:
    case Nil{}:
      h
    case c <> rest:
      fold(rest, update(h, c))

def update_all(h: Hasher, chunks: List<&2, List<&2, U32>>) -> Hasher:
  fold(chunks, h)

def digest(h: Hasher) -> List<&2, U32>:
  match h:
    case Sha256H{st, len}:
      finish256(st, len, 48n)
    case Sha512H{st, len}:
      finish512(st, len, 64n)
    case Sha3H{st, len}:
      finish3(st, len, 24n)