# Executable laws for the strict, lowercase Hex codec.
# Decode accepts exactly pairs of 0-9a-fA-F and returns canonical octets.
import Base
import ./lib.bend as Hx

# Empty and ordinary encoding.
law encode_empty:
  { Hx.Hex.encode(Nil{}) == "" : String }

law encode_zero:
  { Hx.Hex.encode(0 <> Nil{}) == "00" : String }

law encode_one:
  { Hx.Hex.encode(1 <> Nil{}) == "01" : String }

law encode_ten:
  { Hx.Hex.encode(10 <> Nil{}) == "0a" : String }

law encode_fifteen:
  { Hx.Hex.encode(15 <> Nil{}) == "0f" : String }

law encode_sixteen:
  { Hx.Hex.encode(16 <> Nil{}) == "10" : String }

law encode_sevenf:
  { Hx.Hex.encode(127 <> Nil{}) == "7f" : String }

law encode_ff:
  { Hx.Hex.encode(255 <> Nil{}) == "ff" : String }

# Encoding follows the companion Bytes.hex low-octet convention.
law encode_masks_u32:
  { Hx.Hex.encode(256 <> Nil{}) == "00" : String }

law encode_multiple:
  { Hx.Hex.encode(0 <> 10 <> 255 <> Nil{}) == "000aff" : String }

# Empty and lowercase/uppercase input decoding.
law decode_empty:
  { Hx.Hex.decode("") == Some{Nil{}} : Maybe<&2, List<&2, U32>> }

law decode_zero:
  { Hx.Hex.decode("00") == Some{0 <> Nil{}} : Maybe<&2, List<&2, U32>> }

law decode_lowercase:
  { Hx.Hex.decode("0aff") == Some{10 <> 255 <> Nil{}} : Maybe<&2, List<&2, U32>> }

law decode_uppercase:
  { Hx.Hex.decode("0AFF") == Some{10 <> 255 <> Nil{}} : Maybe<&2, List<&2, U32>> }

law decode_mixed_case:
  { Hx.Hex.decode("aB0c") == Some{171 <> 12 <> Nil{}} : Maybe<&2, List<&2, U32>> }

law decode_multiple:
  { Hx.Hex.decode("000aff7f") == Some{0 <> 10 <> 255 <> 127 <> Nil{}} : Maybe<&2, List<&2, U32>> }

# Canonical lowercase encodings round-trip.
law roundtrip_empty:
  { Hx.Hex.decode(Hx.Hex.encode(Nil{})) == Some{Nil{}} : Maybe<&2, List<&2, U32>> }

law roundtrip_one:
  { Hx.Hex.decode(Hx.Hex.encode(1 <> Nil{})) == Some{1 <> Nil{}} : Maybe<&2, List<&2, U32>> }

law roundtrip_multiple:
  {
    Hx.Hex.decode(Hx.Hex.encode(0 <> 10 <> 127 <> 128 <> 255 <> Nil{}))
      == Some{0 <> 10 <> 127 <> 128 <> 255 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

# Strict rejection: odd length, invalid alphabet, and non-hex punctuation.
law reject_odd_length:
  { Hx.Hex.decode("a") == None{} : Maybe<&2, List<&2, U32>> }

law reject_three_chars:
  { Hx.Hex.decode("abc") == None{} : Maybe<&2, List<&2, U32>> }

law reject_invalid_g:
  { Hx.Hex.decode("0g") == None{} : Maybe<&2, List<&2, U32>> }

law reject_invalid_prefix:
  { Hx.Hex.decode("0x") == None{} : Maybe<&2, List<&2, U32>> }

law reject_whitespace:
  { Hx.Hex.decode(" 0") == None{} : Maybe<&2, List<&2, U32>> }

law reject_prefix:
  { Hx.Hex.decode("0x0a") == None{} : Maybe<&2, List<&2, U32>> }

law reject_bad_tail:
  { Hx.Hex.decode("00zz") == None{} : Maybe<&2, List<&2, U32>> }