LAWS.bend source

LAWS.bend on the hub · documented module

# 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 Baseimport ./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>> }