Require Import Helpers.Helpers.
Require Import Proc.
Require Import ProcTheorems.
Require Import Abstraction.

Hint Constructors rexec.
Hint Constructors exec.
Hint Constructors exec_recover.

Theorem clos_refl_trans_1n_unit_tuple : forall `(R: unit * A -> unit * A -> Prop) x y u u',
    Relation_Operators.clos_refl_trans_1n R (u, x) (u', y) ->
    Relation_Operators.clos_refl_trans_1n
      (fun x y =>
         R (tt, x) (tt, y)) x y.

Definition proc_loopspec `(spec: Specification A unit unit State)
           `(rec': proc unit) `(rec: proc unit)
           (abs: Abstraction State) :=
  forall a w state,
    abstraction abs w state ->
    pre (spec a state) ->
    forall rv rv' w',
      Relation_Operators.clos_refl_trans_1n
        (fun '(_, w) '(rv', w') => rexec rec' rec w (Recovered rv' w'))
        (rv, w) (rv', w') ->
      forall rv'' w'',
        exec rec' w' (Finished rv'' w'') ->
        exists state'',
          abstraction abs w'' state'' /\
          post (spec a state) rv'' state''.

Definition idempotent `(spec: Specification A T unit State) :=
  forall a state,
    pre (spec a state) ->
    forall v state', recovered (spec a state) v state' ->
            

            exists a', pre (spec a' state') /\
                  

                  forall rv state'', post (spec a' state') rv state'' ->
                                post (spec a state) rv state''.

Theorem idempotent_loopspec : forall `(rec: proc unit) `(rec': proc unit)
                                     `(spec: Specification A unit unit State)
                                     (abs: Abstraction State),
    forall (Hspec: proc_spec spec rec' rec abs),
      idempotent spec ->
      proc_loopspec spec rec' rec abs.

Theorem compose_recovery : forall `(spec: Specification A'' T unit State)
                             `(rspec: Specification A' unit unit State)
                             `(spec': Specification A T unit State)
                             `(p: proc T) `(rec: proc unit) `(rec': proc unit)
                             `(abs: Abstraction State),
    forall (Hspec: proc_spec spec p rec abs)
      (Hrspec: proc_loopspec rspec rec' rec abs)
      (Hspec_spec':
         forall (a:A) state, pre (spec' a state) ->
                    exists (a'':A''),
                      pre (spec a'' state) /\
                      (forall v state', post (spec a'' state) v state' ->
                               post (spec' a state) v state') /\
                      (forall v state', recovered (spec a'' state) v state' ->
                               exists a', pre (rspec a' state') /\
                                     forall v' state'',
                                       post (rspec a' state') v' state'' ->
                                       recovered (spec' a state) v' state'')),
      proc_spec spec' p (_ <- rec; rec') abs.

Theorem spec_abstraction_compose :
  forall `(spec: Specification A T R State2)
    `(p: proc T) `(rec: proc R)
    `(abs2: LayerAbstraction State1 State2)
    `(abs1: Abstraction State1),
    proc_spec
      (fun '(a, state2) state =>
         {| pre := pre (spec a state2) /\
                   abstraction abs2 state state2;
            post :=
              fun v state' =>
                exists state2',
                  post (spec a state2) v state2' /\
                  abstraction abs2 state' state2';
            recovered :=
              fun v state' =>
                exists state2',
                  recovered (spec a state2) v state2' /\
                  abstraction abs2 state' state2'; |}) p rec abs1 ->
    proc_spec spec p rec (abstraction_compose abs1 abs2).

Theorem rec_noop_compose : forall `(rec: proc unit) `(rec2: proc unit)
                             `(abs1: Abstraction State1)
                             (wipe1: State1 -> State1 -> Prop)
                             `(spec: Specification A unit unit State1)
                             `(abs2: LayerAbstraction State1 State2)
                             (wipe2: State2 -> State2 -> Prop),
    rec_noop rec abs1 wipe1 ->
    proc_loopspec spec rec2 rec abs1 ->
    forall (Hspec: forall state0 state0' state,
          abstraction abs2 state0 state0' ->
          wipe1 state0 state ->
          exists a, pre (spec a state) /\
               forall state' r state'',
                 post (spec a state') r state'' ->
                 exists state2', wipe2 state0' state2' /\
                            abstraction abs2 state'' state2'),
    rec_noop (_ <- rec; rec2) (abstraction_compose abs1 abs2) wipe2.

Definition Semantics State T := State -> T -> State -> Prop.

Definition pre_step {opT State}
           (bg_step: State -> State -> Prop)
           (step: forall `(op: opT T), Semantics State T) :
  forall T (op: opT T), Semantics State T :=
  fun T (op: opT T) state v state'' =>
    exists state', bg_step state state' /\
          step op state' v state''.

Definition post_step {opT State}
           (step: forall `(op: opT T), Semantics State T)
           (bg_step: State -> State -> Prop) :
  forall T (op: opT T), Semantics State T :=
  fun T (op: opT T) state v state'' =>
    exists state', step op state v state' /\
          bg_step state' state''.

Definition op_spec `(sem: Semantics State T) : Specification unit T unit State :=
  fun (_:unit) state =>
    {|
      pre := True;
      post :=
        fun v state' => sem state v state';
      recovered :=
        fun r state' =>
          r = tt /\ (state' = state \/ exists v, sem state v state');
    |}.

Definition no_wipe {State} (state state' : State) : Prop := state' = state.
Hint Unfold no_wipe.

Definition no_crash {State} (state state' : State) : Prop := False.
Hint Unfold no_crash.