proofs/containers/balanced_search_tree/vdef.bend
bend-collections-laws-containers@1.0.0.0 · 50 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 view's model and invariant, and the refinement of view results.
10# (source: tools/generators/tm_hand/vdef.src)
11
12
13# ---- a view's model and invariant ----
14
15def vmod(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> S.View<K, V>:
16 match w:
17 case MI.MV{s, lo2, hi2, d2}:
18 S.VW{ST.model(~K, ~V, ~cmp, s), lo2, hi2, d2}
19
20def vgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> Bool:
21 match w:
22 case MI.MV{s, lo2, hi2, d2}:
23 ST.good(~K, ~V, ~cmp, s)
24
25def vg_dg(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +h: {vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> {MI.dgv(K, V, w) == True{} : Bool}:
26 match w:
27 case MI.MV{+s, +lo2, +hi2, +d2}:
28 OK.dg_good(~K, ~V, ~cmp, s, h)
29
30# a view refining a specification's
31def VOK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sp: S.View<K, V>, r: M.View<K, V, cmp>) -> Type:
32 Sigma<&1, &1, MI.MView<K, V>, w2 => {r == MI.rv(~K, ~V, ~cmp, w2) : M.View<K, V, cmp>} & ({sp == vmod(~K, ~V, ~cmp, w2) : S.View<K, V>} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>
33
34# a mirror view result refining a specification's
35def VM(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, sp: S.View<K, V> & X, mir: MI.MView<K, V> & X) -> Type:
36 Sigma<&1, &1, MI.MView<K, V>, w2 => Sigma<&1, &1, X, o => {MI.rvp(~K, ~V, ~cmp, X, mir) == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X} & ({sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>>
37
38# an implementation view result refining a specification's
39def VPOK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, sp: S.View<K, V> & X, r: M.View<K, V, cmp> & X) -> Type:
40 Sigma<&1, &1, MI.MView<K, V>, w2 => Sigma<&1, &1, X, o => {r == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X} & ({sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>>
41
42def vm_pok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, -sp: S.View<K, V> & X, -mir: MI.MView<K, V> & X, -r: M.View<K, V, cmp> & X, +hs: {r == MI.rvp(~K, ~V, ~cmp, X, mir) : M.View<K, V, cmp> & X}, p: VM(~K, ~V, ~cmp, X, sp, mir)) -> VPOK(~K, ~V, ~cmp, X, sp, r):
43 match p:
44 case Tuple{+w2, Tuple{+o, Tuple{+h1, rest}}}:
45 (w2, (o, (Equal.trans(M.View<K, V, cmp> & X, r, MI.rvp(~K, ~V, ~cmp, X, mir), (MI.rv(~K, ~V, ~cmp, w2), o), hs, h1), rest)))
46
47# a mirror result given exactly
48def vm_exact(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, -sp: S.View<K, V> & X, -mir: MI.MView<K, V> & X, +w2: MI.MView<K, V>, +o: X, +hm: {mir == (w2, o) : MI.MView<K, V> & X}, +hs: {sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X}, +hg: {vgood(~K, ~V, ~cmp, w2) == True{} : Bool}) -> VM(~K, ~V, ~cmp, X, sp, mir):
49 (w2, (o, (L.subst(MI.MView<K, V> & X, z => {MI.rvp(~K, ~V, ~cmp, X, z) == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X}, (w2, o), mir, Equal.sym(MI.MView<K, V> & X, mir, (w2, o), hm), {==}), (hs, hg))))
50