proofs/containers/balanced_search_tree/vdef.bend source

proofs/containers/balanced_search_tree/vdef.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./mirror.bend as MIimport ./ok.bend as OK# A view's model and invariant, and the refinement of view results.# (source: tools/generators/tm_hand/vdef.src)# ---- a view's model and invariant ----def vmod(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> S.View<K, V>:  match w:    case MI.MV{s, lo2, hi2, d2}:      S.VW{ST.model(~K, ~V, ~cmp, s), lo2, hi2, d2}def vgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> Bool:  match w:    case MI.MV{s, lo2, hi2, d2}:      ST.good(~K, ~V, ~cmp, s)def 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}:  match w:    case MI.MV{+s, +lo2, +hi2, +d2}:      OK.dg_good(~K, ~V, ~cmp, s, h)# a view refining a specification'sdef VOK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sp: S.View<K, V>, r: M.View<K, V, cmp>) -> Type:  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})># a mirror view result refining a specification'sdef VM(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, sp: S.View<K, V> & X, mir: MI.MView<K, V> & X) -> Type:  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})>># an implementation view result refining a specification'sdef 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:  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})>>def 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):  match p:    case Tuple{+w2, Tuple{+o, Tuple{+h1, rest}}}:      (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)))# a mirror result given exactlydef 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):  (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))))