Library POCS.Spec.ProcTheorems

Require Import Relations.Relation_Operators.
Require Import RelationClasses.

Require Import Helpers.Helpers.
Require Import Proc.

Automation for inverting execution behavior.

Ltac inv_exec' H :=
  inversion H; subst; clear H; repeat sigT_eq.

Theorem exec_ret : forall T (v:T) w r,
    exec (Ret v) w r ->
    match r with
    | Finished v' w' => v = v' /\ w = w'
    | Crashed w' => w = w'
    end.

Ltac inv_ret :=
  match goal with
  | [ H: exec (Ret _) _ _ |- _ ] =>
    apply exec_ret in H; safe_intuition; subst
  end.

Ltac inv_exec :=
  match goal with
  | _ => inv_ret
  | [ H: exec (Bind _ _) _ _ |- _ ] =>
    inv_exec' H; repeat inv_ret
  | [ H: exec _ _ _ |- _ ] =>
    inv_exec' H; repeat inv_ret
  end.

Ltac inv_rexec :=
  match goal with
  | [ H: rexec (Ret _) _ _ _ |- _ ] =>
    inv_exec' H
  | [ H: rexec _ _ _ _ |- _ ] =>
    inv_exec' H
  end.

Local Hint Constructors exec.

These are the monad laws

TODO: explain what the monad is and what these monad laws mean (specifically, we're proving that exec treats procedures up to the monad laws as equivalences between procedures).

Definition exec_equiv T (p: proc T) p' :=
  forall w r, exec p w r <-> exec p' w r.

Instance exec_equiv_equiv T : Equivalence (exec_equiv (T:=T)).

Theorem monad_left_id : forall T T' (p: T' -> proc T) v,
    exec_equiv (Bind (Ret v) p) (p v).

Theorem monad_assoc : forall `(p1: proc T)
                        `(p2: T -> proc T')
                        `(p3: T' -> proc T''),
    exec_equiv (Bind (Bind p1 p2) p3) (Bind p1 (fun v => Bind (p2 v) p3)).

Local Hint Constructors rexec.

Theorem rexec_equiv : forall T (p p': proc T) `(rec: proc R) w r,
    exec_equiv p p' ->
    rexec p' rec w r ->
    rexec p rec w r.

Theorem rexec_finish_any_rec : forall `(p: proc T)
                               `(rec: proc R)
                               `(rec': proc R')
                               w v w',
    rexec p rec w (RFinished v w') ->
    rexec p rec' w (RFinished v w').

Local Hint Constructors exec_recover.

Invert looped recovery execution for a bind in the recovery procedure. The wment essentially breaks down the execution of recovering with _ <- p; p' into three stages:

First, p runs until it finishes without crashing.
Next, p' is repeatedly run using p as the recovery procedure, crashing and recovering in a loop. The return value in p' rv comes from p and is passed from iteration to the next, initialized with the run of p in the first step.
Finally, the computer stops crashing and p' rv can run to completion.

Theorem exec_recover_bind_inv : forall `(p: proc R)
                                `(p': R -> proc R')
                                w rv' w'',
    exec_recover (Bind p p') w rv' w'' ->
    exists rv1 w1, exec_recover p w rv1 w1 /\
                  exists rv2 w2,
                    clos_refl_trans_1n
                      (fun '(rv , w ) '(rv', w') =>
                         rexec (p' rv) p w (Recovered rv' w'))
                      (rv1 , w1 ) (rv2 , w2 ) /\
                    exec (p' rv2) w2 (Finished rv' w'').