Library mcertikos.multithread.phbthread.INVLemmaSingleInterrupt

Require Import Coqlib.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import AuxLemma.
Require Import DeviceStateDataType.

Require Import Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import AST.
Require Import AuxStateDataType.
Require Import ObjInterruptManagement.
Require Import Omega.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import GlobalOracleProp.
Require Import INVLemmaMemory.
Require Import RealParams.

Require Import AuxSingleAbstractDataType.
Require Import ObjPHBThreadDEV.
Require Import SingleConfiguration.

Section INTERRUPT_INV.

  Section INTR_DISABLE.
    Context `{real_params_ops: RealParamsOps}.
    Context `{multi_oracle_prop: MultiOracleProp}.
    Context `{threads_conf_ops: ThreadsConfigurationOps}.

    Lemma single_serial_intr_disable_aux_preserves_all:
      ∀ n masked d d´,
        single_serial_intr_disable n masked d = ret d´ →
        CPU_ID (fst d) = CPU_ID (fst d´) ∧
        cid (fst d) = cid (fst d´) ∧
        ti (snd d) = ti (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        AC (snd d) = AC (snd d´) ∧
        init (fst d) = init (fst d´) ∧
        ikern (snd d) = ikern (snd d´) ∧
        ihost (snd d) = ihost (snd d´) ∧
        pg (fst d) = pg (fst d´) ∧
        MM (fst d) = MM (fst d´) ∧
        MMSize (fst d) = MMSize (fst d´) ∧
        CR3 (fst d) = CR3 (fst d´) ∧
        nps (fst d) = nps (fst d´) ∧
        pperm (snd d) = pperm (snd d´) ∧
        ipt (snd d) = ipt (snd d´) ∧
        PT (snd d) = PT (snd d´) ∧
        ptpool (snd d) = ptpool (snd d´) ∧
        HP (snd d) = HP (snd d´) ∧
        cid (fst d) = cid (fst d´) ∧
        syncchpool (snd d) = syncchpool (snd d´) ∧
        uctxt (snd d) = uctxt (snd d´) ∧
        ept (snd d) = ept (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        tf (snd d) = tf (snd d´) ∧
        big_oracle (fst d) = big_oracle (fst d´) ∧
        big_log (fst d) = big_log (fst d´) ∧
        lock (fst d) = lock (fst d´) ∧
        vmxinfo (fst d) = vmxinfo (fst d´).
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        repeat (split; [reflexivity|]); try reflexivity.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H.
          simpl in H.
          apply H.
        }
        {
          eapply IHn in H.
          functional inversion Hdestruct1; subst;
          simpl in *; eauto.
        }
        {
          inv H.
          repeat (split; [reflexivity|]); try reflexivity.
        }
      }
    Qed.

    Lemma single_serial_intr_disable_preserves_all:
      ∀ d d´,
        single_serial_intr_disable_spec d = ret d´ →
        CPU_ID (fst d) = CPU_ID (fst d´) ∧
        cid (fst d) = cid (fst d´) ∧
        ti (snd d) = ti (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        AC (snd d) = AC (snd d´) ∧
        init (fst d) = init (fst d´) ∧
        ikern (snd d) = ikern (snd d´) ∧
        ihost (snd d) = ihost (snd d´) ∧
        pg (fst d) = pg (fst d´) ∧
        MM (fst d) = MM (fst d´) ∧
        MMSize (fst d) = MMSize (fst d´) ∧
        CR3 (fst d) = CR3 (fst d´) ∧
        nps (fst d) = nps (fst d´) ∧
        pperm (snd d) = pperm (snd d´) ∧
        ipt (snd d) = ipt (snd d´) ∧
        PT (snd d) = PT (snd d´) ∧
        ptpool (snd d) = ptpool (snd d´) ∧
        HP (snd d) = HP (snd d´) ∧
        cid (fst d) = cid (fst d´) ∧
        syncchpool (snd d) = syncchpool (snd d´) ∧
        uctxt (snd d) = uctxt (snd d´) ∧
        ept (snd d) = ept (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        tf (snd d) = tf (snd d´) ∧
        big_oracle (fst d) = big_oracle (fst d´) ∧
        big_log (fst d) = big_log (fst d´) ∧
        lock (fst d) = lock (fst d´) ∧
        vmxinfo (fst d) = vmxinfo (fst d´).
    Proof.
      intros.
      Opaque single_serial_intr_disable.
      functional inversion H; simpl;
      destruct d´0; destruct d´;
      destruct d; simpl in *; inv H0;
      apply (single_serial_intr_disable_aux_preserves_all
               INTR_DISABLE_REC_MAX masked (d, d2 {pv_in_intr : true}) (s, d1));
      assumption.
      Transparent single_serial_intr_disable.
    Qed.

    Require Import FutureTactic.
    Lemma single_serial_intr_disable_cr2_injection:
      ∀ d d´ m,
        single_serial_intr_disable_spec d = ret d´ →
        val_inject (Mem.flat_inj m) (snd (ti (snd d))) (snd (ti (snd d))) →
        val_inject (Mem.flat_inj m) (snd (ti (snd d´))) (snd (ti (snd d´))).
    Proof.
      intros. generalize (single_serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H4.
      assumption.
    Qed.

    Lemma single_serial_intr_disable_cr2_type:
      ∀ d d´,
        single_serial_intr_disable_spec d = ret d´ →
        Val.has_type (snd (ti (snd d))) Tint →
        Val.has_type (snd (ti (snd d´))) Tint.
    Proof.
      intros. generalize (single_serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H4.
      assumption.
    Qed.

    Lemma single_serial_intr_disable_preserves_tf:
      ∀ d d´,
        single_serial_intr_disable_spec d = Some d´ →
        tf (snd d) = tf (snd d´).
    Proof.
      intros.
      generalize (single_serial_intr_disable_preserves_all d d´ H); intro.
      destruct H0 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]; try assumption).
    Qed.

    Lemma single_serial_intr_disable_uctxt_INJECT:
      ∀ d d´ m,
        single_serial_intr_disable_spec d = ret d´ →
        priv_uctxt_inject_neutral (uctxt (snd d)) m →
        priv_uctxt_inject_neutral (uctxt (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H23.
      assumption.
    Qed.

    Lemma single_serial_intr_disable_VMCS_inject_neutral:
      ∀ d d´ m,
        single_serial_intr_disable_spec d = ret d´ →
        VMCS_inject_neutral (vmcs (snd d)) m →
        VMCS_inject_neutral (vmcs (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H25.
      assumption.
    Qed.

    Lemma single_serial_intr_disable_VMX_inject_neutral:
      ∀ d d´ m,
        single_serial_intr_disable_spec d = ret d´ →
        VMX_inject_neutral (vmx (snd d)) m →
        VMX_inject_neutral (vmx (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H26.
      assumption.
    Qed.

  End INTR_DISABLE.

  Section INTR_ENABLE.

    Context `{multi_oracle_prop: MultiOracleProp}.
    Context `{big_oracle_ops: BigOracleOps}.
    Context `{real_params_ops: RealParamsOps}.
    Context `{threads_conf_ops: ThreadsConfigurationOps}.

    Lemma single_serial_intr_enable_aux_preserves_all:
      ∀ n d d´,
        single_serial_intr_enable n d = ret d´ →
        CPU_ID (fst d) = CPU_ID (fst d´) ∧
        cid (fst d) = cid (fst d´) ∧
        ti (snd d) = ti (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        AC (snd d) = AC (snd d´) ∧
        init (fst d) = init (fst d´) ∧
        ikern (snd d) = ikern (snd d´) ∧
        ihost (snd d) = ihost (snd d´) ∧
        pg (fst d) = pg (fst d´) ∧
        MM (fst d) = MM (fst d´) ∧
        MMSize (fst d) = MMSize (fst d´) ∧
        CR3 (fst d) = CR3 (fst d´) ∧
        nps (fst d) = nps (fst d´) ∧
        pperm (snd d) = pperm (snd d´) ∧
        ipt (snd d) = ipt (snd d´) ∧
        PT (snd d) = PT (snd d´) ∧
        ptpool (snd d) = ptpool (snd d´) ∧
        HP (snd d) = HP (snd d´) ∧
        cid (fst d) = cid (fst d´) ∧
        syncchpool (snd d) = syncchpool (snd d´) ∧
        uctxt (snd d) = uctxt (snd d´) ∧
        ept (snd d) = ept (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        tf (snd d) = tf (snd d´) ∧
        big_oracle (fst d) = big_oracle (fst d´) ∧
        big_log (fst d) = big_log (fst d´) ∧
        lock (fst d) = lock (fst d´) ∧
        vmxinfo (fst d) = vmxinfo (fst d´).
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        repeat (split; [reflexivity|]); try reflexivity.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H.
          functional inversion Hdestruct0; subst;
          simpl in *; eauto.
        }
        {
          inv H.
          repeat (split; [reflexivity|]); try reflexivity.
        }
      }
    Qed.

    Lemma single_serial_intr_enable_preserves_all:
      ∀ d d´,
        single_serial_intr_enable_spec d = ret d´ →
        CPU_ID (fst d) = CPU_ID (fst d´) ∧
        cid (fst d) = cid (fst d´) ∧
        ti (snd d) = ti (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        AC (snd d) = AC (snd d´) ∧
        init (fst d) = init (fst d´) ∧
        ikern (snd d) = ikern (snd d´) ∧
        ihost (snd d) = ihost (snd d´) ∧
        pg (fst d) = pg (fst d´) ∧
        MM (fst d) = MM (fst d´) ∧
        MMSize (fst d) = MMSize (fst d´) ∧
        CR3 (fst d) = CR3 (fst d´) ∧
        nps (fst d) = nps (fst d´) ∧
        pperm (snd d) = pperm (snd d´) ∧
        ipt (snd d) = ipt (snd d´) ∧
        PT (snd d) = PT (snd d´) ∧
        ptpool (snd d) = ptpool (snd d´) ∧
        HP (snd d) = HP (snd d´) ∧
        cid (fst d) = cid (fst d´) ∧
        syncchpool (snd d) = syncchpool (snd d´) ∧
        uctxt (snd d) = uctxt (snd d´) ∧
        ept (snd d) = ept (snd d´) ∧
        vmcs (snd d) = vmcs (snd d´) ∧
        vmx (snd d) = vmx (snd d´) ∧
        tf (snd d) = tf (snd d´) ∧
        big_oracle (fst d) = big_oracle (fst d´) ∧
        big_log (fst d) = big_log (fst d´) ∧
        lock (fst d) = lock (fst d´) ∧
        vmxinfo (fst d) = vmxinfo (fst d´).
    Proof.
      intros.
      Opaque single_serial_intr_enable.
      functional inversion H; simpl.
      destruct d; destruct abd´;
      destruct d´; simpl in *; inv H0;
      apply (single_serial_intr_enable_aux_preserves_all INTR_ENABLE_REC_MAX (d, d0 { pv_in_intr : true}) (s, d2)); assumption.
      Transparent single_serial_intr_enable.
    Qed.

    Require Import FutureTactic.
    Lemma single_serial_intr_enable_cr2_injection:
      ∀ d d´ m,
        single_serial_intr_enable_spec d = ret d´ →
        val_inject (Mem.flat_inj m) (snd (ti (snd d))) (snd (ti (snd d))) →
        val_inject (Mem.flat_inj m) (snd (ti (snd d´))) (snd (ti (snd d´))).
    Proof.
      intros. generalize (single_serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H4.
      assumption.
    Qed.

    Lemma single_serial_intr_enable_cr2_type:
      ∀ d d´,
        single_serial_intr_enable_spec d = ret d´ →
        Val.has_type (snd (ti (snd d))) Tint →
        Val.has_type (snd (ti (snd d´))) Tint.
    Proof.
      intros. generalize (single_serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H4.
      assumption.
    Qed.

    Lemma single_serial_intr_enable_preserves_tf:
      ∀ d d´,
        single_serial_intr_enable_spec d = Some d´ →
        tf (snd d) = tf (snd d´).
    Proof.
      intros.
      generalize (single_serial_intr_enable_preserves_all d d´ H); intro.
      destruct H0 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]; try assumption).
    Qed.

    Lemma single_serial_intr_enable_uctxt_INJECT:
      ∀ d d´ m,
        single_serial_intr_enable_spec d = ret d´ →
        priv_uctxt_inject_neutral (uctxt (snd d)) m →
        priv_uctxt_inject_neutral (uctxt (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H23.
      assumption.
    Qed.

    Lemma single_serial_intr_enable_VMCS_inject_neutral:
      ∀ d d´ m,
        single_serial_intr_enable_spec d = ret d´ →
        VMCS_inject_neutral (vmcs (snd d)) m →
        VMCS_inject_neutral (vmcs (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H25.
      assumption.
    Qed.

    Lemma single_serial_intr_enable_VMX_inject_neutral:
      ∀ d d´ m,
        single_serial_intr_enable_spec d = ret d´ →
        VMX_inject_neutral (vmx (snd d)) m →
        VMX_inject_neutral (vmx (snd d´)) m.
    Proof.
      intros. generalize (single_serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre.
      destruct d; destruct d´; simpl in ×.
      rewrite <- H26.
      assumption.
    Qed.

  End INTR_ENABLE.

End INTERRUPT_INV.

Ltac rest :=
  match goal with
    | Hs: single_serial_intr_disable_spec _ = _ |- _⇒
      pose proof (single_serial_intr_disable_preserves_all _ _ Hs) as Hs´;
        blast Hs´; eauto
    | Hs: single_serial_intr_enable_spec _ = _ |- _⇒
      pose proof (single_serial_intr_enable_preserves_all _ _ Hs) as Hs´;
        blast Hs´; eauto
  end.

Create HintDb single_serial_intr_disable_invariantdb discriminated.

Hint Resolve single_serial_intr_disable_cr2_injection: serial_intr_disable_invariantdb.
Hint Resolve single_serial_intr_disable_cr2_type: serial_intr_disable_invariantdb.
Hint Resolve single_serial_intr_disable_uctxt_INJECT: serial_intr_disable_invariantdb.
Hint Resolve single_serial_intr_disable_VMCS_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve single_serial_intr_disable_VMX_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve single_serial_intr_disable_preserves_tf: serial_intr_disable_invariantdb.

Create HintDb sinble_serial_intr_enable_invariantdb discriminated.

Hint Resolve single_serial_intr_enable_cr2_injection: serial_intr_enable_invariantdb.
Hint Resolve single_serial_intr_enable_cr2_type: serial_intr_enable_invariantdb.
Hint Resolve single_serial_intr_enable_uctxt_INJECT: serial_intr_enable_invariantdb.
Hint Resolve single_serial_intr_enable_VMCS_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve single_serial_intr_enable_VMX_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve single_serial_intr_enable_preserves_tf: serial_intr_enable_invariantdb.