~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law to_words_empty provedin PROOF.bendsource · line 5 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_words(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty) == [] : List<&2, U32>}

Empty is represented by no words.

law is_empty_empty provedin PROOF.bendsource · line 8 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.is_empty(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty) == True{} : Bool}

law size_empty provedin PROOF.bendsource · line 11 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.size(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty) == 0n : Nat}

law to_list_empty provedin PROOF.bendsource · line 14 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty) == [] : List<&2, Nat>}

law contains_empty provedin PROOF.bendsource · line 17 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.contains(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 0n) == False{} : Bool}

law singleton_zero_words provedin PROOF.bendsource · line 21 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_words(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n)) == [1] : List<&2, U32>}

The lowest bit is the first singleton.

law singleton_zero_list provedin PROOF.bendsource · line 24 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n)) == [0n] : List<&2, Nat>}

law singleton_zero_size provedin PROOF.bendsource · line 27 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.size(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n)) == 1n : Nat}

law singleton_zero_contains provedin PROOF.bendsource · line 30 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.contains(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0n) == True{} : Bool}

law remove_singleton_zero provedin PROOF.bendsource · line 33 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.remove(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law insert_singleton_idempotent provedin PROOF.bendsource · line 36 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.insert(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law union_empty_singleton provedin PROOF.bendsource · line 40 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.union(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n)) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law intersect_empty_singleton provedin PROOF.bendsource · line 44 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.intersect(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n)) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law singleton_one_words provedin PROOF.bendsource · line 49 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_words(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(1n)) == [2] : List<&2, U32>}

Small boundary cases exercise the word layout.

law singleton_one_list provedin PROOF.bendsource · line 52 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(1n)) == [1n] : List<&2, Nat>}

law singleton_thirty_one provedin PROOF.bendsource · line 55 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(31n)) == [31n] : List<&2, Nat>}

law singleton_thirty_two_words provedin PROOF.bendsource · line 58 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_words(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n)) == [0, 1] : List<&2, U32>}

law singleton_thirty_two_list provedin PROOF.bendsource · line 61 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n)) == [32n] : List<&2, Nat>}

law contains_absent_singleton provedin PROOF.bendsource · line 64 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.contains(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 1n) == False{} : Bool}

law insert_zero_empty provedin PROOF.bendsource · line 67 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.insert(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 0n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law insert_thirty_two_empty provedin PROOF.bendsource · line 70 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.insert(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 32n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law remove_absent_empty provedin PROOF.bendsource · line 74 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.remove(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 32n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law remove_other_singleton provedin PROOF.bendsource · line 77 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.remove(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 1n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law remove_one_from_two provedin PROOF.bendsource · line 81 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.remove(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.insert(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 1n), 0n) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(1n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law union_two_bits provedin PROOF.bendsource · line 85 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_list(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.union(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(1n))) == [0n, 1n] : List<&2, Nat>}

law union_across_words provedin PROOF.bendsource · line 89 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.to_words(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.union(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n))) == [1, 1] : List<&2, U32>}

law intersect_disjoint provedin PROOF.bendsource · line 93 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.intersect(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n), 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(1n)) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law intersect_same provedin PROOF.bendsource · line 97 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.intersect(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n), 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n)) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law from_words_trims_zero_tail provedin PROOF.bendsource · line 101 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.from_words([1, 0]) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.from_words([1]) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law from_words_zero_is_empty provedin PROOF.bendsource · line 105 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.from_words([0, 0]) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law u32_singleton_wrapper provedin PROOF.bendsource · line 108 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton_u32(0) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(0n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}

law u32_insert_wrapper provedin PROOF.bendsource · line 111 · raw

{0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.insert_u32(0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.empty, 32) == 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet.singleton(32n) : 0x3b8f9f546e51ef5efc252d01094290fb/lib.BitSet}