proofs/containers/doubly_linked_list/ok.bend source

proofs/containers/doubly_linked_list/ok.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../../spec/containers/doubly_linked_list.bend as Simport ../../../src/containers/doubly_linked_list.bend as Dimport ./state.bend as ST# The refinement statement of one step: the implementation's result is the# real list of a new shadow with an observation, the specification's the# shadow's model with the same observation, and the shadow is good.def POK(~T: Data, -X: Data, spec: S.DS<T> & X, r: D.DList<T> & X) -> Type:  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})>># both results rewrittendef 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):  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)  L.subst(S.DS<T> & X, z => POK(~T, X, z, r), spec2, spec, Equal.sym(S.DS<T> & X, spec, spec2, es), p1)