Module PL_PLO

Require Import List.
Import ListNotations.
Require Import Relations.

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

Refinement between PL and PLO machines

We can remove the non-determinism from PL by introducing the oracle for power-loss interrupts occurring during power-continuous sections.

The refinement lemma is at the end of this file, stating that forall trace t, PL.sem t -> ∃ o t', PLO.sem o t' ∧ ∃ b, subtrace_log b t t'.

Subtrace relation


Definition of subtrace_log filtering out portions of trace ending with a aborted power-continuous section.
Inductive subtrace_log : bool -> PL.trace -> PLO.trace -> Prop :=
| committed_end : forall b t t',
    subtrace_log b t t' ->
    subtrace_log true (PL.LogS :: t) t'
| committed_cons : forall e t t',
    subtrace_log true t t' ->
    subtrace_log true (PL.Op e :: t) (e :: t')
| ignored_nil : subtrace_log false [] []
| ignored_end : forall b t t',
    subtrace_log b t t' ->
    subtrace_log false (PL.LogF :: t) t'
| ignored_cons : forall e t t',
    subtrace_log false t t' ->
    subtrace_log false (PL.Op e :: t) t'.

Unicity property for the subtrace_log relation
Lemma subtrace_log_unique: forall b t t',
    subtrace_log b t t' ->
    forall b' t'',
      subtrace_log b' t t'' ->
      b' = b /\ t'' = t'.
Proof.
  induction 1; intros.

  - inv H0.
    apply IHsubtrace_log in H3; auto.
    intuition.

  - inv H0.
    + apply IHsubtrace_log in H5; auto.
      intuition.
      congruence.
    + apply IHsubtrace_log in H5; auto.
      intuition.
      congruence.

  - inv H; auto.

  - inv H0.
    apply IHsubtrace_log in H3; auto.
    intuition.

  - inv H0; auto.
    apply IHsubtrace_log in H5; auto.
    intuition.
    congruence.
Qed.

Lemma subtrace_log_concat: forall b t t',
    subtrace_log b t t' ->
    forall e,
      if b then subtrace_log b (map PL.Op e ++ t) (e ++ t')
      else subtrace_log b (map PL.Op e ++ t) t'.
Proof.
  induction e ; intros.
  - simpl. destruct b; auto.
  - destruct b.
    + simpl. econstructor; eauto.
    + simpl. econstructor; eauto.
Qed.

Lemma subtrace_log_ops: forall op,
    subtrace_log false (map PL.Op op) [].
Proof.
  induction op.
  - constructor.
  - simpl. econstructor; eauto.
Qed.

Alternative, equivalent definition of the subtrace relation subtrace_log, easier to use in the proof of refinement.
Inductive subtrace_log_alt : bool -> PL.trace -> PLO.trace -> Prop :=
| committed_aend : forall b t t',
    subtrace_log_alt b t t' ->
    subtrace_log_alt true (PL.LogS :: t) t'
| committed_acons : forall e t t',
    subtrace_log_alt true t t' ->
    subtrace_log_alt true (map PL.Op e ++ t) (e ++ t')
| ignored_anil : subtrace_log_alt false [] []
| ignored_aend : forall b t t',
    subtrace_log_alt b t t' ->
    subtrace_log_alt false (PL.LogF :: t) t'
| ignored_acons : forall e t t',
    subtrace_log_alt false t t' ->
    subtrace_log_alt false (map PL.Op e ++ t) t'.

Lemma subtrace_log_subtrace_log_alt : forall b t t',
    subtrace_log b t t' ->
    subtrace_log_alt b t t'.
Proof.
  induction 1; intros; try solve [econstructor; eauto].
  - replace (PL.Op e :: t) with (map PL.Op (e::nil) ++ t) by auto with datatypes.
    replace (e:: t') with ([e] ++ t') by auto with datatypes.
    econstructor ; eauto.
  - replace (PL.Op e :: t) with (map PL.Op (e::nil) ++ t) by auto with datatypes.
    econstructor ; eauto.
Qed.
  
Lemma subtrace_log_alt_subtrace_log: forall b t t',
    subtrace_log_alt b t t' ->
    subtrace_log b t t'.
Proof.
  induction 1; intros; try solve [econstructor; eauto].
  - eapply subtrace_log_concat in IHsubtrace_log_alt; eauto.
  - eapply subtrace_log_concat in IHsubtrace_log_alt; eauto.
Qed.

Refinement proof


Converting a PL state into a PLO state by including the oracle.
Definition lift_log (o : oracle) (s: PLstate): PLOstate :=
  match s with
  | PLF.INIT => PLFO.INIT o
  | PLF.USR x x0 x1 => PLFO.USR o x x0 x1
  | PLF.DRV x x0 x1 x2 => PLFO.DRV o x x0 x1 x2
  | PLF.PWR x => PLFO.PWR o x
  | PLF.OFF x => PLFO.OFF o x
  end.

Helper lemma to reason about the empty oracle -- the empty trace is produced.
Lemma empty_run: forall s t s',
    (exists s0, lift_log [] s0 = s) ->
    run PLO.step s t s' ->
    exists s'2, t = [] /\ lift_log [] s'2 = s'.
Proof.
  intros.
  induction H0; intros; auto.
  - inv H0;
      destruct H as [s0 H3]; destruct s0; inv H3.
    + exists (PLF.USR MCU.init DEV.init CHKPT.init).
      try eexists; try split; simpl; eauto.
    + exists (PLF.USR mcu' dev' chkpt);
        try eexists; try split; simpl; eauto.
      eapply SPEC.axiom_usr; eauto.
    + exists (PLF.DRV mcu' dev' (CHKPT.next_log chkpt) (CHKPT.saveNextMCU chkpt mcu));
        try eexists; try split; simpl; eauto.
      eapply SPEC.axiom_enter; eauto.
    + exists (PLF.PWR (CHKPT.saveNextMCU chkpt mcu));
        try eexists; try split; simpl; eauto.
    + exists (PLF.OFF (CHKPT.set chkpt));
        try eexists; try split; simpl; eauto.
    + exists (PLF.USR (CHKPT.last_mcu chkpt) (LOG.restore (CHKPT.last_log chkpt))
                      (CHKPT.reset chkpt)); try eexists; try split; simpl; eauto.
  - destruct H as [s Hs].
    eexists; eauto.
  - apply IHrun1 in H.
    destruct H as [s2 [-> Hs2]].
    simpl.
    eapply IHrun2.
    eauto.
Qed.

Helper lemma to exhibit the oracle generating the subtrace.
Lemma gen_logging_oracle : forall si t sf,
    run_right PL.step si t sf ->
    exists
      (o : oracle) (t' : list DEV.ops)
      (sf' : PLFO.state),
      run PLO.step (lift_log o si) t' sf'
      /\
      match o with
      | [] => subtrace_log_alt false t t'
      | true :: _ => subtrace_log_alt true t t'
      | false :: _ => subtrace_log_alt false t t'
      end.
Proof.
  intros.
  induction H.
  - (* refl *)
    exists [].
    exists [].
    exists (lift_log [] x).
    repeat split; try eapply run_refl; econstructor.
    
  - (* step *)
    enough (CASE x t1 y); [| constructor].
    destruct IHrun_right as [o [t' [sf' [Hrun Hsub]]]].
    destruct STEP.
    + (* INIT -> USR *)
      simpl.
      eexists o.
      eexists t'.
      eexists sf'.
      repeat split; auto.
      change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step; econstructor; eauto.
    + (* USR -> USR *)
      simpl.
      eexists o.
      eexists t'.
      eexists sf'.
      pose proof (SPEC.axiom_usr _ _ _ _ _ INSTR) as [-> ->].
      repeat split; auto.
      change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step; econstructor; eauto.
    + (* USR -> DRV *)
      destruct o; [|destruct b].
      * (* ignoring *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.
      * (* committing *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.
      * (* ignoring *)
        eexists.
        eexists.
        eexists.
        pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]].
        repeat split; eauto.
        eapply run_trans; eauto.
        eapply run_step.
        econstructor; eauto.
        simpl. assumption.

    + (* DRV -> DRV *)
      destruct o; [|destruct b].
      * (* o ~ nil *)
        eexists [].
        eexists [].
        exists ((lift_log [] (PLF.DRV mcu dev l chkpt))).
        repeat split.
        -- eapply run_refl.
        -- apply ignored_acons.
           apply empty_run in Hrun as [_ [-> _]];
             auto.
           eexists; eauto.
      * eexists (true :: o).
        eexists (t ++ t').
        eexists sf'.
        repeat split; eauto.
        -- simpl.
           eapply run_trans; eauto.
           eapply run_step.
           simpl.
           change t with (if true then t else []).
           eapply PLO.sem_drv; eauto.
        -- econstructor.
           auto.
      * exists (false :: o).
        exists ([] ++ t').
        exists sf'.
        repeat split; eauto.
        ++ eapply run_trans; eauto.
           eapply run_step.
           simpl.
           change [] with (if false then t else []).
           eapply PLO.sem_drv; eauto.
        ++ econstructor; auto.

    + (* DRV -> USR *)
      eexists.
      eexists.
      eexists.
      pose proof (SPEC.axiom_leave _ _ _ _ _ INSTR) as [-> [-> ->]].
      repeat split; eauto.
      eapply run_trans; eauto.
      eapply run_step.
      econstructor; eauto.
      simpl.
      destruct o; [| destruct b];
        (econstructor; eauto).

    + (* USR -> PWR *)
      eexists.
      eexists.
      eexists.
      repeat split; eauto.
      simpl. change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step.
      econstructor; eauto.
    + (* DRV -> PWR *)
      eexists (false :: o).
      eexists ([] ++ t').
      eexists.
      repeat split; eauto.
      -- eapply run_trans; eauto.
         eapply run_step.
         apply PLO.sem_pwr_drv.
      -- simpl.
         destruct o; [| destruct b]; (econstructor; eauto).
         
    + (* PWR -> OFF *)
      eexists.
      eexists.
      eexists.
      repeat split; eauto.
      simpl. change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step.
      econstructor; eauto.
    + (* OFF -> USR *)
      eexists.
      eexists.
      eexists.
      repeat split; eauto.
      simpl. change t' with ([] ++ t').
      eapply run_trans; eauto.
      eapply run_step.
      econstructor; eauto.
Qed.

Validity of logging oracle.
Lemma logging_validity : forall t,
    PL.sem t ->
    exists o t', PLO.sem o t' /\ exists b, subtrace_log b t t'.
Proof.
  intros t [s Hsem].
  eapply run_run_right in Hsem.
  apply gen_logging_oracle in Hsem as [o [t' [sf' [Hrun H]]]].
  exists o.
  exists t'.
  split.
  - econstructor; eauto.
  - destruct o; eauto using subtrace_log_alt_subtrace_log.
    destruct b; eauto using subtrace_log_alt_subtrace_log.
Qed.