LAWS.bend open laws/TODOs
raw source on the hub · import 0x99e32f5f97dad3791a32b01d133555c5/LAWS.bend as LAWS
SPDX-License-Identifier: MIT-0
3 imports
import Base import ./main.bend as M import ./fixtures.bend as F
Laws
law path_empty provedin PROOF.bendsource · line 7 · raw
@-V:Data -> @+path:List<&2, Bool> -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, 0x99e32f5f97dad3791a32b01d133555c5/main.Tip{}) == None{} : Maybe<&2, V>}Universal structural path theorems; these have no preconditions.
law path_set provedin PROOF.bendsource · line 12 · raw
@-V:Data -> @+path:List<&2, Bool> -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+v:V -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, 0x99e32f5f97dad3791a32b01d133555c5/main.set_path(V, path, m, key, v)) == Some{v} : Maybe<&2, V>}
law branch_low provedin PROOF.bendsource · line 21 · raw
@-V:Data -> @+lo:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+hi:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> {0x99e32f5f97dad3791a32b01d133555c5/main.low(V, 0x99e32f5f97dad3791a32b01d133555c5/main.branch(V, lo, hi)) == lo : 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V>}Auxiliary projection lemmas for pruning; not behavior claims on their own.
law branch_high provedin PROOF.bendsource · line 27 · raw
@-V:Data -> @+lo:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+hi:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> {0x99e32f5f97dad3791a32b01d133555c5/main.high(V, 0x99e32f5f97dad3791a32b01d133555c5/main.branch(V, lo, hi)) == hi : 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V>}
law path_remove provedin PROOF.bendsource · line 33 · raw
@-V:Data -> @+path:List<&2, Bool> -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, 0x99e32f5f97dad3791a32b01d133555c5/main.remove_path(V, path, m)) == None{} : Maybe<&2, V>}
law empty_get provedin PROOF.bendsource · line 40 · raw
@-V:Data -> @+key:U32 -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.empty(V), key) == None{} : Maybe<&2, V>}Public universal theorems quantify over every U32, value, and map.
law set_get provedin PROOF.bendsource · line 45 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+v:V -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.set(V, m, key, v), key) == Some{v} : Maybe<&2, V>}
law remove_get provedin PROOF.bendsource · line 52 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.remove(V, m, key), key) == None{} : Maybe<&2, V>}
law set_contains provedin PROOF.bendsource · line 58 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+v:V -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.contains(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.set(V, m, key, v), key) == True{} : Bool}
law overwrite provedin PROOF.bendsource · line 65 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+old:V -> @+v:V -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.set(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.set(V, m, key, old), key, v), key) == Some{v} : Maybe<&2, V>}
law path_preserve provedin PROOF.bendsource · line 88 · raw
@-V:Data -> @+p:List<&2, Bool> -> @+q:List<&2, Bool> -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+v:V -> @distinct:separated(p, q) -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, q, 0x99e32f5f97dad3791a32b01d133555c5/main.set_path(V, p, m, key, v)) == 0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, q, m) : Maybe<&2, V>}
law set_preserves provedin PROOF.bendsource · line 98 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+other:U32 -> @+v:V -> @distinct:separated(0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, key), 0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, other)) -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.set(V, m, key, v), other) == 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, m, other) : Maybe<&2, V>}
law distinct_witness provedin PROOF.bendsource · line 107 · raw
separated(0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, 0), 0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, 2147483648))
law boundary_fixture provedin PROOF.bendsource · line 111 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.boundary == True{} : Bool}Concrete normalization witness, not a universally quantified theorem.
law fold_fixture provedin PROOF.bendsource · line 115 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.order_case == True{} : Bool}Concrete normalization witness, not a universally quantified theorem.
law union_fixture provedin PROOF.bendsource · line 119 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.unions == True{} : Bool}Concrete normalization witness, not a universally quantified theorem.
law invocation_fixture provedin PROOF.bendsource · line 123 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.trace_case == True{} : Bool}Concrete normalization witness, not a universally quantified theorem.
law model_union_fixture provedin PROOF.bendsource · line 127 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.union_model == True{} : Bool}Concrete normalization witness, not a universally quantified theorem.
law observe_low provedin PROOF.bendsource · line 131 · raw
@-V:Data -> @+path:List<&2, Bool> -> @+lo:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+hi:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, 0x99e32f5f97dad3791a32b01d133555c5/main.low(V, 0x99e32f5f97dad3791a32b01d133555c5/main.branch(V, lo, hi))) == 0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, lo) : Maybe<&2, V>}Auxiliary observation lemmas for pruned branches.
law observe_high provedin PROOF.bendsource · line 138 · raw
@-V:Data -> @+path:List<&2, Bool> -> @+lo:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+hi:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, 0x99e32f5f97dad3791a32b01d133555c5/main.high(V, 0x99e32f5f97dad3791a32b01d133555c5/main.branch(V, lo, hi))) == 0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, path, hi) : Maybe<&2, V>}
law path_remove_preserve provedin PROOF.bendsource · line 145 · raw
@-V:Data -> @+p:List<&2, Bool> -> @+q:List<&2, Bool> -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @distinct:separated(p, q) -> {0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, q, 0x99e32f5f97dad3791a32b01d133555c5/main.remove_path(V, p, m)) == 0x99e32f5f97dad3791a32b01d133555c5/main.get_path(V, q, m) : Maybe<&2, V>}
law remove_preserves provedin PROOF.bendsource · line 153 · raw
@-V:Data -> @+m:0x99e32f5f97dad3791a32b01d133555c5/main.IntMap<V> -> @+key:U32 -> @+other:U32 -> @distinct:separated(0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, key), 0x99e32f5f97dad3791a32b01d133555c5/main.bits(32n, other)) -> {0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.remove(V, m, key), other) == 0x99e32f5f97dad3791a32b01d133555c5/main.IntMap.get(V, m, other) : Maybe<&2, V>}
law fold_seed_fixture provedin PROOF.bendsource · line 162 · raw
{0x99e32f5f97dad3791a32b01d133555c5/fixtures.fold_seed_case == True{} : Bool}Concrete normalization: exact fold contents include the retained seed.
Definitions
def separated source · line 74 · raw
@p:List<&2, Bool> -> @q:List<&2, Bool> -> Data
Constructive domain: Unit at first differing bit, Empty for prefix/equal paths.