# Library POCS.Spec.Abstraction

# 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'

## Abstraction relation and composition

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.

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; |}.

## Specification

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).

## 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.

## Proving correctness

- 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.

Theorem proc_spec_weaken : forall `(spec1: Specification A T R State)

`(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 abs.

Hint Resolve tt.

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:

Theorem proc_spec_rx : forall `(spec: Specification A T R State)

`(p: proc T) `(rec: proc R)

`(rx: T -> proc T')

`(spec': Specification A' T' R State)

`(abs: Abstraction State),

proc_spec spec p rec abs ->

(forall a' state, pre (spec' a' state) ->

exists a, pre (spec a state) /\

(forall r,

proc_spec

(fun (_:unit) state' =>

{| pre := post (spec a state) r state';

post :=

fun r state'' =>

post (spec' a' state) r state'';

recovered :=

fun r state'' =>

recovered (spec' a' state) r state'' |})

(rx r) rec abs) /\

(forall r state', recovered (spec a state) r state' ->

recovered (spec' a' state) r state')) ->

proc_spec spec' (Bind p rx) rec abs.

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.

Theorem spec_intros : forall `(spec: Specification A T R State)

`(p: proc T) `(rec: proc R)

`(abs: Abstraction State),

(forall a state0,

pre (spec a state0) ->

proc_spec

(fun (_:unit) state =>

{| pre := state = state0;

post :=

fun r state' => post (spec a state) r state';

recovered :=

fun r state' => recovered (spec a state) r state';

|}) p rec abs) ->

proc_spec spec p rec abs.

Ltac spec_intros := intros; eapply spec_intros; intros.

Ltac spec_case pf :=

eapply proc_spec_weaken; [ solve [ apply pf ] |

unfold spec_impl ].

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.

Theorem spec_exec_equiv : forall `(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 abs.

## Reasoning about the Ret return operation.

Definition rec_noop `(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_noop
theorem holds (i.e., the recovery procedure is correctly
described by a wipe relation wipe), and the specification
spec matches the wipe relation:

Theorem ret_spec : forall `(abs: Abstraction State)

(wipe: State -> State -> Prop)

`(spec: Specification A T R State)

(v:T) (rec: proc R),

rec_noop rec abs wipe ->

(forall a state, pre (spec a state) ->

post (spec a state) v state /\

forall state', wipe state state' ->

forall r, recovered (spec a state) r state') ->

proc_spec spec (Ret v) rec abs.

## 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 :=

match goal with

| |- forall _, _ => intros; step_proc_basic

| |- proc_spec _ (Ret _) _ _ =>

eapply ret_spec

| |- proc_spec _ _ _ _ =>

monad_simpl;

eapply proc_spec_rx; [ solve [ eauto ] | ]

| [ H: proc_spec _ ?p _ _

|- proc_spec _ ?p _ _ ] =>

eapply proc_spec_weaken; [ eapply H | unfold spec_impl ]

end.

Ltac step_proc :=

intros;

match goal with

| |- proc_spec _ (Ret _) _ _ =>

eapply ret_spec

| |- proc_spec _ _ _ _ =>

monad_simpl;

eapply proc_spec_rx; [ solve [ eauto ] | ]

| [ H: proc_spec _ ?p _ _

|- proc_spec _ ?p _ _ ] =>

eapply proc_spec_weaken; [ eapply H | unfold spec_impl ]

end;

intros; simpl;

cbn [pre post recovered] in *;

repeat match goal with

| [ H: _ /\ _ |- _ ] => destruct H

| [ |- rec_noop _ _ _ ] => eauto

| [ |- forall _, _ ] => intros

| [ |- exists (_:unit), _ ] => exists tt

| [ |- _ /\ _ ] => split; [ solve [ trivial ] | ]

| [ |- _ /\ _ ] => split; [ | solve [ trivial ] ]

| _ => solve [ trivial ]

| _ => progress subst

| _ => progress autounfold in *

end.

## Initialization

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

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:

Theorem init_abstraction_any_rec : forall (init: proc InitResult)

(rec rec': proc unit)

`(abs: Abstraction State)

(init_sem: State -> Prop),

init_abstraction init rec abs init_sem ->

init_abstraction init rec' abs init_sem.

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

Theorem then_init_compose : forall (init1 init2: proc InitResult)

(rec rec': proc unit)

`(abs1: Abstraction State1)

`(abs2: LayerAbstraction State1 State2)

(init1_sem: State1 -> Prop)

(init2_sem: State2 -> Prop),

init_abstraction init1 rec abs1 init1_sem ->

proc_spec

(fun (_:unit) state =>

{| pre := init1_sem state;

post :=

fun r state' => match r with

| Initialized =>

exists state'', abstraction abs2 state' state'' /\ init2_sem state''

| InitFailed => True

end;

recovered :=

fun _ state' => True; |}) init2 rec abs1 ->

init_abstraction (then_init init1 init2) rec' (abstraction_compose abs1 abs2) init2_sem.