Library mcertikos.proc.UCtxtIntroGenFresh
This file provide the contextual refinement proof between PIPC layer and PUCtxtIntro layer
Require Import UCtxtIntroGenDef.
Require Import UCtxtIntroGenSpec.
Require Import PUCtxtIntroDef.
Require Import ObjProc.
Require Import GlobalOracleProp.
Section Refinement.
Context `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Lemma elf_load_spec_ref:
compatsim (crel HDATA LDATA) elf_load_compatsem elf_load_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
inv H.
∃ ι, (rs2#RA<- Vundef#Asm.PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv H0.
unfold sextcall_sig in ×.
unfold csig_sig in ×.
simpl in EXTCALL_ARG.
unfold signature_of_type in ×.
simpl in EXTCALL_ARG.
inv EXTCALL_ARG.
econstructor. eassumption. inv H7. inv H5.
econstructor. rewrite Z.add_0_l. eassumption.
constructor.
- intros. inv ASM_INV.
inv inv_inject_neutral.
destruct r; simpl;
repeat simpl_Pregmap; eauto.
Qed.
Lemma uctx_get_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_get_spec)
uctx_get_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc
∧ 0≤ Int.unsigned i0 < UCTXT_SIZE
∧ is_UCTXT_ptr (Int.unsigned i0) = false).
{
simpl; inv match_related.
functional inversion H2.
pose proof H8 as Hfalse.
apply is_UCTXT_ptr_range in H8.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern [HOS [HOS´ Hfalse]]].
pose proof H0 as HMem.
specialize (H0 _ _ HOS HOS´). destruct H0 as [v1[HL1[_[_ HM]]]].
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
unfold UContext in H8.
rewrite H8 in HM. inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
Qed.
Lemma uctx_set_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_spec)
uctx_set_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc
∧ 0≤ Int.unsigned i0 < UCTXT_SIZE
∧ is_UCTXT_ptr (Int.unsigned i0) = false).
{
simpl; inv match_related.
functional inversion H1.
pose proof H7 as Hfalse.
apply is_UCTXT_ptr_range in H7.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern [HOS [HOS´ Hfalse]]].
inv H. rename H0 into HMem.
destruct (HMem _ _ HOS HOS´) as [v1[HL1[HV1[_ HM]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i1) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
lift_unfold. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
subst uctx.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i2 (Int.unsigned i)); subst.
+
destruct (zeq n (Int.unsigned i0)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst uctx´.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
×
specialize (HMem _ _ H H8).
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 n (Int.unsigned i0)); [left; omega|right; omega].
rewrite ZMap.gss. subst uctx´.
rewrite ZMap.gso; trivial.
+
specialize (HMem _ _ H H8).
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 i2 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
- apply inject_incr_refl.
Qed.
Lemma uctx_set_eip_spec_ref:
compatsim (crel HDATA LDATA) (uctx_set_eip_compatsem uctx_set_eip_spec)
uctx_set_eip_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H5.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
inv H. rename H0 into HMem.
assert (HOS´: 0≤ U_EIP < UCTXT_SIZE) by omega.
destruct (HMem _ _ HOS HOS´) as [v1[HL1[HV1[_ HM]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vptr b ofs) HV1); intros [m´ HST].
assert(HFB: ι b = Some (b, 0)).
{
destruct H7 as [fun_id Hsymbol].
eapply stencil_find_symbol_inject´; eauto.
}
refine_split.
- econstructor; eauto.
lift_unfold. split; eauto.
- constructor.
- pose proof H5 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
subst uctx.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (Int.unsigned i)); subst.
+
destruct (zeq n U_EIP); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst uctx´.
repeat rewrite ZMap.gss.
econstructor; eauto.
rewrite Int.add_zero; trivial.
×
specialize (HMem _ _ H H8).
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 n U_EIP); [left; omega|right; omega].
rewrite ZMap.gss. subst uctx´.
rewrite ZMap.gso; trivial.
+
specialize (HMem _ _ H H8).
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 i0 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
- apply inject_incr_refl.
Qed.
Lemma restore_uctx_spec_ref:
compatsim (crel HDATA LDATA)
(primcall_restoreuctx_compatsem restore_uctx_spec (fun abd ⇒ ZMap.get (CPU_ID abd) (cid abd)))
restore_uctx_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
assert(HP: ∃ d´, trapout_spec d2 = Some d´
∧ relate_RData ι d1´ d´
∧ uctxt d1´ = uctxt d1
∧ (ZMap.get (CPU_ID d1) (cid d1)) = (ZMap.get (CPU_ID d2) (cid d2))
∧ 0≤ (ZMap.get (CPU_ID d2) (cid d2)) < num_proc
∧ kernel_mode d2
∧ rs´ = ZMap.get (ZMap.get (CPU_ID d1) (cid d1)) (uctxt d1)).
{
simpl; inv match_related.
unfold trapout_spec.
inv Hlow.
pose proof (valid_curid _ Hhigh) as Hcid.
subrewrite´.
functional inversion H7; subst; simpl.
rewrite <- ikern_re, <- init_re, <- pg_re, <- ihost_re, <- ipt_re.
subrewrite´.
refine_split´; trivial; try congruence.
econstructor; eauto.
subst. subst curid. rewrite H11. trivial.
}
destruct HP as [d´[Htrapout[HR[HUctx[HCid [HOS [Hkern Hrs´]]]]]]].
inv match_match. inv H.
set (vcid := (ZMap.get (CPU_ID d1) (cid d1))) in ×.
assert (HV0: ∀ n0, 0≤ n0 < UCTXT_SIZE →
Mem.valid_access m2 Mint32 b0 (vcid × UCTXT_SIZE × 4 + n0 × 4) Readable).
{
intros. specialize (H0 _ _ HOS H).
destruct H0 as [_[_ [HV _]]]. subst vcid.
rewrite HCid. eapply Mem.valid_access_implies; eauto.
constructor.
}
assert (HP: ∃ v0, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EDI × 4) = Some v0).
{
eapply Mem.valid_access_load; eauto.
}
destruct HP as [v0 HLD0].
assert (HP: ∃ v1, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ESI × 4) = Some v1).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v1 HLD1].
assert (HP: ∃ v2, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EBP × 4) = Some v2).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v3 HLD3].
assert (HP: ∃ v4, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EBX × 4) = Some v4).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v4 HLD4].
assert (HP: ∃ v5, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EDX × 4) = Some v5).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v5 HLD5].
assert (HP: ∃ v6, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ECX × 4) = Some v6).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v6 HLD6].
assert (HP: ∃ v7, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EAX × 4) = Some v7).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v7 HLD7].
assert (HP: ∃ v8, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ESP × 4) = Some v8).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v8 HLD8].
assert (HP: ∃ v9, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EIP × 4) = Some v9).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v9 HLD9].
refine_split; eauto 2.
- subst vcid. rewrite HCid in ×.
replace ((ZMap.get (CPU_ID d2) (cid d2)) × 17 × 4 + 0 × 4) with ((ZMap.get (CPU_ID d2) (cid d2)) × 17 × 4) by omega.
rewrite H11 in ×.
econstructor; eauto 2.
eapply reg_symbol_inject; eassumption.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
- econstructor; eauto.
+ econstructor; eauto.
econstructor; eauto.
rewrite HUctx.
econstructor; eauto.
+ assert (Hinj: ∀ n v, 0≤ n < UCTXT_SIZE →
Mem.load Mint32 m2 b0 (vcid × 17 × 4 + n × 4) = Some v →
val_inject ι (ZMap.get n (ZMap.get vcid (uctxt d1))) v).
{
intros. rewrite <- HCid in HOS.
specialize (H0 _ _ HOS H).
specialize (N_TYPE _ H).
destruct H0 as [v´[HL[_[_ Hinj]]]].
rewrite HL in H2. inv H2.
Transparent Val.load_result.
caseEq (ZMap.get n0 (ZMap.get ((ZMap.get (CPU_ID d1) (cid d1))) (uctxt d1))); intros;
unfold UContext in *; rewrite H0 in *; simpl in Hinj; try assumption;
inv N_TYPE.
}
val_inject_simpl; eapply Hinj; eauto 2; omega.
Qed.
End WITHMEM.
End Refinement.
Context `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Lemma elf_load_spec_ref:
compatsim (crel HDATA LDATA) elf_load_compatsem elf_load_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
inv H.
∃ ι, (rs2#RA<- Vundef#Asm.PC <- (rs2#RA)).
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
- inv_val_inject.
inv H0.
unfold sextcall_sig in ×.
unfold csig_sig in ×.
simpl in EXTCALL_ARG.
unfold signature_of_type in ×.
simpl in EXTCALL_ARG.
inv EXTCALL_ARG.
econstructor. eassumption. inv H7. inv H5.
econstructor. rewrite Z.add_0_l. eassumption.
constructor.
- intros. inv ASM_INV.
inv inv_inject_neutral.
destruct r; simpl;
repeat simpl_Pregmap; eauto.
Qed.
Lemma uctx_get_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_get_spec)
uctx_get_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc
∧ 0≤ Int.unsigned i0 < UCTXT_SIZE
∧ is_UCTXT_ptr (Int.unsigned i0) = false).
{
simpl; inv match_related.
functional inversion H2.
pose proof H8 as Hfalse.
apply is_UCTXT_ptr_range in H8.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern [HOS [HOS´ Hfalse]]].
pose proof H0 as HMem.
specialize (H0 _ _ HOS HOS´). destruct H0 as [v1[HL1[_[_ HM]]]].
assert (HP: v1 = Vint z).
{
functional inversion H2; subst.
unfold UContext in H8.
rewrite H8 in HM. inv HM.
rewrite <- Int.repr_unsigned with z; rewrite <- H.
rewrite Int.repr_unsigned. trivial.
}
refine_split´; repeat val_inject_inv; eauto;
try econstructor; eauto.
Qed.
Lemma uctx_set_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_spec)
uctx_set_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc
∧ 0≤ Int.unsigned i0 < UCTXT_SIZE
∧ is_UCTXT_ptr (Int.unsigned i0) = false).
{
simpl; inv match_related.
functional inversion H1.
pose proof H7 as Hfalse.
apply is_UCTXT_ptr_range in H7.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern [HOS [HOS´ Hfalse]]].
inv H. rename H0 into HMem.
destruct (HMem _ _ HOS HOS´) as [v1[HL1[HV1[_ HM]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i1) HV1); intros [m´ HST].
refine_split.
- econstructor; eauto.
lift_unfold. split; eauto.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
subst uctx.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i2 (Int.unsigned i)); subst.
+
destruct (zeq n (Int.unsigned i0)); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst uctx´.
repeat rewrite ZMap.gss.
rewrite Int.repr_unsigned.
constructor.
×
specialize (HMem _ _ H H8).
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 n (Int.unsigned i0)); [left; omega|right; omega].
rewrite ZMap.gss. subst uctx´.
rewrite ZMap.gso; trivial.
+
specialize (HMem _ _ H H8).
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 i2 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
- apply inject_incr_refl.
Qed.
Lemma uctx_set_eip_spec_ref:
compatsim (crel HDATA LDATA) (uctx_set_eip_compatsem uctx_set_eip_spec)
uctx_set_eip_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < num_proc).
{
simpl; inv match_related.
functional inversion H5.
refine_split´; trivial; try congruence.
}
destruct HOS as [Hkern HOS].
inv H. rename H0 into HMem.
assert (HOS´: 0≤ U_EIP < UCTXT_SIZE) by omega.
destruct (HMem _ _ HOS HOS´) as [v1[HL1[HV1[_ HM]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vptr b ofs) HV1); intros [m´ HST].
assert(HFB: ι b = Some (b, 0)).
{
destruct H7 as [fun_id Hsymbol].
eapply stencil_find_symbol_inject´; eauto.
}
refine_split.
- econstructor; eauto.
lift_unfold. split; eauto.
- constructor.
- pose proof H5 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
subst uctx.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (Int.unsigned i)); subst.
+
destruct (zeq n U_EIP); subst.
×
refine_split´; eauto;
try eapply Mem.store_valid_access_1; eauto.
eapply Mem.load_store_same; eauto.
subst uctx´.
repeat rewrite ZMap.gss.
econstructor; eauto.
rewrite Int.add_zero; trivial.
×
specialize (HMem _ _ H H8).
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 n U_EIP); [left; omega|right; omega].
rewrite ZMap.gss. subst uctx´.
rewrite ZMap.gso; trivial.
+
specialize (HMem _ _ H H8).
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 i0 (Int.unsigned i)); [left; omega|right; omega].
rewrite ZMap.gso; trivial.
- apply inject_incr_refl.
Qed.
Lemma restore_uctx_spec_ref:
compatsim (crel HDATA LDATA)
(primcall_restoreuctx_compatsem restore_uctx_spec (fun abd ⇒ ZMap.get (CPU_ID abd) (cid abd)))
restore_uctx_spec_low.
Proof.
compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
assert(HP: ∃ d´, trapout_spec d2 = Some d´
∧ relate_RData ι d1´ d´
∧ uctxt d1´ = uctxt d1
∧ (ZMap.get (CPU_ID d1) (cid d1)) = (ZMap.get (CPU_ID d2) (cid d2))
∧ 0≤ (ZMap.get (CPU_ID d2) (cid d2)) < num_proc
∧ kernel_mode d2
∧ rs´ = ZMap.get (ZMap.get (CPU_ID d1) (cid d1)) (uctxt d1)).
{
simpl; inv match_related.
unfold trapout_spec.
inv Hlow.
pose proof (valid_curid _ Hhigh) as Hcid.
subrewrite´.
functional inversion H7; subst; simpl.
rewrite <- ikern_re, <- init_re, <- pg_re, <- ihost_re, <- ipt_re.
subrewrite´.
refine_split´; trivial; try congruence.
econstructor; eauto.
subst. subst curid. rewrite H11. trivial.
}
destruct HP as [d´[Htrapout[HR[HUctx[HCid [HOS [Hkern Hrs´]]]]]]].
inv match_match. inv H.
set (vcid := (ZMap.get (CPU_ID d1) (cid d1))) in ×.
assert (HV0: ∀ n0, 0≤ n0 < UCTXT_SIZE →
Mem.valid_access m2 Mint32 b0 (vcid × UCTXT_SIZE × 4 + n0 × 4) Readable).
{
intros. specialize (H0 _ _ HOS H).
destruct H0 as [_[_ [HV _]]]. subst vcid.
rewrite HCid. eapply Mem.valid_access_implies; eauto.
constructor.
}
assert (HP: ∃ v0, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EDI × 4) = Some v0).
{
eapply Mem.valid_access_load; eauto.
}
destruct HP as [v0 HLD0].
assert (HP: ∃ v1, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ESI × 4) = Some v1).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v1 HLD1].
assert (HP: ∃ v2, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EBP × 4) = Some v2).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v3 HLD3].
assert (HP: ∃ v4, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EBX × 4) = Some v4).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v4 HLD4].
assert (HP: ∃ v5, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EDX × 4) = Some v5).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v5 HLD5].
assert (HP: ∃ v6, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ECX × 4) = Some v6).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v6 HLD6].
assert (HP: ∃ v7, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EAX × 4) = Some v7).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v7 HLD7].
assert (HP: ∃ v8, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_ESP × 4) = Some v8).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v8 HLD8].
assert (HP: ∃ v9, Mem.load Mint32 m2 b0 (vcid × UCTXT_SIZE × 4 + U_EIP × 4) = Some v9).
{
eapply Mem.valid_access_load; eauto.
eapply HV0. omega.
}
destruct HP as [v9 HLD9].
refine_split; eauto 2.
- subst vcid. rewrite HCid in ×.
replace ((ZMap.get (CPU_ID d2) (cid d2)) × 17 × 4 + 0 × 4) with ((ZMap.get (CPU_ID d2) (cid d2)) × 17 × 4) by omega.
rewrite H11 in ×.
econstructor; eauto 2.
eapply reg_symbol_inject; eassumption.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
- econstructor; eauto.
+ econstructor; eauto.
econstructor; eauto.
rewrite HUctx.
econstructor; eauto.
+ assert (Hinj: ∀ n v, 0≤ n < UCTXT_SIZE →
Mem.load Mint32 m2 b0 (vcid × 17 × 4 + n × 4) = Some v →
val_inject ι (ZMap.get n (ZMap.get vcid (uctxt d1))) v).
{
intros. rewrite <- HCid in HOS.
specialize (H0 _ _ HOS H).
specialize (N_TYPE _ H).
destruct H0 as [v´[HL[_[_ Hinj]]]].
rewrite HL in H2. inv H2.
Transparent Val.load_result.
caseEq (ZMap.get n0 (ZMap.get ((ZMap.get (CPU_ID d1) (cid d1))) (uctxt d1))); intros;
unfold UContext in *; rewrite H0 in *; simpl in Hinj; try assumption;
inv N_TYPE.
}
val_inject_simpl; eapply Hinj; eauto 2; omega.
Qed.
End WITHMEM.
End Refinement.