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.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 Set Default Proof Using "Type".

# Model of sequential procedures with mutable state.

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

At the lowest level, operations are implemented in terms of some machine
primitives that we don't directly model. We group together the assumptions
related to these primitives here, so that we can assume them in one go.
Alluding to the Haskell IO monad, which is where our procedures actually
run, we call this model IO.Model.

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.

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.

`Definition baseOpT : Type -> Type := IO.baseOpT baseModel.`

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.

When we define how procedures execute, we will say they manipulate some state
of this opaque type world. We won't ever define this type in Coq, but it will
show up later to capture the idea that procedures move from one world state to
another in sequence.

`Definition world : Type := IO.world baseModel.`

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.

Inductive Result T := | Finished (v:T) (w:world) | Crashed (w:world). Arguments Crashed {T} w.

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.

```
Inductive exec : forall T, proc T -> world -> Result T -> Prop :=
(** 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

When we talk about recovery, we need to capture one more property of
crashes. Above, a crash just stops execution. In practice, however, some
parts of the state are volatile and are lost after a crash, such as memory
contents or disk write buffers. Our model is that, on a crash, the world
state is modified according to the opaque world_crash function, which we
define as an axiom. This relation is meant to capture the computer losing
volatile state, such as memory contents or disk write buffers.

`Definition world_crash : world -> world := IO.world_crash baseModel.`

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.

```
Inductive exec_recover R (rec:proc R) (w:world) : R -> world -> Prop :=
(** The first constructor, [ExecRecoverExec], says that if the recovery
procedure [rec] executes and finishes normally, then that's a possible
outcome for [exec_recover].
*)
| ExecRecoverExec : forall v w',
exec rec w (Finished v w') ->
exec_recover rec w v w'
(** 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''.
```

RResult ("recovery result") is the outcome of running a procedure with
recovery. It is similar to the Result type defined above, except that in
the case of a crash, we run a recovery procedure and get both a final state

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

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

Notation "x <- p1 ; p2" := (Bind p1 (fun x => p2)) (at level 60, right associativity). Arguments Ret {T} v.