~/bend-docscommunity

proofs/containers/balanced_search_tree/components.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/components.bend as Components

4 imports
import Base
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/dynamic_array.bend as D
import ../../../src/containers/types/dynamic_array.bend as E

Definitions

def empty_size source · line 11 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.size(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Nat)}

def empty_get source · line 14 · raw

@k:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.get(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), k) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), None{}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Maybe<&2, U32>)}

def empty_remove source · line 17 · raw

@k:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.remove(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), k) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), None{}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Maybe<&2, U32>)}

def singleton source · line 20 · raw

@+k:U32 -> @v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>

def put_empty source · line 23 · raw

@+k:U32 -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(U32, U32, U32.cmp), k, v) == (singleton(k, v), Done{None{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<U32, U32>, Maybe<&2, U32>>)}

def zero_get source · line 26 · raw

@+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.get(U32, U32, U32.cmp, singleton(0, v), 0) == (singleton(0, v), Some{v}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Maybe<&2, U32>)}

def zero_replace source · line 29 · raw

@+old:U32 -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put(U32, U32, U32.cmp, singleton(0, old), 0, v) == (singleton(0, v), Done{Some{old}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<U32, U32>, Maybe<&2, U32>>)}

def zero_remove source · line 32 · raw

@+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.remove(U32, U32, U32.cmp, singleton(0, v), 0) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TM{0n, 0n, 0n, 0n, 1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NS{31n, 0n, 1n, 1n, [0n], [0n], [0n], [0n], [None{}]}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{None{}}]}}, Some{v}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Maybe<&2, U32>)}

def reuse_first source · line 35 · raw

@+k:U32 -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TM{0n, 0n, 0n, 0n, 1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NS{31n, 0n, 1n, 1n, [0n], [0n], [0n], [0n], [None{}]}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{None{}}]}}, k, v) == (singleton(k, v), Done{None{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<U32, U32>, Maybe<&2, U32>>)}

def cursor_owns source · line 38 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp> -> @next:Nat -> @current:Nat -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @forward:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_finish(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor{m, next, current, lo, hi, forward}) == m : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>}

def view_owns source · line 41 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp> -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @descending:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_finish(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View{m, lo, hi, descending}) == m : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>}

def set_requires_current source · line 44 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp> -> @+next:Nat -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @+forward:Bool -> @v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_set_value(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor{m, next, 0n, lo, hi, forward}, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor{m, next, 0n, lo, hi, forward}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<U32, U32, U32.cmp>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Error, U32>)}

def rejected_view_put source · line 47 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp> -> @+k:U32 -> @+v:U32 -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<U32> -> @+descending:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_put_checked(U32, U32, U32.cmp, m, k, v, lo, hi, descending, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View{m, lo, hi, descending}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.OutOfRange{}, k, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View<U32, U32, U32.cmp>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<U32, U32>, Maybe<&2, U32>>)}

def data_swap_rejected source · line 50 · raw

@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&2, U32>> -> @i:Nat -> @v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_checked_at(U32, l, d, c, n, a, i, v, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)}

def data_swap_first source · line 53 · raw

@+old:U32 -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_at(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{old}]}, 0n, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{v}]}, Done{old}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)}

def same_class source · line 59 · raw

@a:U32 -> @b:U32 -> Cmp

A valid total preorder whose keys are all comparator-equivalent. This law checks original-key retention for arbitrary different keys and payloads; it is still a singleton law, not an arbitrary-map refinement theorem.

def equivalent_singleton source · line 62 · raw

@+k:U32 -> @v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, same_class>

def equivalent_put_retains_key source · line 65 · raw

@+stored:U32 -> @incoming:U32 -> @+old:U32 -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put(U32, U32, same_class, equivalent_singleton(stored, old), incoming, v) == (equivalent_singleton(stored, v), Done{Some{old}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, same_class>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<U32, U32>, Maybe<&2, U32>>)}

def two_entries source · line 68 · raw

@v0:U32 -> @v1:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<U32, U32, U32.cmp>

def next_after_remove source · line 73 · raw

@r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<U32, U32, U32.cmp>, Maybe<&2, U32>) -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<U32, U32>>

def cursor_remove_preserves_next source · line 77 · raw

@v0:U32 -> @+v1:U32 -> {next_after_remove(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_remove(U32, U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor{two_entries(v0, v1), 2n, 1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Unbounded{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Unbounded{}, True{}})) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{1, v1}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<U32, U32>>}