Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import RData.
Require Import Constants.
Require Import HighSpecs.
Require Import HypsecCommLib.
Local Open Scope Z.
Lemma query_oracle_indisting:
forall vmid d1 d2 d1' d2'
(role1: valid_role vmid d1)
(role2: valid_role vmid d2)
(role1': valid_role vmid d1')
(role2': valid_role vmid d2')
(inv1: invariant d1)
(inv2: invariant d2)
(halt1: halt d1 = false)
(halt2: halt d2 = false)
(halt1': halt d1' = false)
(halt2': halt d2' = false)
(ex1: query_oracle d1 = Some d1')
(ex2: query_oracle d2 = Some d2')
(obseq: obs_eq vmid d1 d2),
obs_eq vmid d1' d2'.
Proof.
Local Transparent query_oracle.
intros. unfold query_oracle in *.
simpl in ex1, ex2.
assert(query_inv: forall d d' (Hinv: invariant d1) (Hquery: query_oracle d = Some d'), invariant d').
{ intros. unfold query_oracle in Hquery.
induction (log d).
assumption.
simpl in *.
destruct e' simpl in *.
- constructor; simpl; intros T; clear_hyp; destruct Hinv; srewrite; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption.
intros; autounfold in *; repeat rewrite ZMap.gss in *; simpl in *.
destruct (gfn =? Z.land (Z.land addr 281474976710655) 1152921504606842880 / 4096) eqn:Hgfn; bool_rel.
rewrite Hgfn in Hpfn. rewrite ZMap.gss in Hpfn. inversion Hpfn.
autounfold in Hpfn_cal. rewrite Hpfn_cal in *; try assumption. left. assumption.
rewrite (ZMap.gso _ _ Hgfn) in Hpfn. eapply host_isolation0; eassumption.
intros; autounfold in *.
assert(Hnh: vmid <> 0) by omega. rewrite (ZMap.gso _ _ Hnh) in Hpfn.
eapply vm_isolation0; eassumption.
- constructor; simpl; intros T; clear_hyp; destruct Hinv; srewrite; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption.
intros; autounfold in *; repeat rewrite ZMap.gss in *; simpl in *.
rewrite Hgfn in Hpfn. rewrite ZMap.gss in Hpfn. inversion Hpfn.
autounfold in Hpfn_cal. rewrite Hpfn_cal in *; try assumption. left. assumption.
intros; autounfold in *.
eapply vm_isolation0; eassumption.
- eapply local_map_page_host_inv.
- eapply local_clear_vm_page_inv.
- constructor; simpl; intros T; destruct Hinv; srewrite; clear_hyp; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption.
intros. destruct (pfn0 =? pfn) eqn:Heq; bool_rel.
rewrite Heq in *. rewrite ZMap.gss; simpl. autounfold. auto.
rewrite (ZMap.gso _ _ Heq). eapply host_isolation0; eassumption.
intros. assert(Hneqvmid: vmid0 <> vmid).
red; intros. rewrite H in *. rewrite Hoff in Hon. inversion Hon.
exploit (vm_isolation0 vmid0); try eassumption. simpl; intro Hiso.
assert(Hneqpfn: pfn0 <> pfn).
red. intros. rewrite H in *. rewrite H0 in Hiso. omega.
rewrite (ZMap.gso _ _ Hneqpfn). eapply vm_isolation0; eassumption.
- eapply local_assign_pfn_to_vm_inv.
- constructor; simpl; intros T; destruct Hinv; srewrite; clear_hyp; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption.
- eapply local_set_vcpu_active_inv.
- eapply local_set_vcpu_inactive_inv.
- eapply local_register_vcpu_inv.
- local_register_kvm_inv.
- local_set_boot_info_inv.
- local_remap_image_inv.
- constructor; simpl; intros T; destruct Hinv; srewrite; clear_hyp; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption.
- constructor; simpl; intros T; destruct Hinv; srewrite; clear_hyp; simpl_local;
destruct Hlocal, Hlocal0; constructor; simpl; try assumption. }
constructor; autounfold; simpl; repeat srewrite; simpl_bool_eq; try reflexivity; try assumption.
inversion C6; inversion C7. subst. replace (1 =? 0) with false in * by (symmetry; bool_rel; omega).
inversion ex1; inversion ex2. rewrite H2, H4. clear_hyp. clear ex1 ex2.
exploit (prep_exit_conf (cur_vmid d1) _ _ _ _ H2 H4); autounfold; simpl; try assumption; try reflexivity.
reflexivity. reflexivity.
constructor; autounfold; simpl; repeat srewrite; simpl_bool_eq; try reflexivity; try assumption.
intros. destruct_zmap. reflexivity. apply shadow_ctxt_eq0. assumption.
intros (Hind3 & cur31 & cur32 & vc3).
srewrite; split_and; try reflexivity. assumption.
inversion C6. subst. simpl_bool_eq. inversion ex1. rewrite <- H2 in hlt1; simpl in hlt1; contra.
simpl_hyp ex1. inversion ex1; inversion ex2. rewrite H2, H4. clear_hyp. clear ex1 ex2.
exploit (prep_exit_conf (cur_vmid d1) _ _ _ _ H2 H4); autounfold; simpl; try assumption; try reflexivity.
rewrite cur1; assumption. rewrite cur1, cur2; reflexivity.
reflexivity. reflexivity.
constructor; autounfold; simpl; repeat srewrite; simpl_bool_eq; try reflexivity; try assumption.
intros. destruct_zmap. reflexivity. apply shadow_ctxt_eq0. assumption.
intros (Hind3 & cur31 & cur32 & vc3).
srewrite; split_and; try reflexivity. assumption.
destruct (X0 @ t0 =? HVC_TIMER_SET_CNTVOFF).
unfold_spec H6. unfold_spec H8. inv H6. inv H8.
destruct indist; repeat split; try assumption.
destruct (X0 @ t0 =? HVC_CLEAR_VM_S2_RANGE).
eassumption.
destruct (X0 @ t0 =? HVC_SET_BOOT_INFO).
unfold_spec H6. unfold_spec H8. simpl_conf H6 H8.
pose proof (query_oracle_conf _ _ vmid _ _ H1 H3 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H1 H3 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
inv H6. inv H8.
unfold_spec H2. unfold_spec H4. simpl_conf H2 H4.
inv H2. inv H4. repeat split; solve_role; try solve_conf indist.
unfold valid_role in *. left. reflexivity. unfold valid_role in *. left. reflexivity.
repeat rewrite Harg_eq in *.
remember (X1 @ t0) as vm0. destruct (vm =? vm0) eqn:Hvms.
bool_rel. inv Hvms. repeat rewrite ZMap.gss.
simpl. pose proof (image_pfn_eq0 (X1 @ t0)).
rewrite H1, H6 in H2. apply H2.
bool_rel. repeat rewrite (ZMap.gso _ _ Hvms). apply image_pfn_eq0.
destruct (X0 @ t0 =? HVC_REMAP_VM_IMAGE).
unfold_spec H6. unfold_spec H8. simpl_conf H6 H8.
pose proof (query_oracle_conf _ _ vmid _ _ H1 H3 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H1 H3 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
inv H6. inv H8.
unfold_spec H2. unfold_spec H4. simpl_conf H2 H4.
unfold_spec H2. unfold_spec H4. simpl in *. simpl_conf H2 H4.
rm_bind H22. rm_bind H26. inv H22. inv H26. inv H2. inv H4.
repeat split; solve_role; try solve_conf indist.
unfold valid_role in *. left. reflexivity. unfold valid_role in *. left. reflexivity.
repeat rewrite (ZMap.gso _ _ host_core_ne). apply mem_eq0.
repeat rewrite Harg_eq in *.
destruct (vm =? X1 @ t0) eqn:Heq; bool_rel.
rewrite <- Heq in *. repeat rewrite ZMap.gss. simpl.
pose proof (image_pfn_eq0 vm). rewrite H1, H11 in H2. inversion H2.
rewrite H22 in *. rewrite H8 in H16. inv H16.
eassumption.
repeat rewrite (ZMap.gso _ _ Heq). apply image_pfn_eq0.
destruct (X0 @ t0 =? HVC_VERIFY_VM_IMAGES).
eassumption.
destruct (X0 @ t0 =? HVC_BOOT_FROM_SAVED_VM).
unfold_spec H6. unfold_spec H8. simpl_conf H6 H8.
pose proof (query_oracle_conf _ _ vmid _ _ H1 H3 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H1 H3 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
inv H6. inv H8.
unfold_spec H2. unfold_spec H4. simpl_conf H2 H4.
inv H2. inv H4. repeat split; solve_role; try solve_conf indist.
unfold valid_role in *. left. reflexivity. unfold valid_role in *. left. reflexivity.
rewrite Harg_eq in *. destruct (vm =? X1 @ t0) eqn:Heq; bool_rel.
rewrite Heq. repeat rewrite ZMap.gss. simpl.
pose proof (image_pfn_eq0 (X1 @ t0)). rewrite H1, H5 in H2. apply H2.
repeat rewrite (ZMap.gso _ _ Heq). apply image_pfn_eq0.
destruct (X0 @ t0 =? HVC_SAVE_CRYPT_VCPU).
unfold_spec H6. unfold_spec H8. unfold shadow_to_int_encrypt_spec, set_int_ctxt_spec in *.
simpl_conf H6 H8. destruct p, p0. simpl_conf H6 H8. inv H8. inv H6. clear H3 H5.
unfold_spec H2. unfold_spec H1. simpl_conf H2 H1.
pose proof (query_oracle_conf _ _ HOSTVISOR _ _ H6 H3 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H6 H3 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
inv H1. inv H2. repeat split; solve_role; try solve_conf indist.
destruct (X0 @ t0 =? HVC_REGISTER_KVM).
simpl_hyp H6. simpl_hyp H8. destruct p. destruct p0. inv H6. inv H8.
unfold_spec H1. unfold_spec H2. simpl_conf H1 H2.
pose proof (query_oracle_conf _ _ HOSTVISOR _ _ H3 H8 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H3 H8 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
unfold_spec H4. unfold_spec H9. simpl_conf H4 H9.
unfold_spec H4. unfold_spec H9. simpl_conf H4 H9.
inv H4. inv H9. inv H1. inv H2. repeat split; solve_role; try solve_conf indist.
unfold valid_role in *. left. reflexivity. unfold valid_role in *. left. reflexivity.
assert(HOSTVISOR <> next_vmid (core_data r3)) by eassumption.
assert(HOSTVISOR <> next_vmid (core_data r5)) by eassumption.
rewrite (ZMap.gso _ _ H1). rewrite (ZMap.gso _ _ H2). apply mem_eq0.
inv H10. inv H5.
destruct (vm =? next_vmid (core_data r3)) eqn:Heq1, (vm =? next_vmid (core_data r5)) eqn:Heq2; bool_rel.
rewrite <- Heq1, <- Heq2. repeat rewrite ZMap.gss. simpl.
rewrite <-Heq1, <-Heq2 in *. pose proof (image_pfn_eq0 vm). rewrite H17, H13 in H1. apply H1.
rewrite (ZMap.gso _ _ Heq2). rewrite Heq1. rewrite ZMap.gss. simpl.
rewrite <- Heq1 in *. pose proof (image_pfn_eq0 vm). rewrite H13 in H1. apply H1.
rewrite (ZMap.gso _ _ Heq1). rewrite Heq2. rewrite ZMap.gss. simpl.
rewrite <- Heq2 in *. pose proof (image_pfn_eq0 vm). rewrite H17 in H1. apply H1.
rewrite (ZMap.gso _ _ Heq1), (ZMap.gso _ _ Heq2). apply image_pfn_eq0.
destruct (X0 @ t0 =? HVC_REGISTER_VCPU).
simpl_hyp H6. simpl_hyp H8. destruct p. destruct p0. inv H6. inv H8.
unfold_spec H1. unfold_spec H2. simpl_conf H1 H2.
pose proof (query_oracle_conf _ _ HOSTVISOR _ _ H3 H10 role1 role2 Hinv1' Hinv2' indist) as Hqo.
clear H3 H10 role1 role2 Hinv1' Hinv2' indist.
destruct Hqo as (role1 & role2 & Hinv1' & Hinv2' & indist & Hact1 & Hact2).
rewrite Hact1 in act1. rewrite Hact2 in act2. clear Hact1 Hact2.
unfold_spec H4. unfold_spec H11. simpl_conf H4 H11.
inv H4. inv H11. inv H1. inv H2. repeat split; solve_role; try solve_conf indist.
unfold valid_role in *. left. reflexivity. unfold valid_role in *. left. reflexivity.
rewrite Harg_eq in *. destruct (vm =? X1 @ t0) eqn:Heq; bool_rel.
rewrite Heq. repeat rewrite ZMap.gss. simpl.
pose proof (image_pfn_eq0 (X1 @ t0)). rewrite H3, H20 in H1. apply H1.
repeat rewrite (ZMap.gso _ _ Heq). apply image_pfn_eq0.
Qed.