Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

_CoqProject

@@ -116,3 +116,4 @@ proofmode/invariants.v
 proofmode/weakestpre.v
 proofmode/ghost_ownership.v
 proofmode/sts.v
+proofmode/classes.v

algebra/cmra.v

@@ -698,8 +698,8 @@ End discrete.
 
 Notation discreteR A ra_mix :=
   (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
-Notation discreteLeibnizR A ra_mix :=
-  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
+Notation discreteUR A ra_mix ucmra_mix :=
+  (UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
 
 Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
   @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).

algebra/dec_agree.v

@@ -18,7 +18,6 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Instance dec_agree_equiv : Equiv (dec_agree A) := equivL.
 Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,

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

@@ -148,81 +148,82 @@ Section heap.
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
+  (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
   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

@@ -25,7 +25,7 @@ Proof. exact: weakestpre.wp_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Φ]".
@@ -41,7 +41,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.
@@ -49,7 +49,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)
@@ -58,7 +58,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)
@@ -68,7 +68,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)
@@ -78,18 +78,17 @@ 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 Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v2 →
-  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
-  ⊢ WP App e1 e2 @ E {{ Φ }}.
+  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
   intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
@@ -98,18 +97,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 Φ :
@@ -128,18 +127,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) //.

program_logic/weakestpre.v

@@ -257,9 +257,11 @@ Lemma wp_strip_pvs E e P Φ :
 Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
+Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
 Lemma wp_value_pvs E Φ e v :
   to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
-Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
+Proof. intros. rewrite -wp_pvs -wp_value //. Qed.
 Lemma wp_frame_l E e Φ R : R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_step_r' E e Φ R :

proofmode/pviewshifts.v

@@ -7,6 +7,8 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 
+Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
@@ -179,3 +181,6 @@ Tactic Notation "iTimeless" constr(H) :=
 
 Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
   iTimeless H; iDestruct H as Hs.
+
+Hint Extern 2 (of_envs _ ⊢ _) =>
+  match goal with |- _ ⊢ (|={_}=> _)%I => iPvsIntro end.

proofmode/tactics.v

 From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
 From iris.algebra Require Export upred.
-From iris.proofmode Require Export notation.
+From iris.proofmode Require Export classes notation.
 From iris.prelude Require Import stringmap hlist.
 
 Declare Reduction env_cbv := cbv [
@@ -112,13 +112,13 @@ Local Tactic Notation "iPersistent" constr(H) :=
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- IsPure ?P _ => P end in
+    |let P := match goal with |- IntoPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- IsPure ?P _ => P end in
+    [let P := match goal with |- FromPure ?P _ => P end in