proofs/containers/deque/stepok.bend

bend-collections-laws-containers@1.0.0.0 · 15 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/deque.bend as S
3import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as ST
6
7# StepOK(sh, op): the public step on the deque of shadow sh lands on the
8# deque of a shadow sh2 and emits o, and (model(sh2), o) is exactly the spec
9# step on model(sh).
10
11def StepOK(~T: Data, sh: ST.Shadow<T>, op: E.Op<T>) -> Type:
12  Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {DQ.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DQ.Deque<T> & E.Obs<T>} & {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs<T>}>>
13
14def mk(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, sh2: ST.Shadow<T>, o: E.Obs<T>, e1: {DQ.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : DQ.Deque<T> & E.Obs<T>}, e2: {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs<T>}) -> StepOK(~T, sh, op):
15  (sh2, (o, (e1, e2)))