LAWS.bend open laws/TODOs

raw source on the hub · import 0xd9193642e70279e288909ba354d1bb6a/LAWS.bend as LAWS

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).

2 imports

import Base
import ./lib.bend as B64

Laws

law encode_empty provedin PROOF.bendsource · line 10 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([]) == "" : String}

Empty input encodes to the empty string.

law encode_one provedin PROOF.bendsource · line 14 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102]) == "Zg==" : String}

One byte uses two alphabet characters and two padding characters.

law encode_two provedin PROOF.bendsource · line 18 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102, 111]) == "Zm8=" : String}

Two bytes use three alphabet characters and one padding character.

law encode_three provedin PROOF.bendsource · line 22 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102, 111, 111]) == "Zm9v" : String}

A complete three-byte group has no padding.

law encode_multiple provedin PROOF.bendsource · line 26 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102, 111, 111, 98, 97, 114]) == "Zm9vYmFy" : String}

Multiple groups concatenate without separators.

law encode_masks_u32 provedin PROOF.bendsource · line 34 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([256]) == "AA==" : String}

Elements are octet-oriented: the low eight bits are encoded.

law decode_empty provedin PROOF.bendsource · line 38 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("") == Some{[]} : Maybe<&2, List<&2, U32>>}

Empty Base64 decodes to an empty list.

law decode_one_pad provedin PROOF.bendsource · line 42 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zg==") == Some{[102]} : Maybe<&2, List<&2, U32>>}

One padded quartet decodes to one octet.

law decode_two_pad provedin PROOF.bendsource · line 46 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zm8=") == Some{[102, 111]} : Maybe<&2, List<&2, U32>>}

Two padded quartet decodes to two octets.

law decode_full provedin PROOF.bendsource · line 50 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zm9v") == Some{[102, 111, 111]} : Maybe<&2, List<&2, U32>>}

An unpadded quartet decodes to three octets.

law decode_multiple provedin PROOF.bendsource · line 57 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zm9vYmFy") == Some{[102, 111, 111, 98, 97, 114]} : Maybe<&2, List<&2, U32>>}

Multiple quartets concatenate in input order.

law roundtrip_one provedin PROOF.bendsource · line 65 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode(0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102])) == Some{[102]} : Maybe<&2, List<&2, U32>>}

Canonical examples round-trip through both public functions.

law roundtrip_two provedin PROOF.bendsource · line 72 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode(0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102, 111])) == Some{[102, 111]} : Maybe<&2, List<&2, U32>>}

law roundtrip_three provedin PROOF.bendsource · line 79 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode(0xd9193642e70279e288909ba354d1bb6a/lib.Base64.encode([102, 111, 111])) == Some{[102, 111, 111]} : Maybe<&2, List<&2, U32>>}

law reject_invalid_alphabet provedin PROOF.bendsource · line 87 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("not!") == None{} : Maybe<&2, List<&2, U32>>}

Invalid alphabet characters are rejected.

law reject_short_quartet provedin PROOF.bendsource · line 91 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zg=") == None{} : Maybe<&2, List<&2, U32>>}

A non-multiple-of-four length is rejected.

law reject_early_padding provedin PROOF.bendsource · line 95 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Z=g=") == None{} : Maybe<&2, List<&2, U32>>}

Padding cannot appear before the final two positions.

law reject_bad_padding_shape provedin PROOF.bendsource · line 99 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zg=A") == None{} : Maybe<&2, List<&2, U32>>}

One '=' requires a real third sextet and two '=' require c='='.

law reject_noncanonical_one provedin PROOF.bendsource · line 103 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zh==") == None{} : Maybe<&2, List<&2, U32>>}

Nonzero unused bits are rejected rather than silently normalized.

law reject_noncanonical_two provedin PROOF.bendsource · line 106 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zm/=") == None{} : Maybe<&2, List<&2, U32>>}

law reject_padding_before_tail provedin PROOF.bendsource · line 110 · raw

{0xd9193642e70279e288909ba354d1bb6a/lib.Base64.decode("Zg==AAAA") == None{} : Maybe<&2, List<&2, U32>>}

Padding is allowed only in the final quartet.