~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law to_list_empty provedin PROOF.bendsource · line 5 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty) == [] : List<&2, U32>}

to_list(empty) is Nil.

law empty_is_b_nil provedin PROOF.bendsource · line 9 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty == 0xc6de6e524c84b0784158389ee44fd48f/lib.B{[]} : 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes}

empty is B{Nil}.

law to_list_b provedin PROOF.bendsource · line 13 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs}) == xs : List<&2, U32>}

to_list undoes the B encoding.

law from_list_b provedin PROOF.bendsource · line 18 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.from_list(xs) == 0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs} : 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes}

from_list is the B constructor.

law to_list_from_list provedin PROOF.bendsource · line 23 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.from_list(xs)) == xs : List<&2, U32>}

to_list ∘ from_list is identity on the underlying list.

law from_list_to_list provedin PROOF.bendsource · line 28 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.from_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs})) == 0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs} : 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes}

from_list ∘ to_list is identity on Bytes.

law to_list_singleton provedin PROOF.bendsource · line 33 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x)) == [x] : List<&2, U32>}

singleton packs a one-element list.

law singleton_is_b provedin PROOF.bendsource · line 38 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x) == 0xc6de6e524c84b0784158389ee44fd48f/lib.B{[x]} : 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes}

singleton is B{x <> Nil}.

law length_empty provedin PROOF.bendsource · line 43 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.length(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty) == 0n : Nat}

length(empty) is 0.

law length_b provedin PROOF.bendsource · line 47 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.length(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs}) == List.length(&2, U32, xs) : Nat}

length(B{xs}) is List.length(xs).

law length_singleton provedin PROOF.bendsource · line 52 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.length(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x)) == 1n : Nat}

length(singleton(x)) is 1.

law get_empty_zero provedin PROOF.bendsource · line 57 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.get(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty, 0n) == None{} : Maybe<&2, U32>}

get(empty, 0) is None.

law get_singleton_zero provedin PROOF.bendsource · line 61 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.get(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x), 0n) == Some{x} : Maybe<&2, U32>}

get(singleton(x), 0) recovers x.

law get_singleton_one provedin PROOF.bendsource · line 66 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.get(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x), 1n) == None{} : Maybe<&2, U32>}

get(singleton(x), 1) is None.

law to_list_append provedin PROOF.bendsource · line 71 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs}, 0xc6de6e524c84b0784158389ee44fd48f/lib.B{ys})) == List.append(&2, U32, xs, ys) : List<&2, U32>}

append unwraps to List.append.

law append_empty_left provedin PROOF.bendsource · line 81 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty, 0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs})) == xs : List<&2, U32>}

append(empty, bs) leaves bs unchanged (via to_list).

law append_empty_right_def provedin PROOF.bendsource · line 90 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs}, 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty)) == List.append(&2, U32, xs, []) : List<&2, U32>}

Definitional form of append(bs, empty) (needs List.append_nil for identity).

law append_singletons provedin PROOF.bendsource · line 99 · raw

@+x:U32 -> @+y:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x), 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(y))) == [x, y] : List<&2, U32>}

append of two singletons.

law length_append_empty_left provedin PROOF.bendsource · line 109 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.length(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty, 0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs})) == List.length(&2, U32, xs) : Nat}

length(append(empty, B{xs})) is List.length(xs).

law get_append_singletons_zero provedin PROOF.bendsource · line 118 · raw

@+x:U32 -> @+y:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.get(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x), 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(y)), 0n) == Some{x} : Maybe<&2, U32>}

get on append of singletons.

law get_append_singletons_one provedin PROOF.bendsource · line 127 · raw

@+x:U32 -> @+y:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.get(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x), 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(y)), 1n) == Some{y} : Maybe<&2, U32>}

law to_list_reverse provedin PROOF.bendsource · line 137 · raw

@xs:List<&2, U32> -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.reverse(0xc6de6e524c84b0784158389ee44fd48f/lib.B{xs})) == List.reverse(&2, U32, xs) : List<&2, U32>}

reverse unwraps to List.reverse.

law reverse_empty provedin PROOF.bendsource · line 146 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.reverse(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty)) == [] : List<&2, U32>}

reverse(empty) is empty.

law reverse_singleton provedin PROOF.bendsource · line 150 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.to_list(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.reverse(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x))) == [x] : List<&2, U32>}

reverse(singleton(x)) is singleton(x).

law eq_empty provedin PROOF.bendsource · line 159 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.eq(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty, 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty) == True{} : Bool}

eq(empty, empty) is True.

law eq_empty_singleton provedin PROOF.bendsource · line 163 · raw

@+x:U32 -> {0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.eq(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty, 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(x)) == False{} : Bool}

eq(empty, singleton(x)) is False.

law eq_singleton_diff provedin PROOF.bendsource · line 168 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.eq(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(1), 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(2)) == False{} : Bool}

eq of distinct concrete singletons is False.

law hex_empty provedin PROOF.bendsource · line 172 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.empty) == "" : String}

hex(empty) is "".

law hex_byte_zero provedin PROOF.bendsource · line 176 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(0)) == "00" : String}

hex(singleton(0)) is "00".

law hex_byte_ff provedin PROOF.bendsource · line 180 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(255)) == "ff" : String}

hex(singleton(255)) is "ff".

law hex_byte_0a provedin PROOF.bendsource · line 184 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(10)) == "0a" : String}

hex(singleton(10)) is "0a".

law hex_byte_10 provedin PROOF.bendsource · line 188 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(16)) == "10" : String}

hex(singleton(16)) is "10".

law hex_byte_7f provedin PROOF.bendsource · line 192 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(127)) == "7f" : String}

hex(singleton(127)) is "7f".

law hex_two_bytes provedin PROOF.bendsource · line 196 · raw

{0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.hex(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.append(0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(0), 0xc6de6e524c84b0784158389ee44fd48f/lib.Bytes.singleton(255))) == "00ff" : String}

hex of two bytes concatenates.