From fa1945be9261c66f4e089b959dd97e9727ebfe51 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Dec 2020 13:26:26 +0100
Subject: [PATCH] remove a couple wp_fupd
---
coq-iris-examples.opam | 2 +-
theories/barrier/proof.v | 2 +-
theories/concurrent_stacks/concurrent_stack1.v | 1 -
theories/concurrent_stacks/concurrent_stack2.v | 3 ---
theories/concurrent_stacks/concurrent_stack3.v | 1 -
theories/concurrent_stacks/concurrent_stack4.v | 4 +---
theories/hocap/concurrent_runners.v | 5 ++---
theories/hocap/fg_bag.v | 2 +-
theories/lecture_notes/coq_intro_example_2.v | 11 ++++-------
theories/lecture_notes/lock.v | 2 +-
theories/lecture_notes/lock_unary_spec.v | 4 ++--
theories/lecture_notes/modular_incr.v | 1 -
theories/logatom/elimination_stack/stack.v | 2 +-
theories/logatom/flat_combiner/peritem.v | 2 +-
theories/logatom/herlihy_wing_queue/hwq.v | 2 +-
theories/logatom/snapshot/atomic_snapshot.v | 1 -
theories/logatom/treiber2.v | 2 --
17 files changed, 16 insertions(+), 31 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 3b36a485..f09b5a9e 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.5.b008a6b2") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
"coq-autosubst" { = "dev" }
"coq-iris-string-ident"
]
diff --git a/theories/barrier/proof.v b/theories/barrier/proof.v
index f0f40d5e..df6a2629 100644
--- a/theories/barrier/proof.v
+++ b/theories/barrier/proof.v
@@ -50,7 +50,7 @@ Proof. solve_proper. Qed.
Lemma newbarrier_spec (P : iProp Σ) :
{{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
Proof.
- iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl".
+ iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl".
iApply ("HΦ" with "[> -]").
iMod (saved_prop_alloc P) as (γsp) "#Hsp".
iMod (own_alloc (● GSet {[ γsp ]} ⋅ ◯ GSet {[ γsp ]})) as (γ) "[H● H◯]".
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index 724a6433..44ae7cd3 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -92,7 +92,6 @@ Section stacks.
{{{ True }}} new_stack #() {{{ s, RET s; is_stack P s }}}.
Proof.
iIntros (ϕ) "_ Hpost".
- iApply wp_fupd.
wp_lam.
wp_alloc ℓ as "Hl".
iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 4a194fc9..1b36d8de 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -82,7 +82,6 @@ Section side_channel.
{{{ P v }}} mk_offer v {{{ o γ, RET o; is_offer γ P o ∗ revoke_tok γ }}}.
Proof.
iIntros (Φ) "HP HΦ".
- rewrite -wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (stages γ P l v) with "[Hl HP]") as "#Hinv".
@@ -162,7 +161,6 @@ Section mailbox.
{{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
Proof.
iIntros (Φ) "_ HΦ".
- rewrite -wp_fupd.
wp_lam.
wp_alloc l as "Hl".
iMod (inv_alloc N _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
@@ -299,7 +297,6 @@ Section stack_works.
{{{ True }}} new_stack #() {{{ v, RET v; is_stack P v }}}.
Proof.
iIntros (ϕ) "_ Hpost".
- rewrite -wp_fupd.
wp_lam.
wp_alloc l as "Hl".
wp_apply mk_mailbox_works; first done.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 5a3506bb..c8959227 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -97,7 +97,6 @@ Section stack_works.
{{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
Proof.
iIntros (Φ) "HP HΦ".
- rewrite -wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
{ iNext; iExists None, []; iFrame. }
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index efac94f2..0d600a2b 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -105,7 +105,6 @@ Section proofs.
{{{ o γ, RET o; is_offer γ P Q o ∗ revoke_tok γ }}}.
Proof.
iIntros (Φ) "HP HΦ".
- rewrite -wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc Nside_channel _ (stages γ P Q l v) with "[Hl HP]") as "#Hinv".
@@ -192,7 +191,7 @@ Section proofs.
{{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
Proof.
iIntros (Φ) "_ HΦ".
- rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+ wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc Nmailbox _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
{ iNext; by iLeft. }
iModIntro.
@@ -320,7 +319,6 @@ Section proofs.
{{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
Proof.
iIntros (Φ) "HP HΦ".
- rewrite -wp_fupd.
wp_lam.
wp_alloc l as "Hl".
wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index f9e8363e..6401ea0c 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -220,7 +220,7 @@ Section contents.
{{{ γ γ' t, RET t; isTask r γ γ' t P Q ∗ task γ γ' t a P Q }}}.
Proof.
iIntros (Φ) "[#Hrunner HP] HΦ".
- wp_rec. wp_pures. iApply wp_fupd.
+ wp_rec. wp_pures.
wp_alloc res as "Hres".
wp_alloc status as "Hstatus".
iMod (new_pending) as (γ) "[Htoken Htask]".
@@ -391,7 +391,7 @@ Section contents.
{{{ γb r, RET r; runner γb P Q r }}}.
Proof.
iIntros (Φ) "#Hf HΦ".
- unfold newRunner. iApply wp_fupd.
+ unfold newRunner.
wp_lam. wp_pures.
wp_bind (newBag b #()).
iApply (newBag_spec b (N.@"bag") (λ x y, ∃ γ γ', isTask (f,x) γ γ' y P Q)%I); auto.
@@ -400,7 +400,6 @@ Section contents.
iAssert (runner γb P Q (PairV f bag))%I with "[]" as "#Hrunner".
{ rewrite runner_unfold. iExists _,_. iSplit; eauto. }
iApply (loop_spec n 0 with "Hrunner [HΦ]"); eauto.
- iNext. iIntros (r) "Hr". by iApply "HΦ".
Qed.
Lemma runner_Fork_spec γb (r a:val) P Q :
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 28ec9c34..3db9c0cb 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -132,7 +132,7 @@ Section proof.
{{{ x γ, RET x; is_bag γ x ∗ bag_contents γ ∅ }}}.
Proof.
iIntros (Φ) "_ HΦ".
- unfold newBag. wp_rec. iApply wp_fupd.
+ unfold newBag. wp_rec.
wp_alloc r as "Hr".
iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done.
iMod (inv_alloc N _ (bag_inv γb r) with "[Ha Hr]") as "#Hinv".
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index e221d4a0..a35bcd31 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -264,7 +264,7 @@ Section monotone_counter.
Lemma newCounter_spec: {{{ True }}} newCounter #() {{{ v, RET #v; isCounter v 0 }}}.
Proof.
iIntros (Φ) "_ HCont".
- rewrite /newCounter -wp_fupd. (* See comment below for why we used wp_fupd. *)
+ rewrite /newCounter.
wp_lam.
(* We allocate ghost state using the rule/lemma own_alloc. Since the
conclusion of the rule is under a modality we wrap the application of
@@ -275,10 +275,7 @@ Section monotone_counter.
iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γ) "[HAuth HFrac]".
- apply mcounterRA_valid_auth_frag; auto. (* NOTE: We use the validity property of the RA we have constructed. *)
- wp_alloc ℓ as "Hpt".
- (* We now allocate an invariant. For this it is crucial we have used the
- wp_fupd lemma above to have the Φ under a modality. Otherwise we would
- have been stuck here, since allocating an invariant is only possible
- under the fancy update modality. *)
+ (* We now allocate an invariant. *)
iMod (inv_alloc N _ (counter_inv ℓ γ) with "[Hpt HAuth]") as "HInv".
+ iExists 0%nat; iFrame.
+ iApply ("HCont" with "[HFrac HInv]").
@@ -465,7 +462,7 @@ Section monotone_counter'.
Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v (MaxNat 0) }}}.
Proof.
iIntros (Φ) "_ HCont".
- rewrite /newCounter -wp_fupd.
+ rewrite /newCounter.
wp_lam.
iMod (own_alloc (● MaxNat 0 ⋅ ◯ MaxNat 0)) as (γ) "[HAuth HFrac]".
- apply mcounterRA_valid_auth_frag'; auto.
@@ -612,7 +609,7 @@ Section ccounter.
newCounter #()
{{{ γ ℓ, RET #ℓ; is_ccounter γ ℓ 1 0%nat }}}.
Proof.
- iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
+ iIntros (Φ) "_ HΦ". rewrite /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
iMod (own_alloc (●F O%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_discrete.
iMod (inv_alloc N _ (ccounter_inv γ ℓ) with "[Hpt Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index 23554be3..adbd9d8e 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -72,7 +72,7 @@ Section lock_spec.
{{{ P }}} newlock #() {{{ l, RET l; ∃ γ, is_lock γ l P }}}.
Proof.
iIntros (φ) "Hi Hcont".
- rewrite -wp_fupd /newlock.
+ rewrite /newlock.
wp_lam.
wp_alloc l as "HPt".
iMod (own_alloc (Excl ())) as (γ) "Hld"; first done.
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 2fc8ffe5..dc4aea9d 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -87,7 +87,7 @@ Section lock_spec.
{{{ True }}} newlock #() {{{v, RET v; ∃ (l: loc) γ, ⌜v = #l⌝ ∧ (∀ P E, P ={E}=∗ is_lock γ l P) }}}.
Proof.
iIntros (φ) "Hi Hcont".
- rewrite -wp_fupd /newlock.
+ rewrite /newlock.
wp_lam.
wp_alloc l as "HPt".
iApply "Hcont".
@@ -147,7 +147,7 @@ Section lock_spec.
True ⊢ WP newlock #() {{v, ∃ (l: loc) γ, ⌜v = #l⌝ ∧ (∀ P E, P ={E}=∗ is_lock γ l P) }}.
Proof.
iIntros "_".
- rewrite -wp_fupd /newlock.
+ rewrite /newlock.
wp_lam.
wp_alloc l as "HPt".
iExists l.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index c209851d..b9f972f5 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -126,7 +126,6 @@ Section cnt_spec.
{{{ True }}} newcounter #m @ E {{{ (ℓ : loc), RET #ℓ; ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m}}}.
Proof.
iIntros (Hsubset Φ) "#Ht HΦ".
- rewrite -wp_fupd.
wp_lam.
wp_alloc ℓ as "Hl".
iApply "HΦ".
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 0e281a4a..cb0161ad 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -172,7 +172,7 @@ Section stack.
Lemma new_stack_spec :
{{{ True }}} new_stack #() {{{ γs s, RET s; is_stack γs s ∗ stack_content γs [] }}}.
Proof.
- iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
+ iIntros (Φ) "_ HΦ". wp_lam.
wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index a23623a6..27d13320 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -49,7 +49,7 @@ Section proofs.
Lemma new_bag_spec:
{{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Proof.
- iIntros (Φ) "_ HΦ". iApply wp_fupd.
+ iIntros (Φ) "_ HΦ".
wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc s as "Hs".
iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 9bd22ad3..3f278c7c 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1482,7 +1482,7 @@ Lemma new_queue_spec sz :
new_queue #sz
{{{ v γ, RET v; is_hwq sz γ v ∗ hwq_cont γ [] }}}.
Proof.
- iIntros (Hsz Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+ iIntros (Hsz Φ) "_ HΦ". wp_lam.
(** Allocate [q.ar], [q.back] and [q.p]. *)
wp_apply wp_allocN; [ lia | done | iIntros (ℓa) "[Hℓa _]" ].
wp_alloc ℓb as "Hℓb".
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 8b856f69..60ca60a5 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -130,7 +130,6 @@ Section atomic_snapshot.
Proof.
iIntros (Φ _) "Hx". rewrite /new_snapshot. wp_lam.
repeat (wp_proj; wp_let).
- iApply wp_fupd.
wp_alloc lx' as "Hlx'".
wp_alloc lx as "Hlx".
set (Excl' v) as p.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 1b3cbf96..939bb31c 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -215,8 +215,6 @@ Proof.
(* Introduce things into the Coq and Iris contexts. Throw away the [True]
precondition. *)
iIntros (Φ) "_ HΦ".
- (* We introduce the fancy update modality in our WP (necessary later). *)
- iApply wp_fupd.
(* We step through the program: β-reduce and allocate a location [ℓ]. *)
wp_lam. wp_alloc ℓ as "Hl". (* We have full ownership of [ℓ] in [Hl]. *)
(* We now need to establish the invariant. First, we allocate an instance of
--
GitLab