# POCS.Spec.Proc

Global Set Implicit Arguments.

Global Generalizable All Variables.

(* turn this on to enforce strict bulleting and braces (every tactic must apply

to a single goal) *)

Global Set Default Goal Selector "!".

Global Generalizable All Variables.

(* turn this on to enforce strict bulleting and braces (every tactic must apply

to a single goal) *)

Global Set Default Goal Selector "!".

# Model of sequential procedures with mutable state.

- What a procedure looks like.
- How a procedure executes.

Module IO.

Inductive Model :=

{ baseOpT : Type -> Type;

world : Type;

world_crash : world -> world;

base_step: forall T, baseOpT T -> world -> T -> world -> Prop;

}.

End IO.

Axiom baseModel : IO.Model.

Inductive Model :=

{ baseOpT : Type -> Type;

world : Type;

world_crash : world -> world;

base_step: forall T, baseOpT T -> world -> T -> world -> Prop;

}.

End IO.

Axiom baseModel : IO.Model.

As a technical detail, we let procedures include arbitrary operations of types
baseOpT T (which will produce a T-typed result). These will tell Coq that
a proc can contain outside code that we don't care to represent here.

Our minimal, generic model of sequential procedures.
The only detail we expose about our opaque procedures is that it's possible
to combine procedures together, using Ret and Bind. If you're familiar
with Haskell, these are the same as return and (>>=) for the IO monad.
Procedures are parametrized by type T, which is the type of value
that will be returned by the procedure. For example, a procedure
that returns a nat has type proc nat, and a procedure that returns
nothing ("void", in C terminology) has type proc unit.
As a technical detail, we include a constructor BaseOp to include
arbitrary external operations. Without this constructor, Coq would think
that every proc consists only of Ret and Bind and thus can't have side
effects.

CoInductive proc (T : Type) : Type :=

| BaseOp (op : baseOpT T)

| Ret (v : T)

| Bind (T1 : Type) (p1 : proc T1) (p2 : T1 -> proc T).

Here we connect our definition of the procedure language, proc,
to Haskell's built-in implementations of Bind and Ret, which are
return and (>>=) respectively. We instruct Coq to extract any
use of BaseOp to an error expression, since we do not expect any
legitimate use of BaseOp in Gallina. We also instruct Coq to
extract any attempts to pattern-match a procedure to an error, since
we do not expect any legitimate code to pattern-match the contents of
a proc procedure.

Require Extraction.

Extraction Language Haskell.

Extract Inductive proc => "Proc"

["error 'accessing BaseOp'" "return" "(>>=)"]

"(\fprim fret fbind -> error 'pattern match on proc')".

# Execution model.

We start by defining the possible outcomes of executing a procedure proc
T: either the procedure finishes and returns something of type T, or the
procedure crashes. Because we are explicitly modeling the effect of
procedures on the state of our system, both of these outcomes also include
the resulting world state.

To define the execution of procedures, we need to state an axiom about how our
opaque baseOpT primitives execute. This axiom is base_step. This is
just another technicality.

Definition base_step : forall T, baseOpT T -> world -> T -> world -> Prop :=

IO.base_step baseModel.

Finally, we define the exec relation to represent the execution semantics
of a procedure, leveraging the step and world_crash definitions from
above. The interpretation is that when exec p w r holds, procedure p
when executed in state w can end up with the result r. Recall that the
Result T type always includes the final world state, and includes a return
value of type T if the execution finishes successfully without crashing.

There are three interesting aspects of this definition:

- First, it defines how Bind and Ret work, in the ExecRet and ExecBindFinished constructors.

| ExecRet : forall T (v:T) w,

exec (Ret v) w (Finished v w)

| ExecBindFinished : forall T T' (p: proc T) (p': T -> proc T')

w v w' r,

exec p w (Finished v w') ->

exec (p' v) w' r ->

exec (Bind p p') w r

- Second, it incorporates the opaque way base operations step.

| ExecOp : forall T (op: baseOpT T) w v w',

base_step op w v w' ->

exec (BaseOp _ op) w (Finished v w')

- And finally, it defines how procedures can crash. Any procedure can crash just before it starts running or just after it finishes. Bind can crash in the middle of running the first sub-procedure. Crashes during the second sub-procedure of a Bind are covered by the ExecBindFinished constructor above.

| ExecCrashBegin : forall T (p: proc T) w,

exec p w (Crashed w)

| ExecCrashEnd : forall T (p: proc T) w v w',

exec p w (Finished v w') ->

exec p w (Crashed w')

| ExecBindCrashed : forall T T' (p: proc T) (p': T -> proc T')

w w',

exec p w (Crashed w') ->

exec (Bind p p') w (Crashed w').

# Execution model with recovery

Before we talk about the whole execution, we first just model executing the
recovery procedure, including repeated attempts in the case of a crash
during recovery. exec_recover rec w rv w' means the procedure rec can
execute from w to w', ultimately returning rv (a "recovery value"),
and possibly crashing and restarting multiple times along the way.

The first constructor, ExecRecoverExec, says that if the recovery
procedure rec executes and finishes normally, then that's a possible
outcome for exec_recover.

The second constructor, ExecRecoverCrashDuringRecovery, allows repeated
crashes by referring to exec_recover recursively. In between crashes, the
world state is transformed according to world_crash.

| ExecRecoverCrashDuringRecovery : forall w' v w'',

exec rec w (Crashed w') ->

exec_recover rec (world_crash w') v w'' ->

exec_recover rec w v w''.

# Chaining normal execution with recovery

*and*a return value from the recovery procedure.

Inductive RResult T R :=

| RFinished (v:T) (w:world)

| Recovered (v:R) (w:world).

Arguments RFinished {T R} v w.

Arguments Recovered {T R} v w.

| RFinished (v:T) (w:world)

| Recovered (v:R) (w:world).

Arguments RFinished {T R} v w.

Arguments Recovered {T R} v w.

Finally, rexec defines what it means to run a procedure and use
some recovery procedure on crashes, including crashes during recovery.
rexec says that:
Note that there is no recursion in this definition; it merely combines
normal execution with crash execution followed by recovery execution, each
of which is defined above.

- either the original procedure p finishes and returns a RFinished outcome, or
- p crashes, and after running the recovery procedure rec one or more times, the system eventually stops crashing, rec finishes, and produces a Recovered outcome.

Inductive rexec T R : proc T -> proc R -> world -> RResult T R -> Prop :=

| RExec : forall (p:proc T) (rec:proc R) w v w',

exec p w (Finished v w') ->

rexec p rec w (RFinished v w')

| RExecCrash : forall (p:proc T) (rec:proc R) w w' rv w'',

exec p w (Crashed w') ->

exec_recover rec (world_crash w') rv w'' ->

rexec p rec w (Recovered rv w'').

# Notation for composing procedures.

x <- firstProcedure;

secondProcedure (x+1)

_ <- firstProcedure;

secondProcedure