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 SmmuAux.Layer.
Require Import Constants.
Require Import HypsecCommLib.
Require Import SmmuOps.Layer.
Require Import SmmuOps.Spec.
Require Import AbsMachine.Spec.
Require Import SmmuAux.Spec.
Require Import BootOps.Spec.
Require Import MmioSPTOps.Spec.
Require Import VMPower.Spec.
Require Import NPTWalk.Spec.
Require Import MmioSPTWalk.Spec.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Local Transparent H_CalLock.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Section SmmuOpsProofHigh.
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 := SmmuOps_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := SmmuAux_ops) HDATA).
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
}.
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
emulate_mmio_spec
init_spt_spec
smmu_assign_page_spec
check64_spec
assign_smmu_spec
el2_free_smmu_pgd_spec
smmu_map_page_spec
el2_arm_lpae_clear_spec
get_vm_poweron_spec
el2_alloc_smmu_pgd_spec0
smmu_map_page_spec0
get_smmu_cfg_vmid_spec
clear_smmu_spec
handle_host_mmio_spec
el2_arm_lpae_clear_spec0
el2_arm_lpae_iova_to_phys_spec0
release_lock_smmu_spec
is_smmu_range_spec
smmu_assign_page_spec0
get_smmu_num_context_banks_spec
walk_spt_spec
el2_free_smmu_pgd_spec0
acquire_lock_smmu_spec
check_spec
map_smmu_spec
el2_arm_lpae_iova_to_phys_spec
el2_alloc_smmu_pgd_spec
emulate_mmio_spec0
panic_spec
set_smmu_cfg_vmid_spec.
Lemma emulate_mmio_spec_exists:
forall habd habd' labd addr hsr res f
(Hspec: emulate_mmio_spec addr hsr habd = Some (habd', res))
(Hrel: relate_RData f habd labd),
exists labd', emulate_mmio_spec0 addr hsr labd = Some (labd', res) /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; srewrite; simpl in *.
destruct_if. eexists; split. reflexivity. constructor; destruct habd'; simpl in *; srewrite; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
eexists; split. reflexivity. constructor; destruct habd'; simpl in *; srewrite; reflexivity.
bool_rel; srewrite. simpl.
eexists; split. reflexivity. constructor; destruct labd; simpl in *; srewrite; reflexivity.
extract_if. repeat simpl_hyp C12; contra; inv C12; reflexivity. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. repeat simpl_hyp C12; contra; inv C12; reflexivity. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. repeat simpl_hyp C12; contra; inv C12; reflexivity. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond0.
srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond1.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond0.
srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond1.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond0.
srewrite; simpl.
extract_if. apply andb_true_iff; split; bool_rel_all; somega; reflexivity. rewrite Cond1.
eexists; split. reflexivity. constructor; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
eexists; split. reflexivity. constructor; destruct labd; simpl in *; srewrite; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
eexists; split. reflexivity. constructor; destruct habd'; simpl in *; srewrite; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
eexists; split. reflexivity. constructor; destruct habd'; simpl in *; srewrite; reflexivity.
extract_if. bool_rel; omega. rewrite Cond. simpl.
eexists; split. reflexivity. constructor; destruct labd; simpl in *; srewrite; reflexivity.
Qed.
Lemma emulate_mmio_spec_ref:
compatsim (crel RData RData) (gensem emulate_mmio_spec) emulate_mmio_spec_low.
Proof.
Opaque emulate_mmio_spec.
compatsim_simpl (@match_RData).
exploit emulate_mmio_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent emulate_mmio_spec.
Qed.
Lemma el2_free_smmu_pgd_spec_exists:
forall habd habd' labd cbndx index f
(Hspec: el2_free_smmu_pgd_spec cbndx index habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', el2_free_smmu_pgd_spec cbndx index labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; repeat srewrite; simpl in *.
inv Hspec; eexists; split. reflexivity. constructor.
destruct habd'; destruct shared; simpl in *; srewrite; reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega; reflexivity. rewrite Cond.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite ZMap.set2; simpl).
repeat rewrite (zmap_comm _ _ Hneq0); repeat rewrite ZMap.set2.
reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite ZMap.set2; simpl).
reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; repeat (srewrite; try rewrite ZMap.gss; try rewrite ZMap.set2; simpl).
reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; repeat (srewrite; try rewrite ZMap.gss; try rewrite ZMap.set2; simpl).
reflexivity.
Qed.
Lemma el2_free_smmu_pgd_spec_ref:
compatsim (crel RData RData) (gensem el2_free_smmu_pgd_spec) el2_free_smmu_pgd_spec_low.
Proof.
Opaque el2_free_smmu_pgd_spec.
compatsim_simpl (@match_RData).
exploit el2_free_smmu_pgd_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent el2_free_smmu_pgd_spec.
Qed.
Lemma el2_alloc_smmu_pgd_spec_exists:
forall habd habd' labd cbndx vmid index f
(Hspec: el2_alloc_smmu_pgd_spec cbndx vmid index habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', el2_alloc_smmu_pgd_spec cbndx vmid index labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; repeat srewrite; simpl in *.
srewrite; eexists; (split; [reflexivity|constructor; destruct habd'; simpl in *; srewrite; reflexivity]).
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq2).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
repeat (try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1); simpl).
repeat (try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *; reflexivity.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Qed.
Lemma el2_alloc_smmu_pgd_spec_ref:
compatsim (crel RData RData) (gensem el2_alloc_smmu_pgd_spec) el2_alloc_smmu_pgd_spec_low.
Proof.
Opaque el2_alloc_smmu_pgd_spec.
compatsim_simpl (@match_RData).
exploit el2_alloc_smmu_pgd_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent el2_alloc_smmu_pgd_spec.
Qed.
Lemma smmu_assign_page_spec_exists:
forall habd habd' labd cbndx index pfn gfn f
(Hspec: smmu_assign_page_spec cbndx index pfn gfn habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', smmu_assign_page_spec cbndx index pfn gfn labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; repeat srewrite; simpl in *.
destruct_if; srewrite; eexists; (split; [reflexivity|constructor; destruct habd'; simpl in *; srewrite; reflexivity]).
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite ZMap.set2; simpl).
repeat rewrite (zmap_comm _ _ Hneq0); repeat rewrite ZMap.set2.
reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq2).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq3).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); try rewrite (ZMap.gso _ _ Hneq3); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); try rewrite (ZMap.gso _ _ Hneq3); simpl).
assert_gso. omega. repeat rewrite (ZMap.gso _ _ Hneq4).
repeat (try rewrite (zmap_comm _ _ Hneq4); try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1); simpl).
repeat (try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat rewrite ZMap.set2; reflexivity.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Qed.
Lemma smmu_assign_page_spec_ref:
compatsim (crel RData RData) (gensem smmu_assign_page_spec) smmu_assign_page_spec_low.
Proof.
Opaque smmu_assign_page_spec.
compatsim_simpl (@match_RData).
exploit smmu_assign_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent smmu_assign_page_spec.
Qed.
Lemma smmu_map_page_spec_exists:
forall habd habd' labd cbndx index iova pte f
(Hspec: smmu_map_page_spec cbndx index iova pte habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', smmu_map_page_spec cbndx index iova pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; repeat srewrite; simpl in *.
inv Hspec; eexists; split. reflexivity. constructor.
destruct habd'; destruct shared; simpl in *; srewrite; reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
destruct_if. bool_rel. apply Z.lor_eq_0_iff in Case. destruct Case. inversion H0.
eexists; split. reflexivity. constructor. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
extract_if. apply andb_true_iff; split; bool_rel_all0; somega. rewrite Cond.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
destruct_if. bool_rel. apply Z.lor_eq_0_iff in Case. destruct Case. inversion H0.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite ZMap.set2; simpl).
repeat rewrite (zmap_comm _ _ Hneq0); repeat rewrite ZMap.set2.
reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *; srewrite; repeat rewrite ZMap.set2; reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *; srewrite; repeat rewrite ZMap.set2; reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *; srewrite; repeat rewrite ZMap.set2; reflexivity.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Qed.
Lemma smmu_map_page_spec_ref:
compatsim (crel RData RData) (gensem smmu_map_page_spec) smmu_map_page_spec_low.
Proof.
Opaque smmu_map_page_spec.
compatsim_simpl (@match_RData).
exploit smmu_map_page_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma el2_arm_lpae_iova_to_phys_spec_exists:
forall habd habd' labd iova cbndx index f
(Hspec: el2_arm_lpae_iova_to_phys_spec iova cbndx index habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', el2_arm_lpae_iova_to_phys_spec iova cbndx index labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; repeat srewrite; simpl in *.
inv Hspec; eexists; split. reflexivity. constructor.
destruct habd'; destruct shared; simpl in *; srewrite. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
inv Hspec. eexists; split. reflexivity. constructor.
destruct labd, shared; repeat rewrite ZMap.set2; reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
inv Hspec; simpl in *. repeat (srewrite; try rewrite ZMap.gss; simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; repeat rewrite ZMap.set2; simpl in *; srewrite; reflexivity.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Qed.
Lemma el2_arm_lpae_iova_to_phys_spec_ref:
compatsim (crel RData RData) (gensem el2_arm_lpae_iova_to_phys_spec) el2_arm_lpae_iova_to_phys_spec_low.
Proof.
Opaque el2_arm_lpae_iova_to_phys_spec.
compatsim_simpl (@match_RData).
exploit el2_arm_lpae_iova_to_phys_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent el2_arm_lpae_iova_to_phys_spec.
Qed.
Lemma el2_arm_lpae_clear_spec_exists:
forall habd habd' labd iova cbndx index f
(Hspec: el2_arm_lpae_clear_spec iova cbndx index habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', el2_arm_lpae_clear_spec iova cbndx index labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
Local Transparent Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; repeat srewrite; simpl in *.
destruct_if; srewrite; eexists; (split; [reflexivity|constructor;reflexivity]).
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct_if. destruct_if. eexists; (split; [reflexivity|constructor;reflexivity]).
inversion C24. inversion C24.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct_if. destruct_if. inversion C24.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite ZMap.set2; simpl).
repeat rewrite (zmap_comm _ _ Hneq0); repeat rewrite ZMap.set2. reflexivity.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite ZMap.set2; simpl).
repeat rewrite (zmap_comm _ _ Hneq0); repeat rewrite ZMap.set2. reflexivity.
assert(id_cpu: negb (zeq (curid labd) (curid labd)) = false).
destruct zeq. reflexivity. omega.
repeat (srewrite; try rewrite ZMap.gss; simpl).
destruct_if. destruct_if. inversion C24.
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq2).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
repeat (try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
repeat (srewrite; try rewrite ZMap.gss; simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); simpl).
assert_gso. bool_rel_all0; omega.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq); try rewrite (ZMap.gso _ _ Hneq0); simpl).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq1).
assert_gso. bool_rel_all0; omega. rewrite (ZMap.gso _ _ Hneq2).
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
eexists; split. reflexivity. constructor.
destruct labd; destruct shared; simpl in *.
repeat (srewrite; try rewrite ZMap.gss; try rewrite (ZMap.gso _ _ Hneq);
try rewrite (ZMap.gso _ _ Hneq0); try rewrite (ZMap.gso _ _ Hneq1);
try rewrite (ZMap.gso _ _ Hneq2); simpl).
repeat (try rewrite (zmap_comm _ _ Hneq0); try rewrite (zmap_comm _ _ Hneq)).
repeat rewrite ZMap.set2. reflexivity.
Local Opaque Z.eqb Z.leb Z.geb Z.ltb Z.gtb.
Qed.
Lemma el2_arm_lpae_clear_spec_ref:
compatsim (crel RData RData) (gensem el2_arm_lpae_clear_spec) el2_arm_lpae_clear_spec_low.
Proof.
Opaque el2_arm_lpae_clear_spec.
compatsim_simpl (@match_RData).
exploit el2_arm_lpae_clear_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Transparent el2_arm_lpae_clear_spec.
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) SmmuOps_passthrough SmmuAux.
Proof.
sim_oplus; layer_sim_simpl; compatsim_simpl (@match_AbData);
match_external_states_simpl; destruct match_related; srewrite; try reflexivity.
- unfold host_get_fault_ipa_spec; srewrite; reflexivity.
- unfold get_exception_vector_spec; srewrite; reflexivity.
- unfold read_hpfar_el2_spec; srewrite; reflexivity.
- unfold read_esr_el2_spec; srewrite; reflexivity.
- unfold set_shadow_dirty_bit_spec; srewrite; reflexivity.
- unfold host_skip_instr_spec; srewrite; reflexivity.
Qed.
End PassthroughPrim.
End WITHMEM.
End SmmuOpsProofHigh.