proofs/containers/balanced_search_tree/mokx.bend
bend-collections-laws-containers@1.0.0.0 · 38 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/spec/containers/balanced_search_tree/main.bend as S
4import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
8
9# A mirror result's answer mapped: a refinement with the value v found
10# gives one with the value's presence (changed_value) or its entry
11# (entry_value). (source: tools/generators/tm_hand/mokx.src)
12
13
14def cv_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +v: V, +sh2: ST.Sh<K, V>, +o: Maybe<&2, V>, +h1: {(ST.real(~K, ~V, ~cmp, m), Some{v}) == (ST.real(~K, ~V, ~cmp, sh2), o) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}, r: {(m0, Some{v}) == (ST.model(~K, ~V, ~cmp, sh2), o) : S.Model<K, V> & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, (m0, True{}), MI.changed_value(~K, ~V, ~cmp, (m, Some{v}))):
15 match r:
16 case Tuple{h2, hg}:
17 +e1 = L.pair_fst(M.TreeMap<K, V, cmp>, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, m), Some{v}, ST.real(~K, ~V, ~cmp, sh2), o, h1)
18 +e2 = L.pair_fst(S.Model<K, V>, Maybe<&2, V>, m0, Some{v}, ST.model(~K, ~V, ~cmp, sh2), o, h2)
19 (sh2, (True{}, (L.pair_eq(M.TreeMap<K, V, cmp>, Bool, ST.real(~K, ~V, ~cmp, m), True{}, ST.real(~K, ~V, ~cmp, sh2), True{}, e1, {==}), (L.pair_eq(S.Model<K, V>, Bool, m0, True{}, ST.model(~K, ~V, ~cmp, sh2), True{}, e2, {==}), hg))))
20
21# the value found: the answer is that something changed
22def cv_mok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +v: V, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (m0, Some{v}), (m, Some{v}))) -> OK.MOK(~K, ~V, ~cmp, Bool, (m0, True{}), MI.changed_value(~K, ~V, ~cmp, (m, Some{v}))):
23 match p:
24 case Tuple{+sh2, Tuple{+o, Tuple{+h1, r}}}:
25 cv_r(~K, ~V, ~cmp, m0, m, v, sh2, o, h1, r)
26
27def ev_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +k: K, +v: V, +sh2: ST.Sh<K, V>, +o: Maybe<&2, V>, +h1: {(ST.real(~K, ~V, ~cmp, m), Some{v}) == (ST.real(~K, ~V, ~cmp, sh2), o) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}, r: {(m0, Some{v}) == (ST.model(~K, ~V, ~cmp, sh2), o) : S.Model<K, V> & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (m0, Some{M.Entry{k, v}}), MI.entry_value(~K, ~V, ~cmp, Some{k}, (m, Some{v}))):
28 match r:
29 case Tuple{h2, hg}:
30 +e1 = L.pair_fst(M.TreeMap<K, V, cmp>, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, m), Some{v}, ST.real(~K, ~V, ~cmp, sh2), o, h1)
31 +e2 = L.pair_fst(S.Model<K, V>, Maybe<&2, V>, m0, Some{v}, ST.model(~K, ~V, ~cmp, sh2), o, h2)
32 (sh2, (Some{M.Entry{k, v}}, (L.pair_eq(M.TreeMap<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, ST.real(~K, ~V, ~cmp, m), Some{M.Entry{k, v}}, ST.real(~K, ~V, ~cmp, sh2), Some{M.Entry{k, v}}, e1, {==}), (L.pair_eq(S.Model<K, V>, Maybe<&2, M.Entry<K, V>>, m0, Some{M.Entry{k, v}}, ST.model(~K, ~V, ~cmp, sh2), Some{M.Entry{k, v}}, e2, {==}), hg))))
33
34# the value found: the answer is its entry
35def ev_mok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +k: K, +v: V, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (m0, Some{v}), (m, Some{v}))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (m0, Some{M.Entry{k, v}}), MI.entry_value(~K, ~V, ~cmp, Some{k}, (m, Some{v}))):
36 match p:
37 case Tuple{+sh2, Tuple{+o, Tuple{+h1, r}}}:
38 ev_r(~K, ~V, ~cmp, m0, m, k, v, sh2, o, h1, r)