Library mcertikos.multithread.phbthread.PHBThread


Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
Require Import LAsm.
Require Import LoadStoreSemPHB.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalRealIntelModule.

Require Import INVLemmaContainer.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaSingleInterrupt.
Require Import INVLemmaProc.

Require Import I64Layer.
Require Import IntelPrimSemantics.
Require Import PUCtxtIntroDef.
Require Import INVLemmaIntel.

Require Import AlgebraicMem.

Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import ObjPHBThreadVMM.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadINTELVIRT.

Require Import FutureTactic.

Section WITHMEM.

  Context `{real_params_ops: RealParamsOps}.
  Context `{multi_oracle_ops : MultiOracleProp}.

  Context `{s_config: SingleConfiguration (spl_data := single_data)}.

  Context `{Hmwd: UseMemWithData mem}.
  Context `{Hstencil: Stencil}.

  Record high_level_invariant (abd: PData) :=
     mkInvariant {
         CPU_ID_range: 0 (CPU_ID (fst abd)) < TOTAL_CPU;
         valid_curid: 0 ZMap.get (CPU_ID (fst abd)) (cid (fst abd)) < num_proc
       }.

  Global Instance phbthread_data_ops : CompatDataOps PData :=
    {
      empty_data := (init_shared_adt, main_init_priv_adt);
      high_level_invariant := high_level_invariant;
      low_level_invariant := low_level_invariant;
      kernel_mode adt := ikern (snd adt) = true ihost (snd adt) = true
    }.

Proofs that the initial abstract_data should satisfy the invariants

  Section Property_Abstract_Data.

    Lemma empty_data_high_level_invariant:
      high_level_invariant (init_shared_adt, main_init_priv_adt).
    Proof.
      constructor; simpl; intros; auto; try inv H.
      - apply GlobalOracle.current_CPU_ID_range.
      - unfold init_real_cidpool.
        simpl.
        case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
        rewrite ZMap.gi; omega.
    Qed.

Definition of the abstract state

    Global Instance phbthread_data_prf : CompatData PData.
    Proof.
      constructor.
      - apply low_level_invariant_incr.
      - apply empty_data_low_level_invariant.
      - apply empty_data_high_level_invariant.
    Qed.

  End Property_Abstract_Data.


  Section INV.

    Lemma kernel_mode_eq: (d : PData),
      ikern (snd d) = true ihost (snd d) = true kernel_mode d.
    Proof.
      intros; split; auto.
    Qed.

    Global Instance single_big_palloc_spec_inv: PreservesInvariants single_big_palloc_spec.
    Proof.
      econstructor; intros; inv_generic_sem H.
      - unfold single_big_palloc_spec in H2; subdestruct; simpl; inv H2; simpl.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
      - unfold single_big_palloc_spec in H2; subdestruct; simpl; inv H2; simpl;
        unfold single_big_palloc_spec_share in Hdestruct7; subdestruct; inv Hdestruct7; simpl in ×.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
      - unfold single_big_palloc_spec in H2; subdestruct; simpl; inv H2; simpl;
        unfold single_big_palloc_spec_share in Hdestruct7; subdestruct; inv Hdestruct7; simpl in ×.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
        + destruct d; simpl in *; inv H0; constructor; auto.
    Qed.

    Global Instance single_setPT_spec_inv: PreservesInvariants single_setPT_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Section pt_Resv_INV.

      Lemma single_big_palloc_spec_preserve_kernel_mode :
       n adt adt´ res,
        single_big_palloc_spec n adt = Some (adt´, res)
        ikern (snd adt) = true ihost (snd adt) = true
        ikern (snd adt´) = true ihost (snd adt´) = true.
      Proof.
        intros.
        unfold single_big_palloc_spec in H.
        subdestruct; substx; simpl; inv H; auto.
      Qed.

      Lemma single_big_ptInsert_spec_preserve_kernel_mode :
         n1 n2 n3 n4 adt adt´ res,
          single_big_ptInsert_spec n1 n2 n3 n4 adt = Some (adt´, res)
          ikern (snd adt) = true ihost (snd adt) = true
          ikern (snd adt´) = true ihost (snd adt´) = true.
      Proof.
        intros.
        functional inversion H; subst.
        - functional inversion H11; simpl; auto.
        - functional inversion H11; subst; simpl;
          eauto using single_big_palloc_spec_preserve_kernel_mode; try congruence; eauto.
        - functional inversion H11; functional inversion H13; simpl; eauto.
      Qed.

      Lemma single_big_ptResv_spec_preserve_kernel_mode:
       i i0 i1 adt adt´ res,
        single_big_ptResv_spec i i0 i1 adt = Some (adt´, res)
        ikern (snd adt) = true ihost (snd adt) = true
        ikern (snd adt´) = true ihost (snd adt´) = true.
      Proof.
        intros.
        functional inversion H; subst.
        - eapply single_big_palloc_spec_preserve_kernel_mode; eassumption.
        - eapply single_big_ptInsert_spec_preserve_kernel_mode; eauto.
          eapply single_big_palloc_spec_preserve_kernel_mode; eassumption.
      Qed.

      Lemma single_big_palloc_spec_preserve_high_level_inv :
       n adt adt´ res,
        single_big_palloc_spec n adt = Some (adt´, res)
        CompatData.high_level_invariant adt
        CompatData.high_level_invariant adt´.
      Proof.
        intros.
        unfold single_big_palloc_spec in H.
        unfold single_big_palloc_spec_share in H.
        destruct adt, adt´.
        subdestruct; substx; simpl; inv H0; auto; inv H.
        - auto; simpl in *; constructor; simpl; auto.
        - auto; simpl in *; constructor; simpl; auto.
        - auto; simpl in *; constructor; simpl; auto.
        - auto; simpl in *; constructor; simpl; auto.
      Qed.

      Lemma single_big_ptInsert_spec_preserve_high_level_inv :
         n1 n2 n3 n4 adt adt´ res,
          single_big_ptInsert_spec n1 n2 n3 n4 adt = Some (adt´, res)
          CompatData.high_level_invariant adt
          CompatData.high_level_invariant adt´.
      Proof.
        intros.
        functional inversion H; subst; destruct adt, adt´; simpl in ×.
        - functional inversion H11; simpl; auto.
          substx; inv H0; constructor; simpl; auto.
        - functional inversion H11; subst; simpl; auto.
          + exploit single_big_palloc_spec_preserve_high_level_inv; eauto.
          + exploit single_big_palloc_spec_preserve_high_level_inv; eauto; intros.
            destruct ; simpl in ×.
            inv H1; constructor; simpl; auto.
        - destruct ; functional inversion H11; subst.
          + exploit single_big_palloc_spec_preserve_high_level_inv; eauto; intros.
            functional inversion H13; simpl; substx; inv H1; constructor; auto.
          + exploit single_big_palloc_spec_preserve_high_level_inv; eauto; intros.
            functional inversion H13; simpl; substx; inv H1; constructor; auto.
      Qed.

      Lemma single_big_ptResv_spec_preserve_high_level_inv:
       i i0 i1 adt adt´ res,
        single_big_ptResv_spec i i0 i1 adt = Some (adt´, res)
        CompatData.high_level_invariant adt
        CompatData.high_level_invariant adt´.
      Proof.
        intros.
        functional inversion H; subst.
        - eapply single_big_palloc_spec_preserve_high_level_inv; eassumption.
        - eapply single_big_ptInsert_spec_preserve_high_level_inv; eauto.
          eapply single_big_palloc_spec_preserve_high_level_inv; eassumption.
      Qed.

      Lemma single_big_palloc_spec_preserve_low_level_inv:
         n adt adt´ res m,
          single_big_palloc_spec n adt = Some (adt´, res)
          CompatData.low_level_invariant m adt
          CompatData.low_level_invariant m adt´.
      Proof.
        intros.
        unfold single_big_palloc_spec in H.
        subdestruct; inv H; simpl in *; auto.
        - inv H0; constructor; simpl; auto.
        - inv H0; constructor; simpl; auto.
        - inv H0; constructor; simpl; auto.
      Qed.

      Lemma single_big_ptInsert_spec_preserve_low_level_inv:
         n1 n2 n3 n4 adt adt´ res m,
          single_big_ptInsert_spec n1 n2 n3 n4 adt = Some (adt´, res)
          CompatData.low_level_invariant m adt
          CompatData.low_level_invariant m adt´.
      Proof.
        intros.
        functional inversion H; subst.
        - functional inversion H11; simpl; auto.
          inv H0; constructor; auto.
        - functional inversion H11; subst;
          [unfold single_big_palloc_spec in H20;
            subdestruct; inversion H20; substx; simpl in *; eauto; inv H0; constructor; auto | try congruence; auto].
        - functional inversion H11; functional inversion H13; substx; simpl.
          + eapply single_big_palloc_spec_preserve_low_level_inv in H21; eauto.
            destruct ; simpl.
            inv H21; constructor; eauto.
          + simpl in ×.
            eapply single_big_palloc_spec_preserve_low_level_inv in H21; eauto.
            destruct d´0; simpl.
            inv H21; constructor; eauto.
      Qed.

      Lemma single_big_ptResv_spec_preserve_low_level_inv:
         i i0 i1 adt adt´ res m,
          single_big_ptResv_spec i i0 i1 adt = Some (adt´, res)
          CompatData.low_level_invariant m adt
          CompatData.low_level_invariant m adt´.
      Proof.
        intros.
        functional inversion H; subst.
        - eapply single_big_palloc_spec_preserve_low_level_inv; eauto.
        - eapply single_big_ptInsert_spec_preserve_low_level_inv; eauto.
          eapply single_big_palloc_spec_preserve_low_level_inv; eauto.
      Qed.

      Global Instance single_big_ptResv_spec_inv: PreservesInvariants single_big_ptResv_spec.
      Proof.
        econstructor; intros; inv_generic_sem H.
        - eauto using single_big_ptResv_spec_preserve_low_level_inv.
        - eauto using single_big_ptResv_spec_preserve_high_level_inv.
        - inv H0; unfold kernel_mode; simpl.
          eauto using single_big_ptResv_spec_preserve_kernel_mode.
      Qed.

    End pt_Resv_INV.

    Global Instance single_cli_spec_inv: PreservesInvariants single_cli_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.

    Global Instance single_sti_spec_inv: PreservesInvariants single_sti_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.

    Global Instance single_big_acquire_lock_SC_spec_inv: PreservesInvariants single_big_acquire_lock_SC_spec.
    Proof.
      econstructor; intros; inv_generic_sem H.
      - unfold ret in H2; simpl in ×.
        unfold single_big_acquire_lock_SC_spec in H2.
        subdestruct.
        inv H2.
        destruct d.
        inv H0; simpl in ×.
        unfold single_big_acquire_lock_SC_spec_share in Hdestruct1; subdestruct; simpl in *; auto.
        inv Hdestruct1; econstructor; auto.
        inv Hdestruct1; econstructor; auto.
      - unfold ret in H2; simpl in ×.
        unfold single_big_acquire_lock_SC_spec in H2.
        unfold single_big_acquire_lock_SC_spec_share in H2.
        subdestruct; inv H2.
        + destruct d; simpl in *; inv H0; constructor; simpl in *; auto.
        + destruct d; simpl in *; inv H0; constructor; simpl in *; auto.
      - unfold ret in H2; simpl in ×.
        unfold single_big_acquire_lock_SC_spec in H2.
        subdestruct.
        inv H2.
        destruct d; simpl in ×.
        unfold single_big_acquire_lock_SC_spec_share in Hdestruct; subdestruct; simpl in *; auto;
        inv Hdestruct; auto.
    Qed.

    Global Instance single_big_release_lock_SC_spec_inv: PreservesInvariants single_big_release_lock_SC_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto.
      - unfold single_big_release_lock_SC_spec_share in H3.
        subdestruct; inv H2; destruct d; simpl in *; inv H3; simpl; auto.
      - unfold single_big_release_lock_SC_spec_share in H3.
        subdestruct; inv H2; destruct d; simpl in *; inv H3; simpl; auto.
    Qed.

    Global Instance single_set_sync_chan_busy_spec_inv: PreservesInvariants single_set_sync_chan_busy_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Global Instance single_ipc_send_body_spec_inv: PreservesInvariants single_big_ipc_send_body_spec.
    Proof.
      constructor; simpl; intros; inv_generic_sem H.
      - functional inversion H2.
        functional inversion H11.
        inversion H; substx.
        inv H25.
        inv H0; constructor; eauto.
      - functional inversion H2.
        functional inversion H11.
        inversion H; substx.
        inv H25.
        inv H0; constructor; eauto.
      - functional inversion H2.
        functional inversion H11.
        inversion H; substx.
        inv H25.
        inv H0; constructor; eauto.
    Qed.

    Section IPC_RECEIVE.

      Lemma single_big_ipc_receive_body_low_level_inv:
         fromid vaddr count d n ,
          single_big_ipc_receive_body_spec fromid vaddr count d = Some (, n)
          low_level_invariant d
          low_level_invariant .
      Proof.
        intros.
        functional inversion H; subst; eauto.
        functional inversion H11.
        inv H0; constructor; simpl; auto.
      Qed.

      Lemma single_big_ipc_receive_body_high_level_inv:
         fromid vaddr count d n,
          single_big_ipc_receive_body_spec fromid vaddr count d = Some (, n)
          high_level_invariant d
          high_level_invariant .
      Proof.
        intros.
        functional inversion H; subst; eauto.
        functional inversion H11.
        inv H0; constructor; simpl; auto.
      Qed.

      Lemma single_big_ipc_receive_body_kernel_mode:
         fromid vaddr count d n,
          single_big_ipc_receive_body_spec fromid vaddr count d = Some (, n)
          kernel_mode d
          kernel_mode .
      Proof.
        intros.
        functional inversion H; subst; eauto.
        functional inversion H11.
        inv H0; constructor; simpl; auto.
      Qed.

      Global Instance single_big_ipc_receive_body_spec_inv: PreservesInvariants single_big_ipc_receive_body_spec.
      Proof.
        constructor; simpl; intros; inv_generic_sem H.
        - eapply single_big_ipc_receive_body_low_level_inv; eauto.
        - eapply single_big_ipc_receive_body_high_level_inv; eauto.
        - eapply single_big_ipc_receive_body_kernel_mode; eauto.
      Qed.

    End IPC_RECEIVE.

    Global Instance single_serial_intr_disable_spec_inv: PreservesInvariants single_serial_intr_disable_spec.
    Proof.
      constructor; simpl; intros; inv_generic_sem H.
      Opaque single_serial_intr_disable.
      - generalize (single_serial_intr_disable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in ×.
        econstructor; simpl; inv H0; eauto.
        + rewrite <- H4; eauto.
        + rewrite <- H4; eauto.
        + rewrite <- H23; eauto.
        + rewrite <- H25; eauto.
        + rewrite <- H26; eauto.
        + rewrite <- H27; eauto.
      - generalize (single_serial_intr_disable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in *; inv H0; constructor; simpl in ×.
        + rewrite <- H1; auto.
        + rewrite <- H1, <- H3; auto.
      - generalize (single_serial_intr_disable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in *; eauto.
        Transparent single_serial_intr_disable.
    Qed.

    Global Instance single_serial_intr_enable_spec_inv: PreservesInvariants single_serial_intr_enable_spec.
    Proof.
      constructor; simpl; intros; inv_generic_sem H.
      Opaque single_serial_intr_enable.
      - generalize (single_serial_intr_enable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in ×.
        econstructor; simpl; inv H0; eauto.
        + rewrite <- H4; eauto.
        + rewrite <- H4; eauto.
        + rewrite <- H23; eauto.
        + rewrite <- H25; eauto.
        + rewrite <- H26; eauto.
        + rewrite <- H27; eauto.
      - generalize (single_serial_intr_enable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in *; inv H0; constructor; simpl in ×.
        + rewrite <- H1; auto.
        + rewrite <- H1, <- H3; auto.
      - generalize (single_serial_intr_enable_preserves_all _ _ H2).
        intros Hpre.
        blast Hpre; destruct d, ; simpl in *; eauto.
        Transparent single_serial_intr_enable.
    Qed.

    Global Instance single_serial_putc_spec_inv: PreservesInvariants single_serial_putc_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Global Instance single_cons_buf_read_spec_inv: PreservesInvariants single_cons_buf_read_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
    Qed.



    Global Instance single_hostin_spec_inv: PrimInvariants single_hostin_spec (data_ops := phbthread_data_ops).
    Proof.
      constructor; intros until ; intros Hspec Hinv; functional inversion Hspec;
      inv Hinv; try subst; constructor; auto; simpl in *;
      intros; functional inversion H0; destruct d; simpl in *; auto.
    Qed.

    Global Instance single_hostout_spec_inv: PrimInvariants single_hostout_spec (data_ops := phbthread_data_ops).
    Proof.
      constructor; intros until ; intros Hspec Hinv; functional inversion Hspec;
      inv Hinv; try subst; constructor; auto; simpl in *;
      intros; functional inversion H0; destruct d; simpl in *; auto.
    Qed.

    Global Instance thread_proc_create_inv: PCreateInvariants single_big_proc_create_spec.
    Proof.
      constructor; intros; inv H0;
      unfold single_big_proc_create_spec in *; unfold single_big_proc_create_spec_share;
      destruct d; subdestruct; inv H; simpl; auto.
      -
        constructor; trivial; intros; simpl in ×.
      - simpl in ×.
        functional inversion Hdestruct8; substx.
        constructor; trivial; intros; simpl in ×.
    Qed.


    Global Instance single_big_thread_wakeup_spec_inv: PreservesInvariants single_big_thread_wakeup_spec.
    Proof.
      preserves_invariants_simpl_auto.
      - destruct d; simpl in ×.
        functional inversion H5; simpl in *; eauto.
      - destruct d; simpl in ×.
        functional inversion H5; simpl in *; eauto.
    Qed.

    Global Instance single_yield_dummy_spec_inv: PreservesInvariants single_yield_dummy_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.

    Global Instance single_sleep_dummy_spec_inv: PreservesInvariants single_sleep_dummy_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.


    Global Instance single_big_sched_init_inv: PreservesInvariants single_big_sched_init_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
      - destruct d; simpl in ×.
        rewrite <- _x2.
        rewrite ZMap.gss.
        auto.
    Qed.

    Global Instance single_uctx_set_inv: PreservesInvariants single_uctx_set_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
      constructor.
      - eapply uctxt_inject_neutral0_gss; eauto.
        eapply uctxt_inject_neutral0_Vint.
      - simpl.
        eapply uctxt_inject_neutral0_gss; eauto.
        eapply uctxt_inject_neutral0_Vint.
    Qed.

    Global Instance single_proc_start_user_inv: TMStartUserInvariants single_proc_start_user_spec.
    Proof.
      constructor; intros; functional inversion H; inv H0.
      - constructor; trivial.
      - subst. constructor; auto; simpl in *; intros; congruence.
    Qed.

    Global Instance single_proc_exit_user_inv: TMExitUserInvariants single_proc_exit_user_spec.
    Proof.
      constructor; intros; functional inversion H; inv H0.
      - constructor; trivial.
        constructor; simpl.
        + unfold uctx4.
          repeat eapply uctxt_inject_neutral0_gss;
          try eapply uctxt_inject_neutral0_Vint; auto.
          eapply uctxt_inject_neutral0_init; auto.
        + simpl.
          unfold uctx4.
          repeat eapply uctxt_inject_neutral0_gss;
          try eapply uctxt_inject_neutral0_Vint; auto.
          eapply uctxt_inject_neutral0_init; auto.
      - constructor; auto; simpl in *; intros.
        Grab Existential Variables.
        auto.
    Qed.

    Global Instance single_proc_start_user_inv2: TMStartUserInvariants2 single_proc_start_user_spec.
    Proof.
      constructor; intros; functional inversion H; inv H0.
      - constructor; trivial.
      - subst. constructor; auto; simpl in *; intros; congruence.
    Qed.

    Global Instance single_proc_exit_user_inv2: TMExitUserInvariants2 single_proc_exit_user_spec.
    Proof.
      constructor; intros; functional inversion H; inv H0.
      - constructor; trivial.
        constructor; simpl.
        + unfold uctx4.
          repeat eapply uctxt_inject_neutral0_gss;
            try eapply uctxt_inject_neutral0_Vint; auto.
          eapply uctxt_inject_neutral0_init; auto.
        + unfold uctx4.
          repeat eapply uctxt_inject_neutral0_gss;
            try eapply uctxt_inject_neutral0_Vint; auto.
          eapply uctxt_inject_neutral0_init; auto.
      - constructor; auto; simpl in *; intros.
        Grab Existential Variables.
        auto.
    Qed.

    Global Instance single_proc_create_postinit_inv:
      PreservesInvariants single_proc_create_postinit_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Section INTELVMSUPPORT.

      Section SINGLE_INTERCEPT_INTWIN.

        Lemma single_vmx_set_intercept_intwin_high_inv:
           d i,
            single_vmx_set_intercept_intwin_spec i d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_intercept_intwin_low_inv:
           d n i,
            single_vmx_set_intercept_intwin_spec i d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          intros; inv H0; functional inversion H; constructor; simpl; intros; try congruence; eauto 2.
          - eapply VMCS_inject_neutral_gss_Vint; eauto.
          - eapply VMCS_inject_neutral_gss_Vint; eauto.
        Qed.

        Lemma single_vmx_set_intercept_intwin_kernel_mode:
           d i,
            single_vmx_set_intercept_intwin_spec i d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_intercept_intwin_inv: PreservesInvariants single_vmx_set_intercept_intwin_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_intercept_intwin_low_inv; eauto.
          - eapply single_vmx_set_intercept_intwin_high_inv; eauto.
          - eapply single_vmx_set_intercept_intwin_kernel_mode; eauto.
        Qed.

      End SINGLE_INTERCEPT_INTWIN.

      Section SINGLE_SET_DESC1.

        Lemma single_vmx_set_desc1_high_inv:
           d i i0 i1,
            single_vmx_set_desc1_spec i i0 i1 d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_desc1_low_inv:
           d n i i0 i1,
            single_vmx_set_desc1_spec i i0 i1 d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          destruct d; destruct ; simpl in ×.
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
          simpl in *; substx.
          functional inversion H9.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT.
            eauto.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT.
            eauto.
        Qed.

        Lemma single_vmx_set_desc1_kernel_mode:
           d i i0 i1,
            single_vmx_set_desc1_spec i i0 i1 d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_desc1_inv: PreservesInvariants single_vmx_set_desc1_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_desc1_low_inv; eauto.
          - eapply single_vmx_set_desc1_high_inv; eauto.
          - eapply single_vmx_set_desc1_kernel_mode; eauto.
        Qed.

      End SINGLE_SET_DESC1.

      Section SINGLE_SET_DESC2.

        Lemma single_vmx_set_desc2_high_inv:
           d i i0 i1,
            single_vmx_set_desc2_spec i i0 i1 d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_desc2_low_inv:
           d n i i0 i1,
            single_vmx_set_desc2_spec i i0 i1 d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          destruct d; destruct .
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
          simpl in *; substx.
          functional inversion H9.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT.
            auto.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT.
            auto.
        Qed.

        Lemma single_vmx_set_desc2_kernel_mode:
           d i i0 i1,
            single_vmx_set_desc2_spec i i0 i1 d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_desc2_inv: PreservesInvariants single_vmx_set_desc2_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_desc2_low_inv; eauto.
          - eapply single_vmx_set_desc2_high_inv; eauto.
          - eapply single_vmx_set_desc2_kernel_mode; eauto.
        Qed.

      End SINGLE_SET_DESC2.

      Section SINGLE_INJECT_EVENT.

        Lemma single_vmx_inject_event_high_inv:
           d i i0 i1 i2,
            single_vmx_inject_event_spec i i0 i1 i2 d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; substx; simpl; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_inject_event_low_inv:
           d n i i0 i1 i2,
            single_vmx_inject_event_spec i i0 i1 i2 d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          intros.
          destruct d, .
          inv H0; functional inversion H; simpl in *; substx; simpl; constructor; simpl; intros; try congruence; eauto 2.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT; auto.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT; auto.
        Qed.

        Lemma single_vmx_inject_event_kernel_mode:
           d i i0 i1 i2,
            single_vmx_inject_event_spec i i0 i1 i2 d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; substx; constructor; trivial.
        Qed.

        Global Instance single_vmx_inject_event_inv: PreservesInvariants single_vmx_inject_event_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_inject_event_low_inv; eauto.
          - eapply single_vmx_inject_event_high_inv; eauto.
          - eapply single_vmx_inject_event_kernel_mode; eauto.
        Qed.

      End SINGLE_INJECT_EVENT.

      Section SINGLE_SET_TSC_OFFSET.

        Lemma single_vmx_set_tsc_offset_high_inv:
           d i,
            single_vmx_set_tsc_offset_spec i d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_tsc_offset_low_inv:
           d n i,
            single_vmx_set_tsc_offset_spec i d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          intros.
          destruct d, .
          inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
          simpl in *; substx.
          - repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
            rewrite H8 in VMCS_INJECT; auto.
        Qed.

        Lemma single_vmx_set_tsc_offset_kernel_mode:
           d i,
            single_vmx_set_tsc_offset_spec i d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_tsc_offset_inv: PreservesInvariants single_vmx_set_tsc_offset_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_tsc_offset_low_inv; eauto.
          - eapply single_vmx_set_tsc_offset_high_inv; eauto.
          - eapply single_vmx_set_tsc_offset_kernel_mode; eauto.
        Qed.

      End SINGLE_SET_TSC_OFFSET.

      Section SINGLE_SET_REG.

        Lemma single_vmx_set_reg_high_inv:
           d i i0,
            single_vmx_set_reg_spec i i0 d = Some
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros; inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_reg_low_inv:
           d n i i0,
            single_vmx_set_reg_spec i i0 d = Some
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          intros.
          destruct d, .
          inv H0; functional inversion H; subst; simpl; constructor; simpl; intros; try congruence; eauto 2.
          simpl in *; substx.
          - eapply VMX_inject_neutral_gss_Vint; eauto.
          - eapply VMCS_inject_neutral_gss_Vint; eauto.
        Qed.

        Lemma single_vmx_set_reg_kernel_mode:
           d i i0,
            single_vmx_set_reg_spec i i0 d = Some
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_reg_inv: PreservesInvariants single_vmx_set_reg_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_reg_low_inv; eauto.
          - eapply single_vmx_set_reg_high_inv; eauto.
          - eapply single_vmx_set_reg_kernel_mode; eauto.
        Qed.

      End SINGLE_SET_REG.

      Section SINGLE_SET_MMAP.

        Lemma single_vmx_set_mmap_high_inv:
           d i i0 i1 v,
            single_vmx_set_mmap_spec i i0 i1 d = Some (, v)
            high_level_invariant d
            high_level_invariant .
        Proof.
          intros.
          inv H0; functional inversion H; functional inversion H3; subst; simpl;
          constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_mmap_low_inv:
           d n i i0 i1 v,
            single_vmx_set_mmap_spec i i0 i1 d = Some (, v)
            low_level_invariant n d
            low_level_invariant n .
        Proof.
          intros.
          inv H0; functional inversion H; functional inversion H3; subst; simpl;
          constructor; simpl; intros; try congruence; eauto 2.
        Qed.

        Lemma single_vmx_set_mmap_kernel_mode:
           d i i0 i1 v,
            single_vmx_set_mmap_spec i i0 i1 d = Some (, v)
            kernel_mode d
            kernel_mode .
        Proof.
          intros; functional inversion H; functional inversion H4; subst; constructor; trivial.
        Qed.

        Global Instance single_vmx_set_mmap_inv: PreservesInvariants single_vmx_set_mmap_spec.
        Proof.
          preserves_invariants_simpl´.
          - eapply single_vmx_set_mmap_low_inv; eauto.
          - eapply single_vmx_set_mmap_high_inv; eauto.
          - eapply single_vmx_set_mmap_kernel_mode; eauto.
        Qed.

      End SINGLE_SET_MMAP.

      Global Instance single_vmx_run_inv: VMXEnterInvariants single_vm_run_spec.
      Proof.
        constructor; intros;
        unfold single_vm_run_spec in *;
        subdestruct; inv H; simpl; auto.
        -
          inv H1. constructor; trivial; intros; simpl in ×.
          + eapply VMCS_inject_neutral_gss_Vint; eauto.
          + eapply VMX_inject_neutral_gss_enter; eauto.
        -
          inv H0. constructor; simpl; eauto 2; try congruence; intros.
      Qed.

      Global Instance single_vmx_return_from_guest_inv: VMXReturnInvariants single_vmx_return_from_guest_spec.
      Proof.
        constructor; intros;
        unfold single_vmx_return_from_guest_spec in *;
        subdestruct; inv H; simpl; auto.
        -
          inv H0. constructor; trivial; intros; simpl in ×.
          repeat eapply VMX_inject_neutral_gss_Vint; eauto.
        -
          inv H0. constructor; simpl; eauto 2; try congruence; intros.
      Qed.

      Global Instance single_vmx_init_inv: VMCSSetDefaultsInvariants single_vmx_init_spec.
      Proof.
        constructor; intros; functional inversion H.
        -
          destruct d; destruct ; simpl in ×.
          unfold pv_adt, sh_adt in ×.
          inv H7; subst.
          inv H6; constructor; trivial; intros; simpl in *; eauto.
          + generalize max_unsigned_val; intro muval.
            inv VMCS_INJECT.
            unfold Calculate_VMCS_at_i.
            repeat (eapply VMCS_inject_neutral_gss_Vint_same
                           || eapply VMCS_inject_neutral_gss_same); eauto 1;
            split; econstructor; eauto;
            try (generalize (H7 ofs); intros tmp; destruct tmp; eauto);
            try (unfold Int.add; simpl; repeat rewrite Int.unsigned_repr);
            try rewrite Z.add_0_r; try reflexivity;
            try rewrite Z.add_0_r; try reflexivity; try omega.
          + unfold Calculate_VMX_at_i; simpl.
            repeat eapply VMX_inject_neutral_gss_Vint.
            assumption.
        -
          inv H1; subst.
          inv H0. constructor; simpl; try congruence; intros; eauto.
        -
          inv H1; simpl; auto.
      Qed.

    End INTELVMSUPPORT.

  End INV.

  Definition single_exec_loadex {F V} := single_exec_loadex (F := F) (V := V).

  Definition single_exec_storeex {F V} := single_exec_storeex (single_flatmem_store:= single_flatmem_store) (F := F) (V := V).

  Global Instance single_flatmem_store_inv: Single_FlatmemStoreInvariant (single_flatmem_store:= single_flatmem_store).
  Proof.
    split; inversion 1; intros.
    - functional inversion H0. split; trivial.
    - functional inversion H1.
      split; simpl; try (eapply dirty_ppage_store_unmaped´; try reflexivity; try eassumption); trivial.
  Qed.

  Global Instance single_trapinfo_set_inv: Single_TrapinfoSetInvariant.
  Proof.
    split; inversion 1; intros; constructor; auto.
  Qed.

  Definition phbthread : compatlayer (cdata PData) :=
    vmxinfo_get gensem single_vmxinfo_get_spec
           palloc gensem single_big_palloc_spec
           set_pt gensem single_setPT_spec
           pt_read gensem single_ptRead_spec
           pt_resv gensem single_big_ptResv_spec

          
           thread_wakeup gensem single_big_thread_wakeup_spec
           thread_yield gensem single_yield_dummy_spec
           thread_sleep gensem single_sleep_dummy_spec
           sched_init gensem single_big_sched_init_spec

          

           uctx_get gensem single_uctx_get_spec
           uctx_set gensem single_uctx_set_spec
           proc_create proc_create_compatsem single_big_proc_create_spec

           container_get_nchildren gensem single_container_get_nchildren_spec
           container_get_quota gensem single_container_get_quota_spec
           container_get_usage gensem single_container_get_usage_spec
           container_can_consume gensem single_container_can_consume_spec

           get_CPU_ID gensem single_get_CPU_ID_spec
           get_curid gensem single_get_curid_spec

           acquire_lock_CHAN gensem single_big_acquire_lock_SC_spec
           release_lock_CHAN gensem single_big_release_lock_SC_spec
           get_sync_chan_busy gensem single_get_sync_chan_busy_spec
           set_sync_chan_busy gensem single_set_sync_chan_busy_spec

          

           ipc_send_body gensem single_big_ipc_send_body_spec
           ipc_receive_body gensem single_big_ipc_receive_body_spec

           rdmsr gensem single_rdmsr_spec
           wrmsr gensem single_wrmsr_spec
           vmx_set_intercept_intwin gensem single_vmx_set_intercept_intwin_spec
           vmx_set_desc1 gensem single_vmx_set_desc1_spec
           vmx_set_desc2 gensem single_vmx_set_desc2_spec
           vmx_inject_event gensem single_vmx_inject_event_spec
           vmx_set_tsc_offset gensem single_vmx_set_tsc_offset_spec
           vmx_get_tsc_offset gensem single_vmx_get_tsc_offset_spec
           vmx_get_exit_reason gensem single_vmx_get_exit_reason_spec
           vmx_get_exit_fault_addr gensem single_vmx_get_exit_fault_addr_spec
           vmx_get_exit_qualification gensem single_vmx_get_exit_qualification_spec
           vmx_check_pending_event gensem single_vmx_check_pending_event_spec
           vmx_check_int_shadow gensem single_vmx_check_int_shadow_spec
           vmx_get_reg gensem single_vmx_get_reg_spec
           vmx_set_reg gensem single_vmx_set_reg_spec

           vmx_get_next_eip gensem single_vmx_get_next_eip_spec
           vmx_get_io_width gensem single_vmx_get_io_width_spec
           vmx_get_io_write gensem single_vmx_get_io_write_spec
           vmx_get_exit_io_rep gensem single_vmx_get_exit_io_rep_spec
           vmx_get_exit_io_str gensem single_vmx_get_exit_io_str_spec
           vmx_get_exit_io_port gensem single_vmx_get_exit_io_port_spec
           vmx_set_mmap gensem single_vmx_set_mmap_spec
           vmx_run_vm primcall_vmx_enter_compatsem single_vm_run_spec vmx_run_vm
           vmx_return_from_guest primcall_vmx_return_compatsem single_vmx_return_from_guest_spec
           vmx_init vmcs_set_defaults_compatsem single_vmx_init_spec

           cli gensem single_cli_spec
           sti gensem single_sti_spec

           serial_intr_disable gensem single_serial_intr_disable_spec
           serial_intr_enable gensem single_serial_intr_enable_spec
           serial_putc gensem single_serial_putc_spec
           cons_buf_read gensem single_cons_buf_read_spec

          
           host_in primcall_general_compatsem single_hostin_spec
           host_out primcall_general_compatsem single_hostout_spec
           proc_create_postinit gensem single_proc_create_postinit_spec

           trap_get primcall_trap_info_get_compatsem single_trap_info_get_spec
           trap_set primcall_trap_info_ret_compatsem single_trap_info_ret_spec

           proc_start_user primcall_start_user_tm_compatsem single_proc_start_user_spec
           proc_exit_user primcall_exit_user_tm_compatsem single_proc_exit_user_spec
           proc_start_user2 primcall_start_user_tm_compatsem2 single_proc_start_user_spec
           proc_exit_user2 primcall_exit_user_tm_compatsem2 single_proc_exit_user_spec

           accessors {| exec_load := @single_exec_loadex; exec_store := @single_exec_storeex |}.

End WITHMEM.