Library mcertikos.proc.EPTIntroGenFresh
This file provide the contextual refinement proof between PProc layer and VEPTIntro layer
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section FRESH_PRIM.
Lemma EPT_PML4_INDEX_range:
∀ i,
0 ≤ Int.unsigned i ≤ EPT_PML4_INDEX (Int.max_unsigned)
→ i = Int.zero.
Proof.
rewrite EPT_PML4_INDEX_max.
intros. rewrite <- (Int.repr_unsigned i).
replace (Int.unsigned i) with 0 by omega.
reflexivity.
Qed.
Lemma EPT_PML4_INDEX_range´:
∀ i,
0 ≤ i ≤ EPT_PML4_INDEX (Int.max_unsigned)
→ i = 0.
Proof.
rewrite EPT_PML4_INDEX_max.
intros. omega.
Qed.
Opaque Z.add.
Lemma ept_invalidate_mappings_spec_ref:
compatsim (crel HDATA LDATA) (gensem ept_invalidate_mappings_spec) ept_invalidate_mappings_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
inv H0.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of Conventions1.destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX<- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv match_related.
econstructor; eauto.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int.repr_unsigned z). rewrite <- H.
constructor.
- intros.
destruct r; simpl; try constructor; elim H0; eauto 13.
Qed.
Lemma setEPML4_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPML4_spec) setEPML4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto.
}
inv H0.
specialize (Mem.valid_access_store _ _ _ _
Vzero HVA´); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA.
specialize (Mem.valid_access_store _ _ _ _ (Vptr b (Int.repr (8413184 × CPU_ID d2 + 4103))) HVA);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
inv Hhigh.
generalize max_unsigned_val; intro muval.
refine_split; eauto.
- econstructor; eauto.
Opaque Z.mul.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d2 + 4103))).
simpl; lift_trivial.
rewrite <- H. rewrite Z.add_0_r. rewrite <- H in HST2. erewrite HST2. reflexivity.
simpl.
rewrite Int.unsigned_repr by omega.
omega.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl. rewrite ZMap.gss.
rewrite ZMap.gss.
econstructor; eauto.
intros. rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + 4096 + 7))).
rewrite Int.unsigned_repr; omega.
rewrite <- H in HST2.
eapply Mem.load_store_same in HST2; eauto.
replace (8413184 × CPU_ID d1 + 4096 + 7) with (8413184 × CPU_ID d1 + 4103) by omega.
eauto.
× specialize (HVA1 _ H5).
destruct HVA1 as (HVA11 & HVA12 & HVA13).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13 _ H7).
destruct HVA13 as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H8).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPDPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPDPTE_spec) setEPDPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto.
}
destruct Hkern as (Hkern & HOS).
inv H0.
destruct (HVA1 _ HOS) as (HVA11 & HVA12 & _).
specialize (Mem.valid_access_store _ _ _ _ Vzero HVA12);
intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA11.
specialize (Mem.valid_access_store _ _ _ _ (Vptr b (Int.repr (8413184 × CPU_ID d1 + ((Int.unsigned i0) + 2) × PgSize + EPTEPERM))) HVA11);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H6 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d1 + (Int.unsigned i0 + 2) × 4096 + 7))).
simpl; lift_trivial.
rewrite <- H.
erewrite HST2. reflexivity.
rewrite Int.unsigned_repr by omega.
simpl.
rewrite <- H.
reflexivity.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite ZMap.gss. econstructor; eauto.
intros. rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + (Int.unsigned i0 + 2) × 4096 + 7))).
rewrite Int.unsigned_repr; trivial.
rewrite_omega.
eapply Mem.load_store_same in HST2; eauto.
}
{
rewrite ZMap.gso; eauto.
specialize (HMat0 _ H7).
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H9).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H10).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
× specialize (HVA1 _ H7).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H9).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H10).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPDTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPDTE_spec) setEPDTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1).
inv H0.
destruct (HVA1 _ HOS) as (_ & _ & HVA13).
specialize (HVA13 _ HOS1).
destruct HVA13 as (HVA0 & HVA0´ & _).
specialize (Mem.valid_access_store _ _ _ _
Vzero HVA0´); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA0.
specialize (Mem.valid_access_store
_ _ _ _
(Vptr b (Int.repr (8413184 × CPU_ID d1 + (6 + (Int.unsigned i0) × 512 + (Int.unsigned i1)) × PgSize + EPTEPERM))) HVA0);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´ epdt´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H7 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
rewrite EPT_PDIR_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d1 + (6 + Int.unsigned i0 × 512 + Int.unsigned i1) × 4096 + 7))).
simpl; lift_trivial. rewrite <- H. erewrite HST2. reflexivity.
rewrite Int.unsigned_repr; trivial.
simpl. rewrite <- H.
reflexivity.
omega.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
specialize (HMat0 _ H9).
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite H8 in ×.
rewrite ZMap.gss. inv HMat0.
econstructor; eauto; intros.
rewrite EPT_PDIR_INDEX_max in ×.
destruct (zeq j (Int.unsigned i1)); subst.
{
rewrite ZMap.gss.
econstructor; eauto; intros.
rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + (6 + Int.unsigned i0 × 512 + Int.unsigned i1) × 4096 + 7))).
rewrite Int.unsigned_repr; trivial.
rewrite_omega.
eapply Mem.load_store_same in HST2; eauto.
}
{
rewrite ZMap.gso; eauto.
specialize (HMat _ H11).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H12).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H11).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H12).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right; omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
× specialize (HVA1 _ H9).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H11).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H12).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPTE_spec) setEPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)
∧ 0 ≤ Int.unsigned i2 ≤ EPT_PTAB_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1 & HOS2).
inv H0.
destruct (HVA1 _ HOS) as (_ & _ & HVA13).
specialize (HVA13 _ HOS1).
destruct HVA13 as (_ & _ & HVA0).
specialize (HVA0 _ HOS2).
specialize (Mem.valid_access_store _ _ _ _
(Vlong (Int64.repr (Int.unsigned i3))) HVA0); intros [m0 HST1].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´ epdt´ eptab´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H8 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
rewrite EPT_PDIR_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
specialize (HMat0 _ H11).
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite H9 in ×.
rewrite ZMap.gss. inv HMat0.
econstructor; eauto; intros.
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H13).
destruct (zeq j (Int.unsigned i1)); subst.
{
rewrite H10 in ×.
rewrite ZMap.gss. inv HMat.
econstructor; eauto; intros.
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H14).
destruct (zeq k (Int.unsigned i2)); subst.
{
rewrite ZMap.gss.
econstructor; eauto; intros.
eapply Mem.load_store_same in HST1; eauto.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt k (Int.unsigned i2)); [left; omega|right; omega].
}
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left. omega.
}
rewrite ZMap.gso; eauto.
{
inv HMat; econstructor; eauto; intros.
{
specialize (HMat0 _ H14).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
rewrite EPT_PTAB_INDEX_max in ×.
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H13).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H14).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
× specialize (HVA1 _ H11).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H13).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H14).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma getEPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem getEPTE_spec) getEPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)
∧ 0 ≤ Int.unsigned i2 ≤ EPT_PTAB_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H2; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1 & HOS2).
pose proof H2 as Hspec.
functional inversion Hspec; subst.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
inv H0.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
econstructor; eauto.
rewrite H9 in HMat.
inv HMat.
specialize (HMat0 _ HOS).
rewrite H10 in HMat0.
inv HMat0. specialize (HMat _ HOS1).
rewrite H11 in HMat.
inv HMat. specialize (HMat0 _ HOS2).
rewrite H12 in HMat0.
inv HMat0.
simpl in ×.
lift_unfold.
rewrite <- H.
assumption.
Qed.
End FRESH_PRIM.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section FRESH_PRIM.
Lemma EPT_PML4_INDEX_range:
∀ i,
0 ≤ Int.unsigned i ≤ EPT_PML4_INDEX (Int.max_unsigned)
→ i = Int.zero.
Proof.
rewrite EPT_PML4_INDEX_max.
intros. rewrite <- (Int.repr_unsigned i).
replace (Int.unsigned i) with 0 by omega.
reflexivity.
Qed.
Lemma EPT_PML4_INDEX_range´:
∀ i,
0 ≤ i ≤ EPT_PML4_INDEX (Int.max_unsigned)
→ i = 0.
Proof.
rewrite EPT_PML4_INDEX_max.
intros. omega.
Qed.
Opaque Z.add.
Lemma ept_invalidate_mappings_spec_ref:
compatsim (crel HDATA LDATA) (gensem ept_invalidate_mappings_spec) ept_invalidate_mappings_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
inv H0.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of Conventions1.destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX<- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv match_related.
econstructor; eauto.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int.repr_unsigned z). rewrite <- H.
constructor.
- intros.
destruct r; simpl; try constructor; elim H0; eauto 13.
Qed.
Lemma setEPML4_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPML4_spec) setEPML4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto.
}
inv H0.
specialize (Mem.valid_access_store _ _ _ _
Vzero HVA´); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA.
specialize (Mem.valid_access_store _ _ _ _ (Vptr b (Int.repr (8413184 × CPU_ID d2 + 4103))) HVA);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
inv Hhigh.
generalize max_unsigned_val; intro muval.
refine_split; eauto.
- econstructor; eauto.
Opaque Z.mul.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d2 + 4103))).
simpl; lift_trivial.
rewrite <- H. rewrite Z.add_0_r. rewrite <- H in HST2. erewrite HST2. reflexivity.
simpl.
rewrite Int.unsigned_repr by omega.
omega.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl. rewrite ZMap.gss.
rewrite ZMap.gss.
econstructor; eauto.
intros. rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + 4096 + 7))).
rewrite Int.unsigned_repr; omega.
rewrite <- H in HST2.
eapply Mem.load_store_same in HST2; eauto.
replace (8413184 × CPU_ID d1 + 4096 + 7) with (8413184 × CPU_ID d1 + 4103) by omega.
eauto.
× specialize (HVA1 _ H5).
destruct HVA1 as (HVA11 & HVA12 & HVA13).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13 _ H7).
destruct HVA13 as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H8).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPDPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPDPTE_spec) setEPDPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto.
}
destruct Hkern as (Hkern & HOS).
inv H0.
destruct (HVA1 _ HOS) as (HVA11 & HVA12 & _).
specialize (Mem.valid_access_store _ _ _ _ Vzero HVA12);
intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA11.
specialize (Mem.valid_access_store _ _ _ _ (Vptr b (Int.repr (8413184 × CPU_ID d1 + ((Int.unsigned i0) + 2) × PgSize + EPTEPERM))) HVA11);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H6 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d1 + (Int.unsigned i0 + 2) × 4096 + 7))).
simpl; lift_trivial.
rewrite <- H.
erewrite HST2. reflexivity.
rewrite Int.unsigned_repr by omega.
simpl.
rewrite <- H.
reflexivity.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite ZMap.gss. econstructor; eauto.
intros. rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + (Int.unsigned i0 + 2) × 4096 + 7))).
rewrite Int.unsigned_repr; trivial.
rewrite_omega.
eapply Mem.load_store_same in HST2; eauto.
}
{
rewrite ZMap.gso; eauto.
specialize (HMat0 _ H7).
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H9).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H10).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
× specialize (HVA1 _ H7).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H9).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H10).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPDTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPDTE_spec) setEPDTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1).
inv H0.
destruct (HVA1 _ HOS) as (_ & _ & HVA13).
specialize (HVA13 _ HOS1).
destruct HVA13 as (HVA0 & HVA0´ & _).
specialize (Mem.valid_access_store _ _ _ _
Vzero HVA0´); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HVA0.
specialize (Mem.valid_access_store
_ _ _ _
(Vptr b (Int.repr (8413184 × CPU_ID d1 + (6 + (Int.unsigned i0) × 512 + (Int.unsigned i1)) × PgSize + EPTEPERM))) HVA0);
intros [m1 HST2].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´ epdt´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H7 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
rewrite EPT_PDIR_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
instantiate (3:= (Int.repr (8413184 × CPU_ID d1 + (6 + Int.unsigned i0 × 512 + Int.unsigned i1) × 4096 + 7))).
simpl; lift_trivial. rewrite <- H. erewrite HST2. reflexivity.
rewrite Int.unsigned_repr; trivial.
simpl. rewrite <- H.
reflexivity.
omega.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
specialize (HMat0 _ H9).
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite H8 in ×.
rewrite ZMap.gss. inv HMat0.
econstructor; eauto; intros.
rewrite EPT_PDIR_INDEX_max in ×.
destruct (zeq j (Int.unsigned i1)); subst.
{
rewrite ZMap.gss.
econstructor; eauto; intros.
rewrite ZMap.gi. constructor.
instantiate (1:= (Int.repr (8413184 × CPU_ID d1 + (6 + Int.unsigned i0 × 512 + Int.unsigned i1) × 4096 + 7))).
rewrite Int.unsigned_repr; trivial.
rewrite_omega.
eapply Mem.load_store_same in HST2; eauto.
}
{
rewrite ZMap.gso; eauto.
specialize (HMat _ H11).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H12).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right. omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H11).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H12).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. right; omega.
simpl; right. right. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
simpl; right. left; omega.
× specialize (HVA1 _ H9).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H11).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H12).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma setEPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem setEPTE_spec) setEPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)
∧ 0 ≤ Int.unsigned i2 ≤ EPT_PTAB_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H1; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1 & HOS2).
inv H0.
destruct (HVA1 _ HOS) as (_ & _ & HVA13).
specialize (HVA13 _ HOS1).
destruct HVA13 as (_ & _ & HVA0).
specialize (HVA0 _ HOS2).
specialize (Mem.valid_access_store _ _ _ _
(Vlong (Int64.repr (Int.unsigned i3))) HVA0); intros [m0 HST1].
pose proof H1 as Hspec.
functional inversion Hspec; subst.
subst ept´ pdpte´ epdt´ eptab´.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
rewrite H8 in ×.
rewrite EPT_PDPT_INDEX_max in ×.
rewrite EPT_PDIR_INDEX_max in ×.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
- econstructor; eauto.
simpl; lift_trivial. rewrite <- H. erewrite HST1. reflexivity.
- split; eauto 1; pattern2_refinement_simpl.
econstructor; eauto 1.
econstructor; eauto 1; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
× simpl; rewrite ZMap.gss.
rewrite ZMap.gss.
inv HMat.
econstructor; eauto; intros.
rewrite EPT_PDPT_INDEX_max in ×.
specialize (HMat0 _ H11).
destruct (zeq j (Int.unsigned i0)); subst.
{
rewrite H9 in ×.
rewrite ZMap.gss. inv HMat0.
econstructor; eauto; intros.
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H13).
destruct (zeq j (Int.unsigned i1)); subst.
{
rewrite H10 in ×.
rewrite ZMap.gss. inv HMat.
econstructor; eauto; intros.
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H14).
destruct (zeq k (Int.unsigned i2)); subst.
{
rewrite ZMap.gss.
econstructor; eauto; intros.
eapply Mem.load_store_same in HST1; eauto.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt k (Int.unsigned i2)); [left; omega|right; omega].
}
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left. omega.
}
rewrite ZMap.gso; eauto.
{
inv HMat; econstructor; eauto; intros.
{
specialize (HMat0 _ H14).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
rewrite EPT_PTAB_INDEX_max in ×.
simpl; right. destruct (zlt j (Int.unsigned i1)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left. omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
{
rewrite ZMap.gso; eauto.
inv HMat0; econstructor; eauto; intros.
{
rewrite EPT_PDIR_INDEX_max in ×.
specialize (HMat _ H13).
inv HMat; econstructor; eauto; intros.
{
rewrite EPT_PTAB_INDEX_max in ×.
specialize (HMat0 _ H14).
inv HMat0; econstructor; eauto; intros.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt j (Int.unsigned i0)); [left; omega|right; omega].
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
}
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. left; omega.
× specialize (HVA1 _ H11).
destruct HVA1 as (HVA11´ & HVA12´ & HVA13´).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA13´ _ H13).
destruct HVA13´ as (HVA131 & HVA132 & HVA133).
refine_split´; repeat (eapply Mem.store_valid_access_1; eauto); intros.
specialize (HVA133 _ H14).
repeat (eapply Mem.store_valid_access_1; eauto).
Qed.
Lemma getEPTE_spec_ref:
compatsim (crel HDATA LDATA) (gensem getEPTE_spec) getEPTE_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2
∧ 0 ≤ Int.unsigned i0 ≤ EPT_PDPT_INDEX Int.max_unsigned
∧ 0 ≤ Int.unsigned i1 ≤ EPT_PDIR_INDEX (Int.max_unsigned)
∧ 0 ≤ Int.unsigned i2 ≤ EPT_PTAB_INDEX (Int.max_unsigned)).
{
inv match_related.
functional inversion H2; subst.
simpl; eauto 10.
}
destruct Hkern as (Hkern & HOS & HOS1 & HOS2).
pose proof H2 as Hspec.
functional inversion Hspec; subst.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
generalize max_unsigned_val; intro muval.
inv Hhigh.
refine_split; eauto.
inv H0.
rewrite (EPT_PML4_INDEX_range´ (Int.unsigned i)) in *; trivial.
rewrite (EPT_PML4_INDEX_range i) in *; trivial.
econstructor; eauto.
rewrite H9 in HMat.
inv HMat.
specialize (HMat0 _ HOS).
rewrite H10 in HMat0.
inv HMat0. specialize (HMat _ HOS1).
rewrite H11 in HMat.
inv HMat. specialize (HMat0 _ HOS2).
rewrite H12 in HMat0.
inv HMat0.
simpl in ×.
lift_unfold.
rewrite <- H.
assumption.
Qed.
End FRESH_PRIM.
End WITHMEM.
End Refinement.