proofs/containers/balanced_search_tree/ins.bend
bend-collections-laws-containers@1.0.0.0 · 62 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
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/ord.bend as OR
9
10# Insertion at a gap of a sorted list: the specification's ins puts the
11# entry there, lookup misses, and order holds; the node and payload lists
12# grown by a slot or rewritten at one. (source: tools/generators/tm_hand/ins.src)
13
14
15def ins_nil(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +ys: List<&2, M.Entry<K, V>>, +hg: {OR.gtall(~K, ~V, ~cmp, k, ys) == True{} : Bool}) -> {S.ins(~K, ~V, ~cmp, k, v, ys) == Con{M.Entry{k, v}, ys} : List<&2, M.Entry<K, V>>}:
16 match ys:
17 case Nil{}:
18 {==}
19 case Con{+e, +t}:
20 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, O.lt_is(cmp(k, S.key(K, V, e)), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), hg))) : {S.pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(_), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)}) == Con{M.Entry{k, v}, Con{e, t}} : List<&2, M.Entry<K, V>>}
21 {==}
22
23# inserting k between the entries below and above it
24def ins_gap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +v: V, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +hl: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, k, ys) == True{} : Bool}) -> {S.ins(~K, ~V, ~cmp, k, v, SC.append(M.Entry<K, V>, xs, ys)) == SC.append(M.Entry<K, V>, xs, Con{M.Entry{k, v}, ys}) : List<&2, M.Entry<K, V>>}:
25 match xs:
26 case Nil{}:
27 ins_nil(~K, ~V, ~cmp, k, v, ys, hg)
28 case Con{+e, +t}:
29 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, OR.lt_gt(~K, ~cmp, ~o, S.key(K, V, e), k, L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hl))) : {S.pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(_), Con{M.Entry{k, v}, Con{e, SC.append(M.Entry<K, V>, t, ys)}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, SC.append(M.Entry<K, V>, t, ys))}) == Con{e, SC.append(M.Entry<K, V>, t, Con{M.Entry{k, v}, ys})} : List<&2, M.Entry<K, V>>}
30 %Equal.sym(List<&2, M.Entry<K, V>>, S.ins(~K, ~V, ~cmp, k, v, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, t, Con{M.Entry{k, v}, ys}), ins_gap(~K, ~V, ~cmp, ~o, k, v, t, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hl), hg)) : {Con{e, _} == Con{e, SC.append(M.Entry<K, V>, t, Con{M.Entry{k, v}, ys})} : List<&2, M.Entry<K, V>>}
31 {==}
32
33# k is found neither below nor above it
34def find_gap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +hl: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, k, ys) == True{} : Bool}) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == None{} : Maybe<&2, M.Entry<K, V>>}:
35 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)), OR.orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.find_e(~K, ~V, ~cmp, k, ys)), OR.find_app(~K, ~V, ~cmp, k, xs, ys)) : {_ == None{} : Maybe<&2, M.Entry<K, V>>}
36 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, xs), None{}, OR.lt_none(~K, ~V, ~cmp, ~o, k, xs, hl)) : {OR.orm(M.Entry<K, V>, _, S.find_e(~K, ~V, ~cmp, k, ys)) == None{} : Maybe<&2, M.Entry<K, V>>}
37 OR.gt_none(~K, ~V, ~cmp, k, ys, hg)
38
39def ord_cons(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, ys) == True{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, S.key(K, V, e), ys) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, Con{e, ys}) == True{} : Bool}:
40 match ys:
41 case Nil{}:
42 {==}
43 case Con{+e2, +u}:
44 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, u}), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), OR.gtall(~K, ~V, ~cmp, S.key(K, V, e), u), hg), h)
45
46def ord_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +a: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +hae: {Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))) == True{} : Bool}, +h: {ST.ordered(~K, ~V, ~cmp, Con{a, SC.append(M.Entry<K, V>, t, ys)}) == True{} : Bool}, +ih: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, t, Con{e, ys})) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, Con{a, SC.append(M.Entry<K, V>, t, Con{e, ys})}) == True{} : Bool}:
47 match t:
48 case Nil{}:
49 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), ST.ordered(~K, ~V, ~cmp, Con{e, ys}), hae, ih)
50 case Con{+b, +u}:
51 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, b))), ST.ordered(~K, ~V, ~cmp, Con{b, SC.append(M.Entry<K, V>, u, Con{e, ys})}), L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, b))), ST.ordered(~K, ~V, ~cmp, Con{b, SC.append(M.Entry<K, V>, u, ys)}), h), ih)
52
53# an entry between the entries below and above it keeps the order
54def ord_ins(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}, +hl: {OR.ltall(~K, ~V, ~cmp, S.key(K, V, e), xs) == True{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, S.key(K, V, e), ys) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}:
55 match xs:
56 case Nil{}:
57 ord_cons(~K, ~V, ~cmp, e, ys, h, hg)
58 case Con{+a, +t}:
59 +ht = OR.ord_tail(~K, ~V, ~cmp, a, SC.append(M.Entry<K, V>, t, ys), h)
60 +ih = ord_ins(~K, ~V, ~cmp, ~o, t, e, ys, ht, L.and_right(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), OR.ltall(~K, ~V, ~cmp, S.key(K, V, e), t), hl), hg)
61 ord_step(~K, ~V, ~cmp, a, t, e, ys, L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), OR.ltall(~K, ~V, ~cmp, S.key(K, V, e), t), hl), h, ih)
62