Library mcertikos.multithread.highrefins.PHThread2TGen
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 LoadStoreSem3high.
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 I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmPHThread2T.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import PHThread2TComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import ObjBigThread.
Require Import BigLogThreadConfigFunction.
Require Import StencilImpl.
Require Import PHThread2TGenDef.
Require Import PHThread2TGenLemma.
Require Import PHThread2TGenLemmaHASEVENT.
Require Import PHThread2TGenLemmaPTRESV.
Section PHThread2TREFGEN.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := s_oracle_prf.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Section ABS_RELT_INSTANCE.
Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.
Program Instance abs_relT : AbstractRelT (spl_data := single_data) (mem := mem)
(spl_mem_ops := memory_model_ops) (s_link_config := s_link_config)
(stencil_ops := @stencil_ops) (real_params_ops := real_params_ops)
(LH:= phbthread) :=
{
match_dproc_RData pd l rd := ∃ (kctxt_val : KContext), relate_RData kctxt_val rd l pd
}.
Lemma get_env_log_same_id:
∀ n curid l l´,
TAsm.get_env_log n curid l = Some l´ → curid = proc_id (uRData l´).
Proof.
induction n; intros; simpl in ×.
- inv H.
- case_eq (zeq (ZMap.get(CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l))) curid).
+ intros; subst.
rewrite zeq_true in H; inv H; auto.
+ intros.
rewrite zeq_false in H; eauto.
Qed.
Next Obligation. inversion s_oracle_basic_prop_prf; auto. Qed.
Next Obligation.
unfold combine_data.
∃ (Pregmap.init Vundef).
econstructor; simpl; eauto.
- rewrite ZMap.gss; auto.
- rewrite ZMap.gi; auto.
- rewrite ZMap.gss; auto.
- rewrite ZMap.gss; auto.
- rewrite ZMap.gss; auto.
- rewrite ZMap.gss; auto.
- simpl; constructor; simpl.
+ rewrite CPU_ID_unchange; auto.
+ rewrite big_oracle_unchange.
inversion multi_oracle_prop.
auto.
Qed.
Opaque update uRData proc_id cl_oplus.
Next Obligation. rewrite H1; eapply abs_rel_t_get_env_log_exist_prop; eauto. Qed.
Notation tempD := (@cdata mem memory_model_ops RData
(@phthread_data_ops (@single_data oracle_ops big_ops)
s_oracle_ops s_threads_ops
(@SingleOracleImpl.s_oracle_prf s_oracle_ops
s_threads_ops real_params_ops oracle_ops6
oracle_ops big_ops))
(@phthread_data_prf (@single_data oracle_ops big_ops)
s_oracle_ops s_threads_ops
(@SingleOracleImpl.s_oracle_prf s_oracle_ops
s_threads_ops real_params_ops oracle_ops6
oracle_ops big_ops) s_threads_prf
(@SingleOracleImpl.s_oracle_prop_prf
s_oracle_ops
s_threads_ops real_params_ops real_params
oracle_ops6 oracle_ops big_ops s_threads_prf
s_oracle_basic_prop_prf))).
Next Obligation.
rename H9 into Hrelated.
rename H1 into kctxt.
destruct ef; try contradiction.
case_eq (peq name thread_yield); intros; subst; [ rewrite peq_true in H7 | rewrite peq_false in H7];
auto; try contradiction.
inv H8; inv H1; subst.
destruct H2 as (Hprim & Hsem).
assert (Htemp: get_layer_primitive thread_yield (D:= tempD) (phthread ⊕ L64)
= OK (Some (gensem big2_thread_yield_spec))).
{ eapply get_layer_primitive_left; auto; decision. }
simpl in Htemp, Hprim.
rewrite Hprim in Htemp; subst; inv Htemp.
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H10.
Transparent uRData update.
assert (same_proc_id: proc_id (uRData (LEvent current_curid LogYieldBack :: l´´)) = proc_id (uRData l)).
{ simpl; simpl in H3.
eapply get_env_log_same_id in H3; simpl in H3; symmetry in H3.
eassumption. }
assert (state_check_cond: state_check thread_yield nil l ae).
{ unfold state_check.
rewrite peq_true.
unfold thread_yield_state_check; simpl in ×.
inv Hrelated; simpl in *; rewritesb.
functional inversion H2; subst.
simpl in ×.
- rewrite H11, H12, H13, H14, H15, H16, H17, H18.
unfold cpu in H22.
unfold cpu in H9; rewrite H9, H21, H22, H10.
unfold cpu in H23.
rewrite CPU_ID_re.
rewrite <- cid_re, <- CPU_ID_re.
rewrite H23.
rewrite H19, H20.
unfold l´, l1, cpu, e0, to in H24.
unfold cpu in H26, H27.
rewrite H24, H25, H26, H27.
unfold ObjTMSCHED.option_z_check in H28.
unfold option_z_check.
rewrite H28.
unfold ObjTMSCHED.z_check in H29.
unfold z_check.
rewrite H29.
auto.
- rewrite H11, H12, H13, H14, H15, H16, H17, H18.
unfold cpu in H22.
unfold cpu in H9; rewrite H9, H21, H22, H10.
unfold cpu in H23.
rewrite CPU_ID_re.
rewrite <- cid_re, <- CPU_ID_re.
rewrite H23.
rewrite H19, H20.
unfold l´, l1, cpu, e0, to in H24.
unfold cpu in H26, H27.
rewrite H24, H25, H26, H27.
unfold ObjTMSCHED.option_z_check in H28.
unfold option_z_check.
rewrite H28.
unfold ObjTMSCHED.z_check in H29.
unfold z_check.
rewrite H29.
auto. }
exploit big2_thread_yield_satisfies_CHECKUNCHAGNED; eauto; intros.
exploit abs_rel_t_thread_yield_match_state_prop; eauto.
intros Hrel; destruct Hrel as (Hrel_a & Hrel_b); eauto.
subst.
replace ((Pos.to_nat (Mem.nextblock m´) - Pos.to_nat (Mem.nextblock m´))%nat) with 0%nat; try omega.
simpl.
assert ((@mem_lift_nextblock mem memory_model_ops Hmem
(@AlgebraicMemImpl.algebraicmem mem memory_model_ops Hmem) m´ O) = m´).
{ remember (mem_lift_nextblock m´ 0) as m´´.
symmetry in Heqm´´.
eapply mem_lift_nextblock_source_eq; eauto. }
rewrite H8; eauto.
Opaque uRData update.
Qed.
Next Obligation.
rename H10 into Hrelated.
rename H1 into kctxt.
destruct ef; try contradiction.
case_eq (peq name thread_sleep); intros; subst; [ rewrite peq_true in H7 | rewrite peq_false in H7]; auto; try contradiction.
inv H8; inv H1; subst.
destruct H2 as (Hprim & Hsem).
assert (Htemp: get_layer_primitive (D := tempD) thread_sleep (phthread ⊕ L64)
= OK (Some (gensem big2_thread_sleep_spec))).
{ eapply get_layer_primitive_left; auto; decision. }
simpl in Htemp, Hprim.
rewrite Hprim in Htemp; subst; inv Htemp.
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H10.
inv H13.
Transparent uRData update.
assert (same_proc_id: proc_id (uRData (LEvent current_curid LogYieldBack :: l´´)) = proc_id (uRData l)).
{ simpl.
simpl in H3.
eapply get_env_log_same_id in H3; simpl in H3; symmetry in H3.
eassumption. }
assert (state_check_cond: state_check thread_sleep (Lint i :: nil) l ae).
{ unfold state_check.
rewrite peq_false; auto; [ | intro contra; inv contra].
rewrite peq_true; auto.
unfold thread_sleep_state_check; simpl in ×.
inv Hrelated; simpl in *; rewritesb.
functional inversion H2; subst.
- rewrite H9, H11, H12, H13, H14, H15, H16, H17, H18.
rewrite CPU_ID_re; rewrite <- cid_re; rewrite H21, H22, H23.
unfold abid in H24; unfold n in H24; rewrite H24.
unfold sc_id in H25; unfold n in H25; rewrite H25.
rewrite <- CPU_ID_re; rewrite H26, H10, H19, H20.
unfold l´, e0, l1, to in H27; rewrite H27.
unfold sc_id in H28, H29; unfold n in H28, H29; rewrite H28; unfold l1 in H29; unfold to in H29; rewrite H29.
rewrite H30, H31, H32; auto.
unfold ObjTMSCHED.z_check in H33.
unfold z_check.
rewrite H33.
auto.
- rewrite H9, H11, H12, H13, H14, H15, H16, H17, H18.
rewrite CPU_ID_re; rewrite <- cid_re; rewrite H21, H22, H23.
unfold abid in H24; unfold n in H24; rewrite H24.
unfold sc_id in H25; unfold n in H25; rewrite H25.
rewrite <- CPU_ID_re; rewrite H26, H10, H19, H20.
unfold l´, e0, l1, to in H27; rewrite H27.
unfold sc_id in H28, H29; unfold n in H28, H29; rewrite H28; unfold l1 in H29; unfold to in H29; rewrite H29.
rewrite H30, H31, H32; auto.
unfold ObjTMSCHED.z_check in H33.
unfold z_check.
rewrite H33.
auto. }
exploit big2_sleep_yield_satisfies_CHECKUNCHAGNED; eauto; intros.
exploit abs_rel_t_thread_sleep_match_state_prop; eauto.
intros Hrel; destruct Hrel as (Hrel_a & Hrel_b); eauto.
subst.
replace ((Pos.to_nat (Mem.nextblock m´) - Pos.to_nat (Mem.nextblock m´))%nat) with 0%nat; try omega.
simpl.
assert ((@mem_lift_nextblock mem memory_model_ops Hmem
(@AlgebraicMemImpl.algebraicmem mem memory_model_ops Hmem) m´ O) = m´).
{ remember (mem_lift_nextblock m´ 0) as m´´.
symmetry in Heqm´´.
eapply mem_lift_nextblock_source_eq; eauto. }
rewrite H8; eauto.
Opaque uRData update.
Qed.
Transparent cl_oplus update uRData proc_id.
Opaque Zdivide_dec Z.add Z.sub Z.div Z.mul.
Next Obligation.
rename H0 into kctxt.
unfold acc_exec_load.
unfold acc_exec_load_strong; simpl.
case_eq acc_def; simpl.
intros.
unfold exec_loadex in H.
unfold exec_loadex3high in H; simpl in ×.
assert (Hflag: AbstractDataType.init a = init (uRData l) ∧
AbstractDataType.ihost a = ihost d ∧
AbstractDataType.pg a = pg (uRData l) ∧
AbstractDataType.ikern a = ikern d) by (inv H1; eauto).
destruct Hflag as (Hflag_init & Hflag_ihost & Hflag_pg & Hflag_ikern); simpl in ×.
unfold PHBThread.single_exec_loadex; simpl; unfold single_exec_loadex.
subdestruct.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_load in ×.
unfold Mem.loadv in *; rewrite Hdestruct3 in H; rewrite Hdestruct3.
subdestruct; unfold Mem.load in Hdestruct4.
simpl in Hdestruct4; lift_unfold.
rewrite Hdestruct4; inv H; split; auto.
∃ kctxt; auto.
-
rewrite <- Hflag_init, <- Hflag_ihost, <- Hflag_ikern, <- Hflag_pg.
unfold HostAccess2high.exec_host_load2high in H; unfold HostAccessPHB.single_exec_host_load.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a)
(AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
AbstractDataType.PT a = PT d ∧
AbstractDataType.ptpool a = ptpool d ∧
AbstractDataType.pperm a = pperm d) by (inv H1; eauto); simpl.
destruct Htemp as (Hflag_cid & Hflag_PT & Hflag_ptp & Hflag_pperm).
rewrite <- Hflag_cid, <- Hflag_PT, <- Hflag_ptp, <- Hflag_pperm.
case_eq (zeq (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a)) (AbstractDataType.PT a));
intros; subst; [ simpl in H; subst | rewrite zeq_false in H; auto; inv H].
simpl; subdestruct; subst.
+ unfold FlatLoadStoreSem.exec_flatmem_load in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_load; simpl; inv H.
∃ d.
split.
× inv H1; simpl in ×.
rewrite flatmem_re; simpl; eauto.
× ∃ kctxt; eauto.
+ unfold FlatLoadStoreSem.exec_flatmem_load in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_load; simpl; inv H.
∃ d.
split.
× inv H1; simpl in ×.
rewrite flatmem_re; simpl; eauto.
× ∃ kctxt; eauto.
+
unfold PageFault.exec_pagefault in H.
unfold PageFaultPHB.single_exec_pagefault.
simpl; subdestruct.
inv H; unfold trapinfo_set; unfold single_trapinfo_set; simpl.
∃ (d {pv_ti : (i, rs RA)}); split; auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_load in ×.
unfold Mem.loadv in *; rewrite Hdestruct3 in H; rewrite Hdestruct3.
subdestruct; unfold Mem.load in Hdestruct4.
simpl in Hdestruct4; lift_unfold.
rewrite Hdestruct4; inv H; split; auto.
∃ kctxt; auto.
-
rewrite <- Hflag_ihost, <- Hflag_init.
assert (CPU_ID_re: AbstractDataType.CPU_ID a = CPU_ID (uRData l)) by (inv H1; simpl in *; auto).
unfold GuestAccessIntel2high.exec_guest_intel_load2high in H.
unfold GuestAccessIntelDef2high.exec_guest_intel_accessor2high in H.
unfold GuestAccessIntel2high.load_accessor2 in H.
unfold GuestAccessIntelPHB.single_exec_guest_intel_load.
unfold GuestAccessIntelPHB.single_load_accessor,
GuestAccessIntelDefPHB.single_exec_guest_intel_accessor; subdestruct; simpl in ×.
∃ d; lift_unfold; simpl in ×.
rewrite CPU_ID_re in ×.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
(ZMap.get (CPU_ID (update init_shared_adt l)) (AbstractDataType.ept a)) = ept d ∧
AbstractDataType.pperm a = pperm d).
{ inv H1; split; auto; rewrite <- CPU_ID_re; auto. }
destruct Htemp as (Htemp1 & Htemp2 & Htemp3).
rewrite <- Htemp2.
rewrite <- Htemp1.
rewrite <- Htemp3.
rewrite e, Hdestruct6, Hdestruct7, Hdestruct8, Hdestruct9, Hdestruct10.
rewrite zeq_true.
unfold FlatLoadStoreSem.exec_flatmem_load in H; unfold FlatLoadStoreSemPHB.single_exec_flatmem_load.
simpl.
assert (flatmem_re: AbstractDataType.HP a = HP d) by (inv H1; simpl in *; auto).
rewrite <- flatmem_re.
unfold FlatMem.load in H; unfold FlatMem.load; simpl in ×.
inv H; split; [reflexivity | ].
∃ kctxt; auto.
-
rewrite <- Hflag_ihost, <- Hflag_init.
assert (CPU_ID_re: AbstractDataType.CPU_ID a = CPU_ID (uRData l)) by (inv H1; simpl in *; auto).
unfold GuestAccessIntel2high.exec_guest_intel_load2high in H.
unfold GuestAccessIntelDef2high.exec_guest_intel_accessor2high in H.
unfold GuestAccessIntel2high.load_accessor2 in H.
unfold GuestAccessIntelPHB.single_exec_guest_intel_load.
unfold GuestAccessIntelPHB.single_load_accessor,
GuestAccessIntelDefPHB.single_exec_guest_intel_accessor; subdestruct; simpl in ×.
∃ d; lift_unfold; simpl in ×.
rewrite CPU_ID_re in ×.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
(ZMap.get (CPU_ID (update init_shared_adt l)) (AbstractDataType.ept a)) = ept d ∧
AbstractDataType.pperm a = pperm d).
{ inv H1; split; auto; rewrite <- CPU_ID_re; auto. }
destruct Htemp as (Htemp1 & Htemp2 & Htemp3).
rewrite <- Htemp2.
rewrite <- Htemp1.
rewrite <- Htemp3.
rewrite e, Hdestruct6, Hdestruct7, Hdestruct8, Hdestruct9, Hdestruct10.
rewrite zeq_true.
unfold FlatLoadStoreSem.exec_flatmem_load in H; unfold FlatLoadStoreSemPHB.single_exec_flatmem_load.
simpl.
assert (flatmem_re: AbstractDataType.HP a = HP d) by (inv H1; simpl in *; auto).
rewrite <- flatmem_re.
unfold FlatMem.load in H; unfold FlatMem.load; simpl in ×.
inv H; split; [reflexivity | ].
∃ kctxt; auto.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_load in ×.
unfold Mem.loadv in *; rewrite Hdestruct2 in H; rewrite Hdestruct2.
subdestruct; unfold Mem.load in Hdestruct3.
simpl in Hdestruct3; lift_unfold.
rewrite Hdestruct3; inv H; split; auto.
∃ kctxt; auto.
Fail idtac.
Qed.
Next Obligation.
rename H0 into kctxt.
unfold acc_exec_store.
unfold acc_exec_store_strong; simpl.
case_eq acc_def; simpl.
intros.
unfold exec_storeex in H.
unfold exec_storeex3high in H.
assert (Hflag: AbstractDataType.init a = init (uRData l) ∧
AbstractDataType.ihost a = ihost d ∧
AbstractDataType.pg a = pg (uRData l) ∧
AbstractDataType.ikern a = ikern d) by (inv H1; eauto).
destruct Hflag as (Hflag_init & Hflag_ihost & Hflag_pg & Hflag_ikern); simpl in ×.
unfold PHBThread.single_exec_storeex; simpl; unfold single_exec_storeex; simpl in ×.
subdestruct.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_store in ×.
unfold Mem.storev in *; rewrite Hdestruct3 in H; rewrite Hdestruct3.
subdestruct; unfold Mem.store in Hdestruct4.
destruct m0.
simpl in Hdestruct4; lift_unfold.
destruct Hdestruct4; subst.
rewrite H2; inv H; split; auto.
∃ kctxt; auto.
-
rewrite <- Hflag_init, <- Hflag_ihost, <- Hflag_ikern, <- Hflag_pg.
unfold HostAccess2high.exec_host_store2high in H; unfold HostAccessPHB.single_exec_host_store.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
AbstractDataType.PT a = PT d ∧
AbstractDataType.ptpool a = ptpool d ∧
AbstractDataType.pperm a = pperm d) by (inv H1; eauto); simpl.
destruct Htemp as (Hflag_cid & Hflag_PT & Hflag_ptp & Hflag_pperm).
rewrite <- Hflag_cid, <- Hflag_PT, <- Hflag_ptp.
case_eq (zeq (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a)) (AbstractDataType.PT a));
intros; subst; [ simpl in H; subst | rewrite zeq_false in H; auto; inv H].
simpl; subdestruct; subst.
+ unfold FlatLoadStoreSem.exec_flatmem_store in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_store; simpl; inv H.
unfold flatmem_store in H3; unfold single_flatmem_store.
simpl; subdestruct.
assert (AbstractDataType.pperm a = pperm d).
{ inv H1; simpl in *; rewrite pperm_re; auto. }
rewrite <- H. rewrite Hdestruct9.
inv H3.
∃ (d {pv_HP : FlatMem.store TY (HP d) (PTADDR v (Int.unsigned i)) (rs rd)}); split; auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
× rewrite <- flatmem_re; auto.
× inv inv_re; constructor; simpl; auto.
+ unfold FlatLoadStoreSem.exec_flatmem_store in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_store; simpl; inv H.
unfold flatmem_store in H3; unfold single_flatmem_store.
simpl; subdestruct.
assert (AbstractDataType.pperm a = pperm d).
{ inv H1; simpl in *; rewrite pperm_re; auto. }
rewrite <- H. rewrite Hdestruct9.
inv H3.
∃ (d {pv_HP : FlatMem.store TY (HP d) (PTADDR v (Int.unsigned i)) (rs rd)}); split; auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
× rewrite <- flatmem_re; auto.
× inv inv_re; constructor; simpl; auto.
+
unfold PageFault.exec_pagefault in H.
unfold PageFaultPHB.single_exec_pagefault.
simpl; subdestruct.
inv H; unfold trapinfo_set; unfold single_trapinfo_set; simpl.
∃ (d {pv_ti : (i, rs RA)}); split; auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
× inv inv_re; constructor; simpl; auto.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_store in ×.
unfold Mem.storev in *; rewrite Hdestruct3 in H; rewrite Hdestruct3.
subdestruct; unfold Mem.store in Hdestruct4.
destruct m0.
simpl in Hdestruct4; lift_unfold.
destruct Hdestruct4; subst.
rewrite H2; inv H; split; auto.
∃ kctxt; auto.
-
rewrite <- Hflag_init, <- Hflag_ihost.
assert (CPU_ID_re: AbstractDataType.CPU_ID a = CPU_ID (uRData l)) by (inv H1; simpl in *; auto).
assert (flatmem_re: AbstractDataType.HP a = HP d) by (inv H1; simpl in *; auto).
assert (pperm_re: AbstractDataType.pperm a = pperm d) by (inv H1; simpl in *; auto).
unfold GuestAccessIntel2high.exec_guest_intel_store2high in H.
unfold GuestAccessIntelDef2high.exec_guest_intel_accessor2high in H.
unfold GuestAccessIntel2high.store_accessor2 in H.
unfold GuestAccessIntelPHB.single_exec_guest_intel_store.
unfold GuestAccessIntelDefPHB.single_exec_guest_intel_accessor,
GuestAccessIntelPHB.single_store_accessor; subdestruct; simpl in ×.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
(ZMap.get (CPU_ID (update init_shared_adt l)) (AbstractDataType.ept a)) = ept d).
{ inv H1; split; auto; rewrite <- CPU_ID_re; auto. }
destruct Htemp as (Htemp1 & Htemp2).
rewrite <- Htemp1, <- Htemp2.
rewrite <- CPU_ID_re in ×.
rewrite e, Hdestruct6, Hdestruct7, Hdestruct8, Hdestruct9.
rewrite zeq_true.
unfold FlatLoadStoreSem.exec_flatmem_store in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_store.
unfold flatmem_store in H.
unfold single_flatmem_store; simpl in ×.
rewrite flatmem_re, pperm_re in ×.
subdestruct.
∃ (d { pv_HP : FlatMem.store TY (HP d) (EPTADDR (hpa / 4096) (Int.unsigned i)) (rs rd)}).
inv H; simpl in *; split; try auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
-
rewrite <- Hflag_init, <- Hflag_ihost.
assert (CPU_ID_re: AbstractDataType.CPU_ID a = CPU_ID (uRData l)) by (inv H1; simpl in *; auto).
assert (flatmem_re: AbstractDataType.HP a = HP d) by (inv H1; simpl in *; auto).
assert (pperm_re: AbstractDataType.pperm a = pperm d) by (inv H1; simpl in *; auto).
unfold GuestAccessIntel2high.exec_guest_intel_store2high in H.
unfold GuestAccessIntelDef2high.exec_guest_intel_accessor2high in H.
unfold GuestAccessIntel2high.store_accessor2 in H.
unfold GuestAccessIntelPHB.single_exec_guest_intel_store.
unfold GuestAccessIntelDefPHB.single_exec_guest_intel_accessor,
GuestAccessIntelPHB.single_store_accessor; subdestruct; simpl in ×.
assert (Htemp: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)) ∧
(ZMap.get (CPU_ID (update init_shared_adt l)) (AbstractDataType.ept a)) = ept d).
{ inv H1; split; auto; rewrite <- CPU_ID_re; auto. }
destruct Htemp as (Htemp1 & Htemp2).
rewrite <- Htemp1, <- Htemp2.
rewrite <- CPU_ID_re in ×.
rewrite e, Hdestruct6, Hdestruct7, Hdestruct8, Hdestruct9.
rewrite zeq_true.
unfold FlatLoadStoreSem.exec_flatmem_store in H.
unfold FlatLoadStoreSemPHB.single_exec_flatmem_store.
unfold flatmem_store in H.
unfold single_flatmem_store; simpl in ×.
rewrite flatmem_re, pperm_re in ×.
subdestruct.
∃ (d { pv_HP : FlatMem.store TY (HP d) (EPTADDR (hpa / 4096) (Int.unsigned i)) (rs rd)}).
inv H; simpl in *; split; try auto.
∃ kctxt.
inv H1; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
-
simpl in ×.
∃ d.
rewrite <- Hflag_ihost, <- Hflag_ikern.
unfold Asm.exec_store in ×.
unfold Mem.storev in *; rewrite Hdestruct2 in H; rewrite Hdestruct2.
subdestruct; unfold Mem.store in Hdestruct3.
destruct m0.
simpl in Hdestruct3; lift_unfold.
destruct Hdestruct3; subst.
rewrite H2; inv H; split; auto.
∃ kctxt; auto.
Fail idtac.
Qed.
Transparent Zdivide_dec Z.add Z.sub Z.div Z.mul.
Opaque compatlayer_ops update uRData proc_id.
Next Obligation.
rename H0 into kctxt.
destruct (ef_cases ef) as [Hcase|Hcase].
- destruct ef; inv Hcase; inv H; inv H0.
subdestruct; try (inv H3; fail); clear H3.
destruct H as [Hprims Hsem].
inv_layer Hprims; has_event_remove Hdestruct1.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
inv_monad H0; inv H0.
Transparent update proc_id uRData.
refine_split´; eauto.
econstructor; [| simpl; eauto].
∃ (gensem single_vmxinfo_get_spec); split; [reflexivity|].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmxinfo_get_spec, thread_vmxinfo_get_spec in *;
unfold vmxinfo_get_spec in *; simpl in *; subdestruct.
inv H4; simpl in ×.
rewrite <- ikern_re, <- ihost_re.
rewrite Hdestruct2, Hdestruct3.
inv H5; rewrite <- vmxinfo_re; eauto.
Opaque update proc_id uRData.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
functional inversion H0.
functional inversion H1; inv H5.
Transparent update proc_id uRData.
refine_split´; eauto.
× econstructor; [| simpl; eauto].
∃ (gensem single_setPT_spec); split; [reflexivity|].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_setPT_spec in *; simpl in ×.
inv H4; simpl in ×.
rewrite <- init_re, <- ikern_re, <- ihost_re, <- ipt_re.
rewrite H3, H6, H7, H8, H9; reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
Opaque update proc_id uRData.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
inv H8; inv_monad H0; inv H0.
Transparent uRData update proc_id.
∃ ae; split; [ | simpl; eauto].
exploit thread_ptRead_related_t; eauto; intros Hrelated.
destruct Hrelated as (res´ & Hrelated_a & Hrelated_b).
econstructor; [| simpl; eauto].
∃ (gensem single_ptRead_spec); split; [reflexivity|].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
simpl in Hrelated_a; rewrite Hrelated_a; reflexivity.
Opaque uRData update proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
inv H8; inv_monad H0; inv H0.
functional inversion H5.
functional inversion H0.
Transparent update proc_id uRData.
refine_split´; eauto.
econstructor; [| simpl; eauto].
∃ (gensem single_uctx_get_spec); split; [reflexivity|].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_uctx_get_spec in *; simpl in ×.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- big_log_re, <- CPU_ID_re, <- uctxt_re.
rewrite H1, H3, H12, H9, H10, H11, H6; unfold cpu in H7; rewrite H7, H13, H14.
rewrite <- _x in H15; rewrite H15.
rewrite H8.
reflexivity.
Opaque update proc_id uRData.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
functional inversion H0.
functional inversion H1.
Transparent update proc_id uRData.
refine_split´; eauto.
× econstructor; [| simpl; eauto].
∃ (gensem single_uctx_set_spec); split; [reflexivity|].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_uctx_set_spec in *; simpl in ×.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- big_log_re, <- CPU_ID_re, <- uctxt_re.
rewrite H3, H5, H6, H9, H10, H11, H12; unfold cpu in H7; rewrite H7, H13, H14.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl; unfold uctx´; simpl in ×.
rewrite _x; rewrite ZMap.gss; unfold uctx; auto. }
{ inv inv_re; constructor; simpl; auto. }
Opaque update proc_id uRData.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_container_get_nchildren_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_container_get_nchildren_spec; simpl.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- AC_re, <- CPU_ID_re, <- big_log_re; simpl.
unfold cpu in ×.
rewrite H1, H3, H6, H7, H8, H9.
rewrite <- H0; unfold c.
rewrite _x.
reflexivity.
Opaque uRData update proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_container_get_quota_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_container_get_quota_spec; simpl.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- AC_re, <- CPU_ID_re, <- big_log_re; simpl.
unfold cpu in ×.
rewrite H1, H3, H6, H7, H8, H9.
rewrite <- H0; unfold c.
rewrite _x.
reflexivity.
Opaque uRData update proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_container_get_usage_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_container_get_usage_spec; simpl.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- AC_re, <- CPU_ID_re, <- big_log_re; simpl.
unfold cpu in ×.
rewrite H1, H3, H6, H7, H8, H9.
rewrite <- H0; unfold c.
rewrite _x.
reflexivity.
Opaque uRData update proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
inv H8; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
× ∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_container_can_consume_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_container_can_consume_spec; simpl.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- AC_re, <- CPU_ID_re, <- big_log_re; simpl.
unfold cpu in ×.
rewrite H1, H3, H6, H7, H8, H9.
unfold c in H10.
rewrite <- _x.
rewrite H10.
rewrite H0.
reflexivity.
× ∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_container_can_consume_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_container_can_consume_spec; simpl.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- ikern_re, <- ihost_re, <- AC_re, <- CPU_ID_re, <- big_log_re; simpl.
unfold cpu in ×.
rewrite H1, H3, H6, H7, H8, H9.
unfold c in H10.
rewrite <- _x.
rewrite H10.
rewrite H0.
reflexivity.
Opaque uRData update proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
functional inversion H0; subst.
∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_get_CPU_ID_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_get_CPU_ID_spec; simpl.
inv H4; rewrite <- ikern_re, <- ihost_re, <- CPU_ID_re, <- init_re.
rewrite H1, H7, H6, H3; auto.
Opaque update proc_id uRData.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6; inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst; simpl in ×.
functional inversion H0; subst; auto.
∃ ae; split; [ | split; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_get_curid_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_get_curid_spec; simpl.
inv H4; rewrite <- ikern_re, <- ihost_re, <- CPU_ID_re, <- init_re.
rewrite <- cid_eq.
rewrite H6, H7, H1, H3; auto.
Opaque update proc_id uRData.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
inv_monad H0; inv H0.
Transparent update proc_id uRData.
functional inversion H5; subst.
functional inversion H0; subst.
refine_split´; auto; [ | simpl; eauto].
econstructor; [simpl | simpl; eauto].
∃ (gensem single_get_sync_chan_busy_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_get_sync_chan_busy_spec; simpl.
inv H4.
rewrite <- init_re, <- ikern_re, <- pg_re, <- ihost_re, <- ipt_re, <- CPU_ID_re, <- big_log_re.
rewrite H1, H3, H7, H8, H9, H10.
rewrite zle_lt_true; eauto.
rewrite <- syncchpool_re; rewrite H12.
rewrite H6; reflexivity.
Opaque update proc_id uRData.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
destruct args; inv H0.
inv H3; functional inversion H0.
functional inversion H1.
Transparent update proc_id uRData.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_set_sync_chan_busy_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_set_sync_chan_busy_spec; simpl.
inv H4.
rewrite <- init_re, <- ikern_re, <- pg_re, <- ihost_re, <- ipt_re, <- CPU_ID_re, <- big_log_re.
rewrite H3, H5, H7, H8, H9, H10.
rewrite zle_lt_true; eauto.
rewrite <- syncchpool_re; rewrite H12; reflexivity.
× instantiate (1:= kctxt); auto.
inv H4; constructor; simpl in *; auto.
inv inv_re; constructor; simpl; auto.
Opaque update proc_id uRData.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
destruct args; inv H0.
destruct args; inv H3.
inv H9; functional inversion H0.
functional inversion H1; inv H6.
functional inversion H14; subst.
functional inversion H15; subst.
Transparent update proc_id uRData.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_ipc_receive_body_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_big_ipc_receive_body_spec; simpl.
unfold single_flatmem_copy_spec; simpl.
inv H4; rewrite <- init_re, <- ikern_re, <- pg_re, <- ihost_re, <- ipt_re, <- syncchpool_re, <- CPU_ID_re, <- big_log_re.
unfold single_big_page_copy_back_spec.
simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pperm_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- flatmem_re.
unfold index in H15.
unfold index in H24, H25, H26.
simpl in H12.
rewrite H5, H8, H9, H10, H11, H13, H3, H12, H15, H19, H20, H21, H22, H23, H24, H25, H26.
rewrite zeq_true.
rewrite H28.
simpl.
rewrite H7.
reflexivity.
× instantiate (1:= kctxt); auto.
inv H4; simpl in *; constructor; auto.
{ simpl; rewrite syncchpool_re; auto. }
{ inv inv_re; constructor; simpl; auto. }
Opaque update proc_id uRData.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update uRData proc_id.
inv_monad H0.
inv H0.
functional inversion H5.
functional inversion H1; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
{ ∃ (gensem single_rdmsr_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_rdmsr_spec; simpl; inv H4; simpl in ×.
rewrite <- ikern_re, <- ihost_re, H3, H6, H0.
instantiate (1:= z); reflexivity. }
{ simpl; reflexivity. }
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H0.
× inv H3.
Transparent update uRData proc_id.
inv_monad H0.
inv H0.
functional inversion H5.
functional inversion H1; subst.
refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_wrmsr_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_wrmsr_spec; simpl; inv H4; simpl in ×.
rewrite <- ikern_re, <- ihost_re, H3, H6, H0.
econstructor. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id. }
× inv H3.
Transparent update uRData proc_id.
inv_monad H0.
inv H0.
functional inversion H6.
functional inversion H1; subst.
refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_wrmsr_spec); split; [reflexivity | ].
rewrite <- H5.
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_wrmsr_spec; simpl; inv H4; simpl in ×.
rewrite <- ikern_re, <- ihost_re, H3, H7.
rewrite <- H0.
econstructor. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id. }
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update uRData proc_id.
functional inversion H0; functional inversion H1; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_intercept_intwin_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_intercept_intwin_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11, H12, H13.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
- simpl.
rewrite ZMap.gss.
unfold d´.
unfold res.
reflexivity.
- inv inv_re; simpl; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_intercept_intwin_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_intercept_intwin_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11, H12, H13.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
- simpl.
rewrite ZMap.gss.
unfold d´.
unfold res.
reflexivity.
- inv inv_re; constructor; simpl; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
Transparent update uRData proc_id.
functional inversion H0; subst.
functional inversion H1; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_desc1_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_desc1_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11, H12.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
Transparent update uRData proc_id.
functional inversion H0; subst.
functional inversion H1; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_desc2_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_desc2_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11, H12.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
destruct args; inv H9.
inv H8.
Transparent update uRData proc_id.
functional inversion H0; functional inversion H1; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_inject_event_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_inject_event_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
unfold i3 in H13.
rewrite H3, H5, H7, H8, H9, H10, H11, H12, H13, H14.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
unfold d2.
unfold d1.
unfold i6.
unfold i5.
unfold i4.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_inject_event_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_inject_event_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
unfold i3 in H13.
rewrite H3, H5, H7, H8, H9, H10, H11, H12, H13, H14.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
unfold d1.
unfold i5.
unfold i4.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_inject_event_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_inject_event_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
unfold is_invalid, i3 in H13.
rewrite H3, H5, H7, H8, H9, H10, H11, H12, H13.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H0; inv H3.
Transparent update uRData proc_id.
× functional inversion H0; functional inversion H1; subst.
refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_tsc_offset_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_tsc_offset_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
× functional inversion H0; functional inversion H1; subst.
refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
rewrite <- H5.
∃ (gensem single_vmx_set_tsc_offset_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_tsc_offset_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H3, H6, H8, H9, H10, H11, H12.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
{ ∃ (gensem single_vmx_get_tsc_offset_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_tsc_offset_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
rewrite H3.
instantiate (1 := z).
reflexivity. }
{ simpl; reflexivity. }
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_reason_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_reason_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_fault_addr_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_fault_addr_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_qualification_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_qualification_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_check_pending_event_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_check_pending_event_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_check_pending_event_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_check_pending_event_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_check_int_shadow_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_check_int_shadow_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_check_int_shadow_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_check_int_shadow_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
inv_monad H0; inv H0.
Transparent update uRData proc_id.
functional inversion H5; functional inversion H0; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_reg_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_reg_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_reg_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_reg_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
inv H8.
Transparent update uRData proc_id.
functional inversion H0; functional inversion H1; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_reg_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_reg_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl; rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_reg_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_reg_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- vmcs_re, <- init_re.
rewrite H3, H5, H7, H8, H9, H10, H11, H12.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl; rewrite ZMap.gss.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_next_eip_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_next_eip_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- vmcs_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_io_width_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_io_width_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_io_width_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_io_width_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12, H13.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_io_width_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_io_width_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H7, H8, H9, H10, H11.
unfold qsize in H12, H13.
rewrite H12, H13.
rewrite H3.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_io_write_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_io_write_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11, H12.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_io_write_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_io_write_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11.
unfold qdir in H12; rewrite H12.
rewrite H6.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_io_rep_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_io_rep_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_io_str_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_io_str_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
inv_monad H0; inv H0.
functional inversion H5; functional inversion H0; subst.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_get_exit_io_port_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_get_exit_io_port_spec; simpl; inv H4; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- vmx_re, <- init_re.
rewrite H1, H3, H7, H8, H9, H10, H11.
rewrite H6.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
Transparent update uRData proc_id.
functional inversion H0.
unfold vmx_set_mmap_spec in H1.
unfold ept_add_mapping_spec in H1.
unfold ept_invalidate_mappings_spec in H1.
subdestruct; inv H1.
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_mmap_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_mmap_spec; simpl; inv H4; simpl in ×.
unfold single_ept_add_mapping_spec; simpl.
unfold single_ept_invalidate_mappings_spec; simpl.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- ept_re, <- init_re.
rewrite H3, Hdestruct12, Hdestruct3, Hdestruct13, Hdestruct5, Hdestruct6.
rewrite Hdestruct14.
rewrite Hdestruct7, Hdestruct9, Hdestruct10, Hdestruct11.
rewrite Hdestruct8.
rewrite H5.
rewrite zle_le_true; [ | unfold Int.max_unsigned; simpl; omega].
rewrite zeq_true.
simpl.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- init_re.
rewrite H3, Hdestruct12, Hdestruct13, H5.
rewrite <- H8.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
rewrite ept_re.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
× refine_split´; auto.
{ econstructor; [simpl | simpl; eauto; simpl].
∃ (gensem single_vmx_set_mmap_spec);
split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_vmx_set_mmap_spec; simpl; inv H4; simpl in ×.
unfold single_ept_add_mapping_spec; simpl.
unfold single_ept_invalidate_mappings_spec; simpl.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- pg_re, <- CPU_ID_re, <- ept_re, <- init_re.
rewrite H3, Hdestruct12, Hdestruct3, Hdestruct13, Hdestruct5, Hdestruct6.
rewrite Hdestruct14.
rewrite Hdestruct7, Hdestruct9, Hdestruct10, Hdestruct11.
rewrite Hdestruct8.
rewrite H5.
rewrite zle_le_true; [ | unfold Int.max_unsigned; simpl; omega].
rewrite zeq_true.
simpl.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- init_re.
rewrite H3, Hdestruct12, Hdestruct13, H5.
rewrite <- H8.
reflexivity. }
{ instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss.
rewrite ept_re.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. } }
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
Transparent update uRData proc_id.
functional inversion H6.
functional inversion H0; inv H3.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (IntelPrimSemantics.vmcs_set_defaults_compatsem single_vmx_init_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
eapply IntelPrimSemantics.extcall_vmcs_set_defaults_sem_intro; eauto.
unfold single_vmx_init_spec; simpl in ×.
inv H4; simpl in ×.
rewrite <- cid_re, <- init_re, <- pg_re, <- in_intr_re, <- ikern_re, <- ihost_re, <- ipt_re, <- CPU_ID_re.
rewrite H1, H5, H10, H12, H15, H16, H17, H18, H19.
reflexivity.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
{ simpl.
rewrite ZMap.gss; auto.
rewrite ept_re.
reflexivity. }
{ simpl.
rewrite ZMap.gss; auto.
rewrite vmcs_re.
reflexivity. }
{ simpl.
rewrite ZMap.gss; auto.
rewrite vmx_re.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. }
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
functional inversion H0.
functional inversion H0; inv H1.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_cli_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_cli_spec; simpl; inv H4; simpl in *; rewrite <- CPU_ID_re; rewrite <- cid_eq, <- init_re.
rewrite <- _x, H8; rewrite zeq_true; eauto.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
Opaque update uRData proc_id.
+
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H4; rewrite <- CPU_ID_re in cid_re; auto. }
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
Transparent update uRData proc_id.
functional inversion H0.
functional inversion H0; inv H1.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_sti_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_sti_spec; simpl; inv H4; simpl in *; rewrite <- CPU_ID_re; rewrite <- cid_eq, <- init_re.
rewrite <- _x, H8; rewrite zeq_true; eauto.
× instantiate (1:= kctxt).
inv H4; simpl in *; constructor; auto.
inv inv_re; constructor; simpl; auto.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
exploit serial_intr_disable_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c).
Transparent update uRData proc_id.
∃ pd´; refine_split´.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_serial_intr_disable_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
simpl in Hrelated_a; rewrite Hrelated_a.
simpl in Hrelated_c; rewrite Hrelated_c; auto.
× instantiate (1:= kctxt); auto.
inv Hrelated_b.
simpl in Hrelated_c.
rewrite <- Hrelated_c in ×.
constructor; eauto.
inv inv_re; constructor; simpl; rewrite Hrelated_c; auto.
× reflexivity.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
exploit serial_intr_enable_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c).
Transparent update uRData proc_id.
∃ pd´; refine_split´.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_serial_intr_enable_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
simpl in Hrelated_a; rewrite Hrelated_a.
simpl in Hrelated_c; rewrite Hrelated_c; auto.
× instantiate (1:= kctxt); auto.
inv Hrelated_b.
simpl in Hrelated_c.
rewrite <- Hrelated_c in ×.
constructor; eauto.
inv inv_re; constructor; simpl; rewrite Hrelated_c; auto.
× reflexivity.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
exploit serial_putc_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c).
∃ pd´.
Transparent update uRData proc_id.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_serial_putc_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
simpl in Hrelated_a; rewrite Hrelated_a.
simpl in Hrelated_c; rewrite Hrelated_c; auto.
× instantiate (1:= kctxt); auto.
inv Hrelated_b.
simpl in Hrelated_c.
rewrite <- Hrelated_c in ×.
constructor; eauto.
inv inv_re; constructor; simpl; rewrite Hrelated_c; auto.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
inv H6.
exploit cons_buf_read_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d).
∃ pd´.
Transparent update uRData proc_id.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_cons_buf_read_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
simpl in Hrelated_a; rewrite Hrelated_a.
simpl in Hrelated_c; rewrite Hrelated_c.
rewrite Hrelated_d; auto.
× instantiate (1:= kctxt); auto.
inv Hrelated_b.
simpl in Hrelated_c.
rewrite <- Hrelated_c in ×.
constructor; eauto.
inv inv_re; constructor; simpl; rewrite Hrelated_c; auto.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
functional inversion H0; subst.
functional inversion H1; subst.
Transparent update uRData proc_id.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_proc_create_postinit_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
unfold single_proc_create_postinit_spec; simpl in ×.
inv H4.
rewrite <- ikern_re, <- init_re, <- ihost_re; rewrite H3, H6, H7.
reflexivity.
× instantiate (1:= kctxt); auto.
Opaque update uRData proc_id.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst; inv Hsem.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_longoffloat_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_longuoffloat_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_floatoflong_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_floatoflong_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_floatoflongu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_floatoflongu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_singleoflong_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_singleoflong_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_singleoflongu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_singleoflongu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
destruct args; inv H1.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_divls_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_divls_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
destruct args; inv H1.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_divlu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_divlu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
destruct args; inv H1.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_modls_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_modls_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
destruct args; inv H1.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_modlu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
× refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_modlu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_shll_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_shrlu_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
+
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H1.
destruct args; inv H3.
destruct args; inv H5.
refine_split´; eauto.
econstructor; simpl; [| reflexivity].
∃ sextcall_shrl_compatsem; split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl; repeat constructor; auto.
- assert (Hext:= H); apply exec_external_prop in H; auto; inv H.
∃ ae.
simpl in H0; inv H0.
refine_split´; eauto.
inv Hext.
destruct ef; inv Hcase; inv H.
× econstructor; simpl; eauto; simpl in *; rewritesb.
apply CompCertBuiltins.builtin_sem_i64_neg; auto.
× econstructor; simpl; eauto; simpl in *; rewritesb.
apply CompCertBuiltins.builtin_sem_i64_add; auto.
× econstructor; simpl; eauto; simpl in *; rewritesb.
apply CompCertBuiltins.builtin_sem_i64_sub; auto.
× econstructor; simpl; eauto; simpl in *; rewritesb.
apply CompCertBuiltins.builtin_sem_i64_mul; auto.
× econstructor; simpl; eauto; rewritesb.
destruct args; [inv H0| ].
inv H0; inv H8; repeat constructor; auto.
× econstructor; simpl; eauto; rewritesf.
inv H0; repeat constructor; auto.
destruct args; [ inv H5 |].
simpl in H5; subdestruct.
{ inv H5; inv H1; subst; [ econstructor; auto | ].
econstructor; auto; unfold Mem.store in ×.
simpl in *; lift_unfold; destruct H0; split; auto. }
{ inv H5; inv H1; subst; [ econstructor; auto | ].
econstructor; auto; unfold Mem.store in ×.
simpl in *; lift_unfold; destruct H0; split; auto. }
{ inv H5; inv H1; subst; [ econstructor; auto | ].
econstructor; auto; unfold Mem.store in ×.
simpl in *; lift_unfold; destruct H0; split; auto. }
{ inv H5; inv H1; subst; [ econstructor; auto | ].
econstructor; auto; unfold Mem.store in ×.
simpl in *; lift_unfold; destruct H0; split; auto. }
{ inv H5; inv H1; subst; [ econstructor; auto | ].
econstructor; auto; unfold Mem.store in ×.
simpl in *; lift_unfold; destruct H0; split; auto. }
× econstructor; simpl; eauto.
simpl in H5; subst.
econstructor; eauto.
inv H9; repeat constructor; auto.
× econstructor; simpl; eauto; rewritesb.
subdestruct.
{ inv H0; inv H5; repeat constructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor ;eauto.
lift_unfold; simpl; tauto. }
{ inv H0; inv H5; repeat constructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor ;eauto.
lift_unfold; simpl; tauto. }
{ inv H0; inv H5; repeat constructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor ;eauto.
lift_unfold; simpl; tauto. }
{ inv H0; inv H5; repeat constructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor ;eauto.
lift_unfold; simpl; tauto. }
{ inv H0; inv H5; repeat constructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
econstructor ;eauto.
lift_unfold; simpl; tauto. }
× destruct args; inv H0.
destruct m´0 as [m0 d0].
econstructor; try eauto.
econstructor.
{ instantiate (1:= (m0, (update init_shared_adt l, ae))).
unfold Mem.alloc in H1; simpl in H1.
unfold Mem.store in H5; simpl in H5.
lift_unfold.
destruct H1 as (H1a, _); destruct H5 as (H5a, H5b); subst; auto. }
{ lift_unfold; tauto. }
× econstructor; simpl; eauto; rewritesb.
destruct args; inv H0.
econstructor; eauto.
lift_unfold; intuition.
× econstructor; simpl; eauto; rewritesb.
destruct args; try inv H0.
destruct args; try inv H13.
econstructor; eauto.
lift_unfold; intuition.
× econstructor; simpl; eauto.
constructor; auto.
× econstructor; simpl; eauto; rewritesb.
constructor; auto.
Fail idtac.
Qed.
Next Obligation.
rename H0 into kctxt.
destruct (ef_cases ef) as [Hcase|Hcase].
- destruct ef; inv Hcase; inv H; inv H0.
subdestruct; try (inv H3; fail); clear H3.
destruct H as [Hprims Hsem].
inv_layer Hprims; no_event_remove Hdestruct1.
+
assert (no_event: has_event palloc = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num palloc = 1)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update proc_id uRData.
exploit big_palloc_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e).
∃ (Lint i::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_palloc_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a, Hrelated_e; auto.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event pt_resv = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num pt_resv = 2)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
Transparent update proc_id uRData.
exploit ptResv_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e).
∃ (Lint i::Lint i0::Lint i1::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_ptResv_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a, Hrelated_e; auto.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event thread_wakeup = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num thread_wakeup = 4)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update proc_id uRData.
exploit big_thread_wakeup_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e).
∃ (Lint i::nil), ae, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_thread_wakeup_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a, Hrelated_e; reflexivity.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event sched_init = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num sched_init = 5)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update proc_id uRData.
exploit big_sched_init_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d).
∃ (Lint i::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_sched_init_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a; reflexivity.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event proc_create = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num proc_create = 3)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H0.
destruct args; inv H5.
destruct args; inv H3.
Transparent update proc_id uRData.
exploit big_proc_create_related_t; eauto; intros Hrelated.
instantiate (1:= elf_id) in Hrelated.
destruct Hrelated as (l´ & pd´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e & Hrelated_f).
∃ (Lint elf_id :: Lptr buc ofs_uc :: Lint q :: nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (proc_create_compatsem single_big_proc_create_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
eapply extcall_proccreate_sem_intro; eauto.
rewrite Hrelated_a, Hrelated_e; auto.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event acquire_lock_CHAN = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num acquire_lock_CHAN = 6)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update proc_id uRData.
exploit big_acquire_lock_SC_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d).
∃ (Lint i::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_acquire_lock_SC_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a; reflexivity.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event release_lock_CHAN = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num release_lock_CHAN = 7)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
inv H9.
Transparent update proc_id uRData.
exploit big_release_lock_SC_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d).
∃ (Lint i::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_release_lock_SC_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_a; reflexivity.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
+
assert (no_event: has_event ipc_send_body = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num ipc_send_body = 8)
by (unfold prim_id_num; simpl; reflexivity).
destruct Hsem as [s [sem [? [Hsig [Hsem [? ?]]]]]]; subst.
inv Hsem; simpl in *; inv Hsig.
destruct args; inv H6.
destruct args; inv H9.
destruct args; inv H8.
inv H9.
Transparent update proc_id uRData.
exploit big_ipc_send_body_related_t; eauto; intros Hrelated.
destruct Hrelated as (l´ & pd´ & res´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e).
∃ (Lint i::Lint i0::Lint i1::nil), pd´, l´.
simpl in ×.
refine_split´; auto.
× econstructor; [simpl | simpl; eauto].
∃ (gensem single_big_ipc_send_body_spec); split; [reflexivity | ].
∃ s; refine_split´; auto; try reflexivity; simpl.
repeat constructor.
rewrite Hrelated_e; rewrite Hrelated_a; reflexivity.
× instantiate (1:= kctxt); auto.
× repeat (constructor; auto).
Opaque update proc_id uRData.
- subdestruct; contradiction.
Fail idtac.
Qed.
Next Obligation.
rename H into ef.
rename H0 into kctxt.
case_eq (peq ef thread_yield); intros; subst; [ rewrite peq_true in H2 | rewrite peq_false in H2]; auto; try contradiction.
case_eq (peq ef thread_sleep); intros; subst; [ rewrite peq_true in H2 | rewrite peq_false in H2]; auto; try contradiction.
inv H8.
inv_layer H7.
-
assert (in_event: has_event vmx_run_vm = false) by (unfold has_event; auto).
inv H6; subst.
unfold thread_vm_run_spec in H10.
unfold vm_run_spec in H10.
subdestruct; inv H10.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := IntelPrimSemantics.primcall_vmx_enter_compatsem single_vm_run_spec vmx_run_vm).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_vm_run_spec.
inv H3; simpl in *; rewritesb.
rewrite zeq_true.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6.
reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
{ simpl; rewrite ZMap.gss; auto. }
{ simpl; rewrite ZMap.gss; auto. }
{ inv inv_re; constructor; simpl; auto. }
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event vmx_return_from_guest = false) by (unfold has_event; auto).
inv H6; subst.
unfold thread_vmx_return_from_guest_spec in H10.
unfold vmx_return_from_guest_spec in H10.
subdestruct; inv H10.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := IntelPrimSemantics.primcall_vmx_return_compatsem single_vmx_return_from_guest_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_vmx_return_from_guest_spec.
inv H3; simpl in *; rewritesb.
rewrite zeq_true.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7, Hdestruct8.
reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
{ simpl; rewrite ZMap.gss; auto. }
{ inv inv_re; constructor; simpl; auto. }
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event host_in = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5; subst.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := primcall_general_compatsem single_hostin_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_hostin_spec.
inv H3; simpl in *; rewritesb.
rewrite H6, H8, H9; reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
inv inv_re; constructor; simpl; auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event host_out = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := primcall_general_compatsem single_hostout_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_hostout_spec.
inv H3; simpl in *; rewritesb.
rewrite H6, H8, H9, H12; reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
inv inv_re; constructor; simpl; auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event trap_get = false) by (unfold has_event; auto).
inv H6; subst.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := primcall_trap_info_get_compatsem single_trap_info_get_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_trap_info_get_spec.
inv H3; simpl in *; rewritesb.
unfold trap_info_get_spec; reflexivity.
+ instantiate (1:= kctxt); auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event trap_set = false) by (unfold has_event; auto).
inv H6; subst.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := primcall_trap_info_ret_compatsem single_trap_info_ret_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
unfold single_trap_info_ret_spec.
inv H3; simpl in *; rewritesb.
unfold trap_info_ret_spec; reflexivity.
+ instantiate (1:= kctxt); auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event proc_start_user = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := PrimTMSemantics.primcall_start_user_tm_compatsem single_proc_start_user_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
× unfold single_proc_start_user_spec.
inv H3; simpl in *; rewritesb.
rewrite H11, H12, H13, H14, H15, H6.
unfold curid, cpu in H7; rewrite H7.
reflexivity.
× unfold uctx0.
intros; auto.
unfold curid0.
inv H8.
simpl.
unfold curid0 in H9.
rewrite H9.
auto.
× unfold uctx0.
intros; auto.
unfold curid0.
inv H8.
simpl.
unfold curid0 in H9.
rewrite H9.
auto.
× subst.
rewrite H9.
assumption.
× subst.
rewrite H9.
assumption.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
inv inv_re; constructor; simpl; auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event proc_exit_user = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := PrimTMSemantics.primcall_exit_user_tm_compatsem single_proc_exit_user_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
× unfold single_proc_exit_user_spec.
inv H3; simpl in *; rewritesb.
rewrite H9, H11, H13, H14, H6.
unfold curid, cpu in H7; rewrite H7.
reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
{ simpl.
unfold curid0.
rewrite ZMap.gss.
fold uctx1.
fold uctx2.
fold uctx3.
fold uctx4.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. }
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event proc_start_user2 = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := PrimTMSemantics.primcall_start_user_tm_compatsem2 single_proc_start_user_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
× unfold single_proc_start_user_spec.
inv H3; simpl in *; rewritesb.
rewrite H11, H12, H13, H14, H15, H6.
unfold curid, cpu in H7; rewrite H7.
reflexivity.
× unfold uctx0.
intros; auto.
unfold curid0.
inv H8.
simpl.
unfold curid0 in H9.
rewrite H9.
auto.
× unfold uctx0.
intros; auto.
unfold curid0.
inv H8.
simpl.
unfold curid0 in H9.
rewrite H9.
auto.
× subst.
rewrite H9.
assumption.
× subst.
rewrite H9.
assumption.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
inv inv_re; constructor; simpl; auto.
+ rewrite in_event; auto.
Opaque update uRData proc_id.
-
assert (in_event: has_event proc_exit_user2 = false) by (unfold has_event; auto).
inv H6; subst.
functional inversion H10; subst.
functional inversion H5.
Transparent update uRData proc_id.
refine_split´; auto; simpl in ×.
+ instantiate (1 := PrimTMSemantics.primcall_exit_user_tm_compatsem2 single_proc_exit_user_spec).
eapply get_layer_primitive_left; auto; decision.
+ econstructor; eauto; simpl.
econstructor; eauto; simpl.
× unfold single_proc_exit_user_spec.
inv H3; simpl in *; rewritesb.
rewrite H9, H11, H13, H14, H6.
unfold curid, cpu in H7; rewrite H7.
reflexivity.
+ instantiate (1:= kctxt).
inv H3; constructor; auto.
{ simpl.
unfold curid0.
rewrite ZMap.gss.
fold uctx1.
fold uctx2.
fold uctx3.
fold uctx4.
reflexivity. }
{ inv inv_re; constructor; simpl; auto. }
+ rewrite in_event; auto.
Opaque update uRData proc_id.
Fail idtac.
Qed.
End ABS_RELT_INSTANCE.
End PHThread2TREFGEN.