# Definitional laws for Crc32's Base-only List<&2, U32> API.
import Base
import ./lib.bend as Crc

# The standard empty CRC is zero after init and final XOR.
law encode_empty:
  { Crc.Crc32.encode(Nil{}) == 0 : U32 }

# A zero octet is the standard CRC-32 vector D202EF8D.
law encode_zero_octet:
  { Crc.Crc32.encode(0 <> Nil{}) == 3523407757 : U32 }

# The canonical CRC-32 check vector for ASCII "123456789" is CBF43926.
law encode_check_vector:
  {
    Crc.Crc32.encode(49 <> 50 <> 51 <> 52 <> 53 <> 54 <> 55 <> 56 <> 57 <> Nil{})
      == 3421780262
    : U32
  }

# A second short ASCII vector: CRC-32("hello") = 3610A686.
law encode_hello:
  {
    Crc.Crc32.encode(104 <> 101 <> 108 <> 108 <> 111 <> Nil{})
      == 907060870
    : U32
  }

# Values are interpreted as octets, so high bits are ignored.
law encode_masks_octet:
  { Crc.Crc32.encode(256 <> Nil{}) == Crc.Crc32.encode(0 <> Nil{}) : U32 }

# Finalization is the same operation exposed independently.
law finalize_update_empty:
  {
    Crc.Crc32.finalize(Crc.Crc32.update(Crc.Crc32.init(), Nil{})) == 0
    : U32
  }