Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Import SPEC.
Require Import plf.
Require Import PL.
Require Import PLFO.
Require Import PLO.

Refinement proof : PLO.sem o ⊆ SPEC.sem

Simulation relation between PLO state and SPEC states.

Inductive match_states : PLOstate -> SPEC.state -> Prop :=
| match_states_init : forall oracle,
    match_states (INIT oracle)
                 (STATE Usr MCU.init DEV.init)

| match_states_usr : forall oracle mcu dev dev' chkpt,
    forall (WFINV: DEV.equiv (LOG.restore (CHKPT.next_log chkpt)) dev)
           (EQUIV: DEV.equiv dev dev'),
      match_states (USR oracle mcu dev chkpt)
                   (STATE Usr mcu dev')

| match_states_drv_fail : forall oracle dev' mcu dev l chkpt,
    forall (WFINV: DEV.equiv (LOG.restore l) dev)
           (EQUIV: DEV.equiv (LOG.restore (CHKPT.next_log chkpt)) dev')
           (ORACLE: match oracle with
                    | (false::_) | [] => True
                    | _ => False
                    end),
      match_states (DRV oracle mcu dev l chkpt)
                   (STATE Usr (CHKPT.next_mcu chkpt) dev')

| match_states_drv_success : forall oracle mcu dev dev' l chkpt,
    forall (WFINV: DEV.equiv (LOG.restore l) dev)
           (EQUIV: DEV.equiv dev dev'),
      match_states (DRV (true::oracle) mcu dev l chkpt)
                   (STATE Drv mcu dev')

| match_states_pwr : forall oracle chkpt dev,
    forall (WFINV: DEV.equiv (LOG.restore (CHKPT.next_log chkpt)) dev),
      match_states (PWR oracle chkpt)
                   (STATE Usr (CHKPT.next_mcu chkpt) dev)

| match_states_off : forall oracle chkpt dev,
    forall (WFINVLOG: CHKPT.next_log chkpt = CHKPT.last_log chkpt)
           (WFINVMCU: CHKPT.next_mcu chkpt = CHKPT.last_mcu chkpt)
           (DEV: DEV.equiv (LOG.restore (CHKPT.next_log chkpt)) dev),
      match_states (OFF oracle chkpt)
                   (STATE Usr (CHKPT.next_mcu chkpt) dev).

Star-simulation diagram between PLO and SPEC.

Lemma match_states_step: forall s1 t s2,
    forall (STEP: PLO.step s1 t s2)
           as1
           (MATCH: match_states s1 as1),
      (exists as2, run SPEC.step as1 t as2 /\ match_states s2 as2).

Proof.

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

  induction 1; intros.

  - (* first boot *)
    inv MATCH.
    exists (SPEC.STATE SPEC.Usr MCU.init DEV.init).
    split; [| repeat constructor; auto].
    + simpl. apply run_refl.
    + apply LOG.restore_init.
    + apply equiv_refl.
      apply DEV.equiv_equiv.

  - (*  usr step *)
    inv MATCH.
    pose proof (SPEC.axiom_usr _ _ _ _ _ INSTR) as [-> ->]; eauto.
    edestruct SPEC.axiom_equiv with (1:= EQUIV) as [dev'' Hstep]; eauto.
    pose proof (SPEC.axiom_usr _ _ _ _ _ Hstep) as [-> _]; eauto.
    eexists. split.
    + apply run_step.
      eauto.
    + constructor; auto.

  - (* From userland to drv *)
    inv MATCH.
    pose proof (SPEC.axiom_enter _ _ _ _ _ INSTR) as [-> [-> ->]]; eauto.
    edestruct SPEC.axiom_equiv with (1:= EQUIV) as [dev'' Hstep]; eauto.
    pose proof (SPEC.axiom_enter _ _ _ _ _ Hstep) as [-> _]; eauto.
    destruct oracle.
    + eexists.
      split.
      * apply run_refl.
      * eapply match_states_drv_fail; eauto.
        simpl.
        eapply DEV.equiv_equiv; eauto.
    + destruct b.
      -- (* Start a completed (in the future) power-continuous section *)
        {
          eexists; split.
          + apply run_step.
            eauto.
          + eapply match_states_drv_success; eauto.
        }
      -- (* Start an aborted (in the future) power-continuous section *)
        {
          eexists; split.
          + apply run_refl.
          + eapply match_states_drv_fail; eauto.
            simpl. eapply DEV.equiv_equiv; eauto.
        }

  - (* Committed in-drv operation *)
    inv MATCH; try destruct b; try contradiction.

    + (* in a failing power-continuous section *)
      eexists.
      split.
      * apply run_refl.
      * eapply match_states_drv_fail ; auto.
        pose proof (SPEC.axiom_drv _ _ _ _ _ INSTR).
        unfold LOG.log_ops in *. subst.
        eapply LOG.restore_log_trace; eauto.

    + (* in a successful power-continuous section *)
      edestruct SPEC.axiom_equiv with (2:= INSTR) as [dev'' Hstep]; eauto.
      eexists; split.
      * apply run_step; eauto.
      * econstructor; eauto.
        -- pose proof (SPEC.axiom_drv _ _ _ _ _ INSTR).
           unfold LOG.log_ops in *. subst.
           eapply LOG.restore_log_trace; eauto.
        -- pose proof (SPEC.axiom_drv _ _ _ _ _ Hstep).
           pose proof (SPEC.axiom_drv _ _ _ _ _ INSTR).
           eapply DEV.ops_sem_equiv; eauto.

  - (* From drv to userland *)
    inv MATCH; try contradiction.
    edestruct SPEC.axiom_equiv with (2:= INSTR) as [dev'' Hstep]; eauto.
    pose proof (SPEC.axiom_leave _ _ _ _ _ INSTR) as [<- [<- ->]].
    pose proof (SPEC.axiom_leave _ _ _ _ _ Hstep) as [<- _].
    eexists; split.
    * apply run_step.
      eauto.
    * econstructor; eauto.

  - (* pwr triggered from userland *)
    inv MATCH.
    eexists. split.
    + apply run_refl.
    + set (chkpt' := CHKPT.saveNextMCU chkpt mcu).
      assert (mcu = chkpt'.(CHKPT.next_mcu)) by auto.
      rewrite H0; clear H0.
      econstructor; eauto.
      eapply equiv_trans; eauto. apply DEV.equiv_equiv.

  - (* pwr triggered from drv *)
    inv MATCH.
    eexists. split.
    + apply run_refl.
    + econstructor; eauto.

  - (* switching off, chkp done *)
    inv MATCH.
    eexists. split.
    + apply run_refl.
    + destruct chkpt; simpl in *.
      econstructor; eauto.

  - (* reboot and restore *)
    inv MATCH.
    eexists. split.
    * apply run_refl.
    * destruct chkpt; simpl in *. subst.
      constructor; auto.
      eapply DEV.equiv_equiv.
Qed.

The simulation relation is preserved after any number of steps of PLO.

Lemma match_states_star : forall s1 t s2,
    run PLO.step s1 t s2 ->
    forall as1,
      match_states s1 as1 ->
      exists as2, run SPEC.step as1 t as2 /\ match_states s2 as2.

Proof.

  induction 1 ; intros.
  - eapply match_states_step; eauto.
  - exists as1; split; auto.
    apply run_refl.
  - eapply IHrun1 in H1.
    destruct H1 as [as2 [HSTEP HMATCH]].
    eapply IHrun2 in HMATCH.
    destruct HMATCH as [as3 [HSTEP2 HMATCH2]].
    exists as3; split; eauto.
    eapply run_trans; eauto.
Qed.

Trace inclusion result between PLO and SPEC.

Theorem logging_correctness: forall o t,
PLO.sem o t ->
SPEC.sem t.

Proof.

  unfold sem, SPEC.sem.
  intros o t [s STEP].
  eapply match_states_star in STEP; eauto.
  - destruct STEP as [as2 [STEPSTAR MATCH]].
    eauto.
  - constructor; try solve [apply LOG.restore_init].
Qed.

Module PLO_SPEC

Refinement proof : PLO.sem o ⊆ SPEC.sem