proofs/containers/doubly_linked_list/ok.bend

bend-collections-laws-containers@1.0.0.0 · 17 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/doubly_linked_list.bend as S
4import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
6
7# The refinement statement of one step: the implementation's result is the
8# real list of a new shadow with an observation, the specification's the
9# shadow's model with the same observation, and the shadow is good.
10
11def POK(~T: Data, -X: Data, spec: S.DS<T> & X, r: D.DList<T> & X) -> Type:
12  Sigma<&1, &1, ST.Sh<T>, sh2 => Sigma<&1, &1, X, o => {r == (ST.real(~T, sh2), o) : D.DList<T> & X} & ({spec == (ST.model(~T, sh2), o) : S.DS<T> & X} & {ST.good(~T, sh2) == True{} : Bool})>>
13
14# both results rewritten
15def pok_eq(~T: Data, -X: Data, -spec: S.DS<T> & X, -spec2: S.DS<T> & X, -r: D.DList<T> & X, -r2: D.DList<T> & X, +es: {spec == spec2 : S.DS<T> & X}, +er: {r == r2 : D.DList<T> & X}, p: POK(~T, X, spec2, r2)) -> POK(~T, X, spec, r):
16  p1 = L.subst(D.DList<T> & X, z => POK(~T, X, spec2, z), r2, r, Equal.sym(D.DList<T> & X, r, r2, er), p)
17  L.subst(S.DS<T> & X, z => POK(~T, X, z, r), spec2, spec, Equal.sym(S.DS<T> & X, spec, spec2, es), p1)