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 RData.
Require Import MemAux.Layer.
Require Import Constants.
Require Import MemAux.Spec.
Require Import HypsecCommLib.
Require Import PageMgmt.Layer.
Require Import AbsMachine.Spec.
Require Import PageMgmt.Spec.
Require Import NPTOps.Spec.
Require Import NPTWalk.Spec.
Require Import MmioSPTWalk.Spec.
Require Import MmioSPTOps.Spec.
Require Import NPTWalk.ProofHighAux.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Local Opaque Z.eqb.
Local Transparent H_CalLock.
Section MemAuxProofHigh.
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 := MemAux_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := PageMgmt_ops) HDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Record cache_invs (adt: RData) :=
mkcache_invs {
Hcinv1: forall pfn val label,
pfn @ (cache (shared adt)) = (val, label) ->
(label = -1) \/ (label = (cur_vmid adt)) \/ (label = -2);
Hfminv1: forall pfn val label,
pfn @ (flatmem (shared adt)) = (val, label) ->
(label = -2) \/ (label = (cur_vmid adt));
Hptinv1: forall gfn vmid pfn level pte,
gfn @ (pt (vmid @ (npts (shared adt)))) = (pfn, level, pte) ->
pfn <> 0 ->
(s2_owner (pfn @ (s2page (shared adt))) = vmid) \/
(s2_count (pfn @ (s2page (shared adt))) > 0) \/
(s2_owner (pfn @ (s2page (shared adt))) = INVALID)
}.
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
(* id_rel: hadt = ladt *)
id_icore: icore hadt = icore ladt;
id_curid: curid hadt = curid ladt;
id_cur_vmid: cur_vmid hadt = cur_vmid ladt;
id_lock: lock hadt = lock ladt;
id_halt: halt hadt = halt ladt;
id_cache: cache (shared hadt) = cache (shared ladt);
id_flatmem: flatmem (shared hadt) = flatmem (shared ladt);
id_s2page: s2page (shared hadt) = s2page (shared ladt);
relate_invs: cache_invs ladt;
id_npts: npts (shared hadt) = 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.
Local Hint Unfold
phys_page
acquire_lock_s2page_spec
assign_pfn_to_smmu_spec
assign_pfn_to_smmu_spec0
assign_pfn_to_vm_spec
assign_pfn_to_vm_spec0
clear_pfn_host_spec
clear_phys_page_spec
clear_vm_page_spec
clear_vm_page_spec0
fetch_from_doracle_spec
get_pfn_count_spec
get_pfn_map_spec
get_pfn_owner_spec
grant_vm_page_spec
grant_vm_page_spec0
map_page_host_spec
map_page_host_spec0
map_pfn_vm_spec
map_pfn_vm_spec0
map_s2pt_spec
map_spt_spec
map_vm_io_spec
map_vm_io_spec0
panic_spec
release_lock_s2page_spec
revoke_vm_page_spec
revoke_vm_page_spec0
set_pfn_count_spec
set_pfn_map_spec
set_pfn_owner_spec
unmap_smmu_page_spec
unmap_smmu_page_spec0
unmap_spt_spec
update_smmu_page_spec
update_smmu_page_spec0.
Lemma addr_range_gfn:
forall n, n < 281474976710656 -> n / 4096 < 68719476736.
Proof.
intros. assert(n <= 281474976710655) by omega.
assert(n / 4096 <= 281474976710655 / 4096) by( apply Z_div_le; omega).
assert(n / 4096 <= 68719476735) by apply H1; omega.
Qed.
Lemma map_page_host_spec_exists:
forall habd habd' labd addr f
(Hspec: map_page_host_spec addr habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', map_page_host_spec0 addr labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
assert(NE52: 5 <> 2) by omega. assert(NE25: 2 <> 5) by omega.
repeat simpl_hyp Hspec; contra.
- extract_if. apply andb_true_iff; split; bool_rel_all; somega.
apply addr_range_gfn; assumption. rewrite Cond.
inv Hspec. repeat srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega. rewrite Cond0.
srewrite. eexists; split. reflexivity. constructor; reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn; assumption. rewrite Cond.
srewrite. destruct_if.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond0.
rewrite Z.add_0_r. rewrite (ZMap.gso _ _ NE52). srewrite.
assert(NZ: Z.lor (z / 4096 * 4096) (Z.lor 18014398509483847 192) =? 0 = false).
bool_rel. red; intro T. apply Z.lor_eq_0_iff in T.
destruct T as [T1 T2]. inversion T2. rewrite NZ. rewrite (ZMap.gso _ _ NE52).
repeat (srewrite; simpl; try rewrite ZMap.gss). destruct b.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; reflexivity.
repeat rewrite (ZMap.gso _ _ NE25). repeat rewrite ZMap.gss. simpl; srewrite.
repeat (rewrite id_cpu; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl. repeat (rewrite (zmap_comm _ _ NE52); rewrite ZMap.set2).
reflexivity. simpl in C16; srewrite.
extract_if. apply andb_true_iff; split; bool_rel_all; somega. rewrite Cond0.
rewrite Z.add_0_r. rewrite (ZMap.gso _ _ NE52). srewrite.
assert(NZ: Z.lor (z / 4096 * 4096) 4095 =? 0 = false).
bool_rel. red; intro T. apply Z.lor_eq_0_iff in T.
destruct T as [T1 T2]. inversion T2. rewrite NZ. rewrite (ZMap.gso _ _ NE52).
repeat (srewrite; simpl; try rewrite ZMap.gss). destruct b.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; reflexivity.
repeat rewrite (ZMap.gso _ _ NE25). repeat rewrite ZMap.gss. simpl; srewrite.
repeat (rewrite id_cpu; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl. repeat (rewrite (zmap_comm _ _ NE52); rewrite ZMap.set2).
reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn; assumption. rewrite Cond.
srewrite. destruct_if. simpl in C16; contra. destruct_if. simpl in C16; contra.
inv Hspec. eexists; split. reflexivity. constructor. reflexivity.
Local Opaque Z.eqb.
Qed.
Lemma map_page_host_spec_ref:
compatsim (crel RData RData) (gensem map_page_host_spec) map_page_host_spec_low.
Proof.
Opaque map_page_host_spec.
compatsim_simpl (@match_RData).
exploit map_page_host_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent map_page_host_spec.
Qed.
Lemma clear_vm_page_spec_exists:
forall habd habd' labd vmid pfn f
(Hspec: clear_vm_page_spec vmid pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', clear_vm_page_spec0 vmid pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
assert(NE02: 0 <> 2) by omega. assert(NE20: 2 <> 0) by omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
srewrite. simpl. destruct vmid; (eexists; split; [reflexivity|constructor; reflexivity]).
- assert(NE0m: 0 =? 4294967295 = false) by (bool_rel; omega).
simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. destruct_if. bool_rel_all; omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
rewrite (ZMap.gso _ _ NE20). rewrite ZMap.gss. simpl.
rewrite C4. repeat (rewrite id_cpu; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl.
repeat (rewrite (zmap_comm _ _ NE02); rewrite ZMap.set2).
repeat rewrite (ZMap.gso _ _ NE02). repeat rewrite ZMap.set2.
match goal with
| [ |- context [?p {s2_owner : 0} {s2_count : 0} {s2_gfn : z + 1000000000}]] =>
replace (p {s2_owner : 0} {s2_count : 0} {s2_gfn : z + 1000000000}) with
(mkS2Page 0 0 (z + 1000000000)) by reflexivity
end.
reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. inv Hspec. eexists; split. reflexivity. constructor.
repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma clear_vm_page_spec_ref:
compatsim (crel RData RData) (gensem clear_vm_page_spec) clear_vm_page_spec_low.
Proof.
Opaque clear_vm_page_spec.
compatsim_simpl (@match_RData).
exploit clear_vm_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent clear_vm_page_spec.
Qed.
Lemma assign_pfn_to_vm_spec_exists:
forall habd habd' labd vmid gfn pfn f
(Hspec: assign_pfn_to_vm_spec vmid gfn pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', assign_pfn_to_vm_spec0 vmid gfn pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
assert(NE02: 0 <> 2) by omega. assert(NE20: 2 <> 0) by omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
srewrite. simpl. simpl_bool_eq. destruct vmid; (eexists; split; [reflexivity|constructor; reflexivity]).
- simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. destruct_if. bool_rel_all; omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct_if. bool_rel_all; omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
rewrite Z.add_0_r. assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq).
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct b. repeat (srewrite; try rewrite ZMap.gss; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl in *; repeat rewrite ZMap.set2.
match goal with
| [ |- context [?p {s2_owner : vmid} {s2_gfn : z}]] =>
replace (p {s2_owner : vmid} {s2_gfn : z}) with
(mkS2Page vmid 0 z)
end.
reflexivity. bool_rel.
destruct ((z0 @ (CalS2Page s2page (2 @ oracle curid 2 @ log)))).
simpl in *. srewrite; reflexivity.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond0.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq0). rewrite ZMap.gss.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq1).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq2). rewrite ZMap.gss.
simpl; repeat (srewrite; try rewrite ZMap.gss; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl in *; repeat rewrite ZMap.set2.
repeat (rewrite (zmap_comm _ _ Hneq); rewrite ZMap.set2).
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq3).
repeat rewrite (ZMap.gso _ _ NE02).
match goal with
| [ |- context [?p {s2_owner : vmid} {s2_gfn : z}]] =>
replace (p {s2_owner : vmid} {s2_gfn : z}) with
(mkS2Page vmid 0 z)
end.
repeat (rewrite (zmap_comm _ _ NE02); rewrite (zmap_comm _ _ Hneq); rewrite ZMap.set2).
reflexivity. bool_rel.
destruct ((z0 @ (CalS2Page s2page (2 @ oracle curid 2 @ log)))).
simpl in *. srewrite; reflexivity.
- Local Transparent H_CalLock. simpl in *.
repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
- simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. destruct_if. destruct_if. destruct_if. bool_rel_all; omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl in *; repeat rewrite ZMap.set2.
reflexivity. inversion C21. inversion C21.
- simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. reflexivity. rewrite Cond.
srewrite. destruct_if. destruct_if.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl in *; repeat rewrite ZMap.set2.
reflexivity. inversion C21. inversion C21.
- simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega; reflexivity. rewrite Cond.
srewrite. destruct_if. destruct_if. inversion C21.
inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
Qed.
Lemma assign_pfn_to_vm_spec_ref:
compatsim (crel RData RData) (gensem assign_pfn_to_vm_spec) assign_pfn_to_vm_spec_low.
Proof.
Opaque assign_pfn_to_vm_spec.
compatsim_simpl (@match_RData).
exploit assign_pfn_to_vm_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent assign_pfn_to_vm_spec.
Qed.
Lemma map_pfn_vm_spec_exists:
forall habd habd' labd vmid addr pte level f
(Hspec: map_pfn_vm_spec vmid addr pte level habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', map_pfn_vm_spec0 vmid addr pte level labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. destruct_if.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
- simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct (level =? 2); srewrite.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
extract_if. bool_rel; red; intro T. apply Z.bits_inj_iff' with (n:=0) in T.
autorewrite with bitwise in T. simpl in T. rewrite orb_comm in T. inversion T. omega.
rewrite Cond0. inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
extract_if. bool_rel; red; intro T. apply Z.bits_inj_iff' with (n:=0) in T.
autorewrite with bitwise in T. simpl in T. rewrite orb_comm in T. inversion T. omega.
rewrite Cond0. inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
Local Opaque Z.eqb.
Qed.
Lemma map_pfn_vm_spec_ref:
compatsim (crel RData RData) (gensem map_pfn_vm_spec) map_pfn_vm_spec_low.
Proof.
Opaque map_pfn_vm_spec.
compatsim_simpl (@match_RData).
exploit map_pfn_vm_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent map_pfn_vm_spec.
Qed.
Lemma grant_vm_page_spec_exists:
forall habd habd' labd vmid pfn f
(Hspec: grant_vm_page_spec vmid pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', grant_vm_page_spec0 vmid pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite. extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond0. srewrite; simpl.
destruct vmid; simpl; eexists; (split; [reflexivity|constructor; reflexivity]).
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond0.
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. destruct_if. bool_rel_all0; omega.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
Qed.
Lemma grant_vm_page_spec_ref:
compatsim (crel RData RData) (gensem grant_vm_page_spec) grant_vm_page_spec_low.
Proof.
Opaque grant_vm_page_spec.
compatsim_simpl (@match_RData).
exploit grant_vm_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent grant_vm_page_spec.
Qed.
Lemma revoke_vm_page_spec_exists:
forall habd habd' labd vmid pfn f
(Hspec: revoke_vm_page_spec vmid pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', revoke_vm_page_spec0 vmid pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond0. srewrite; simpl.
destruct vmid; simpl; eexists; (split; [reflexivity|constructor; reflexivity]).
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond0.
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. bool_rel_all0; omega. srewrite.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq).
rewrite Z.add_0_r. repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq0).
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct b. repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
assert(T: 2<>5) by omega. repeat (rewrite (zmap_comm _ _ T); rewrite ZMap.set2). reflexivity.
extract_if. apply andb_true_iff; split; bool_rel_all; omega. rewrite Cond1.
repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq1). repeat rewrite ZMap.gss.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq2). rewrite (ZMap.gso _ _ Hneq1).
rewrite ZMap.gss. repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq3).
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq4).
repeat rewrite (zmap_comm _ _ Hneq4); repeat rewrite (zmap_comm _ _ Hneq0).
repeat rewrite ZMap.set2. reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond0.
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. bool_rel_all0; omega.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond0.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
Qed.
Lemma revoke_vm_page_spec_ref:
compatsim (crel RData RData) (gensem revoke_vm_page_spec) revoke_vm_page_spec_low.
Proof.
Opaque revoke_vm_page_spec.
compatsim_simpl (@match_RData).
exploit revoke_vm_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent revoke_vm_page_spec.
Qed.
Lemma map_vm_io_spec_exists:
forall habd habd' labd vmid gpa pa f
(Hspec: map_vm_io_spec vmid gpa pa habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', map_vm_io_spec0 vmid gpa pa labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite. extract_if. apply andb_true_iff; split; bool_rel_all; somega.
apply addr_range_gfn; assumption. rewrite Cond.
simpl. eexists; split. reflexivity. constructor; reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn; assumption. rewrite Cond.
srewrite. extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond0.
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq); srewrite.
extract_if. bool_rel; red; intro T. apply Z.lor_eq_0_iff in T.
destruct T as [T1 T2]. inversion T2. rewrite Cond1.
assert_gso. bool_rel_all0; omega. repeat rewrite (ZMap.gso _ _ Hneq0).
repeat (srewrite; simpl; try rewrite ZMap.gss). destruct b.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; reflexivity.
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
repeat (srewrite; simpl; try rewrite ZMap.gss).
rewrite (ZMap.gso _ _ Hneq1). rewrite ZMap.gss.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; simpl in *. repeat (rewrite (zmap_comm _ _ Hneq0); rewrite ZMap.set2).
reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn; assumption. rewrite Cond.
srewrite. inv Hspec. eexists; split. reflexivity.
repeat rewrite ZMap.set2. constructor; reflexivity.
Local Opaque Z.eqb.
Qed.
Lemma map_vm_io_spec_ref:
compatsim (crel RData RData) (gensem map_vm_io_spec) map_vm_io_spec_low.
Proof.
Opaque map_vm_io_spec.
compatsim_simpl (@match_RData).
exploit map_vm_io_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent map_vm_io_spec.
Qed.
Lemma assign_pfn_to_smmu_spec_exists:
forall habd habd' labd vmid gfn pfn f
(Hspec: assign_pfn_to_smmu_spec vmid gfn pfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', assign_pfn_to_smmu_spec0 vmid gfn pfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond. simpl. srewrite.
simpl; eexists; (split; [reflexivity|constructor; reflexivity]).
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
rewrite Z.add_0_r; assert_gso. omega. rewrite (ZMap.gso _ _ Hneq).
srewrite; simpl. repeat rewrite (ZMap.gso _ _ Hneq).
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct b. repeat (simpl halt; srewrite). simpl.
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
extract_if. apply andb_true_iff; split; bool_rel_all; somega. rewrite Cond0.
repeat (simpl halt; srewrite). simpl.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq0). rewrite ZMap.gss.
destruct_if. bool_rel_all0; omega.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. bool_rel_all0; omega.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq1). rewrite (ZMap.gso _ _ Hneq0).
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq2).
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq3).
repeat rewrite (zmap_comm _ _ Hneq3); repeat rewrite (zmap_comm _ _ Hneq).
repeat rewrite ZMap.set2. reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor; reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
- simpl in *. repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
Qed.
Lemma assign_pfn_to_smmu_spec_ref:
compatsim (crel RData RData) (gensem assign_pfn_to_smmu_spec) assign_pfn_to_smmu_spec_low.
Proof.
Opaque assign_pfn_to_smmu_spec.
compatsim_simpl (@match_RData).
exploit assign_pfn_to_smmu_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent assign_pfn_to_smmu_spec.
Qed.
Lemma update_smmu_page_spec_exists:
forall habd habd' labd vmid cbndx index iova pte f
(Hspec: update_smmu_page_spec vmid cbndx index iova pte habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', update_smmu_page_spec0 vmid cbndx index iova pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
apply addr_range_gfn. pose proof (phys_page_upper_bound z0).
autounfold in H. omega. rewrite Cond0. simpl.
simpl_bool_eq; srewrite.
destruct_if; eexists; (split; [reflexivity|constructor; try reflexivity]).
destruct habd'; simpl in *; srewrite; reflexivity.
- simpl in *. extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn. pose proof (phys_page_upper_bound z0).
autounfold in H. omega. rewrite Cond0. simpl.
repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). srewrite.
rewrite (ZMap.gso _ _ Hneq). repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if; (inv Hspec; eexists; split; [reflexivity|constructor;reflexivity]).
- simpl in *.
extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn. pose proof (phys_page_upper_bound z0).
autounfold in H. omega. rewrite Cond0. simpl.
repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). srewrite.
rewrite (ZMap.gso _ _ Hneq). repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq0).
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. destruct_if. simpl in *.
destruct_if. bool_rel; omega.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
- simpl in *.
extract_if. apply andb_true_iff; split; bool_rel_all0; somega; reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. pose proof (phys_page_upper_bound z0). autounfold in H.
apply andb_true_iff; split; bool_rel_all0; somega; apply addr_range_gfn; omega.
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *. reflexivity.
Qed.
Lemma update_smmu_page_spec_ref:
compatsim (crel RData RData) (gensem update_smmu_page_spec) update_smmu_page_spec_low.
Proof.
Opaque update_smmu_page_spec.
compatsim_simpl (@match_RData).
exploit update_smmu_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent update_smmu_page_spec.
Qed.
Lemma unmap_smmu_page_spec_exists:
forall habd habd' labd cbndx index iova f
(Hspec: unmap_smmu_page_spec cbndx index iova habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', unmap_smmu_page_spec0 cbndx index iova labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat simpl_hyp Hspec; contra.
- inv Hspec. srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega.
reflexivity. rewrite Cond.
Local Transparent Z.land Z.div Z.eqb. simpl.
eexists; (split; [reflexivity|constructor; try reflexivity]).
- simpl in *.
extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. repeat (rewrite (ZMap.gso _ _ Hneq); srewrite).
repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec; eexists; split; [reflexivity|constructor;reflexivity].
- simpl. extract_if. apply andb_true_iff; split; bool_rel_all; somega. reflexivity. rewrite Cond.
repeat (srewrite; simpl; try rewrite ZMap.gss).
assert_gso. omega. repeat (rewrite (ZMap.gso _ _ Hneq); srewrite).
repeat (srewrite; simpl; try rewrite ZMap.gss).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega.
apply addr_range_gfn. pose proof (phys_page_upper_bound z1).
autounfold in H. omega. rewrite Cond0. simpl.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq0).
repeat (srewrite; simpl; try rewrite ZMap.gss).
destruct_if. destruct_if. simpl in *.
destruct_if. bool_rel; omega.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
rewrite (ZMap.gso _ _ Hneq0). repeat (srewrite; simpl; try rewrite ZMap.gss).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; simpl in *.
repeat rewrite (zmap_comm _ _ Hneq); repeat rewrite ZMap.set2. reflexivity.
Qed.
Lemma unmap_smmu_page_spec_ref:
compatsim (crel RData RData) (gensem unmap_smmu_page_spec) unmap_smmu_page_spec_low.
Proof.
Opaque unmap_smmu_page_spec.
compatsim_simpl (@match_RData).
exploit unmap_smmu_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent unmap_smmu_page_spec.
Qed.
Lemma mem_load_no_check_spec_exists:
forall habd habd' labd gfn bypass f
(Hspec: mem_load_no_check_spec gfn bypass habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', mem_load_check_spec gfn bypass labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. unfold mem_load_no_check_spec, mem_load_check_spec in *.
autounfold in *; repeat (simpl_hyp Hspec; contra).
duplicate Hrel. inv D. rewrite <- id_icore0, C0.
rewrite id_cur_vmid0 in C1.
rewrite id_npts0 in C1. rewrite C1.
destruct (z1 =? 0) eqn: pt_entry.
- inv C3.
- simpl. autounfold. srewrite. bool_rel.
srewrite. inv C3.
destruct_if.
+ eexists. split. bool_rel.
destruct_if.
* reflexivity.
* destruct relate_invs0.
simpl; try reflexivity; try assumption.
pose proof (Hfminv2 _ _ _ C7). bool_rel_all. omega.
* destruct Hrel. inv Hspec.
constructor; simpl; try reflexivity; try assumption.
destruct relate_invs0.
constructor; simpl; try reflexivity; try assumption.
intros.
destruct (pfn =? z1) eqn: Heq.
bool_rel.
rewrite Heq in H. rewrite ZMap.gss in H.
inv H. pose proof (Hfminv2 _ _ _ C7). omega.
bool_rel.
rewrite ZMap.gso in H.
eapply Hcinv2. eassumption. assumption.
+ eexists. split. bool_rel. destruct_if.
* reflexivity.
* inv Case0. omega.
* destruct Hrel. inv Case.
- autounfold in *; repeat (simpl_hyp Hspec; contra).
duplicate Hrel. inv D. rewrite id_icore0 in C0. rewrite C0.
rewrite id_cur_vmid0 in C1. rewrite id_npts0 in C1. rewrite C1.
bool_rel.
destruct_if.
+ bool_rel. contra.
+ simpl. autounfold. srewrite. bool_rel.
srewrite. simpl.
destruct_if.
* bool_rel. contra.
* eexists. split. destruct_if.
reflexivity.
destruct relate_invs0.
pose proof (Hcinv2 _ _ _ C5).
bool_rel_all. omega.
destruct Hrel. inv Hspec.
constructor; simpl; try reflexivity; try assumption.
- autounfold in *; repeat (simpl_hyp Hspec; contra).
duplicate Hrel. inv D. rewrite id_icore0 in C0. rewrite C0.
rewrite id_cur_vmid0 in C1. rewrite id_npts0 in C1. rewrite C1.
bool_rel.
destruct_if.
+ bool_rel. contra.
+ simpl. autounfold. srewrite. bool_rel.
srewrite.
destruct_if.
* eexists. split. auto.
destruct Hrel. inv Hspec.
constructor; simpl; try reflexivity; try assumption.
* destruct relate_invs0.
simpl. srewrite.
pose proof (Hfminv2 _ _ _ C5).
bool_rel_all.
omega.
Qed.
Lemma mem_store_no_check_spec_exists:
forall habd habd' labd gfn val bypass f
(Hspec: mem_store_no_check_spec gfn val bypass habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', mem_store_check_spec gfn val bypass labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. unfold mem_store_no_check_spec, mem_store_check_spec in *.
autounfold in *; repeat (simpl_hyp Hspec; contra).
inv Hrel. rewrite <- id_icore0, C0.
rewrite id_cur_vmid0 in C1.
rewrite id_npts0 in C1. rewrite C1.
destruct (z1 =? 0) eqn: pt_entry.
- inv C3.
- simpl. autounfold. srewrite. bool_rel.
srewrite. inv C3.
destruct_if.
* eexists. split. reflexivity.
inversion Hspec.
constructor; simpl; try reflexivity; try assumption.
rewrite C0. rewrite id_icore0. auto.
srewrite.
constructor; simpl; try reflexivity; try assumption.
destruct relate_invs0.
pose proof (Hcinv2 _ _ _ C5).
intros.
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. rewrite Hpfn in H1.
rewrite ZMap.gss in H1. inv H1. auto.
destruct ((s2_owner z1 @ (s2page (shared labd)) =? INVALID) ||
(s2_count z1 @ (s2page (shared labd)) >? 0)) eqn: Hs2page.
autounfold in *.
rewrite Hs2page. auto.
autounfold in *.
rewrite Hs2page. auto.
bool_rel. rewrite ZMap.gso in H1.
eapply Hcinv2. eassumption. assumption.
intros. destruct relate_invs0.
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. rewrite Hpfn in H.
rewrite ZMap.gss in H. inv H. auto.
destruct ((s2_owner z1 @ (s2page (shared labd)) =? INVALID) ||
(s2_count z1 @ (s2page (shared labd)) >? 0)) eqn: Hs2page.
autounfold in *.
rewrite Hs2page. auto.
autounfold in *.
rewrite Hs2page. auto.
bool_rel. rewrite ZMap.gso in H.
eapply Hfminv2. eassumption. assumption.
intros.
destruct relate_invs0.
pose proof (Hptinv2 gfn vmid _ _ _ H).
srewrite.
apply H2. assumption.
* bool_rel. contra.
- autounfold in *; repeat (simpl_hyp Hspec; contra).
inv Hrel. rewrite id_icore0 in C0. rewrite C0.
rewrite id_cur_vmid0 in C1. rewrite id_npts0 in C1. rewrite C1.
bool_rel.
destruct_if.
* bool_rel. contra.
* simpl. autounfold. srewrite. bool_rel.
srewrite. simpl.
destruct_if.
bool_rel. contra.
eexists. split.
srewrite. bool_rel. simpl.
destruct_if.
reflexivity.
destruct relate_invs0.
pose proof (Hcinv2 _ _ _ C5). bool_rel_all. omega.
(*omega.*)
bool_rel.
rewrite C4.
inversion Hspec.
constructor; simpl; try reflexivity; try assumption.
rewrite C0. rewrite id_icore0. auto.
srewrite.
constructor; simpl; try reflexivity; try assumption.
destruct relate_invs0.
pose proof (Hcinv2 _ _ _ C5).
intros.
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. rewrite Hpfn in H1.
rewrite ZMap.gss in H1. inv H1. auto.
destruct ((s2_owner z1 @ (s2page (shared labd)) =? INVALID) ||
(s2_count z1 @ (s2page (shared labd)) >? 0)) eqn: Hs2page.
autounfold in *.
rewrite Hs2page. auto.
autounfold in *.
rewrite Hs2page. auto.
bool_rel. rewrite ZMap.gso in H1.
eapply Hcinv2. eassumption. assumption.
intros. destruct relate_invs0.
pose proof (Hfminv2 pfn val0 label).
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. apply H1. assumption.
bool_rel. apply H1. assumption.
intros.
destruct relate_invs0.
pose proof (Hptinv2 gfn vmid _ _ _ H).
srewrite.
apply H2. assumption.
- autounfold in *; repeat (simpl_hyp Hspec; contra).
inv Hrel. rewrite id_icore0 in C0. rewrite C0.
rewrite id_cur_vmid0 in C1. rewrite id_npts0 in C1. rewrite C1.
bool_rel.
destruct_if.
* bool_rel. contra.
* simpl. autounfold. srewrite. bool_rel.
srewrite.
destruct_if.
+ destruct_if.
eexists. split. reflexivity.
inversion Hspec.
constructor; simpl; try reflexivity; try assumption.
rewrite C0. rewrite id_icore0. auto.
srewrite.
constructor; simpl; try reflexivity; try assumption.
destruct relate_invs0.
intros.
pose proof (Hcinv2 pfn val0 label).
apply H1. assumption.
destruct relate_invs0.
pose proof (Hfminv2 _ _ _ C5).
intros.
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. rewrite Hpfn in H1.
rewrite ZMap.gss in H1. inv H1. auto.
bool_rel.
rewrite ZMap.gso in H1.
eapply Hfminv2; eassumption.
assumption.
intros.
destruct relate_invs0.
pose proof (Hptinv2 gfn vmid _ _ _ H).
srewrite. apply H2. assumption.
eexists. split. reflexivity.
inversion Hspec.
constructor; simpl; try reflexivity; try assumption.
rewrite C0. rewrite id_icore0. auto.
srewrite.
constructor; simpl; try reflexivity; try assumption.
destruct relate_invs0.
intros.
pose proof (Hcinv2 pfn val0 label).
apply H1. assumption.
destruct relate_invs0.
pose proof (Hfminv2 _ _ _ C5).
intros.
destruct (pfn =? z1) eqn: Hpfn.
bool_rel. rewrite Hpfn in H1.
rewrite ZMap.gss in H1. inv H1. auto.
bool_rel.
rewrite ZMap.gso in H1.
eapply Hfminv2; eassumption.
assumption.
intros.
destruct relate_invs0.
pose proof (Hptinv2 gfn vmid _ _ _ H).
srewrite. apply H2. assumption.
+ destruct relate_invs0.
pose proof (Hfminv2 _ _ _ C5).
bool_rel_all. omega.
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) MemAux_passthrough PageMgmt.
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_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.
Qed.
End PassthroughPrim.
End WITHMEM.
End MemAuxProofHigh.