From 2ebe30f235048976b0563c42a736705128054d93 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Nov 2023 21:38:41 +0100
Subject: [PATCH] update dependencies
---
coq-iris-examples.opam | 2 +-
.../concurrent_stacks/concurrent_stack1.v | 4 +-
.../concurrent_stacks/concurrent_stack2.v | 4 +-
.../concurrent_stacks/concurrent_stack3.v | 6 +-
.../concurrent_stacks/concurrent_stack4.v | 6 +-
theories/hocap/fg_bag.v | 4 +-
theories/lecture_notes/coq_intro_example_2.v | 2 +-
theories/logatom/conditional_increment/cinc.v | 22 +++----
theories/logatom/elimination_stack/stack.v | 4 +-
theories/logatom/flat_combiner/peritem.v | 4 +-
theories/logatom/rdcss/rdcss.v | 16 ++---
theories/logatom/rdcss/spec.v | 2 +-
theories/logatom/snapshot/atomic_snapshot.v | 6 +-
theories/logatom/treiber.v | 14 ++---
theories/logatom/treiber2.v | 6 +-
.../binary/examples/stack/refinement.v | 6 +-
theories/logrel/F_mu_ref_conc/binary/rules.v | 42 ++++++-------
.../logrel/F_mu_ref_conc/binary/soundness.v | 4 +-
theories/logrel/F_mu_ref_conc/lang.v | 60 +++++++++----------
theories/logrel/F_mu_ref_conc/wp_rules.v | 48 +++++++--------
theories/logrel/stlc/lang.v | 26 ++++----
theories/logrel/stlc/rules.v | 12 ++--
22 files changed, 150 insertions(+), 150 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 2834910a..cf9b6ede 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
depends: [
- "coq-iris-heap-lang" { (= "dev.2023-10-30.0.b5d08cb7") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-11-06.5.4cfd3db8") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index d83ece09..dec4e4e5 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -100,7 +100,7 @@ Section stacks.
iInv N as (â„“'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
destruct (decide (v' = v'')) as [->|Hne].
- wp_cmpxchg_suc. { destruct v''; left; done. }
- iMod (mapsto_persist with "Hl'") as "Hl'".
+ iMod (pointsto_persist with "Hl'") as "Hl'".
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (Some â„“'); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (Some _)) /=. eauto with iFrame. }
@@ -145,7 +145,7 @@ Section stacks.
* rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist) /=".
wp_cmpxchg_suc.
- iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
+ iDestruct (pointsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists â„“'', _; by iFrame. }
iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 3e294388..8ec72252 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -312,7 +312,7 @@ Section stack_works.
iInv N as (list) "(Hl & Hlist)" "Hclose".
destruct (decide (v'' = list)) as [ -> |].
* wp_cmpxchg_suc. { destruct list; left; done. }
- iMod (mapsto_persist with "Hl'") as "#Hl'".
+ iMod (pointsto_persist with "Hl'") as "#Hl'".
iMod ("Hclose" with "[HP Hl Hlist]") as "_".
{ iNext; iExists (Some _); iFrame.
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
@@ -362,7 +362,7 @@ Section stack_works.
+ rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
wp_cmpxchg_suc.
- iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
+ iDestruct (pointsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index dc29fcde..233bf783 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -66,7 +66,7 @@ Section stack_works.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
- iDestruct (mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
+ iDestruct (pointsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
@@ -103,7 +103,7 @@ Section stack_works.
iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
- wp_cmpxchg_suc. { destruct list'; left; done. }
- iMod (mapsto_persist with "Hl'") as "#Hl'".
+ iMod (pointsto_persist with "Hl'") as "#Hl'".
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hclose" with "[Hl HP Hlist]") as "_".
{ iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
@@ -162,7 +162,7 @@ Section stack_works.
iDestruct "Hupd" as "[Hupdcons _]".
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
- iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
+ iDestruct (pointsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 8e4a9f14..22224c11 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -289,7 +289,7 @@ Section proofs.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
- iDestruct (mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
+ iDestruct (pointsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
@@ -335,7 +335,7 @@ Section proofs.
iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
* wp_cmpxchg_suc. { destruct list'; left; done. }
- iMod (mapsto_persist with "Hl'") as "#Hl'".
+ iMod (pointsto_persist with "Hl'") as "#Hl'".
iMod (fupd_mask_subseteq inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
@@ -418,7 +418,7 @@ Section proofs.
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
- iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
+ iDestruct (pointsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index a15aee83..684251af 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -78,7 +78,7 @@ Section proof.
destruct ys as [| y ys]; eauto. simpl.
iDestruct 1 as (tl) "(Hro & Hls)".
iDestruct 1 as (tl') "(Hro' & Hls')".
- iDestruct (mapsto_agree with "Hro Hro'") as %?; simplify_eq/=.
+ iDestruct (pointsto_agree with "Hro Hro'") as %?; simplify_eq/=.
iDestruct ("IH" with "Hls Hls'") as %->. done.
Qed.
@@ -157,7 +157,7 @@ Section proof.
iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
destruct (decide (o = o')) as [->|?].
- wp_cmpxchg_suc. { destruct o'; left; done. }
- iMod (mapsto_persist with "Hn") as "#Hn".
+ iMod (pointsto_persist with "Hn") as "#Hn".
iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
{ iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index c75a08b6..c0664a2c 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -208,7 +208,7 @@ Section monotone_counter.
Lemma mcounterRA_update m n: ((â— m â‹… â—¯ n) : mcounterRA) ~~> (â— (1 + m) â‹… â—¯ (1 + n)).
Proof.
(* Use the specialized definition of update, since our RA is a nice one. *)
- apply cmra_discrete_update.
+ apply cmra_discrete_total_update.
intros [[] k].
- rewrite /op /cmra_op !mcounterRA_valid; lia.
- intros [].
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index 4c65e63e..e8d0d507 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -226,10 +226,10 @@ Section conditional_counter.
(** A few more helper lemmas that will come up later *)
- Lemma mapsto_valid_3 l v1 v2 q :
+ Lemma pointsto_valid_3 l v1 v2 q :
l ↦ v1 -∗ l ↦{q} v2 -∗ ⌜FalseâŒ.
Proof.
- iIntros "Hl1 Hl2". iDestruct (mapsto_ne with "Hl1 Hl2") as %?; done.
+ iIntros "Hl1 Hl2". iDestruct (pointsto_ne with "Hl1 Hl2") as %?; done.
Qed.
(** Once a [state] protocol is [done] (as reflected by the [γ_s] token here),
@@ -285,7 +285,7 @@ Section conditional_counter.
(* So, we are [Accepted]. Now we can show that l = l', because
while a [state] protocol is not [done], it owns enough of
the [counter] protocol to ensure that does not move anywhere else. *)
- iDestruct (mapsto_agree with "Hc Hc'") as %[= ->].
+ iDestruct (pointsto_agree with "Hc Hc'") as %[= ->].
(* We perform the CmpXchg. *)
iCombine "Hc Hc'" as "Hc".
wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
@@ -299,7 +299,7 @@ Section conditional_counter.
(* Update state to Done. *)
{ iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
iFrame "#∗". iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
- iDestruct (mapsto_agree with "Hl_ghost Hl_ghost_inv") as %<-.
+ iDestruct (pointsto_agree with "Hl_ghost Hl_ghost_inv") as %<-.
iSplitR "Hl"; iExists _; iFrame. }
iModIntro. iSplitR "HQ".
{ iNext. iDestruct "Hc" as "[Hc1 Hc2]".
@@ -325,7 +325,7 @@ Section conditional_counter.
succeed, and our prophecy would have told us that.
So here we can prove that the prophecy was wrong. *)
iDestruct "NotDone" as "(_ & >Hc' & State)".
- iDestruct (mapsto_agree with "Hc Hc'") as %[=->].
+ iDestruct (pointsto_agree with "Hc Hc'") as %[=->].
iCombine "Hc Hc'" as "Hc".
wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros "!>" (vs' ->). iDestruct "State" as "[Pending | Accepted]".
@@ -338,9 +338,9 @@ Section conditional_counter.
of the [counter]? Impossible, now we will own more than the whole location! *)
iDestruct "Done" as "(_ & _ & >Hl'')".
iDestruct "Hl''" as (v') "Hl''".
- iDestruct (mapsto_combine with "Hl Hl''") as "[Hl _]".
+ iDestruct (pointsto_combine with "Hl Hl''") as "[Hl _]".
rewrite dfrac_op_own Qp.half_half.
- iDestruct (mapsto_valid_3 with "Hl Hl'") as "[]".
+ iDestruct (pointsto_valid_3 with "Hl Hl'") as "[]".
}
(* The CmpXchg fails. *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
@@ -381,7 +381,7 @@ Section conditional_counter.
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[AU >[Hvs Hnâ—]]".
iMod (lc_fupd_elim_later with "Hlc AU") as "AU".
- iMod (inv_mapsto_own_acc_strong with "GC") as "Hgc"; first solve_ndisj.
+ iMod (inv_pointsto_own_acc_strong with "GC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync flag and counter *)
iMod "AU" as (b n2) "[[Hnâ—¯ Hf] [_ Hclose]]".
iDestruct ("Hgc" with "Hf") as "(_ & Hf & Hfclose)".
@@ -415,7 +415,7 @@ Section conditional_counter.
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
by iCombine "Hlghost Hl_ghost'" gives %[??].
- (* we are the failing thread. exploit that [f] is a GC location. *)
- iMod (inv_mapsto_acc with "GC isGC") as (b) "(_ & H↦ & Hclose)"; first solve_ndisj.
+ iMod (inv_pointsto_acc with "GC isGC") as (b) "(_ & H↦ & Hclose)"; first solve_ndisj.
wp_load.
iMod ("Hclose" with "H↦") as "_". iModIntro.
(* close invariant *)
@@ -452,12 +452,12 @@ Section conditional_counter.
iInv counterN as (l'' q2 s) "(>Hc & >Hl & Hrest)".
destruct (decide (l' = l'')) as [<- | Hn].
+ (* CAS succeeds *)
- iDestruct (mapsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
+ iDestruct (pointsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
iDestruct "Hrest" as ">[Hc' Hnâ—]". iCombine "Hc Hc'" as "Hc".
wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
iMod "AU" as (b' n') "[[CC Hf] [Hclose _]]".
- iDestruct (inv_mapsto_own_inv with "Hf") as "#Hgc".
+ iDestruct (inv_pointsto_own_inv with "Hf") as "#Hgc".
iMod ("Hclose" with "[CC Hf]") as "AU"; first by iFrame.
(* Initialize new [state] protocol .*)
iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 72bf3df9..fdb04f94 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -212,7 +212,7 @@ Section stack.
[->%stack_elem_to_val_inj|_].
- (* The CAS succeeded. Update everything accordingly. *)
iMod "AU" as (l') "[Hl' [_ Hclose]]".
- iMod (mapsto_persist with "Hhead_new") as "#Hhead_new".
+ iMod (pointsto_persist with "Hhead_new") as "#Hhead_new".
iCombine "Hsâ— Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hsâ— Hl'") as "[Hsâ— Hl']".
@@ -314,7 +314,7 @@ Section stack.
destruct l as [|v' l]; simpl.
{ (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
iDestruct "Hlist" as (tail' rep') "[>% [>Htail' Hlist]]". simplify_eq.
- iDestruct (mapsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj].
+ iDestruct (pointsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj].
iMod (own_update_2 with "Hsâ— Hl'") as "[Hsâ— Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}".
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index 0eac65e0..6eabb56f 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -43,7 +43,7 @@ Section proofs.
Proof.
iIntros (Φ) "_ HΦ".
wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
- iMod (mapsto_persist with "Hl") as "#Hl".
+ iMod (pointsto_persist with "Hl") as "#Hl".
wp_alloc s as "Hs".
iAssert (∃ xs, is_bag_R N R xs s)%I with "[-HΦ]" as "Hxs".
{ iFrame. iExists [], l.
@@ -68,7 +68,7 @@ Section proofs.
iDestruct "H1" as (xs' hd') "[>Hs H1]".
destruct (decide (hd = hd')) as [->|Hneq].
- wp_cmpxchg_suc.
- iMod (mapsto_persist with "Hl") as "#Hl".
+ iMod (pointsto_persist with "Hl") as "#Hl".
iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
iMod ("Hclose" with "[Hs Hl H1]").
{ iNext. iFrame. iExists (x::xs'), l.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index f18b0726..f95a0c43 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -389,8 +389,8 @@ Section rdcss.
while a [descr] protocol is not [done], it owns enough of
the [rdcss] protocol to ensure that does not move anywhere else. *)
destruct s as [n' | l_descr' l_m' m1' n1' n2' p'].
- { simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
- iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
+ { simpl. iDestruct (pointsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
+ iDestruct (pointsto_agree with "Hln Hln'") as %[= ->].
simpl.
iDestruct "Hrest" as (q Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
(* We perform the CmpXchg. *)
@@ -427,7 +427,7 @@ Section rdcss.
succeed, and our prophecy would have told us that.
So here we can prove that the prophecy was wrong. *)
iDestruct "NotDone" as "(_ & >Hln' & State)".
- iDestruct (mapsto_agree with "Hln Hln'") as %[=->].
+ iDestruct (pointsto_agree with "Hln Hln'") as %[=->].
iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros "!>" (vs'' ->). simpl.
@@ -454,9 +454,9 @@ Section rdcss.
iDestruct "Done" as "(_ & _ & >Hld & _)".
iDestruct "Hld" as (v') "Hld".
iDestruct "Hrest" as (q Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
- iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
+ iDestruct (pointsto_combine with "Hld Hld'") as "[Hld _]".
rewrite dfrac_op_own Qp.half_half.
- by iDestruct (mapsto_ne with "Hld Hld''") as %[].
+ by iDestruct (pointsto_ne with "Hld Hld''") as %[].
+ (* l_descr' ≠l_descr: The CmpXchg fails. *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros "!>" (vs'' ->) "Hp". iModIntro.
@@ -499,7 +499,7 @@ Section rdcss.
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[AU >(Hvs & Hnâ— & Token_a)]".
iMod (lc_fupd_elim_later with "Hlc AU") as "AU".
- iMod (inv_mapsto_own_acc_strong with "InvGC") as "Hgc"; first solve_ndisj.
+ iMod (inv_pointsto_own_acc_strong with "InvGC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync B location l_n and A location l_m *)
iMod "AU" as (m' n') "[CC [_ Hclose]]".
iDestruct "CC" as "[Hgc_lm Hnâ—¯]".
@@ -538,7 +538,7 @@ Section rdcss.
by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
- (* we are the failing thread *)
(* close invariant *)
- iMod (inv_mapsto_acc with "InvGC isGC") as (v) "(_ & Hlm & Hclose)"; first solve_ndisj.
+ iMod (inv_pointsto_acc with "InvGC isGC") as (v) "(_ & Hlm & Hclose)"; first solve_ndisj.
wp_load.
iMod ("Hclose" with "Hlm") as "_". iModIntro.
iModIntro.
@@ -580,7 +580,7 @@ Section rdcss.
wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
iMod "AU" as (b' n') "[[Hf CC] [Hclose _]]".
- iDestruct (inv_mapsto_own_inv with "Hf") as "#Hgc".
+ iDestruct (inv_pointsto_own_inv with "Hf") as "#Hgc".
iMod ("Hclose" with "[Hf CC]") as "AU"; first by iFrame.
(* Initialize new [descr] protocol .*)
iMod (own_alloc (Excl ())) as (γ_t) "Token_t"; first done.
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
index 587ad42a..62930149 100644
--- a/theories/logatom/rdcss/spec.v
+++ b/theories/logatom/rdcss/spec.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
See [rdcss.v] for references and more details about this data structure.
_Note on the use of "invariant" locations_: the specification of the [rdcss]
-operation as given by [rdcss_spec] relies on the [inv_mapsto l_m m] assertion,
+operation as given by [rdcss_spec] relies on the [inv_pointsto l_m m] assertion,
written [l_m ↦_(λ _, True) m]. It roughly corresponds to the usual [l_m ↦ m] but
with an additional guarantee that [l_m] will not be deallocated (and the value
stored there satisfies the given predicate, which is trivial in this case). This
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index e9d22924..bb9e05a6 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -130,7 +130,7 @@ Section atomic_snapshot.
iIntros (Φ _) "Hx". rewrite /new_snapshot. wp_lam.
repeat (wp_proj; wp_let).
wp_alloc lx' as "Hlx'".
- iMod (mapsto_persist with "Hlx'") as "Hlx'".
+ iMod (pointsto_persist with "Hlx'") as "Hlx'".
wp_alloc lx as "Hlx".
set (Excl' v) as p.
iMod (own_alloc (◠p ⋅ ◯ p)) as (γ1) "[Hx⚫ Hx◯]". {
@@ -231,8 +231,8 @@ Section atomic_snapshot.
iDestruct "Ht" as %[Ht Hvt].
destruct (decide (l1'' = l1')) as [-> | Hn].
- wp_cmpxchg_suc.
- iMod (mapsto_persist with "Hl1'new") as "Hl1'new".
- iDestruct (mapsto_agree with "Hl1' Hl1''") as %[= -> ->].
+ iMod (pointsto_persist with "Hl1'new") as "Hl1'new".
+ iDestruct (pointsto_agree with "Hl1' Hl1''") as %[= -> ->].
(* open AU *)
iMod "AU" as (xv) "[Hx [_ Hclose]]".
(* update snapshot ghost state to (x2, y') *)
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
index 5e2d9e3a..a790d9da 100644
--- a/theories/logatom/treiber.v
+++ b/theories/logatom/treiber.v
@@ -52,15 +52,15 @@ Section proof.
+ auto.
+ iIntros "[Hxs Hys] /=".
iDestruct "Hys" as (hd') "[Hhd Hys']".
- by iDestruct (mapsto_agree with "Hxs Hhd") as %?.
+ by iDestruct (pointsto_agree with "Hxs Hhd") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros "[Hxs Hys] /=".
iDestruct "Hxs" as (?) "[Hhd _]".
- by iDestruct (mapsto_agree with "Hhd Hys") as %?.
+ by iDestruct (pointsto_agree with "Hhd Hys") as %?.
+ iIntros "[Hxs Hys] /=".
iDestruct "Hxs" as (?) "[Hhd Hxs']".
iDestruct "Hys" as (?) "[Hhd' Hys']".
- iDestruct (mapsto_agree with "Hhd Hhd'") as %[= -> ->].
+ iDestruct (pointsto_agree with "Hhd Hhd'") as %[= -> ->].
by iDestruct (IHxs' with "[$Hxs' $Hys']") as %->.
Qed.
@@ -77,7 +77,7 @@ Section proof.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_bind (ref NONE)%E. wp_alloc l as "Hl".
- iMod (mapsto_persist with "Hl") as "Hl".
+ iMod (pointsto_persist with "Hl") as "Hl".
wp_alloc l' as "Hl'".
iApply "HΦ". rewrite /is_stack. auto.
Qed.
@@ -94,7 +94,7 @@ Section proof.
iDestruct "Hxs" as (hd) "[Hs Hhd]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by eauto with iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
- iMod (mapsto_persist with "Hl") as "Hl".
+ iMod (pointsto_persist with "Hl") as "Hl".
wp_bind (CmpXchg _ _ _)%E.
iMod "HP" as (xs') "[Hxs' Hvs']".
iDestruct "Hxs'" as (hd') "[Hs' Hhd']".
@@ -138,9 +138,9 @@ Section proof.
destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cmpxchg_suc. iDestruct "Hvs'" as "[_ Hvs']".
destruct xs'' as [|x'' xs'']; simpl.
- { by iDestruct (mapsto_agree with "Hhd Hhd''") as %?. }
+ { by iDestruct (pointsto_agree with "Hhd Hhd''") as %?. }
iDestruct "Hhd''" as (hd''') "[Hhd'' Hxs'']".
- iDestruct (@mapsto_agree with "Hhd Hhd''") as %[= -> ->].
+ iDestruct (@pointsto_agree with "Hhd Hhd''") as %[= -> ->].
iMod ("Hvs'" with "[-]") as "HQ".
{ eauto with iFrame. }
iModIntro. wp_pures. eauto.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index d383d96e..88fc5ab7 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -269,7 +269,7 @@ Proof.
(* Commit operation. *)
iMod ("HClose" with "Hγ◯") as "H".
(* We can eliminate the modality. *)
- iMod (mapsto_persist with "Hr") as "Hr".
+ iMod (pointsto_persist with "Hr") as "Hr".
iModIntro. iSplitR "H"; first by eauto 10 with iFrame.
(* And conclude the proof easily, after some computation steps. *)
wp_pures. iExact "H".
@@ -325,9 +325,9 @@ Proof.
iDestruct (auth_agree with "Hγ◠Hγ◯") as %<-.
(* Update the value of [γ] to [ys] (the tail of previous value). *)
iMod (auth_update γ ys with "Hγ◠Hγ◯") as "[Hγ◠Hγ◯]".
- (* We need to learn that [r = u] (true since mapsto must agree). *)
+ (* We need to learn that [r = u] (true since pointsto must agree). *)
iDestruct "HPhys" as (u) "[Hw' HPhys]".
- iDestruct (mapsto_agree with "Hw Hw'") as %[=-> ->%to_val_inj].
+ iDestruct (pointsto_agree with "Hw Hw'") as %[=-> ->%to_val_inj].
(* Perform the commit. *)
iMod ("HClose" with "Hγ◯") as "HΦ".
(* Eliminate the modality. *)
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
index 862f13f8..7e300a20 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
@@ -47,7 +47,7 @@ Section Stack_refinement.
iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk".
simpl. iApply wp_pure_step_later; trivial. iIntros "!> _". simpl.
iAsimpl.
- iMod (mapsto_persist with "Histk") as "#Histk".
+ iMod (pointsto_persist with "Histk") as "#Histk".
(* establishing the invariant *)
iAssert (StackLink Ï„i (LocV istk, FoldV (InjLV UnitV))) with "[]" as "HLK".
{ rewrite StackLink_unfold.
@@ -107,7 +107,7 @@ Section Stack_refinement.
{ rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
iApply (wp_cas_suc with "Hstk"); auto.
iNext. iIntros "Hstk".
- iMod (mapsto_persist with "Hltmp") as "#Hltmp".
+ iMod (pointsto_persist with "Hltmp") as "#Hltmp".
iMod ("Hclose" with "[-Hj]") as "_".
{ iNext. iExists ltmp, _.
iFrame "Hstk' Hstk Hl".
@@ -196,7 +196,7 @@ Section Stack_refinement.
iNext. iIntros "Hstk {HLK'}". iPoseProof "HLK" as "HLK'".
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as (istk4 w2) "[% [Hmpt' HLK']]"; simplify_eq/=.
- iDestruct (mapsto_agree with "Hmpt Hmpt'") as %<-.
+ iDestruct (pointsto_agree with "Hmpt Hmpt'") as %<-.
iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
"[% [% [#Hrel HLK'']]]"; simplify_eq/=.
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 21685ff1..2bbba4ce 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -30,10 +30,10 @@ Class cfgSG Σ := CFGSG { cfg_inG :: inG Σ (authR cfgUR); cfg_name : gname }.
Section definitionsS.
Context `{cfgSG Σ, invGS Σ}.
- Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
+ Definition heapS_pointsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name (◯ (ε, {[ l := (q, to_agree v) ]})).
- Definition tpool_mapsto (j : nat) (e: expr) : iProp Σ :=
+ Definition tpool_pointsto (j : nat) (e: expr) : iProp Σ :=
own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
Definition spec_inv (Ï : cfg F_mu_ref_conc_lang) : iProp Σ :=
@@ -42,17 +42,17 @@ Section definitionsS.
Definition spec_ctx : iProp Σ :=
(∃ Ï, inv specN (spec_inv Ï))%I.
- Global Instance heapS_mapsto_timeless l q v : Timeless (heapS_mapsto l q v).
+ Global Instance heapS_pointsto_timeless l q v : Timeless (heapS_pointsto l q v).
Proof. apply _. Qed.
Global Instance spec_ctx_persistent : Persistent spec_ctx.
Proof. apply _. Qed.
End definitionsS.
-Global Typeclasses Opaque heapS_mapsto tpool_mapsto.
+Global Typeclasses Opaque heapS_pointsto tpool_pointsto.
-Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
+Notation "l ↦ₛ{ q } v" := (heapS_pointsto l q v)
(at level 20, q at level 50, format "l ↦ₛ{ q } v") : bi_scope.
-Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : bi_scope.
-Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : bi_scope.
+Notation "l ↦ₛ v" := (heapS_pointsto l 1 v) (at level 20) : bi_scope.
+Notation "j ⤇ e" := (tpool_pointsto j e) (at level 20) : bi_scope.
Ltac iAsimpl :=
repeat match goal with
@@ -166,7 +166,7 @@ Section cfg.
Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2âŒ.
Proof.
apply entails_wand, wand_intro_r.
- rewrite /heapS_mapsto -own_op own_valid uPred.discrete_valid. f_equiv.
+ rewrite /heapS_pointsto -own_op own_valid uPred.discrete_valid. f_equiv.
rewrite auth_frag_op_valid -pair_op singleton_op -pair_op.
rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L.
by intros [_ [_ [=]]].
@@ -175,11 +175,11 @@ Section cfg.
l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ l ↦ₛ{q1 + q2} v1 ∗ ⌜v1 = v2âŒ.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapstoS_agree with "Hl1 Hl2") as %->.
- rewrite /heapS_mapsto. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+ rewrite /heapS_pointsto. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
Qed.
Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
Proof.
- rewrite /heapS_mapsto own_valid !discrete_valid auth_frag_valid.
+ rewrite /heapS_pointsto own_valid !discrete_valid auth_frag_valid.
by apply entails_wand, pure_mono=> -[_] /singleton_valid [??].
Qed.
Lemma mapstoS_valid_2 l q1 q2 v1 v2 :
@@ -198,7 +198,7 @@ Section cfg.
Qed.
Lemma step_insert K tp j e σ κ e' σ' efs :
- tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs →
+ tp !! j = Some (fill K e) → base_step e σ κ e' σ' efs →
erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
Proof.
intros. rewrite -(take_drop_middle tp j (fill K e)) //.
@@ -209,7 +209,7 @@ Section cfg.
Qed.
Lemma step_insert_no_fork K tp j e σ κ e' σ' :
- tp !! j = Some (fill K e) → head_step e σ κ e' σ' [] →
+ tp !! j = Some (fill K e) → base_step e σ κ e' σ' [] →
erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
@@ -232,7 +232,7 @@ Section cfg.
spec_ctx ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
Proof.
iIntros (HP Hex ?) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hspec".
- rewrite /spec_ctx /tpool_mapsto.
+ rewrite /spec_ctx /tpool_pointsto.
iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
iDestruct "Hrtc" as %Hrtc.
iCombine "Hown Hj" gives
@@ -281,7 +281,7 @@ Section cfg.
spec_ctx ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
Proof.
iIntros (??) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto.
+ rewrite /spec_ctx /tpool_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom σ)) as [l Hl%not_elem_of_dom].
iCombine "Hown Hj"
@@ -294,7 +294,7 @@ Section cfg.
{ eapply auth_update_alloc, prod_local_update_2,
(alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
by apply lookup_to_heap_None. }
- iExists l. rewrite /heapS_mapsto. iFrame "Hj Hl". iApply "Hclose". iNext.
+ iExists l. rewrite /heapS_pointsto. iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (Loc l)]> tp), (<[l:=v]>σ).
rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
@@ -306,7 +306,7 @@ Section cfg.
={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+ rewrite /spec_ctx /tpool_pointsto /heapS_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
@@ -327,7 +327,7 @@ Section cfg.
={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+ rewrite /spec_ctx /tpool_pointsto /heapS_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _]
@@ -354,7 +354,7 @@ Section cfg.
={E}=∗ j ⤇ fill K (#♠false) ∗ l ↦ₛ{q} v'.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+ rewrite /spec_ctx /tpool_pointsto /heapS_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _]%prod_included ?]
@@ -376,7 +376,7 @@ Section cfg.
={E}=∗ j ⤇ fill K (#♠true) ∗ l ↦ₛ v2.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+ rewrite /spec_ctx /tpool_pointsto /heapS_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _]%prod_included _]
@@ -403,7 +403,7 @@ Section cfg.
={E}=∗ j ⤇ fill K (#n m) ∗ l ↦ₛ #nv (m + k).
Proof.
iIntros (??) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+ rewrite /spec_ctx /tpool_pointsto /heapS_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _]%prod_included _]
@@ -506,7 +506,7 @@ Section cfg.
spec_ctx ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e.
Proof.
iIntros (?) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hinv".
- rewrite /spec_ctx /tpool_mapsto.
+ rewrite /spec_ctx /tpool_pointsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iCombine "Hown Hj"
gives %[[?%tpool_singleton_included' _] %prod_included ?]
diff --git a/theories/logrel/F_mu_ref_conc/binary/soundness.v b/theories/logrel/F_mu_ref_conc/binary/soundness.v
index d17fc858..003f9cd0 100644
--- a/theories/logrel/F_mu_ref_conc/binary/soundness.v
+++ b/theories/logrel/F_mu_ref_conc/binary/soundness.v
@@ -40,10 +40,10 @@ Proof.
simpl.
replace e with e.[env_subst[]] at 2 by by asimpl.
iApply ("Hrel" $! 0 []).
- { rewrite /tpool_mapsto. asimpl. by iFrame. }
+ { rewrite /tpool_pointsto. asimpl. by iFrame. }
- iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
- rewrite /tpool_mapsto /=.
+ rewrite /tpool_pointsto /=.
iCombine "Hown Hj" gives %Hvalid.
move: Hvalid=> /auth_both_valid_discrete
[/prod_included [/tpool_singleton_included Hv2 _] _].
diff --git a/theories/logrel/F_mu_ref_conc/lang.v b/theories/logrel/F_mu_ref_conc/lang.v
index d000a33f..44012e02 100644
--- a/theories/logrel/F_mu_ref_conc/lang.v
+++ b/theories/logrel/F_mu_ref_conc/lang.v
@@ -199,82 +199,82 @@ Module F_mu_ref_conc.
Definition state : Type := gmap loc val.
- Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
+ Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2 →
- head_step (App (Rec e1) e2) σ [] e1.[(Rec e1), e2/] σ []
+ base_step (App (Rec e1) e2) σ [] e1.[(Rec e1), e2/] σ []
(* Lam-β *)
| LamBetaS e1 e2 v2 σ :
to_val e2 = Some v2 →
- head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
+ base_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
(* LetIn-β *)
| LetInBetaS e1 e2 v2 σ :
to_val e1 = Some v2 →
- head_step (LetIn e1 e2) σ [] e2.[e1/] σ []
+ base_step (LetIn e1 e2) σ [] e2.[e1/] σ []
(* Seq-β *)
| SeqBetaS e1 e2 v2 σ :
to_val e1 = Some v2 →
- head_step (Seq e1 e2) σ [] e2 σ []
+ base_step (Seq e1 e2) σ [] e2 σ []
(* Products *)
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- head_step (Fst (Pair e1 e2)) σ [] e1 σ []
+ base_step (Fst (Pair e1 e2)) σ [] e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- head_step (Snd (Pair e1 e2)) σ [] e2 σ []
+ base_step (Snd (Pair e1 e2)) σ [] e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
- head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
+ base_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
- head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
+ base_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
(* nat bin op *)
| BinOpS op a b σ :
- head_step (BinOp op (#n a) (#n b)) σ [] (of_val (binop_eval op a b)) σ []
+ base_step (BinOp op (#n a) (#n b)) σ [] (of_val (binop_eval op a b)) σ []
(* If then else *)
| IfFalse e1 e2 σ :
- head_step (If (#♠false) e1 e2) σ [] e2 σ []
+ base_step (If (#♠false) e1 e2) σ [] e2 σ []
| IfTrue e1 e2 σ :
- head_step (If (#♠true) e1 e2) σ [] e1 σ []
+ base_step (If (#♠true) e1 e2) σ [] e1 σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v →
- head_step (Unfold (Fold e)) σ [] e σ []
+ base_step (Unfold (Fold e)) σ [] e σ []
(* Polymorphic Types *)
| TBeta e σ :
- head_step (TApp (TLam e)) σ [] e σ []
+ base_step (TApp (TLam e)) σ [] e σ []
(* Existential Types *)
| UnpackS e1 v e2 σ :
to_val e1 = Some v →
- head_step (UnpackIn (Pack e1) e2) σ [] e2.[e1/] σ []
+ base_step (UnpackIn (Pack e1) e2) σ [] e2.[e1/] σ []
(* Concurrency *)
| ForkS e σ:
- head_step (Fork e) σ [] Unit σ [e]
+ base_step (Fork e) σ [] Unit σ [e]
(* Reference Types *)
| AllocS e v σ l :
to_val e = Some v → σ !! l = None →
- head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) []
+ base_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) []
| LoadS l v σ :
σ !! l = Some v →
- head_step (Load (Loc l)) σ [] (of_val v) σ []
+ base_step (Load (Loc l)) σ [] (of_val v) σ []
| StoreS l e v σ :
to_val e = Some v → is_Some (σ !! l) →
- head_step (Store (Loc l) e) σ [] Unit (<[l:=v]>σ) []
+ base_step (Store (Loc l) e) σ [] Unit (<[l:=v]>σ) []
(* Compare and swap *)
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ !! l = Some vl → vl ≠v1 →
- head_step (CAS (Loc l) e1 e2) σ [] (#♠false) σ []
+ base_step (CAS (Loc l) e1 e2) σ [] (#♠false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ !! l = Some v1 →
- head_step (CAS (Loc l) e1 e2) σ [] (#♠true) (<[l:=v2]>σ) []
+ base_step (CAS (Loc l) e1 e2) σ [] (#♠true) (<[l:=v2]>σ) []
| FAAS l m e2 k σ :
to_val e2 = Some (NatV k) →
σ !! l = Some (NatV m) →
- head_step (FAA (Loc l) e2) σ [] (#n m) (<[l:=NatV (m + k)]>σ) [].
+ base_step (FAA (Loc l) e2) σ [] (#n m) (<[l:=NatV (m + k)]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -296,11 +296,11 @@ Module F_mu_ref_conc.
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
Lemma val_stuck e1 σ1 κs e2 σ2 ef :
- head_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
+ base_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
- Lemma head_ctx_step_val Ki e σ1 κs e2 σ2 ef :
- head_step (fill_item Ki e) σ1 κs e2 σ2 ef → is_Some (to_val e).
+ Lemma base_ctx_step_val Ki e σ1 κs e2 σ2 ef :
+ base_step (fill_item Ki e) σ1 κs e2 σ2 ef → is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -315,16 +315,16 @@ Module F_mu_ref_conc.
Lemma alloc_fresh e v σ :
let l := fresh (dom σ) in
- to_val e = Some v → head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) [].
+ to_val e = Some v → base_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
- Lemma val_head_stuck e1 σ1 κs e2 σ2 efs : head_step e1 σ1 κs e2 σ2 efs → to_val e1 = None.
+ Lemma val_base_stuck e1 σ1 κs e2 σ2 efs : base_step e1 σ1 κs e2 σ2 efs → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
- Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+ Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof.
- split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
- fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+ split; apply _ || eauto using to_of_val, of_to_val, val_base_stuck,
+ fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
Qed.
Canonical Structure stateO := leibnizO state.
diff --git a/theories/logrel/F_mu_ref_conc/wp_rules.v b/theories/logrel/F_mu_ref_conc/wp_rules.v
index f180433b..b0d7b9e0 100644
--- a/theories/logrel/F_mu_ref_conc/wp_rules.v
+++ b/theories/logrel/F_mu_ref_conc/wp_rules.v
@@ -22,13 +22,13 @@ Global Instance heapIG_irisG `{heapIG Σ} : irisGS F_mu_ref_conc_lang Σ := {
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
-Notation "l ↦ᵢ{ dq } v" := (mapsto (L:=loc) (V:=val) l dq v)
+Notation "l ↦ᵢ{ dq } v" := (pointsto (L:=loc) (V:=val) l dq v)
(at level 20, format "l ↦ᵢ{ dq } v") : bi_scope.
-Notation "l ↦ᵢ□ v" := (mapsto (L:=loc) (V:=val) l DfracDiscarded v)
+Notation "l ↦ᵢ□ v" := (pointsto (L:=loc) (V:=val) l DfracDiscarded v)
(at level 20, format "l ↦ᵢ□ v") : bi_scope.
-Notation "l ↦ᵢ{# q } v" := (mapsto (L:=loc) (V:=val) l (DfracOwn q) v)
+Notation "l ↦ᵢ{# q } v" := (pointsto (L:=loc) (V:=val) l (DfracOwn q) v)
(at level 20, format "l ↦ᵢ{# q } v") : bi_scope.
-Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l (DfracOwn 1) v)
+Notation "l ↦ᵢ v" := (pointsto (L:=loc) (V:=val) l (DfracOwn 1) v)
(at level 20, format "l ↦ᵢ v") : bi_scope.
Section lang_rules.
@@ -39,22 +39,22 @@ Section lang_rules.
Implicit Types e : expr.
Implicit Types v w : val.
- Ltac inv_head_step :=
+ Ltac inv_base_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
- | H : head_step ?e _ _ _ _ _ |- _ =>
+ | H : base_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Local Hint Extern 0 (atomic _) => solve_atomic : core.
- Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
+ Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
- Local Hint Constructors head_step : core.
+ Local Hint Constructors base_step : core.
Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val : core.
@@ -63,9 +63,9 @@ Section lang_rules.
IntoVal e v →
{{{ True }}} Alloc e @ E {{{ l, RET (LocV l); l ↦ᵢ v }}}.
Proof.
- iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>"; iSplit; first by auto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -73,10 +73,10 @@ Section lang_rules.
Lemma wp_load E l dq v :
{{{ ▷ l ↦ᵢ{dq} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{dq} v }}}.
Proof.
- iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -86,9 +86,9 @@ Section lang_rules.
{{{ RET UnitV; l ↦ᵢ v }}}.
Proof.
iIntros (<- Φ) ">Hl HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
@@ -99,10 +99,10 @@ Section lang_rules.
{{{ RET (BoolV false); l ↦ᵢ{dq} v' }}}.
Proof.
iIntros (<- <- ? Φ) ">Hl HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
- iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -112,9 +112,9 @@ Section lang_rules.
{{{ RET (BoolV true); l ↦ᵢ v2 }}}.
Proof.
iIntros (<- <- Φ) ">Hl HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_head_step.
+ iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_base_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
@@ -125,9 +125,9 @@ Section lang_rules.
{{{ RET (#nv m); l ↦ᵢ #nv (m + k) }}}.
Proof.
iIntros (<- Φ) ">Hl HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ????) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_head_step.
+ iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep) "_"; inv_base_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
@@ -135,17 +135,17 @@ Section lang_rules.
Lemma wp_fork E e Φ :
▷ (|={E}=> Φ UnitV) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
Proof.
- iIntros "[He HΦ]". iApply wp_lift_atomic_head_step; [done|].
+ iIntros "[He HΦ]". iApply wp_lift_atomic_base_step; [done|].
iIntros (σ1 ????) "Hσ !>"; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step. by iFrame.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. by iFrame.
Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
- Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
+ Local Ltac solve_exec_puredet := simpl; intros; by inv_base_step.
Local Ltac solve_pure_exec :=
unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
- intros ?; apply nsteps_once, pure_head_step_pure_step;
+ intros ?; apply nsteps_once, pure_base_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_rec e1 e2 `{!AsVal e2} :
diff --git a/theories/logrel/stlc/lang.v b/theories/logrel/stlc/lang.v
index ba7ef613..392a236e 100644
--- a/theories/logrel/stlc/lang.v
+++ b/theories/logrel/stlc/lang.v
@@ -77,22 +77,22 @@ Module stlc.
Definition state : Type := ().
- Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
+ Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2 →
- head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
+ base_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- head_step (Fst (Pair e1 e2)) σ [] e1 σ []
+ base_step (Fst (Pair e1 e2)) σ [] e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- head_step (Snd (Pair e1 e2)) σ [] e2 σ []
+ base_step (Snd (Pair e1 e2)) σ [] e2 σ []
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
- head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
+ base_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
- head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ [].
+ base_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -114,11 +114,11 @@ Module stlc.
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
Lemma val_stuck e1 σ1 κ e2 σ2 ef :
- head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
+ base_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
- Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
- head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
+ Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 ef :
+ base_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -131,13 +131,13 @@ Module stlc.
end; auto.
Qed.
- Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
+ Lemma val_base_stuck e1 σ1 κ e2 σ2 efs : base_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
- Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+ Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof.
- split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
- fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+ split; apply _ || eauto using to_of_val, of_to_val, val_base_stuck,
+ fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
Qed.
End stlc.
diff --git a/theories/logrel/stlc/rules.v b/theories/logrel/stlc/rules.v
index b64881d6..42bf71b0 100644
--- a/theories/logrel/stlc/rules.v
+++ b/theories/logrel/stlc/rules.v
@@ -12,26 +12,26 @@ Section stlc_rules.
Context `{irisGS stlc_lang Σ}.
Implicit Types e : expr.
- Ltac inv_head_step :=
+ Ltac inv_base_step :=
repeat match goal with
| H : to_val _ = Some _ |- _ => apply of_to_val in H
- | H : head_step ?e _ _ _ _ _ |- _ =>
+ | H : base_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
- Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
+ Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
- Local Hint Constructors head_step : core.
+ Local Hint Constructors base_step : core.
Local Hint Resolve to_of_val : core.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
- Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
+ Local Ltac solve_exec_puredet := simpl; intros; by inv_base_step.
Local Ltac solve_pure_exec :=
unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
- intros ?; apply nsteps_once, pure_head_step_pure_step;
+ intros ?; apply nsteps_once, pure_base_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
(** Helper Lemmas for weakestpre. *)
--
GitLab