proofs/containers/balanced_search_tree/alloc.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/alloc.bend as Alloc
25 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 ./mirror.bend as MI import ./ok.bend as OK import ./reads.bend as RD import ./path.bend as P import ./plug.bend as PG import ./agree.bend as AG import ./prim.bend as PR import ./frame.bend as FR import ./ord.bend as OR import ./ins.bend as INS import ./slot.bend as SL import ./alls.bend as AL import ./dj.bend as DJ import ./spath.bend as SP import ./insf.bend as IF import ../../lib/nat_list.bend as NL
Definitions
def fl_nil source · line 33 · raw
@+fl:List<&2, Nat> -> @+n:Nat -> @+h0:{0n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(fl) : Nat} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(fl, n) == True{} : Bool} -> {fl == [] : List<&2, Nat>}
Templates
template spec_rej source · line 42 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+l:Nat -> @+n: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 -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+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/proofs/containers/balanced_search_tree/path.after(c)) : List<&2, Nat>} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> @+hsz:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) : Nat} -> @+hfull:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, k, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.CapacityExceeded{}, k, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)}the specification rejects at the capacity
template app_case source · line 52 · 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 -> @+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, 0n, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+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/proofs/containers/balanced_search_tree/path.after(c)) : List<&2, Nat>} -> @+hplug:{tg == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, c, 0n, nl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> @+room:Bool -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, nl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == room : Bool} -> @+grow:Bool -> @+hgw:{Nat.is_lt(d, l) == grow : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.MOK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, 0n, l, d, nl, pl, tg, fl}), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.put_allocated(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.dir(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.app_room(K, V, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, k, v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), room, grow)))appending: into room, growing the block, or rejected at the capacity
template reuse_case source · line 125 · 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 -> @+f: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, 1n+f, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+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/proofs/containers/balanced_search_tree/path.after(c)) : List<&2, Nat>} -> @+hplug:{tg == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, c, 0n, nl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+f) == y : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.MOK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, 1n+f, l, d, nl, pl, tg, fl}), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.put_allocated(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.dir(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.alloc_read(K, V, cmp, 1n+f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), k, v, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, 1n+f, l, d, nl, pl, tg, fl}, y))))