Library mcertikos.mm.ALInitGenFresh
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require Import ALInitGenSpec.
Require Import ALInitGenDef.
Require Import ALInitGenLemma.
Require Import Conventions.
Require Import ALInitGenDef.
Require Import ALInitGenLemma.
Require Import Conventions.
Section Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Require Import XOmega.
Section acquire_lock_AT_ref.
Lemma acquire_lock_AT_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_AT_spec) acquire_lock_AT_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
pose proof H as HAT.
inv H.
assert (HFB: ι b1 = Some (b1, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold acquire_lock_AT_spec; subrewrite.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. rewrite Hdestruct2 in H1. inv H1.
exploit (relate_AT_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_AT_Log_GetSharedAT_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H12.
intros i Hi.
assert (Hrange: 0 ≤ i / 8 < maxpage).
{
xomega.
}
specialize (H4 _ Hrange).
destruct H4 as (_ & _ & _ & _ & Hv1 & Hv2 & _).
assert (Hieq: ∃ j, i = (i / 8) × 8 + j ∧ 0 ≤ j < 8).
{
specialize (Z_div_mod_eq i 8). intros Hieq.
∃ (i mod 8).
split.
- replace (i / 8 × 8) with (8 × (i / 8)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
}
rewrite H5 in H7; inv H7.
destruct HST as (m2´ & HST).
specialize (H11 _ _ HST).
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× rewrite Hget; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× inv HATC. econstructor; eauto.
intros ? Hrange. specialize (H1 _ Hrange).
destruct H1 as (v & HLD & Hvalid & HM).
assert (Hneq: b1 ≠ b2).
{
red; intros; subst.
exploit (genv_vars_inj s AT_LOC ATC_LOC); eauto.
intros HF. inv HF.
}
refine_split´; eauto.
erewrite Mem.load_storebytes_other; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
× destruct H0 as (HL & HV).
assert (Hneq: b0 ≠ b2).
{
red; intros; subst.
exploit (genv_vars_inj s AT_LOC NPS_LOC); eauto.
intros HF. inv HF.
}
split.
erewrite Mem.load_storebytes_other; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
- inv HQ.
inv multi_log_re. rewrite Hdestruct2 in H1. inv H1.
exploit (relate_AT_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_AT_Log_GetSharedAT_None; eauto.
intros Hget.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× rewrite Hget; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
Qed.
End acquire_lock_AT_ref.
Lemma match_AT_info_Vint:
∀ a v1 v2,
match_AT_info a v2 v1 →
∃ v2´ v1´,
v2 = Vint v2´ ∧ v1 = Vint v1´.
Proof.
intros. inv H; eauto.
unfold Vzero. eauto.
Qed.
Lemma loadbytes_rel:
∀ iend a m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 8) 8 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 8) (ByteList l) = Some m´ →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m´ b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
exploit match_AT_info_Vint; eauto.
intros (v2´ & v1´ & ? & ?); subst.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l1 & HLD1 & Hd1).
exploit decode_val_bytelist; eauto.
intros (l1´ & ?); subst.
revert HL1; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l2 & HLD2 & Hd2).
exploit decode_val_bytelist; eauto.
intros (l2´ & ?); subst.
∃ (l2´ ++ l1´).
split.
- rewrite ByteList_cons.
change 8 with (4 + 4) at 2.
eapply Mem.loadbytes_concat; eauto; omega.
- intros ? ? HSTB.
rewrite ByteList_cons in HSTB.
eapply Mem.storebytes_split in HSTB.
destruct HSTB as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Hlen.
revert HLD1; intros.
exploit Mem.loadbytes_length; eauto.
intros Hlen´.
assert (Hlen2: Z.of_nat (length (ByteList l2´)) = 4).
{
rewrite Hlen.
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
assert (Hlen1: Z.of_nat (length (ByteList l1´)) = 4).
{
rewrite Hlen´.
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
rewrite Hlen2 in HST2.
∃ (Vint v1´), (Vint v2´).
refine_split´; eauto.
+ erewrite Mem.load_storebytes_other; try eapply HST2.
eapply Mem.loadbytes_storebytes_same in HST1.
rewrite Hlen2 in HST1.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2). xomega.
right. simpl. left. reflexivity.
+ eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen1 in HST2.
rewrite Hd1. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2 + 1). xomega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen2 in HST1.
split; trivial. ∃ (ofs × 2). omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST2.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST2.
split; trivial. ∃ (ofs × 2 + 1). omega.
Qed.
Lemma loadbytes_rel_ind:
∀ iend a m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∃ l, Mem.loadbytes m b 0 (Z.of_nat iend × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat iend →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m´ b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1)).
Proof.
induction iend.
- change (Z.of_nat 0) with 0.
intros. simpl.
erewrite Mem.loadbytes_empty; [|reflexivity].
∃ nil. split; trivial.
intros. omega.
- intros.
assert (Hrange: 0 ≤ Z.of_nat (iend) < Z.of_nat (S iend)) by xomega.
exploit loadbytes_rel; eauto.
intros (l & HLD & HST).
exploit (IHiend a m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 8) with ((Z.of_nat (iend) × 8) + 8) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
+ intros.
rewrite ByteList_cons in H.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Heq. rewrite Heq in HST2.
rewrite nat_of_Z_max in HST2.
replace (Z.max (Z.of_nat iend × 8) 0) with (Z.of_nat iend × 8) in HST2 by xomega.
simpl in HST2.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- eapply Mem.storebytes_valid_access_1; eauto.
}
{
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
assert (Heq1: ofs = Z.of_nat iend).
{
destruct (zeq ofs (Z.of_nat iend)); trivial.
xomega.
}
rewrite Heq1.
refine_split´; eauto.
}
Qed.
Lemma loadbytes_rel_storebytes:
∀ a m b s
(Hsymbol: find_symbol s AT_LOC = Some b)
(Hpre: ∀ ofs,
0 ≤ ofs < maxpage →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∃ l, Mem.loadbytes m b 0 (maxpage × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_AT s a m´).
Proof.
intros.
specialize (loadbytes_rel_ind (Z.to_nat maxpage) a m b).
rewrite Z2Nat.id; [| omega].
intros HM. specialize (HM Hpre).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. specialize (HST _ _ H).
econstructor; eauto.
Qed.
Section release_lock_AT_ref.
Lemma release_lock_AT_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_AT_spec) release_lock_AT_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
pose proof H as HAT.
inv H.
assert (HFB: ι b1 = Some (b1, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold release_lock_AT_spec; subrewrite.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. rewrite Hdestruct1 in H1. inv H1.
exploit loadbytes_rel_storebytes; eauto.
intros (l0 & HLD & HST).
assert (Hrel_e: relate_AT_MultiEvent s (TSHARED (OATE (AT d1))) (TSHARED (OMEME l0))).
{
constructor; eauto.
econstructor; eauto.
eapply Mem.loadbytes_length in HLD. rewrite HLD.
rewrite nat_of_Z_max. reflexivity.
}
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold release_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_ticket; eauto.
econstructor; eauto.
× trivial.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_ticket; eauto.
constructor; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
Qed.
End release_lock_AT_ref.
Section getnps_ref.
Lemma getnps_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_nps_spec) get_nps_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV].
refine_split; try (econstructor; eauto).
- simpl. inv match_related.
functional inversion H2; subst. split; congruence.
- functional inversion H2; subst; simpl in ×.
rewrite <- Int.repr_unsigned with z.
rewrite <- Int.repr_unsigned with n. rewrite <- H0, <- H1.
constructor.
- apply inject_incr_refl.
Qed.
End getnps_ref.
Section setnps_ref.
Lemma setnps_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_nps_spec) set_nps_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV].
specialize (Mem.valid_access_store _ _ _ _ (Vint i) HV); intros [m2´ Hm2´].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. subrewrite´. reflexivity.
simpl. inv match_related.
functional inversion H1; subst. split; congruence.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
inv H. inv HATC.
econstructor; eauto.
+ assert (HNB: b ≠ b1).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H7).
discriminate.
}
econstructor; eauto.
intros. specialize (H _ H8).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H; eauto.
destruct H as [v1[HL1[HV1 HAT]]].
∃ v1.
refine_split´; trivial;
try apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+
assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H6).
discriminate.
}
econstructor; eauto.
intros. specialize (H0 _ H8).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H0; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H0; eauto.
destruct H0 as [v1[v2[HL1[HL2[HV1[HV2 HAT]]]]]].
∃ v1, v2.
refine_split´; trivial;
try apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+ split.
exploit Mem.load_store_same; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+ reflexivity.
- apply inject_incr_refl.
Qed.
End setnps_ref.
Section getatu_ref.
Lemma getatu_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_at_u_spec) at_get_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H.
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HAT.
specialize (H0 _ HOS). destruct H0 as [v1[v2[HL1[HL2[_ [_ HM]]]]]].
assert (HP: ∃ v, Int.unsigned z = IntToBoolZ v ∧ v2 = Vint v).
{
unfold get_at_u_spec in *; subdestruct;
inv HM; esplit; split; eauto; inv H2; functional inversion H8; trivial.
}
destruct HP as [v[HEQ HEV]]; subst.
refine_split; eauto; econstructor; eauto.
Qed.
End getatu_ref.
Section getatc_ref.
Lemma getatc_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_at_c_spec) at_get_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H. inv HATC.
assert(HOS: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H as HAT.
specialize (H _ HOS). destruct H as [v1[HL1[_ HM]]].
assert (HP: v1 = Vint z).
{
unfold get_at_c_spec in *; subdestruct.
inv HM; eauto.
rewrite <- (Int.repr_unsigned z).
rewrite <- (Int.repr_unsigned z0). inv H2.
reflexivity.
}
subst. refine_split; eauto; econstructor; eauto.
Qed.
End getatc_ref.
Section setatu_ref.
Lemma setatu_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_u_spec) at_set_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage
∧ (∃ atype, ZtoBool (Int.unsigned i0) = Some atype)).
{
inv match_related.
unfold set_at_u_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern[HOS [attype HZ2AT]]].
inv H. rename H4 into HMAT; destruct (HMAT _ HOS) as [v1 [v2[HL1 [HL2[HV1[HV2 HM]]]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m2´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. subrewrite´. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
× inv HATC.
assert (HNB: b2 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H10 H5).
discriminate.
}
econstructor; eauto. intros.
specialize (H _ H11).
destruct H as (v0 & HL0 & HV0 & HM0).
refine_split´; trivial.
{ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; eauto. }
{ eapply Mem.store_valid_access_1; eauto. }
{ trivial. }
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ v1, (Vint i0).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; auto.
right; left; simpl; omega.
apply Mem.load_store_same in HST; trivial.
rewrite ZMap.gss.
rewrite <- Int.repr_unsigned with i0.
rewrite H9 in HM. inv HM; try econstructor; eauto.
}
{
specialize (HMAT _ H).
destruct HMAT as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
refine_split´; trivial;
try eapply Mem.store_valid_access_1; eauto.
simpl; rewrite ZMap.gso; trivial.
}
× assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
destruct H0 as [HL0 HV0].
split. rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
eapply Mem.store_valid_access_1; eauto.
- apply inject_incr_refl.
Qed.
End setatu_ref.
Section setatc_ref.
Lemma setatc_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_c_spec) at_set_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
inv match_related.
unfold set_at_c_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern HOS].
inv HATC. rename H4 into HMAT.
destruct (HMAT _ HOS) as [v1[HL1[HV1 HM]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m3 HST].
refine_split.
- econstructor; eauto.
simpl. lift_trivial. subrewrite´. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint i0).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
apply Mem.load_store_same in HST; trivial.
rewrite ZMap.gss. econstructor; eauto.
}
{
specialize (HMAT _ H4).
destruct HMAT as [v1´[HL1´[HV1´ HM2]]].
∃ v1´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
refine_split´; trivial;
try eapply Mem.store_valid_access_1; eauto.
simpl; rewrite ZMap.gso; trivial.
}
× inv H.
assert (HNB: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H10 H5).
discriminate.
}
econstructor; eauto.
intros.
specialize (H4 _ H).
destruct H4 as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
refine_split´; try (eapply Mem.store_valid_access_1; eauto).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
trivial.
× assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
destruct H0 as [HL0 HV0].
split. rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
eapply Mem.store_valid_access_1; eauto.
- apply inject_incr_refl.
Qed.
End setatc_ref.
Section getatnorm_ref.
Lemma getatnorm_spec_ref:
compatsim (crel HDATA LDATA) (gensem is_at_norm_spec) is_norm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H.
assert(HOS: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HAT.
specialize (H0 _ HOS); destruct H0 as [v1 [v2[HL1 [HL2[_[_ HM]]]]]].
assert (HP: ∃ v, Int.unsigned z = ZToATTypeZ (Int.unsigned v) ∧ v1 = Vint v).
{
unfold is_at_norm_spec in *; subdestruct;
inv HM; refine_split´; eauto; inv H2.
- functional inversion H5; trivial.
- destruct t; functional inversion H5; trivial. congruence.
}
destruct HP as [v[HEQ HEV]]; subst.
refine_split; eauto; econstructor; eauto.
Qed.
End getatnorm_ref.
Section setatnorm_ref.
Lemma setatnorm_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_norm_spec) set_norm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage
∧ (∃ atype, ZtoATType (Int.unsigned i0) = Some atype)).
{
simpl; inv match_related.
unfold set_at_norm_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern[HOS [attype HZ2AT]]].
inv H. rename H4 into HMAT. destruct (HMAT _ HOS) as [v1[v2[HL1[HL2[HV1[HV2 HM]]]]]].
inv HATC. rename H into HMATC. destruct (HMATC _ HOS) as [v3[HL3[HV3 HM3]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m0 HST].
assert (HP: ∃ m1, Mem.store Mint32 m0 b0 (Int.unsigned i × 8 + 4) (Vzero) = Some m1).
{
apply (Mem.valid_access_store); auto.
eapply Mem.store_valid_access_1; eauto.
}
destruct HP as [m1 HST1].
assert (HP: ∃ m2, Mem.store Mint32 m1 b1 (Int.unsigned i × 4) (Vzero) = Some m2).
{
apply (Mem.valid_access_store); auto.
repeat (eapply Mem.store_valid_access_1; eauto).
}
destruct HP as [m22 HST2].
refine_split.
- econstructor; eauto; simpl; lift_trivial.
simpl. subrewrite´.
simpl. subrewrite´.
simpl. subrewrite´. unfold set; simpl. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
assert (HNB: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H4 H5).
discriminate.
}
econstructor; simpl; eauto.
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint Int.zero).
refine_split´;
repeat (eapply Mem.store_valid_access_1; eauto).
apply Mem.load_store_same in HST2. eauto.
rewrite ZMap.gss.
change 0 with (Int.unsigned (Int.repr 0)).
econstructor; eauto.
}
{
specialize (HMATC _ H).
destruct HMATC as [v1´[HL1´[HV1´ HM2]]].
∃ v1´.
refine_split´; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL1´; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL1´; auto.
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
repeat (eapply Mem.store_valid_access_1; eauto).
simpl; rewrite ZMap.gso; trivial.
}
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint i0), (Vint (Int.repr 0)).
refine_split´;
repeat (eapply Mem.store_valid_access_1; eauto).
apply Mem.load_store_same in HST.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HST; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HST; trivial.
left. auto.
right; left; simpl; omega.
apply Mem.load_store_same in HST1; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HST1; trivial.
left. auto.
rewrite ZMap.gss.
change 0 with (Int.unsigned (Int.repr 0)).
econstructor; eauto.
}
{
specialize (HMAT _ H).
destruct HMAT as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL1´, HL2´;
try (simpl; left; auto).
refine_split´; trivial;
repeat (eapply Mem.store_valid_access_1; eauto).
simpl; rewrite ZMap.gso; trivial.
}
× assert (HNB1: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
assert (HNB2: b ≠ b1).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H4).
discriminate.
}
destruct H0 as [HL0 HV0]. split.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL0; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL0; auto.
repeat (eapply Mem.store_valid_access_1; eauto).
- apply inject_incr_refl.
Qed.
End setatnorm_ref.
End WITHMEM.
End Refinement.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Require Import XOmega.
Section acquire_lock_AT_ref.
Lemma acquire_lock_AT_spec_ref:
compatsim (crel HDATA LDATA) (gensem acquire_lock_AT_spec) acquire_lock_AT_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
pose proof H as HAT.
inv H.
assert (HFB: ι b1 = Some (b1, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold acquire_lock_AT_spec; subrewrite.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. rewrite Hdestruct2 in H1. inv H1.
exploit (relate_AT_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_AT_Log_GetSharedAT_Some; eauto.
intros (a´ & Hget & Hrel_e).
inv Hrel_e.
assert (HST: ∃ m2´, Mem.storebytes m2 b1 0 (ByteList a´) = Some m2´).
{
eapply Mem.range_perm_storebytes; eauto. rewrite H12.
intros i Hi.
assert (Hrange: 0 ≤ i / 8 < maxpage).
{
xomega.
}
specialize (H4 _ Hrange).
destruct H4 as (_ & _ & _ & _ & Hv1 & Hv2 & _).
assert (Hieq: ∃ j, i = (i / 8) × 8 + j ∧ 0 ≤ j < 8).
{
specialize (Z_div_mod_eq i 8). intros Hieq.
∃ (i mod 8).
split.
- replace (i / 8 × 8) with (8 × (i / 8)) by omega.
eapply Hieq. omega.
- eapply Z_mod_lt. omega.
}
destruct Hieq as (j & Heq & Hj).
rewrite Heq.
destruct (zlt j 4).
{
destruct Hv1 as (Hv1 & _).
eapply Hv1. simpl. omega.
}
{
destruct Hv2 as (Hv2 & _).
eapply Hv2. simpl. omega.
}
}
rewrite H5 in H7; inv H7.
destruct HST as (m2´ & HST).
specialize (H11 _ _ HST).
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× rewrite Hget; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× inv HATC. econstructor; eauto.
intros ? Hrange. specialize (H1 _ Hrange).
destruct H1 as (v & HLD & Hvalid & HM).
assert (Hneq: b1 ≠ b2).
{
red; intros; subst.
exploit (genv_vars_inj s AT_LOC ATC_LOC); eauto.
intros HF. inv HF.
}
refine_split´; eauto.
erewrite Mem.load_storebytes_other; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
× destruct H0 as (HL & HV).
assert (Hneq: b0 ≠ b2).
{
red; intros; subst.
exploit (genv_vars_inj s AT_LOC NPS_LOC); eauto.
intros HF. inv HF.
}
split.
erewrite Mem.load_storebytes_other; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
- inv HQ.
inv multi_log_re. rewrite Hdestruct2 in H1. inv H1.
exploit (relate_AT_Log_oracle_cons (CPU_ID d2)); eauto.
intros Hrel_o.
exploit relate_AT_Log_GetSharedAT_None; eauto.
intros Hget.
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold acquire_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
× rewrite Hget; eauto.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_pull; eauto.
eapply relate_AT_Log_ticket; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
Qed.
End acquire_lock_AT_ref.
Lemma match_AT_info_Vint:
∀ a v1 v2,
match_AT_info a v2 v1 →
∃ v2´ v1´,
v2 = Vint v2´ ∧ v1 = Vint v1´.
Proof.
intros. inv H; eauto.
unfold Vzero. eauto.
Qed.
Lemma loadbytes_rel:
∀ iend a m b
(Hpre: ∀ ofs,
0 ≤ ofs < iend →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∀ ofs
(Hrange: 0 ≤ ofs < iend),
∃ l, Mem.loadbytes m b (ofs × 8) 8 = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b (ofs × 8) (ByteList l) = Some m´ →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m´ b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1).
Proof.
intros. specialize (Hpre _ Hrange).
destruct Hpre as (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
exploit match_AT_info_Vint; eauto.
intros (v2´ & v1´ & ? & ?); subst.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l1 & HLD1 & Hd1).
exploit decode_val_bytelist; eauto.
intros (l1´ & ?); subst.
revert HL1; intros.
exploit Mem.load_loadbytes; eauto.
simpl. intros (l2 & HLD2 & Hd2).
exploit decode_val_bytelist; eauto.
intros (l2´ & ?); subst.
∃ (l2´ ++ l1´).
split.
- rewrite ByteList_cons.
change 8 with (4 + 4) at 2.
eapply Mem.loadbytes_concat; eauto; omega.
- intros ? ? HSTB.
rewrite ByteList_cons in HSTB.
eapply Mem.storebytes_split in HSTB.
destruct HSTB as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Hlen.
revert HLD1; intros.
exploit Mem.loadbytes_length; eauto.
intros Hlen´.
assert (Hlen2: Z.of_nat (length (ByteList l2´)) = 4).
{
rewrite Hlen.
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
assert (Hlen1: Z.of_nat (length (ByteList l1´)) = 4).
{
rewrite Hlen´.
rewrite nat_of_Z_max.
replace (Z.max 4 0) with 4 by xomega. trivial.
}
rewrite Hlen2 in HST2.
∃ (Vint v1´), (Vint v2´).
refine_split´; eauto.
+ erewrite Mem.load_storebytes_other; try eapply HST2.
eapply Mem.loadbytes_storebytes_same in HST1.
rewrite Hlen2 in HST1.
rewrite Hd2. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2). xomega.
right. simpl. left. reflexivity.
+ eapply Mem.loadbytes_storebytes_same in HST2.
rewrite Hlen1 in HST2.
rewrite Hd1. eapply Mem.loadbytes_load; eauto.
simpl. ∃ (ofs × 2 + 1). xomega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST1.
unfold Mem.valid_access.
simpl. rewrite Hlen2 in HST1.
split; trivial. ∃ (ofs × 2). omega.
+ eapply Mem.storebytes_valid_access_1; eauto.
eapply Mem.storebytes_range_perm in HST2.
unfold Mem.valid_access.
simpl. rewrite Hlen1 in HST2.
split; trivial. ∃ (ofs × 2 + 1). omega.
Qed.
Lemma loadbytes_rel_ind:
∀ iend a m b
(Hpre: ∀ ofs,
0 ≤ ofs < Z.of_nat (iend) →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∃ l, Mem.loadbytes m b 0 (Z.of_nat iend × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
(∀ ofs,
0 ≤ ofs < Z.of_nat iend →
∃ v1 v2,
Mem.load Mint32 m´ b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m´ b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m´ Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m´ Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1)).
Proof.
induction iend.
- change (Z.of_nat 0) with 0.
intros. simpl.
erewrite Mem.loadbytes_empty; [|reflexivity].
∃ nil. split; trivial.
intros. omega.
- intros.
assert (Hrange: 0 ≤ Z.of_nat (iend) < Z.of_nat (S iend)) by xomega.
exploit loadbytes_rel; eauto.
intros (l & HLD & HST).
exploit (IHiend a m b); eauto.
{
intros. eapply Hpre. omega.
}
intros (l´ & HLD´ & HST´).
∃ (l´ ++ l).
split.
+ replace (Z.of_nat (S iend) × 8) with ((Z.of_nat (iend) × 8) + 8) by xomega.
rewrite ByteList_cons.
eapply Mem.loadbytes_concat; eauto; try xomega.
+ intros.
rewrite ByteList_cons in H.
eapply Mem.storebytes_split in H.
destruct H as (m1 & HST1 & HST2).
exploit Mem.loadbytes_length; eauto.
intros Heq. rewrite Heq in HST2.
rewrite nat_of_Z_max in HST2.
replace (Z.max (Z.of_nat iend × 8) 0) with (Z.of_nat iend × 8) in HST2 by xomega.
simpl in HST2.
destruct (zlt ofs (Z.of_nat (iend))).
{
specialize (HST´ _ _ HST1).
exploit (HST´ ofs). omega.
intros (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
refine_split´; eauto.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- erewrite Mem.load_storebytes_other; eauto.
simpl. right. left. omega.
- eapply Mem.storebytes_valid_access_1; eauto.
- eapply Mem.storebytes_valid_access_1; eauto.
}
{
specialize (HST _ _ HST2).
destruct HST as (v1 & v2 & HL1 & HL2 & HV1 & HV2 & HM).
assert (Heq1: ofs = Z.of_nat iend).
{
destruct (zeq ofs (Z.of_nat iend)); trivial.
xomega.
}
rewrite Heq1.
refine_split´; eauto.
}
Qed.
Lemma loadbytes_rel_storebytes:
∀ a m b s
(Hsymbol: find_symbol s AT_LOC = Some b)
(Hpre: ∀ ofs,
0 ≤ ofs < maxpage →
∃ v1 v2,
Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
match_AT_info (ZMap.get ofs a) v2 v1),
∃ l, Mem.loadbytes m b 0 (maxpage × 8) = Some (ByteList l)
∧ (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
match_AT s a m´).
Proof.
intros.
specialize (loadbytes_rel_ind (Z.to_nat maxpage) a m b).
rewrite Z2Nat.id; [| omega].
intros HM. specialize (HM Hpre).
destruct HM as (l & HLD & HST).
∃ l. split; trivial.
intros. specialize (HST _ _ H).
econstructor; eauto.
Qed.
Section release_lock_AT_ref.
Lemma release_lock_AT_spec_ref:
compatsim (crel HDATA LDATA) (gensem release_lock_AT_spec) release_lock_AT_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros Hargs0 Hasm_inv Hesp HRA Hle.
pose proof H as HAT.
inv H.
assert (HFB: ι b1 = Some (b1, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
pose proof match_related as Hre.
simpl; inv match_related.
revert H1.
unfold release_lock_AT_spec; subrewrite.
set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs2))).
∃ ι, (rs2´#RA <- Vundef #PC <- (rs2#RA)).
subdestruct.
- inv HQ.
inv multi_log_re. rewrite Hdestruct1 in H1. inv H1.
exploit loadbytes_rel_storebytes; eauto.
intros (l0 & HLD & HST).
assert (Hrel_e: relate_AT_MultiEvent s (TSHARED (OATE (AT d1))) (TSHARED (OMEME l0))).
{
constructor; eauto.
econstructor; eauto.
eapply Mem.loadbytes_length in HLD. rewrite HLD.
rewrite nat_of_Z_max. reflexivity.
}
refine_split´; repeat val_inject_inv; eauto.
+ econstructor; eauto; simpl; lift_trivial.
× unfold release_lock_spec. simpl; subrewrite´.
rewrite <- H8.
erewrite (H_CalLock_relate_AT_log _ _ s); eauto.
eapply relate_AT_Log_ticket; eauto.
econstructor; eauto.
× trivial.
+ split; eauto; pattern2_refinement_simpl; econstructor; eauto.
× intros. pose proof H1 as Hneq. eapply index2Z_neq in Hneq; eauto.
repeat rewrite ZMap.gso; eauto.
× repeat rewrite ZMap.gss. constructor.
eapply relate_AT_Log_ticket; eauto.
constructor; eauto.
+ intros. inv Hasm_inv.
inv inv_inject_neutral. subst rs2´.
destruct r; simpl;
repeat simpl_Pregmap; eauto;
(elim H1; eauto 20).
Qed.
End release_lock_AT_ref.
Section getnps_ref.
Lemma getnps_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_nps_spec) get_nps_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV].
refine_split; try (econstructor; eauto).
- simpl. inv match_related.
functional inversion H2; subst. split; congruence.
- functional inversion H2; subst; simpl in ×.
rewrite <- Int.repr_unsigned with z.
rewrite <- Int.repr_unsigned with n. rewrite <- H0, <- H1.
constructor.
- apply inject_incr_refl.
Qed.
End getnps_ref.
Section setnps_ref.
Lemma setnps_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_nps_spec) set_nps_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV].
specialize (Mem.valid_access_store _ _ _ _ (Vint i) HV); intros [m2´ Hm2´].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. subrewrite´. reflexivity.
simpl. inv match_related.
functional inversion H1; subst. split; congruence.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
inv H. inv HATC.
econstructor; eauto.
+ assert (HNB: b ≠ b1).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H7).
discriminate.
}
econstructor; eauto.
intros. specialize (H _ H8).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H; eauto.
destruct H as [v1[HL1[HV1 HAT]]].
∃ v1.
refine_split´; trivial;
try apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+
assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H6).
discriminate.
}
econstructor; eauto.
intros. specialize (H0 _ H8).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H0; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ Hm2´) in H0; eauto.
destruct H0 as [v1[v2[HL1[HL2[HV1[HV2 HAT]]]]]].
∃ v1, v2.
refine_split´; trivial;
try apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+ split.
exploit Mem.load_store_same; eauto.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ Hm2´); trivial.
+ reflexivity.
- apply inject_incr_refl.
Qed.
End setnps_ref.
Section getatu_ref.
Lemma getatu_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_at_u_spec) at_get_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H.
assert(HOS: kernel_mode d2 ∧ 0 ≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HAT.
specialize (H0 _ HOS). destruct H0 as [v1[v2[HL1[HL2[_ [_ HM]]]]]].
assert (HP: ∃ v, Int.unsigned z = IntToBoolZ v ∧ v2 = Vint v).
{
unfold get_at_u_spec in *; subdestruct;
inv HM; esplit; split; eauto; inv H2; functional inversion H8; trivial.
}
destruct HP as [v[HEQ HEV]]; subst.
refine_split; eauto; econstructor; eauto.
Qed.
End getatu_ref.
Section getatc_ref.
Lemma getatc_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_at_c_spec) at_get_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H. inv HATC.
assert(HOS: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H as HAT.
specialize (H _ HOS). destruct H as [v1[HL1[_ HM]]].
assert (HP: v1 = Vint z).
{
unfold get_at_c_spec in *; subdestruct.
inv HM; eauto.
rewrite <- (Int.repr_unsigned z).
rewrite <- (Int.repr_unsigned z0). inv H2.
reflexivity.
}
subst. refine_split; eauto; econstructor; eauto.
Qed.
End getatc_ref.
Section setatu_ref.
Lemma setatu_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_u_spec) at_set_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage
∧ (∃ atype, ZtoBool (Int.unsigned i0) = Some atype)).
{
inv match_related.
unfold set_at_u_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern[HOS [attype HZ2AT]]].
inv H. rename H4 into HMAT; destruct (HMAT _ HOS) as [v1 [v2[HL1 [HL2[HV1[HV2 HM]]]]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV2); intros [m2´ HST].
refine_split.
- econstructor; eauto.
simpl; lift_trivial. subrewrite´. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
× inv HATC.
assert (HNB: b2 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H10 H5).
discriminate.
}
econstructor; eauto. intros.
specialize (H _ H11).
destruct H as (v0 & HL0 & HV0 & HM0).
refine_split´; trivial.
{ rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; eauto. }
{ eapply Mem.store_valid_access_1; eauto. }
{ trivial. }
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ v1, (Vint i0).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1; auto.
right; left; simpl; omega.
apply Mem.load_store_same in HST; trivial.
rewrite ZMap.gss.
rewrite <- Int.repr_unsigned with i0.
rewrite H9 in HM. inv HM; try econstructor; eauto.
}
{
specialize (HMAT _ H).
destruct HMAT as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
refine_split´; trivial;
try eapply Mem.store_valid_access_1; eauto.
simpl; rewrite ZMap.gso; trivial.
}
× assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
destruct H0 as [HL0 HV0].
split. rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
eapply Mem.store_valid_access_1; eauto.
- apply inject_incr_refl.
Qed.
End setatu_ref.
Section setatc_ref.
Lemma setatc_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_c_spec) at_set_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
inv match_related.
unfold set_at_c_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern HOS].
inv HATC. rename H4 into HMAT.
destruct (HMAT _ HOS) as [v1[HL1[HV1 HM]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m3 HST].
refine_split.
- econstructor; eauto.
simpl. lift_trivial. subrewrite´. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint i0).
refine_split´; try eapply Mem.store_valid_access_1; eauto.
apply Mem.load_store_same in HST; trivial.
rewrite ZMap.gss. econstructor; eauto.
}
{
specialize (HMAT _ H4).
destruct HMAT as [v1´[HL1´[HV1´ HM2]]].
∃ v1´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
refine_split´; trivial;
try eapply Mem.store_valid_access_1; eauto.
simpl; rewrite ZMap.gso; trivial.
}
× inv H.
assert (HNB: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H10 H5).
discriminate.
}
econstructor; eauto.
intros.
specialize (H4 _ H).
destruct H4 as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
refine_split´; try (eapply Mem.store_valid_access_1; eauto).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; eauto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL2´; eauto.
trivial.
× assert (HNB: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
destruct H0 as [HL0 HV0].
split. rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
eapply Mem.store_valid_access_1; eauto.
- apply inject_incr_refl.
Qed.
End setatc_ref.
Section getatnorm_ref.
Lemma getatnorm_spec_ref:
compatsim (crel HDATA LDATA) (gensem is_at_norm_spec) is_norm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
destruct H0 as [HL HV]. inv H.
assert(HOS: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage).
{
simpl; inv match_related.
functional inversion H2; repeat (split; trivial); congruence.
}
destruct HOS as [Hkern HOS].
pose proof H0 as HAT.
specialize (H0 _ HOS); destruct H0 as [v1 [v2[HL1 [HL2[_[_ HM]]]]]].
assert (HP: ∃ v, Int.unsigned z = ZToATTypeZ (Int.unsigned v) ∧ v1 = Vint v).
{
unfold is_at_norm_spec in *; subdestruct;
inv HM; refine_split´; eauto; inv H2.
- functional inversion H5; trivial.
- destruct t; functional inversion H5; trivial. congruence.
}
destruct HP as [v[HEQ HEV]]; subst.
refine_split; eauto; econstructor; eauto.
Qed.
End getatnorm_ref.
Section setatnorm_ref.
Lemma setatnorm_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_at_norm_spec) set_norm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ 0≤ Int.unsigned i < maxpage
∧ (∃ atype, ZtoATType (Int.unsigned i0) = Some atype)).
{
simpl; inv match_related.
unfold set_at_norm_spec in *; subdestruct;
repeat (split; congruence); eauto.
}
destruct Hkern as [Hkern[HOS [attype HZ2AT]]].
inv H. rename H4 into HMAT. destruct (HMAT _ HOS) as [v1[v2[HL1[HL2[HV1[HV2 HM]]]]]].
inv HATC. rename H into HMATC. destruct (HMATC _ HOS) as [v3[HL3[HV3 HM3]]].
specialize (Mem.valid_access_store _ _ _ _ (Vint i0) HV1); intros [m0 HST].
assert (HP: ∃ m1, Mem.store Mint32 m0 b0 (Int.unsigned i × 8 + 4) (Vzero) = Some m1).
{
apply (Mem.valid_access_store); auto.
eapply Mem.store_valid_access_1; eauto.
}
destruct HP as [m1 HST1].
assert (HP: ∃ m2, Mem.store Mint32 m1 b1 (Int.unsigned i × 4) (Vzero) = Some m2).
{
apply (Mem.valid_access_store); auto.
repeat (eapply Mem.store_valid_access_1; eauto).
}
destruct HP as [m22 HST2].
refine_split.
- econstructor; eauto; simpl; lift_trivial.
simpl. subrewrite´.
simpl. subrewrite´.
simpl. subrewrite´. unfold set; simpl. reflexivity.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
assert (HNB: b1 ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H4 H5).
discriminate.
}
econstructor; simpl; eauto.
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint Int.zero).
refine_split´;
repeat (eapply Mem.store_valid_access_1; eauto).
apply Mem.load_store_same in HST2. eauto.
rewrite ZMap.gss.
change 0 with (Int.unsigned (Int.repr 0)).
econstructor; eauto.
}
{
specialize (HMATC _ H).
destruct HMATC as [v1´[HL1´[HV1´ HM2]]].
∃ v1´.
refine_split´; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL1´; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL1´; auto.
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
repeat (eapply Mem.store_valid_access_1; eauto).
simpl; rewrite ZMap.gso; trivial.
}
× econstructor; eauto; intros.
destruct (zeq ofs (Int.unsigned i)); subst.
{
∃ (Vint i0), (Vint (Int.repr 0)).
refine_split´;
repeat (eapply Mem.store_valid_access_1; eauto).
apply Mem.load_store_same in HST.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HST; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HST; trivial.
left. auto.
right; left; simpl; omega.
apply Mem.load_store_same in HST1; trivial.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HST1; trivial.
left. auto.
rewrite ZMap.gss.
change 0 with (Int.unsigned (Int.repr 0)).
econstructor; eauto.
}
{
specialize (HMAT _ H).
destruct HMAT as [v1´[v2´[HL1´[HL2´[HV1´[HV2´ HM2]]]]]].
∃ v1´, v2´.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL1´, HL2´;
try (simpl; right; destruct (zle ofs (Int.unsigned i)); [left; omega|right; omega]).
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL1´, HL2´;
try (simpl; left; auto).
refine_split´; trivial;
repeat (eapply Mem.store_valid_access_1; eauto).
simpl; rewrite ZMap.gso; trivial.
}
× assert (HNB1: b ≠ b0).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H5).
discriminate.
}
assert (HNB2: b ≠ b1).
{
red; intros; subst.
specialize (genv_vars_inj _ _ _ _ H3 H4).
discriminate.
}
destruct H0 as [HL0 HV0]. split.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) in HL0; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST1) in HL0; auto.
rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST2) in HL0; auto.
repeat (eapply Mem.store_valid_access_1; eauto).
- apply inject_incr_refl.
Qed.
End setatnorm_ref.
End WITHMEM.
End Refinement.