~/bend-docscommunity

proofs/containers/balanced_search_tree/life.bend checks

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

8 imports
import Base
import ../../lib/nat.bend as N
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 ../../../src/containers/dynamic_array.bend as D
import ./state.bend as ST
import ./mirror.bend as MI

Templates

template good_empty source · line 15 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+d:Nat -> @+hcl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hcd:{Nat.is_le(d, l) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, l, d, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}

template new_ok source · line 18 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(K, V, cmp) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.new(K, V) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))

template wl_c source · line 22 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(k, 31n) == b : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TM{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NS{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 0n, 1n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_nats(0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_nats(0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_nats(0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_nats(0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_nokeys(K, 0n)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 0n, 1n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_slots_at(Maybe<&2, V>, 0n)}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Nat, b, k, 31n), []} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))

template with_limit_ok source · line 30 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:Nat -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.with_limit(K, V, cmp, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.with_limit(K, V, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))

with_limit: the limit clamped to 31

template clear_ok source · line 34 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_: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} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.clear(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, l, d, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.clear(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, l, d, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, l, d, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))

clearing: the same limit and depth, no nodes