Make all the wp stuff (lemmas and tactics) preserve view shifts.

Concretely, when execution of any of the wp_ tactics does not yield
another wp, it will make sure that a view shift is kept. This
behavior was already partially there, but now it is hopefully more
consistent.

heap_lang/derived.v

@@ -46,8 +46,8 @@ Lemma wp_match_inr E e0 v0 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 ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (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 ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  (n1 < n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -64,8 +64,8 @@ Proof.
 Qed.
 
 Lemma wp_eq E (n1 n2 : Z) P Φ :
-  (n1 = n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n1 ≠ n2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  (n1 = n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n1 ≠ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].

heap_lang/heap.v

@@ -150,79 +150,79 @@ Section heap.
   (** Weakest precondition *)
   Lemma wp_alloc N E e v Φ :
     to_val e = Some v → nclose N ⊆ E →
-    heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
+    heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
     iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
-    iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
+    iIntros {l} "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
-    iFrame "Hheap". iSplit; first iPureIntro.
+    iFrame "Hheap". iSplitR; first iPureIntro.
     { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
     iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
   Lemma wp_load N E l q v Φ :
     nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)
+    heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
     iIntros {?} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iExists _; iSplit; first done.
+    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
     rewrite of_heap_singleton_op //. by iFrame.
   Qed.
 
   Lemma wp_store N E l v' e v Φ :
     to_val e = Some v → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))
+    heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
+    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
     { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
     rewrite of_heap_singleton_op //; eauto. by iFrame.
   Qed.
 
   Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))
+    heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {????} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iExists _; iSplit; first done.
+    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
     rewrite of_heap_singleton_op //. by iFrame.
   Qed.
 
   Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))
+    heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {???} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
+    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
     { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
     rewrite of_heap_singleton_op //; eauto. by iFrame.
   Qed.

heap_lang/lib/barrier/proof.v

@@ -100,7 +100,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
   iIntros {HN} "[#? HΦ]".
-  rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
+  rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
   iApply "HΦ".
   iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
   iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -127,7 +127,7 @@ Proof.
   rewrite /signal /send /barrier_ctx.
   iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
-  wp_store. destruct p; [|done].
+  wp_store. iPvsIntro. destruct p; [|done].
   iExists (State High I), (∅ : set token).
   iSplit; [iPureIntro; by eauto using signal_step|].
   iSplitR "HΦ"; [iNext|by auto].
@@ -143,7 +143,7 @@ Proof.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
-  wp_load. destruct p.
+  wp_load. iPvsIntro. destruct p.
   - (* a Low state. The comparison fails, and we recurse. *)
     iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
     { iNext. rewrite {2}/barrier_inv /=. by iFrame. }

heap_lang/lib/lock.v

@@ -51,7 +51,7 @@ Lemma newlock_spec N (R : iProp) Φ :
   heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
-  wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
+  wp_seq. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
   iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
   { iIntros ">". iExists false. by iFrame. }
@@ -64,10 +64,10 @@ Proof.
   iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
   iInv N as { [] } "[Hl HR]".
-  - wp_cas_fail. iSplitL "Hl".
+  - wp_cas_fail. iPvsIntro; iSplitL "Hl".
     + iNext. iExists true; eauto.
     + wp_if. by iApply "IH".
-  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+  - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true; eauto.
     + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto.
 Qed.
@@ -77,6 +77,6 @@ Lemma release_spec R l (Φ : val → iProp) :
 Proof.
   iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
   rewrite /release. wp_let. iInv N as {b} "[Hl _]".
-  wp_store. iFrame "HΦ". iNext. iExists false. by iFrame.
+  wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
 Qed.
 End proof.

heap_lang/lib/par.v

@@ -27,7 +27,8 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
-  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. wp_let. wp_proj.
+  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)".
+  rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
   wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
   iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.

heap_lang/lib/spawn.v

@@ -23,8 +23,7 @@ Class spawnG Σ := SpawnG {
 (** The functor we need. *)
 Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
 (* Show and register that they match. *)
-Instance inGF_spawnG
-  `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
+Instance inGF_spawnG `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
 Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
@@ -63,10 +62,10 @@ Proof.
   iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame; eauto. }
   wp_apply wp_fork. iSplitR "Hf".
-  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
+  - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
   - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
     iInv N as {v'} "[Hl _]"; first wp_done.
-    wp_store. iSplit; [iNext|done].
+    wp_store. iPvsIntro; iSplit; [iNext|done].
     iExists (InjRV v); iFrame; eauto.
 Qed.
 
@@ -76,10 +75,10 @@ Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
+  - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
     wp_match. iApply ("IH" with "Hγ Hv").
   - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
-    + iSplitL "Hl Hγ".
+    + iPvsIntro; iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame; eauto. }
       wp_match. by iApply "Hv".
     + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].

heap_lang/lifting.v

@@ -20,7 +20,7 @@ Proof. exact: wp_ectx_bind. Qed.
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →
-  ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LitV (LitLoc l)))
+  ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   iIntros {?}  "[HP HΦ]".
@@ -36,7 +36,7 @@ Qed.
 
 Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
-  ▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
@@ -44,7 +44,7 @@ Qed.
 
 Lemma wp_store_pst E σ l e v v' Φ :
   to_val e = Some v → σ !! l = Some v' →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit))
+  ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
   ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
@@ -53,7 +53,7 @@ Qed.
 
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
-  ▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false))
+  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
   ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
@@ -63,7 +63,7 @@ Qed.
 
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
-  ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true))
+  ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
   ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
@@ -73,11 +73,11 @@ Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e Φ :
-  ▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_head_step; eauto.
-  rewrite later_sep -(wp_value _ _ (Lit _)) //.
+  rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
 Qed.
 
 Lemma wp_rec E f x erec e1 e2 v2 Φ :
@@ -92,18 +92,18 @@ Qed.
 
 Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
-  ▷ Φ (LitV l') ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
-  ▷ Φ (LitV l') ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
@@ -122,18 +122,18 @@ Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_case_inl E e0 v0 e1 e2 Φ :

heap_lang/proofmode.v

@@ -22,7 +22,7 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
   IntoLaterEnvs Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
+    (Δ'' ⊢ |={E}=> Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
@@ -36,7 +36,7 @@ Lemma tac_wp_load Δ Δ' N E i l q v Φ :
   (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ Φ v) →
+  (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
@@ -50,7 +50,8 @@ Lemma tac_wp_store Δ Δ' Δ'' N 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 Δ'' →
-  (Δ'' ⊢ Φ (LitV LitUnit)) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -62,7 +63,7 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ Φ (LitV (LitBool false))) →
+  (Δ' ⊢ |={E}=> Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
@@ -76,7 +77,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' N 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 Δ'' →
-  (Δ'' ⊢ Φ (LitV (LitBool true))) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  (Δ'' ⊢ |={E}=> Φ (LitV (LitBool true))) →
+  Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros; subst.
   rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.

heap_lang/wp_tactics.v

@@ -11,27 +11,34 @@ Ltac wp_bind K :=
 
 Ltac wp_done := rewrite /= ?to_of_val; fast_done.
 
-Ltac wp_value_head :=
-  match goal with
-  | |- _ ⊢ wp _ _ _ =>
-    etrans; [|eapply wp_value_pvs; wp_done]; lazy beta;
-    (* sometimes, we will have to do a final view shift, so only apply
-    pvs_intro if we obtain a consecutive wp *)
-    try (
-      etrans; [|apply pvs_intro];
-      match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
+(* sometimes, we will have to do a final view shift, so only apply
+pvs_intro if we obtain a consecutive wp *)
+Ltac wp_strip_pvs :=
+  lazymatch goal with
+  | |- _ ⊢ |={?E}=> _ =>
+    etrans; [|apply pvs_intro];
+    match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
   end.
 
+Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta.
+
 Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
 
 Ltac wp_seq_head :=
   lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; wp_strip_later
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
   end.
 
 Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val; try wp_strip_later; try wp_value_head);
-  repeat wp_seq_head.
+  rewrite /= ?to_of_val;
+  try wp_strip_later;
+  repeat lazymatch goal with
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
+  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
+  | |- _ ⊢ |={_}=> _ => wp_strip_pvs
+  end).
 
 Tactic Notation "wp_value" :=
   lazymatch goal with

program_logic/ectx_lifting.v

@@ -39,7 +39,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1
   atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
+    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_step. Qed.
 
@@ -48,7 +49,7 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
   head_reducible e1 σ1 →
   (∀ e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :

program_logic/lifting.v

@@ -66,7 +66,8 @@ Lemma wp_lift_atomic_step {E Φ} e1
   reducible e1 σ1 →
   (∀ e2 σ2 ef,
     prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
+    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
@@ -77,7 +78,7 @@ Proof.
   apply forall_intro=>ef; apply wand_intro_l.
   rewrite always_and_sep_l -assoc -always_and_sep_l.
   apply pure_elim_l=>-[[v2 Hv] ?] /=.
-  rewrite -pvs_intro.
+  rewrite -pvs_intro -wp_pvs.
   rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) pure_equiv //.
   rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //.
   by erewrite of_to_val.
@@ -88,7 +89,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
   reducible e1 σ1 →
   (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //.

tests/one_shot.v

@@ -63,7 +63,7 @@ Proof.
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
       + iExists (InjLV #0). iFrame. eauto.
       + iExists (InjRV #m). iFrame. eauto. }
-    iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
+    iDestruct "Hv" as {v} "[Hl Hv]". wp_load; iPvsIntro.
     iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
       v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
@@ -75,11 +75,11 @@ Proof.
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
-    wp_load.
+    wp_load; iPvsIntro.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
-    wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
+    wp_match. iApply wp_assert'. wp_op=>?; iPvsIntro; simplify_eq/=; eauto.
 Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :