Module PLFO_PL

Require Import List.
Import ListNotations.
Require Import Relations.

Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.

Refinement proof: PLFO.sem o ⊆ PL.sem


Auxiliary definitions


States are equal, modulo the equivalence relation on device states.
Inductive same : PLFO.state -> PLF.state -> Prop :=
| same_init: forall oraclechk,
    same (PLFO.INIT oraclechk)
         PLF.INIT
| same_usr : forall oraclechk mcu dev chkpt dev',
    forall (EQUIV: DEV.equiv dev dev'),
      same (PLFO.USR oraclechk mcu dev chkpt)
           (PLF.USR mcu dev' chkpt)
| same_drv : forall oraclechk mcu dev l chkpt dev',
    forall (EQUIV: DEV.equiv dev dev'),
      same (PLFO.DRV oraclechk mcu dev l chkpt)
           (PLF.DRV mcu dev' l chkpt)
| same_pwr : forall oraclechk chkpt,
    same (PLFO.PWR oraclechk chkpt)
         (PLF.PWR chkpt)
| same_off : forall oraclechk chkpt,
    same (PLFO.OFF oraclechk chkpt)
         (PLF.OFF chkpt).

Getting the oracle of a PLFO state.
Definition oracle_of (s: PLFO.state): oracle :=
  match s with
  | PLFO.INIT o => o
  | PLFO.USR o _ _ _ => o
  | PLFO.DRV o _ _ _ _ => o
  | PLFO.PWR o _ => o
  | PLFO.OFF o _ => o
  end.

Getting the non-volatile checkpointing storage of a PLFO state.
Definition chkpt_of (s: PLFO.state): CHKPT.t :=
  match s with
  | PLFO.INIT _ => CHKPT.init
  | PLFO.USR _ _ _ chkpt => chkpt
  | PLFO.DRV _ _ _ _ chkpt => chkpt
  | PLFO.PWR _ chkpt => chkpt
  | PLFO.OFF _ chkpt => chkpt
  end.

Predicates to factorize cases in the definition of the matching relation.
Definition off_or_osucceed (s: PLFO.state) : Prop :=
  (exists o c, s = PLFO.OFF o c)
  \/ (match oracle_of s with
      | true::_ => True
      | _ => False
      end).

Definition off_or_ofail (s: PLFO.state) : Prop :=
  (exists o c, s = PLFO.OFF o c)
  \/ match oracle_of s with
     | [] | false::_ => True
     | _ => False
     end.
  
Simulation relation.
Inductive match_states : PLFO.state -> PLstate -> Prop :=
| match_init: forall oraclechk,
    match_states (PLFO.INIT oraclechk)
                 PLF.INIT

| match_stutter : forall s chkpt',
    forall (WAIT: off_or_ofail s)
           (LASTMCU: CHKPT.last_mcu chkpt' = CHKPT.last_mcu (chkpt_of s))
           (LASTDEVICE: CHKPT.last_log chkpt' = CHKPT.last_log (chkpt_of s))
           (SWAPMCU: CHKPT.last_mcu chkpt' = CHKPT.next_mcu chkpt')
           (SWAPDEVICE: CHKPT.last_log chkpt' = CHKPT.next_log chkpt'),
      match_states s
                   (PLF.OFF chkpt')

| match_stutter_init : forall s,
    forall (WAIT: off_or_ofail s)
           (LASTMCU: CHKPT.last_mcu CHKPT.init = CHKPT.last_mcu (chkpt_of s))
           (LASTDEVICE: CHKPT.last_log CHKPT.init = CHKPT.last_log (chkpt_of s)),
      match_states s
                   PLF.INIT
                   
| match_step_off : forall s chkpt',
    forall (SAME: same s (PLF.OFF chkpt'))
           (SWAPMCU: CHKPT.last_mcu chkpt' = CHKPT.next_mcu chkpt')
           (SWAPDEVICE: CHKPT.last_log chkpt' = CHKPT.next_log chkpt'),
      match_states s
                   (PLF.OFF chkpt')

| match_step_oth : forall s st,
    forall (FOLLOW: off_or_osucceed s)
           (SAME: same s st)
           (NOTOFF: forall chkpt, st <> PLF.OFF chkpt),
      match_states s
                   st.

Star-simulation diagram between PLFO and PL.
Lemma match_step: forall s1 t s2,
    forall (STEP: PLFO.step s1 t s2)
           as1
           (COH: match_states s1 as1),
      (exists as2, run PL.step as1 t as2 /\ match_states s2 as2).
Proof.

  intros.
  enough (CASE s1 t s2); [| constructor; auto].
  revert dependent s1.
  revert dependent s2.

  induction 1 ; intros; subst.

  - (* INIT -> USR *)
    inv COH.

    + destruct oraclechk.
      * eexists. split.
        -- eapply run_refl.
        -- econstructor; eauto.
           right; auto.
           
      * destruct b.
        -- (* Chp will succeed *)
          eexists. split.
          ++ eapply run_step.
             econstructor; eauto.
          ++ econstructor; eauto.
             ** right; auto.
             ** constructor; auto.
                apply equiv_refl.
                apply DEV.equiv_equiv.
             ** congruence.
        -- (* Chp will fail *)
          eexists. split.
          ++ eapply run_refl; eauto.
          ++ econstructor; eauto.
             right; auto.
    + inv WAIT.
      { edestruct H0 as [o [c HEQ]]; congruence. }
      { eexists. split.
        * eapply run_refl; eauto.
        * econstructor 2 ; eauto.
          right; auto.
      }

    + inv WAIT.
      { edestruct H0 as [o [c HEQ]]; congruence. }
      { eexists. split.
        * eapply run_refl.
        * econstructor; eauto.
          right; auto.
      }
    + inv SAME.

    + eexists. split.
      * eapply run_step.
        inv SAME.
        econstructor; eauto.
      * econstructor; eauto.
        -- inv FOLLOW.
           ++ destruct H0 as [o [c HEQ]]; congruence.
           ++ destruct oraclechk; try intuition; simpl in *.
              intuition.
              destruct b; try intuition.
              right; auto.
        -- econstructor; eauto.
           apply equiv_refl.
           apply DEV.equiv_equiv.
        -- congruence.

  - (* USR -> USR *)
    pose proof (SPEC.axiom_usr _ _ _ _ _ INSTR) as [-> ->]; eauto.
    simpl.
    inv COH.

    + destruct oraclechk.
      * eexists. split.
        -- eapply run_refl.
        -- econstructor; eauto.
           right; auto.
           
      * destruct b.
        -- inv WAIT.
           { edestruct H0 as [o [c HEQ]]; congruence. }
           { inv H0. }
        -- eexists. split.
           ++ eapply run_refl.
           ++ econstructor; eauto.
              right; auto.
              
    + eexists. split.
      * eapply run_refl; eauto.
      * econstructor 3 ; eauto.
        inv WAIT.
        -- destruct H0 as [o [c HEQ]]; congruence.
        -- right; auto.
           
    + inv SAME.

    + inv SAME.
      eexists. split.
      * edestruct SPEC.axiom_equiv as [dev'' Hstep]; eauto; subst.
        apply run_step.
        pose proof (SPEC.axiom_usr _ _ _ _ _ Hstep) as [-> _]; eauto.
        change [] with (map PL.Op []) ; auto.
        eapply PL.sem_usr.
        eapply Hstep; eauto.

      * econstructor; eauto.
        -- inv FOLLOW.
           ++ destruct H0 as [o [c Heq]] ; inv Heq.
           ++ destruct oraclechk; simpl in H0.
              ** intuition.
              ** destruct b ; try intuition.
                 right; auto.
        -- constructor; auto.
        -- congruence.

  - (* USR -> DRV *)
    pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]]; eauto.
    simpl.
    simpl in *.
    inv COH.

    + destruct oraclechk.
      * eexists. split.
        -- apply run_refl.
        -- econstructor; eauto.
           right; auto.
           
      * destruct b.
        -- inv WAIT.
           edestruct H0 as [o [c HEQ]]; congruence.
           inv H0.
        -- eexists. split.
           ++ apply run_refl.
           ++ econstructor; eauto.
              right; auto.
              
    + eexists. split.
      * apply run_refl.
      * econstructor 3 ; eauto.
        inv WAIT.
        -- destruct H0 as [o [c HEQ]]; congruence.
        -- destruct oraclechk.
           ++ right; auto.
           ++ simpl in H0. destruct b; intuition.
              right; auto.
             
    + inv SAME.

    + inv SAME.
      eexists. split.
      * edestruct SPEC.axiom_equiv as [dev'' Hstep]; eauto; subst.
        apply run_step.
        pose proof (SPEC.axiom_enter _ _ _ _ _ Hstep) as [-> _]; eauto.
        change [] with (map PL.Op []) ; auto.
        eapply PL.sem_enter; eauto.

      * econstructor ; eauto.
        -- inv FOLLOW.
           ++ destruct H0 as [o [c Heq]] ; inv Heq.
           ++ destruct oraclechk; simpl in H0.
              ** intuition.
              ** destruct b ; try intuition.
                 right; auto.
        -- econstructor; eauto.
        -- congruence.
        
  - (* DRV -> DRV *)
    destruct oc.
    + inv COH; try contradiction.
      * inv WAIT.
        destruct H0 as [o [c HEQ]]; try congruence.
        inv H0.
      * inv WAIT.
        destruct H0 as [o [c HEQ]]; try congruence.
        inv H0.
      * inv SAME.
      * inv SAME.
        edestruct SPEC.axiom_equiv as [dev'' Hstep]; eauto; subst.
        eexists. split.
        -- apply run_step.
           eapply PL.sem_drv with (l':= l'); eauto.
        -- econstructor; eauto.
           ++ inv FOLLOW.
              ** destruct H0 as [o [c Heq]]; inv Heq.
              ** inv H0. right; auto.
           ++ econstructor; eauto.
              pose proof (SPEC.axiom_drv _ _ _ _ _ INSTR); eauto.
              pose proof (SPEC.axiom_drv _ _ _ _ _ Hstep); eauto.
              eapply DEV.ops_sem_equiv; eauto.
           ++ congruence.
        
    + inv COH; try contradiction.
      * eexists. split.
        -- eapply run_refl; eauto.
        -- econstructor ; eauto.
           right; auto.
      * eexists. split.
        -- eapply run_refl; eauto.
        -- econstructor ; eauto.
           right; auto.
           
      * inv SAME.
      * inv FOLLOW.
        -- destruct H0 as [o [c Heq]]; inv Heq.
        -- inv H0.
        
  - (* DRV -> USR *)
    pose proof (SPEC.axiom_leave _ _ _ _ _ INSTR) as [-> [-> ->]]; eauto.
    destruct oc.
    + inv COH; try contradiction.
      * inv WAIT.
        destruct H0 as [o [c HEQ]]; try congruence.
        inv H0.
      * inv WAIT.
        destruct H0 as [o [c HEQ]]; try congruence.
        inv H0.
      * inv SAME.
      * inv SAME.
        edestruct SPEC.axiom_equiv as [dev'' Hstep]; eauto; subst.
        pose proof (SPEC.axiom_leave _ _ _ _ _ Hstep) as [-> _]; eauto.
        eexists. split.
        -- eapply run_step; eauto.
           econstructor; eauto.
        
        -- econstructor; eauto.
           ++ right; auto.
           ++ econstructor; eauto.
           ++ congruence.
        
    + inv COH; try contradiction; simpl in *.
      
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
      * inv SAME.

      * inv FOLLOW.
        -- destruct H0 as [o [c Heq]]; try congruence.
        -- inv H0.
        
  - (* USR -> PWR *)
    inv COH; simpl in *.

    + eexists. split.
      eapply run_refl; eauto.
      econstructor; eauto.
      inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      destruct oraclechk.
      right; auto.
      destruct b; simpl in H0. intuition. right; auto.
    + eexists. split.
      eapply run_refl; eauto.
      econstructor; eauto.
      inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      destruct oraclechk.
      right; auto.
      destruct b; simpl in H0. intuition. right; auto.
    + inv SAME.
    + inv SAME.
      eexists. split.
      * eapply run_step; eauto.
        econstructor; eauto.
        
      * eapply match_step_oth; eauto.
        -- inv FOLLOW.
           ++ destruct H0 as [o [c Heq]]; try congruence.
           ++ destruct oraclechk ; simpl in *; try intuition.
              destruct b ; try intuition.
              right; auto.
        -- econstructor; eauto.
        -- congruence.
        
  - (* DRV -> PWR *)
    destruct oc; inv COH; try contradiction.

    + inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      inv H0.

    + inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      inv H0.

    + inv SAME.

    + inv SAME. eexists. split.
      * eapply run_step; eauto.
        econstructor; eauto.
      * eapply match_step_oth; eauto.
        right; auto.
        econstructor; eauto.
        congruence.
        
    + eexists. split.
      eapply run_refl; eauto.
      econstructor; eauto.
      right; auto.
      
    + eexists. split.
      eapply run_refl; eauto.
      econstructor; eauto.
      right; auto.
      
    + inv SAME.

    + inv FOLLOW.
      * destruct H0 as [o [c Heq]]; try congruence.
      * inv H0.
      
  - (* PWR -> OFF OK *)
    inv COH; try contradiction; try inv SAME.
    + inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      inv H0.
    + inv WAIT.
      destruct H0 as [o [c HEQ]]; try congruence.
      inv H0.
    + eexists. split.
    * eapply run_step; eauto.
      econstructor; eauto.
      
    * econstructor 4; eauto.
      econstructor; eauto.

  - (* PWR -> OFF Fail *)
    inv COH; try contradiction; simpl in *.

    + eexists. split.
      eapply run_refl; eauto.
      eapply match_stutter; eauto.
      left; eauto.
    + eexists. split.
      eapply run_refl; eauto.
      econstructor; eauto.
      left; eauto.
    + inv SAME.
    + inv FOLLOW.
      * destruct H0 as [o [c Heq]]; try congruence.
      * inv H0.
      
      
  - (* OFF -> USR *)
    inv COH; try contradiction.

    + (* Chp Fail *)
      simpl in *.
      destruct oraclechk; [| destruct b].
      
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
      * eexists. split.
        eapply run_step ; eauto.
        econstructor ; eauto.
        econstructor ; eauto.
        right; auto.
        unfold CHKPT.reset.
        rewrite <- LASTDEVICE.
        rewrite <- LASTMCU.
        rewrite SWAPMCU.
        rewrite SWAPDEVICE.
        econstructor.
        apply DEV.equiv_equiv.
        congruence.
        
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
    + (* Chp Fail *)
      simpl in *.
      destruct oraclechk; [| destruct b].
      
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
      * eexists. split.
        eapply run_step ; eauto.
        econstructor ; eauto.
        econstructor ; eauto.
        right; auto.
        unfold CHKPT.reset.
        rewrite <- LASTDEVICE.
        rewrite <- LASTMCU.
        simpl.
        econstructor.
        apply LOG.restore_init.
        congruence.
        
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
    + inv SAME.
      destruct oraclechk; [|destruct b].
      
      * eexists. split.
        eapply run_refl; eauto.
        econstructor 2; eauto.
        right; auto.
        
      * eexists. split.
        -- eapply run_step; eauto.
           econstructor; eauto.
        -- econstructor 5; eauto.
           right; auto.
           rewrite SWAPMCU.
           rewrite SWAPDEVICE.
           eapply same_usr; eauto.
           apply DEV.equiv_equiv.
           congruence.
      * eexists. split.
        eapply run_refl; eauto.
        econstructor; eauto.
        right; auto.
        
    + inv SAME. elim (NOTOFF chkpt).
      auto.
      
  - inv COH; try contradiction.

    + eexists. split.
      * eapply run_refl; eauto.
      * econstructor; eauto.
        left; eauto.
        
    + eexists. split.
      * eapply run_refl; eauto.
      * econstructor; eauto.
        left; eauto.
        
    + inv SAME.

    + inv FOLLOW.
      * destruct H0 as [o [c Heq]]; congruence.
      * inv H0.
      
  - inv COH; try contradiction.

    + eexists. split.
      * eapply run_refl; eauto.
      * econstructor; eauto.
        left; eauto.
        
    + eexists. split.
      * eapply run_refl; eauto.
      * econstructor; eauto.
        left; eauto.
        
    + inv SAME.

    + inv FOLLOW.
      * destruct H0 as [o [c Heq]]; congruence.
      * inv H0.
      
Qed.

The simulation relation is preserved after any number of steps of PLFO.
Lemma match_star : forall s1 t s2,
    run PLFO.step s1 t s2 ->
    forall as1,
      match_states s1 as1 ->
      exists as2, run PL.step as1 t as2 /\ match_states s2 as2.
Proof.
  induction 1 ; intros.
  - eapply match_step; eauto.
  - exists as1; split; auto.
    apply run_refl.
  - eapply IHrun1 in H1.
    destruct H1 as [as2 [HSTEP HCOH]].
    eapply IHrun2 in HCOH.
    destruct HCOH as [as3 [HSTEP2 HCOH2]].
    exists as3; split; eauto.
    eapply run_trans; eauto.
Qed.

Trace inclusion result between PLFO and PL.
Theorem checkpointing_correctness : forall o t,
    PLFO.sem o t ->
    PL.sem t.
Proof.
  unfold PLFO.sem, PL.sem.
  intros o t [s RUN].
  eapply match_star in RUN; eauto.
  - destruct RUN as [as2 [RUN MATCH]].
    eauto.
  - constructor.
Qed.
Generated by coq2html