proofs/containers/balanced_search_tree/ok.bend checks

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

6 imports

import Base
import ../../lib/logic.bend as L
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI

Templates

template POK source · line 13 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X) -> Type

template pok_eq source · line 16 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @-spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @-spec2:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X) -> @-r2:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X) -> @+es:{spec == spec2 : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X)} -> @+er:{r == r2 : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X)} -> @p:POK(K, V, cmp, X, spec2, r2) -> POK(K, V, cmp, X, spec, r)

template dg_good source · line 21 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.dg(K, V, sh) == True{} : Bool}

the layout facts the simulation needs, from the invariant

template pok_read source · line 27 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+o:X -> @-spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X) -> @+es:{spec == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X)} -> @+er:{r == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X)} -> POK(K, V, cmp, X, spec, r)

a read-only operation: the same shadow, the answer of both

template MOK source · line 32 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, X) -> Type

the refinement of a mirror result: its real map and answer are a good shadow's, whose model and the answer are the specification's

template mok_eq source · line 35 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @-spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @-mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, X) -> @-mir2:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, X) -> @+e:{mir == mir2 : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, X)} -> @p:MOK(K, V, cmp, X, spec, mir2) -> MOK(K, V, cmp, X, spec, mir)

template mok_pok source · line 39 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @-spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>, X) -> @-mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, X) -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X) -> @+hs:{r == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rp(K, V, cmp, X, mir) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, X)} -> @p:MOK(K, V, cmp, X, spec, mir) -> POK(K, V, cmp, X, spec, r)

a mirror refinement and the simulation give the implementation's