LAWS.bend source
LAWS.bend on the hub · documented module
import Baseimport ./lib.bend as By# to_list(empty) is Nil.law to_list_empty: { By.Bytes.to_list(By.Bytes.empty()) == Nil{} : List<&2, U32> }# empty is B{Nil}.law empty_is_b_nil: { By.Bytes.empty() == By.B{Nil{}} : By.Bytes }# to_list undoes the B encoding.law to_list_b: for xs: List<&2, U32> { By.Bytes.to_list(By.B{xs}) == xs : List<&2, U32> }# from_list is the B constructor.law from_list_b: for xs: List<&2, U32> { By.Bytes.from_list(xs) == By.B{xs} : By.Bytes }# to_list ∘ from_list is identity on the underlying list.law to_list_from_list: for xs: List<&2, U32> { By.Bytes.to_list(By.Bytes.from_list(xs)) == xs : List<&2, U32> }# from_list ∘ to_list is identity on Bytes.law from_list_to_list: for xs: List<&2, U32> { By.Bytes.from_list(By.Bytes.to_list(By.B{xs})) == By.B{xs} : By.Bytes }# singleton packs a one-element list.law to_list_singleton: for +x: U32 { By.Bytes.to_list(By.Bytes.singleton(x)) == x <> Nil{} : List<&2, U32> }# singleton is B{x <> Nil}.law singleton_is_b: for +x: U32 { By.Bytes.singleton(x) == By.B{x <> Nil{}} : By.Bytes }# length(empty) is 0.law length_empty: { By.Bytes.length(By.Bytes.empty()) == 0n : Nat }# length(B{xs}) is List.length(xs).law length_b: for xs: List<&2, U32> { By.Bytes.length(By.B{xs}) == List.length(&2, U32, xs) : Nat }# length(singleton(x)) is 1.law length_singleton: for +x: U32 { By.Bytes.length(By.Bytes.singleton(x)) == 1n : Nat }# get(empty, 0) is None.law get_empty_zero: { By.Bytes.get(By.Bytes.empty(), 0n) == None{} : Maybe<&2, U32> }# get(singleton(x), 0) recovers x.law get_singleton_zero: for +x: U32 { By.Bytes.get(By.Bytes.singleton(x), 0n) == Some{x} : Maybe<&2, U32> }# get(singleton(x), 1) is None.law get_singleton_one: for +x: U32 { By.Bytes.get(By.Bytes.singleton(x), 1n) == None{} : Maybe<&2, U32> }# append unwraps to List.append.law to_list_append: for xs: List<&2, U32> for ys: List<&2, U32> { By.Bytes.to_list(By.Bytes.append(By.B{xs}, By.B{ys})) == List.append(&2, U32, xs, ys) : List<&2, U32> }# append(empty, bs) leaves bs unchanged (via to_list).law append_empty_left: for xs: List<&2, U32> { By.Bytes.to_list(By.Bytes.append(By.Bytes.empty(), By.B{xs})) == xs : List<&2, U32> }# Definitional form of append(bs, empty) (needs List.append_nil for identity).law append_empty_right_def: for xs: List<&2, U32> { By.Bytes.to_list(By.Bytes.append(By.B{xs}, By.Bytes.empty())) == List.append(&2, U32, xs, Nil{}) : List<&2, U32> }# append of two singletons.law append_singletons: for +x: U32 for +y: U32 { By.Bytes.to_list(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y))) == x <> (y <> Nil{}) : List<&2, U32> }# length(append(empty, B{xs})) is List.length(xs).law length_append_empty_left: for xs: List<&2, U32> { By.Bytes.length(By.Bytes.append(By.Bytes.empty(), By.B{xs})) == List.length(&2, U32, xs) : Nat }# get on append of singletons.law get_append_singletons_zero: for +x: U32 for +y: U32 { By.Bytes.get(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y)), 0n) == Some{x} : Maybe<&2, U32> }law get_append_singletons_one: for +x: U32 for +y: U32 { By.Bytes.get(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y)), 1n) == Some{y} : Maybe<&2, U32> }# reverse unwraps to List.reverse.law to_list_reverse: for xs: List<&2, U32> { By.Bytes.to_list(By.Bytes.reverse(By.B{xs})) == List.reverse(&2, U32, xs) : List<&2, U32> }# reverse(empty) is empty.law reverse_empty: { By.Bytes.to_list(By.Bytes.reverse(By.Bytes.empty())) == Nil{} : List<&2, U32> }# reverse(singleton(x)) is singleton(x).law reverse_singleton: for +x: U32 { By.Bytes.to_list(By.Bytes.reverse(By.Bytes.singleton(x))) == x <> Nil{} : List<&2, U32> }# eq(empty, empty) is True.law eq_empty: { By.Bytes.eq(By.Bytes.empty(), By.Bytes.empty()) == True{} : Bool }# eq(empty, singleton(x)) is False.law eq_empty_singleton: for +x: U32 { By.Bytes.eq(By.Bytes.empty(), By.Bytes.singleton(x)) == False{} : Bool }# eq of distinct concrete singletons is False.law eq_singleton_diff: { By.Bytes.eq(By.Bytes.singleton(1), By.Bytes.singleton(2)) == False{} : Bool }# hex(empty) is "".law hex_empty: { By.Bytes.hex(By.Bytes.empty()) == "" : String }# hex(singleton(0)) is "00".law hex_byte_zero: { By.Bytes.hex(By.Bytes.singleton(0)) == "00" : String }# hex(singleton(255)) is "ff".law hex_byte_ff: { By.Bytes.hex(By.Bytes.singleton(255)) == "ff" : String }# hex(singleton(10)) is "0a".law hex_byte_0a: { By.Bytes.hex(By.Bytes.singleton(10)) == "0a" : String }# hex(singleton(16)) is "10".law hex_byte_10: { By.Bytes.hex(By.Bytes.singleton(16)) == "10" : String }# hex(singleton(127)) is "7f".law hex_byte_7f: { By.Bytes.hex(By.Bytes.singleton(127)) == "7f" : String }# hex of two bytes concatenates.law hex_two_bytes: { By.Bytes.hex(By.Bytes.append(By.Bytes.singleton(0), By.Bytes.singleton(255))) == "00ff" : String }