# Crc32 — Base-only CRC-32 (ISO 3309 / Ethernet).
#
# Input is a List<&2, U32>. Each element is an octet; only its low eight bits
# are consumed. The state uses the reflected polynomial 0xEDB88320.
import Base

# Reflected CRC-32 constants. 0xFFFFFFFF is expressed as bitwise not of zero.
def Crc32.init() -> U32:
  U32.not(0)

def Crc32.polynomial() -> U32:
  3988292384

# One reflected bit step. The low state bit selects whether the polynomial is
# XORed after the logical right shift.
def Crc32.step(+crc: U32) -> U32:
  +shifted = U32.shr(crc)
  Bool.pick(U32,
    U32.is_zero(U32.and(crc, 1)),
    shifted,
    U32.xor(shifted, Crc32.polynomial()))

# Process exactly eight bits of one octet.
def Crc32.byte.go(n: Nat, +crc: U32) -> U32:
  match n:
    case 0n:
      crc
    case 1n+p:
      Crc32.byte.go(p, Crc32.step(crc))

def Crc32.byte(+octet: U32, +crc: U32) -> U32:
  Crc32.byte.go(8n, U32.xor(crc, U32.and(octet, 255)))

# Update the unfinalized CRC state over a list of octets.
def Crc32.update.go(xs: List<&2, U32>, +crc: U32) -> U32:
  match xs:
    case Nil{}:
      crc
    case +octet <> rest:
      Crc32.update.go(rest, Crc32.byte(octet, crc))

def Crc32.update(+crc: U32, xs: List<&2, U32>) -> U32:
  Crc32.update.go(xs, crc)

# Apply the standard final XOR. `update` leaves this step to the caller so
# chunks can be processed incrementally.
def Crc32.finalize(+crc: U32) -> U32:
  U32.xor(crc, Crc32.init())

def Crc32.encode(xs: List<&2, U32>) -> U32:
  Crc32.finalize(Crc32.update(Crc32.init(), xs))