Commit 4fbce512 authored by Ralf Jung's avatar Ralf Jung
Browse files

make Iris more compatible with name mangling

parent 8cfbc446
......@@ -310,6 +310,7 @@ Section ectx_language.
End ectx_language.
Global Arguments ectx_lang : clear implicits.
Global Arguments Ectx_step {Λ e1 σ1 κ e2 σ2 efs}.
Coercion ectx_lang : ectxLanguage >-> language.
(* This definition makes sure that the fields of the [language] record do not
......
......@@ -67,7 +67,7 @@ Proof.
apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
- destruct t as [|e1' ?]; simplify_eq/=.
+ iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
{ by eapply step_atomic with (t1:=[]). }
{ by eapply (step_atomic _ _ _ _ _ _ _ _ []). }
iModIntro. iExists n2. iFrame "Hσ".
rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
by setoid_rewrite (right_id_L [] (++)).
......
......@@ -1048,7 +1048,7 @@ Section tac_modal_intro.
naive_solver. }
assert ( [] Γp M ( [] Γp'))%I as HMp.
{ remember (modality_intuitionistic_action M).
destruct HΓp as [?|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
destruct HΓp as [? M|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
- rewrite {1}intuitionistically_elim_emp (modality_emp M)
intuitionistically_True_emp //.
- eauto using modality_intuitionistic_forall_big_and.
......@@ -1059,7 +1059,7 @@ Section tac_modal_intro.
- eauto using modality_intuitionistic_id. }
move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
remember (modality_spatial_action M).
destruct HΓs as [?|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
- by rewrite -HQ' /= !right_id.
- rewrite -HQ' {1}(modality_spatial_forall_big_sep _ _ Γs) //.
by rewrite modality_sep.
......
......@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, inv_heap_inv - WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
intros Hwp; eapply (wp_adequacy _ _); iIntros (? κs) "".
iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
iMod (inv_heap_init loc (option val)) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
......
......@@ -64,18 +64,18 @@ Section atomic.
Proof.
rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
- subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
- subst. inversion_clear step. by eapply (H σ1 (Val _) _ σ2 efs), head_prim_step.
- rewrite fill_app. rewrite fill_app in Hfill.
assert ( v, Val v = fill Ks e1' False) as fill_absurd.
{ intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
destruct K; (inversion Hfill; clear Hfill; subst; try
match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
refine (_ (H σ1 (fill (Ks ++ [_]) e2') _ σ2 efs _)).
+ destruct s; intro Hs; simpl in *.
* destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
* apply irreducible_resolve. by rewrite fill_app in Hs.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+ econstructor; try done. simpl. by rewrite fill_app.
Qed.
End atomic.
......
......@@ -797,5 +797,5 @@ Proof.
apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
end).
eapply (H κs (fill_item _ (foldl (flip fill_item) e2' Ks)) σ' efs).
eapply (Ectx_step _ _ _ _ _ _ (Ks ++ [_])); last done; simpl; by rewrite fill_app.
eapply (Ectx_step (Ks ++ [_])); last done; simpl; by rewrite fill_app.
Qed.
......@@ -224,7 +224,7 @@ Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
as "(Hσ & Hl & Hm)".
{ apply heap_array_map_disjoint.
rewrite replicate_length Z2Nat.id; auto with lia. }
......@@ -380,6 +380,7 @@ Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto with head_step.
iIntros "!>" (v2 σ2 efs Hstep). inv_head_step.
rename select proph_id into p.
iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
iModIntro; iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -393,7 +394,7 @@ Lemma resolve_reducible e σ (p : proph_id) v :
Proof.
intros A (κ & e' & σ' & efs & H).
exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
eapply Ectx_step with (K:=[]); try done.
eapply (Ectx_step []); try done.
assert (w, Val w = e') as [w <-].
{ unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
......@@ -409,18 +410,21 @@ Proof.
induction Ks as [|K Ks _] using rev_ind.
+ simpl in *. subst. inv_head_step. by constructor.
+ rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
- assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
- rename select ectx_item into Ki.
assert (fill_item Ki (fill Ks e1') = fill (Ks ++ [Ki]) e1') as Eq1;
first by rewrite fill_app.
assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
assert (fill_item Ki (fill Ks e2') = fill (Ks ++ [Ki]) e2') as Eq2;
first by rewrite fill_app.
rewrite fill_app /=. rewrite Eq1 in A.
assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
{ apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
assert (is_Some (to_val (fill (Ks ++ [Ki]) e2'))) as H.
{ apply (A σ1 _ κ σ2 efs). eapply (Ectx_step (Ks ++ [Ki])); done. }
destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
- assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
apply to_val_fill_some in H as [-> ->]. inv_head_step.
- assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
apply to_val_fill_some in H as [-> ->]. inv_head_step.
- rename select (of_val vp = _) into Hvp.
assert (to_val (fill Ks e1') = Some vp) as Hfillvp by rewrite -Hvp //.
apply to_val_fill_some in Hfillvp as [-> ->]. inv_head_step.
- rename select (of_val vt = _) into Hvt.
assert (to_val (fill Ks e1') = Some vt) as Hfillvt by rewrite -Hvt //.
apply to_val_fill_some in Hfillvt as [-> ->]. inv_head_step.
Qed.
Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
......
......@@ -420,7 +420,8 @@ Proof.
eapply Resolve_3_vals_head_stuck; eauto. }
rewrite fill_app in Hrs.
destruct Ki; simplify_eq/=.
- pose proof (fill_item_val Ki (fill K e1')) as Hnv.
- rename select ectx_item into Ki.
pose proof (fill_item_val Ki (fill K e1')) as Hnv.
apply fill_val in Hnv as [? Hnv]; last by rewrite -Hrs; eauto.
by erewrite val_head_stuck in Hnv.
- edestruct Hvfill as [? Heq]; eauto.
......@@ -629,7 +630,7 @@ Proof.
rewrite app_length in IHm; simpl in *.
rewrite fill_app /=; rewrite fill_app /= in He1.
eapply prim_step_matched_by_erased_steps_ectx_item; eauto; [].
{ intros; simpl in *; apply (IHm (length K')); auto with lia. }
{ intros K' **; simpl in *. apply (IHm (length K')); auto with lia. }
Qed.
Lemma head_step_erased_prim_step_CmpXchg v1 v2 σ l vl:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment