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 Constants.
Require Import HypsecCommLib.
Require Import SmmuOps.Layer.
Require Import VCPUOpsAux.Layer.
Require Import VCPUOpsAux.Spec.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section VCPUOpsAuxProofHigh.
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 := VCPUOpsAux_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := SmmuOps_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.
Lemma reset_gp_regs_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: reset_gp_regs_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', reset_gp_regs_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; srewrite; try reflexivity.
simpl; repeat destruct_if; reflexivity.
Qed.
Lemma reset_gp_regs_spec_ref:
compatsim (crel RData RData) (gensem reset_gp_regs_spec) reset_gp_regs_spec_low.
Proof.
Opaque reset_gp_regs_spec.
compatsim_simpl (@match_RData).
exploit reset_gp_regs_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma reset_sys_regs_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: reset_sys_regs_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', reset_sys_regs_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *; repeat simpl_hyp Hspec; contra; inv Hspec; srewrite;
try (eexists; split; [reflexivity|constructor;reflexivity]).
extract_if. autounfold in *; apply andb_true_iff; split; bool_rel_all; somega. rewrite Cond.
simpl. unfold set_shadow_ctxt_spec; srewrite.
repeat destruct_if; eexists; (split; [reflexivity|constructor;destruct habd'; simpl in *; srewrite; reflexivity]).
extract_if. autounfold in *; apply andb_true_iff; split; bool_rel_all; somega. rewrite Cond.
eexists; split. reflexivity. constructor; reflexivity.
Qed.
Lemma reset_sys_regs_spec_ref:
compatsim (crel RData RData) (gensem reset_sys_regs_spec) reset_sys_regs_spec_low.
Proof.
Opaque reset_sys_regs_spec.
compatsim_simpl (@match_RData).
exploit reset_sys_regs_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma sync_dirty_to_shadow_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: sync_dirty_to_shadow_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', sync_dirty_to_shadow_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros until f.
solve_refine_proof sync_dirty_to_shadow0; repeat hstep; try htrivial.
Qed.
Lemma sync_dirty_to_shadow_spec_ref:
compatsim (crel RData RData) (gensem sync_dirty_to_shadow_spec) sync_dirty_to_shadow_spec_low.
Proof.
Opaque sync_dirty_to_shadow_spec.
compatsim_simpl (@match_RData).
exploit sync_dirty_to_shadow_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma prep_wfx_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: prep_wfx_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', prep_wfx_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros; inv Hrel; repeat autounfold in *; srewrite. reflexivity.
Qed.
Lemma prep_wfx_spec_ref:
compatsim (crel RData RData) (gensem prep_wfx_spec) prep_wfx_spec_low.
Proof.
Opaque prep_wfx_spec.
compatsim_simpl (@match_RData).
exploit prep_wfx_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma prep_hvc_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: prep_hvc_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', prep_hvc_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. inv Hrel. repeat autounfold in *.
pose proof (id_npts0 vmid). destruct H. srewrite.
repeat (simpl_hyp Hspec; contra); inv Hspec; repeat destruct_con0.
- destruct_if.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
srewrite.
destruct_if. eexists; split. reflexivity. constructor; try assumption; srewrite; try reflexivity.
eexists; split. reflexivity. constructor; try assumption; srewrite; try reflexivity.
- eexists; split. reflexivity. constructor; try assumption; srewrite; try reflexivity.
- repeat (srewrite; simpl in *); bool_rel_all.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
simpl. extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
destruct_if. bool_rel_all; omega.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
rewrite ZMap.gss. simpl. srewrite. simpl. srewrite.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
intros. destruct_zmap. constructor; simpl; try assumption; srewrite; try reflexivity.
apply id_npts0.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
destruct_if. bool_rel_all; omega.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
destruct_if. bool_rel_all; omega.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
destruct_if. bool_rel_all; omega.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
destruct_if. bool_rel_all; omega.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
Qed.
Lemma prep_hvc_spec_ref:
compatsim (crel RData RData) (gensem prep_hvc_spec) prep_hvc_spec_low.
Proof.
Opaque prep_hvc_spec.
compatsim_simpl (@match_RData).
exploit prep_hvc_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma prep_abort_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: prep_abort_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', prep_abort_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. inv Hrel. repeat autounfold in *.
pose proof (id_npts0 vmid). destruct H. srewrite.
repeat (simpl_hyp Hspec; contra); inv Hspec; repeat destruct_con0.
- repeat (srewrite; simpl); bool_rel_all.
destruct_if.
srewrite. eexists; split. reflexivity. constructor; try assumption; srewrite; try reflexivity.
eexists; split. reflexivity. constructor; try assumption; srewrite; try reflexivity.
- repeat (srewrite; simpl in *); bool_rel_all.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
simpl. extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
rewrite ZMap.gss. simpl. srewrite. simpl. srewrite.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
intros. destruct_zmap. constructor; simpl; try assumption; srewrite; try reflexivity.
apply id_npts0.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
- extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite]. simpl.
eexists; split. reflexivity. constructor; simpl; try assumption; srewrite; try reflexivity.
Qed.
Lemma prep_abort_spec_ref:
compatsim (crel RData RData) (gensem prep_abort_spec) prep_abort_spec_low.
Proof.
Opaque prep_abort_spec.
compatsim_simpl (@match_RData).
exploit prep_abort_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma update_exception_gp_regs_spec_exists:
forall habd habd' labd vmid vcpuid f
(Hspec: update_exception_gp_regs_spec vmid vcpuid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', update_exception_gp_regs_spec vmid vcpuid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. inv Hrel. repeat autounfold in *.
repeat (simpl_hyp Hspec; contra); inv Hspec; repeat (srewrite; simpl); bool_rel_all.
destruct_if. eexists; split. reflexivity. constructor. reflexivity.
eexists; split. reflexivity.
constructor. rewrite <- C0. destruct habd'; destruct shared; simpl; reflexivity.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
eexists; split. reflexivity. constructor. reflexivity.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
eexists; split. reflexivity. constructor. reflexivity.
Qed.
Lemma update_exception_gp_regs_spec_ref:
compatsim (crel RData RData) (gensem update_exception_gp_regs_spec) update_exception_gp_regs_spec_low.
Proof.
Opaque update_exception_gp_regs_spec.
compatsim_simpl (@match_RData).
exploit update_exception_gp_regs_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma post_handle_shadow_s2pt_fault_spec_exists:
forall habd habd' labd vmid vcpuid addr f
(Hspec: post_handle_shadow_s2pt_fault_spec vmid vcpuid addr habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', post_handle_shadow_s2pt_fault_spec vmid vcpuid addr labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. inv Hrel. repeat autounfold in *.
repeat (simpl_hyp Hspec; contra); inv Hspec; repeat (srewrite; simpl); bool_rel_all.
destruct_if. eexists; split. reflexivity. constructor. reflexivity.
eexists; split. reflexivity.
constructor. rewrite <- C0. destruct habd'; destruct shared; simpl; reflexivity.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
eexists; split. reflexivity. constructor. reflexivity.
extract_if; [try (apply andb_true_iff; split); bool_rel; trivial; somega|srewrite].
eexists; split. reflexivity. constructor. reflexivity.
Qed.
Lemma post_handle_shadow_s2pt_fault_spec_ref:
compatsim (crel RData RData) (gensem post_handle_shadow_s2pt_fault_spec) post_handle_shadow_s2pt_fault_spec_low.
Proof.
Opaque post_handle_shadow_s2pt_fault_spec.
compatsim_simpl (@match_RData).
exploit post_handle_shadow_s2pt_fault_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) VCPUOpsAux_passthrough SmmuOps.
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 read_esr_el2_spec; srewrite; reflexivity.
- unfold set_shadow_dirty_bit_spec; srewrite; reflexivity.
Qed.
End PassthroughPrim.
End WITHMEM.
End VCPUOpsAuxProofHigh.