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
}.
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.
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.
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 d´; simpl in ×.
inv H1; constructor; simpl; auto.
- destruct d´; 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 d´; 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 d´ n n´,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
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 d´ n,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
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 d´ n,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
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, 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, 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, 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, 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, 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, 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 d´; 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 d´; 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 d´ i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; inv H0; functional inversion H; constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma single_vmx_set_intercept_intwin_low_inv:
∀ d d´ n i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
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 d´ i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
destruct d; destruct d´; 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 d´ i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
destruct d; destruct d´.
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 d´ i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i,
single_vmx_set_tsc_offset_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i,
single_vmx_set_tsc_offset_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i,
single_vmx_set_tsc_offset_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
low_level_invariant n d →
low_level_invariant n d´.
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 d´ i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
kernel_mode d →
kernel_mode d´.
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 d´; 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.
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 d´; simpl in ×.
inv H1; constructor; simpl; auto.
- destruct d´; 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 d´; 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 d´ n n´,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
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 d´ n,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
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 d´ n,
single_big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
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, 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, 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, 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, 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, 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, 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 d´; 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 d´; 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 d´ i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; inv H0; functional inversion H; constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma single_vmx_set_intercept_intwin_low_inv:
∀ d d´ n i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
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 d´ i,
single_vmx_set_intercept_intwin_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
destruct d; destruct d´; 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 d´ i i0 i1,
single_vmx_set_desc1_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
destruct d; destruct d´.
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 d´ i i0 i1,
single_vmx_set_desc2_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i i0 i1 i2,
single_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i,
single_vmx_set_tsc_offset_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i,
single_vmx_set_tsc_offset_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i,
single_vmx_set_tsc_offset_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
destruct d, 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 d´ i i0,
single_vmx_set_reg_spec i i0 d = Some d´→
kernel_mode d →
kernel_mode d´.
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 d´ i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
high_level_invariant d →
high_level_invariant d´.
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 d´ n i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
low_level_invariant n d →
low_level_invariant n d´.
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 d´ i i0 i1 v,
single_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
kernel_mode d →
kernel_mode d´.
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 d´; 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.