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.

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

@@ -127,7 +127,7 @@ Section heap.
     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. iFrame "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. }
@@ -143,7 +143,7 @@ Section heap.
     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σ !>".
+    iIntros "{$Hσ}"; iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
@@ -156,7 +156,7 @@ Section heap.
     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".
+    iIntros "{$Hσ}"; 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'. }
@@ -172,7 +172,7 @@ Section heap.
     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σ !>".
+    iIntros "{$Hσ}"; iNext; iIntros "Hσ".
     iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
   Qed.
 
@@ -184,8 +184,8 @@ Section heap.
     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 _ σ); first by eauto using heap_singleton_included.
+    iIntros "{$Hσ}". 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

@@ -95,7 +95,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
   {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
 Proof.
   iIntros (HN Φ) "[#? HΦ]".
-  rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
+  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 "[-]")
@@ -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/counter.v

@@ -37,7 +37,7 @@ Section mono_proof.
     heapN ⊥ N →
     {{{ heap_ctx }}} newcounter #() {{{ l; #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. }
@@ -114,7 +114,7 @@ Section contrib_spec.
     {{{ heap_ctx }}} newcounter #()
     {{{ γ l; #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γ]").

heap_lang/lib/par.v

@@ -23,7 +23,7 @@ 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.
+  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.

heap_lang/lib/spawn.v

@@ -57,7 +57,7 @@ Proof.
   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.

heap_lang/lib/spin_lock.v

@@ -49,7 +49,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; 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 "#?".
@@ -75,7 +75,7 @@ Section proof.
   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 "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 

heap_lang/lib/ticket_lock.v

@@ -78,7 +78,7 @@ Section proof.
     heapN ⊥ N →
     {{{ heap_ctx ★ R }}} newlock #() {{{ lk γ; 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. }
@@ -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.

heap_lang/lifting.v

@@ -46,47 +46,47 @@ 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; 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 {{{; v, ownP σ }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+  intros ? Φ. rewrite -(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
+  {{{; LitV LitUnit, ownP (<[l:=v]>σ) }}}.
 Proof.
   intros. rewrite-(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
+  {{{; LitV $ LitBool false, ownP σ }}}.
 Proof.
   intros. rewrite -(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
+  {{{; LitV $ LitBool true, ownP (<[l:=v2]>σ) }}}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
     (<[l:=v2]>σ)); eauto.
@@ -95,10 +95,10 @@ 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Δ. rewrite -wp_alloc // -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. rewrite -wp_load // -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. rewrite -wp_store // -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. rewrite -wp_cas_fail // -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. rewrite -wp_cas_suc // -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,7 +56,7 @@ 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.
 
@@ -65,7 +65,7 @@ Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
   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 ★ ▷ (ownP σ2 -★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
     ?big_sepL_nil ?right_id; eauto.

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.

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 {{ Φ }}.

tests/one_shot.v

@@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "[#? Hf] /=".
-  rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
+  rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
@@ -69,7 +69,7 @@ Proof.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
-    wp_let. iModIntro. iIntros "!#". wp_seq.
+    wp_let. iIntros "!#". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.