Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import ZSet.
Require Import ListLemma2.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AuxStateDataType.
Require Import RealParams.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import LayerCalculusLemma.
Require Import TacticsForTesting.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import NPTOps.Layer.
Require Import NPTWalk.Layer.
Require Import HypsecCommLib.
Require Import NPTOps.Spec.
Require Import NPTWalk.Spec.
Require Import AbsMachine.Spec.
Require Import Constants.
Require Import RData.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section NPTOpsProofHigh.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := NPTOps_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := NPTWalk_ops) HDATA).
Inductive relate_entry_tlb (curid: Z) (vmid: Z) (hnpt: NPT) (lnpt: NPT): Z -> Z -> Z -> Z -> Prop :=
| RELATE_ENTRY:
forall addr pfn level pte
(Hlevel: level = 0 \/ level = 2 \/ level = 3)
(Hpte0: level = 0 <-> pte = 0)
(Hpfn0: level = 0 -> pfn = 0)
(Hpfn2: level = 2 -> pfn = phys_page pte / PAGE_SIZE +
(addr / PAGE_SIZE - addr / PAGE_SIZE / PTRS_PER_PMD * PTRS_PER_PMD))
(Hpfn3: level = 3 -> pfn = phys_page pte / PAGE_SIZE)
(* FIXME: avoid using adt here *)
(Hlevel0: level = 0 ->
let gfn := addr / PAGE_SIZE in
let pfn1 := tlb_look_up_h2 vmid curid (VZ64 gfn) lnpt in
(pfn1 = Some 0 /\
let '(pfn2, level2, pte2) := ZMap.get (addr / PAGE_SIZE) (pt lnpt) in
pfn2 = 0
)
)
(Hlevel2: level = 2 ->
let gfn := addr / PAGE_SIZE in
let pfn1 := tlb_look_up_h2 vmid curid (VZ64 gfn) lnpt in
(pfn1 <> Some 0 /\
let '(pfn2, level2, pte2) := (addr / PAGE_SIZE) @ (pt lnpt) in
level2 = 2 /\ pfn2 <> 0 /\ pfn1 = Some pfn2)
)
(Hlevel3: level = 3 ->
let gfn := addr / PAGE_SIZE in
let pfn1 := tlb_look_up_h2 vmid curid (VZ64 gfn) lnpt in
(pfn1 <> Some 0 /\
let '(pfn2, level2, pte2) := (addr / PAGE_SIZE) @ (pt lnpt) in
level2 = 3 /\ pfn2 <> 0 /\ pfn1 = Some pfn2)
),
relate_entry_tlb curid vmid hnpt lnpt addr pfn level pte.
Inductive valid_npt_entry (gfn pfn level pte: Z) :=
| VALID_ENTRY:
forall
(Hlevel: level = 0 \/ level = 2 \/ level = 3)
(Hpte0: level = 0 <-> pte = 0)
(Hpfn0: level = 0 -> pfn = 0)
(Hpfn2: level = 2 -> pfn = phys_page pte / PAGE_SIZE +
(gfn - gfn / PTRS_PER_PMD * PTRS_PER_PMD))
(Hpfn3: level = 3 -> pfn = phys_page pte / PAGE_SIZE),
valid_npt_entry gfn pfn level pte.
Inductive relate_npt_tlb : Z -> Z -> NPT -> NPT -> Prop :=
| RELATE_NPT_TLB:
forall curid vmid hnpt lnpt
(Hpt: pt hnpt = pt lnpt)
(Hpgd_t: pgd_t hnpt = pgd_t lnpt)
(Hpud_t: pud_t hnpt = pud_t lnpt)
(Hpmd_t: pmd_t hnpt = pmd_t lnpt)
(Hrelate: forall gfn pfn level,
curid @ (gfn @ (tlbe (tlb lnpt))) = (pfn, level) ->
pfn <> 0 ->
exists pte, ZMap.get gfn (pt lnpt) = (pfn, level, pte))
(* (Hrelate1: forall gfn pfn,
tlb_look_up_h3 curid (VZ64 gfn) lnpt = Some pfn ->
pfn <> 0 ->
exists level pte, ZMap.get gfn (pt lnpt) = (pfn, level, pte)) *)
(Hnpt: forall gfn pfn level pte
(Hhpt: ZMap.get gfn (pt hnpt) = (pfn, level, pte)),
valid_npt_entry gfn pfn level pte)
(Hlevel2: forall gfn pfn pte (Hnpt: ZMap.get gfn (pt hnpt) = (pfn, 2, pte)),
forall gfn' (Hgfn': gfn / 512 * 512 <= gfn' < gfn / 512 * 512 + 512),
exists pfn', ZMap.get gfn' (pt hnpt) = (pfn', 2, pte)),
relate_npt_tlb curid vmid hnpt lnpt.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
(* id_rel: hadt = ladt *)
id_icore: icore hadt = icore ladt;
id_ihost: ihost hadt = ihost ladt;
id_tstate: tstate hadt = tstate ladt;
id_curid: curid hadt = curid ladt;
id_cur_vmid: cur_vmid hadt = cur_vmid ladt;
id_cur_vcpuid: cur_vcpuid hadt = cur_vcpuid ladt;
id_regs: regs hadt = regs ladt;
id_lock: lock hadt = lock ladt;
id_region_cnt: region_cnt hadt = region_cnt ladt;
id_regions: regions hadt = regions ladt;
id_shadow_ctxts: shadow_ctxts hadt = shadow_ctxts ladt;
id_smmu_conf: smmu_conf hadt = smmu_conf ladt;
id_log: log hadt = log ladt;
id_oracle: oracle hadt = oracle ladt;
id_doracle: doracle hadt = doracle ladt;
id_core_doracle: core_doracle hadt = core_doracle ladt;
id_data_log: data_log hadt = data_log ladt;
id_core_data_log: core_data_log hadt = core_data_log ladt;
id_halt: halt hadt = halt ladt;
id_flatmem: flatmem (shared hadt) = flatmem (shared ladt);
id_s2page: s2page (shared hadt) = s2page (shared ladt);
id_core_data: core_data (shared hadt) = core_data (shared ladt);
id_vminfos: vminfos (shared hadt) = vminfos (shared ladt);
id_spts: spts (shared hadt) = spts (shared ladt);
id_smmu_vmid: smmu_vmid (shared hadt) = smmu_vmid (shared ladt);
rel_npts: forall i, relate_npt_tlb (curid hadt) i (i @ (npts (shared hadt))) (i @ (npts (shared ladt)))
}.
Inductive match_RData: stencil -> HDATA -> mem -> meminj -> Prop :=
| MATCH_RDATA: forall habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
constructor; inv H; trivial.
Qed.
Section FreshPrim.
Hint Unfold
acquire_lock_pt_spec
release_lock_pt_spec
get_npt_level_spec
walk_npt_spec
set_npt_spec
check_spec
check64_spec
get_level_s2pt_spec
get_level_s2pt_spec0
walk_s2pt_spec
walk_s2pt_spec0
map_s2pt_spec
map_s2pt_spec0
clear_pfn_host_spec
clear_pfn_host_spec0.
Lemma get_level_s2pt_spec_exists:
forall habd habd' labd vmid addr res f
(Hspec: get_level_s2pt_spec vmid addr habd = Some (habd', res))
(Hrel: relate_RData f habd labd),
exists labd', get_level_s2pt_spec0 vmid addr labd = Some (labd', res) /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
repeat simpl_hyp Hspec; contra.
- repeat srewrite; simpl. eexists. split. reflexivity. constructor; reflexivity.
- Local Transparent H_CalLock. simpl in *.
simpl_hyp C7. simpl_hyp C8. simpl_hyp C9. simpl_hyp C10.
destruct p4; destruct p4; destruct h; destruct o; contra.
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct (phys_page z0 =? 0).
+ simpl. inv Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl. repeat rewrite ZMap.set2. reflexivity.
+ srewrite. simpl. inv Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl. repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma get_level_s2pt_spec_ref:
compatsim (crel RData RData) (gensem get_level_s2pt_spec) get_level_s2pt_spec_low.
Proof.
Opaque get_level_s2pt_spec.
compatsim_simpl (@match_RData).
exploit get_level_s2pt_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent get_level_s2pt_spec.
Qed.
Lemma walk_s2pt_spec_exists:
forall habd habd' labd vmid addr res f
(Hspec: walk_s2pt_spec vmid addr habd = Some (habd', (VZ64 res)))
(Hrel: relate_RData f habd labd),
exists labd', walk_s2pt_spec0 vmid addr labd = Some (labd', (VZ64 res)) /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
repeat simpl_hyp Hspec; contra.
- repeat srewrite; simpl. eexists. split. reflexivity. constructor; reflexivity.
- Local Transparent H_CalLock. simpl in *.
simpl_hyp C7. simpl_hyp C8. simpl_hyp C9. simpl_hyp C10.
destruct p4; destruct p4; destruct h; destruct o; contra.
repeat (srewrite; try rewrite ZMap.gss; simpl).
inv Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl. repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma walk_s2pt_spec_ref:
compatsim (crel RData RData) (gensem walk_s2pt_spec) walk_s2pt_spec_low.
Proof.
Opaque walk_s2pt_spec.
compatsim_simpl (@match_RData).
exploit walk_s2pt_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent walk_s2pt_spec.
Qed.
Lemma map_s2pt_spec_exists:
forall habd habd' labd vmid addr level pte f
(Hspec: map_s2pt_spec vmid addr level pte habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', map_s2pt_spec0 vmid addr level pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
repeat autounfold in *.
repeat simpl_hyp Hspec; contra.
- inv Hspec. repeat srewrite; simpl. eexists.
split. reflexivity. constructor; reflexivity.
- Local Transparent H_CalLock. simpl in *.
simpl_hyp C10. simpl_hyp C11. simpl_hyp C12. simpl_hyp C13.
destruct p5; destruct p5; destruct h; destruct o; contra.
repeat (srewrite; try rewrite ZMap.gss; simpl). destruct b.
+ inv Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl.
repeat rewrite ZMap.set2. reflexivity.
+ inv Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl.
repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma map_s2pt_spec_ref:
compatsim (crel RData RData) (gensem map_s2pt_spec) map_s2pt_spec_low.
Proof.
Opaque map_s2pt_spec.
compatsim_simpl (@match_RData).
exploit map_s2pt_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent map_s2pt_spec.
Qed.
Lemma clear_pfn_host_spec_exists:
forall habd habd' labd pfn f
(Hspec: clear_pfn_host_spec pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', clear_pfn_host_spec0 pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
repeat autounfold in *.
repeat simpl_hyp Hspec; contra.
- inv Hspec. repeat srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; omega. rewrite Cond. simpl.
eexists. split. reflexivity. constructor; reflexivity.
- Local Transparent H_CalLock. simpl in *.
simpl_hyp C8. simpl_hyp C9. simpl_hyp C10. simpl_hyp C11.
destruct p6; destruct p6; destruct h; destruct o; contra.
assert(z * 4096 / 4096 = z) by (apply Z_div_mult_full; omega).
repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all; omega. rewrite Cond. simpl.
destruct (phys_page z0 =? 0).
+ simpl in *. inversion C6. rewrite <- H1 in *.
inversion Hspec. rewrite <- H2 in *. rewrite <- H3 in *.
eexists. split. reflexivity.
constructor. destruct labd, shared; simpl in *.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2. rewrite C1. reflexivity.
+ srewrite.
destruct (z2 =? 0).
* inversion C6. rewrite <- H1 in *.
inversion Hspec. rewrite <- H2 in *. rewrite <- H3 in *.
eexists. split. reflexivity.
constructor. destruct labd, shared; simpl in *.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2. rewrite C1. reflexivity.
* repeat (srewrite; try rewrite ZMap.gss; simpl). destruct b.
inversion Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl.
repeat rewrite ZMap.set2. reflexivity.
inversion Hspec. eexists. split. reflexivity.
constructor. destruct labd, shared; simpl.
repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma clear_pfn_host_spec_ref:
compatsim (crel RData RData) (gensem clear_pfn_host_spec) clear_pfn_host_spec_low.
Proof.
Opaque clear_pfn_host_spec.
compatsim_simpl (@match_RData).
exploit clear_pfn_host_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent clear_pfn_host_spec.
Qed.
Lemma mem_load_no_tlb_spec_exists:
forall habd habd' labd gfn reg f
(Hspec: mem_load_no_tlb_spec gfn reg habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', mem_load_ref_spec0 gfn reg labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. unfold mem_load_ref_spec2, mem_load_no_tlb_spec in *.
autounfold in *; repeat (simpl_hyp Hspec; contra).
duplicate Hrel. inv D. rewrite <- id_icore0, C0.
pose proof (rel_npts0 (cur_vmid labd)).
remember ((cur_vmid labd) @ (npts (shared habd))) as hnpt.
remember ((cur_vmid labd) @ (npts (shared labd))) as lnpt.
remember (curid habd) as cid.
destruct H.
destruct (tlb_look_up_h2 vmid (RData.curid labd) (VZ64 z) lnpt) eqn:look_up.
- destruct (z3 =? 0) eqn:tlb_entry.
+ srewrite. rewrite Hpt in C1. rewrite C1. srewrite. destruct_if.
(* level = 3*)
* bool_rel. srewrite.
destruct ((RData.curid habd) @ (z @ (tlbe (tlb vmid @ (npts (shared labd)))))) eqn: look_up_low.
destruct_if.
(* level = 3, no conflict *)
srewrite. inversion Hspec. eexists. split. reflexivity.
destruct Hrel. constructor; simpl; try reflexivity; try assumption.
intros. destruct_zmap.
pose proof (rel_npts1 vmid). destruct H. constructor; simpl; try assumption.
intros gfn pfn level. destruct_zmap. intros. inv H. rewrite C1. eexists. reflexivity.
apply Hrelate0. apply rel_npts1.
(* level = 3, conflict *)
unfold_spec look_up. rewrite look_up_low in look_up. rewrite Case0 in look_up.
inv look_up. inversion Case0.
* bool_rel. srewrite.
destruct_if.
(* level = 2 *)
destruct ((RData.curid habd) @ ((z / 512 * 512) @ (tlbe (tlb vmid @ (npts (shared labd))))))
eqn: look_up_low_2m.
destruct (z4 =? 0) eqn: tlb_entry_no.
(* level = 2, no conflict, z4 = 0 *)
bool_rel. srewrite. simpl. srewrite. inversion Hspec.
eexists. split. reflexivity.
destruct Hrel. constructor; simpl; try reflexivity; try assumption.
intros. destruct_zmap.
pose proof (rel_npts1 vmid). destruct H. constructor; simpl; try assumption.
intros gfn pfn level. destruct_zmap. intros. inv H.
pose proof (Hlevel2 _ _ _ C1).
exploit (H (z / 512 * 512)). omega. intros (? & ?).
rewrite H0. pose proof (Hnpt _ _ _ _ C1). pose proof (Hnpt _ _ _ _ H0).
destruct H2, H3. exploit Hpfn2. reflexivity.
exploit Hpfn4. reflexivity. intros. autounfold in *.
(* level = 2, *)
unfold_spec look_up. autounfold in look_up.
rewrite look_up_low_2m in look_up.
destruct (RData.curid habd) @ (z @ (tlbe (tlb vmid @ (npts (shared labd))))) eqn:Hxxx.
destruct (z6 =? 0) eqn:Hz6. destruct (z =? z / 512 * 512) eqn:Hzalign.
bool_rel. rewrite <- Hzalign in look_up_low_2m. rewrite Hxxx in look_up_low_2m.
inversion look_up_low_2m. omega. rewrite tlb_entry_no in look_up.
destruct (z5 =? 2) eqn:Hz5.
inversion look_up.
assert(z4 + (z - z / 512 * 512) > 0) by (bool_rel; omega). omega.
bool_rel; srewrite.
pose proof (Hlevel2 _ _ _ C1).
pose proof (Hrelate _ _ _ look_up_low_2m tlb_entry_no). destruct H0.
exploit (H (z / 512 * 512)). omega.
intros (? & ?). rewrite H0 in H1. inversion H1. omega.
inversion look_up. bool_rel; contra.
pose proof (Hnpt _ _ _ _ C1). destruct H. bool_rel. omega.
+ bool_rel. srewrite. rewrite Hpt in C1.
pose proof (Hnpt _ _ _ _ C1). destruct H.
destruct Hlevel. omega. destruct H.
unfold_spec look_up; repeat simpl_hyp look_up; inv look_up; contra.
bool_rel. pose proof (Hrelate _ _ _ C7 C8). destruct H. autounfold in *.
rewrite C9 in H.
assert(z1 = z6 + (z - z / 512 * 512)).
{ exploit Hpfn2. reflexivity. intros.
pose proof (Hlevel2 _ _ _ C1).
exploit (H1 (z / 512 * 512)). omega. intros (? & ?).
rewrite H in H2. inversion H2. srewrite.
pose proof (Hnpt _ _ _ _ H). destruct H3.
autounfold in Hpfn4. exploit Hpfn4. reflexivity.
autounfold; intros.
rewrite H6 in H3. rewrite H3.
repeat match goal with | [H: _ |- _] => clear H end. omega. }
rewrite <- H0. rewrite C5.
inversion Hspec. eexists. split. reflexivity. destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
bool_rel. pose proof (Hrelate _ _ _ C C2). destruct H.
rewrite C1 in H. inversion H. srewrite.
inversion Hspec. eexists. split. reflexivity. destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
unfold_spec look_up; repeat simpl_hyp look_up; inv look_up; contra.
bool_rel. pose proof (Hrelate _ _ _ C7 C8). destruct H. autounfold in *.
srewrite. pose proof (Hlevel2 _ _ _ H).
exploit (H0 z).
intros (? & ?). rewrite C1 in H1. inversion H1.
bool_rel. pose proof (Hrelate _ _ _ C C2). destruct H.
rewrite C1 in H. inversion H. srewrite.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
- unfold_spec look_up.
repeat simpl_hyp look_up; contra.
Qed.
Lemma mem_store_no_tlb_spec_exists:
forall habd habd' labd gfn reg f
(Hspec: mem_store_no_tlb_spec gfn reg habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', mem_store_ref_spec0 gfn reg labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. unfold mem_store_ref_spec2, mem_store_no_tlb_spec in *.
autounfold in *; repeat (simpl_hyp Hspec; contra).
duplicate Hrel. inv D. rewrite <- id_icore0, C0.
pose proof (rel_npts0 (cur_vmid labd)).
remember ((cur_vmid labd) @ (npts (shared habd))) as hnpt.
remember ((cur_vmid labd) @ (npts (shared labd))) as lnpt.
remember (curid habd) as cid.
destruct H.
destruct (tlb_look_up_h2 vmid (RData.curid labd) (VZ64 z) lnpt) eqn:look_up.
- destruct (z3 =? 0) eqn:tlb_entry.
+ srewrite. rewrite Hpt in C1. rewrite C1. srewrite.
destruct_if.
(* level = 3*)
* bool_rel. srewrite.
destruct ((RData.curid habd) @ (z @ (tlbe (tlb vmid @ (npts (shared labd)))))) eqn: look_up_low.
destruct_if.
(* level = 3, no conflict *)
srewrite.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
intros. destruct_zmap.
pose proof (rel_npts1 vmid).
destruct H.
constructor; simpl; try assumption.
intros gfn pfn level.
destruct_zmap. intros. inv H. rewrite C1. eexists. reflexivity.
apply Hrelate0.
apply rel_npts1.
(* level = 3, conflict *)
unfold_spec look_up.
rewrite look_up_low in look_up. rewrite Case0 in look_up.
inv look_up. inversion Case0.
* bool_rel. srewrite.
destruct_if.
(* level = 2 *)
destruct ((RData.curid habd) @ ((z / 512 * 512) @ (tlbe (tlb vmid @ (npts (shared labd))))))
eqn: look_up_low_2m.
destruct (z4 =? 0) eqn: tlb_entry_no.
(* level = 2, no conflict, z4 = 0 *)
bool_rel. srewrite.
simpl. srewrite.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
intros. destruct_zmap.
pose proof (rel_npts1 vmid).
destruct H.
constructor; simpl; try assumption.
intros gfn pfn level.
destruct_zmap. intros. inv H.
pose proof (Hlevel2 _ _ _ C1).
exploit (H (z / 512 * 512)). omega. intros (? & ?).
rewrite H0.
pose proof (Hnpt _ _ _ _ C1).
pose proof (Hnpt _ _ _ _ H0).
destruct H2, H3. exploit Hpfn2. reflexivity.
exploit Hpfn4. reflexivity. intros. autounfold in *.
apply Hrelate0.
apply rel_npts1.
(* level = 2, *)
unfold_spec look_up. autounfold in look_up.
rewrite look_up_low_2m in look_up.
destruct (RData.curid habd) @ (z @ (tlbe (tlb vmid @ (npts (shared labd))))) eqn:Hxxx.
destruct (z6 =? 0) eqn:Hz6. destruct (z =? z / 512 * 512) eqn:Hzalign.
bool_rel. rewrite <- Hzalign in look_up_low_2m. rewrite Hxxx in look_up_low_2m.
inversion look_up_low_2m. omega.
rewrite tlb_entry_no in look_up.
destruct (z5 =? 2) eqn:Hz5.
inversion look_up.
assert(z4 + (z - z / 512 * 512) > 0) by (bool_rel; omega). omega.
bool_rel; srewrite.
pose proof (Hlevel2 _ _ _ C1).
pose proof (Hrelate _ _ _ look_up_low_2m tlb_entry_no). destruct H0.
exploit (H (z / 512 * 512)). omega.
intros (? & ?). rewrite H0 in H1. inversion H1. omega.
inversion look_up. bool_rel; contra.
pose proof (Hnpt _ _ _ _ C1). destruct H. bool_rel. omega.
+ bool_rel. srewrite. rewrite Hpt in C1.
pose proof (Hnpt _ _ _ _ C1). destruct H.
destruct Hlevel. omega. destruct H.
unfold_spec look_up; repeat simpl_hyp look_up; inv look_up; contra.
bool_rel. pose proof (Hrelate _ _ _ C7 C8). destruct H. autounfold in *.
rewrite C9 in H.
assert(z1 = z6 + (z - z / 512 * 512)).
{ exploit Hpfn2. reflexivity. intros.
pose proof (Hlevel2 _ _ _ C1).
exploit (H1 (z / 512 * 512)). omega. intros (? & ?).
rewrite H in H2. inversion H2. srewrite.
pose proof (Hnpt _ _ _ _ H). destruct H3.
autounfold in Hpfn4. exploit Hpfn4. reflexivity.
autounfold; intros.
rewrite H6 in H3. rewrite H3.
repeat match goal with | [H: _ |- _] => clear H end. omega. }
rewrite <- H0. rewrite C5.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
bool_rel. pose proof (Hrelate _ _ _ C C2). destruct H.
rewrite C1 in H. inversion H. srewrite.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
unfold_spec look_up; repeat simpl_hyp look_up; inv look_up; contra.
bool_rel. pose proof (Hrelate _ _ _ C7 C8). destruct H. autounfold in *.
srewrite. pose proof (Hlevel2 _ _ _ H).
exploit (H0 z).
intros (? & ?). rewrite C1 in H1. inversion H1.
bool_rel. pose proof (Hrelate _ _ _ C C2). destruct H.
rewrite C1 in H. inversion H. srewrite.
inversion Hspec.
eexists. split. reflexivity.
destruct Hrel.
constructor; simpl; try reflexivity; try assumption.
- unfold_spec look_up.
repeat simpl_hyp look_up; contra.
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) NPTOps_passthrough NPTWalk.
Proof.
sim_oplus; layer_sim_simpl; compatsim_simpl (@match_AbData);
match_external_states_simpl; destruct match_related; srewrite; try reflexivity.
- unfold host_dabt_is_write_spec; srewrite; reflexivity.
- unfold host_get_fault_ipa_spec; srewrite; reflexivity.
- unfold set_vm_remap_addr_spec; srewrite; reflexivity.
- unfold host_dabt_get_rd_spec; srewrite; reflexivity.
- unfold clear_phys_page_spec; srewrite; reflexivity.
- unfold get_mem_region_cnt_spec; srewrite; reflexivity.
- unfold get_exception_vector_spec; srewrite; reflexivity.
- unfold read_hpfar_el2_spec; srewrite; reflexivity.
- unfold read_actlr_el1_spec; srewrite; reflexivity.
- unfold host_dabt_get_as_spec; srewrite; reflexivity.
- unfold read_esr_el2_spec; srewrite; reflexivity.
- unfold set_vm_kvm_spec; srewrite; reflexivity.
- unfold set_vm_mapped_pages_spec; srewrite; reflexivity.
- unfold readl_relaxed_spec; srewrite; reflexivity.
- unfold set_shadow_dirty_bit_spec; srewrite; reflexivity.
- unfold set_vm_load_size_spec; srewrite; reflexivity.
- unfold host_skip_instr_spec; srewrite; reflexivity.
- unfold set_vm_load_addr_spec; srewrite; reflexivity.
- unfold set_vm_vcpu_spec; srewrite; reflexivity.
- unfold readq_relaxed_spec; srewrite; reflexivity.
End.
End PassthroughPrim.
End WITHMEM.
End NPTOpsProofHigh.