Library mcertikos.virt.intel.EPTIntroGenAccessor
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
This file provide the contextual refinement proof between MAL layer and MPTIntro layer
Section Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Require Import LoadStoreSem2.
Require Import GuestAccessIntel2.
Require Import GuestAccessIntel1.
Require Import HostAccess2.
Require Import LoadStoreGeneral.
Notation hStore := (fun F V ⇒ exec_storeex3 (flatmem_store := flatmem_store) (F:=F) (V:=V)).
Notation lStore := (fun F V ⇒ exec_storeex2 (flatmem_store := flatmem_store) (F:=F) (V:=V)).
Notation lLoad := (fun F V ⇒ exec_loadex2 (F:=F) (V:=V)).
Notation hLoad := (fun F V ⇒ exec_loadex3 (F:=F) (V:=V)).
Lemma guest_intel_correct21:
∀ {F V} (ge: Genv.t F V) accessor2 accessor1 m1 m1´ m2 d1 d2 d1´ rs1 rs2 rs1´ f s rd t i,
exec_guest_intel_accessor2 accessor2 i t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´)
→ MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1 m1 d1 rs2 m2 d2
→ stencil_matches s ge
→ ∀ ACCESSOR_CORRECT:
(∀ i0 i i´,
accessor2 (Int.unsigned i0) i´ t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´) →
i = Int64.repr (Int.unsigned i0) →
∃ r´0 m2´ d2´,
accessor1 i i´ t (m2, d2) rs2 rd = Next r´0 (m2´, d2´) ∧
MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´),
∃ r´0 m2´ d2´,
exec_guest_intel_accessor1 ge accessor1 i t (m2, d2) rs2 rd = Next r´0 (m2´, d2´)
∧ MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´.
Proof.
unfold exec_guest_intel_accessor1, exec_guest_intel_accessor2. intros.
pose proof H0 as Hmatch.
inv H0. inv match_extcall_states.
generalize match_match. intros HM. inv match_match.
inv H0.
assert (HFB: Genv.find_symbol ge EPT_LOC = Some b).
{
inv H1. congruence.
}
rewrite HFB.
Opaque Z.mul.
simpl.
lift_trivial.
erewrite EPT_PML4_INDEX_unsigned in ×.
change (Int.unsigned (Int.repr (0 × 8))) with 0.
simpl in H.
inv HMat; rewrite <- H3 in H; contra_inv.
rewrite HLD. rewrite peq_true.
revert H. inv match_related. subrewrite´´. intros HLoad.
change ((4096 + 7) / 4096 × 4096) with 4096.
pose proof (EPT_PDPT_INDEX_range i) as HR.
specialize (HMat0 _ HR).
inv HMat0; rewrite <- H2 in HLoad; contra_inv.
rewrite EPT_PDPT_INDEX_max in HR.
rewrite Int.unsigned_repr; [|rewrite_omega].
rewrite HLD0. rewrite peq_true. rewrite Hofs.
replace (((EPT_PDPT_INDEX (Int.unsigned i) + 2) × 4096 + 7) / 4096) with
(EPT_PDPT_INDEX (Int.unsigned i) + 2)
by (rewrite Z_div_plus_full_l; [|omega];
change (7/4096) with 0;
rewrite Z.add_0_r; reflexivity).
pose proof (EPT_PDIR_INDEX_range i) as HR1.
specialize (HMat _ HR1).
inv HMat; rewrite <- H4 in HLoad; contra_inv.
rewrite EPT_PDIR_INDEX_max in HR1.
rewrite Int.unsigned_repr; [|rewrite_omega].
rewrite HLD1. rewrite peq_true. rewrite Hofs0.
replace (((6 + EPT_PDPT_INDEX (Int.unsigned i) × 512 +
EPT_PDIR_INDEX (Int.unsigned i)) × 4096 + 7) / 4096) with
(6 + EPT_PDPT_INDEX (Int.unsigned i) × 512 +
EPT_PDIR_INDEX (Int.unsigned i))
by (rewrite Z_div_plus_full_l; [|omega];
change (7/4096) with 0;
rewrite Z.add_0_r; reflexivity).
pose proof (EPT_PTAB_INDEX_range i) as HR2.
specialize (HMat0 _ HR2).
rewrite EPT_PTAB_INDEX_max in HR2.
rewrite Int.unsigned_repr; [|rewrite_omega].
inv HMat0; rewrite <- H5 in HLoad; contra_inv.
rewrite HLD2.
eauto.
Qed.
Lemma Int_unsigned_64_range:
∀ i,
0 ≤ Int.unsigned i ≤ Int64.max_unsigned.
Proof.
change Int64.max_unsigned with (MAX_INT_64 - 1).
intros. specialize (Int.unsigned_range i).
change Int.modulus with MAX_INT_32.
intros. omega.
Qed.
Lemma load_correct:
load_accessor_sim_def HDATAOps LDATAOps (one_crel HDATA LDATA) hLoad lLoad.
Proof.
unfold load_accessor_sim_def. intros.
pose proof H2 as Hmatch.
inv H2. inv match_extcall_states.
unfold exec_loadex3 in ×.
unfold exec_loadex2.
unfold exec_guest_intel_load1, exec_guest_intel_load2 in ×.
inv H4.
exploit (eval_addrmode_correct ge1 ge2 a); eauto. intros HW.
Local Opaque Z.sub.
simpl in ×. revert H1. inv match_related. subrewrite´´. intros HLoad.
destruct (eval_addrmode ge1 a rs1) eqn: Hev; contra_inv.
-
inv HW. destruct (ihost d2) eqn:HPH; contra_inv.
destruct (pg d2) eqn:HPE; contra_inv.
destruct (ipt d2) eqn:HIPT; contra_inv.
+
eapply host_load_correct2; eauto.
+
eapply guest_intel_correct21; eauto.
intros. unfold load_accessor2, load_accessor1 in ×.
subdestruct. subrewrite´.
rewrite Int64.unsigned_repr.
rewrite Int.repr_unsigned.
eapply exec_flatmem_load_correct; eauto.
eapply Int_unsigned_64_range; eauto.
-
inv HW; subdestruct; eapply loadl_correct; eauto.
Qed.
Lemma store_correct:
store_accessor_sim_def HDATAOps LDATAOps (one_crel HDATA LDATA) hStore lStore.
Proof.
unfold store_accessor_sim_def. intros.
pose proof H2 as Hmatch.
inv H2. inv match_extcall_states.
unfold exec_storeex3 in ×.
unfold exec_storeex2.
unfold exec_guest_intel_store1, exec_guest_intel_store2 in ×.
inv H4.
exploit (eval_addrmode_correct ge1 ge2 a); eauto. intros HW.
Local Opaque Z.sub.
simpl in ×. revert H1. inv match_related. subrewrite´´. intros HLoad.
destruct (eval_addrmode ge1 a rs1) eqn: Hev; contra_inv.
-
inv HW. destruct (ihost d2) eqn:HPH; contra_inv.
destruct (pg d2) eqn:HPE; contra_inv.
destruct (ipt d2) eqn:HIPT; contra_inv.
+
eapply host_store_correct2; eauto.
+
eapply guest_intel_correct21; eauto.
unfold store_accessor2, store_accessor1 in ×. intros.
subdestruct. subrewrite´.
rewrite Int64.unsigned_repr.
rewrite Int.repr_unsigned.
eapply exec_flatmem_store_correct; eauto.
apply PTADDR_mod_lt. assumption.
eapply Int_unsigned_64_range; eauto.
-
inv HW; subdestruct; eapply storel_correct; eauto.
Qed.
End WITHMEM.
End Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Require Import LoadStoreSem2.
Require Import GuestAccessIntel2.
Require Import GuestAccessIntel1.
Require Import HostAccess2.
Require Import LoadStoreGeneral.
Notation hStore := (fun F V ⇒ exec_storeex3 (flatmem_store := flatmem_store) (F:=F) (V:=V)).
Notation lStore := (fun F V ⇒ exec_storeex2 (flatmem_store := flatmem_store) (F:=F) (V:=V)).
Notation lLoad := (fun F V ⇒ exec_loadex2 (F:=F) (V:=V)).
Notation hLoad := (fun F V ⇒ exec_loadex3 (F:=F) (V:=V)).
Lemma guest_intel_correct21:
∀ {F V} (ge: Genv.t F V) accessor2 accessor1 m1 m1´ m2 d1 d2 d1´ rs1 rs2 rs1´ f s rd t i,
exec_guest_intel_accessor2 accessor2 i t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´)
→ MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1 m1 d1 rs2 m2 d2
→ stencil_matches s ge
→ ∀ ACCESSOR_CORRECT:
(∀ i0 i i´,
accessor2 (Int.unsigned i0) i´ t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´) →
i = Int64.repr (Int.unsigned i0) →
∃ r´0 m2´ d2´,
accessor1 i i´ t (m2, d2) rs2 rd = Next r´0 (m2´, d2´) ∧
MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´),
∃ r´0 m2´ d2´,
exec_guest_intel_accessor1 ge accessor1 i t (m2, d2) rs2 rd = Next r´0 (m2´, d2´)
∧ MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´.
Proof.
unfold exec_guest_intel_accessor1, exec_guest_intel_accessor2. intros.
pose proof H0 as Hmatch.
inv H0. inv match_extcall_states.
generalize match_match. intros HM. inv match_match.
inv H0.
assert (HFB: Genv.find_symbol ge EPT_LOC = Some b).
{
inv H1. congruence.
}
rewrite HFB.
Opaque Z.mul.
simpl.
lift_trivial.
erewrite EPT_PML4_INDEX_unsigned in ×.
change (Int.unsigned (Int.repr (0 × 8))) with 0.
simpl in H.
inv HMat; rewrite <- H3 in H; contra_inv.
rewrite HLD. rewrite peq_true.
revert H. inv match_related. subrewrite´´. intros HLoad.
change ((4096 + 7) / 4096 × 4096) with 4096.
pose proof (EPT_PDPT_INDEX_range i) as HR.
specialize (HMat0 _ HR).
inv HMat0; rewrite <- H2 in HLoad; contra_inv.
rewrite EPT_PDPT_INDEX_max in HR.
rewrite Int.unsigned_repr; [|rewrite_omega].
rewrite HLD0. rewrite peq_true. rewrite Hofs.
replace (((EPT_PDPT_INDEX (Int.unsigned i) + 2) × 4096 + 7) / 4096) with
(EPT_PDPT_INDEX (Int.unsigned i) + 2)
by (rewrite Z_div_plus_full_l; [|omega];
change (7/4096) with 0;
rewrite Z.add_0_r; reflexivity).
pose proof (EPT_PDIR_INDEX_range i) as HR1.
specialize (HMat _ HR1).
inv HMat; rewrite <- H4 in HLoad; contra_inv.
rewrite EPT_PDIR_INDEX_max in HR1.
rewrite Int.unsigned_repr; [|rewrite_omega].
rewrite HLD1. rewrite peq_true. rewrite Hofs0.
replace (((6 + EPT_PDPT_INDEX (Int.unsigned i) × 512 +
EPT_PDIR_INDEX (Int.unsigned i)) × 4096 + 7) / 4096) with
(6 + EPT_PDPT_INDEX (Int.unsigned i) × 512 +
EPT_PDIR_INDEX (Int.unsigned i))
by (rewrite Z_div_plus_full_l; [|omega];
change (7/4096) with 0;
rewrite Z.add_0_r; reflexivity).
pose proof (EPT_PTAB_INDEX_range i) as HR2.
specialize (HMat0 _ HR2).
rewrite EPT_PTAB_INDEX_max in HR2.
rewrite Int.unsigned_repr; [|rewrite_omega].
inv HMat0; rewrite <- H5 in HLoad; contra_inv.
rewrite HLD2.
eauto.
Qed.
Lemma Int_unsigned_64_range:
∀ i,
0 ≤ Int.unsigned i ≤ Int64.max_unsigned.
Proof.
change Int64.max_unsigned with (MAX_INT_64 - 1).
intros. specialize (Int.unsigned_range i).
change Int.modulus with MAX_INT_32.
intros. omega.
Qed.
Lemma load_correct:
load_accessor_sim_def HDATAOps LDATAOps (one_crel HDATA LDATA) hLoad lLoad.
Proof.
unfold load_accessor_sim_def. intros.
pose proof H2 as Hmatch.
inv H2. inv match_extcall_states.
unfold exec_loadex3 in ×.
unfold exec_loadex2.
unfold exec_guest_intel_load1, exec_guest_intel_load2 in ×.
inv H4.
exploit (eval_addrmode_correct ge1 ge2 a); eauto. intros HW.
Local Opaque Z.sub.
simpl in ×. revert H1. inv match_related. subrewrite´´. intros HLoad.
destruct (eval_addrmode ge1 a rs1) eqn: Hev; contra_inv.
-
inv HW. destruct (ihost d2) eqn:HPH; contra_inv.
destruct (pg d2) eqn:HPE; contra_inv.
destruct (ipt d2) eqn:HIPT; contra_inv.
+
eapply host_load_correct2; eauto.
+
eapply guest_intel_correct21; eauto.
intros. unfold load_accessor2, load_accessor1 in ×.
subdestruct. subrewrite´.
rewrite Int64.unsigned_repr.
rewrite Int.repr_unsigned.
eapply exec_flatmem_load_correct; eauto.
eapply Int_unsigned_64_range; eauto.
-
inv HW; subdestruct; eapply loadl_correct; eauto.
Qed.
Lemma store_correct:
store_accessor_sim_def HDATAOps LDATAOps (one_crel HDATA LDATA) hStore lStore.
Proof.
unfold store_accessor_sim_def. intros.
pose proof H2 as Hmatch.
inv H2. inv match_extcall_states.
unfold exec_storeex3 in ×.
unfold exec_storeex2.
unfold exec_guest_intel_store1, exec_guest_intel_store2 in ×.
inv H4.
exploit (eval_addrmode_correct ge1 ge2 a); eauto. intros HW.
Local Opaque Z.sub.
simpl in ×. revert H1. inv match_related. subrewrite´´. intros HLoad.
destruct (eval_addrmode ge1 a rs1) eqn: Hev; contra_inv.
-
inv HW. destruct (ihost d2) eqn:HPH; contra_inv.
destruct (pg d2) eqn:HPE; contra_inv.
destruct (ipt d2) eqn:HIPT; contra_inv.
+
eapply host_store_correct2; eauto.
+
eapply guest_intel_correct21; eauto.
unfold store_accessor2, store_accessor1 in ×. intros.
subdestruct. subrewrite´.
rewrite Int64.unsigned_repr.
rewrite Int.repr_unsigned.
eapply exec_flatmem_store_correct; eauto.
apply PTADDR_mod_lt. assumption.
eapply Int_unsigned_64_range; eauto.
-
inv HW; subdestruct; eapply storel_correct; eauto.
Qed.
End WITHMEM.
End Refinement.