Merge branch 'ralf/texan' into 'master'

Change the way we handle view shifts in post-conditions

Now we try to avoid adding them unnecessarily, so we don't have to remove them automatically any more.

The overall tally in the proofs (i.e., excluding changes in proof mode and lifting lemmas) is: 14 removed `iModIntro` (and equivalent tactics), 7 insertions of `wp_fupd`. So it seems we actually more often do not need that final update than we do need it. Not to mention this also simplifies the lifting lemmas and the proof mode, doing less unnecessary work (adding updates and then removing them again).

On the minus side, *if* the update is missing, unexperienced users will have a hard time figuring out what to do. The change typically needs to be made at the beginning of the proof, the problem only surfaces at the end. This could be mitigated by providing a tactic for proving texan triples that does the `wp_fupd` (and the introducing the `\Phi`). While this would re-add most of the 14 removed `iModIntro`, we could still keep the simplified lifting lemmas and proof mode.

Cc @robbertkrebbers @jjourdan what do you think?

See merge request !20

base_logic/derived.v

@@ -352,14 +352,8 @@ Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
 Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
 Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R.
 Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply P Q R S : (P ⊢ Q -★ R) → (S ⊢ P ★ Q) → S ⊢ R.
+Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
 Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
 Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
 Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.

heap_lang/derived.v

@@ -46,8 +46,8 @@ Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
 Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
-  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+  (n1 ≤ n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -55,8 +55,8 @@ Proof.
 Qed.
 
 Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (n1 < n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
-  (n2 ≤ n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -65,8 +65,8 @@ Qed.
 
 Lemma wp_eq E e1 e2 v1 v2 P Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (v1 = v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
-  (v1 ≠ v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
+  (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (v1 ≠ v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].

heap_lang/heap.v

@@ -122,12 +122,12 @@ Section heap.
   (** Weakest precondition *)
   Lemma wp_alloc E e v :
     to_val e = Some v → nclose heapN ⊆ E →
-    {{{ heap_ctx }}} Alloc e @ E {{{ l; LitV (LitLoc l), l ↦ v }}}.
+    {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
   Proof.
-    iIntros (<-%of_to_val ? Φ) "[#Hinv HΦ]". rewrite /heap_ctx.
+    iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
     iMod (auth_empty heap_name) as "Ha".
     iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !>".
+    iApply (wp_alloc_pst with "Hσ"). iNext. iIntros (l) "[% Hσ]".
     iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
@@ -137,26 +137,26 @@ Section heap.
   Lemma wp_load E l q v :
     nclose heapN ⊆ E →
     {{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
-    {{{; v, l ↦{q} v }}}.
+    {{{ RET v; l ↦{q} v }}}.
   Proof.
-    iIntros (? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+    iApply (wp_load_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+    iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
   Lemma wp_store E l v' e v :
     to_val e = Some v → nclose heapN ⊆ E →
     {{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
-    {{{; LitV LitUnit, l ↦ v }}}.
+    {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
-    iIntros (<-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
+    iApply (wp_store_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
+    iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }
@@ -166,26 +166,26 @@ Section heap.
   Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E →
     {{{ heap_ctx ★ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
-    {{{; LitV (LitBool false), l ↦{q} v' }}}.
+    {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+    iApply (wp_cas_fail_pst _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
+    iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
   Lemma wp_cas_suc E l e1 v1 e2 v2 :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
     {{{ heap_ctx ★ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
-    {{{; LitV (LitBool true), l ↦ v2 }}}.
+    {{{ RET LitV (LitBool true); l ↦ v2 }}}.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
+    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
+    iApply (wp_cas_suc_pst _ σ with "Hσ"); first by eauto using heap_singleton_included.
+    iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
     { iFrame. iPureIntro. rewrite to_heap_insert.
       eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }

heap_lang/lib/barrier/proof.v

@@ -92,10 +92,10 @@ Qed.
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp Σ) :
   heapN ⊥ N →
-  {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
+  {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ★ send l P }}}.
 Proof.
-  iIntros (HN Φ) "[#? HΦ]".
-  rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
+  iIntros (HN Φ) "#? HΦ".
+  rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -117,10 +117,10 @@ Proof.
 Qed.
 
 Lemma signal_spec l P :
-  {{{ send l P ★ P }}} signal #l {{{; #(), True }}}.
+  {{{ send l P ★ P }}} signal #l {{{ RET #(); True }}}.
 Proof.
   rewrite /signal /send /barrier_ctx /=.
-  iIntros (Φ) "((Hs&HP)&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
+  iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   destruct p; [|done]. wp_store.
@@ -133,10 +133,10 @@ Proof.
 Qed.
 
 Lemma wait_spec l P:
-  {{{ recv l P }}} wait #l {{{ ; #(), P }}}.
+  {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
-  iIntros (Φ) "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
@@ -158,7 +158,7 @@ Proof.
       iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
     iModIntro. wp_if.
-    iModIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+    iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
 
 Lemma recv_split E l P1 P2 :

heap_lang/lib/barrier/specification.v

@@ -20,10 +20,10 @@ Proof.
   intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); first done.
-    iSplit; first done. iNext. eauto.
-  - iIntros (l P) "!# [Hl HP]". iApply signal_spec; iFrame "Hl HP"; by eauto.
-  - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
+  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
+    iNext. eauto.
+  - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
+  - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
   - iIntros (l P Q) "!#". by iApply recv_split.
   - apply recv_weaken.
 Qed.

heap_lang/lib/counter.v

@@ -35,9 +35,9 @@ Section mono_proof.
 
   Lemma newcounter_mono_spec (R : iProp Σ) :
     heapN ⊥ N →
-    {{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}.
+    {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -45,9 +45,9 @@ Section mono_proof.
   Qed.
 
   Lemma inc_mono_spec l n :
-    {{{ mcounter l n }}} inc #l {{{; #(), mcounter l (S n) }}}.
+    {{{ mcounter l n }}} inc #l {{{ RET #(); mcounter l (S n) }}}.
   Proof.
-    iIntros (Φ) "[Hl HΦ]". iLöb as "IH". wp_rec.
+    iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
     iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
@@ -70,9 +70,9 @@ Section mono_proof.
   Qed.
 
   Lemma read_mono_spec l j :
-    {{{ mcounter l j }}} read #l {{{ i; #i, ■ (j ≤ i)%nat ∧ mcounter l i }}}.
+    {{{ mcounter l j }}} read #l {{{ i, RET #i; ■ (j ≤ i)%nat ∧ mcounter l i }}}.
   Proof.
-    iIntros (ϕ) "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
+    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]")
       as %[?%mnat_included _]%auth_valid_discrete_2.
@@ -112,9 +112,9 @@ Section contrib_spec.
   Lemma newcounter_contrib_spec (R : iProp Σ) :
     heapN ⊥ N →
     {{{ heap_ctx }}} newcounter #()
-    {{{ γ l; #l, ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
+    {{{ γ l, RET #l; ccounter_ctx γ l ★ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat))))
       as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
@@ -124,9 +124,9 @@ Section contrib_spec.
 
   Lemma inc_contrib_spec γ l q n :
     {{{ ccounter_ctx γ l ★ ccounter γ q n }}} inc #l
-    {{{; #(), ccounter γ q (S n) }}}.
+    {{{ RET #(); ccounter γ q (S n) }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)". iLöb as "IH". wp_rec.
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iModIntro. wp_let. wp_op.
@@ -145,9 +145,9 @@ Section contrib_spec.
 
   Lemma read_contrib_spec γ l q n :
     {{{ ccounter_ctx γ l ★ ccounter γ q n }}} read #l
-    {{{ c; #c, ■ (n ≤ c)%nat ∧ ccounter γ q n }}}.
+    {{{ c, RET #c; ■ (n ≤ c)%nat ∧ ccounter γ q n }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]")
       as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
@@ -157,9 +157,9 @@ Section contrib_spec.
 
   Lemma read_contrib_spec_1 γ l n :
     {{{ ccounter_ctx γ l ★ ccounter γ 1 n }}} read #l
-    {{{ n; #n, ccounter γ 1 n }}}.
+    {{{ n, RET #n; ccounter γ 1 n }}}.
   Proof.
-    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
+    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
     apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.

heap_lang/lib/lock.v

@@ -18,11 +18,11 @@ Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operation specs -- *)
   newlock_spec N (R : iProp Σ) :
     heapN ⊥ N →
-    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock N γ lk R }}};
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
   acquire_spec N γ lk R :
-    {{{ is_lock N γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}};
+    {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}};
   release_spec N γ lk R :
-    {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}
+    {{{ is_lock N γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}
 }.
 
 Arguments newlock {_ _} _.

heap_lang/lib/par.v

@@ -16,6 +16,10 @@ Global Opaque par.
 Section proof.
 Context `{!heapG Σ, !spawnG Σ}.
 
+(* Notice that this allows us to strip a later *after* the two Ψ have been
+   brought together.  That is strictly stronger than first stripping a later
+   and then merging them, as demonstrated by [tests/joining_existentials.v].
+   This is why these are not Texan triples. *)
 Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) :
   to_val e = Some (f1,f2)%V →
   (heap_ctx ★ WP f1 #() {{ Ψ1 }} ★ WP f2 #() {{ Ψ2 }} ★
@@ -23,11 +27,11 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
   ⊢ WP par e {{ Φ }}.
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
-  rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
-  wp_apply (spawn_spec parN with "[- $Hh $Hf1]"); try wp_done; try solve_ndisj.
+  rewrite /par. wp_value. wp_let. wp_proj.
+  wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
-  wp_apply (join_spec with "[- $Hl]"). iIntros (w) "H1".
+  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 

heap_lang/lib/spawn.v

@@ -49,31 +49,31 @@ Proof. solve_proper. Qed.
 Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   to_val e = Some f →
   heapN ⊥ N →
-  {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l; #l, join_handle l Ψ }}}.
+  {{{ heap_ctx ★ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "((#Hh & Hf) & HΦ)". rewrite /spawn /=.
+  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
   wp_apply wp_fork; simpl. iSplitR "Hf".
-  - iModIntro. wp_seq. iModIntro. iApply "HΦ". rewrite /join_handle. eauto.
+  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]" "Hclose".
     wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :
-  {{{ join_handle l Ψ }}} join #l {{{ v; v, Ψ v }}}.
+  {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
 Proof.
-  rewrite /join_handle; iIntros (Φ) "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+  rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
-    iModIntro. wp_match. iApply ("IH" with "Hγ [Hv]"). auto.
+    iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
-      iModIntro. wp_match. by iApply "Hv".
+      iModIntro. wp_match. by iApply "HΦ".
     + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.

heap_lang/lib/spin_lock.v

@@ -47,9 +47,9 @@ Section proof.
 
   Lemma newlock_spec (R : iProp Σ):
     heapN ⊥ N →
-    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (? Φ) "[[#Hh HR] HΦ]". rewrite /newlock /=.
+    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -59,9 +59,9 @@ Section proof.
 
   Lemma try_acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} try_acquire lk
-    {{{b; #b, if b is true then locked γ ★ R else True }}}.
+    {{{ b, RET #b; if b is true then locked γ ★ R else True }}}.
   Proof.
-    iIntros (Φ) "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
     wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
     - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
       iModIntro. iApply ("HΦ" $! false). done.
@@ -71,18 +71,18 @@ Section proof.
   Qed.
 
   Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
+    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}.
   Proof.
-    iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "[- $Hl]"). iIntros ([]).
-    - iIntros "[Hlked HR]". wp_if. iModIntro. iApply "HΦ"; iFrame.
+    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
+    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 
   Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
+    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}.
   Proof.
-    iIntros (Φ) "((Hlock & Hlocked & HR) & HΦ)".
+    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
     iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.

heap_lang/lib/ticket_lock.v

@@ -76,9 +76,9 @@ Section proof.
 
   Lemma newlock_spec (R : iProp Σ) :
     heapN ⊥ N →
-    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}.
+    {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (HN Φ) "((#Hh & HR) & HΦ)". rewrite /newlock /=.
+    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
     iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
@@ -89,9 +89,9 @@ Section proof.
   Qed.
 
   Lemma wait_loop_spec γ lk x R :
-    {{{ issued γ lk x R }}} wait_loop #x lk {{{; #(), locked γ ★ R }}}.
+    {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ★ R }}}.
   Proof.
-    iIntros (Φ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
+    iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -99,7 +99,7 @@ Section proof.
       + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iModIntro. wp_let. wp_op=>[_|[]] //.
-        wp_if. iModIntro.
+        wp_if. 
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
         set_solver.
@@ -110,9 +110,9 @@ Section proof.
   Qed.
 
   Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
+    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ★ R }}}.
   Proof.
-    iIntros (ϕ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
@@ -131,8 +131,9 @@ Section proof.
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       iModIntro. wp_if.
-      iApply (wait_loop_spec γ (#lo, #ln)).
-      iFrame "HΦ". rewrite /issued; eauto 10.
+      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+      + rewrite /issued; eauto 10.
+      + by iNext. 
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
@@ -140,9 +141,9 @@ Section proof.
   Qed.
 
   Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{; #(), True }}}.
+    {{{ is_lock γ lk R ★ locked γ ★ R }}} release lk {{{ RET #(); True }}}.
   Proof.
-    iIntros (Φ) "((Hl & Hγ & HR) & HΦ)".
+    iIntros (Φ) "(Hl & Hγ & HR) HΦ".
     iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
     iDestruct "Hγ" as (o) "Hγo".
     rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.

heap_lang/lifting.v

@@ -46,59 +46,59 @@ Lemma wp_bind_ctxi {E e} Ki Φ :
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ v Φ :
-  ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
-  ⊢ WP Alloc (of_val v) @ E {{ Φ }}.
+Lemma wp_alloc_pst E σ v :
+  {{{ ▷ ownP σ }}} Alloc (of_val v) @ E
+  {{{ l, RET LitV (LitLoc l); σ !! l = None ∧ ownP (<[l:=v]>σ) }}}.
 Proof.
-  iIntros "[HP HΦ]".
+  iIntros (Φ) "HP HΦ".
   iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
   subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
 Qed.
 
-Lemma wp_load_pst E σ l v Φ :
+Lemma wp_load_pst E σ l v :
   σ !! l = Some v →
-  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+  intros ? Φ. apply (wp_lift_atomic_det_head_step' σ v σ); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_store_pst E σ l v v' Φ :
+Lemma wp_store_pst E σ l v v' :
   σ !! l = Some v' →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
+  {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
+Lemma wp_cas_fail_pst E σ l v1 v2 v' :
   σ !! l = Some v' → v' ≠ v1 →
-  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
-  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
+  {{{ RET LitV $ LitBool false; ownP σ }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
+Lemma wp_cas_suc_pst E σ l v1 v2 :
   σ !! l = Some v1 →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
-  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
+  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
+  {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
+  intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
     (<[l:=v2]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e Φ :
-  ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+  ▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite later_sep -(wp_value_fupd _ _ (Lit _)) // big_sepL_singleton.
+  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
   - intros; inv_head_step; eauto.
 Qed.
 
@@ -116,20 +116,20 @@ Qed.
 Lemma wp_un_op E op e v v' Φ :
   to_val e = Some v →
   un_op_eval op v = Some v' →
-  ▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}.
+  ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
-    -?wp_value_fupd'; eauto.
+    -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   bin_op_eval op v1 v2 = Some v' →
-  ▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
+  ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
-    -?wp_value_fupd'; eauto.
+    -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -149,19 +149,19 @@ Qed.
 
 Lemma wp_fst E e1 v1 e2 Φ :
   to_val e1 = Some v1 → is_Some (to_val e2) →
-  ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
+  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros ? [v2 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_fupd; eauto.
+  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 e2 v2 Φ :
   is_Some (to_val e1) → to_val e2 = Some v2 →
-  ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
+  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros [v1 ?] ?.
-  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_fupd; eauto.
+  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 

heap_lang/proofmode.v

@@ -22,10 +22,10 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   IntoLaterEnvs Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ |={E}=> Φ (LitV (LitLoc l)))) →
+    (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
+  intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
@@ -36,10 +36,10 @@ Lemma tac_wp_load Δ Δ' E i l q v Φ :
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ |={E}=> Φ v) →
+  (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_fupd -wp_load // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -51,10 +51,10 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  (Δ'' ⊢ Φ (LitV LitUnit)) →
   Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_fupd -wp_store // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
@@ -65,10 +65,10 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ |={E}=> Φ (LitV (LitBool false))) →
+  (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_fupd -wp_cas_fail // -assoc -always_and_sep_l.
+  intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -80,10 +80,10 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  (Δ'' ⊢ |={E}=> Φ (LitV (LitBool true))) →
+  (Δ'' ⊢ Φ (LitV (LitBool true))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros; subst. rewrite -wp_fupd -wp_cas_suc // -assoc -always_and_sep_l.
+  intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.

heap_lang/wp_tactics.v

@@ -18,20 +18,7 @@ Ltac wp_done :=
   | _ => fast_done
   end.
 
-(* sometimes, we want to keep the update modality, so only apply [fupd_intro]
-if we obtain a consecutive wp *)
-Ltac wp_strip_fupd :=
-  lazymatch goal with
-  | |- _ ⊢ |={?E}=> _ =>
-    etrans; [|apply fupd_intro];
-    match goal with
-    | |- _ ⊢ wp E _ _ => simpl
-    | |- _ ⊢ |={E,_}=> _ => simpl
-    | _ => fail
-    end
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
+Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
 
 Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
 
@@ -48,7 +35,6 @@ Ltac wp_finish := intros_revert ltac:(
   | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
      etrans; [|eapply wp_seq; wp_done]; wp_strip_later
   | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  | |- _ ⊢ |={_,_}=> _ => wp_strip_fupd
   end).
 
 Tactic Notation "wp_value" :=

program_logic/ectx_lifting.v

@@ -43,7 +43,7 @@ Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
   head_reducible e1 σ1 →
   ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
   ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
-    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+    Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
@@ -56,19 +56,19 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
   (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
   ▷ ownP σ1 ★ ▷ (ownP σ2 -★
-    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+    Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
-Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
+Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
   atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 ={E}=★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
+  {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
-    ?big_sepL_nil ?right_id; eauto.
+  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
+  rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :

program_logic/lifting.v

@@ -48,7 +48,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
   (▷ ownP σ1 ★ ▷ ∀ v2 σ2 efs, ■ prim_step e1 σ1 (of_val v2) σ2 efs ★ ownP σ2 -★
-    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+    Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
@@ -57,7 +57,7 @@ Proof.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
   edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
   iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
-  iMod "Hclose". iMod "HΦ". iApply wp_value; auto using to_of_val.
+  iMod "Hclose". iApply wp_value; auto using to_of_val.
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
@@ -66,7 +66,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
   (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
   ▷ ownP σ1 ★ ▷ (ownP σ2 -★
-    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+    Φ v2 ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.

program_logic/weakestpre.v

@@ -68,43 +68,43 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
 (* Texan triples *)
-Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
+      P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
+      P -★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
-  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
+     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
-  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : uPred_scope.
+     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
 
-Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }})
+      P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : C_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e @ E {{ Φ }})
+      P ⊢ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : C_scope.
-Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
-  (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e {{ Φ }})
+     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : C_scope.
-Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
-  (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e @ E {{ Φ }})
+     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : C_scope.
+     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : C_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.

tests/barrier_client.v

@@ -37,11 +37,12 @@ Section client.
   Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
   Proof.
     iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y) with "[- $Hh]"); first done.
+    wp_apply (newbarrier_spec N (y_inv 1 y) with "Hh"); first done.
     iIntros (l) "[Hr Hs]". wp_let.
     iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. iApply (signal_spec with "[- $Hs]"). iSplitL "Hy"; [|by eauto].
+      wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
+      iSplitR "Hy"; first by eauto.
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros (_ _) "_ !>"].

tests/counter.v

@@ -95,7 +95,7 @@ Lemma newcounter_spec N :
   heapN ⊥ N →
   heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}.
 Proof.
-  iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
+  iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
   rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
   iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
@@ -119,7 +119,7 @@ Proof.
     rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
     wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]").
     { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-    iModIntro. wp_if. iModIntro; rewrite {3}/C; eauto 10.
+    iModIntro. wp_if. rewrite {3}/C; eauto 10.
   - wp_cas_fail; first (intros [=]; abstract omega).
     iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
     iModIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.

tests/heap_lang.v

@@ -46,7 +46,7 @@ Section LiftingTests.
     iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - iApply ("IH" with "[%] HΦ"). omega.
-    - iApply fupd_intro. by assert (n1 = n2 - 1) as -> by omega.
+    - by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.