Library mcertikos.proc.VMXIntroGenFresh
This file provide the contextual refinement proof between VMCSInit layer and PVMXIntro 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}.
Lemma val_inject_reg:
∀ (rs1 rs2: regset) ι,
(∀ reg,
val_inject ι (Pregmap.get reg rs1) (Pregmap.get reg rs2)) →
∀ rd,
val_inject ι (Val.load_result Mint32 (rs1 rd))
(Val.load_result Mint32 (rs2 rd)).
Proof.
intros. specialize (H rd).
unfold Pregmap.get in ×.
destruct (rs1 rd); inv H;
try econstructor; eauto.
Qed.
Lemma vmx_exit_spec_ref:
compatsim (crel HDATA LDATA) (primcall_vmx_exit_compatsem vmx_exit_spec get_CPU_ID_spec)
vmx_exit_spec_low.
Proof.
compatsim_simpl (@match_AbData).
unfold vmx_exit_spec in ×.
subdestruct; inv H4.
inv match_extcall_states.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv match_match.
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RDI´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_G_RAX´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_G_RBX´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_G_RDX´ < VMX_Size´) by omega.
assert (HOS5: 0 ≤ VMX_G_RSI´ < VMX_Size´) by omega.
assert (HOS6: 0 ≤ VMX_G_RBP´ < VMX_Size´) by omega.
assert (HOS7: 0 ≤ VMX_HOST_EBP´ < VMX_Size´) by omega.
assert (HOS8: 0 ≤ VMX_HOST_EDI´ < VMX_Size´) by omega.
destruct (HMem _ HOS1) as (_ & _ & HV1 & _).
destruct (HMem _ HOS2) as (_ & _ & HV2 & _).
destruct (HMem _ HOS3) as (_ & _ & HV3 & _).
destruct (HMem _ HOS4) as (_ & _ & HV4 & _).
destruct (HMem _ HOS5) as (_ & _ & HV5 & _).
destruct (HMem _ HOS6) as (_ & _ & HV6 & _).
destruct (HMem _ HOS7) as (v7 & HL7 & _ & HM7).
destruct (HMem _ HOS8) as (v8 & HL8 & _ & HM8).
set (rs02 := ((((((Pregmap.init Vundef) # EAX <- (rs2 EAX)) # EBX <- (rs2 EBX))
# EDX <- (rs2 EDX)) # EDI <- (rs2 EDI)) # ESI <- (rs2 ESI)) # EBP <- (rs2 EBP)).
assert (HVAL_INJECT:
∀ reg,
val_inject ι (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
{
subst rs01 rs02.
val_inject_simpl.
}
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDI) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EAX) HV2); intros [m20 HST20].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBX) HV3); intros [m30 HST30].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDX) HV4); intros [m40 HST40].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST40) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST40) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 ESI) HV5); intros [m50 HST50].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST50) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBP) HV6); intros [m60 HST60].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST10) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST20) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST30) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST40) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST50) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST60) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H2. rename H into CPU_ID_eq.
generalize (match_reg ECX); intro MECX.
unfold get_CPU_ID_spec in cpuidVal.
unfold ObjMultiprocessor.get_CPU_ID_spec in cpuidVal.
rewrite Hdestruct, Hdestruct0 in cpuidVal.
inv cpuidVal.
assert(ECXVal: rs2 ECX = Vint (Int.repr (CPU_ID d1 × (38 × 4)))).
{
unfold Pregmap.get in MECX.
rewrite HECXVal in MECX.
destruct (rs2 ECX); try inv MECX.
reflexivity.
}
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; eauto.
specialize (match_reg PC).
unfold Pregmap.get in ×.
rewrite HPC in match_reg. inv match_reg.
clear H1.
exploit stencil_find_symbol_inject´; eauto.
rewrite H3. intros HF.
inv HF. rewrite Int.add_zero. trivial.
- econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 12); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gss.
rewrite ZMap.gso; [| assumption].
destruct (zeq i 8); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 6); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 2); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 0); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 10); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
{
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 10); [left; omega|right; omega].
simpl; right. destruct (zlt i 0); [left; omega|right; omega].
simpl; right. destruct (zlt i 2); [left; omega|right; omega].
simpl; right. destruct (zlt i 6); [left; omega|right; omega].
simpl; right. destruct (zlt i 8); [left; omega|right; omega].
simpl; right. destruct (zlt i 12); [left; omega|right; omega].
}
+ intros.
assert (HINJ: ∀ n1 v,
val_inject ι (Val.load_result Mint32 (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1)))) v →
Val.has_type (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) AST.Tint →
val_inject ι (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) v).
{
intros.
destruct (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))); inv H; inv H0; try econstructor; eauto.
}
subst rs0.
repeat simpl_Pregmap; eauto.
val_inject_simpl; eauto 2; try eapply HINJ; eauto 2.
generalize (N_TYPE RA).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBP).
repeat simpl_Pregmap; eauto.
Qed.
Lemma vmx_enter_spec_ref:
compatsim (crel HDATA LDATA) (primcall_vmx_enter_compatsem vmx_enter_spec vmx_enter)
vmx_enter_spec_low.
Proof.
compatsim_simpl (@match_AbData).
unfold vmx_enter_spec in ×.
subdestruct; inv H4.
repeat simpl_Pregmap; eauto.
inv match_extcall_states.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv match_match.
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RDI´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_G_RAX´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_G_RBX´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_G_RDX´ < VMX_Size´) by omega.
assert (HOS5: 0 ≤ VMX_G_RSI´ < VMX_Size´) by omega.
assert (HOS6: 0 ≤ VMX_G_RBP´ < VMX_Size´) by omega.
assert (HOS7: 0 ≤ VMX_HOST_EBP´ < VMX_Size´) by omega.
assert (HOS8: 0 ≤ VMX_HOST_EDI´ < VMX_Size´) by omega.
assert (HOS9: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
destruct (HMem _ HOS7) as (_ & _ & HV1 & _).
destruct (HMem _ HOS8) as (_ & _ & HV2 & _).
destruct (HMem _ HOS2) as (v3 & HL3 & _ & HM3).
destruct (HMem _ HOS3) as (v4 & HL4 & _ & HM4).
destruct (HMem _ HOS4) as (v5 & HL5 & _ & HM5).
destruct (HMem _ HOS5) as (v6 & HL6 & _ & HM6).
destruct (HMem _ HOS1) as (v7 & HL7 & _ & HM7).
destruct (HMem _ HOS6) as (v8 & HL8 & _ & HM8).
destruct (HMem _ HOS9) as (v9 & HL9 & _ & HM9).
set (rs02 := ((Pregmap.init Vundef) # EDI <- (rs2 EDI)) # EBP <- (rs2 EBP)).
assert (HVAL_INJECT:
∀ reg,
val_inject ι (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
{
subst rs01 rs02.
val_inject_simpl.
}
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBP) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDI) HV2); intros [m20 HST20].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST10) in HL3, HL4, HL5, HL6, HL7, HL8, HL9 ; eauto;
try (simpl; right; left; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST20) in HL3, HL4, HL5, HL6, HL7, HL8, HL9 ; eauto;
try (simpl; right; left; omega).
assert (HHost: hostout_spec d1 = Some d1 {ihost: false}).
{
unfold hostout_spec.
unfold ObjCPU.hostout_spec.
inv match_related.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
trivial.
}
exploit hostout_exist; eauto.
intros (labd´ & HP & HR).
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; eauto.
specialize (match_reg PC).
unfold Pregmap.get in ×.
rewrite HPC in match_reg. inv match_reg.
clear H1.
exploit stencil_find_symbol_inject´; eauto.
rewrite H3. intros HF.
inv HF. rewrite Int.add_zero. trivial.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv ASM_INV.
inv inv_inject_neutral.
inv match_reg; try congruence.
intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
rewrite H in H2.
inv H2.
split.
× eapply match_inject_forward in H3; eauto.
destruct H3.
rewrite H2 in H.
unfold Int.add in H.
change (Int.unsigned (Int.repr 0)) with 0 in H.
rewrite Z.add_0_r in H.
rewrite Int.repr_unsigned in H.
destruct HESP_STACK.
generalize H4, H3.
clear.
intros.
apply Ple_trans with b2; eauto.
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
- econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 34); subst.
{
repeat rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gss.
rewrite ZMap.gso; [| assumption].
destruct (zeq i 33); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
specialize (HMem _ H).
destruct HMem as (v & HLD & HVA & HInj).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 33); [left; omega|right; omega].
simpl; right. destruct (zlt i 34); [left; omega|right; omega].
+ intros.
assert (HINJ: ∀ n1 v,
val_inject ι (Val.load_result Mint32 (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1)))) v →
Val.has_type (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) AST.Tint →
val_inject ι (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) v).
{
intros.
destruct (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))); inv H; inv H0; try econstructor; eauto.
}
subst rs0.
val_inject_simpl; try eapply HINJ; eauto 2.
generalize (N_TYPE RA).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBP).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE ESI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDX).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBX).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EAX).
repeat simpl_Pregmap; eauto.
Qed.
Lemma vmx_enter_pre_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_enter_pre_spec)
vmx_enter_pre_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
pose proof H as HMM. inv H.
pose proof H0 as HMem.
assert (HOS: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
specialize (H0 _ HOS). destruct H0 as (v1 & HL1 & _ & HM).
simpl in HL1.
functional inversion H1. rewrite H8 in HM.
inv HM.
assert (HP: vmcs_writez_spec C_VMCS_GUEST_RIP (Int.unsigned v) d1 = Some d1 {vmcs : ZMap.set (CPU_ID d1) (VMCSValid revid abrtid d´) (vmcs d1)}).
{
unfold vmcs_writez_spec. subrewrite´.
simpl. rewrite Int.repr_unsigned.
reflexivity.
}
exploit vmcs_writez_exist; eauto.
intros (labd´ & HP´ & HR´).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
rewrite <- CPU_ID_eq; auto.
constructor; eauto.
Qed.
Lemma vmx_exit_post_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_exit_post_spec)
vmx_exit_post_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1; subst.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_EXIT_REASON´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_EXIT_QUALIFICATION´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_LAUNCHED´ < VMX_Size´) by omega.
destruct (HMem _ HOS1) as (_ & _ & HV1 & _).
destruct (HMem _ HOS2) as (_ & _ & HV2 & _).
destruct (HMem _ HOS3) as (_ & _ & HV3 & _).
destruct (HMem _ HOS4) as (_ & _ & HV4 & _).
specialize (Mem.valid_access_store _ _ _ _ (Vint v1) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint v2) HV2); intros [m20 HST20].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint v3) HV3); intros [m30 HST30].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV4.
specialize (Mem.valid_access_store _ _ _ _ Vone HV4); intros [m40 HST40].
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
specialize (vmcs_re _ _ _ match_related (CPU_ID d1) (ZMap.get (CPU_ID d1) (vmcs d1)) (ZMap.get (CPU_ID d1) (vmcs d2)) _x refl_equal refl_equal).
intro vmcs_inj.
inv vmcs_inj.
rewrite H6 in H; inv H.
refine_split.
- inv match_related.
assert (HK: ikern d2 = true ∧ pg d2 = true ∧ ihost d2 = true).
{
refine_split´; try congruence.
}
destruct HK as (Hik & Hip & Hih).
econstructor; try rewrite <- CPU_ID_eq; eauto.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 26654).
rewrite H7 in H12. inv H12.
trivial.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 17410).
rewrite H8 in H12. inv H12.
trivial.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 25600).
rewrite H9 in H12. inv H12.
trivial.
- constructor.
- pose proof H1 as Hspec.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 31); subst.
{
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst vvmx4 vvmx3 vvmx2 vvmx1.
repeat rewrite ZMap.gss.
constructor.
}
destruct (zeq i 28); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
destruct (zeq i 27); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
destruct (zeq i 14); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
simpl. right; left; omega.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
{
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 14); [left; omega|right; omega].
simpl; right. destruct (zlt i 27); [left; omega|right; omega].
simpl; right. destruct (zlt i 28); [left; omega|right; omega].
simpl; right. destruct (zlt i 31); [left; omega|right; omega].
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
repeat rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma vmx_readz_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_readz_spec)
vmx_readz_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2
∧ 0≤ Int.unsigned i < VMX_Size´).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HMem.
specialize (H0 _ HOS). destruct H0 as (v1 & HL1 & _ & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
rewrite H7 in HM. inv HM.
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;
try econstructor; eauto.
Opaque Z.mul.
simpl. lift_unfold. rewrite <- H; auto.
Qed.
Lemma vmx_writez_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_writez_spec)
vmx_writez_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ 0≤ Int.unsigned i < VMX_Size´).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
inv H. rename H0 into HMem.
destruct (HMem _ HOS) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; 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.
econstructor; eauto; intros.
destruct (zeq i1 (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
+
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt i1 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gss.
rewrite ZMap.gso; 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}.
Lemma val_inject_reg:
∀ (rs1 rs2: regset) ι,
(∀ reg,
val_inject ι (Pregmap.get reg rs1) (Pregmap.get reg rs2)) →
∀ rd,
val_inject ι (Val.load_result Mint32 (rs1 rd))
(Val.load_result Mint32 (rs2 rd)).
Proof.
intros. specialize (H rd).
unfold Pregmap.get in ×.
destruct (rs1 rd); inv H;
try econstructor; eauto.
Qed.
Lemma vmx_exit_spec_ref:
compatsim (crel HDATA LDATA) (primcall_vmx_exit_compatsem vmx_exit_spec get_CPU_ID_spec)
vmx_exit_spec_low.
Proof.
compatsim_simpl (@match_AbData).
unfold vmx_exit_spec in ×.
subdestruct; inv H4.
inv match_extcall_states.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv match_match.
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RDI´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_G_RAX´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_G_RBX´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_G_RDX´ < VMX_Size´) by omega.
assert (HOS5: 0 ≤ VMX_G_RSI´ < VMX_Size´) by omega.
assert (HOS6: 0 ≤ VMX_G_RBP´ < VMX_Size´) by omega.
assert (HOS7: 0 ≤ VMX_HOST_EBP´ < VMX_Size´) by omega.
assert (HOS8: 0 ≤ VMX_HOST_EDI´ < VMX_Size´) by omega.
destruct (HMem _ HOS1) as (_ & _ & HV1 & _).
destruct (HMem _ HOS2) as (_ & _ & HV2 & _).
destruct (HMem _ HOS3) as (_ & _ & HV3 & _).
destruct (HMem _ HOS4) as (_ & _ & HV4 & _).
destruct (HMem _ HOS5) as (_ & _ & HV5 & _).
destruct (HMem _ HOS6) as (_ & _ & HV6 & _).
destruct (HMem _ HOS7) as (v7 & HL7 & _ & HM7).
destruct (HMem _ HOS8) as (v8 & HL8 & _ & HM8).
set (rs02 := ((((((Pregmap.init Vundef) # EAX <- (rs2 EAX)) # EBX <- (rs2 EBX))
# EDX <- (rs2 EDX)) # EDI <- (rs2 EDI)) # ESI <- (rs2 ESI)) # EBP <- (rs2 EBP)).
assert (HVAL_INJECT:
∀ reg,
val_inject ι (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
{
subst rs01 rs02.
val_inject_simpl.
}
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDI) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EAX) HV2); intros [m20 HST20].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBX) HV3); intros [m30 HST30].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDX) HV4); intros [m40 HST40].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST40) in HV5.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST40) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 ESI) HV5); intros [m50 HST50].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST50) in HV6.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBP) HV6); intros [m60 HST60].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST10) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST20) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST30) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST40) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST50) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST60) in HL7, HL8 ; eauto;
try (simpl; right; right; omega).
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
clear H2. rename H into CPU_ID_eq.
generalize (match_reg ECX); intro MECX.
unfold get_CPU_ID_spec in cpuidVal.
unfold ObjMultiprocessor.get_CPU_ID_spec in cpuidVal.
rewrite Hdestruct, Hdestruct0 in cpuidVal.
inv cpuidVal.
assert(ECXVal: rs2 ECX = Vint (Int.repr (CPU_ID d1 × (38 × 4)))).
{
unfold Pregmap.get in MECX.
rewrite HECXVal in MECX.
destruct (rs2 ECX); try inv MECX.
reflexivity.
}
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; eauto.
specialize (match_reg PC).
unfold Pregmap.get in ×.
rewrite HPC in match_reg. inv match_reg.
clear H1.
exploit stencil_find_symbol_inject´; eauto.
rewrite H3. intros HF.
inv HF. rewrite Int.add_zero. trivial.
- econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 12); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
rewrite ZMap.gss.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gss.
rewrite ZMap.gso; [| assumption].
destruct (zeq i 8); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 6); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 2); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 0); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
destruct (zeq i 10); subst.
{
rewrite ZMap.gss.
refine_split´; eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; right; omega.
simpl; right; left; omega.
repeat (eapply Mem.store_valid_access_1; eauto).
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
{
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST60); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST50); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 10); [left; omega|right; omega].
simpl; right. destruct (zlt i 0); [left; omega|right; omega].
simpl; right. destruct (zlt i 2); [left; omega|right; omega].
simpl; right. destruct (zlt i 6); [left; omega|right; omega].
simpl; right. destruct (zlt i 8); [left; omega|right; omega].
simpl; right. destruct (zlt i 12); [left; omega|right; omega].
}
+ intros.
assert (HINJ: ∀ n1 v,
val_inject ι (Val.load_result Mint32 (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1)))) v →
Val.has_type (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) AST.Tint →
val_inject ι (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) v).
{
intros.
destruct (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))); inv H; inv H0; try econstructor; eauto.
}
subst rs0.
repeat simpl_Pregmap; eauto.
val_inject_simpl; eauto 2; try eapply HINJ; eauto 2.
generalize (N_TYPE RA).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBP).
repeat simpl_Pregmap; eauto.
Qed.
Lemma vmx_enter_spec_ref:
compatsim (crel HDATA LDATA) (primcall_vmx_enter_compatsem vmx_enter_spec vmx_enter)
vmx_enter_spec_low.
Proof.
compatsim_simpl (@match_AbData).
unfold vmx_enter_spec in ×.
subdestruct; inv H4.
repeat simpl_Pregmap; eauto.
inv match_extcall_states.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv match_match.
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RDI´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_G_RAX´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_G_RBX´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_G_RDX´ < VMX_Size´) by omega.
assert (HOS5: 0 ≤ VMX_G_RSI´ < VMX_Size´) by omega.
assert (HOS6: 0 ≤ VMX_G_RBP´ < VMX_Size´) by omega.
assert (HOS7: 0 ≤ VMX_HOST_EBP´ < VMX_Size´) by omega.
assert (HOS8: 0 ≤ VMX_HOST_EDI´ < VMX_Size´) by omega.
assert (HOS9: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
destruct (HMem _ HOS7) as (_ & _ & HV1 & _).
destruct (HMem _ HOS8) as (_ & _ & HV2 & _).
destruct (HMem _ HOS2) as (v3 & HL3 & _ & HM3).
destruct (HMem _ HOS3) as (v4 & HL4 & _ & HM4).
destruct (HMem _ HOS4) as (v5 & HL5 & _ & HM5).
destruct (HMem _ HOS5) as (v6 & HL6 & _ & HM6).
destruct (HMem _ HOS1) as (v7 & HL7 & _ & HM7).
destruct (HMem _ HOS6) as (v8 & HL8 & _ & HM8).
destruct (HMem _ HOS9) as (v9 & HL9 & _ & HM9).
set (rs02 := ((Pregmap.init Vundef) # EDI <- (rs2 EDI)) # EBP <- (rs2 EBP)).
assert (HVAL_INJECT:
∀ reg,
val_inject ι (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
{
subst rs01 rs02.
val_inject_simpl.
}
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EBP) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
specialize (Mem.valid_access_store _ _ _ _ (rs02 EDI) HV2); intros [m20 HST20].
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST10) in HL3, HL4, HL5, HL6, HL7, HL8, HL9 ; eauto;
try (simpl; right; left; omega).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST20) in HL3, HL4, HL5, HL6, HL7, HL8, HL9 ; eauto;
try (simpl; right; left; omega).
assert (HHost: hostout_spec d1 = Some d1 {ihost: false}).
{
unfold hostout_spec.
unfold ObjCPU.hostout_spec.
inv match_related.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
trivial.
}
exploit hostout_exist; eauto.
intros (labd´ & HP & HR).
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; eauto.
specialize (match_reg PC).
unfold Pregmap.get in ×.
rewrite HPC in match_reg. inv match_reg.
clear H1.
exploit stencil_find_symbol_inject´; eauto.
rewrite H3. intros HF.
inv HF. rewrite Int.add_zero. trivial.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv ASM_INV.
inv inv_inject_neutral.
inv match_reg; try congruence.
intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
rewrite H in H2.
inv H2.
split.
× eapply match_inject_forward in H3; eauto.
destruct H3.
rewrite H2 in H.
unfold Int.add in H.
change (Int.unsigned (Int.repr 0)) with 0 in H.
rewrite Z.add_0_r in H.
rewrite Int.repr_unsigned in H.
destruct HESP_STACK.
generalize H4, H3.
clear.
intros.
apply Ple_trans with b2; eauto.
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
- econstructor; eauto.
+ split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 34); subst.
{
repeat rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
eapply Mem.load_store_same; eauto.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gss.
rewrite ZMap.gso; [| assumption].
destruct (zeq i 33); subst.
{
rewrite ZMap.gss.
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl; right; left; omega.
eapply val_inject_reg; eauto.
}
rewrite ZMap.gso; [| assumption].
specialize (HMem _ H).
destruct HMem as (v & HLD & HVA & HInj).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 33); [left; omega|right; omega].
simpl; right. destruct (zlt i 34); [left; omega|right; omega].
+ intros.
assert (HINJ: ∀ n1 v,
val_inject ι (Val.load_result Mint32 (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1)))) v →
Val.has_type (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) AST.Tint →
val_inject ι (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))) v).
{
intros.
destruct (ZMap.get n1 (ZMap.get (CPU_ID d1) (vmx d1))); inv H; inv H0; try econstructor; eauto.
}
subst rs0.
val_inject_simpl; try eapply HINJ; eauto 2.
generalize (N_TYPE RA).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBP).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE ESI).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EDX).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EBX).
repeat simpl_Pregmap; eauto.
generalize (N_TYPE EAX).
repeat simpl_Pregmap; eauto.
Qed.
Lemma vmx_enter_pre_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_enter_pre_spec)
vmx_enter_pre_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
pose proof H as HMM. inv H.
pose proof H0 as HMem.
assert (HOS: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
specialize (H0 _ HOS). destruct H0 as (v1 & HL1 & _ & HM).
simpl in HL1.
functional inversion H1. rewrite H8 in HM.
inv HM.
assert (HP: vmcs_writez_spec C_VMCS_GUEST_RIP (Int.unsigned v) d1 = Some d1 {vmcs : ZMap.set (CPU_ID d1) (VMCSValid revid abrtid d´) (vmcs d1)}).
{
unfold vmcs_writez_spec. subrewrite´.
simpl. rewrite Int.repr_unsigned.
reflexivity.
}
exploit vmcs_writez_exist; eauto.
intros (labd´ & HP´ & HR´).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
rewrite <- CPU_ID_eq; auto.
constructor; eauto.
Qed.
Lemma vmx_exit_post_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_exit_post_spec)
vmx_exit_post_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1; subst.
assert(Hkern: kernel_mode d2).
{
simpl; inv match_related.
refine_split´; trivial; try congruence.
}
inv H. rename H0 into HMem.
assert (HOS1: 0 ≤ VMX_G_RIP´ < VMX_Size´) by omega.
assert (HOS2: 0 ≤ VMX_EXIT_REASON´ < VMX_Size´) by omega.
assert (HOS3: 0 ≤ VMX_EXIT_QUALIFICATION´ < VMX_Size´) by omega.
assert (HOS4: 0 ≤ VMX_LAUNCHED´ < VMX_Size´) by omega.
destruct (HMem _ HOS1) as (_ & _ & HV1 & _).
destruct (HMem _ HOS2) as (_ & _ & HV2 & _).
destruct (HMem _ HOS3) as (_ & _ & HV3 & _).
destruct (HMem _ HOS4) as (_ & _ & HV4 & _).
specialize (Mem.valid_access_store _ _ _ _ (Vint v1) HV1); intros [m10 HST10].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST10) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint v2) HV2); intros [m20 HST20].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST20) in HV4.
specialize (Mem.valid_access_store _ _ _ _ (Vint v3) HV3); intros [m30 HST30].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST30) in HV4.
specialize (Mem.valid_access_store _ _ _ _ Vone HV4); intros [m40 HST40].
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
specialize (vmcs_re _ _ _ match_related (CPU_ID d1) (ZMap.get (CPU_ID d1) (vmcs d1)) (ZMap.get (CPU_ID d1) (vmcs d2)) _x refl_equal refl_equal).
intro vmcs_inj.
inv vmcs_inj.
rewrite H6 in H; inv H.
refine_split.
- inv match_related.
assert (HK: ikern d2 = true ∧ pg d2 = true ∧ ihost d2 = true).
{
refine_split´; try congruence.
}
destruct HK as (Hik & Hip & Hih).
econstructor; try rewrite <- CPU_ID_eq; eauto.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 26654).
rewrite H7 in H12. inv H12.
trivial.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 17410).
rewrite H8 in H12. inv H12.
trivial.
+ unfold vmcs_readz_spec;
repeat rewrite <- CPU_ID_eq;
clear CPU_ID_eq CPU_ID_re.
subrewrite´. rewrite <- H11. simpl.
specialize (H12 25600).
rewrite H9 in H12. inv H12.
trivial.
- constructor.
- pose proof H1 as Hspec.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i 31); subst.
{
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst vvmx4 vvmx3 vvmx2 vvmx1.
repeat rewrite ZMap.gss.
constructor.
}
destruct (zeq i 28); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
destruct (zeq i 27); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
destruct (zeq i 14); subst.
{
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
eapply Mem.load_store_same; eauto.
simpl. right; left; omega.
simpl. right; left; omega.
simpl. right; left; omega.
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gso; [|discriminate].
rewrite ZMap.gss.
constructor.
}
{
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
repeat (eapply Mem.store_valid_access_1; eauto).
rewrite (Mem.load_store_other _ _ _ _ _ _ HST40); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST30); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST20); eauto.
rewrite (Mem.load_store_other _ _ _ _ _ _ HST10); eauto.
simpl; right. destruct (zlt i 14); [left; omega|right; omega].
simpl; right. destruct (zlt i 27); [left; omega|right; omega].
simpl; right. destruct (zlt i 28); [left; omega|right; omega].
simpl; right. destruct (zlt i 31); [left; omega|right; omega].
subst vvmx4 vvmx3 vvmx2 vvmx1.
rewrite ZMap.gss.
repeat rewrite ZMap.gso; trivial.
}
- apply inject_incr_refl.
Qed.
Lemma vmx_readz_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_readz_spec)
vmx_readz_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2
∧ 0≤ Int.unsigned i < VMX_Size´).
{
simpl; inv match_related.
functional inversion H2.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HMem.
specialize (H0 _ HOS). destruct H0 as (v1 & HL1 & _ & HM).
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
rewrite H7 in HM. inv HM.
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;
try econstructor; eauto.
Opaque Z.mul.
simpl. lift_unfold. rewrite <- H; auto.
Qed.
Lemma vmx_writez_spec_ref:
compatsim (crel HDATA LDATA) (gensem vmx_writez_spec)
vmx_writez_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2
∧ 0≤ Int.unsigned i < VMX_Size´).
{
simpl; inv match_related.
functional inversion H1.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
inv H. rename H0 into HMem.
destruct (HMem _ HOS) as (v1 & HL1 & HV1 & HM).
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m´ HST].
exploit relate_impl_CPU_ID_eq; eauto; simpl; intro CPU_ID_eq.
refine_split.
- econstructor; try rewrite <- CPU_ID_eq; 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.
econstructor; eauto; intros.
destruct (zeq i1 (Int.unsigned i)); subst.
+
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
+
specialize (HMem _ H).
destruct HMem as (v1´ & HL1´ & HV1´ & HM´).
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
simpl; right. destruct (zlt i1 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gss.
rewrite ZMap.gso; trivial.
- apply inject_incr_refl.
Qed.
End WITHMEM.
End Refinement.