Library mcertikos.objects.ObjEPT
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalRealIntelModule.
Require Import CalTicketLock.
Require Import liblayers.compat.CompatGenSem.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section OBJ_EPT.
Context `{real_params: RealParams}.
primitive: set value of n-th entry of guest page table layer construct nested page table, with the last layer mapping to undef addr
Function setEPML4_spec (pml4: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
let ept´ := ZMap.set pml4 (EPML4EValid (ZMap.init EPDPTEUndef)) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
else None
| _ ⇒ None
end.
Function setEPDPTE_spec (pml4 pdpt: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
let pdpte´ := ZMap.set pdpt (EPDPTEValid (ZMap.init EPDTEUndef)) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function setEPDTE_spec (pml4 pdpt pdir: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
let epdt´ := ZMap.set pdir (EPDTEValid (ZMap.init EPTEUndef)) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function getEPTE_spec (pml4 pdpt pdir ptab: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
if zle_le 0 ptab (EPT_PTAB_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
match ZMap.get ptab eptab with
| EPTEValid hpa ⇒ Some hpa
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
| _ ⇒ None
end.
Function setEPTE_spec (pml4 pdpt pdir ptab hpa: Z) (adt: RData): option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
if zle_le 0 ptab (EPT_PTAB_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let eptab´ := ZMap.set ptab (EPTEValid hpa) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
| _ ⇒ None
end.
Definition EPT_PTAB_INDEX´ (i:Z) := i mod five_one_two.
Definition EPT_PDIR_INDEX´ (i:Z) := (i/ five_one_two) mod five_one_two.
Definition EPT_PDPT_INDEX´ (i:Z) := (i/ (five_one_two × five_one_two)) mod five_one_two.
Definition EPT_PML4_INDEX´ (i:Z) := (i/ (five_one_two × five_one_two ×
five_one_two)) mod five_one_two.
Function ept_get_page_entry_spec (gpa: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
let pml4 := EPT_PML4_INDEX´ gpa in
let pdpt := EPT_PDPT_INDEX´ gpa in
let pdir := EPT_PDIR_INDEX´ gpa in
let ptab := EPT_PTAB_INDEX´ gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
match ZMap.get ptab eptab with
| EPTEValid hpa ⇒ Some hpa
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function ept_set_page_entry_spec (gpa hpa : Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
if zle_lt 0 hpa maxpage then
let pml4 := EPT_PML4_INDEX´ gpa in
let pdpt := EPT_PDPT_INDEX´ gpa in
let pdir := EPT_PDIR_INDEX´ gpa in
let ptab := EPT_PTAB_INDEX´ gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let eptab´ := ZMap.set ptab (EPTEValid hpa) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept: ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function ept_add_mapping_spec (gpa hpa : Z) (memtype: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
if zle_lt 0 hpa maxpage then
if zle_lt 0 memtype 4096 then
let pml4 := EPT_PML4_INDEX gpa in
let pdpt := EPT_PDPT_INDEX gpa in
let pdir := EPT_PDIR_INDEX gpa in
let ptab := EPT_PTAB_INDEX gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let va := Z.lor (Z.lor (Z.land hpa EPT_ADDR_MASK) EPT_PG_IGNORE_PAT_or_PERM)
(Z.shiftl memtype EPT_PG_MEMORY_TYPE) in
let eptab´ := ZMap.set ptab (EPTEValid va) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some (adt {ept: ZMap.set (CPU_ID adt) ept´ (ept adt)}, 0)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function ept_invalidate_mappings_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function ept_gpa_to_hpa_spec (gpa: Z) (adt: RData) : option Z :=
match ept_get_page_entry_spec gpa adt with
| Some hpa ⇒
if zle_le 0 hpa Int.max_unsigned then
if zeq (Z.land hpa EPTEPERM) 0 then (Some 0)
else let va := Z.lor (Z.land hpa EPT_ADDR_MASK)
(Z.land gpa EPT_ADDR_OFFSET_MASK) in
Some va
else None
| _ ⇒ None
end.
Function ept_mmap_spec (gpa hpa : Z) (memtype: Z) (adt: RData) : option (RData × Z) :=
match ept_get_page_entry_spec gpa adt with
| Some hpa´ ⇒
if (zle_le 0 hpa´ Int.max_unsigned) then
if zle_lt 0 memtype 4096 then
(if zeq (Z.land hpa´ EPTEPERM) 0
then ept_add_mapping_spec gpa hpa memtype adt
else Some (adt, 1))
else None
else None
| _ ⇒ None
end.
Function ept_set_permission_spec (gpa perm: Z) (adt: RData) : option RData :=
match ept_get_page_entry_spec gpa adt with
| Some hpa´ ⇒
if (zle_le 0 hpa´ Int.max_unsigned) then
(let hpa := Z.lor (Z.land hpa´ EPT_NO_PERM)
(Z.land perm EPTEPERM) in
ept_set_page_entry_spec gpa hpa adt)
else None
| _ ⇒ None
end.
Function ept_init_spec (adt: RData) : option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true, true, true) ⇒
Some adt {ept: ZMap.set (CPU_ID adt)
(Calculate_EPDPTE 3 (ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef))
(ZMap.get (CPU_ID adt) (ept adt)))) (ept adt)}
| _ ⇒ None
end.
End OBJ_EPT.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section EPT_GET_PAGE_ENTRY_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_CPU_ID}.
Context {re2: relate_impl_ept}.
Lemma ept_get_page_entry_exist:
∀ s habd labd gpa hpa f,
ept_get_page_entry_spec gpa habd = Some hpa
→ relate_AbData s f habd labd
→ ept_get_page_entry_spec gpa labd = Some hpa.
Proof.
unfold ept_get_page_entry_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma ept_get_page_entry_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ept_get_page_entry_spec)
(id ↦ gensem ept_get_page_entry_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite ept_get_page_entry_exist; eauto.
reflexivity.
Qed.
End EPT_GET_PAGE_ENTRY_SIM.
Section EPT_SET_PAGE_ENTRY_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_set_page_entry_exist:
∀ s habd habd´ labd gpa hpa´ f,
ept_set_page_entry_spec gpa hpa´ habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_set_page_entry_spec gpa hpa´ labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ept_set_page_entry_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_ept_update. assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ept}.
Lemma ept_set_page_entry_match:
∀ s d d´ m gpa hpa´ f,
ept_set_page_entry_spec gpa hpa´ d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_set_page_entry_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ept_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_set_page_entry_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_set_page_entry_spec}.
Lemma ept_set_page_entry_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_set_page_entry_spec)
(id ↦ gensem ept_set_page_entry_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_set_page_entry_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_set_page_entry_match; eauto.
Qed.
End EPT_SET_PAGE_ENTRY_SIM.
Section EPT_ADD_MAPPING_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_add_mapping_exist:
∀ s habd habd´ labd gpa hpa´ memtype n f,
ept_add_mapping_spec gpa hpa´ memtype habd = Some (habd´, n)
→ relate_AbData s f habd labd
→ ∃ labd´, ept_add_mapping_spec gpa hpa´ memtype labd = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.shiftl.
unfold ept_add_mapping_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_ept_update. assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ept}.
Lemma ept_add_mapping_match:
∀ s d d´ m gpa hpa´ memtype n f,
ept_add_mapping_spec gpa hpa´ memtype d = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_add_mapping_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ept_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_add_mapping_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_add_mapping_spec}.
Lemma ept_add_mapping_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_add_mapping_spec)
(id ↦ gensem ept_add_mapping_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_add_mapping_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_add_mapping_match; eauto.
Qed.
End EPT_ADD_MAPPING_SIM.
Section EPT_GPA_TO_HPA_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_gpa_to_hpa_exist:
∀ s habd labd gpa va f,
ept_gpa_to_hpa_spec gpa habd = Some va
→ relate_AbData s f habd labd
→ ept_gpa_to_hpa_spec gpa labd = Some va.
Proof.
Local Opaque Z.land Z.lor.
unfold ept_gpa_to_hpa_spec. intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
revert H. subrewrite.
Qed.
End EPT_GPA_TO_HPA_SIM.
Section EPT_MMAP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_mmap_exist:
∀ s habd habd´ labd gpa hpa´ memtype n f,
ept_mmap_spec gpa hpa´ memtype habd = Some (habd´, n)
→ relate_AbData s f habd labd
→ ∃ labd´, ept_mmap_spec gpa hpa´ memtype labd = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land.
unfold ept_mmap_spec; intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
revert H. subrewrite. subdestruct.
- eapply ept_add_mapping_exist; eassumption.
- inv HQ; refine_split´; trivial.
Qed.
End EPT_MMAP_SIM.
Section EPT_SET_PERMISSION_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_set_permission_exist:
∀ s habd habd´ labd gpa perm f,
ept_set_permission_spec gpa perm habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_set_permission_spec gpa perm labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.lor.
unfold ept_set_permission_spec; intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
subrewrite´. subdestruct.
eapply ept_set_page_entry_exist; eassumption.
Qed.
End EPT_SET_PERMISSION_SIM.
Section EPT_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re10: relate_impl_smspool}.
Context {re11: relate_impl_abtcb}.
Context {re12: relate_impl_abq}.
Context {re13: relate_impl_cid}.
Context {re14: relate_impl_syncchpool}.
Context {re15: relate_impl_vmxinfo}.
Context {re16: relate_impl_ept}.
Context {re17: relate_impl_AC}.
Context {re18: relate_impl_in_intr}.
Context {re19: relate_impl_ioapic}.
Context {re20: relate_impl_lapic}.
Context {re21: relate_impl_CPU_ID}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re300: relate_impl_big_log}.
Lemma ept_init_exist:
∀ s habd habd´ labd f,
ept_init_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_init_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ept_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
rewrite H.
apply relate_impl_ept_update.
assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_nps}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_PT}.
Context {mt7: match_impl_ptpool}.
Context {mt8: match_impl_idpde}.
Context {mt10: match_impl_smspool}.
Context {mt11: match_impl_abtcb}.
Context {mt12: match_impl_abq}.
Context {mt13: match_impl_cid}.
Context {mt14: match_impl_syncchpool}.
Context {mt15: match_impl_vmxinfo}.
Context {mt16: match_impl_ept}.
Context {mt17: match_impl_AC}.
Context {mt18: match_impl_ioapic}.
Context {mt19: match_impl_lapic}.
Context {mt50: match_impl_big_log}.
Context {mt30: match_impl_syncchpool}.
Lemma ept_init_match:
∀ s d d´ m f,
ept_init_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_init_spec; intros. subdestruct. inv H.
eapply match_impl_ept_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_init_spec}.
Lemma ept_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_init_spec)
(id ↦ gensem ept_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_init_match; eauto.
Qed.
End EPT_INIT_SIM.
Section EPT_INV_SIM.
Context {re1: relate_impl_iflags}.
Lemma ept_invalidate_mappings_exists:
∀ habd labd z s f,
ept_invalidate_mappings_spec habd = Some z →
relate_AbData s f habd labd →
ept_invalidate_mappings_spec labd = Some z.
Proof.
unfold ept_invalidate_mappings_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
Qed.
Lemma ept_invalidate_mappings_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ept_invalidate_mappings_spec)
(id ↦ gensem ept_invalidate_mappings_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite ept_invalidate_mappings_exists; eauto.
reflexivity.
Qed.
End EPT_INV_SIM.
End OBJ_SIM.
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
let ept´ := ZMap.set pml4 (EPML4EValid (ZMap.init EPDPTEUndef)) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
else None
| _ ⇒ None
end.
Function setEPDPTE_spec (pml4 pdpt: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
let pdpte´ := ZMap.set pdpt (EPDPTEValid (ZMap.init EPDTEUndef)) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function setEPDTE_spec (pml4 pdpt pdir: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
let epdt´ := ZMap.set pdir (EPDTEValid (ZMap.init EPTEUndef)) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function getEPTE_spec (pml4 pdpt pdir ptab: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
if zle_le 0 ptab (EPT_PTAB_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
match ZMap.get ptab eptab with
| EPTEValid hpa ⇒ Some hpa
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
| _ ⇒ None
end.
Function setEPTE_spec (pml4 pdpt pdir ptab hpa: Z) (adt: RData): option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_le 0 pml4 (EPT_PML4_INDEX Int.max_unsigned) then
if zle_le 0 pdpt (EPT_PDPT_INDEX Int.max_unsigned) then
if zle_le 0 pdir (EPT_PDIR_INDEX Int.max_unsigned) then
if zle_le 0 ptab (EPT_PTAB_INDEX Int.max_unsigned) then
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let eptab´ := ZMap.set ptab (EPTEValid hpa) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept : ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
| _ ⇒ None
end.
Definition EPT_PTAB_INDEX´ (i:Z) := i mod five_one_two.
Definition EPT_PDIR_INDEX´ (i:Z) := (i/ five_one_two) mod five_one_two.
Definition EPT_PDPT_INDEX´ (i:Z) := (i/ (five_one_two × five_one_two)) mod five_one_two.
Definition EPT_PML4_INDEX´ (i:Z) := (i/ (five_one_two × five_one_two ×
five_one_two)) mod five_one_two.
Function ept_get_page_entry_spec (gpa: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
let pml4 := EPT_PML4_INDEX´ gpa in
let pdpt := EPT_PDPT_INDEX´ gpa in
let pdir := EPT_PDIR_INDEX´ gpa in
let ptab := EPT_PTAB_INDEX´ gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
match ZMap.get ptab eptab with
| EPTEValid hpa ⇒ Some hpa
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function ept_set_page_entry_spec (gpa hpa : Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
if zle_lt 0 hpa maxpage then
let pml4 := EPT_PML4_INDEX´ gpa in
let pdpt := EPT_PDPT_INDEX´ gpa in
let pdir := EPT_PDIR_INDEX´ gpa in
let ptab := EPT_PTAB_INDEX´ gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let eptab´ := ZMap.set ptab (EPTEValid hpa) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some adt {ept: ZMap.set (CPU_ID adt) ept´ (ept adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function ept_add_mapping_spec (gpa hpa : Z) (memtype: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 gpa maxpage then
if zle_lt 0 hpa maxpage then
if zle_lt 0 memtype 4096 then
let pml4 := EPT_PML4_INDEX gpa in
let pdpt := EPT_PDPT_INDEX gpa in
let pdir := EPT_PDIR_INDEX gpa in
let ptab := EPT_PTAB_INDEX gpa in
match ZMap.get pml4 (ZMap.get (CPU_ID adt) (ept adt)) with
| EPML4EValid epdpt ⇒
match ZMap.get pdpt epdpt with
| EPDPTEValid epdt ⇒
match ZMap.get pdir epdt with
| EPDTEValid eptab ⇒
let va := Z.lor (Z.lor (Z.land hpa EPT_ADDR_MASK) EPT_PG_IGNORE_PAT_or_PERM)
(Z.shiftl memtype EPT_PG_MEMORY_TYPE) in
let eptab´ := ZMap.set ptab (EPTEValid va) eptab in
let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ZMap.get (CPU_ID adt) (ept adt)) in
Some (adt {ept: ZMap.set (CPU_ID adt) ept´ (ept adt)}, 0)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function ept_invalidate_mappings_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function ept_gpa_to_hpa_spec (gpa: Z) (adt: RData) : option Z :=
match ept_get_page_entry_spec gpa adt with
| Some hpa ⇒
if zle_le 0 hpa Int.max_unsigned then
if zeq (Z.land hpa EPTEPERM) 0 then (Some 0)
else let va := Z.lor (Z.land hpa EPT_ADDR_MASK)
(Z.land gpa EPT_ADDR_OFFSET_MASK) in
Some va
else None
| _ ⇒ None
end.
Function ept_mmap_spec (gpa hpa : Z) (memtype: Z) (adt: RData) : option (RData × Z) :=
match ept_get_page_entry_spec gpa adt with
| Some hpa´ ⇒
if (zle_le 0 hpa´ Int.max_unsigned) then
if zle_lt 0 memtype 4096 then
(if zeq (Z.land hpa´ EPTEPERM) 0
then ept_add_mapping_spec gpa hpa memtype adt
else Some (adt, 1))
else None
else None
| _ ⇒ None
end.
Function ept_set_permission_spec (gpa perm: Z) (adt: RData) : option RData :=
match ept_get_page_entry_spec gpa adt with
| Some hpa´ ⇒
if (zle_le 0 hpa´ Int.max_unsigned) then
(let hpa := Z.lor (Z.land hpa´ EPT_NO_PERM)
(Z.land perm EPTEPERM) in
ept_set_page_entry_spec gpa hpa adt)
else None
| _ ⇒ None
end.
Function ept_init_spec (adt: RData) : option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true, true, true) ⇒
Some adt {ept: ZMap.set (CPU_ID adt)
(Calculate_EPDPTE 3 (ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef))
(ZMap.get (CPU_ID adt) (ept adt)))) (ept adt)}
| _ ⇒ None
end.
End OBJ_EPT.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section EPT_GET_PAGE_ENTRY_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_CPU_ID}.
Context {re2: relate_impl_ept}.
Lemma ept_get_page_entry_exist:
∀ s habd labd gpa hpa f,
ept_get_page_entry_spec gpa habd = Some hpa
→ relate_AbData s f habd labd
→ ept_get_page_entry_spec gpa labd = Some hpa.
Proof.
unfold ept_get_page_entry_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma ept_get_page_entry_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ept_get_page_entry_spec)
(id ↦ gensem ept_get_page_entry_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite ept_get_page_entry_exist; eauto.
reflexivity.
Qed.
End EPT_GET_PAGE_ENTRY_SIM.
Section EPT_SET_PAGE_ENTRY_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_set_page_entry_exist:
∀ s habd habd´ labd gpa hpa´ f,
ept_set_page_entry_spec gpa hpa´ habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_set_page_entry_spec gpa hpa´ labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ept_set_page_entry_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_ept_update. assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ept}.
Lemma ept_set_page_entry_match:
∀ s d d´ m gpa hpa´ f,
ept_set_page_entry_spec gpa hpa´ d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_set_page_entry_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ept_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_set_page_entry_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_set_page_entry_spec}.
Lemma ept_set_page_entry_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_set_page_entry_spec)
(id ↦ gensem ept_set_page_entry_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_set_page_entry_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_set_page_entry_match; eauto.
Qed.
End EPT_SET_PAGE_ENTRY_SIM.
Section EPT_ADD_MAPPING_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_add_mapping_exist:
∀ s habd habd´ labd gpa hpa´ memtype n f,
ept_add_mapping_spec gpa hpa´ memtype habd = Some (habd´, n)
→ relate_AbData s f habd labd
→ ∃ labd´, ept_add_mapping_spec gpa hpa´ memtype labd = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.shiftl.
unfold ept_add_mapping_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_ept_update. assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ept}.
Lemma ept_add_mapping_match:
∀ s d d´ m gpa hpa´ memtype n f,
ept_add_mapping_spec gpa hpa´ memtype d = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_add_mapping_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ept_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_add_mapping_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_add_mapping_spec}.
Lemma ept_add_mapping_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_add_mapping_spec)
(id ↦ gensem ept_add_mapping_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_add_mapping_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_add_mapping_match; eauto.
Qed.
End EPT_ADD_MAPPING_SIM.
Section EPT_GPA_TO_HPA_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_gpa_to_hpa_exist:
∀ s habd labd gpa va f,
ept_gpa_to_hpa_spec gpa habd = Some va
→ relate_AbData s f habd labd
→ ept_gpa_to_hpa_spec gpa labd = Some va.
Proof.
Local Opaque Z.land Z.lor.
unfold ept_gpa_to_hpa_spec. intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
revert H. subrewrite.
Qed.
End EPT_GPA_TO_HPA_SIM.
Section EPT_MMAP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_mmap_exist:
∀ s habd habd´ labd gpa hpa´ memtype n f,
ept_mmap_spec gpa hpa´ memtype habd = Some (habd´, n)
→ relate_AbData s f habd labd
→ ∃ labd´, ept_mmap_spec gpa hpa´ memtype labd = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land.
unfold ept_mmap_spec; intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
revert H. subrewrite. subdestruct.
- eapply ept_add_mapping_exist; eassumption.
- inv HQ; refine_split´; trivial.
Qed.
End EPT_MMAP_SIM.
Section EPT_SET_PERMISSION_SIM.
Context {re1: relate_impl_iflags}.
Context {re2 : relate_impl_ept}.
Context {re3: relate_impl_CPU_ID}.
Lemma ept_set_permission_exist:
∀ s habd habd´ labd gpa perm f,
ept_set_permission_spec gpa perm habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_set_permission_spec gpa perm labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.lor.
unfold ept_set_permission_spec; intros.
destruct (ept_get_page_entry_spec gpa habd) eqn:Hdestruct; try discriminate.
exploit ept_get_page_entry_exist; eauto. intros.
subrewrite´. subdestruct.
eapply ept_set_page_entry_exist; eassumption.
Qed.
End EPT_SET_PERMISSION_SIM.
Section EPT_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re10: relate_impl_smspool}.
Context {re11: relate_impl_abtcb}.
Context {re12: relate_impl_abq}.
Context {re13: relate_impl_cid}.
Context {re14: relate_impl_syncchpool}.
Context {re15: relate_impl_vmxinfo}.
Context {re16: relate_impl_ept}.
Context {re17: relate_impl_AC}.
Context {re18: relate_impl_in_intr}.
Context {re19: relate_impl_ioapic}.
Context {re20: relate_impl_lapic}.
Context {re21: relate_impl_CPU_ID}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re300: relate_impl_big_log}.
Lemma ept_init_exist:
∀ s habd habd´ labd f,
ept_init_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ept_init_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ept_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_ept_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
rewrite H.
apply relate_impl_ept_update.
assumption.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_nps}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_PT}.
Context {mt7: match_impl_ptpool}.
Context {mt8: match_impl_idpde}.
Context {mt10: match_impl_smspool}.
Context {mt11: match_impl_abtcb}.
Context {mt12: match_impl_abq}.
Context {mt13: match_impl_cid}.
Context {mt14: match_impl_syncchpool}.
Context {mt15: match_impl_vmxinfo}.
Context {mt16: match_impl_ept}.
Context {mt17: match_impl_AC}.
Context {mt18: match_impl_ioapic}.
Context {mt19: match_impl_lapic}.
Context {mt50: match_impl_big_log}.
Context {mt30: match_impl_syncchpool}.
Lemma ept_init_match:
∀ s d d´ m f,
ept_init_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ept_init_spec; intros. subdestruct. inv H.
eapply match_impl_ept_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ept_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ept_init_spec}.
Lemma ept_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ept_init_spec)
(id ↦ gensem ept_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ept_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ept_init_match; eauto.
Qed.
End EPT_INIT_SIM.
Section EPT_INV_SIM.
Context {re1: relate_impl_iflags}.
Lemma ept_invalidate_mappings_exists:
∀ habd labd z s f,
ept_invalidate_mappings_spec habd = Some z →
relate_AbData s f habd labd →
ept_invalidate_mappings_spec labd = Some z.
Proof.
unfold ept_invalidate_mappings_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
Qed.
Lemma ept_invalidate_mappings_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ept_invalidate_mappings_spec)
(id ↦ gensem ept_invalidate_mappings_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite ept_invalidate_mappings_exists; eauto.
reflexivity.
Qed.
End EPT_INV_SIM.
End OBJ_SIM.