Library mcertikos.objects.tmobj.ObjTMINTELVIRT

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.

Require Import CalRealIntelModule.
Require Import ObjVMX.
Require Import ObjVMCS.
Require Import liblayers.compat.CompatGenSem.
Require Import ObjEPT.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.

Require Import SingleOracle.

Section OBJ_SECOND_INTEL_VIRT.

  Context `{real_params_ops: RealParamsOps}.
  Context `{thread_conf_ops: ThreadsConfigurationOps}.

  Function thread_rdmsr_spec (r: Z) (adt: RData) : option Z64 := rdmsr_spec r adt.

  Function thread_wrmsr_spec (r: Z) (v: Z64) (adt: RData) := wrmsr_spec r v adt.

  Function thread_vmx_set_intercept_intwin_spec (enable: Z) (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_intercept_intwin_spec enable adt
         else None
    else None.

  Function thread_vmx_set_desc1_spec (seg sel base: Z) (adt: RData) : option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_desc1_spec seg sel base adt
         else None
    else None.

  Function thread_vmx_set_desc2_spec (seg lim ar: Z) (adt: RData) : option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_desc2_spec seg lim ar adt
         else None
    else None.

  Function thread_vmx_inject_event_spec (type vector errcode ev : Z) (adt: RData) : option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then
           vmx_inject_event_spec type vector errcode ev adt
         else None
    else None.

  Function thread_vmx_set_tsc_offset_spec (tsc_offset: Z64) (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_tsc_offset_spec tsc_offset adt
         else None
    else None.

  Function thread_vmx_get_tsc_offset_spec (adt: RData): option Z64 :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_tsc_offset_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_reason_spec (adt: RData) : option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_reason_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_fault_addr_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_fault_addr_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_qualification_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_qualification_spec adt
         else None
    else None.

  Function thread_vmx_check_pending_event_spec (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_check_pending_event_spec adt
         else None
    else None.

  Function thread_vmx_check_int_shadow_spec (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_check_int_shadow_spec adt
         else None
    else None.

  Function thread_vmx_get_reg_spec (reg: Z) (adt: RData) : option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_reg_spec reg adt
         else None
    else None.

  Function thread_vmx_set_reg_spec (reg v: Z) (adt: RData): option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_reg_spec reg v adt
         else None
    else None.

  Function thread_vmx_get_next_eip_spec (adt: RData) : option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_next_eip_spec adt
         else None
    else None.

  Function thread_vmx_get_io_width_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_io_width_spec adt
         else None
    else None.

  Function thread_vmx_get_io_write_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_io_write_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_io_rep_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_io_rep_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_io_str_spec (adt: RData): option Z :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_io_str_spec adt
         else None
    else None.

  Function thread_vmx_get_exit_io_port_spec (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_get_exit_io_port_spec adt
         else None
    else None.

  Function thread_vmx_set_mmap_spec (gpa : Z) (hpa : Z) (mem_type: Z) (adt: RData) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then if init adt then vmx_set_mmap_spec gpa hpa mem_type adt
         else None
    else None.

  Definition thread_vm_run_spec (rs: regset) (adt: RData) : option (RData × regset) :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then vm_run_spec rs adt
    else None.

  Function thread_vmx_return_from_guest_spec (adt: RData) : option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then vmx_return_from_guest_spec adt
    else None.

End OBJ_SECOND_INTEL_VIRT.

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

Local Open Scope Z_scope.

Section OBJ_SIM.

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

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

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

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

  Local Open Scope Z_scope.

  Context `{thread_conf_ops: ThreadsConfigurationOps}.

  Lemma val_inject_vint_eq:
    ∀ f n v v´ i,
      val_inject f (ZMap.get n v) (ZMap.get n v´)
      → ZMap.get n v = Vint i
      → ZMap.get n v´ = Vint i.
  Proof.
    intros.
    rewrite H0 in H; inversion H; reflexivity.
  Qed.

  Section THREAD_RDMSR_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.

    Lemma thread_rdmsr_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_rdmsr_spec)
            (id ↦ gensem thread_rdmsr_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      unfold thread_rdmsr_spec in ×.
      unfold rdmsr_spec in ×.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      revert H2; subrewrite. subdestruct.
      inv HQ; trivial.
    Qed.

  End THREAD_RDMSR_SIM.

  Section WRMSR_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.

    Lemma thread_wrmsr_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_wrmsr_spec)
            (id ↦ gensem thread_wrmsr_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      unfold thread_wrmsr_spec in ×.
      unfold wrmsr_spec in ×.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      revert H2; subrewrite. subdestruct.

      inv HQ; trivial.
    Qed.

  End WRMSR_SIM.

  Section THREAD_VMX_SET_INTERCEPT_INTWIN_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_set_intercept_intwin_exist:
      ∀ s habd habd´ labd enable f,
        thread_vmx_set_intercept_intwin_spec enable habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_intercept_intwin_spec enable labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_intercept_intwin_spec; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      exploit vmx_set_intercept_intwin_exist; eauto.
    Qed.

    Context {mt1: match_impl_vmcs}.

    Lemma thread_vmx_set_intercept_intwin_match:
      ∀ s d d´ m enable f,
        thread_vmx_set_intercept_intwin_spec enable d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_intercept_intwin_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_intercept_intwin_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_intercept_intwin_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_intercept_intwin_spec}.

    Lemma thread_vmx_set_intercept_intwin_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_intercept_intwin_spec)
            (id ↦ gensem thread_vmx_set_intercept_intwin_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_intercept_intwin_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_intercept_intwin_match; eauto.
    Qed.

  End THREAD_VMX_SET_INTERCEPT_INTWIN_SIM.

  Section THREAD_VMX_SET_DESC1_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_set_desc1_exist:
      ∀ s habd habd´ labd seg sel base f,
        thread_vmx_set_desc1_spec seg sel base habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_desc1_spec seg sel base labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_desc1_spec ; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      exploit vmx_set_desc1_exist; eauto.
    Qed.

    Context {mt1: match_impl_vmcs}.

    Lemma thread_vmx_set_desc1_match:
      ∀ s d d´ m seg sel base f,
        thread_vmx_set_desc1_spec seg sel base d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_desc1_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_desc1_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_desc1_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_desc1_spec}.

    Lemma thread_vmx_set_desc1_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_desc1_spec)
            (id ↦ gensem thread_vmx_set_desc1_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_desc1_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_desc1_match; eauto.
    Qed.

  End THREAD_VMX_SET_DESC1_SIM.

  Section THREAD_VMX_SET_DESC2_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_set_desc2_exist:
      ∀ s habd habd´ labd seg lim ar f,
        thread_vmx_set_desc2_spec seg lim ar habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_desc2_spec seg lim ar labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_desc2_spec ; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      exploit vmx_set_desc2_exist; eauto.
    Qed.

    Context {mt1: match_impl_vmcs}.

    Lemma thread_vmx_set_desc2_match:
      ∀ s d d´ m seg lim ar f,
        thread_vmx_set_desc2_spec seg lim ar d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_desc2_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_desc2_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_desc2_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_desc2_spec}.

    Lemma thread_vmx_set_desc2_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_desc2_spec)
            (id ↦ gensem thread_vmx_set_desc2_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_desc2_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_desc2_match; eauto.
    Qed.

  End THREAD_VMX_SET_DESC2_SIM.

  Section THREAD_VMX_INJECT_EVENT_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_inject_event_exist:
      ∀ s habd habd´ labd type vector errcode ev f,
        thread_vmx_inject_event_spec type vector errcode ev habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_inject_event_spec type vector errcode ev labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_inject_event_spec ; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      exploit vmx_inject_event_exist; eauto.
    Qed.

    Context {mt1: match_impl_vmcs}.

    Lemma thread_vmx_inject_event_match:
      ∀ s d d´ m type vecter errcode ev f,
        thread_vmx_inject_event_spec type vecter errcode ev d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_inject_event_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_inject_event_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_inject_event_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_inject_event_spec}.

    Lemma thread_vmx_inject_event_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_inject_event_spec)
            (id ↦ gensem thread_vmx_inject_event_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_inject_event_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_inject_event_match; eauto.
    Qed.

  End THREAD_VMX_INJECT_EVENT_SIM.

  Section THREAD_VMX_SET_TSC_OFFSET_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_set_tsc_offset_exist:
      ∀ s habd habd´ labd tsc_offset f,
        thread_vmx_set_tsc_offset_spec tsc_offset habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_tsc_offset_spec tsc_offset labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_tsc_offset_spec; intros.
      exploit relate_impl_CPU_ID_eq; eauto. inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      exploit vmx_set_tsc_offset_exist; eauto.
    Qed.

    Context {mt1: match_impl_vmcs}.

    Lemma thread_vmx_set_tsc_offset_match:
      ∀ s d d´ m tsc_offset f,
        thread_vmx_set_tsc_offset_spec tsc_offset d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_tsc_offset_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_tsc_offset_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_tsc_offset_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_tsc_offset_spec}.

    Lemma thread_vmx_set_tsc_offset_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_tsc_offset_spec)
            (id ↦ gensem thread_vmx_set_tsc_offset_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_tsc_offset_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_tsc_offset_match; eauto.
    Qed.

  End THREAD_VMX_SET_TSC_OFFSET_SIM.

  Section THREAD_VMX_GET_TSC_OFFSET_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_tsc_offset_exists:
      ∀ habd labd z s f,
        thread_vmx_get_tsc_offset_spec habd = Some z →
        relate_AbData s f habd labd →
        thread_vmx_get_tsc_offset_spec labd = Some z.
    Proof.
      unfold thread_vmx_get_tsc_offset_spec; intros.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_tsc_offset_exists.
    Qed.

    Lemma thread_vmx_get_tsc_offset_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_tsc_offset_spec)
            (id ↦ gensem thread_vmx_get_tsc_offset_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      erewrite thread_vmx_get_tsc_offset_exists; eauto.
      reflexivity.
    Qed.

  End THREAD_VMX_GET_TSC_OFFSET_SIM.

  Section THREAD_VMX_GET_EXIT_REASON_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_reason_exists:
      ∀ habd labd z s f,
        thread_vmx_get_exit_reason_spec habd = Some z →
        relate_AbData s f habd labd →
        thread_vmx_get_exit_reason_spec labd = Some z.
    Proof.
      unfold thread_vmx_get_exit_reason_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_reason_exists.
    Qed.

    Lemma thread_vmx_get_exit_reason_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_reason_spec)
            (id ↦ gensem thread_vmx_get_exit_reason_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      erewrite thread_vmx_get_exit_reason_exists; eauto.
      reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_REASON_SIM.

  Section THREAD_VMX_GET_EXIT_FAULT_ADDR_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_fault_addr_exists:
      ∀ habd labd z s f,
        thread_vmx_get_exit_fault_addr_spec habd = Some z →
        relate_AbData s f habd labd →
        thread_vmx_get_exit_fault_addr_spec labd = Some z.
    Proof.
      unfold thread_vmx_get_exit_fault_addr_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_fault_addr_exists.
    Qed.

    Lemma thread_vmx_get_exit_fault_addr_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_fault_addr_spec)
            (id ↦ gensem thread_vmx_get_exit_fault_addr_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      erewrite thread_vmx_get_exit_fault_addr_exists; eauto.
      reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_FAULT_ADDR_SIM.

  Section THREAD_VMX_GET_EXIT_QUALIFICATION_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_qualification_exist:
      ∀ s habd labd v f,
        thread_vmx_get_exit_qualification_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_exit_qualification_spec labd = Some v.
    Proof.
      unfold thread_vmx_get_exit_qualification_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_qualification_exist.
    Qed.

    Lemma thread_vmx_get_exit_qualification_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_qualification_spec)
            (id ↦ gensem thread_vmx_get_exit_qualification_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_exit_qualification_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_QUALIFICATION_SIM.

  Section THREAD_VMX_CHECK_PENDING_EVENT_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_init}.

    Lemma thread_vmx_check_pending_event_exists:
      ∀ habd labd z s f,
        thread_vmx_check_pending_event_spec habd = Some z →
        relate_AbData s f habd labd →
        thread_vmx_check_pending_event_spec labd = Some z.
    Proof.
      unfold thread_vmx_check_pending_event_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_check_pending_event_exists.
    Qed.

    Lemma thread_vmx_check_pending_event_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_check_pending_event_spec)
            (id ↦ gensem thread_vmx_check_pending_event_spec).
    Proof.
      Local Opaque Z.land.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      erewrite thread_vmx_check_pending_event_exists; eauto.
      reflexivity.
    Qed.

  End THREAD_VMX_CHECK_PENDING_EVENT_SIM.

  Section THREAD_VMX_CHECK_INT_SHADOW_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_init}.

    Lemma thread_vmx_check_int_shadow_exists:
      ∀ habd labd z s f,
        thread_vmx_check_int_shadow_spec habd = Some z →
        relate_AbData s f habd labd →
        thread_vmx_check_int_shadow_spec labd = Some z.
    Proof.
      unfold thread_vmx_check_int_shadow_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_check_int_shadow_exists.
    Qed.

    Lemma thread_vmx_check_int_shadow_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_check_int_shadow_spec)
            (id ↦ gensem thread_vmx_check_int_shadow_spec).
    Proof.
      Local Opaque Z.land.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      erewrite thread_vmx_check_int_shadow_exists; eauto.
      reflexivity.
    Qed.

  End THREAD_VMX_CHECK_INT_SHADOW_SIM.

  Section THREAD_VMX_GET_REG_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_init}.

    Lemma thread_vmx_get_reg_exist:
      ∀ s habd labd reg v f,
        thread_vmx_get_reg_spec reg habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_reg_spec reg labd = Some v.
    Proof.
      unfold thread_vmx_get_reg_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite; subdestruct.
      eauto using vmx_get_reg_exist.
    Qed.

    Lemma thread_vmx_get_reg_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_reg_spec)
            (id ↦ gensem thread_vmx_get_reg_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_reg_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_REG_SIM.

  Section THREAD_VMX_SET_REG_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_init}.

    Lemma thread_vmx_set_reg_exist:
      ∀ s habd habd´ labd reg v f,
        thread_vmx_set_reg_spec reg v habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_reg_spec reg v labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_reg_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite; subdestruct.
      eauto using vmx_set_reg_exist.
    Qed.

    Context {mt1: match_impl_vmx}.
    Context {mt2: match_impl_vmcs}.

    Lemma thread_vmx_set_reg_match:
      ∀ s d d´ m reg v f,
        thread_vmx_set_reg_spec reg v d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_reg_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_reg_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_reg_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_reg_spec}.

    Lemma thread_vmx_set_reg_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_reg_spec)
            (id ↦ gensem thread_vmx_set_reg_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_reg_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_reg_match; eauto.
    Qed.

  End THREAD_VMX_SET_REG_SIM.

  Section THREAD_VMX_GET_NEXT_EIP_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_init}.

    Lemma thread_vmx_get_next_eip_exist:
      ∀ s habd labd v f,
        thread_vmx_get_next_eip_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_next_eip_spec labd = Some v.
    Proof.
      unfold thread_vmx_get_next_eip_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_next_eip_exist.
    Qed.

    Lemma thread_vmx_get_next_eip_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_next_eip_spec)
            (id ↦ gensem thread_vmx_get_next_eip_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_next_eip_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_NEXT_EIP_SIM.

  Section THREAD_VMX_GET_IO_WIDTH_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_io_width_exist:
      ∀ s habd labd v f,
        thread_vmx_get_io_width_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_io_width_spec labd = Some v.
    Proof.
      Local Opaque Z.land.

      unfold thread_vmx_get_io_width_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_io_width_exist.
    Qed.

    Lemma thread_vmx_get_io_width_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_io_width_spec)
            (id ↦ gensem thread_vmx_get_io_width_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_io_width_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_IO_WIDTH_SIM.

  Section THREAD_VMX_GET_IO_WRITE_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_io_write_exist:
      ∀ s habd labd v f,
        thread_vmx_get_io_write_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_io_write_spec labd = Some v.
    Proof.
      Local Opaque Z.shiftr.

      unfold thread_vmx_get_io_write_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_io_write_exist.
    Qed.

    Lemma thread_vmx_get_io_write_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_io_write_spec)
            (id ↦ gensem thread_vmx_get_io_write_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_io_write_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_IO_WRITE_SIM.

  Section THREAD_VMX_GET_EXIT_IO_REP_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_io_rep_exist:
      ∀ s habd labd v f,
        thread_vmx_get_exit_io_rep_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_exit_io_rep_spec labd = Some v.
    Proof.
      Local Opaque Z.land Z.shiftr.

      unfold thread_vmx_get_exit_io_rep_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_io_rep_exist.
    Qed.

    Lemma thread_vmx_get_exit_io_rep_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_io_rep_spec)
            (id ↦ gensem thread_vmx_get_exit_io_rep_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_exit_io_rep_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_IO_REP_SIM.

  Section THREAD_VMX_GET_EXIT_IO_STR_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_io_str_exist:
      ∀ s habd labd v f,
        thread_vmx_get_exit_io_str_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_exit_io_str_spec labd = Some v.
    Proof.
      Local Opaque Z.land Z.shiftr.

      unfold thread_vmx_get_exit_io_str_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_io_str_exist.
    Qed.

    Lemma thread_vmx_get_exit_io_str_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_io_str_spec)
            (id ↦ gensem thread_vmx_get_exit_io_str_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_exit_io_str_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_IO_STR_SIM.

  Section THREAD_VMX_GET_EXIT_IO_PORT_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_CPU_ID}.
    Context {re4: relate_impl_cid}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_get_exit_io_port_exist:
      ∀ s habd labd v f,
        thread_vmx_get_exit_io_port_spec habd = Some v
        → relate_AbData s f habd labd
        → thread_vmx_get_exit_io_port_spec labd = Some v.
    Proof.
      unfold thread_vmx_get_exit_io_port_spec in ×. intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_get_exit_io_port_exist.
    Qed.

    Lemma thread_vmx_get_exit_io_port_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_get_exit_io_port_spec)
            (id ↦ gensem thread_vmx_get_exit_io_port_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      match_external_states_simpl.
      eapply thread_vmx_get_exit_io_port_exist in H2; eauto.
      rewrite H2; reflexivity.
    Qed.

  End THREAD_VMX_GET_EXIT_IO_PORT_SIM.

  Section THREAD_VMX_SET_MMAP_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ept}.
    Context {re3: relate_impl_cid}.
    Context {re4: relate_impl_CPU_ID}.
    Context {re5: relate_impl_init}.

    Lemma thread_vmx_set_mmap_exist:
      ∀ s habd habd´ labd gpa hpa mem_type i f,
        thread_vmx_set_mmap_spec gpa hpa mem_type habd = Some (habd´, i)
        → relate_AbData s f habd labd
        → ∃ labd´, thread_vmx_set_mmap_spec gpa hpa mem_type labd = Some (labd´, i)
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_set_mmap_spec; intros.
      exploit relate_impl_cid_eq; eauto; inversion 1; subst.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      exploit relate_impl_init_eq; eauto; intros.
      revert H. subrewrite. subdestruct.
      eauto using vmx_set_mmap_exist.
    Qed.

    Context {mt1: match_impl_ept}.

    Lemma thread_vmx_set_mmap_match:
      ∀ s d d´ m gpa hpa mem_type i f,
        thread_vmx_set_mmap_spec gpa hpa mem_type d = Some (d´, i)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_set_mmap_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_set_mmap_match.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_vmx_set_mmap_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_vmx_set_mmap_spec}.

    Lemma thread_vmx_set_mmap_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_vmx_set_mmap_spec)
            (id ↦ gensem thread_vmx_set_mmap_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_set_mmap_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_set_mmap_match; eauto.
    Qed.

  End THREAD_VMX_SET_MMAP_SIM.

  Section THREAD_VMX_RUN_VM_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_init}.
    Context {re5: relate_impl_CPU_ID}.
    Context {re6: relate_impl_cid}.

    Lemma thread_vm_run_exist:
      ∀ s n habd habd´ labd rs0 rs1 r´0 f,
        thread_vm_run_spec rs0 habd = Some (habd´, rs1)
        → relate_AbData s f habd labd
        → (∀ r, val_inject f (Pregmap.get r rs0) (Pregmap.get r r´0))
        → (∀ r, Val.has_type (r´0#r) AST.Tint)
        → (∀ r, val_inject (Mem.flat_inj n) (r´0 r) (r´0 r))
        → VMXPool_inject_neutral (vmx labd) n
        → ∃ labd´ r´1, thread_vm_run_spec r´0 labd = Some (labd´, r´1)
                             ∧ relate_AbData s f habd´ labd´
                             ∧ (∀ r, val_inject f (Pregmap.get r rs1) (Pregmap.get r r´1))
                             ∧ (∀ r, Val.has_type (r´1#r) AST.Tint)
                             ∧ (∀ r, val_inject (Mem.flat_inj n) (r´1 r) (r´1 r)).
    Proof.
      unfold thread_vm_run_spec; intros.
      exploit relate_impl_cid_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
      revert H; subrewrite; subdestruct.
      eauto using vm_run_exist.
    Qed.

    Context {mt1: match_impl_iflags}.
    Context {mt2: match_impl_vmx}.
    Context {mt3: match_impl_vmcs}.

    Lemma thread_vm_run_match:
      ∀ s d d´ m rs0 rs1 f,
        thread_vm_run_spec rs0 d = Some (d´, rs1)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vm_run_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vm_run_match.
    Qed.

    Context {inv: VMXEnterInvariants (data_ops := data_ops) thread_vm_run_spec}.
    Context {inv0: VMXEnterInvariants (data_ops:= data_ops0) thread_vm_run_spec}.

    Lemma thread_vm_run_sim :
      ∀ id,
        (∀ n d, low_level_invariant n d → VMXPool_inject_neutral (vmx d) n) →
        sim (crel RData RData) (id ↦ primcall_vmx_enter_compatsem thread_vm_run_spec id)
            (id ↦ primcall_vmx_enter_compatsem thread_vm_run_spec id).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. intros.
      inv H1. inv H0. inv match_extcall_states.
      set (rs02 := (Pregmap.init Vundef) # EDI <- (rs2 EDI) # EBP <- (rs2 EBP)).
      assert (HR: ∀ reg,
                    val_inject f (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
      {
        intros. subst rs01 rs02.
        val_inject_simpl.
      }
      exploit thread_vm_run_exist; eauto 2.

      intros r; destruct r as [| [] | [] | | [] |]; try constructor;
      try apply ASM_INV.

      intros r; destruct r as [| [] | [] | | [] |]; try constructor;
      try apply ASM_INV.

      intros (labd´ & r´1 & HP & HM & Hrinj´ & Hrwt´ & Hrinj_flat´).
      refine_split; eauto 1.
      econstructor; eauto 1.
      - eapply reg_symbol_inject; eassumption.
      - eapply reg_val_inject_defined; eauto 1.
      - intros.
        specialize (match_reg ESP); unfold Pregmap.get in match_reg.
        inv match_reg; try congruence.
        specialize (HESP_STACK _ _ (eq_sym H1)).
        replace b1 with b2 by congruence.
        split.
        × apply Ple_trans with b0;
          [ apply HESP_STACK | apply (match_inject_forward _ _ _ H3) ].
        × apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
      - econstructor; eauto. econstructor; eauto.
        eapply thread_vm_run_match; eassumption.
        subst rs0.
        val_inject_simpl.
    Qed.

  End THREAD_VMX_RUN_VM_SIM.

  Section THREAD_VMX_RETURN_FROM_GUEST_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_init}.
    Context {re5: relate_impl_ipt}.
    Context {re6: relate_impl_cid}.
    Context {re7: relate_impl_PT}.
    Context {re8: relate_impl_uctxt}.
    Context {re9: relate_impl_CPU_ID}.

    Lemma thread_vmx_return_from_guest_exist:
      ∀ s habd habd´ labd f,
        thread_vmx_return_from_guest_spec habd = Some habd´
        → relate_AbData s f habd labd
        → True
        → ∃ labd´, thread_vmx_return_from_guest_spec labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_return_from_guest_spec; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      revert H. subrewrite. subdestruct.
      eauto using vmx_return_from_guest_exist.
    Qed.

    Context {mt1: match_impl_iflags}.
    Context {mt2: match_impl_vmx}.

    Lemma thread_vmx_return_from_guest_match:
      ∀ s d d´ m f,
        thread_vmx_return_from_guest_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_return_from_guest_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_return_from_guest_match.
    Qed.

    Context {inv: VMXReturnInvariants (data_ops := data_ops) thread_vmx_return_from_guest_spec}.
    Context {inv0: VMXReturnInvariants (data_ops:= data_ops0) thread_vmx_return_from_guest_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma thread_vmx_return_from_guest_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec)
            (id ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. intros.
      inv H. inv H0. inv match_extcall_states.

      exploit thread_vmx_return_from_guest_exist; eauto 2.
      intros (labd´ & HP & HM).
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      refine_split; eauto 1.
      econstructor; eauto 1.
      - eapply reg_symbol_inject; eassumption.
      - eapply reg_val_inject_defined; eauto 1.
      - intros.
        specialize (match_reg ESP); unfold Pregmap.get in match_reg.
        inv match_reg; try congruence.
        specialize (HESP_STACK _ _ (eq_sym H1)).
        replace b1 with b2 by congruence.
        split.
        × apply Ple_trans with b0;
          [ apply HESP_STACK | apply (match_inject_forward _ _ _ H3) ].
        × apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
      - econstructor; eauto. econstructor; eauto.
        eapply thread_vmx_return_from_guest_match; eassumption.
        subst rs0.
        val_inject_simpl;
          try (eapply Hrinj´; omega).
        specialize (match_reg PC).
        unfold Pregmap.get in match_reg.
        rewrite HPC in match_reg.
        inv match_reg.
        inv ASM_INV.
        inv inv_inject_neutral.
        specialize (inv_reg_inject_neutral PC).
        rewrite <- H2 in inv_reg_inject_neutral.
        inv inv_reg_inject_neutral.
        generalize H3; intro tmp.
        eapply inject_forward_equal´ in tmp; eauto.
        inv tmp.
        econstructor; eauto.
    Qed.

  End THREAD_VMX_RETURN_FROM_GUEST_SIM.