Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use

`Ctrl+↑``Ctrl+↓`to navigate,`Ctrl+🖱️`to focus.Require Import Helpers.Helpers. Require Import Proc. Require Import ProcTheorems.

The Coq standard library requires us to explicitly import support
for printing strings. This is used to display hints in the proof
context about where the proof goal came from.

Require Import String. Export String.StringSyntax.

# Specification style: Abstractions with pre- and post-conditions

- You need to define an abstraction relation that connects code
states and spec states;
- Whenever the code runs from state w to state w' and the abstraction relation holds between w and state, you must show that there exists a spec state state' for which the abstraction relation holds between w' and state', and that the specification allows the procedure to change the abstract state from state to state'.

spec semantics forall state ===================> exists state' ^ ^^ absR | absR || V semantics of code VV forall w -----------------------> forall w'

A LayerAbstraction is a record with one field, abstraction,
which relates two states: one of type State1 and another of type State2.
Think of State1 as being the type of code states whereas State2 is the
type for specification states. The abstraction relation links these two
states together.
For example, in StatDB lab, the spec state is a list of
integers and the implementation state is is a pair of variables. In the
StatDB lab, the
abstraction function must state what must be true of the relationship between
the list of integers and the pair of variables.

```
Record LayerAbstraction State1 State2 :=
{ abstraction : State1 -> State2 -> Prop; }.
```

The above definition of LayerAbstraction helps us connect two
layers, such as the layer of variables and the layer of the StatDB
specification.
A particular kind of abstraction is one that connects the bottom-most
type of state, world, with some abstract state above the world.
(Recall that our model of execution is that, at the lowest level,
procedures (code) always manipulates the "real world", whose state
is of type world.)
We define Abstraction to be this particular kind of abstraction:
it is a relation between world states and some other type of states,
State.

`Definition Abstraction State := LayerAbstraction world State.`

We can compose abstractions, by layering one abstraction on top
of another. In our case, since everything is ultimately connected
to world states at the bottom, we define a composition of two
kinds of abstraction: one that goes from world states to State1,
and another that goes from State1 to State2, to produce an
abstraction from world to State2.
abstraction_compose makes this connection precise, by saying
that world and State2 states are connected by the fact that
there exists some intermediate State1 state that matches the
two abstractions being composed.

```
Definition abstraction_compose
`(abs1: Abstraction State1)
`(abs2: LayerAbstraction State1 State2) :=
{| abstraction := fun w state' => exists state, abstraction abs2 state state' /\
abstraction abs1 w state; |}.
```

In some situations, we will want to keep the same level of abstraction
(i.e., have the code and spec states be the same). IdAbstraction
defines this "identity" kind of abstraction: it is a relation between
states of the same type State, and the relation says that the two
states must be equal.

```
Definition IdAbstraction State : LayerAbstraction State State :=
{| abstraction := fun state state' => state' = state; |}.
```

Our specifications describe how a procedure can change the
state of the system, at some level of abstraction. We describe
the allowed state changes using pre- and post-conditions, as
captured by the following structure, SpecProps.
SpecProps is parametrized by three types: T, R, and State.
State is the type of states that this specification uses.
For instance, in the StatDB example, State would be list nat.
T is the type of the return value of the procedure being
specified. Note that the post condition is a function of
two arguments: one of type T (the returned value), and another
of type State (the resulting state).
In addition to pre- and post-conditions, our specifications include
recovery conditions, which help reason about crashes during the
execution of a procedure. After a crash, a recovery procedure will
run to recover any state from the crash. The recovery procedure may
also return some result; this result's type is R, and the recovery
condition, recovered, takes two arguments: the return value from
recovery, R, and the state after recovery, State.

```
Record SpecProps T R State :=
Spec {
pre: Prop;
post: T -> State -> Prop;
recovered: R -> State -> Prop;
}.
```

One obvious part missing from the SpecProps specification is any
reference to the starting state. The reason we didn't pass it as
an argument to the precondition, pre, is that it's useful to refer
to the starting state inside the post and recovered conditions
as well, in order to connect the final state to the starting state.
Another part which is not so obviously missing is a way to talk about
existential variables in the specification (sometimes called "ghost
variables" in the PL literature). This is a bit hard to
grasp in an abstract sense; we will use this in lab 4, and it's safe
to ignore it until then.
We add these two missing parts to a specification by defining the
actual type of specifications, Specification, as a function from
a ghost variable A and a starting state State to a SpecProps.
This allows the pre-, post-, and recovered conditions in SpecProps
to refer to the starting state (and the ghost variable).

`Definition Specification A T R State := A -> State -> SpecProps T R State.`

## Correctness of a procedure

pre post | || V VV state state' ^ ^^ absR | absR || V VV w ---[procedure p]-----> w'

- assume that the abstraction relation holds between w and state
- assume that the precondition holds for a and state
- if the procedure p starts from code state w, then one of the
following must be true:
- (1) if execution finishes without crashes in code state w' and
returns v, then there exists a spec state state' in which the
abstraction relation holds between w' and state' and the
postcondition holds in state' with return value v, OR
- (2) if execution finishes in code state w' and returns v (after perhaps several crashes and running the recovery procedure r on each crash), then there exists a spec state state' and some return value v from the recovery procedure, in which the abstraction relation holds between w' and state' and the recovered condition holds in state' with return value v.

- (1) if execution finishes without crashes in code state w' and
returns v, then there exists a spec state state' in which the
abstraction relation holds between w' and state' and the
postcondition holds in state' with return value v, OR

```
Definition proc_spec `(spec: Specification A T R State) `(p: proc T)
`(rec: proc R)
`(abs: Abstraction State) :=
forall a w state,
abstraction abs w state ->
pre (spec a state) ->
forall r, rexec p rec w r ->
match r with
| RFinished v w' => exists state',
abstraction abs w' state' /\
post (spec a state) v state'
| Recovered v w' => exists state',
abstraction abs w' state' /\
recovered (spec a state) v state'
end.
```

To help us construct proofs about procedures satisfying
a specification, it helps to have a notion of when one
specification implies another specification. Here, we
define what it means for spec1 to imply spec2 (the
two specifications must be at the same level of abstraction
and must talk about the same types of return values):

- for all ghost variables and all states state for which spec2's
precondition holds,
- there exists a ghost variable for which spec1's precondition
holds in state
- for all states state' in which the postcondition of spec1
holds, then the post condition of spec2 also holds
- for all states state' in which the recovered condition of spec1 holds, then the recovered condition of spec2 also holds.

```
Definition spec_impl
`(spec1: Specification A' T R State)
`(spec2: Specification A T R State) :=
forall a state, pre (spec2 a state) ->
exists a', pre (spec1 a' state) /\
(forall v state', post (spec1 a' state) v state' ->
post (spec2 a state) v state') /\
(forall rv state', recovered (spec1 a' state) rv state' ->
recovered (spec2 a state) rv state').
```

We now prove that the above definition of what it means for
one specification to imply another one is actually correct.
This means that, if a procedure satisfies spec1, and spec1
implies spec2, then the same procedure must also satisfy spec2.

forall (A T R State : Type) (spec1 : Specification A T R State) (A' : Type) (spec2 : Specification A' T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), proc_spec spec1 p rec abs -> spec_impl spec1 spec2 -> proc_spec spec2 p rec absforall (A T R State : Type) (spec1 : Specification A T R State) (A' : Type) (spec2 : Specification A' T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), proc_spec spec1 p rec abs -> spec_impl spec1 spec2 -> proc_spec spec2 p rec absA, T, R, State:Typespec1:Specification A T R StateA':Typespec2:Specification A' T R Statep:proc Trec:proc Rabs:Abstraction StateH:proc_spec spec1 p rec absH0:spec_impl spec1 spec2a:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec2 a state)r:RResult T RH3:rexec p rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec2 a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec2 a state) v state' endA, T, R, State:Typespec1:Specification A T R StateA':Typespec2:Specification A' T R Statep:proc Trec:proc Rabs:Abstraction StateH:proc_spec spec1 p rec absH0:spec_impl spec1 spec2a:A'w:worldstate:StateH1:abstraction abs w statea':AH2:pre (spec1 a' state)H4:forall (v : T) (state' : State), post (spec1 a' state) v state' -> post (spec2 a state) v state'H5:forall (rv : R) (state' : State), recovered (spec1 a' state) rv state' -> recovered (spec2 a state) rv state'r:RResult T RH3:rexec p rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec2 a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec2 a state) v state' enddestruct r; simpl in *; repeat deex; intuition eauto. Qed. Hint Resolve tt : core.A, T, R, State:Typespec1:Specification A T R StateA':Typespec2:Specification A' T R Statep:proc Trec:proc Rabs:Abstraction StateH:proc_spec spec1 p rec absH0:spec_impl spec1 spec2a:A'w:worldstate:StateH1:abstraction abs w statea':AH2:pre (spec1 a' state)H4:forall (v : T) (state' : State), post (spec1 a' state) v state' -> post (spec2 a state) v state'H5:forall (rv : R) (state' : State), recovered (spec1 a' state) rv state' -> recovered (spec2 a state) rv state'r:RResult T RH3:match r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec1 a' state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec1 a' state) v state' endmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec2 a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec2 a state) v state' end

We are about to introduce machinery for constructing proofs of
correctness by considering a procedure one step at a time. This will
generate multiple sub-goals for you to prove. To help you keep track
of where these goals are coming from, we introduce the Marker type.
A Marker is a logical statement that's always true (it has exactly
one constructor, mark, that has no additional requirements), so
formally speaking, it carries no new logical facts. Marker takes two
arguments: a string s and a procedure p. The reason the Marker
is useful is that it allows the lab infrastructure to introduce Marker
statements in the proof context, where the string s and procedure
p provide a hint about what led to any particular sub-goal.

Inductive Marker (s:string) {T} (p: proc T) : Prop := | mark. Hint Resolve mark : core. (* re-state proc_spec_weaken in a more automation-friendly way *)forall (A T R State : Type) (spec1 : Specification A T R State) (A' : Type) (spec2 : Specification A' T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), (Marker "using spec for" p -> proc_spec spec1 p rec abs) -> (forall (a : A') (state : State), pre (spec2 a state) -> exists a' : A, pre (spec1 a' state) /\ (forall (v : T) (state' : State), post (spec1 a' state) v state' -> post (spec2 a state) v state') /\ (forall (rv : R) (state' : State), recovered (spec1 a' state) rv state' -> recovered (spec2 a state) rv state')) -> proc_spec spec2 p rec absforall (A T R State : Type) (spec1 : Specification A T R State) (A' : Type) (spec2 : Specification A' T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), (Marker "using spec for" p -> proc_spec spec1 p rec abs) -> (forall (a : A') (state : State), pre (spec2 a state) -> exists a' : A, pre (spec1 a' state) /\ (forall (v : T) (state' : State), post (spec1 a' state) v state' -> post (spec2 a state) v state') /\ (forall (rv : R) (state' : State), recovered (spec1 a' state) rv state' -> recovered (spec2 a state) rv state')) -> proc_spec spec2 p rec absA, T, R, State:Typespec1:Specification A T R StateA':Typespec2:Specification A' T R Statep:proc Trec:proc Rabs:Abstraction StateH:Marker "using spec for" p -> proc_spec spec1 p rec absH0:forall (a : A') (state : State), pre (spec2 a state) -> exists a' : A, pre (spec1 a' state) /\ (forall (v : T) (state' : State), post (spec1 a' state) v state' -> post (spec2 a state) v state') /\ (forall (rv : R) (state' : State), recovered (spec1 a' state) rv state' -> recovered (spec2 a state) rv state')proc_spec spec2 p rec abseapply proc_spec_weaken; eauto. Qed.A, T, R, State:Typespec1:Specification A T R StateA':Typespec2:Specification A' T R Statep:proc Trec:proc Rabs:Abstraction StateH:Marker "using spec for" p -> proc_spec spec1 p rec absH0:spec_impl spec1 spec2proc_spec spec2 p rec abs

This is a crucial step for constructing proofs of correctness.
We will decompose proofs about a Bind operation (i.e.,
combining two procedures, p and rx, with a semicolon) into
smaller proofs about the individual procedures p and rx.
Specifically, in order to prove that p; rx satisfies spec',
it suffices to have some specification spec for p, and to
prove that the precondition of spec' implies the precondition
of spec, and that rx meets a specification that, informally,
fixes up the postcondition of spec to match the postcondition
of spec'.
More precisely:

forall (A T R State : Type) (spec : Specification A T R State) (p : proc T) (rec : proc R) (T' : Type) (rx : T -> proc T') (A' : Type) (spec' : Specification A' T' R State) (abs : Abstraction State), proc_spec spec p rec abs -> (forall (a' : A') (state : State), pre (spec' a' state) -> exists a : A, (Marker "precondition" p -> pre (spec a state)) /\ (forall (r : R) (state' : State), recovered (spec a state) r state' -> Marker "recovered condition" p -> recovered (spec' a' state) r state') /\ (forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a' state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a' state) r0 state'' |}) (rx r) rec abs)) -> proc_spec spec' (x <- p; rx x) rec absforall (A T R State : Type) (spec : Specification A T R State) (p : proc T) (rec : proc R) (T' : Type) (rx : T -> proc T') (A' : Type) (spec' : Specification A' T' R State) (abs : Abstraction State), proc_spec spec p rec abs -> (forall (a' : A') (state : State), pre (spec' a' state) -> exists a : A, (Marker "precondition" p -> pre (spec a state)) /\ (forall (r : R) (state' : State), recovered (spec a state) r state' -> Marker "recovered condition" p -> recovered (spec' a' state) r state') /\ (forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a' state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a' state) r0 state'' |}) (rx r) rec abs)) -> proc_spec spec' (x <- p; rx x) rec absA, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absH0:forall (a' : A') (state : State), pre (spec' a' state) -> exists a : A, (Marker "precondition" p -> pre (spec a state)) /\ (forall (r : R) (state' : State), recovered (spec a state) r state' -> Marker "recovered condition" p -> recovered (spec' a' state) r state') /\ (forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a' state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a' state) r0 state'' |}) (rx r) rec abs)a:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)r:RResult T' RH3:rexec (x <- p; rx x) rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec' a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec' a state) v state' endA, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absH0:forall (a' : A') (state : State), pre (spec' a' state) -> exists a : A, (Marker "precondition" p -> pre (spec a state)) /\ (forall (r : R) (state' : State), recovered (spec a state) r state' -> Marker "recovered condition" p -> recovered (spec' a' state) r state') /\ (forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a' state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a' state) r0 state'' |}) (rx r) rec abs)a:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)v:T'w':worldH4:exec (x <- p; rx x) w (Finished v w')exists state' : State, abstraction abs w' state' /\ post (spec' a state) v state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absH0:forall (a' : A') (state : State), pre (spec' a' state) -> exists a : A, (Marker "precondition" p -> pre (spec a state)) /\ (forall (r : R) (state' : State), recovered (spec a state) r state' -> Marker "recovered condition" p -> recovered (spec' a' state) r state') /\ (forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a' state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a' state) r0 state'' |}) (rx r) rec abs)a:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH4:exec (x <- p; rx x) w (Crashed w')H5:exec_recover rec (world_crash w') rv w''exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)v:T'w':worldH4:exec (x <- p; rx x) w (Finished v w')exists state' : State, abstraction abs w' state' /\ post (spec' a state) v state'match goal with | [ Hexec: exec p _ _ |- _ ] => eapply RExec in Hexec end. eapply H0 in H2; repeat deex.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)v:T'w':worldv0:Tw'0:worldH9:exec p w (Finished v0 w'0)H11:exec (rx v0) w'0 (Finished v w')exists state' : State, abstraction abs w' state' /\ post (spec' a state) v state'match goal with | [ Hexec: exec (rx _) _ _ |- _ ] => eapply RExec in Hexec; eapply H4 in Hexec; eauto end.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w statea0:AH2:pre (spec a0 state)H3:forall (r : R) (state' : State), recovered (spec a0 state) r state' -> Marker "recovered condition" p -> recovered (spec' a state) r state'H4:forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a0 state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a state) r0 state'' |}) (rx r) rec absv:T'w':worldv0:Tw'0:worldH11:exec (rx v0) w'0 (Finished v w')state':StateH5:abstraction abs w'0 state'H6:post (spec a0 state) v0 state'exists state' : State, abstraction abs w' state' /\ post (spec' a state) v state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH4:exec (x <- p; rx x) w (Crashed w')H5:exec_recover rec (world_crash w') rv w''exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:Tw'0:worldH10:exec p w (Finished v w'0)H12:exec (rx v) w'0 (Crashed w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'state:Statew':worldH1:abstraction abs w' stateH2:pre (spec' a state)rv:Rw'':worldH5:exec_recover rec (world_crash w') rv w''exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:T'H9:exec (x <- p; rx x) w (Finished v w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''H10:exec p w (Crashed w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'match goal with | [ Hexec: exec p _ _ |- _ ] => eapply RExec in Hexec end. eapply H0 in H2; repeat deex.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:Tw'0:worldH10:exec p w (Finished v w'0)H12:exec (rx v) w'0 (Crashed w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'match goal with | [ Hexec: exec (rx _) _ _ |- _ ] => eapply RExecCrash in Hexec; eauto; eapply H4 in Hexec; eauto end.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w statea0:AH2:pre (spec a0 state)H3:forall (r : R) (state' : State), recovered (spec a0 state) r state' -> Marker "recovered condition" p -> recovered (spec' a state) r state'H4:forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a0 state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a state) r0 state'' |}) (rx r) rec absrv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:Tw'0:worldH12:exec (rx v) w'0 (Crashed w')state':StateH6:abstraction abs w'0 state'H7:post (spec a0 state) v state'exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'state:Statew':worldH1:abstraction abs w' stateH2:pre (spec' a state)rv:Rw'':worldH5:exec_recover rec (world_crash w') rv w''exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'state:Statew':worldH1:abstraction abs w' stateH2:pre (spec' a state)rv:Rw'':worldH5:exec_recover rec (world_crash w') rv w''Hexec:exec p w' (Crashed w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'state:Statew':worldH1:abstraction abs w' stateH2:pre (spec' a state)rv:Rw'':worldH5:exec_recover rec (world_crash w') rv w''Hexec:rexec p rec w' (Recovered rv w'')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'eapply H in Hexec; simpl in *; safe_intuition (repeat deex; eauto).A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'state:Statew':worldH1:abstraction abs w' statea0:AH2:Marker "precondition" p -> pre (spec a0 state)H3:forall (r : R) (state' : State), recovered (spec a0 state) r state' -> Marker "recovered condition" p -> recovered (spec' a state) r state'H4:forall r : T, Marker "after" p -> proc_spec (fun (_ : unit) (state' : State) => {| pre := post (spec a0 state) r state'; post := fun (r' : T') (state'' : State) => post (spec' a state) r' state''; recovered := fun (r0 : R) (state'' : State) => recovered (spec' a state) r0 state'' |}) (rx r) rec absrv:Rw'':worldH5:exec_recover rec (world_crash w') rv w''Hexec:rexec p rec w' (Recovered rv w'')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:T'H9:exec (x <- p; rx x) w (Finished v w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'match goal with | [ Hexec: exec p _ _ |- _ ] => eapply RExec in Hexec end. eapply H0 in H2; repeat deex.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:T'v0:Tw'0:worldH10:exec p w (Finished v0 w'0)H12:exec (rx v0) w'0 (Finished v w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'match goal with | [ Hexec: exec (rx _) _ _ |- _ ] => apply ExecCrashEnd in Hexec; eapply RExecCrash in Hexec; eauto; eapply H4 in Hexec; eauto end.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w statea0:AH2:pre (spec a0 state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''v:T'v0:Tw'0:worldH12:exec (rx v0) w'0 (Finished v w')state':StateH6:abstraction abs w'0 state'H7:post (spec a0 state) v0 state'exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''H10:exec p w (Crashed w')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w stateH2:pre (spec' a state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''H10:rexec p rec w (Recovered rv w'')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'eapply H in H10; simpl in *; safe_intuition (repeat deex; eauto). Qed.A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc RT':Typerx:T -> proc T'A':Typespec':Specification A' T' R Stateabs:Abstraction StateH:proc_spec spec p rec absa:A'w:worldstate:StateH1:abstraction abs w statea0:AH2:Marker "precondition" p -> pre (spec a0 state)rv:Rw'', w':worldH5:exec_recover rec (world_crash w') rv w''H10:rexec p rec w (Recovered rv w'')exists state' : State, abstraction abs w'' state' /\ recovered (spec' a state) rv state'

In some situations, the precondition of a specification
may define variables or facts that you want to intros.
Here we define several helper theorems and an Ltac tactic, spec_intros,
that does so. This is done by changing the specification's precondition
from an arbitrary Prop (i.e., pre) into a statement that there's
some state state0 such that state = state0, and introsing the
arbitrary Prop in question as a hypothesis about state0.

forall (A T R State : Type) (spec : Specification A T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), (forall (a : A) (state0 : State), pre (spec a state0) -> proc_spec (fun (_ : unit) (state : State) => {| pre := state = state0; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}) p rec abs) -> proc_spec spec p rec absforall (A T R State : Type) (spec : Specification A T R State) (p : proc T) (rec : proc R) (abs : Abstraction State), (forall (a : A) (state0 : State), pre (spec a state0) -> proc_spec (fun (_ : unit) (state : State) => {| pre := state = state0; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}) p rec abs) -> proc_spec spec p rec absA, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc Rabs:Abstraction StateH:forall (a : A) (state0 : State), pre (spec a state0) -> proc_spec (fun (_ : unit) (state : State) => {| pre := state = state0; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}) p rec absa:Aw:worldstate:StateH0:abstraction abs w stateH1:pre (spec a state)r:RResult T RH2:rexec p rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' endA, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc Rabs:Abstraction StateH:forall (a : A) (state0 : State), pre (spec a state0) -> proc_spec (fun (_ : unit) (state : State) => {| pre := state = state0; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}) p rec absa:Aw:worldstate:StateH0:abstraction abs w stateH1:proc_spec (fun (_ : unit) (state0 : State) => {| pre := state0 = state; post := fun (r : T) (state' : State) => post (spec a state0) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state0) r state' |}) p rec absr:RResult T RH2:rexec p rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' endsimpl in *; eauto. Qed. Ltac spec_intros := intros; eapply spec_intros; intros; cbn [pre post recovered] in *. Ltac spec_case pf := eapply proc_spec_weaken; [ solve [ apply pf ] | unfold spec_impl ].A, T, R, State:Typespec:Specification A T R Statep:proc Trec:proc Rabs:Abstraction StateH:forall (a : A) (state0 : State), pre (spec a state0) -> proc_spec (fun (_ : unit) (state : State) => {| pre := state = state0; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}) p rec absa:Aw:worldstate:StateH0:abstraction abs w stateH1:proc_spec (fun (_ : unit) (state0 : State) => {| pre := state0 = state; post := fun (r : T) (state' : State) => post (spec a state0) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state0) r state' |}) p rec absr:RResult T RH2:rexec p rec w rpre {| pre := state = state; post := fun (r : T) (state' : State) => post (spec a state) r state'; recovered := fun (r : R) (state' : State) => recovered (spec a state) r state' |}

Finally, we prove that our notion of equivalent procedures,
exec_equiv, is actually correct: if p and p' are equivalent,
then they meet the same specifications.
We will use this next to reason about procedure transformations
that shouldn't change the behavior of a procedure.

forall (A T R State : Type) (spec : Specification A T R State) (p p' : proc T) (rec : proc R) (abs : Abstraction State), exec_equiv p p' -> proc_spec spec p' rec abs -> proc_spec spec p rec absforall (A T R State : Type) (spec : Specification A T R State) (p p' : proc T) (rec : proc R) (abs : Abstraction State), exec_equiv p p' -> proc_spec spec p' rec abs -> proc_spec spec p rec absA, T, R, State:Typespec:Specification A T R Statep, p':proc Trec:proc Rabs:Abstraction StateH:exec_equiv p p'H0:forall (a : A) (w : world) (state : State), abstraction abs w state -> pre (spec a state) -> forall r : RResult T R, rexec p' rec w r -> match r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' enda:Aw:worldstate:StateH1:abstraction abs w stateH2:pre (spec a state)r:RResult T RH3:rexec p rec w rmatch r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' endA, T, R, State:Typespec:Specification A T R Statep, p':proc Trec:proc Rabs:Abstraction StateH:exec_equiv p p'H0:forall (a : A) (w : world) (state : State), abstraction abs w state -> pre (spec a state) -> forall r : RResult T R, rexec p' rec w r -> match r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' enda:Aw:worldstate:StateH1:abstraction abs w stateH2:pre (spec a state)r:RResult T RH3:rexec p rec w rrexec p' rec w rsymmetry; auto. Qed.A, T, R, State:Typespec:Specification A T R Statep, p':proc Trec:proc Rabs:Abstraction StateH:exec_equiv p p'H0:forall (a : A) (w : world) (state : State), abstraction abs w state -> pre (spec a state) -> forall r : RResult T R, rexec p' rec w r -> match r with | RFinished v w' => exists state' : State, abstraction abs w' state' /\ post (spec a state) v state' | Recovered v w' => exists state' : State, abstraction abs w' state' /\ recovered (spec a state) v state' enda:Aw:worldstate:StateH1:abstraction abs w stateH2:pre (spec a state)r:RResult T RH3:rexec p rec w rexec_equiv p' p

## Reasoning about the Ret return operation.

```
Definition rec_wipe `(rec: proc R) `(abs: Abstraction State) (wipe: State -> State -> Prop) :=
forall T (v:T),
proc_spec
(fun (_:unit) state =>
{| pre := True;
post := fun r state' => r = v /\
state' = state;
recovered := fun _ state' => wipe state state'; |})
(Ret v) rec abs.
```

A more general theorem about specifications for Ret, which
we will use as part of our proof automation, says
that Ret v meets a specification spec if the rec_wipe
theorem holds (i.e., the recovery procedure is correctly
described by a wipe relation wipe), and the specification
spec matches the wipe relation:

forall (State : Type) (abs : Abstraction State) (wipe : State -> State -> Prop) (A T R : Type) (spec : Specification A T R State) (v : T) (rec : proc R), rec_wipe rec abs wipe -> (forall (a : A) (state : State), pre (spec a state) -> Marker "post" (Ret v) -> post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')) -> proc_spec spec (Ret v) rec absforall (State : Type) (abs : Abstraction State) (wipe : State -> State -> Prop) (A T R : Type) (spec : Specification A T R State) (v : T) (rec : proc R), rec_wipe rec abs wipe -> (forall (a : A) (state : State), pre (spec a state) -> Marker "post" (Ret v) -> post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')) -> proc_spec spec (Ret v) rec absState:Typeabs:Abstraction Statewipe:State -> State -> PropA, T, R:Typespec:Specification A T R Statev:Trec:proc RH:rec_wipe rec abs wipeH0:forall (a : A) (state : State), pre (spec a state) -> Marker "post" (Ret v) -> post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')proc_spec spec (Ret v) rec absState:Typeabs:Abstraction Statewipe:State -> State -> PropA, T, R:Typespec:Specification A T R Statev:Trec:proc RH:rec_wipe rec abs wipeH0:forall (a : A) (state : State), pre (spec a state) -> Marker "post" (Ret v) -> post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')a:Aw:worldstate:StateH1:abstraction abs w stateH2:pre (spec a state)r:RResult T RH3:rexec (Ret v) rec w rState:Typeabs:Abstraction Statewipe:State -> State -> PropA, T, R:Typespec:Specification A T R Statev:Trec:proc RH:rec_wipe rec abs wipeH0:forall (a : A) (state : State), pre (spec a state) -> Marker "post" (Ret v) -> post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')a:Aw:worldstate:StateH1:abstraction abs w stateH2:pre (spec a state)r:RResult T RH3:match r with | RFinished v0 w' => exists state' : State, abstraction abs w' state' /\ v0 = v /\ state' = state | Recovered _ w' => exists state' : State, abstraction abs w' state' /\ wipe state state' enddestruct r; intuition eauto. Qed.State:Typeabs:Abstraction Statewipe:State -> State -> PropA, T, R:Typespec:Specification A T R Statev:Trec:proc RH:rec_wipe rec abs wipea:Aw:worldstate:StateH1:abstraction abs w stateH2:post (spec a state) v state /\ (forall state' : State, wipe state state' -> forall r : R, recovered (spec a state) r state')r:RResult T RH3:match r with | RFinished v0 w' => exists state' : State, abstraction abs w' state' /\ v0 = v /\ state' = state | Recovered _ w' => exists state' : State, abstraction abs w' state' /\ wipe state state' end

## Proof automation

```
Ltac monad_simpl :=
repeat match goal with
| |- proc_spec _ (Bind (Ret _) _) _ _ =>
eapply spec_exec_equiv; [ apply monad_left_id | ]
| |- proc_spec _ (Bind (Bind _ _) _) _ _ =>
eapply spec_exec_equiv; [ apply monad_assoc | ]
end.
```

## step_proc

pre post | | V V state0 --[a]--> state1 --[b]--> state2

- a proc_spec for the a procedure
- a way to line up our current state's precondition with a's proc_spec precondition

- a proc_spec with a procedure that invokes a Ret operation:
if so, apply the ret_spec theorem to consume the Ret. This
will generate some proof obligations, corresponding to the premises
of the ret_spec theorem.
- a proc_spec with a procedure that sequences two operations a and b
(with Bind): if so, apply the proc_spec_rx theorem to consume the
Bind. This will generate some proof obligations, corresponding to
the premises of the proc_spec_rx theorem.
- a proc_spec that is implied by a proc_spec that is already in context: if so, apply the proc_spec_weaken theorem and try to prove that one spec implies the other.

Ltac step_proc_basic := intros; monad_simpl; match goal with | |- proc_spec _ (Ret _) _ _ => eapply ret_spec | |- proc_spec _ _ _ _ => eapply proc_spec_implication; [ solve [eauto] | ] | |- proc_spec _ _ _ _ => eapply proc_spec_rx; [ solve [ eauto ] | ] end; cbn [pre post recovered] in *. Ltac simplify := simpl; repeat match goal with | [ H: _ /\ _ |- _ ] => destruct H | [ |- forall _, _ ] => intros | [ |- rec_wipe _ _ _ ] => solve [ eauto ] | [ |- exists (_:unit), _ ] => exists tt | [ H: pre ((match ?a with | (x, y) => _ end) _) |- _ ] => let x := fresh x in let y := fresh y in destruct a as [x y]; cbn [pre post recovered] in * | _ => progress subst | _ => progress autounfold in * | |- _ /\ _ => split end. Ltac split_all := repeat match goal with | |- _ /\ _ => split end. Ltac finish := repeat match goal with | _ => solve [ trivial ] end. Ltac step_proc := step_proc_basic; simplify; finish.

## Initialization

```
Inductive InitResult :=
| Initialized
| InitFailed.
```

When we compose multiple layers together, a common pattern
that emerges is trying to initialize the lower level first,
and then initializing the higher level. The reason we don't
just combine the procedures using semicolon (i.e., Bind)
is that if the lower-level initialization fails, we should
return failure right away, instead of continuing to run the
higher-level initialization.

```
Definition then_init (init1 init2: proc InitResult) : proc InitResult :=
r <- init1;
match r with
| Initialized => init2
| Failed => Ret Failed
end.
```

## Initialization specs

`Definition inited_any `(s : State) : Prop := True.`

We define this shorthand for the specification of an initialization
procedure. Given a description of the states that initialization
should produce (e.g., inited_any above), init_abstraction produces
a full-fledged pre- and post-condition-style specification, which
says that, if initialization returns success, the resulting state
is one of the allowed states:

```
Definition init_abstraction
(init: proc InitResult) (rec: proc unit)
`(abs: Abstraction State) (init_sem: State -> Prop) :=
proc_spec
(fun (_:unit) w =>
{| pre := True;
post :=
fun r w' => match r with
| Initialized =>
exists state, abstraction abs w' state /\ init_sem state
| InitFailed => True
end;
recovered :=
fun _ w' => True;
|}) init rec (IdAbstraction world).
```

Since the init_abstraction specification above does not
place any requirements in case we crash during initialization,
the specific recovery procedure doesn't matter:

forall (init : proc InitResult) (rec rec' : proc unit) (State : Type) (abs : Abstraction State) (init_sem : State -> Prop), init_abstraction init rec abs init_sem -> init_abstraction init rec' abs init_semforall (init : proc InitResult) (rec rec' : proc unit) (State : Type) (abs : Abstraction State) (init_sem : State -> Prop), init_abstraction init rec abs init_sem -> init_abstraction init rec' abs init_seminit:proc InitResultrec, rec':proc unitState:Typeabs:Abstraction Stateinit_sem:State -> PropH:unit -> forall w state : world, state = w -> True -> forall r : RResult InitResult unit, rexec init rec w r -> match r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state0 : State, abstraction abs state' state0 /\ init_sem state0 | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True enda:unitw, state:worldH0:state = wH1:Truer:RResult InitResult unitH2:rexec init rec' w rmatch r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state : State, abstraction abs state' state /\ init_sem state | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True endeapply rexec_finish_any_rec in H2. eapply H in H2; eauto. Qed.init:proc InitResultrec, rec':proc unitState:Typeabs:Abstraction Stateinit_sem:State -> PropH:unit -> forall w state : world, state = w -> True -> forall r : RResult InitResult unit, rexec init rec w r -> match r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state0 : State, abstraction abs state' state0 /\ init_sem state0 | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True enda:unitw:worldH1:Truew0:worldH2:rexec init rec' w (RFinished Initialized w0)exists state' : world, state' = w0 /\ (exists state : State, abstraction abs state' state /\ init_sem state)

Finally, we prove a specialized theorem about how to compose
two initialization procedures using the then_init composition
operator defined above:

forall (init1 init2 : proc InitResult) (rec rec' : proc unit) (State1 : Type) (abs1 : Abstraction State1) (State2 : Type) (abs2 : LayerAbstraction State1 State2) (init1_sem : State1 -> Prop) (init2_sem : State2 -> Prop), init_abstraction init1 rec abs1 init1_sem -> proc_spec (fun (_ : unit) (state : State1) => {| pre := init1_sem state; post := fun (r : InitResult) (state' : State1) => match r with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end; recovered := fun (_ : unit) (_ : State1) => True |}) init2 rec abs1 -> init_abstraction (then_init init1 init2) rec' (abstraction_compose abs1 abs2) init2_semforall (init1 init2 : proc InitResult) (rec rec' : proc unit) (State1 : Type) (abs1 : Abstraction State1) (State2 : Type) (abs2 : LayerAbstraction State1 State2) (init1_sem : State1 -> Prop) (init2_sem : State2 -> Prop), init_abstraction init1 rec abs1 init1_sem -> proc_spec (fun (_ : unit) (state : State1) => {| pre := init1_sem state; post := fun (r : InitResult) (state' : State1) => match r with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end; recovered := fun (_ : unit) (_ : State1) => True |}) init2 rec abs1 -> init_abstraction (then_init init1 init2) rec' (abstraction_compose abs1 abs2) init2_seminit1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_semH0:proc_spec (fun (_ : unit) (state : State1) => {| pre := init1_sem state; post := fun (r : InitResult) (state' : State1) => match r with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end; recovered := fun (_ : unit) (_ : State1) => True |}) init2 rec abs1init_abstraction (then_init init1 init2) rec' (abstraction_compose abs1 abs2) init2_seminit1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_semH0:proc_spec (fun (_ : unit) (state : State1) => {| pre := init1_sem state; post := fun (r : InitResult) (state' : State1) => match r with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end; recovered := fun (_ : unit) (_ : State1) => True |}) init2 rec abs1init_abstraction (then_init init1 init2) rec (abstraction_compose abs1 abs2) init2_seminit1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_semH0:proc_spec (fun (_ : unit) (state : State1) => {| pre := init1_sem state; post := fun (r : InitResult) (state' : State1) => match r with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end; recovered := fun (_ : unit) (_ : State1) => True |}) init2 rec abs1proc_spec (fun (_ : unit) (_ : world) => {| pre := True; post := fun (r : InitResult) (w' : world) => match r with | Initialized => exists state : State2, abstraction (abstraction_compose abs1 abs2) w' state /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) (then_init init1 init2) rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldr:InitResultLexec:Marker "after" init1proc_spec (fun (_ : unit) (state' : world) => {| pre := match r with | Initialized => exists state : State1, abstraction abs1 state' state /\ init1_sem state | InitFailed => True end; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) match r with | Initialized => init2 | InitFailed => Ret r end rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldr:InitResultLexec:Marker "after" init1proc_spec (fun (_ : unit) (state' : world) => {| pre := match r with | Initialized => exists state : State1, abstraction abs1 state' state /\ init1_sem state | InitFailed => True end; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) match r with | Initialized => init2 | InitFailed => Ret r end rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1proc_spec (fun (_ : unit) (state' : world) => {| pre := exists state : State1, abstraction abs1 state' state /\ init1_sem state; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) init2 rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1proc_spec (fun (_ : unit) (_ : world) => {| pre := True; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) (Ret InitFailed) rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1proc_spec (fun (_ : unit) (state' : world) => {| pre := exists state : State1, abstraction abs1 state' state /\ init1_sem state; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) init2 rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> Propa':unitstate:worldLexec:Marker "after" init1proc_spec (fun (_ : unit) (state' : world) => {| pre := exists state : State1, abstraction abs1 state' state /\ init1_sem state; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) init2 rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH0:unit -> forall (w : world) (state : State1), abstraction abs1 w state -> init1_sem state -> forall r : RResult InitResult unit, rexec init2 rec w r -> match r with | RFinished v w' => exists state' : State1, abstraction abs1 w' state' /\ match v with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end | Recovered _ w' => exists state' : State1, abstraction abs1 w' state' /\ True enda':unitstate:worldLexec:Marker "after" init1a:unitw:worldstate1:State1H1:abstraction abs1 w state1H3:init1_sem state1r:RResult InitResult unitH2:rexec init2 rec w rmatch r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state' state0) /\ init2_sem state | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True endinit1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH0:unit -> forall (w : world) (state : State1), abstraction abs1 w state -> init1_sem state -> forall r : RResult InitResult unit, rexec init2 rec w r -> match r with | RFinished v w' => exists state' : State1, abstraction abs1 w' state' /\ match v with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end | Recovered _ w' => exists state' : State1, abstraction abs1 w' state' /\ True enda':unitstate:worldLexec:Marker "after" init1a:unitw:worldstate1:State1H1:abstraction abs1 w state1H3:init1_sem state1r:RResult InitResult unitH2:match r with | RFinished v w' => exists state' : State1, abstraction abs1 w' state' /\ match v with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end | Recovered _ w' => exists state' : State1, abstraction abs1 w' state' /\ True endmatch r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state' state0) /\ init2_sem state | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True enddescend; intuition eauto.init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH0:unit -> forall (w : world) (state : State1), abstraction abs1 w state -> init1_sem state -> forall r : RResult InitResult unit, rexec init2 rec w r -> match r with | RFinished v w' => exists state' : State1, abstraction abs1 w' state' /\ match v with | Initialized => exists state'' : State2, abstraction abs2 state' state'' /\ init2_sem state'' | InitFailed => True end | Recovered _ w' => exists state' : State1, abstraction abs1 w' state' /\ True enda':unitstate:worldLexec:Marker "after" init1a:unitw:worldstate1:State1H1:abstraction abs1 w state1H3:init1_sem state1w0:worldstate':State1H:abstraction abs1 w0 state'state'':State2H2:abstraction abs2 state' state''H4:init2_sem state''exists state' : world, state' = w0 /\ (exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state' state0) /\ init2_sem state)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1proc_spec (fun (_ : unit) (_ : world) => {| pre := True; post := fun (r' : InitResult) (state'' : world) => match r' with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state'' state0) /\ init2_sem state | InitFailed => True end; recovered := fun (_ : unit) (_ : world) => True |}) (Ret InitFailed) rec (IdAbstraction world)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1a:unitw, state0:worldH1:state0 = wH2:Truer:RResult InitResult unitH3:rexec (Ret InitFailed) rec w rmatch r with | RFinished v w' => exists state' : world, state' = w' /\ match v with | Initialized => exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state' state0) /\ init2_sem state | InitFailed => True end | Recovered _ w' => exists state' : world, state' = w' /\ True endinit1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1a:unitw:worldH2:Truew0:worldH3:rexec (Ret InitFailed) rec w (RFinished Initialized w0)exists state' : world, state' = w0 /\ (exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 state' state0) /\ init2_sem state)init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1a:unitw, w0:worldH3:rexec (Ret InitFailed) rec w (RFinished Initialized w0)exists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 w0 state0) /\ init2_sem statecongruence. Qed.init1, init2:proc InitResultrec, rec':proc unitState1:Typeabs1:Abstraction State1State2:Typeabs2:LayerAbstraction State1 State2init1_sem:State1 -> Propinit2_sem:State2 -> PropH:init_abstraction init1 rec abs1 init1_sema':unitstate:worldLexec:Marker "after" init1a:unitw0:worldH1:InitFailed = Initializedexists state : State2, (exists state0 : State1, abstraction abs2 state0 state /\ abstraction abs1 w0 state0) /\ init2_sem state

This theorem allows converting between abstraction layers:
to prove the correctness of procedure p at a higher level of
abstraction, it suffices to drop down to the lower level of
abstraction, and prove that there exists a connection to the
higher level in the postcondition.

forall (A T R State2 : Type) (spec : Specification A T R State2) (p : proc T) (rec : proc R) (State1 : Type) (abs2 : LayerAbstraction State1 State2) (abs1 : Abstraction State1), proc_spec (fun '(a, state2) (state : State1) => {| pre := pre (spec a state2) /\ abstraction abs2 state state2; post := fun (v : T) (state' : State1) => exists state2' : State2, post (spec a state2) v state2' /\ abstraction abs2 state' state2'; recovered := fun (v : R) (state' : State1) => exists state2' : State2, recovered (spec a state2) v state2' /\ abstraction abs2 state' state2' |}) p rec abs1 -> proc_spec spec p rec (abstraction_compose abs1 abs2)forall (A T R State2 : Type) (spec : Specification A T R State2) (p : proc T) (rec : proc R) (State1 : Type) (abs2 : LayerAbstraction State1 State2) (abs1 : Abstraction State1), proc_spec (fun '(a, state2) (state : State1) => {| pre := pre (spec a state2) /\ abstraction abs2 state state2; post := fun (v : T) (state' : State1) => exists state2' : State2, post (spec a state2) v state2' /\ abstraction abs2 state' state2'; recovered := fun (v : R) (state' : State1) => exists state2' : State2, recovered (spec a state2) v state2' /\ abstraction abs2 state' state2' |}) p rec abs1 -> proc_spec spec p rec (abstraction_compose abs1 abs2)A, T, R, State2:Typespec:Specification A T R State2p:proc Trec:proc RState1:Typeabs2:LayerAbstraction State1 State2abs1:Abstraction State1H:proc_spec (fun '(a, state2) (state : State1) => {| pre := pre (spec a state2) /\ abstraction abs2 state state2; post := fun (v : T) (state' : State1) => exists state2' : State2, post (spec a state2) v state2' /\ abstraction abs2 state' state2'; recovered := fun (v : R) (state' : State1) => exists state2' : State2, recovered (spec a state2) v state2' /\ abstraction abs2 state' state2' |}) p rec abs1proc_spec spec p rec (abstraction_compose abs1 abs2)A, T, R, State2:Typespec:Specification A T R State2p:proc Trec:proc RState1:Typeabs2:LayerAbstraction State1 State2abs1:Abstraction State1H:proc_spec (fun '(a, state2) (state : State1) => {| pre := pre (spec a state2) /\ abstraction abs2 state state2; post := fun (v : T) (state' : State1) => exists state2' : State2, post (spec a state2) v state2' /\ abstraction abs2 state' state2'; recovered := fun (v : R) (state' : State1) => exists state2' : State2, recovered (spec a state2) v state2' /\ abstraction abs2 state' state2' |}) p rec abs1a:Aw:worldstate:State2state0:State1H0:abstraction abs2 state0 stateH3:abstraction abs1 w state0H1:pre (spec a state)r:RResult T RH2:rexec p rec w rmatch r with | RFinished v w' => exists state' : State2, (exists state : State1, abstraction abs2 state state' /\ abstraction abs1 w' state) /\ post (spec a state) v state' | Recovered v w' => exists state' : State2, (exists state : State1, abstraction abs2 state state' /\ abstraction abs1 w' state) /\ recovered (spec a state) v state' enddestruct r; intuition (repeat deex; eauto). Qed.A, T, R, State2:Typespec:Specification A T R State2p:proc Trec:proc RState1:Typeabs2:LayerAbstraction State1 State2abs1:Abstraction State1H:proc_spec (fun '(a, state2) (state : State1) => {| pre := pre (spec a state2) /\ abstraction abs2 state state2; post := fun (v : T) (state' : State1) => exists state2' : State2, post (spec a state2) v state2' /\ abstraction abs2 state' state2'; recovered := fun (v : R) (state' : State1) => exists state2' : State2, recovered (spec a state2) v state2' /\ abstraction abs2 state' state2' |}) p rec abs1a:Aw:worldstate:State2state0:State1H0:abstraction abs2 state0 stateH3:abstraction abs1 w state0H1:pre (spec a state)r:RResult T RH2:match r with | RFinished v w' => exists state' : State1, abstraction abs1 w' state' /\ (exists state2' : State2, post (spec a state) v state2' /\ abstraction abs2 state' state2') | Recovered v w' => exists state' : State1, abstraction abs1 w' state' /\ (exists state2' : State2, recovered (spec a state) v state2' /\ abstraction abs2 state' state2') endmatch r with | RFinished v w' => exists state' : State2, (exists state : State1, abstraction abs2 state state' /\ abstraction abs1 w' state) /\ post (spec a state) v state' | Recovered v w' => exists state' : State2, (exists state : State1, abstraction abs2 state state' /\ abstraction abs1 w' state) /\ recovered (spec a state) v state' end