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 VCPUOpsAux.Layer.
Require Import VCPUOps.Layer.
Require Import HypsecCommLib.
Require Import VCPUOps.Spec.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section VCPUOpsProofHigh.
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 := VCPUOps_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := VCPUOpsAux_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 save_shadow_kvm_regs_spec_exists:
forall habd habd' labd f
(Hspec: save_shadow_kvm_regs_spec habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', save_shadow_kvm_regs_spec labd = Some labd' /\ 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 save_shadow_kvm_regs_spec_ref:
compatsim (crel RData RData) (gensem save_shadow_kvm_regs_spec) save_shadow_kvm_regs_spec_low.
Proof.
Opaque save_shadow_kvm_regs_spec.
compatsim_simpl (@match_RData).
exploit save_shadow_kvm_regs_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma restore_shadow_kvm_regs_spec_exists:
forall habd habd' labd f
(Hspec: restore_shadow_kvm_regs_spec habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', restore_shadow_kvm_regs_spec 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 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.
Qed.
Lemma restore_shadow_kvm_regs_spec_ref:
compatsim (crel RData RData) (gensem restore_shadow_kvm_regs_spec) restore_shadow_kvm_regs_spec_low.
Proof.
Opaque restore_shadow_kvm_regs_spec.
compatsim_simpl (@match_RData).
exploit restore_shadow_kvm_regs_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) VCPUOps_passthrough VCPUOpsAux.
Proof.
sim_oplus; layer_sim_simpl; compatsim_simpl (@match_AbData);
match_external_states_simpl; destruct match_related; srewrite; try reflexivity.
Qed.
End PassthroughPrim.
End WITHMEM.
End VCPUOpsProofHigh.