Library mcertikos.objects.dev.ObjX86

Require Import Coqlib.
Require Import Maps.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Constant.
Require Import AsmX.
Require Import LAsm.
Require Import XOmega.
Require Export DevicePrimSemantics.
Require Import AbstractDataType.
Require Import Integers.
Import ListNotations.
Require Import DeviceStateDataType.

Section OBJ_X86_Hardware.

    Local Open Scope Z_scope.

    Function save_context_spec (rs: Asm.regset) (abd: RData): RData :=
      abd {tf: tf abd ++ (mkTrapFrame rs (curr_intr_num abd) 0 (rs #ESP) :: nil)}.

    Function restore_context_spec (abd: RData): (regset × RData) :=
      match tf abd with
        | nil ⇒ (tf_regs tf_init_d, abd)
        | _ :: _ ⇒ (tf_regs (last (tf abd) tf_init_d), abd {tf: removelast (tf abd)})
      end.

    Function set_tf_spec (pc: val) (abd: AbstractDataType.RData) : option AbstractDataType.RData :=
      let t := last (tf abd) tf_init_d in
      Some (abd {tf: removelast (tf abd) ++ [t {tf_regs: (tf_regs t)#PC <- pc}]}).

End OBJ_X86_Hardware.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.

Local Open Scope Z_scope.

Section OBJ_SIM.

  Context `{data : CompatData RData}.
  Context `{data0 : CompatData RData}.

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.

  Notation HDATAOps := (cdata (cdata_prf := data) RData).
  Notation LDATAOps := (cdata (cdata_prf := data0) RData).

  Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
                               (stencil_ops:= stencil_ops) HDATAOps LDATAOps}.

  Lemma tfs_inj_rev: ∀ f tfs tfs´ tf tf´,
                       tfs_inj f tfs tfs´ →
                       tf_inj f tf tf´ →
                       tfs_inj f (tfs ++ (tf::nil)) (tfs´ ++ (tf´::nil)).
  Proof.
    intro f.
    induction tfs.
    intros.
    simpl in H.
    subdestruct.
    split; auto.
    inv H.
    intros.
    simpl in H.
    subdestruct.
    inv H.
    split; destruct H; auto.
  Qed.

  Lemma tfs_inj_last: ∀ f tfs tfs´ d,
                       tfs_inj f tfs tfs´ →
                       tfs ≠ nil →
                       tf_inj f (last tfs d) (last tfs´ d).
  Proof.
    intros.
    destruct tfs.
    congruence.
    destruct tfs´.
    simpl in H.
    inv H.
    clear H0.
    generalize dependent t0.
    generalize dependent t.
    generalize dependent tfs´.
    generalize dependent tfs.
    induction tfs.
    intros.
    simpl in ×.
    destruct H.
    subdestruct; auto.
    inv H0.

    intros.
    simpl.
    destruct tfs´.
    simpl in H.
    destruct H; auto.
    inv H0.
    simpl in ×.
    eapply IHtfs; auto.
    simpl in H.
    destruct H.
    destruct H0.
    auto.
  Qed.

  Lemma tfs_inj_removelast: ∀ f tfs tfs´,
                       tfs_inj f tfs tfs´ →
                       tfs ≠ nil →
                       tfs_inj f (removelast tfs) (removelast tfs´).
  Proof.
    intros.
    destruct tfs.
    congruence.
    destruct tfs´.
    simpl in H.
    inv H.
    clear H0.
    generalize dependent t0.
    generalize dependent t.
    generalize dependent tfs´.
    generalize dependent tfs.
    induction tfs.
    intros.
    simpl in ×.
    destruct H.
    subdestruct; auto.

    intros.
    simpl.
    destruct tfs´.
    simpl in H.
    destruct H; auto.
    split.
    simpl in H.
    destruct H; auto.
    simpl in IHtfs.
    simpl.
    eapply IHtfs; auto.
    simpl in H.
    destruct H.
    destruct H0.
    auto.
  Qed.

  Section SAVE_CONTEXT.

    Context {re1: relate_impl_tf}.
    Context {re2: relate_impl_curr_intr_num}.

    Lemma save_context_exists:
      ∀ s habd habd´ labd rs rs´ f,
        save_context_spec rs habd = habd´
        → relate_AbData s f habd labd
        → (∀ reg : PregEq.t,
              val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs´))
        → ∃ labd´, save_context_spec rs´ labd = labd´ ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold save_context_spec; intros.
      exploit relate_impl_tf_eq; eauto. intro.
      exploit relate_impl_curr_intr_num_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct; inv HQ.
      refine_split´; trivial.
      apply relate_impl_tf_update; trivial.
      eapply tfs_inj_rev; eauto.
      econstructor; eauto.
    Qed.

    Context {mt1: match_impl_tf}.

    Lemma save_context_match:
      ∀ s d d´ m rs f,
        save_context_spec rs d = d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold save_context_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_tf_update. assumption.
    Qed.

    Context {inv: SaveContextInvariants (data_ops:= data_ops) save_context_spec}.
    Context {inv0: SaveContextInvariants (data_ops:= data_ops0) save_context_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma save_context_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_save_context_compatsem save_context_spec)
            (id ↦ primcall_save_context_compatsem save_context_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
      inv H. inv H0. inv match_extcall_states.
      exploit save_context_exists; eauto 1.
      intros (labd´ & HP & HM).
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
      inv ASM_INV.
      unfold wt_regset in inv_reg_wt.
      eapply inv_reg_wt.
      inv ASM_INV.
      inv inv_inject_neutral.
      lift_simpl.
      unfold lift in inv_reg_inject_neutral; simpl in inv_reg_inject_neutral.
      intros; eapply inv_reg_inject_neutral; eauto.
      eapply save_context_match; eauto.
    Qed.

  End SAVE_CONTEXT.

  Section RESTORE_CONTEXT.

    Context {re1: relate_impl_tf}.
    Context {re2: relate_impl_curr_intr_num}.

    Lemma restore_context_exists:
      ∀ s habd habd´ labd rs f,
        restore_context_spec habd = (rs, habd´)
        → relate_AbData s f habd labd
        → ∃ labd´ rs´, restore_context_spec labd = (rs´, labd´) ∧ (∀ r : PregEq.t, val_inject f (rs r) (rs´ r)) ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold restore_context_spec; intros.
      exploit relate_impl_tf_eq; eauto. intro.
      exploit relate_impl_curr_intr_num_eq; eauto; inversion 1.
      revert H. subrewrite.
      destruct (tf habd).
      simpl in H1.
      subdestruct.
      inv HQ.
      refine_split´; trivial.
      inv H1.

      inv HQ.
      simpl in H1.
      subdestruct.
      inv H1.
      destruct H1.
      destruct t2.
      destruct t0.
      refine_split´; trivial.
      intros.
      unfold tf_inj in H.
      specialize (H r).
      destruct H.
      unfold Pregmap.get in H.
      assumption.
      apply relate_impl_tf_update; trivial.
      simpl in H1.
      inv H1.
      destruct t0.
      inv H1.
      refine_split´; trivial.
      intros.
      eapply tfs_inj_last; eauto.
      intro contra; inv contra.
      apply relate_impl_tf_update; trivial.
      econstructor.
      assumption.
      eapply tfs_inj_removelast; auto.
      intro.
      inv H3.
    Qed.

    Context {mt1: match_impl_tf}.

    Lemma restore_context_match:
      ∀ s d d´ m rs f,
        restore_context_spec d = (rs, d´)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold restore_context_spec; intros.
      destruct (tf d); inv H; trivial.
      eapply match_impl_tf_update. assumption.
    Qed.

    Context {inv: RestoreContextInvariants (data_ops:= data_ops) restore_context_spec}.
    Context {inv0: RestoreContextInvariants (data_ops:= data_ops0) restore_context_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma restore_context_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_restore_context_compatsem restore_context_spec)
            (id ↦ primcall_restore_context_compatsem restore_context_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
      inv H. inv H0. inv match_extcall_states.
      exploit restore_context_exists; eauto 1.
      intros (labd´ & rs´´ & HP & INJ & HM).
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
      unfold wt_regset in ×.
      intros.
      unfold restore_context_spec in HP.
      induction (tf d2).
      inv HP.
      constructor.
      inv HP.
      simpl in ×.
      destruct t.
      inv tf_INJECT.
      unfold tf_inject_neutral in H2.
      specialize (H2 r).
      destruct H2.
      assumption.
      inv tf_INJECT.
      assert (tf_inject_neutral (Mem.nextblock m2) (last (t :: t0) tf_init_d)).
      {
        eapply ListLemma.forall_last; eauto.
        constructor.
        simpl; auto.
        simpl.
        constructor.
      }
      unfold tf_inject_neutral in H0.
      specialize (H0 r).
      destruct H0.
      assumption.

      intros.
      unfold restore_context_spec in HP.
      induction (tf d2).
      inv HP.
      constructor.
      inv HP.
      simpl in ×.
      destruct t.
      inv tf_INJECT.
      unfold tf_inject_neutral in H2.
      specialize (H2 r).
      destruct H2.
      assumption.
      inv tf_INJECT.
      assert (tf_inject_neutral (Mem.nextblock m2) (last (t :: t0) tf_init_d)).
      {
        eapply ListLemma.forall_last; eauto.
        constructor.
        simpl; auto.
        simpl.
        constructor.
      }
      unfold tf_inject_neutral in H0.
      specialize (H0 r).
      destruct H0.
      assumption.
      eapply restore_context_match; eauto.
    Qed.

  End RESTORE_CONTEXT.

End OBJ_SIM.