~/bend-docscommunity

LAWS.bend open laws/TODOs

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

Executable laws for the strict, lowercase Hex codec. Decode accepts exactly pairs of 0-9a-fA-F and returns canonical octets.

2 imports
import Base
import ./lib.bend as Hx

Laws

law encode_empty provedin PROOF.bendsource · line 7 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([]) == "" : String}

Empty and ordinary encoding.

law encode_zero provedin PROOF.bendsource · line 10 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([0]) == "00" : String}

law encode_one provedin PROOF.bendsource · line 13 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([1]) == "01" : String}

law encode_ten provedin PROOF.bendsource · line 16 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([10]) == "0a" : String}

law encode_fifteen provedin PROOF.bendsource · line 19 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([15]) == "0f" : String}

law encode_sixteen provedin PROOF.bendsource · line 22 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([16]) == "10" : String}

law encode_sevenf provedin PROOF.bendsource · line 25 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([127]) == "7f" : String}

law encode_ff provedin PROOF.bendsource · line 28 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([255]) == "ff" : String}

law encode_masks_u32 provedin PROOF.bendsource · line 32 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([256]) == "00" : String}

Encoding follows the companion Bytes.hex low-octet convention.

law encode_multiple provedin PROOF.bendsource · line 35 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([0, 10, 255]) == "000aff" : String}

law decode_empty provedin PROOF.bendsource · line 39 · raw

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

Empty and lowercase/uppercase input decoding.

law decode_zero provedin PROOF.bendsource · line 42 · raw

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

law decode_lowercase provedin PROOF.bendsource · line 45 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("0aff") == Some{[10, 255]} : Maybe<&2, List<&2, U32>>}

law decode_uppercase provedin PROOF.bendsource · line 48 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("0AFF") == Some{[10, 255]} : Maybe<&2, List<&2, U32>>}

law decode_mixed_case provedin PROOF.bendsource · line 51 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("aB0c") == Some{[171, 12]} : Maybe<&2, List<&2, U32>>}

law decode_multiple provedin PROOF.bendsource · line 54 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("000aff7f") == Some{[0, 10, 255, 127]} : Maybe<&2, List<&2, U32>>}

law roundtrip_empty provedin PROOF.bendsource · line 58 · raw

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

Canonical lowercase encodings round-trip.

law roundtrip_one provedin PROOF.bendsource · line 61 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode(0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([1])) == Some{[1]} : Maybe<&2, List<&2, U32>>}

law roundtrip_multiple provedin PROOF.bendsource · line 64 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode(0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.encode([0, 10, 127, 128, 255])) == Some{[0, 10, 127, 128, 255]} : Maybe<&2, List<&2, U32>>}

law reject_odd_length provedin PROOF.bendsource · line 72 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("a") == None{} : Maybe<&2, List<&2, U32>>}

Strict rejection: odd length, invalid alphabet, and non-hex punctuation.

law reject_three_chars provedin PROOF.bendsource · line 75 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("abc") == None{} : Maybe<&2, List<&2, U32>>}

law reject_invalid_g provedin PROOF.bendsource · line 78 · raw

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

law reject_invalid_prefix provedin PROOF.bendsource · line 81 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("0x") == None{} : Maybe<&2, List<&2, U32>>}

law reject_whitespace provedin PROOF.bendsource · line 84 · raw

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

law reject_prefix provedin PROOF.bendsource · line 87 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("0x0a") == None{} : Maybe<&2, List<&2, U32>>}

law reject_bad_tail provedin PROOF.bendsource · line 90 · raw

{0xf941a081d658b4ed09b0d1c5a3d26f48/lib.Hex.decode("00zz") == None{} : Maybe<&2, List<&2, U32>>}