proofs/containers/balanced_search_tree/life.bend
bend-collections-laws-containers@1.0.0.0 · 35 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
6import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
9
10# The empty map: the shadow with no nodes is good at any limit and depth
11# within bounds; new and with_limit build it, and its model is the
12# specification's empty map. (source: tools/generators/tm_hand/life.src)
13
14
15def good_empty(~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}) -> {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}:
16 ST.good_intro(~K, ~V, ~cmp, 0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}, hcl, hcd, N.zero_le(SC.pow2(d)), {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==})
17
18def new_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.new(~K, ~V, ~cmp) : M.TreeMap<K, V, cmp>} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.new(K, V) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
19 ({==}, ({==}, good_empty(~K, ~V, ~cmp, 31n, 0n, {==}, {==})))
20
21
22def wl_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: Nat, +b: Bool, +hb: {Nat.is_lt(k, 31n) == b : Bool}) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, b), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.TM{0n, 0n, 0n, 0n, 0n, M.NS{D.clamp_limit(k, b), 0n, 1n, 0n, M.ns_nats(0n), M.ns_nats(0n), M.ns_nats(0n), M.ns_nats(0n), M.ns_nokeys(~K, 0n)}, D.DA{D.clamp_limit(k, b), 0n, 1n, 0n, D.empty_slots_at(~Maybe<&2, V>, 0n)}} : M.TreeMap<K, V, cmp>} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, b), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.TM{S.pick(Nat, b, k, 31n), Nil{}} : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, b), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
23 match b:
24 case True{}:
25 ({==}, ({==}, good_empty(~K, ~V, ~cmp, k, 0n, N.lt_le(k, 31n, hb), N.zero_le(k))))
26 case False{}:
27 ({==}, ({==}, good_empty(~K, ~V, ~cmp, 31n, 0n, {==}, {==})))
28
29# with_limit: the limit clamped to 31
30def with_limit_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: Nat) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.with_limit(~K, ~V, ~cmp, k) : M.TreeMap<K, V, cmp>} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.with_limit(K, V, k) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
31 wl_c(~K, ~V, ~cmp, k, Nat.is_lt(k, 31n), {==})
32
33# clearing: the same limit and depth, no nodes
34def clear_ok(~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, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}) -> {ST.real(~K, ~V, ~cmp, MI.clear(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : M.TreeMap<K, V, cmp>} & ({S.clear(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
35 ({==}, ({==}, good_empty(~K, ~V, ~cmp, l, d, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))