From a8425b708ec51d918d5cf6eb3ab6fde88f4e2c2a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Dec 2020 13:35:23 +0100
Subject: [PATCH] Bump Iris (persistent mapsto).
---
coq-iris-examples.opam | 2 +-
theories/barrier/example_client.v | 2 +-
.../concurrent_stacks/concurrent_stack1.v | 27 ++---
.../concurrent_stacks/concurrent_stack2.v | 24 ++--
.../concurrent_stacks/concurrent_stack3.v | 38 ++-----
.../concurrent_stacks/concurrent_stack4.v | 38 ++-----
theories/hocap/fg_bag.v | 27 ++---
theories/lecture_notes/ccounter.v | 2 +-
theories/lecture_notes/coq_intro_example_2.v | 2 +-
theories/logatom/conditional_increment/cinc.v | 15 +--
theories/logatom/elimination_stack/stack.v | 15 +--
theories/logatom/flat_combiner/flat.v | 15 ++-
theories/logatom/flat_combiner/peritem.v | 25 ++---
theories/logatom/rdcss/rdcss.v | 19 ++--
theories/logatom/snapshot/atomic_snapshot.v | 41 ++++---
theories/logatom/treiber.v | 75 +++++--------
theories/logatom/treiber2.v | 27 ++---
.../F_mu_ref_conc/examples/stack/refinement.v | 106 ++++++++----------
.../examples/stack/stack_rules.v | 76 +------------
theories/logrel/F_mu_ref_conc/rules.v | 21 ++--
20 files changed, 203 insertions(+), 394 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index f09b5a9e..e8569924 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"
depends: [
- "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2020-12-18.1.afe51813") | (= "dev") }
"coq-autosubst" { = "dev" }
"coq-iris-string-ident"
]
diff --git a/theories/barrier/example_client.v b/theories/barrier/example_client.v
index c93ddb48..39e74ca6 100644
--- a/theories/barrier/example_client.v
+++ b/theories/barrier/example_client.v
@@ -20,7 +20,7 @@ Section client.
Definition N := nroot .@ "barrier".
Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
- (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌠}})%I.
+ (∃ f : val, l ↦{# q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌠}})%I.
Lemma y_inv_split q l : y_inv q l -∗ (y_inv (q/2) l ∗ y_inv (q/2) l).
Proof.
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index 44ae7cd3..393623b6 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -27,15 +27,6 @@ Section stacks.
Context `{!heapG Σ} (N : namespace).
Implicit Types l : loc.
- Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
- (at level 20, format "l ↦{-} v") : bi_scope.
-
- Lemma partial_mapsto_duplicable l v :
- l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
- Proof.
- iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
- Qed.
-
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -47,7 +38,7 @@ Section stacks.
Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iPropO Σ) :
option loc -d> iPropO Σ := λ v, match v with
| None => True
- | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+ | Some l => ∃ (h : val) (t : option loc), l ↦□ (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
end%I.
Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
@@ -71,14 +62,13 @@ Section stacks.
Lemma is_list_dup (P : val → iProp Σ) v :
is_list P v -∗ is_list P v ∗ match v with
| None => True
- | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+ | Some l => ∃ h t, l ↦□ (h, oloc_to_val t)%V
end.
Proof.
iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
destruct v as [l|].
- - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
- iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
- rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+ - iDestruct "Hstack" as (h t) "(#Hl & ? & ?)".
+ rewrite (is_list_unfold _ (Some _)). iSplitL; iExists _, _; by iFrame.
- rewrite is_list_unfold; iSplitR; eauto.
Qed.
@@ -114,9 +104,10 @@ 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 ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (Some â„“'); iFrame; iSplit; first done;
- rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
+ rewrite (is_list_unfold _ (Some _)) /=. eauto with iFrame. }
iModIntro.
wp_pures.
by iApply "HΦ".
@@ -147,7 +138,7 @@ Section stacks.
iApply "HΦ"; by iLeft.
- wp_match. wp_bind (Load _).
iInv N as (â„“' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
- iDestruct "Hlist2" as (???) "Hl".
+ iDestruct "Hlist2" as (??) "Hl".
wp_load.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
@@ -156,9 +147,7 @@ Section stacks.
iInv N as (â„“'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
destruct (decide (v'' = (Some l))) as [-> |].
* rewrite is_list_unfold.
- iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
- iDestruct "Hl''" as (q') "Hl''".
- simpl.
+ iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist) /=".
wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl' Hlist]") as "_".
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 1b36d8de..03e4c6d1 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -234,15 +234,6 @@ Section stack_works.
Definition Nmailbox := N .@ "mailbox".
- Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
- (at level 20, format "l ↦{-} v") : bi_scope.
-
- Lemma partial_mapsto_duplicable l v :
- l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
- Proof.
- iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
- Qed.
-
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -254,7 +245,7 @@ Section stack_works.
Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iPropO Σ) :
option loc -d> iPropO Σ := λ v, match v with
| None => True
- | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+ | Some l => ∃ (h : val) (t : option loc), l ↦□ (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
end%I.
Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
@@ -278,14 +269,13 @@ Section stack_works.
Lemma is_list_dup (P : val → iProp Σ) v :
is_list P v -∗ is_list P v ∗ match v with
| None => True
- | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+ | Some l => ∃ h t, l ↦□ (h, oloc_to_val t)%V
end.
Proof.
iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
destruct v as [l|].
- - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
- iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
- rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+ - iDestruct "Hstack" as (h t) "[#Hl Hlist]".
+ rewrite (is_list_unfold _ (Some _)); iSplitL; iExists _, _; by iFrame.
- rewrite is_list_unfold; iSplitR; eauto.
Qed.
@@ -326,7 +316,8 @@ Section stack_works.
iInv N as (list) "(Hl & Hlist)" "Hclose".
destruct (decide (v'' = list)) as [ -> |].
* wp_cmpxchg_suc. { destruct list; left; done. }
- iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
+ iMod (mapsto_persist with "Hl'") as "#Hl'".
+ iMod ("Hclose" with "[HP Hl Hlist]") as "_".
{ iNext; iExists (Some _); iFrame.
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
@@ -364,7 +355,7 @@ Section stack_works.
iApply "HΦ"; by iLeft.
* wp_match. wp_bind (Load _).
iInv N as (v') "[>Hl Hlist]" "Hclose".
- iDestruct "Hlist2" as (???) "Hl'".
+ iDestruct "Hlist2" as (??) "Hl'".
wp_load.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
@@ -374,7 +365,6 @@ Section stack_works.
destruct (decide (v'' = Some list)) as [-> |].
+ rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
- iDestruct "Hl''" as (q') "Hl''".
wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
iMod ("Hclose" with "[Hl Hlist]") as "_".
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index c8959227..a10d7fa0 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -26,24 +26,6 @@ Section stack_works.
Context `{!heapG Σ} (N : namespace).
Implicit Types l : loc.
- Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
- (at level 20, format "l ↦{-} v") : bi_scope.
-
- Lemma partial_mapsto_duplicable l v :
- l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
- Proof.
- iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
- Qed.
-
- Lemma partial_mapsto_agree l v1 v2 :
- l ↦{-} v1 -∗ l ↦{-} v2 -∗ ⌜v1 = v2âŒ.
- Proof.
- iIntros "H1 H2".
- iDestruct "H1" as (?) "H1".
- iDestruct "H2" as (?) "H2".
- iApply (mapsto_agree with "H1 H2").
- Qed.
-
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -55,20 +37,19 @@ Section stack_works.
Fixpoint is_list xs v : iProp Σ :=
(match xs, v with
| [], None => True
- | x :: xs, Some l => ∃ t, l ↦{-} (x, oloc_to_val t)%V ∗ is_list xs t
+ | x :: xs, Some l => ∃ t, l ↦□ (x, oloc_to_val t)%V ∗ is_list xs t
| _, _ => False
end)%I.
Lemma is_list_dup xs v :
is_list xs v -∗ is_list xs v ∗ match v with
| None => True
- | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+ | Some l => ∃ h t, l ↦□ (h, oloc_to_val t)%V
end.
Proof.
destruct xs, v; simpl; auto; first by iIntros "[]".
- iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
- iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
- iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
+ iIntros "H"; iDestruct "H" as (t) "[#Hl Hstack]".
+ iSplitL; first by (iExists _; iFrame). by iExists _, _.
Qed.
Lemma is_list_empty xs :
@@ -78,13 +59,13 @@ Section stack_works.
Qed.
Lemma is_list_cons xs l h t :
- l ↦{-} (h, t)%V -∗
+ l ↦□ (h, t)%V -∗
is_list xs (Some l) -∗
∃ ys, ⌜xs = h :: ysâŒ.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
- iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
+ iDestruct (mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
@@ -121,8 +102,9 @@ 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 ("Hupd" with "HP") as "[HP HΨ]".
- iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
+ iMod ("Hclose" with "[Hl HP Hlist]") as "_".
{ iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_pures.
@@ -166,7 +148,6 @@ Section stack_works.
iModIntro.
wp_match. wp_bind (Load _).
iInv N as (v xs') "(Hl & Hlist & HP)" "Hclose".
- iDestruct "Hl'" as (q) "Hl'".
wp_load.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
@@ -175,12 +156,11 @@ Section stack_works.
iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
* wp_cmpxchg_suc.
- iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
+ iDestruct (is_list_cons with "Hl' Hlist") as (ys) "%".
simplify_eq.
iDestruct "Hupd" as "[Hupdcons _]".
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
- iDestruct "Hl''" as (q') "Hl''".
iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 0d600a2b..82403214 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -248,24 +248,6 @@ Section proofs.
iIntros (v'') "H"; iApply "HΦ"; auto.
Qed.
- Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
- (at level 20, format "l ↦{-} v") : bi_scope.
-
- Lemma partial_mapsto_duplicable l v :
- l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
- Proof.
- iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
- Qed.
-
- Lemma partial_mapsto_agree l v1 v2 :
- l ↦{-} v1 -∗ l ↦{-} v2 -∗ ⌜v1 = v2âŒ.
- Proof.
- iIntros "H1 H2".
- iDestruct "H1" as (?) "H1".
- iDestruct "H2" as (?) "H2".
- iApply (mapsto_agree with "H1 H2").
- Qed.
-
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -277,20 +259,19 @@ Section proofs.
Fixpoint is_list xs v : iProp Σ :=
(match xs, v with
| [], None => True
- | x :: xs, Some l => ∃ t, l ↦{-} (x, oloc_to_val t)%V ∗ is_list xs t
+ | x :: xs, Some l => ∃ t, l ↦□ (x, oloc_to_val t)%V ∗ is_list xs t
| _, _ => False
end)%I.
Lemma is_list_dup xs v :
is_list xs v -∗ is_list xs v ∗ match v with
| None => True
- | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+ | Some l => ∃ h t, l ↦□ (h, oloc_to_val t)%V
end.
Proof.
destruct xs, v; simpl; auto; first by iIntros "[]".
- iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
- iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
- iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
+ iIntros "H"; iDestruct "H" as (t) "[#Hl Hstack]".
+ iSplitL; first by (iExists _; iFrame). by iExists _, _.
Qed.
Lemma is_list_empty xs :
@@ -300,13 +281,13 @@ Section proofs.
Qed.
Lemma is_list_cons xs l h t :
- l ↦{-} (h, t)%V -∗
+ l ↦□ (h, t) -∗
is_list xs (Some l) -∗
∃ ys, ⌜xs = h :: ysâŒ.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
- iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
+ iDestruct (mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
@@ -352,10 +333,11 @@ 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 (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
- iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
+ iMod ("Hclose" with "[Hl HP Hlist]") as "_".
{ iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_pures.
@@ -419,7 +401,6 @@ Section proofs.
iModIntro.
wp_match. wp_bind (Load _).
iInv Nstack as (v xs') "(Hl & Hlist & HP)" "Hclose".
- iDestruct "Hl'" as (q) "Hl'".
wp_load.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
@@ -428,14 +409,13 @@ Section proofs.
iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
+ wp_cmpxchg_suc.
- iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
+ iDestruct (is_list_cons with "Hl' Hlist") as (ys) "%".
simplify_eq.
iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iDestruct "Hupd" as "[Hupdcons _]".
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
- iDestruct "Hl''" as (q') "Hl''".
iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 3db9c0cb..e61ad729 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -44,11 +44,6 @@ Section proof.
Context `{heapG Σ, bagG Σ}.
Variable N : namespace.
- Definition rown (l : loc) (v : val) :=
- (∃ q, l ↦{q} v)%I.
- Lemma rown_duplicate l v : rown l v -∗ rown l v ∗ rown l v.
- Proof. iDestruct 1 as (q) "[Hl Hl']". iSplitL "Hl"; iExists _; eauto. Qed.
-
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
@@ -61,7 +56,7 @@ Section proof.
match xs, hd with
| [], None => True
| x::xs, Some l => ∃ (tl : option loc),
- rown l (x, oloc_to_val tl) ∗ is_list tl xs
+ l ↦□ (x, oloc_to_val tl) ∗ is_list tl xs
| _, _ => False
end%I.
@@ -69,8 +64,7 @@ Section proof.
Proof.
iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto.
destruct hd; last by auto.
- iDestruct 1 as (tl) "[Hro Htl]".
- rewrite rown_duplicate. iDestruct "Hro" as "[Hro Hro']".
+ iDestruct 1 as (tl) "[#Hro Htl]".
iDestruct ("IH" with "Htl") as "[Htl Htl']".
iSplitL "Hro Htl"; iExists _; iFrame; eauto.
Qed.
@@ -84,10 +78,7 @@ Section proof.
destruct ys as [| y ys]; eauto. simpl.
iDestruct 1 as (tl) "(Hro & Hls)".
iDestruct 1 as (tl') "(Hro' & Hls')".
- iDestruct "Hro" as (q) "Hro".
- iDestruct "Hro'" as (q') "Hro'".
- iDestruct (mapsto_agree l q q' (PairV x (oloc_to_val tl)) (PairV y (oloc_to_val tl'))
- with "Hro Hro'") as %?. simplify_eq/=.
+ iDestruct (mapsto_agree l with "Hro Hro'") as %?; simplify_eq/=.
iDestruct ("IH" with "Hls Hls'") as %->. done.
Qed.
@@ -166,10 +157,11 @@ 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 ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
{ iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
- simpl. iExists _. iFrame. by iExists 1%Qp. }
+ simpl. iExists _. by iFrame. }
iModIntro. wp_pures. by iApply "HΦ".
- wp_cmpxchg_fail.
{ destruct o, o'; simpl; congruence. }
@@ -206,14 +198,11 @@ Section proof.
iModIntro. repeat wp_pure _.
by iApply "HΦ".
- destruct o as [hd|]; last done.
- iDestruct "Hls" as (tl) "(Hhd & Hls)"; simplify_eq/=.
- rewrite rown_duplicate. iDestruct "Hhd" as "[Hhd Hhd']".
+ iDestruct "Hls" as (tl) "[#Hhd Hls]"; simplify_eq/=.
rewrite is_list_duplicate. iDestruct "Hls" as "[Hls Hls']".
iMod ("Hcl" with "[Ho Hb Hhd Hls]") as "_".
- { iNext. iExists (Some _),(x::ls). simpl; iFrame; eauto.
- iExists _; eauto. by iFrame. }
+ { iNext. iExists (Some _),(x::ls). simpl; iFrame; eauto. }
iModIntro. repeat wp_pure _.
- iDestruct "Hhd'" as (q) "Hhd".
wp_load. wp_pures.
wp_bind (CmpXchg _ _ _).
iInv N as (o' ls') "[Ho [Hls >Hb]]" "Hcl".
@@ -222,7 +211,7 @@ Section proof.
(* The list is still the same *)
rewrite (is_list_duplicate tl). iDestruct "Hls'" as "[Hls' Htl]".
iAssert (is_list (Some hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
- { simpl. iExists tl. iFrame. iExists q. iFrame. }
+ { simpl. iExists tl. by iFrame. }
iDestruct (is_list_agree with "Hls Hls'") as %?. simplify_eq.
iClear "Hls'".
iDestruct "Hls" as (tl') "(Hro' & Htl')".
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index 39d1ecd2..33f8ac0f 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -20,7 +20,7 @@ Section ccounter.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
- by apply nat_included, (frac_auth_included_total q).
+ apply nat_included. by apply: (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): ✓ (â—F m â‹… â—¯F n) → n = m.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index a35bcd31..c64ed5e8 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -557,7 +557,7 @@ Section ccounter.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
- by apply nat_included, (frac_auth_included_total q).
+ apply nat_included. by apply: (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): ✓ (â—F m â‹… â—¯F n) → (n = m)%nat.
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index 91adf546..d6181064 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -159,7 +159,7 @@ Section conditional_counter.
(* After the prophecy said we are going to win the race, we commit and run the AU,
switching from [pending] to [accepted]. *)
Definition accepted_state Q (proph_winner : option loc) (l_ghost_winner : loc) :=
- ((∃ v, l_ghost_winner ↦{1/2} v) ∗ match proph_winner with None => True | Some l => ⌜l = l_ghost_winner⌠∗ Q end)%I.
+ ((∃ v, l_ghost_winner ↦{#1/2} v) ∗ match proph_winner with None => True | Some l => ⌜l = l_ghost_winner⌠∗ Q end)%I.
(* The same thread then wins the CmpXchg and moves from [accepted] to [done].
Then, the [γ_t] token guards the transition to take out [Q].
@@ -171,7 +171,7 @@ Section conditional_counter.
owns *more than* half of its [l], which means we know that the [l] there
and here cannot be the same. *)
Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
- ((Q ∨ own_token γ_t) ∗ (∃ v, l_ghost_winner ↦ v) ∗ (∃ v, l ↦{1/2} v))%I.
+ ((Q ∨ own_token γ_t) ∗ (∃ v, l_ghost_winner ↦ v) ∗ (∃ v, l ↦{#1/2} v))%I.
(* We always need the [proph] in here so that failing threads coming late can
always resolve their stuff.
@@ -180,7 +180,7 @@ Section conditional_counter.
Definition state_inv P Q (p : proph_id) n (c_l l l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
(∃ vs, proph p vs ∗
(own γ_s (Cinl $ Excl ()) ∗
- (c_l ↦{1/2} #l ∗ ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
+ (c_l ↦{#1/2} #l ∗ ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
∨ accepted_state Q (val_to_some_loc vs) l_ghost_winner ))
∨ own γ_s (Cinr $ to_agree ()) ∗ done_state Q l l_ghost_winner γ_t))%I.
@@ -192,9 +192,9 @@ Section conditional_counter.
(∃ (l : loc) (q : Qp) (s : abstract_state),
(* We own *more than* half of [l], which shows that this cannot
be the [l] of any [state] protocol in the [done] state. *)
- c ↦{1/2} #l ∗ l ↦{1/2 + q} (state_to_val s) ∗
+ c ↦{#1/2} #l ∗ l ↦{#1/2 + q} (state_to_val s) ∗
match s with
- | Quiescent n => c ↦{1/2} #l ∗ own γ_n (◠Excl' n)
+ | Quiescent n => c ↦{#1/2} #l ∗ own γ_n (◠Excl' n)
| Updating f n p =>
∃ P Q l_ghost_winner γ_t γ_s,
(* There are two pieces of per-[state]-protocol ghost state:
@@ -260,7 +260,7 @@ Section conditional_counter.
(m n : Z) (l l_ghost l_new : loc) Φ :
inv counterN (counter_inv γ_n c_l) -∗
inv stateN (state_inv P Q p m c_l l l_ghost γ_n γ_t γ_s) -∗
- l_ghost ↦{1 / 2} #() -∗
+ l_ghost ↦{# 1 / 2} #() -∗
(□(own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
own γ_n (◠Excl' n) -∗
l_new ↦ InjLV #n -∗
@@ -339,7 +339,8 @@ Section conditional_counter.
iDestruct "Done" as "(_ & _ & >Hl'')".
iDestruct "Hl''" as (v') "Hl''".
iDestruct (mapsto_combine with "Hl Hl''") as "[Hl _]".
- rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hl Hl'") as "[]".
+ rewrite dfrac_op_own Qp_half_half.
+ iDestruct (mapsto_valid_3 with "Hl Hl'") as "[]".
}
(* The CmpXchg fails. *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index cb0161ad..bf39dc34 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -110,8 +110,8 @@ Section stack.
Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
match l with
| nil => ⌜rep = NoneâŒ
- | v::l => ∃ (ℓ : loc) q (rep' : option loc), ⌜rep = Some ℓ⌠∗
- ℓ ↦{q} (v, stack_elem_to_val rep') ∗ list_inv l rep'
+ | v::l => ∃ (ℓ : loc) (rep' : option loc), ⌜rep = Some ℓ⌠∗
+ ℓ ↦□ (v, stack_elem_to_val rep') ∗ list_inv l rep'
end%I.
Local Hint Extern 0 (environments.envs_entails _ (list_inv (_::_) _)) => simpl : core.
@@ -209,6 +209,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".
iDestruct (own_valid_2 with "Hsâ— Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hsâ— Hl'") as "[Hsâ— Hl']".
@@ -289,12 +290,12 @@ Section stack.
iSplitR "HΦ"; first by eauto 10 with iFrame.
iIntros "!>". wp_pures. by iApply "HΦ".
- (* Non-empty list, let's try to pop. *)
- iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep.
+ iDestruct "Hlist" as (tail rep) "[>% [#Htail Hlist]]". subst stack_rep.
iSplitR "AU Htail"; first by eauto 15 with iFrame.
clear offer_rep l.
iIntros "!>". wp_match.
wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
- iIntros "Htail". wp_pures.
+ iIntros "_". wp_pures.
(* CAS to change the head *)
awp_apply cas_spec; [done|].
iInv stackN as (stack_rep offer_rep l) "(>Hs◠& >H↦ & Hlist & Hrem)".
@@ -309,17 +310,17 @@ Section stack.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
destruct l as [|v' l]; simpl.
{ (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
- iDestruct "Hlist" as (tail' q' rep') "[>% [>Htail' Hlist]]". simplify_eq.
+ iDestruct "Hlist" as (tail' rep') "[>% [>Htail' Hlist]]". simplify_eq.
iDestruct (mapsto_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'}".
iSplitR "HΦ"; first by eauto 10 with iFrame.
- iIntros "!>". clear q' q offer_rep l.
+ iIntros "!>". clear offer_rep l.
wp_pures. by iApply "HΦ".
+ (* CAS failed. Go on looking for an offer. *)
iSplitR "AU"; first by eauto 10 with iFrame.
- iIntros "!>". wp_if. clear rep stack_rep offer_rep l q tail v.
+ iIntros "!>". wp_if. iClear (rep stack_rep offer_rep l tail v) "Htail".
wp_proj.
(* Load the offer pointer. *)
awp_apply load_spec.
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index 94361448..04e7968a 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -192,10 +192,9 @@ Section proof.
induction xs as [|x xs' IHxs].
- iIntros (hd Φ) "[Hxs ?] HΦ".
simpl. wp_rec. wp_let.
- iDestruct "Hxs" as (?) "Hhd".
wp_load. wp_match. by iApply "HΦ".
- iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
- iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
+ iDestruct "Hxs" as (hd') "(#Hhd & #Hinv & Hxs')".
wp_rec. wp_let. wp_bind (! _)%E.
iInv N as "H" "Hclose".
iDestruct "H" as (ts p) "[>% #?]". subst.
@@ -221,12 +220,12 @@ Section proof.
iIntros "[Hlocked [Ho2 HR]]".
wp_if. wp_bind (! _)%E.
iInv N as "H" "Hclose".
- iDestruct "H" as (xs' hd') "[>Hs Hxs]".
- wp_load. iDestruct (dup_is_list_R with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
- iMod ("Hclose" with "[Hs Hxs1]").
+ iDestruct "H" as (xs' hd') "[>Hs #Hxs]".
+ wp_load.
+ iMod ("Hclose" with "[Hs]").
{ iNext. iFrame. iExists xs', hd'. by iFrame. }
iModIntro. wp_let. wp_bind (treiber.iter _ _).
- iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
+ iApply wp_wand_r. iSplitL "HR Ho2".
{ iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
iFrame "#". iFrame. eauto. }
iIntros (f') "[Ho HR]". wp_seq.
@@ -255,14 +254,14 @@ Section proof.
iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+ iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
wp_load. iMod ("Hclose" with "[-Ho3 HΦ]").
- { iNext. iFrame. iRight. iRight. iLeft. iExists f, x. iFrame. }
+ { iNext. iRight. iRight. iLeft. iExists f, x. iFrame. }
iModIntro. wp_match.
wp_bind (try_srv _ _). iApply try_srv_spec=>//.
iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+ iDestruct "Hp" as (x y) "[>Hp Hs']".
iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
- { iNext. iFrame. iLeft. iExists y. iFrame. }
+ { iNext. iLeft. iExists y. iFrame. }
iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
iExists Q. iFrame.
Qed.
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index 27d13320..790aa7ba 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -15,23 +15,14 @@ Section defs.
Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
match xs with
- | [] => (∃ q, hd ↦{ q } NONEV)%I
- | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ inv N (R x) ∗ is_list_R hd' xs)%I
+ | [] => hd ↦□ NONEV
+ | x :: xs => ∃ hd': loc, hd ↦□ SOMEV (x, #hd') ∗ inv N (R x) ∗ is_list_R hd' xs
end.
Definition is_bag_R xs s := (∃ hd: loc, s ↦ #hd ∗ is_list_R hd xs)%I.
- Lemma dup_is_list_R : ∀ xs hd,
- is_list_R hd xs ⊢ |==> is_list_R hd xs ∗ is_list_R hd xs.
- Proof.
- induction xs as [|y xs' IHxs'].
- - iIntros (hd) "Hs".
- simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- - iIntros (hd) "Hs". simpl.
- iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
- iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
- iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
- Qed.
+ Global Instance is_list_R_persistent hd xs : Persistent (is_list_R hd xs).
+ Proof. revert hd. induction xs; apply _. Qed.
Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
{{{ inv N R ∗ Rf }}}
@@ -51,14 +42,15 @@ Section proofs.
Proof.
iIntros (Φ) "_ HΦ".
wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+ iMod (mapsto_persist with "Hl") as "#Hl".
wp_alloc s as "Hs".
- iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
+ iAssert (∃ xs, is_bag_R N R xs s)%I with "[-HΦ]" as "Hxs".
{ iFrame. iExists [], l.
iFrame. simpl. eauto. }
iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
iApply "HΦ". iFrame "#". done.
Qed.
-
+
Lemma push_spec (s: loc) (x: val):
{{{ R x ∗ bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
Proof.
@@ -75,10 +67,11 @@ 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 (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
iMod ("Hclose" with "[Hs Hl H1]").
{ iNext. iFrame. iExists (x::xs'), l.
- iFrame. simpl. iExists hd', 1%Qp. iFrame.
+ iFrame. simpl. iExists hd'. iFrame.
by iFrame "#". }
iModIntro. wp_pures. by iApply "HΦ".
- wp_cmpxchg_fail.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 5cfd86fe..301c30b8 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -263,7 +263,7 @@ Section rdcss.
which means we know that the [l_descr] there and here cannot be the same. *)
Definition done_state Qn l_descr (tid_ghost_winner : proph_id) γ_t γ_a :=
((Qn ∨ own_token γ_t) ∗ (∃ vs, proph tid_ghost_winner vs) ∗
- (∃ v, l_descr ↦{1/2} v) ∗ own_token γ_a)%I.
+ (∃ v, l_descr ↦{# 1/2} v) ∗ own_token γ_a)%I.
(* Invariant expressing the descriptor protocol.
- We always need the [proph] in here so that failing threads coming late can
@@ -280,7 +280,7 @@ Section rdcss.
Definition descr_inv P Q p n l_n l_descr (tid_ghost_winner : proph_id) γ_t γ_s γ_a: iProp Σ :=
(∃ vs, proph p vs ∗
(own γ_s (Cinl $ Excl ()) ∗
- (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) tid_ghost_winner l_n γ_a
+ (l_n ↦{# 1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) tid_ghost_winner l_n γ_a
∨ accepted_state (Q n) (proph_extract_winner vs) tid_ghost_winner ))
∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q n) l_descr tid_ghost_winner γ_t γ_a))%I.
@@ -293,13 +293,13 @@ Section rdcss.
Definition rdcss_inv l_n :=
(∃ (s : abstract_state),
- l_n ↦{1/2} (state_to_val s) ∗
+ l_n ↦{# 1/2} (state_to_val s) ∗
match s with
| Quiescent n =>
(* (InjLV #n) = state_to_val (Quiescent n) *)
(* In this state the CmpXchg which expects to read (InjRV _) in
[complete] fails always.*)
- l_n ↦{1/2} (InjLV n) ∗ rdcss_state_auth l_n n
+ l_n ↦{# 1/2} (InjLV n) ∗ rdcss_state_auth l_n n
| Updating l_descr l_m m1 n1 n2 p =>
∃ q P Q tid_ghost_winner γ_t γ_s γ_a,
(* (InjRV #l_descr) = state_to_val (Updating l_descr l_m m1 n1 n2 p) *)
@@ -312,7 +312,7 @@ Section rdcss.
(* We own *more than* half of [l_descr], which shows that this cannot
be the [l_descr] of any [descr] protocol in the [done] state. *)
⌜val_is_unboxed m1⌠∗
- l_descr ↦{1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗
+ l_descr ↦{# 1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_winner γ_t γ_s γ_a) ∗
□ pau P Q l_n l_m m1 n1 n2 ∗ l_m ↦_(λ _, True) □
end)%I.
@@ -340,12 +340,6 @@ Section rdcss.
(** A few more helper lemmas that will come up later *)
- Lemma mapsto_valid_3 l v1 v2 q :
- l ↦ v1 -∗ l ↦{q} v2 -∗ ⌜FalseâŒ.
- Proof.
- iIntros "Hl1 Hl2". iDestruct (mapsto_ne with "Hl1 Hl2") as %?; done.
- Qed.
-
(** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here),
we can at any later point in time extract the [Q]. *)
Lemma state_done_extract_Q P Q p n l_n l_descr tid_ghost γ_t γ_s γ_a :
@@ -462,7 +456,8 @@ Section rdcss.
iDestruct "Hld" as (v') "Hld".
iDestruct "Hrest" as (q P' Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
- rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
+ rewrite dfrac_op_own Qp_half_half.
+ by iDestruct (mapsto_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.
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 60ca60a5..b2f2af11 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -94,15 +94,15 @@ Section atomic_snapshot.
Definition gmap_to_UR T : timestampUR := to_agree <$> T.
Definition snapshot_inv γ1 γ2 l1 : iProp Σ :=
- (∃ q (l1':loc) (T : gmap Z val) x (t : Z),
+ (∃ (l1':loc) (T : gmap Z val) x (t : Z),
(* we add the q to make the l1' map fractional. that way,
we can take a fraction of the l1' map out of the invariant
and do a case analysis on whether the pointer is the same
throughout invariant openings *)
- l1 ↦ #l1' ∗ l1' ↦{q} (x, #t) ∗
+ l1 ↦ #l1' ∗ l1' ↦□ (x, #t) ∗
own γ1 (◠Excl' x) ∗ own γ2 (◠gmap_to_UR T) ∗
⌜T !! t = Some x⌠∗
- ⌜forall (t' : Z), t' ∈ dom (gset Z) T → (t' <= t)%ZâŒ)%I.
+ ⌜∀ (t' : Z), t' ∈ dom (gset Z) T → (t' ≤ t)%ZâŒ)%I.
Definition is_snapshot (γs: gname * gname) (p : val) :=
(∃ (l1 : loc), ⌜p = #l1%V⌠∗ inv N (snapshot_inv γs.1 γs.2 l1))%I.
@@ -131,6 +131,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'".
wp_alloc lx as "Hlx".
set (Excl' v) as p.
iMod (own_alloc (◠p ⋅ ◯ p)) as (γ1) "[Hx⚫ Hx◯]". {
@@ -143,7 +144,7 @@ Section atomic_snapshot.
}
iApply ("Hx" $! (γ1, γ2)).
iMod (inv_alloc N _ (snapshot_inv γ1 γ2 _) with "[-Hx◯ Ht◯]") as "#Hinv". {
- iNext. rewrite /snapshot_inv. iExists _, _, _, _, 0. iFrame.
+ iNext. rewrite /snapshot_inv. iExists _, _, _, 0. iFrame.
iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
rewrite elem_of_singleton. lia.
}
@@ -193,7 +194,7 @@ Section atomic_snapshot.
Lemma timestamp_sub γ (T1 T2 : gmap Z val):
own γ (◠gmap_to_UR T1) ∗ own γ (◯ gmap_to_UR T2) -∗
- ⌜forall t x, T2 !! t = Some x → T1 !! t = Some xâŒ.
+ ⌜∀ t x, T2 !! t = Some x → T1 !! t = Some xâŒ.
Proof.
iIntros "[Hγ⚫ Hγ◯]".
iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
@@ -217,10 +218,9 @@ Section atomic_snapshot.
iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
(* first read *)
(* open invariant *)
- wp_bind (!_)%E. iInv N as (q l1' T x v') "[Hl1 [Hl1' [Hxâš« Htime]]]".
+ wp_bind (!_)%E. iInv N as (l1' T x v') "[Hl1 [#Hl1' [Hxâš« Htime]]]".
wp_load.
- iDestruct "Hl1'" as "[Hl1'frac1 Hl1'frac2]".
- iModIntro. iSplitR "AU Hl1'frac2".
+ iModIntro. iSplitR "AU".
(* close invariant *)
{ iNext. rewrite /snapshot_inv. eauto 10 with iFrame. }
wp_let. wp_bind (!_)%E. clear T.
@@ -229,11 +229,12 @@ Section atomic_snapshot.
(* CAS *)
wp_bind (CmpXchg _ _ _)%E.
(* open invariant *)
- iInv N as (q' l1'' T x' v'') ">[Hl1 [Hl1'' [Hxâš« [Htâ— Ht]]]]".
+ iInv N as (l1'' T x' v'') ">[Hl1 [#Hl1'' [Hxâš« [Htâ— Ht]]]]".
iDestruct "Ht" as %[Ht Hvt].
destruct (decide (l1'' = l1')) as [-> | Hn].
- wp_cmpxchg_suc.
- iDestruct (mapsto_agree with "Hl1'frac2 Hl1''") as %[= -> ->]. iClear "Hl1'frac2".
+ iMod (mapsto_persist with "Hl1'new") as "Hl1'new".
+ iDestruct (mapsto_agree with "Hl1' Hl1''") as %[= -> ->].
(* open AU *)
iMod "AU" as (xv) "[Hx [_ Hclose]]".
(* update snapshot ghost state to (x2, y') *)
@@ -249,7 +250,7 @@ Section atomic_snapshot.
iModIntro. iSplitR "HΦ".
+ iNext. rewrite /snapshot_inv.
set (<[ (v'' + 1)%Z := x2]> T) as T'.
- iExists 1%Qp, l1'new, T', x2, (v'' + 1)%Z.
+ iExists l1'new, T', x2, (v'' + 1)%Z.
iFrame.
iPureIntro. split.
* apply: lookup_insert.
@@ -277,9 +278,8 @@ Section atomic_snapshot.
iDestruct "Hx" as (l1 ->) "#Hinv".
wp_lam. wp_bind (! #l1)%E.
(* open invariant for 1st read *)
- iInv N as (q l1' T x v') ">[Hl1 [Hl1' [Hxâš« Htime]]]".
+ iInv N as (l1' T x v') ">[Hl1 [#Hl1' [Hxâš« Htime]]]".
wp_load.
- iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
iMod "AU" as (xv) "[Hx [_ Hclose]]".
iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
iMod ("Hclose" with "Hx") as "HΦ".
@@ -311,10 +311,9 @@ Section atomic_snapshot.
(* ************ 1st readX ********** *)
iDestruct "Hx" as (l1 ->) "#Hinv". wp_bind (! #l1)%E.
(* open invariant for 1st read *)
- iInv N as (q_x1 l1' T_x x1 v_x1) ">[Hl1 [Hl1' [Hxâš« [Ht_x Htime_x]]]]".
+ iInv N as (l1' T_x x1 v_x1) ">[Hl1 [#Hl1' [Hxâš« [Ht_x Htime_x]]]]".
iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
wp_load.
- iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
iMod "AU" as (xv yv) "[[Hx Hy] [Hclose _]]".
iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
iMod ("Hclose" with "[$Hx $Hy]") as "AU".
@@ -327,7 +326,7 @@ Section atomic_snapshot.
wp_load. wp_let.
(* ************ readY ********** *)
repeat (wp_lam; wp_pures). wp_bind (!_)%E.
- iInv N as (q_y l1'_y T_y x_y v_y) ">[Hl1 [Hl1'_y [Hxâš« [Ht_y Htime_y]]]]".
+ iInv N as (l1'_y T_y x_y v_y) ">[Hl1 [#Hl1'_y [Hxâš« [Ht_y Htime_y]]]]".
iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
(* linearization point *)
clear yv.
@@ -351,13 +350,12 @@ Section atomic_snapshot.
(* ************ 2nd readX ********** *)
repeat (wp_lam; wp_pures). wp_bind (! #l1)%E.
(* open invariant *)
- iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) ">[Hl1 [Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
+ iInv N as (l1'_x2 T_x2 x2 v_x2) ">[Hl1 [#Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
iDestruct "Htime_x2" as %[Hlookup_x2 Hdom_x2].
- iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
wp_load.
(* show that T_y <= T_x2 *)
iDestruct (timestamp_sub with "[Ht_x2 Ht_yâ—¯]") as "%Hs'"; first by iFrame.
- iModIntro. iSplitR "HΦ Hl1'_x2_frag Hpr". {
+ iModIntro. iSplitR "HΦ Hpr". {
iNext. unfold snapshot_inv. eauto 8 with iFrame.
}
wp_load. wp_pures.
@@ -390,10 +388,9 @@ Section atomic_snapshot.
(* ************ 2nd readX ********** *)
wp_bind (! #l1)%E.
(* open invariant *)
- iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) "[Hl1 [Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
- iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
+ iInv N as (l1'_x2 T_x2 x2 v_x2) "[Hl1 [#Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
wp_load.
- iModIntro. iSplitR "AU Hl1'_x2_frag Hpr". {
+ iModIntro. iSplitR "AU Hpr". {
iNext. unfold snapshot_inv. eauto 8 with iFrame.
}
wp_load. wp_pures.
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
index bee5df4a..34d8ad07 100644
--- a/theories/logatom/treiber.v
+++ b/theories/logatom/treiber.v
@@ -37,45 +37,30 @@ Section proof.
Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
match xs with
- | [] => (∃ q, hd ↦{ q } NONEV)%I
- | x :: xs => (∃ (hd': loc) q, hd ↦{ q } SOMEV (x, #hd') ∗ is_list hd' xs)%I
+ | [] => hd ↦□ NONEV
+ | x :: xs => ∃ hd': loc, hd ↦□ SOMEV (x, #hd') ∗ is_list hd' xs
end.
- Lemma dup_is_list : ∀ xs hd,
- is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs.
- Proof.
- induction xs as [|y xs' IHxs'].
- - iIntros (hd) "Hs".
- simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- - iIntros (hd) "Hs". simpl.
- iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
- iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
- iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
- Qed.
+ Global Instance is_list_persistent hd xs : Persistent (is_list hd xs).
+ Proof. revert hd. induction xs; simpl; apply _. Qed.
- Lemma uniq_is_list:
- ∀ xs ys hd, is_list hd xs ∗ is_list hd ys ⊢ ⌜xs = ysâŒ.
+ Lemma uniq_is_list xs ys hd : is_list hd xs ∗ is_list hd ys ⊢ ⌜xs = ysâŒ.
Proof.
- induction xs as [|x xs' IHxs'].
+ revert ys hd. induction xs as [|x xs' IHxs']; intros ys hd.
- induction ys as [|y ys' IHys'].
+ auto.
- + iIntros (hd) "(Hxs & Hys)".
- simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
- iExFalso. iDestruct "Hxs" as (?) "Hhd'".
- (* FIXME: If I dont use the @ here and below through this file, it loops. *)
- by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+ + iIntros "[Hxs Hys] /=".
+ iDestruct "Hys" as (hd') "[Hhd Hys']".
+ by iDestruct (mapsto_agree with "Hxs Hhd") as %?.
- induction ys as [|y ys' IHys'].
- + iIntros (hd) "(Hxs & Hys)".
- simpl.
- iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
- iDestruct "Hys" as (?) "Hhd'".
- by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
- + iIntros (hd) "(Hxs & Hys)".
- simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
- iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
- iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
- subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
- by subst.
+ + iIntros "[Hxs Hys] /=".
+ iDestruct "Hxs" as (?) "[Hhd _]".
+ by iDestruct (mapsto_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 %[= -> ->].
+ by iDestruct (IHxs' with "[$Hxs' $Hys']") as %->.
Qed.
Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ∗ is_list hd xs)%I.
@@ -91,11 +76,11 @@ Section proof.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+ iMod (mapsto_persist with "Hl") as "Hl".
wp_alloc l' as "Hl'".
- iApply "HΦ". rewrite /is_stack. iExists l.
- iFrame. by iExists 1%Qp.
+ iApply "HΦ". rewrite /is_stack. auto.
Qed.
-
+
Lemma push_atomic_spec (s: loc) (x: val) :
⊢ <<< ∀ (xs : list val), is_stack s xs >>>
push #s x @ ⊤
@@ -108,6 +93,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".
wp_bind (CmpXchg _ _ _)%E.
iMod "HP" as (xs') "[Hxs' Hvs']".
iDestruct "Hxs'" as (hd') "[Hs' Hhd']".
@@ -133,18 +119,16 @@ Section proof.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_bind (! _)%E.
iMod "HP" as (xs) "[Hxs Hvs']".
- iDestruct "Hxs" as (hd) "[Hs Hhd]".
+ iDestruct "Hxs" as (hd) "[Hs #Hhd]".
destruct xs as [|y' xs'].
- simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
- iDestruct "Hhd" as (q) "[Hhd Hhd']".
- iMod ("Hvs'" with "[-Hhd]") as "HQ".
+ iMod ("Hvs'" with "[-]") as "HQ".
{ eauto with iFrame. }
iModIntro. wp_let. wp_load. wp_pures.
eauto.
- - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
- iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
+ - simpl. iDestruct "Hhd" as (hd') "(Hhd & Hxs')".
wp_load. iDestruct "Hvs'" as "[Hvs' _]".
- iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
+ iMod ("Hvs'" with "[-]") as "HP".
{ eauto with iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CmpXchg _ _ _).
@@ -152,11 +136,10 @@ Section proof.
iDestruct "Hxs''" as (hd'') "[Hs'' Hhd'']".
destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cmpxchg_suc. iDestruct "Hvs'" as "[_ Hvs']".
- destruct xs'' as [|x'' xs''].
- { simpl. iDestruct "Hhd''" as (?) "H".
- iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
- iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
+ destruct xs'' as [|x'' xs'']; simpl.
+ { by iDestruct (mapsto_agree with "Hhd Hhd''") as %?. }
+ iDestruct "Hhd''" as (hd''') "[Hhd'' Hxs'']".
+ iDestruct (@mapsto_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 939bb31c..8540d0a0 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -89,7 +89,7 @@ Fixpoint phys_list (lopt : option loc) (xs : list val) : iProp :=
| (None , [] ) => True
| (None , _ :: _ ) => False
| (Some _, [] ) => False
- | (Some ℓ, x :: xs) => ∃r q, ℓ ↦{q} (x, to_val r) ∗ phys_list r xs
+ | (Some ℓ, x :: xs) => ∃ r, ℓ ↦□ (x, to_val r) ∗ phys_list r xs
end%I.
(** Representation relation for stacks: the location [â„“] physically represents
@@ -132,15 +132,9 @@ Proof.
intros l1 l2 H. case l1, l2; try done. inversion H. reflexivity.
Qed.
-(** Duplicability of the [phys_list] relation. *)
-Lemma phys_list_dup l xs : phys_list l xs -∗ phys_list l xs ∗ phys_list l xs.
-Proof.
- iInduction xs as [|x xs] "IH" forall (l); destruct l as [l|]; try done.
- simpl. iIntros "H".
- iDestruct "H" as (r q) "[[Hl1 Hl2] HPhys]".
- iDestruct ("IH" with "HPhys") as "[HPhys1 HPhys2]".
- iSplitL "Hl1 HPhys1"; eauto with iFrame.
-Qed.
+(** Persistence of the [phys_list] relation. *)
+Global Instance phys_list_dup l xs : Persistent (phys_list l xs).
+Proof. revert l. induction xs; apply _. Qed.
(** Timelessness of the [phys_list] relation. *)
Global Instance phys_list_timeless l xs : Timeless (phys_list l xs).
@@ -274,6 +268,7 @@ Proof.
(* Commit operation. *)
iMod ("HClose" with "Hγ◯") as "H".
(* We can eliminate the modality. *)
+ iMod (mapsto_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".
@@ -303,16 +298,14 @@ Proof.
iIntros "#HInv" (Φ) "AU". iLöb as "IH". wp_lam. wp_bind (! _)%E.
(* We can then use the invariant to be able to perform the load. *)
iInv "HInv" as (xs) ">[HPhys Hγâ—]".
- iDestruct "HPhys" as (w) "[Hl HPhys]". wp_load.
- (* We now duplicate [phys_list w xs] as we will need two copies. *)
- iDestruct (phys_list_dup with "HPhys") as "[HPhys1 HPhys2]".
+ iDestruct "HPhys" as (w) "[Hl #HPhys]". wp_load.
(* We then inspect the contents of the stack and the optional location. They
must agree, otherwise the proof is trivial. *)
destruct w as [w|], xs as [|x xs]; try done; simpl.
- (* The stack is non-empty, we eliminate the modality. *)
- iModIntro. iSplitL "Hl Hγ◠HPhys1"; first by eauto 10 with iFrame.
+ iModIntro. iSplitL "Hl Hγâ—"; first by eauto 10 with iFrame.
(* We continue stepping through the program, and focus on the CAS. *)
- wp_let. wp_match. iDestruct "HPhys2" as (r q) "[Hw HP]".
+ wp_let. wp_match. iDestruct "HPhys" as (r) "[Hw HP]".
wp_load. wp_let. wp_proj. wp_bind (CmpXchg _ _ _)%E.
(* We need to use the invariant again to gain information on [â„“]. *)
iInv "HInv" as (ys) ">[H Hγâ—]".
@@ -332,7 +325,7 @@ Proof.
(* 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). *)
- iDestruct "HPhys" as (u q') "[Hw' HPhys]".
+ iDestruct "HPhys" as (u) "[Hw' HPhys]".
iDestruct (mapsto_agree with "Hw Hw'") as %[=-> ->%to_val_inj].
(* Perform the commit. *)
iMod ("HClose" with "Hγ◯") as "HΦ".
@@ -348,7 +341,7 @@ Proof.
wp_pures. iApply "IH". iExact "AU".
- (* The stack is empty, the load was the linearization point, we can hence
commit (without updating the stack). So we access the precondition. *)
- iClear "HPhys1 HPhys2". iMod "AU" as (xs) "[Hγ◯ [_ HClose]]".
+ iMod "AU" as (xs) "[Hγ◯ [_ HClose]]".
(* Thanks to agreement, we learn that [xs] must be the empty list. *)
iDestruct (auth_agree with "Hγ◠Hγ◯") as %<-.
(* And we can commit (we are still at the linearization point). *)
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
index a7456a24..4b099f8e 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
@@ -9,7 +9,7 @@ From iris.proofmode Require Import tactics.
Definition stackN : namespace := nroot .@ "stack".
Section Stack_refinement.
- Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
+ Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types Δ : listO D.
@@ -46,29 +46,20 @@ Section Stack_refinement.
iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk".
simpl. iApply wp_pure_step_later; trivial. iNext. simpl.
iAsimpl.
+ iMod (mapsto_persist with "Histk") as "#Histk".
(* establishing the invariant *)
- iMod (own_alloc (◠(∅ : stackUR))) as (γ) "Hemp"; first by apply auth_auth_valid.
- set (istkG := StackG _ _ γ).
- change γ with (@stack_name _ istkG).
- change H1 with (@stack_inG _ istkG).
- clearbody istkG. clear γ H1.
- iAssert (@stack_owns _ istkG _ ∅) with "[Hemp]" as "Hoe".
- { rewrite /stack_owns big_sepM_empty fmap_empty. iFrame "Hemp"; trivial. }
- iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe Hls]".
- iAssert (StackLink Ï„i (LocV istk, FoldV (InjLV UnitV))) with "[Hls]" as "HLK".
+ iAssert (StackLink Ï„i (LocV istk, FoldV (InjLV UnitV))) with "[]" as "HLK".
{ rewrite StackLink_unfold.
iExists _, _. iSplitR; simpl; trivial.
- iFrame "Hls". iLeft. iSplit; trivial. }
- iAssert ((∃ istk v h, (stack_owns h)
- ∗ stk' ↦ₛ v
- ∗ stk ↦ᵢ (LocV istk)
- ∗ StackLink τi (LocV istk, v)
- ∗ l ↦ₛ (#â™v false)
- )%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
- { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". }
+ iFrame "Histk". iLeft. iSplit; trivial. }
+ iAssert ((∃ istk v, stk' ↦ₛ v
+ ∗ stk ↦ᵢ (LocV istk)
+ ∗ StackLink τi (LocV istk, v)
+ ∗ l ↦ₛ (#â™v false)
+ )%I) with "[Hstk Hstk' HLK Hl]" as "Hinv".
+ { iExists _, _. by iFrame "Hstk' Hstk Hl HLK". }
iMod (inv_alloc stackN with "[Hinv]") as "#Hinv"; [iNext; iExact "Hinv"|].
- clear istk.
- Opaque stack_owns.
+ iClear (istk) "Histk HLK".
(* splitting *)
iApply wp_value; simpl; trivial.
iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (LamV _)).
@@ -91,11 +82,11 @@ Section Stack_refinement.
iAsimpl.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
- iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
+ iInv stackN as (istk v) "[Hstk' [Hstk [HLK Hl]]]" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
- iMod ("Hclose" with "[Hoe Hstk' HLK Hl Hstk]") as "_".
- { iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk". }
- clear v h.
+ iMod ("Hclose" with "[Hstk' HLK Hl Hstk]") as "_".
+ { iNext. iExists _, _; by iFrame "Hstk' HLK Hl Hstk". }
+ clear v.
iApply wp_pure_step_later; auto using to_of_val.
iModIntro. iNext. iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
@@ -104,7 +95,7 @@ Section Stack_refinement.
iNext. iIntros (ltmp) "Hltmp".
iApply (wp_bind (fill [IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "H"; iExact "H"|].
- iInv stackN as (istk2 v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
+ iInv stackN as (istk2 v) "[Hstk' [Hstk [HLK Hl]]]" "Hclose".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk = istk2)) as [|Hneq]; subst.
* (* CAS succeeds *)
@@ -115,20 +106,20 @@ 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 (stack_owns_alloc with "[$Hoe $Hltmp]") as "[Hoe Hpt]".
+ iMod (mapsto_persist with "Hltmp") as "#Hltmp".
iMod ("Hclose" with "[-Hj]") as "_".
- { iNext. iExists ltmp, _, _.
- iFrame "Hoe Hstk' Hstk Hl".
+ { iNext. iExists ltmp, _.
+ iFrame "Hstk' Hstk Hl".
do 2 rewrite StackLink_unfold.
rewrite -StackLink_unfold.
iExists _, _. iSplit; trivial.
- iFrame "Hpt". eauto 10. }
+ iFrame "Hltmp". eauto 10. }
iModIntro.
iApply wp_pure_step_later; auto. iNext; iApply wp_value; trivial.
iExists UnitV; eauto.
* iApply (wp_cas_fail with "Hstk"); auto. congruence.
iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]").
- { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk Hl". }
iApply wp_pure_step_later; auto. iModIntro. iNext. by iApply "Hlat".
+ (* refinement of pop *)
iModIntro. clear j K. iIntros ( [v1 v2] ) "[% %]".
@@ -141,7 +132,7 @@ Section Stack_refinement.
iAsimpl.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
- iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
+ iInv stackN as (istk v) "[Hstk' [Hstk [#HLK Hl]]]" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
iPoseProof "HLK" as "HLK'".
(* Checking whether the stack is empty *)
@@ -152,19 +143,16 @@ Section Stack_refinement.
iMod (steps_CG_locked_pop_fail with "[$Hspec $Hstk' $Hl $Hj]")
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj Hmpt]") as "_".
- { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk Hl". }
iModIntro.
iApply wp_pure_step_later; auto. iNext. iAsimpl.
- clear h.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iClear "HLK".
- iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
- iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
- iApply (wp_load with "Histk").
- iNext. iIntros "Histk". iMod ("Hclose" with "[-Hj]") as "_".
- { iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl".
- by iApply "HLoe". }
+ iInv stackN as (istk3 w) "[Hstk' [Hstk [HLK Hl]]]" "Hclose".
+ iApply (wp_load with "Hmpt").
+ iNext. iIntros "_". iMod ("Hclose" with "[-Hj]") as "_".
+ { iNext. iExists _, _. iFrame "Hstk' Hstk HLK Hl". }
iApply wp_pure_step_later; simpl; trivial.
iModIntro. iNext. iAsimpl.
iApply wp_pure_step_later; trivial.
@@ -172,19 +160,16 @@ Section Stack_refinement.
iSplit; trivial. iLeft. iExists (_, _); repeat iSplit; simpl; trivial.
* (* The stack is not empty *)
iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
- { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk HLK Hl". }
iModIntro. iApply wp_pure_step_later; auto.
iNext. iAsimpl.
- clear h.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
iClear "HLK".
- iInv stackN as (istk3 w' h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
- iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
- iApply (wp_load with "Histk"). iNext; iIntros "Histk".
- iDestruct ("HLoe" with "Histk") as "Hh".
+ iInv stackN as (istk3 w') "[Hstk' [Hstk [HLK Hl]]]" "Hclose".
+ iApply (wp_load with "Hmpt"). iNext; iIntros "_".
iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
- { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk HLK Hl". }
iApply wp_pure_step_later; auto.
iModIntro. iNext. iAsimpl.
iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl.
@@ -200,8 +185,8 @@ Section Stack_refinement.
simpl. iNext. iApply wp_value.
iApply (wp_bind (fill [IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
- clear istk3 h. iAsimpl.
- iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
+ clear istk3. iAsimpl.
+ iInv stackN as (istk3 w) "[Hstk' [Hstk [#HLK Hl]]]" "Hclose".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk2 = istk3)) as [|Hneq]; subst.
-- (* CAS succeeds *)
@@ -210,8 +195,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 (stack_mapstos_agree with "[Hmpt Hmpt']") as %?;
- first (iSplit; [iExact "Hmpt"| iExact "Hmpt'"]).
+ iDestruct (mapsto_agree with "Hmpt Hmpt'") as %<-.
iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
"[% [% [#Hrel HLK'']]]"; simplify_eq/=.
@@ -222,7 +206,7 @@ Section Stack_refinement.
iMod ("Hclose" with "[-Hj]") as "_".
{ iNext. iIntros "{Hmpt Hmpt' HLK}". rewrite StackLink_unfold.
iDestruct "HLK''" as (istk5 w2) "[% [Hmpt HLK]]"; simplify_eq/=.
- iExists istk5, _, _. iFrame "Hoe Hstk' Hstk Hl".
+ iExists istk5, _. iFrame "Hstk' Hstk Hl".
rewrite StackLink_unfold.
iExists _, _; iSplitR; trivial.
by iFrame "HLK". }
@@ -236,7 +220,7 @@ Section Stack_refinement.
-- (* CAS will fail *)
iApply (wp_cas_fail with "Hstk"); [rewrite /= ?to_of_val //; congruence..|].
iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]") as "_".
- { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk HLK Hl". }
iApply wp_pure_step_later; auto. iModIntro. iNext. by iApply "Hlat".
- (* refinement of iter *)
iModIntro. clear j K. iIntros ( [f1 f2] ) "/= #Hfs". iIntros (j K) "Hj".
@@ -249,14 +233,14 @@ Section Stack_refinement.
by (by rewrite CG_iter_of_val).
iApply (wp_bind (fill [FoldCtx; AppRCtx _])); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
- iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose".
+ iInv stackN as (istk3 w) "[>Hstk' [>Hstk [#HLK >Hl]]]" "Hclose".
iMod (steps_CG_snap _ _ (AppRCtx _ :: K)
with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]"; first solve_ndisj.
{ rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". }
iApply (wp_load with "[$Hstk]"). iNext. iIntros "Hstk".
iMod ("Hclose" with "[-Hj]") as "_".
- { iNext. iExists _, _, _; by iFrame "Hoe Hstk' Hstk HLK Hl". }
- clear h. iModIntro.
+ { iNext. iExists _, _; by iFrame "Hstk' Hstk HLK Hl". }
+ iModIntro.
rewrite ?fill_app /= -FG_iter_folding.
iLöb as "Hlat" forall (istk3 w) "HLK".
rewrite {2}FG_iter_folding.
@@ -270,15 +254,13 @@ Section Stack_refinement.
iSplitR; [iIntros (v) "Hw"; iExact "Hw"|].
rewrite StackLink_unfold.
iDestruct "HLK" as (istk4 v) "[% [Hmpt HLK]]"; simplify_eq/=.
- iInv stackN as (istk5 v' h) "[Hoe [Hstk' [Hstk [HLK' Hl]]]]" "Hclose".
- iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
- iApply (wp_load with "[$Histk]"). iNext. iIntros "Histk".
- iDestruct ("HLoe" with "Histk") as "Hh".
+ iInv stackN as (istk5 v') "[Hstk' [Hstk [HLK' Hl]]]" "Hclose".
+ iApply (wp_load with "Hmpt"). iNext. iIntros "_".
iDestruct "HLK" as "[[% %]|HLK'']"; simplify_eq/=.
* rewrite CG_iter_of_val.
iMod (steps_CG_iter_end with "[$Hspec $Hj]") as "Hj"; first solve_ndisj.
iMod ("Hclose" with "[-Hj]").
- { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk Hl". }
iApply wp_pure_step_later; trivial.
iModIntro. iNext. iApply wp_value; trivial. iExists UnitV; eauto.
* iDestruct "HLK''" as (yn1 yn2 zn1 zn2)
@@ -286,7 +268,7 @@ Section Stack_refinement.
rewrite CG_iter_of_val.
iMod (steps_CG_iter with "[$Hspec $Hj]") as "Hj"; first solve_ndisj.
iMod ("Hclose" with "[-Hj HLK'']") as "_".
- { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk Hl". }
+ { iNext. iExists _, _. by iFrame "Hstk' Hstk Hl". }
simpl.
iApply wp_pure_step_later; simpl; rewrite ?to_of_val; trivial.
iAsimpl.
@@ -333,7 +315,7 @@ Theorem stack_ctx_refinement :
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
- set (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR); GFunctor (authR stackUR)]).
+ set (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR)]).
set (HG := soundness_unary.HeapPreIG Σ _ _).
eapply (binary_soundness Σ); eauto using FG_stack_type, CG_stack_type.
intros; apply FG_CG_counter_refinement.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
index d11b2018..83caa77b 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
@@ -1,33 +1,12 @@
From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth gmap agree.
From iris_examples.logrel.F_mu_ref_conc Require Import logrel_binary.
-Import uPred.
-
-Definition stackUR : ucmraT := gmapUR loc (agreeR valO).
-
-Class stackG Σ :=
- StackG { stack_inG :> inG Σ (authR stackUR); stack_name : gname }.
-
-Definition stack_mapsto `{stackG Σ} (l : loc) (v : val) : iProp Σ :=
- own stack_name (â—¯ {[ l := to_agree v ]}).
-
-Notation "l ↦ˢᵗᵠv" := (stack_mapsto l v) (at level 20) : bi_scope.
Section Rules.
- Context `{stackG Σ}.
+ Context `{heapIG Σ}.
Notation D := (prodO valO valO -n> iPropO Σ).
- Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵠv).
- Proof. apply _. Qed.
-
- Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵠv ∗ l ↦ˢᵗᵠw ⊢ ⌜v = wâŒ.
- Proof.
- rewrite -own_op -auth_frag_op singleton_op own_valid.
- by iIntros (->%auth_frag_valid%singleton_valid%to_agree_op_inv_L).
- Qed.
-
Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
- (∃ l w, ⌜v.1 = LocV l⌠∗ l ↦ˢᵗᵠw ∗
+ (∃ l w, ⌜v.1 = LocV l⌠∗ l ↦ᵢ□ w ∗
((⌜w = InjLV UnitV⌠∧ ⌜v.2 = FoldV (InjLV UnitV)âŒ) ∨
(∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌠∗
⌜v.2 = FoldV (InjRV (PairV y2 z2))⌠∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
@@ -40,7 +19,7 @@ Section Rules.
Lemma StackLink_unfold Q v :
StackLink Q v ≡ (∃ l w,
- ⌜v.1 = LocV l⌠∗ l ↦ˢᵗᵠw ∗
+ ⌜v.1 = LocV l⌠∗ l ↦ᵢ□ w ∗
((⌜w = InjLV UnitV⌠∧ ⌜v.2 = FoldV (InjLV UnitV)âŒ) ∨
(∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))âŒ
∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))âŒ
@@ -57,54 +36,7 @@ Section Rules.
iDestruct "H" as (l w) "[% [#Hl [#Hr|Hr]]]"; subst.
{ iExists l, w; iModIntro; eauto. }
iDestruct "Hr" as (y1 z1 y2 z2) "[#H1 [#H2 [#HQ H']]]".
- rewrite later_forall. iDestruct ("IH" with "H'") as "#H''". iClear "H'".
+ iDestruct ("IH" with "H'") as "#H''". iClear "H'".
iModIntro. eauto 20.
Qed.
-
- Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) :
- h !! i = None → ◠h ~~> ◠(<[i := to_agree v]> h) ⋅ ◯ {[i := to_agree v]}.
- Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
-
- Context `{heapIG Σ}.
-
- Definition stack_owns (h : gmap loc val) :=
- (own stack_name (â— ((to_agree <$> h) : stackUR))
- ∗ [∗ map] l ↦ v ∈ h, l ↦ᵢ v)%I.
-
- Lemma stack_owns_alloc h l v :
- stack_owns h ∗ l ↦ᵢ v ==∗ stack_owns (<[l := v]> h) ∗ l ↦ˢᵗᵠv.
- Proof.
- iIntros "[[Hown Hall] Hl]".
- iDestruct (own_valid with "Hown") as %Hvalid.
- destruct (h !! l) as [w|] eqn:?.
- { iDestruct (@big_sepM_lookup with "Hall") as "Hl'"; first done.
- by iDestruct (@mapsto_valid_2 loc val with "Hl Hl'") as %[??]. }
- iMod (own_update with "Hown") as "[Hown Hl']".
- { eapply auth_update_alloc.
- eapply (alloc_singleton_local_update _ l (to_agree v)); last done.
- by rewrite lookup_fmap Heqo. }
- iModIntro. rewrite /stack_owns. rewrite fmap_insert. iFrame "Hl' Hown".
- iApply @big_sepM_insert; simpl; try iFrame; auto.
- Qed.
-
- Lemma stack_owns_open_close h l v :
- stack_owns h -∗ l ↦ˢᵗᵠv -∗ l ↦ᵢ v ∗ (l ↦ᵢ v -∗ stack_owns h).
- Proof.
- iIntros "[Howns Hls] Hl".
- iDestruct (own_valid_2 with "Howns Hl")
- as %[[az [Haz Hq]]%singleton_included_l _]%auth_both_valid_discrete.
- rewrite lookup_fmap in Haz.
- assert (∃ z, h !! l = Some z) as Hz.
- { revert Haz; case: (h !! l) => [z|] Hz; first (by eauto); inversion Hz. }
- destruct Hz as [z Hz]; rewrite Hz in Haz.
- apply Some_equiv_inj in Haz; revert Hq; rewrite -Haz => Hq.
- apply Some_included_total, to_agree_included, leibniz_equiv in Hq; subst.
- rewrite (big_sepM_lookup_acc _ _ l); eauto.
- iDestruct "Hls" as "[Hl' Hls]".
- iIntros "{$Hl'} Hl'". rewrite /stack_owns. iFrame "Howns". by iApply "Hls".
- Qed.
-
- Lemma stack_owns_later_open_close h l v :
- ▷ stack_owns h -∗ l ↦ˢᵗᵠv -∗ ▷ (l ↦ᵢ v ∗ (l ↦ᵢ v -∗ stack_owns h)).
- Proof. iIntros "H1 H2". iNext; by iApply (stack_owns_open_close with "H1"). Qed.
End Rules.
diff --git a/theories/logrel/F_mu_ref_conc/rules.v b/theories/logrel/F_mu_ref_conc/rules.v
index 1dbf43f9..98e29358 100644
--- a/theories/logrel/F_mu_ref_conc/rules.v
+++ b/theories/logrel/F_mu_ref_conc/rules.v
@@ -21,9 +21,14 @@ Instance heapIG_irisG `{heapIG Σ} : irisG F_mu_ref_conc_lang Σ := {
}.
Global Opaque iris_invG.
-Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v)
- (at level 20, q at level 50, format "l ↦ᵢ{ q } v") : bi_scope.
-Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : bi_scope.
+Notation "l ↦ᵢ{ dq } v" := (mapsto (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)
+ (at level 20, format "l ↦ᵢ□ v") : bi_scope.
+Notation "l ↦ᵢ{# q } v" := (mapsto (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)
+ (at level 20, format "l ↦ᵢ v") : bi_scope.
Section lang_rules.
Context `{heapIG Σ}.
@@ -64,8 +69,8 @@ Section lang_rules.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
- Lemma wp_load E l q v :
- {{{ ▷ l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
+ 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 (σ1 ???) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -87,10 +92,10 @@ Section lang_rules.
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
- Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
+ Lemma wp_cas_fail E l dq v' e1 v1 e2 v2 :
IntoVal e1 v1 → IntoVal e2 v2 → v' ≠v1 →
- {{{ ▷ l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E
- {{{ RET (BoolV false); l ↦ᵢ{q} v' }}}.
+ {{{ ▷ l ↦ᵢ{dq} v' }}} CAS (Loc l) e1 e2 @ E
+ {{{ RET (BoolV false); l ↦ᵢ{dq} v' }}}.
Proof.
iIntros (<- <- ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
--
GitLab