LAWS.bend source

LAWS.bend on the hub · documented module

# Executable laws for the strict, lowercase Hex codec.# Decode accepts exactly pairs of 0-9a-fA-F and returns canonical octets.import Baseimport ./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>> }