Library mcertikos.proc.VMCSIntroGenFresh
This file provide the contextual refinement proof between VEPTInit layer and PVMCSIntro layer
Section Refinement.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{real_params: RealParams}.
Require Import Conventions.
Local Opaque Z.shiftl.
Lemma Int64_unsigned_repr_32:
∀ i,
Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i.
Proof.
intros. rewrite Int64.unsigned_repr; trivial.
pose proof (Int.unsigned_range i) as Hr.
change Int64.max_unsigned with (MAX_INT_64 -1).
change Int.modulus with MAX_INT_32 in Hr.
omega.
Qed.
Require Import CLemmas.
Lemma Int64_ofswords_Z:
∀ i1 i2,
Int64.repr (Z.lor (Z.shiftl (Int.unsigned i2) 32) (Int.unsigned i1)) =
Int64.ofwords i2 i1.
Proof.
unfold Int64.ofwords.
unfold Int64.or, Int64.shl.
change (Int64.unsigned (Int64.repr Int.zwordsize)) with 32.
intros.
repeat rewrite Int64_unsigned_repr_32.
rewrite Int64.unsigned_repr. trivial.
eapply Z_shiftl_32_range.
pose proof (Int.unsigned_range i2) as Hr.
change Int.modulus with MAX_INT_32 in Hr.
rewrite_omega.
Qed.
Locate Z.lor_nonneg.
Lemma neq_i:
∀ i,
i ≠ i + 1.
Proof.
red; intros.
omega.
Qed.
Lemma Z_shiftr_32_range:
∀ i a,
0 ≤ i ≤ a →
0 ≤ Z.shiftr i 32 ≤ a.
Proof.
split.
rewrite Z.shiftr_nonneg. omega.
rewrite (Z.shiftr_div_pow2 i 32); try omega.
destruct (zeq i 0); subst.
- change (0 / 2 ^ 32) with 0. omega.
- exploit (Z_div_lt i (2 ^ 32)); try omega.
change (2 ^ 32) with MAX_INT_32. omega.
Qed.
Lemma Int64_unsigned_range:
∀ i,
0 ≤ Int64.unsigned i ≤ Int64.max_unsigned.
Proof.
intros. specialize (Int64.unsigned_range i).
change Int64.modulus with MAX_INT_64.
change Int64.max_unsigned with (MAX_INT_64 - 1).
omega.
Qed.
Lemma vmx_enable_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_enable_spec) vmx_enable_spec_low.
Proof.
simpl. constructor.
reduce_to_sim_step.
intros s b ι WB1 vargs1 vargs2 vres m1 d1 m1´ d1´ rs2 m2 d2 _
Hlow Hhigh Hhigh´ H Hmd Hsi Hpc Hι. intros.
∃ ι, (rs2 # RA <- Vundef # PC <- (rs2 RA)).
compatsim_simpl_inv_match H Hmd (@match_AbData).
functional inversion H1; subst.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
intros.
destruct r; simpl; try constructor; elim H0; eauto 13.
Qed.
Lemma vmcs_writez64_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_writez64_spec)
vmcs_writez64_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (Hrange´: 0 ≤ Int.unsigned i + 1 ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
destruct (HMem _ Hrange´) as (v2 & HL2 & HV2 & HM´).
intros.
inv_val_inject.
inv EXTCALL_ARG. inv H12. inv H14.
inv H16. inv Hargs. inv H.
inv H8.
destruct v0; destruct v; inv H13.
specialize (Mem.valid_access_store _ _ _ _ (Vint i2) HV1); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store
_ _ _ _ (Vint i1) HV2);
intros [m1 HST2].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split.
- econstructor; eauto.
instantiate (1:= (m0, d2)).
instantiate (1:= i2).
Opaque Z.mul.
simpl; lift_trivial. rewrite <- H. rewrite HST1. trivial.
instantiate (1:= d2).
instantiate (1:= m1).
instantiate (1:= i1).
simpl; lift_trivial.
replace (4096 × CPU_ID d1 + (Int.unsigned i + 1) × 4 + 8)
with (4096 × CPU_ID d1 + Int.unsigned i × 4 + 12) in HST2 by omega.
rewrite <- H.
rewrite HST2. trivial.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
constructor.
apply H11.
assumption.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H17 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
+ destruct (zeq i0 (Int.unsigned i)); subst.
×
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
eapply Mem.load_store_same; eauto.
right; simpl. left; omega.
unfold write64_aux.
rewrite ZMap.gso; [| apply neq_i].
rewrite ZMap.gss.
simpl.
rewrite <- (Int64.lo_ofwords i1 i2) at 2.
unfold Int64.loword.
rewrite Int64.unsigned_repr.
constructor.
eapply Int64_unsigned_range.
×
destruct (zeq i0 (Int.unsigned i + 1)); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
unfold write64_aux.
rewrite ZMap.gss.
simpl.
rewrite <- (Int64.hi_ofwords i1 i2) at 2.
unfold Int64.hiword, Int64.shru.
change (Int64.unsigned (Int64.repr Int.zwordsize)) with 32.
rewrite Int64.unsigned_repr; trivial.
rewrite Int64.unsigned_repr; trivial.
rewrite Int64.unsigned_repr; trivial.
eapply Z_shiftr_32_range; eauto.
eapply Int64_unsigned_range; eauto.
eapply Int64_unsigned_range; eauto.
eapply Z_shiftr_32_range; eauto.
eapply Int64_unsigned_range; eauto.
}
{
specialize (HMem _ H0).
destruct HMem as (v & HLD & HV & HVV).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt i0 ((Int.unsigned i + 1))); [left; omega|right; omega].
simpl; right. destruct (zlt i0 ((Int.unsigned i))); [left; omega|right; omega].
unfold write64_aux.
repeat rewrite ZMap.gso; eauto.
}
+ rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right; left. omega.
simpl; right; left. omega.
+ rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right; left. omega.
simpl; right; left. omega.
- apply inject_incr_refl.
- constructor;
constructor.
- intros.
destruct r; simpl; try constructor; elim H2; eauto 13.
- constructor.
- constructor.
Qed.
Lemma vmcs_readz64_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_readz64_spec)
vmcs_readz64_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
pose proof H1 as HMem.
pose proof H1 as HMem´.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (Hrange´: 0 ≤ Int.unsigned i + 1 ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
specialize (H1 _ Hrange).
destruct H1 as (v1 & HL1 & _ & HM).
specialize (HMem´ _ Hrange´).
destruct HMem´ as (v2 & HL2 & _ & HM´).
functional inversion H2; subst.
rewrite H11 in H0. inv H0.
rewrite H13 in HM. inv HM.
rewrite H14 in HM´. inv HM´.
replace (4096 × CPU_ID d1´ + (Int.unsigned i + 1) × 4 + 8)
with (4096 × CPU_ID d1´ + Int.unsigned i × 4 + 12) in HL2 by omega.
intros.
assert (Heq: z = Int64.ofwords v3 v0).
{
rewrite <- (Int64.repr_unsigned z).
rewrite <- H.
eapply Int64_ofswords_Z.
}
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX <- (Vint v0) #EDX <- (Vint v3)).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. lift_unfold. rewrite <- H0. rewrite HL1. reflexivity.
- simpl. lift_unfold. rewrite <- H0.
eauto.
- rewrite H. reflexivity.
- inv EXTCALL_ARG.
inv Hι. inv Hargs. inv H21. inv H20. inv H22;
econstructor; eauto.
constructor.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint v3)
end.
rewrite Heq.
simpl. rewrite Int64.hi_ofwords.
constructor.
- constructor.
match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint v0)
end.
rewrite Heq.
simpl. rewrite Int64.lo_ofwords.
constructor.
constructor.
- intros.
destruct r; simpl; try constructor; elim H15; eauto 13.
Qed.
Lemma vmcs_readz_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_readz_spec)
vmcs_readz_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros. inv H.
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
pose proof H1 as HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
specialize (H1 _ Hrange).
destruct H1 as (v1 & HL1 & _ & HM).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
rewrite H13 in H0. inv H0.
rewrite H15 in HM. inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H1.
rewrite Int.repr_unsigned. trivial.
}
subst v1.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX <- (Vint z)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. lift_unfold. rewrite <- H.
eauto.
- inv EXTCALL_ARG. inv H12.
inv Hι. inv Hargs. inv H12. inv H13.
econstructor; eauto.
constructor.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint z)
end.
constructor.
- intros.
destruct r; simpl; try constructor; elim H1; eauto 13.
Qed.
Lemma vmcs_writez_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_writez_spec)
vmcs_writez_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split.
- econstructor; eauto.
+ lift_unfold. rewrite <- H. split; eauto.
+ inv Hargs. inv EXTCALL_ARG.
inv H11.
econstructor; eauto.
inv H13.
econstructor; eauto.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H13 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (HMem _ H0).
destruct HMem as (z & HLD & HV & HVV).
destruct (zeq i3 (Int.unsigned i)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto. subst d´.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right. destruct (zlt i3 ((Int.unsigned i))); [left; omega|right; omega].
subst d´.
rewrite ZMap.gso; trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left.
omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H5; eauto.
simpl; right; left.
omega.
- apply inject_incr_refl.
- constructor; eauto.
- intros.
destruct r; simpl; try constructor; elim H2; eauto 13.
- constructor.
- constructor.
Qed.
Lemma vmcs_write_ident_spec_ref:
compatsim (crel HDATA LDATA) (vmcs_writeb_compatsem vmcs_write_ident_spec)
vmcs_write_ident_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned loc) = Some enc).
{
simpl; inv match_related.
functional inversion H5.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned loc ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (HFB: ι b0 = Some (b0, 0)).
{
revert H7.
intros (fun_id & Hsymbol).
exploit stencil_find_symbol_inject´; eauto.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vptr b0 ofs) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H9. rename H into CPU_eq.
refine_split.
- econstructor; eauto.
+ lift_unfold. rewrite <- CPU_eq. split; eauto.
+ inv H0. inv EXTCALL_ARG.
inv H13. inv H15.
rewrite H2 in HFB. inv HFB.
rewrite Int.add_zero in H12.
econstructor; eauto.
econstructor; eauto.
constructor; eauto.
- pose proof H5 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H14 in H1. inv H1.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (HMem _ H).
destruct HMem as (z & HLD & HV & HVV).
destruct (zeq i0 (Int.unsigned loc)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto. subst d´.
repeat rewrite ZMap.gss.
econstructor; eauto.
rewrite Int.add_zero; trivial.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right. destruct (zlt i0 ((Int.unsigned loc))); [left; omega|right; omega].
subst d´.
rewrite ZMap.gso; trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left.
omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H6; eauto.
simpl; right; left.
omega.
- apply inject_incr_refl.
- constructor; eauto.
- intros.
destruct r; simpl; try constructor; elim H; eauto 13.
- constructor.
- constructor.
Qed.
Lemma rcr0_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr0_spec) rcr0_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma rcr3_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr3_spec) rcr3_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma rcr4_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr4_spec) rcr4_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma vmptrld_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmptrld_spec) vmptr_ld_spec_low.
Proof.
simpl. constructor.
reduce_to_sim_step.
intros s b ι WB1 vargs1 vargs2 vres m1 d1 m1´ d1´ rs2 m2 d2 _
Hlow Hhigh Hhigh´ H Hmd Hsi Hpc Hι.
compatsim_simpl_inv_match H Hmd (@match_AbData).
functional inversion H1; subst.
inv H.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. inv match_related. split; congruence.
- intros.
destruct r; simpl; try constructor; elim H; eauto 13.
Qed.
Lemma rdmsr_spec_ref:
compatsim (crel HDATA LDATA) (gensem rdmsr_spec) rdmsr_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#EAX<- Vzero#EDX <- Vzero#PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv Hargs.
inv EXTCALL_ARG. inv H9.
econstructor. eassumption.
constructor.
- simpl. inv match_related. split; congruence.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int64.repr_unsigned z). rewrite <- H0.
constructor.
- constructor.
match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int64.repr_unsigned z). rewrite <- H0.
constructor.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma wrmsr_spec_ref:
compatsim (crel HDATA LDATA) (gensem wrmsr_spec) wrmsr_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX:: IR EDX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA) #EAX <- Vzero).
inv_val_inject.
inv Hargs. inv H4.
inv EXTCALL_ARG. inv H12. inv H14. inv H13. inv H7.
destruct v0; destruct v; inv H9.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- econstructor. eassumption.
econstructor. eassumption.
econstructor. eassumption.
constructor.
- simpl. inv match_related. split; congruence.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma vmcs_get_revid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_get_revid_spec)
vmcs_get_revid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
assert (HP: revid = z).
{
functional inversion H2; subst.
rewrite H12 in H0. inv H0.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto.
econstructor; eauto.
simpl. lift_unfold. rewrite Z.add_0_r. rewrite <- H; eauto.
Qed.
Lemma vmcs_get_abrtid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_get_abrtid_spec)
vmcs_get_abrtid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
assert (HP: abrtid = z).
{
functional inversion H2; subst.
rewrite H12 in H0. inv H0.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto.
econstructor; eauto.
simpl. lift_unfold. rewrite <- H; eauto.
Qed.
Lemma vmcs_set_revid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_set_revid_spec)
vmcs_set_revid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
inv H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) H4); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H8.
rename H into CPU_ID_eq.
refine_split.
- econstructor; eauto.
lift_unfold. rewrite Z.add_0_r. rewrite <- CPU_ID_eq. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H12 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (H2 _ H).
destruct H2 as (v & HLD & HV & HVV).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right; right; omega.
+ exploit Mem.load_store_same; eauto.
simpl.
rewrite Int.repr_unsigned. trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H5; eauto.
simpl; right; right; omega.
- apply inject_incr_refl.
Qed.
Lemma vmcs_set_abrtid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_set_abrtid_spec)
vmcs_set_abrtid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
inv H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) H6); intros [m´ HST].
refine_split.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H8. rename H into CPU_ID_eq.
- econstructor; eauto.
lift_unfold. rewrite <- CPU_ID_eq. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H12 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (H2 _ H).
destruct H2 as (v & HLD & HV & HVV).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right; right; omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left; omega.
+ exploit Mem.load_store_same; eauto.
simpl.
rewrite Int.repr_unsigned. trivial.
- apply inject_incr_refl.
Qed.
End WITHMEM.
End Refinement.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{real_params: RealParams}.
Require Import Conventions.
Local Opaque Z.shiftl.
Lemma Int64_unsigned_repr_32:
∀ i,
Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i.
Proof.
intros. rewrite Int64.unsigned_repr; trivial.
pose proof (Int.unsigned_range i) as Hr.
change Int64.max_unsigned with (MAX_INT_64 -1).
change Int.modulus with MAX_INT_32 in Hr.
omega.
Qed.
Require Import CLemmas.
Lemma Int64_ofswords_Z:
∀ i1 i2,
Int64.repr (Z.lor (Z.shiftl (Int.unsigned i2) 32) (Int.unsigned i1)) =
Int64.ofwords i2 i1.
Proof.
unfold Int64.ofwords.
unfold Int64.or, Int64.shl.
change (Int64.unsigned (Int64.repr Int.zwordsize)) with 32.
intros.
repeat rewrite Int64_unsigned_repr_32.
rewrite Int64.unsigned_repr. trivial.
eapply Z_shiftl_32_range.
pose proof (Int.unsigned_range i2) as Hr.
change Int.modulus with MAX_INT_32 in Hr.
rewrite_omega.
Qed.
Locate Z.lor_nonneg.
Lemma neq_i:
∀ i,
i ≠ i + 1.
Proof.
red; intros.
omega.
Qed.
Lemma Z_shiftr_32_range:
∀ i a,
0 ≤ i ≤ a →
0 ≤ Z.shiftr i 32 ≤ a.
Proof.
split.
rewrite Z.shiftr_nonneg. omega.
rewrite (Z.shiftr_div_pow2 i 32); try omega.
destruct (zeq i 0); subst.
- change (0 / 2 ^ 32) with 0. omega.
- exploit (Z_div_lt i (2 ^ 32)); try omega.
change (2 ^ 32) with MAX_INT_32. omega.
Qed.
Lemma Int64_unsigned_range:
∀ i,
0 ≤ Int64.unsigned i ≤ Int64.max_unsigned.
Proof.
intros. specialize (Int64.unsigned_range i).
change Int64.modulus with MAX_INT_64.
change Int64.max_unsigned with (MAX_INT_64 - 1).
omega.
Qed.
Lemma vmx_enable_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_enable_spec) vmx_enable_spec_low.
Proof.
simpl. constructor.
reduce_to_sim_step.
intros s b ι WB1 vargs1 vargs2 vres m1 d1 m1´ d1´ rs2 m2 d2 _
Hlow Hhigh Hhigh´ H Hmd Hsi Hpc Hι. intros.
∃ ι, (rs2 # RA <- Vundef # PC <- (rs2 RA)).
compatsim_simpl_inv_match H Hmd (@match_AbData).
functional inversion H1; subst.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
intros.
destruct r; simpl; try constructor; elim H0; eauto 13.
Qed.
Lemma vmcs_writez64_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_writez64_spec)
vmcs_writez64_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (Hrange´: 0 ≤ Int.unsigned i + 1 ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
destruct (HMem _ Hrange´) as (v2 & HL2 & HV2 & HM´).
intros.
inv_val_inject.
inv EXTCALL_ARG. inv H12. inv H14.
inv H16. inv Hargs. inv H.
inv H8.
destruct v0; destruct v; inv H13.
specialize (Mem.valid_access_store _ _ _ _ (Vint i2) HV1); intros [m0 HST1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST1) in HV2.
specialize (Mem.valid_access_store
_ _ _ _ (Vint i1) HV2);
intros [m1 HST2].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split.
- econstructor; eauto.
instantiate (1:= (m0, d2)).
instantiate (1:= i2).
Opaque Z.mul.
simpl; lift_trivial. rewrite <- H. rewrite HST1. trivial.
instantiate (1:= d2).
instantiate (1:= m1).
instantiate (1:= i1).
simpl; lift_trivial.
replace (4096 × CPU_ID d1 + (Int.unsigned i + 1) × 4 + 8)
with (4096 × CPU_ID d1 + Int.unsigned i × 4 + 12) in HST2 by omega.
rewrite <- H.
rewrite HST2. trivial.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
constructor.
apply H11.
assumption.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H17 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
repeat (eapply Mem.store_valid_access_1; eauto).
+ destruct (zeq i0 (Int.unsigned i)); subst.
×
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
eapply Mem.load_store_same; eauto.
right; simpl. left; omega.
unfold write64_aux.
rewrite ZMap.gso; [| apply neq_i].
rewrite ZMap.gss.
simpl.
rewrite <- (Int64.lo_ofwords i1 i2) at 2.
unfold Int64.loword.
rewrite Int64.unsigned_repr.
constructor.
eapply Int64_unsigned_range.
×
destruct (zeq i0 (Int.unsigned i + 1)); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
unfold write64_aux.
rewrite ZMap.gss.
simpl.
rewrite <- (Int64.hi_ofwords i1 i2) at 2.
unfold Int64.hiword, Int64.shru.
change (Int64.unsigned (Int64.repr Int.zwordsize)) with 32.
rewrite Int64.unsigned_repr; trivial.
rewrite Int64.unsigned_repr; trivial.
rewrite Int64.unsigned_repr; trivial.
eapply Z_shiftr_32_range; eauto.
eapply Int64_unsigned_range; eauto.
eapply Int64_unsigned_range; eauto.
eapply Z_shiftr_32_range; eauto.
eapply Int64_unsigned_range; eauto.
}
{
specialize (HMem _ H0).
destruct HMem as (v & HLD & HV & HVV).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right. destruct (zlt i0 ((Int.unsigned i + 1))); [left; omega|right; omega].
simpl; right. destruct (zlt i0 ((Int.unsigned i))); [left; omega|right; omega].
unfold write64_aux.
repeat rewrite ZMap.gso; eauto.
}
+ rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right; left. omega.
simpl; right; left. omega.
+ rewrite (Mem.load_store_other _ _ _ _ _ _ HST2); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST1); eauto.
simpl; right; left. omega.
simpl; right; left. omega.
- apply inject_incr_refl.
- constructor;
constructor.
- intros.
destruct r; simpl; try constructor; elim H2; eauto 13.
- constructor.
- constructor.
Qed.
Lemma vmcs_readz64_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_readz64_spec)
vmcs_readz64_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
pose proof H1 as HMem.
pose proof H1 as HMem´.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (Hrange´: 0 ≤ Int.unsigned i + 1 ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
specialize (H1 _ Hrange).
destruct H1 as (v1 & HL1 & _ & HM).
specialize (HMem´ _ Hrange´).
destruct HMem´ as (v2 & HL2 & _ & HM´).
functional inversion H2; subst.
rewrite H11 in H0. inv H0.
rewrite H13 in HM. inv HM.
rewrite H14 in HM´. inv HM´.
replace (4096 × CPU_ID d1´ + (Int.unsigned i + 1) × 4 + 8)
with (4096 × CPU_ID d1´ + Int.unsigned i × 4 + 12) in HL2 by omega.
intros.
assert (Heq: z = Int64.ofwords v3 v0).
{
rewrite <- (Int64.repr_unsigned z).
rewrite <- H.
eapply Int64_ofswords_Z.
}
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX <- (Vint v0) #EDX <- (Vint v3)).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. lift_unfold. rewrite <- H0. rewrite HL1. reflexivity.
- simpl. lift_unfold. rewrite <- H0.
eauto.
- rewrite H. reflexivity.
- inv EXTCALL_ARG.
inv Hι. inv Hargs. inv H21. inv H20. inv H22;
econstructor; eauto.
constructor.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint v3)
end.
rewrite Heq.
simpl. rewrite Int64.hi_ofwords.
constructor.
- constructor.
match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint v0)
end.
rewrite Heq.
simpl. rewrite Int64.lo_ofwords.
constructor.
constructor.
- intros.
destruct r; simpl; try constructor; elim H15; eauto 13.
Qed.
Lemma vmcs_readz_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_readz_spec)
vmcs_readz_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros. inv H.
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
pose proof H1 as HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
specialize (H1 _ Hrange).
destruct H1 as (v1 & HL1 & _ & HM).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
rewrite H13 in H0. inv H0.
rewrite H15 in HM. inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H1.
rewrite Int.repr_unsigned. trivial.
}
subst v1.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)#EAX <- (Vint z)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. lift_unfold. rewrite <- H.
eauto.
- inv EXTCALL_ARG. inv H12.
inv Hι. inv Hargs. inv H12. inv H13.
econstructor; eauto.
constructor.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with (Vint z)
end.
constructor.
- intros.
destruct r; simpl; try constructor; elim H1; eauto 13.
Qed.
Lemma vmcs_writez_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_writez_spec)
vmcs_writez_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned i) = Some enc).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned i ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split.
- econstructor; eauto.
+ lift_unfold. rewrite <- H. split; eauto.
+ inv Hargs. inv EXTCALL_ARG.
inv H11.
econstructor; eauto.
inv H13.
econstructor; eauto.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H13 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (HMem _ H0).
destruct HMem as (z & HLD & HV & HVV).
destruct (zeq i3 (Int.unsigned i)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto. subst d´.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right. destruct (zlt i3 ((Int.unsigned i))); [left; omega|right; omega].
subst d´.
rewrite ZMap.gso; trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left.
omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H5; eauto.
simpl; right; left.
omega.
- apply inject_incr_refl.
- constructor; eauto.
- intros.
destruct r; simpl; try constructor; elim H2; eauto 13.
- constructor.
- constructor.
Qed.
Lemma vmcs_write_ident_spec_ref:
compatsim (crel HDATA LDATA) (vmcs_writeb_compatsem vmcs_write_ident_spec)
vmcs_write_ident_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ ∃ enc, vmcs_ZtoEncoding (Int.unsigned loc) = Some enc).
{
simpl; inv match_related.
functional inversion H5.
refine_split´; eauto 1; try congruence.
}
destruct HOS as (Hkern & enc & Henc).
inv H. rename H2 into HMem.
assert (Hrange: 0 ≤ Int.unsigned loc ≤ 27670 + 1).
{
eapply vmcs_ZtoEncoding_range in Henc.
omega.
}
assert (HFB: ι b0 = Some (b0, 0)).
{
revert H7.
intros (fun_id & Hsymbol).
exploit stencil_find_symbol_inject´; eauto.
}
destruct (HMem _ Hrange) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vptr b0 ofs) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H9. rename H into CPU_eq.
refine_split.
- econstructor; eauto.
+ lift_unfold. rewrite <- CPU_eq. split; eauto.
+ inv H0. inv EXTCALL_ARG.
inv H13. inv H15.
rewrite H2 in HFB. inv HFB.
rewrite Int.add_zero in H12.
econstructor; eauto.
econstructor; eauto.
constructor; eauto.
- pose proof H5 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H14 in H1. inv H1.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (HMem _ H).
destruct HMem as (z & HLD & HV & HVV).
destruct (zeq i0 (Int.unsigned loc)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto. subst d´.
repeat rewrite ZMap.gss.
econstructor; eauto.
rewrite Int.add_zero; trivial.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right. destruct (zlt i0 ((Int.unsigned loc))); [left; omega|right; omega].
subst d´.
rewrite ZMap.gso; trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left.
omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H6; eauto.
simpl; right; left.
omega.
- apply inject_incr_refl.
- constructor; eauto.
- intros.
destruct r; simpl; try constructor; elim H; eauto 13.
- constructor.
- constructor.
Qed.
Lemma rcr0_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr0_spec) rcr0_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma rcr3_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr3_spec) rcr3_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma rcr4_spec_ref:
compatsim (crel HDATA LDATA) (gensem rcr4_spec) rcr4_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, (rs2#RA<- Vundef#PC <- (rs2#RA)#EAX <- Vzero).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- change (((rs2 # RA <- Vundef) # PC <- (rs2 RA)) # EAX <- Vzero EAX) with Vzero.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma vmptrld_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmptrld_spec) vmptr_ld_spec_low.
Proof.
simpl. constructor.
reduce_to_sim_step.
intros s b ι WB1 vargs1 vargs2 vres m1 d1 m1´ d1´ rs2 m2 d2 _
Hlow Hhigh Hhigh´ H Hmd Hsi Hpc Hι.
compatsim_simpl_inv_match H Hmd (@match_AbData).
functional inversion H1; subst.
inv H.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- simpl. inv match_related. split; congruence.
- intros.
destruct r; simpl; try constructor; elim H; eauto 13.
Qed.
Lemma rdmsr_spec_ref:
compatsim (crel HDATA LDATA) (gensem rdmsr_spec) rdmsr_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#EAX<- Vzero#EDX <- Vzero#PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv Hargs.
inv EXTCALL_ARG. inv H9.
econstructor. eassumption.
constructor.
- simpl. inv match_related. split; congruence.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int64.repr_unsigned z). rewrite <- H0.
constructor.
- constructor.
match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int64.repr_unsigned z). rewrite <- H0.
constructor.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma wrmsr_spec_ref:
compatsim (crel HDATA LDATA) (gensem wrmsr_spec) wrmsr_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
functional inversion H2.
∃ ι, ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX:: IR EDX:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))
#PC <- (rs2#RA) #EAX <- Vzero).
inv_val_inject.
inv Hargs. inv H4.
inv EXTCALL_ARG. inv H12. inv H14. inv H13. inv H7.
destruct v0; destruct v; inv H9.
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- econstructor. eassumption.
econstructor. eassumption.
econstructor. eassumption.
constructor.
- simpl. inv match_related. split; congruence.
- match goal with
| |- val_inject _ _ ?r ⇒
change r with Vzero
end.
rewrite <- (Int.repr_unsigned z). rewrite <- H0.
constructor.
- intros.
destruct r; simpl; try constructor; elim H4; eauto 13.
Qed.
Lemma vmcs_get_revid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_get_revid_spec)
vmcs_get_revid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
assert (HP: revid = z).
{
functional inversion H2; subst.
rewrite H12 in H0. inv H0.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto.
econstructor; eauto.
simpl. lift_unfold. rewrite Z.add_0_r. rewrite <- H; eauto.
Qed.
Lemma vmcs_get_abrtid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_get_abrtid_spec)
vmcs_get_abrtid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
assert (HP: abrtid = z).
{
functional inversion H2; subst.
rewrite H12 in H0. inv H0.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
refine_split´; repeat val_inject_inv; eauto.
econstructor; eauto.
simpl. lift_unfold. rewrite <- H; eauto.
Qed.
Lemma vmcs_set_revid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_set_revid_spec)
vmcs_set_revid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
inv H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) H4); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H8.
rename H into CPU_ID_eq.
refine_split.
- econstructor; eauto.
lift_unfold. rewrite Z.add_0_r. rewrite <- CPU_ID_eq. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H12 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (H2 _ H).
destruct H2 as (v & HLD & HV & HVV).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right; right; omega.
+ exploit Mem.load_store_same; eauto.
simpl.
rewrite Int.repr_unsigned. trivial.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H5; eauto.
simpl; right; right; omega.
- apply inject_incr_refl.
Qed.
Lemma vmcs_set_abrtid_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmcs_set_abrtid_spec)
vmcs_set_abrtid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
inv H.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) H6); intros [m´ HST].
refine_split.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H8. rename H into CPU_ID_eq.
- econstructor; eauto.
lift_unfold. rewrite <- CPU_ID_eq. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
rewrite H12 in H0. inv H0.
rewrite ZMap.gss.
econstructor; eauto; intros;
try eapply Mem.store_valid_access_1; eauto.
+ specialize (H2 _ H).
destruct H2 as (v & HLD & HV & HVV).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HLD; eauto.
simpl; right; right; omega.
+ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in H3; eauto.
simpl; right; left; omega.
+ exploit Mem.load_store_same; eauto.
simpl.
rewrite Int.repr_unsigned. trivial.
- apply inject_incr_refl.
Qed.
End WITHMEM.
End Refinement.