# Laws for Base64's Base-only List<&2, U32> API.
#
# The decoder is strict RFC 4648: input length is a multiple of four, only the
# standard alphabet is accepted, '=' occurs only in the final quartet, and
# unused padding bits must be zero. A decoded U32 is an octet (0..255).
import Base
import ./lib.bend as B64

# Empty input encodes to the empty string.
law encode_empty:
  { B64.Base64.encode(Nil{}) == "" : String }

# One byte uses two alphabet characters and two padding characters.
law encode_one:
  { B64.Base64.encode(102 <> Nil{}) == "Zg==" : String }

# Two bytes use three alphabet characters and one padding character.
law encode_two:
  { B64.Base64.encode(102 <> 111 <> Nil{}) == "Zm8=" : String }

# A complete three-byte group has no padding.
law encode_three:
  { B64.Base64.encode(102 <> 111 <> 111 <> Nil{}) == "Zm9v" : String }

# Multiple groups concatenate without separators.
law encode_multiple:
  {
    B64.Base64.encode(102 <> 111 <> 111 <> 98 <> 97 <> 114 <> Nil{})
      == "Zm9vYmFy"
    : String
  }

# Elements are octet-oriented: the low eight bits are encoded.
law encode_masks_u32:
  { B64.Base64.encode(256 <> Nil{}) == "AA==" : String }

# Empty Base64 decodes to an empty list.
law decode_empty:
  { B64.Base64.decode("") == Some{Nil{}} : Maybe<&2, List<&2, U32>> }

# One padded quartet decodes to one octet.
law decode_one_pad:
  { B64.Base64.decode("Zg==") == Some{102 <> Nil{}} : Maybe<&2, List<&2, U32>> }

# Two padded quartet decodes to two octets.
law decode_two_pad:
  { B64.Base64.decode("Zm8=") == Some{102 <> 111 <> Nil{}} : Maybe<&2, List<&2, U32>> }

# An unpadded quartet decodes to three octets.
law decode_full:
  {
    B64.Base64.decode("Zm9v") == Some{102 <> 111 <> 111 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

# Multiple quartets concatenate in input order.
law decode_multiple:
  {
    B64.Base64.decode("Zm9vYmFy")
      == Some{102 <> 111 <> 111 <> 98 <> 97 <> 114 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

# Canonical examples round-trip through both public functions.
law roundtrip_one:
  {
    B64.Base64.decode(B64.Base64.encode(102 <> Nil{}))
      == Some{102 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

law roundtrip_two:
  {
    B64.Base64.decode(B64.Base64.encode(102 <> 111 <> Nil{}))
      == Some{102 <> 111 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

law roundtrip_three:
  {
    B64.Base64.decode(B64.Base64.encode(102 <> 111 <> 111 <> Nil{}))
      == Some{102 <> 111 <> 111 <> Nil{}}
    : Maybe<&2, List<&2, U32>>
  }

# Invalid alphabet characters are rejected.
law reject_invalid_alphabet:
  { B64.Base64.decode("not!") == None{} : Maybe<&2, List<&2, U32>> }

# A non-multiple-of-four length is rejected.
law reject_short_quartet:
  { B64.Base64.decode("Zg=") == None{} : Maybe<&2, List<&2, U32>> }

# Padding cannot appear before the final two positions.
law reject_early_padding:
  { B64.Base64.decode("Z=g=") == None{} : Maybe<&2, List<&2, U32>> }

# One '=' requires a real third sextet and two '=' require c='='.
law reject_bad_padding_shape:
  { B64.Base64.decode("Zg=A") == None{} : Maybe<&2, List<&2, U32>> }

# Nonzero unused bits are rejected rather than silently normalized.
law reject_noncanonical_one:
  { B64.Base64.decode("Zh==") == None{} : Maybe<&2, List<&2, U32>> }

law reject_noncanonical_two:
  { B64.Base64.decode("Zm/=") == None{} : Maybe<&2, List<&2, U32>> }

# Padding is allowed only in the final quartet.
law reject_padding_before_tail:
  { B64.Base64.decode("Zg==AAAA") == None{} : Maybe<&2, List<&2, U32>> }