proofs/containers/balanced_search_tree/putf.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/putf.bend as Putf
21 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/list.bend as LL import ../../lib/order.bend as O import ../../../spec/lib/common.bend as SC import ../../../spec/containers/balanced_search_tree/main.bend as S import ../../../src/containers/balanced_search_tree.bend as M import ./state.bend as ST import ./tree.bend as TR import ./find.bend as FI import ./path.bend as P import ./prim.bend as PR import ./ord.bend as OR import ./slot.bend as SL import ./alls.bend as AL import ./dj.bend as DJ import ./agree.bend as AG import ./navs.bend as NS import ./spath.bend as SP import ../../lib/nat_list.bend as NL
Definitions
def some_ex_c source · line 61 · raw
@-V:Data -> @+pl:List<&2, Maybe<&2, V>> -> @+i:Nat -> @+w:Maybe<&2, V> -> @+jj:Nat -> @+hj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+jj)) == True{} : Bool} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, w) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, pl)) == b : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(i, jj) == e : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(List<&2, Maybe<&2, V>>, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, pl, i, w), pl), jj, None{})) == True{} : Bool}
def some_ex source · line 75 · raw
@-V:Data -> @+pl:List<&2, Maybe<&2, V>> -> @+id:Nat -> @+w:Maybe<&2, V> -> @+j:Nat -> @+hj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, j)) == True{} : Bool} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/prim.ex_pl(V, pl, id, w), j)) == True{} : Bool}
Templates
template set_val_mid source · line 29 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, xs) == True{} : Bool} -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == EQ{} : Cmp} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, e <> ys)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), v} <> ys) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}setting the value of the entry equal to k
template ord_key source · line 40 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+e2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e2) : K} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, e <> ys)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, e2 <> ys)) == True{} : Bool}order reads only keys
template pay_ex source · line 84 · raw
@-V:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pl:List<&2, Maybe<&2, V>> -> @+id:Nat -> @+w:Maybe<&2, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pay(V, t, pl) == True{} : Bool} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pay(V, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/prim.ex_pl(V, pl, id, w)) == True{} : Bool}
template ents_at source · line 95 · raw
@-K:Data -> @-V:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+q:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hbc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, a, b}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(a)), nl, q), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.cons_m(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ent(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, q, i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c)), nl, q))) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}the entries around a node the path leads to, for a payload list
template hit_core source · line 103 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+k:K -> @+v:V -> @+hbc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, a, b}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, a, b}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), nl) == True{} : Bool} -> @+hfin:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.fin(K, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, a, b}, nl) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+m:Maybe<&2, V> -> @+hxi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i) == x : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hmi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, i) == m : Maybe<&2, V>} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.is_node(K, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c)) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, m) == True{} : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/prim.ex_pl(V, pl, i, Some{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/prim.ex_pl(V, pl, i, Some{v}), tg, fl) == True{} : Bool})the node of k found: exchanging its payload for v gives the entries set_val(k, v) and keeps the invariant