Invariants over states in WP and get rid of heap_ctx.

The WP construction now takes an invariant on states as a parameter
(part of the irisG class) and no longer builds in the authoritative
ownership of the entire state. When instantiating WP with a concrete
language on can choose its state invariant. For example, for heap_lang
we directly use `auth (gmap loc (frac * dec_agree val))`, and avoid
the indirection through invariants entirely.

As a result, we no longer have to carry `heap_ctx` around.

heap_lang/adequacy.v

 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.base_logic.lib Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
 Class heapPreG Σ := HeapPreG {
-  heap_preG_iris :> irisPreG heap_lang Σ;
-  heap_preG_heap :> authG Σ heapUR
+  heap_preG_iris :> invPreG Σ;
+  heap_preG_heap :> inG Σ (authR heapUR)
 }.
 
-Definition heapΣ : gFunctors :=
-  #[irisΣ state; authΣ heapUR].
+Definition heapΣ : gFunctors := #[invΣ; GFunctor (constRF (authR heapUR))].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?]%subG_inv. split; apply _. Qed.
+Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
-  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iMod (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
-  { exact: to_heap_valid. }
-  set (Hheap := HeapG _ _ _ γ).
-  iApply (Hwp _). by rewrite /heap_ctx.
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
+  iMod (own_alloc (● to_heap σ)) as (γ) "Hh".
+  { apply: auth_auth_valid. exact: to_heap_valid. }
+  iModIntro. iExists (λ σ, own γ (● to_heap σ)); iFrame.
+  set (Hheap := HeapG _ _ _ γ). iApply (Hwp _).
 Qed.

heap_lang/heap.v

 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
 From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import wsat auth fractional.
+From iris.base_logic.lib Require Import fractional.
+From iris.program_logic Require Import ectx_lifting.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
    predicates over finmaps instead of just ownP. *)
 
-Definition heapN : namespace := nroot .@ "heap".
 Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
+Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
 
 (** The CMRA we need. *)
 Class heapG Σ := HeapG {
-  heapG_iris_inG :> irisG heap_lang Σ;
-  heap_inG :> authG Σ heapUR;
+  heapG_invG : invG Σ;
+  heap_inG :> inG Σ (authR heapUR);
   heap_name : gname
 }.
-
-Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
+Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
+  iris_invG := heapG_invG;
+  state_interp σ := own heap_name (● to_heap σ)
+}.
 
 Section definitions.
   Context `{heapG Σ}.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    auth_own heap_name ({[ l := (q, DecAgree v) ]}).
+    own heap_name (◯ {[ l := (q, DecAgree v) ]}).
   Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
   Definition heap_mapsto := proj1_sig heap_mapsto_aux.
   Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
     proj2_sig heap_mapsto_aux.
-
-  Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
 End definitions.
 
-Typeclasses Opaque heap_ctx heap_mapsto.
+Typeclasses Opaque heap_mapsto.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -43,6 +44,11 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : uPred_scope.
 
+Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+Local Hint Constructors head_step.
+Local Hint Resolve alloc_fresh.
+Local Hint Resolve to_of_val.
+
 Section heap.
   Context {Σ : gFunctors}.
   Implicit Types P Q : iProp Σ.
@@ -62,11 +68,6 @@ Section heap.
     move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
     by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
   Qed.
-  Lemma heap_singleton_included' σ l q v :
-    {[l := (q, DecAgree v)]} ≼ to_heap σ → to_heap σ !! l = Some (1%Qp,DecAgree v).
-  Proof.
-    intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
-  Qed.
   Lemma to_heap_insert l v σ :
     to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
   Proof. by rewrite /to_heap fmap_insert. Qed.
@@ -74,26 +75,22 @@ Section heap.
   Context `{heapG Σ}.
 
   (** General properties of mapsto *)
-  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
-  Proof. rewrite /heap_ctx. apply _. Qed.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
   Global Instance heap_mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
-    unfold Fractional; intros.
-    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
+    intros p q. by rewrite heap_mapsto_eq -own_op -auth_frag_op
+      op_singleton pair_op dec_agree_idemp.
   Qed.
   Global Instance heap_mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. done. Qed.
 
-  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid
-            op_singleton singleton_valid.
-    f_equiv. move=>[_ ] /=.
-    destruct (decide (v1 = v2)) as [->|?]; first done. by rewrite dec_agree_ne.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+    by move=> [_ /= /dec_agree_op_inv [?]].
   Qed.
 
   Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
@@ -109,8 +106,8 @@ Section heap.
 
   Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
   Proof.
-    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
-    by apply pure_mono=> /singleton_valid [??].
+    rewrite heap_mapsto_eq /heap_mapsto_def own_valid !discrete_valid.
+    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
   Qed.
   Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
     l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
@@ -121,74 +118,80 @@ Section heap.
 
   (** Weakest precondition *)
   Lemma wp_alloc E e v :
-    to_val e = Some v → ↑heapN ⊆ E →
-    {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+    to_val e = Some v →
+    {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
   Proof.
-    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 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. }
+    iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+    iMod (own_update with "Hσ") as "[Hσ Hl]".
+    { eapply auth_update_alloc,
+        (alloc_singleton_local_update _ _ (1%Qp, DecAgree _))=> //.
+      by apply lookup_to_heap_None. }
+    iModIntro; iSplit=> //. rewrite to_heap_insert. iFrame.
     iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
   Lemma wp_load E l q v :
-    ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
-    {{{ RET v; l ↦{q} v }}}.
+    {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}.
   Proof.
-    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 _ σ with "Hσ"); first eauto using heap_singleton_included.
-    iNext; iIntros "Hσ".
-    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
+    iIntros (Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
+    iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
+      as %[?%heap_singleton_included _]%auth_valid_discrete_2.
+    iSplit; first by eauto.
+    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 
   Lemma wp_store E l v' e v :
-    to_val e = Some v → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
-    {{{ RET LitV LitUnit; l ↦ v }}}.
+    to_val e = Some v →
+    {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
-    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 _ σ 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'. }
-    by iApply "HΦ".
+    iIntros (<-%of_to_val Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
+    iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
+      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
+    iSplit; first by eauto.
+    iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+    iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
+    { eapply auth_update, singleton_local_update,
+        (exclusive_local_update _ (1%Qp, DecAgree _))=> //.
+      by rewrite /to_heap lookup_fmap Hl. }
+    iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. by iApply "HΦ".
   Qed.
 
   Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
+    {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
   Proof.
-    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 _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
-    iNext; iIntros "Hσ".
-    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
+    iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
+    rewrite heap_mapsto_eq /heap_mapsto_def.
+    iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
+      as %[?%heap_singleton_included _]%auth_valid_discrete_2.
+    iSplit; first by eauto.
+    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. (* FIXME: this inversion is slow *)
+    iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 
   Lemma wp_cas_suc E l e1 v1 e2 v2 :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+    to_val e1 = Some v1 → to_val e2 = Some v2 →
+    {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{ RET LitV (LitBool true); l ↦ v2 }}}.
   Proof.
-    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 _ σ 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'. }
-    by iApply "HΦ".
+    iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
+    rewrite heap_mapsto_eq /heap_mapsto_def.
+    iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
+      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
+    iSplit; first by eauto.
+    iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+    iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
+    { eapply auth_update, singleton_local_update,
+        (exclusive_local_update _ (1%Qp, DecAgree _))=> //.
+      by rewrite /to_heap lookup_fmap Hl. }
+    iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. by iApply "HΦ".
   Qed.
 End heap.

heap_lang/lib/barrier/proof.v

@@ -38,7 +38,7 @@ Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ :=
   (l ↦ s ∗ ress (state_to_prop s P) (state_I s))%I.
 
 Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ :=
-  (⌜heapN ⊥ N⌝ ∗ heap_ctx ∗ sts_ctx γ N (barrier_inv l P))%I.
+  sts_ctx γ N (barrier_inv l P).
 
 Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
   (∃ γ, barrier_ctx γ l P ∗ sts_ownS γ low_states {[ Send ]})%I.
@@ -91,10 +91,9 @@ Qed.
 
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp Σ) :
-  heapN ⊥ N →
-  {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
+  {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
-  iIntros (HN Φ) "#? HΦ".
+  iIntros (Φ) "HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
@@ -120,7 +119,7 @@ Lemma signal_spec l P :
   {{{ 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 (γ) "[#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.
@@ -136,7 +135,7 @@ Lemma wait_spec 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) "(#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.
@@ -165,7 +164,7 @@ Lemma recv_split E l P1 P2 :
   ↑N ⊆ E → recv l (P1 ∗ P2) ={E}=∗ recv l P1 ∗ recv l P2.
 Proof.
   rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
-  iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   iMod (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".

heap_lang/lib/barrier/specification.v

@@ -8,19 +8,17 @@ Section spec.
 Context `{!heapG Σ} `{!barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :
-  heapN ⊥ N →
   ∃ recv send : loc → iProp Σ -n> iProp Σ,
-    (∀ P, heap_ctx ⊢ {{ True }} newbarrier #()
+    (∀ P, {{ True }} newbarrier #()
                      {{ v, ∃ l : loc, ⌜v = #l⌝ ∗ recv l P ∗ send l P }}) ∧
     (∀ l P, {{ send l P ∗ P }} signal #l {{ _, True }}) ∧
     (∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧
     (∀ l P Q, recv l (P ∗ Q) ={↑N}=> recv l P ∗ recv l Q) ∧
     (∀ l P Q, (P -∗ Q) ⊢ recv l P -∗ recv l Q).
 Proof.
-  intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
+  - 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.

heap_lang/lib/counter.v

@@ -24,18 +24,16 @@ Section mono_proof.
     (∃ n, own γ (● (n : mnat)) ∗ l ↦ #n)%I.
 
   Definition mcounter (l : loc) (n : nat) : iProp Σ :=
-    (∃ γ, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
-          inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
+    (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
 
   (** The main proofs. *)
   Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_mono_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
+    {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "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. }
@@ -46,7 +44,7 @@ Section mono_proof.
     {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
-    iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
+    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|].
     iModIntro. wp_let. wp_op.
@@ -70,7 +68,7 @@ Section mono_proof.
   Lemma read_mono_spec l j :
     {{{ 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.
@@ -97,7 +95,7 @@ Section contrib_spec.
     (∃ n, own γ (● Some (1%Qp, n)) ∗ l ↦ #n)%I.
 
   Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
-    (⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ inv N (ccounter_inv γ l))%I.
+    inv N (ccounter_inv γ l).
 
   Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
     own γ (◯ Some (q, n)).
@@ -108,11 +106,10 @@ Section contrib_spec.
   Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.
 
   Lemma newcounter_contrib_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx }}} newcounter #()
+    {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "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,7 +121,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} incr #l
     {{{ 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,7 +142,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
     {{{ 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,7 +154,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
     {{{ 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

@@ -17,8 +17,7 @@ Structure lock Σ `{!heapG Σ} := Lock {
   locked_exclusive γ : locked γ ∗ locked γ ⊢ False;
   (* -- operation specs -- *)
   newlock_spec N (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
   acquire_spec N γ lk R :
     {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
   release_spec N γ lk R :

heap_lang/lib/par.v

@@ -21,13 +21,13 @@ Context `{!heapG Σ, !spawnG Σ}.
    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 }} ∗
+  (WP f1 #() {{ Ψ1 }} ∗ WP f2 #() {{ Ψ2 }} ∗
    ▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
+  iIntros (?) "(Hf1 & Hf2 & HΦ)".
   rewrite /par. wp_value. wp_let. wp_proj.
-  wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
+  wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
@@ -36,11 +36,11 @@ Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
     (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) :
-  (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗
+  (WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗
    ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 ||| e2 {{ Φ }}.
 Proof.
-  iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- $Hh $H]"); try wp_done.
+  iIntros "(H1 & H2 & H)". iApply (par_spec Ψ1 Ψ2 with "[- $H]"); try wp_done.
   iSplitL "H1"; by wp_let.
 Qed.
 End proof.

heap_lang/lib/spawn.v

@@ -32,8 +32,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :
                    ∃ v, ⌜lv = SOMEV v⌝ ∗ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (⌜heapN ⊥ N⌝ ∗ ∃ γ, heap_ctx ∗ own γ (Excl ()) ∗
-                    inv N (spawn_inv γ l Ψ))%I.
+  (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
 
 Typeclasses Opaque join_handle.
 
@@ -47,10 +46,9 @@ Proof. solve_proper. Qed.
 (** The main proofs. *)
 Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   to_val e = Some f →
-  heapN ⊥ N →
-  {{{ heap_ctx ∗ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
+  {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
+  iIntros (<-%of_to_val Φ) "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 "#?".
@@ -65,7 +63,7 @@ Qed.
 Lemma join_spec (Ψ : val → iProp Σ) l :
   {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
 Proof.
-  rewrite /join_handle; iIntros (Φ) "[% H] HΦ". 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|].

heap_lang/lib/spin_lock.v

@@ -26,7 +26,7 @@ Section proof.
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ l: loc, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
+    (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
 
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
@@ -45,10 +45,9 @@ Section proof.
   Proof. apply _. Qed.
 
   Lemma newlock_spec (R : iProp Σ):
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
+    iIntros (Φ) "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 "#?".
@@ -60,7 +59,7 @@ Section proof.
     {{{ is_lock γ lk R }}} try_acquire lk
     {{{ 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.
@@ -82,7 +81,7 @@ Section proof.
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
-    iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
+    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.
   Qed.

heap_lang/lib/ticket_lock.v

@@ -46,12 +46,10 @@ Section proof.
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     (∃ lo ln : loc,
-       ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
        ⌜lk = (#lo, #ln)%V⌝ ∧ inv N (lock_inv γ lo ln R))%I.
 
   Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
     (∃ lo ln: loc,
-       ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
        ⌜lk = (#lo, #ln)%V⌝ ∧ inv N (lock_inv γ lo ln R) ∧
        own γ (◯ (∅, GSet {[ x ]})))%I.
 
@@ -74,10 +72,9 @@ Section proof.
   Qed.
 
   Lemma newlock_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock.
+    iIntros (Φ) "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. }
@@ -90,7 +87,7 @@ Section proof.
   Lemma wait_loop_spec γ lk x 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].
@@ -111,7 +108,7 @@ Section proof.
   Lemma acquire_spec γ lk 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 "_".
@@ -142,8 +139,7 @@ Section proof.
   Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
-    iIntros (Φ) "(Hl & Hγ & HR) HΦ".
-    iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
+    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.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".

heap_lang/lifting.v

@@ -45,52 +45,6 @@ Lemma wp_bind_ctxi {E e} Ki Φ :
      WP fill_item Ki e @ E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-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Φ".
-  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
-Qed.
-
-Lemma wp_load_pst E σ l v :
-  σ !! l = Some v →
-  {{{ ▷ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
-Proof.
-  intros ? Φ. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_store_pst E σ l v v' :
-  σ !! l = Some v' →
-  {{{ ▷ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_cas_fail_pst E σ l v1 v2 v' :
-  σ !! l = Some v' → v' ≠ v1 →
-  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
-  {{{ RET LitV $ LitBool false; ownP σ }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_cas_suc_pst E σ l v1 v2 :
-  σ !! l = Some v1 →
-  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
-  {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-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 {{ Φ }}.
@@ -106,7 +60,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
   Closed (f :b: x :b: []) erec →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
-  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step' (App _ _)
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -116,7 +70,7 @@ Lemma wp_un_op E op e v v' Φ :
   un_op_eval op v = Some v' →
   ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
     -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -126,7 +80,7 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
   bin_op_eval op v1 v2 = Some v' →
   ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
     -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -134,14 +88,14 @@ Qed.
 Lemma wp_if_true E e1 e2 Φ :
   ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
-  apply wp_lift_pure_det_head_step'; eauto.
+  apply wp_lift_pure_det_head_step_no_fork; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
   ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
-  apply wp_lift_pure_det_head_step'; eauto.
+  apply wp_lift_pure_det_head_step_no_fork; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -150,7 +104,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
   ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros ? [v2 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value; eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -159,7 +113,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
   ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros [v1 ?] ?.
-  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value; eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -168,7 +122,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e1 e0)); eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -177,7 +131,7 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e2 e0)); eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 End lifting.

heap_lang/proofmode.v

@@ -14,73 +14,63 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
-  apply and_intro; first done.
-  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
+  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
 
 Lemma tac_wp_load Δ Δ' E i l q v Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   to_val e = Some v' →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   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 {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   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 {{ Φ }}.
 Proof.
-  intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -103,8 +93,6 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
     eapply tac_wp_alloc with _ H _;
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_alloc:" e' "not a value"
-      |iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_alloc: cannot open heap invariant"
       |apply _
       |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
         eexists; split;
@@ -124,9 +112,7 @@ Tactic Notation "wp_load" :=
          match eval hnf in e' with Load _ => wp_bind_core K end)
       |fail 1 "wp_load: cannot find 'Load' in" e];
     eapply tac_wp_load;
-      [iAssumption || fail "wp_load: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_load: cannot open heap invariant"
-      |apply _
+      [apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
       |wp_finish]
@@ -143,8 +129,6 @@ Tactic Notation "wp_store" :=
     eapply tac_wp_store;
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_store:" e' "not a value"
-      |iAssumption || fail "wp_store: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_store: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
@@ -165,8 +149,6 @@ Tactic Notation "wp_cas_fail" :=
        wp_done || fail "wp_cas_fail:" e' "not a value"
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_fail:" e' "not a value"
-      |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_cas_fail: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -187,8 +169,6 @@ Tactic Notation "wp_cas_suc" :=
        wp_done || fail "wp_cas_suc:" e' "not a value"
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_suc:" e' "not a value"
-      |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_cas_suc: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"

program_logic/adequacy.v

@@ -22,21 +22,6 @@ Proof.
   intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
 Qed.
 
-
-Definition irisΣ (Λstate : Type) : gFunctors :=
-  #[invΣ;
-    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
-
-Class irisPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
-  inv_inG :> invPreG Σ;
-  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
-}.
-Notation irisPreG Λ Σ := (irisPreG' (state Λ) Σ).
-
-Instance subG_irisΣ {Λstate Σ} : subG (irisΣ Λstate) Σ → irisPreG' Λstate Σ.
-Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
-
-
 (* Allocation *)
 Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
@@ -49,17 +34,6 @@ Proof.
   iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
 Qed.
 
-Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
-  (|==> ∃ _ : irisG' Λstate Σ, wsat ∗ ownE ⊤ ∗ ownP_auth σ ∗ ownP σ)%I.
-Proof.
-  iIntros.
-  iMod wsat_alloc as (?) "[Hws HE]".
-  iMod (own_alloc (● (Excl' (σ:leibnizC Λstate)) ⋅ ◯ (Excl' σ)))
-    as (γσ) "[Hσ Hσ']"; first done.
-  iModIntro; iExists (IrisG _ _ _ _ γσ). rewrite /ownP_auth /ownP; iFrame.
-Qed.
-
-
 (* Program logic adequacy *)
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
@@ -91,7 +65,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ ownP_auth σ)%I.
+Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
 
 Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
 
@@ -104,8 +78,7 @@ Proof.
   rewrite fupd_eq /fupd_def.
   iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
   iModIntro; iNext.
-  iMod ("H" $! e2 σ2 efs with "[%] [Hw HE]")
-    as ">($ & $ & $ & $)"; try iFrame; eauto.
+  by iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)".
 Qed.
 
 Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
@@ -178,50 +151,58 @@ Proof.
   iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
+Lemma wptp_invariance I n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
-  I ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ σ2⌝.
+  I ∗ (state_interp σ2 -∗ I ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ⌝.
 Proof.
-  intros ? HI. rewrite wptp_steps //.
-  rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono.
-  iIntros "[HI H]".
+  intros ?. rewrite wptp_steps //.
+  rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
+  iIntros "(HI & Hback & H)".
   iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
-  rewrite fupd_eq in HI;
-    iMod (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
-  iDestruct "H" as (σ2') "[Hσf %]".
-  iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
+  rewrite fupd_eq.
+  iMod ("Hback" with "Hσ HI [$Hw $HE]") as "> (_ & _ & $)"; auto.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
-  (∀ `{irisG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Theorem wp_adequacy Σ Λ `{invPreG Σ} (e : expr Λ) σ φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
     eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(?&?&?&Hσ)".
-    iModIntro. iNext. iApply wptp_result; eauto.
-    iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
+    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]".
+    iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
+    iFrame. by iApply big_sepL_nil.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
-    iModIntro. iNext. iApply wptp_safe; eauto.
-    iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
+    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]".
+    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
+    iFrame. by iApply big_sepL_nil.
 Qed.
 
-Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=∗ I ∗ WP e {{ Φ }}) →
-  (∀ `{irisG Λ Σ}, I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+Theorem wp_invariance {Λ} `{invPreG Σ} e σ1 t2 σ2 I φ Φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ1 ∗ I ∗ WP e {{ Φ }} ∗
+         (stateI σ2 -∗ I ={⊤,∅}=∗ ⌜φ⌝)) →
   rtc step ([e], σ1) (t2, σ2) →
-  φ σ2.
+  φ.
 Proof.
-  intros Hwp HI [n ?]%rtc_nsteps.
+  intros Hwp [n ?]%rtc_nsteps.
   eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-  rewrite Nat_iter_S. iMod (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
-  rewrite fupd_eq in Hwp.
-  iMod (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
-  iModIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
+  rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iDestruct "Hwp" as (Istate) "(HIstate & HI & Hwp & Hclose)".
+  iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate) I); eauto.
+  iFrame "HI Hw HE Hwp HIstate Hclose". by iApply big_sepL_nil.
 Qed.

program_logic/ectx_lifting.v

@@ -16,15 +16,17 @@ Lemma wp_ectx_bind {E e} K Φ :
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E Φ e1 :
-  (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
-    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-          ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros "H". iApply (wp_lift_step E); try done.
-  iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
-  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
-  iApply ("Hwp" with "* []"); by eauto.
+  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
+  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Φ e1 :
@@ -38,47 +40,48 @@ Proof.
   iIntros (????). iApply "H". eauto.
 Qed.
 
-Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
-  head_reducible e1 σ1 →
-  ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
-  ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_head_step {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
-  iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
+  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
-  head_reducible e1 σ1 →
-  (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-  ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-    Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_atomic_det_step. Qed.
-
-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 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
-  rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iNext; iIntros (v2 σ2 efs) "%".
+  iMod ("H" $! v2 σ2 efs with "[#]") as "(% & $ & $)"=>//; subst.
+  by iApply big_sepL_nil.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.

program_logic/lifting.v

@@ -11,23 +11,15 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step E Φ e1 :
-  (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
-    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-          ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof.
-  iIntros "H". rewrite wp_unfold /wp_pre.
-  destruct (to_val e1) as [v|] eqn:EQe1.
-  - iLeft. iExists v. iSplit. done. iMod "H" as (σ1) "[% _]".
-    by erewrite reducible_not_val in EQe1.
-  - iRight; iSplit; eauto.
-    iIntros (σ1) "Hσ". iMod "H" as (σ1') "(% & >Hσf & H)".
-    iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
-    iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-    iMod (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
-    iApply ("H" with "* []"); eauto.
-Qed.
+Proof. iIntros (?) "H". rewrite wp_unfold /wp_pre; auto. Qed.
 
+(** Derived lifting lemmas. *)
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
@@ -35,41 +27,30 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  { iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
+  { eapply reducible_not_val, (Hsafe inhabitant). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
 
-(** Derived lifting lemmas. *)
-Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
-  reducible e1 σ1 →
-  (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_step {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1).
-  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
-  iExists σ1. iFrame "Hσ"; iSplit; eauto.
-  iNext; iIntros (e2 σ2 efs) "% Hσ".
-  iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
+  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
+  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
-  iMod "Hclose". iApply wp_value; auto using to_of_val. done.
-Qed.
-
-Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
-  reducible e1 σ1 →
-  (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
-                   σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-  ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-    Φ 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.
-  iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
-  edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
+  by iApply wp_value.
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :

program_logic/weakestpre.v

@@ -2,26 +2,14 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-From iris.algebra Require Import auth.
 Import uPred.
 
-Class irisG' (Λstate : Type) (Σ : gFunctors) : Set := IrisG {
+Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
-  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
-  state_name : gname;
+  state_interp : Λstate → iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition ownP `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
-  own state_name (◯ (Excl' σ)).
-Typeclasses Opaque ownP.
-Instance: Params (@ownP) 3.
-
-Definition ownP_auth `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
-  own state_name (● (Excl' (σ:leibnizC Λstate))).
-Typeclasses Opaque ownP_auth.
-Instance: Params (@ownP_auth) 4.
-
 Definition wp_pre `{irisG Λ Σ}
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
@@ -29,9 +17,9 @@ Definition wp_pre `{irisG Λ Σ}
   (∃ v, ⌜to_val e1 = Some v⌝ ∧ |={E}=> Φ v) ∨
   (* step case *)
   (⌜to_val e1 = None⌝ ∧ ∀ σ1,
-     ownP_auth σ1 ={E,∅}=∗ ⌜reducible e1 σ1⌝ ∗
+     state_interp σ1 ={E,∅}=∗ ⌜reducible e1 σ1⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-       ownP_auth σ2 ∗ wp E e2 Φ ∗
+       state_interp σ2 ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
@@ -109,23 +97,6 @@ Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
-(* Physical state *)
-Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
-Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
-Proof. rewrite /ownP; apply _. Qed.
-
-Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ∗ ownP σ2 ⊢ ⌜σ1 = σ2⌝.
-Proof.
-  rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
-  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
-Qed.
-Lemma ownP_update σ1 σ2 : ownP_auth σ1 ∗ ownP σ1 ==∗ ownP_auth σ2 ∗ ownP σ2.
-Proof.
-  rewrite /ownP -!own_op.
-  by apply own_update, auth_update, option_local_update, exclusive_local_update.
-Qed.
-
 (* Weakest pre *)
 Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

tests/barrier_client.v

@@ -25,20 +25,20 @@ Section client.
   Qed.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
-    heap_ctx ∗ recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}.
+    recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}.
   Proof.
-    iIntros "[#Hh Hrecv]". wp_lam. wp_let.
+    iIntros "Hrecv". wp_lam. wp_let.
     wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
     wp_seq. wp_load.
     iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
   Qed.
 
-  Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
+  Lemma client_safe : True ⊢ 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.
+    iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
+    wp_apply (newbarrier_spec N (y_inv 1 y)).
     iIntros (l) "[Hr Hs]". wp_let.
-    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
+    iApply (wp_par (λ _, True%I) (λ _, True%I)). iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
       wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
       iSplitR "Hy"; first by eauto.
@@ -48,9 +48,9 @@ Section client.
       iDestruct (recv_weaken with "[] Hr") as "Hr".
       { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
       iMod (recv_split with "Hr") as "[H1 H2]"; first done.
-      iApply (wp_par (λ _, True%I) (λ _, True%I) with "[- $Hh]").
+      iApply (wp_par (λ _, True%I) (λ _, True%I)).
       iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
-        iApply worker_safe; by iSplit.
+        by iApply worker_safe.
 Qed.
 End client.
 

tests/counter.v

@@ -84,19 +84,19 @@ Definition I (γ : gname) (l : loc) : iProp Σ :=
   (∃ c : nat, l ↦ #c ∗ own γ (Auth c))%I.
 
 Definition C (l : loc) (n : nat) : iProp Σ :=
-  (∃ N γ, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ inv N (I γ l) ∧ own γ (Frag n))%I.
+  (∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
 
 (** The main proofs. *)
 Global Instance C_persistent l n : PersistentP (C l n).
 Proof. apply _. Qed.
 
-Lemma newcounter_spec N :
-  heapN ⊥ N →
-  heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
+Lemma newcounter_spec :
+  {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
 Proof.
-  iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+  iIntros "!# _ /=". 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]".
+  set (N := nroot .@ "C").
   iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
   { iIntros "!>". iExists 0%nat. by iFrame. }
   iModIntro. rewrite /C; eauto 10.
@@ -106,16 +106,17 @@ Lemma incr_spec l n :
   {{ C l n }} incr #l {{ v, ⌜v = #()⌝ ∧ C l (S n) }}.
 Proof.
   iIntros "!# Hl /=". iLöb as "IH". wp_rec.
-  iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
+  iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
   wp_bind (! _)%E; iInv N as (c) "[Hl Hγ]" "Hclose".
   wp_load. iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
   iModIntro. wp_let. wp_op.
   wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
   destruct (decide (c' = c)) as [->|].
-  - iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
-    iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
-    rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
+  - iDestruct (own_valid_2 with "Hγ Hγf") as %?%auth_frag_valid.
+    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
+    { rewrite -auth_frag_op. apply M_update. done. }
+    rewrite (auth_frag_op (S n) (S c)); last omega.
+    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. rewrite {3}/C; eauto 10.
@@ -127,7 +128,7 @@ Qed.
 Lemma read_spec l n :
   {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
 Proof.
-  iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
+  iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
   rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
   iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
   { iApply own_op. by iFrame. }

tests/heap_lang.v

@@ -11,10 +11,10 @@ Section LiftingTests.
 
   Definition heap_e  : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
-  Lemma heap_e_spec E :
-    ↑heapN ⊆ E → heap_ctx ⊢ WP heap_e @ E {{ v, ⌜v = #2⌝ }}.
+
+  Lemma heap_e_spec E : True ⊢ WP heap_e @ E {{ v, ⌜v = #2⌝ }}.
   Proof.
-    iIntros (HN) "#?". rewrite /heap_e.
+    iIntros "". rewrite /heap_e.
     wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
   Qed.
 
@@ -22,10 +22,10 @@ Section LiftingTests.
     let: "x" := ref #1 in
     let: "y" := ref #1 in
     "x" <- !"x" + #1 ;; !"x".
-  Lemma heap_e2_spec E :
-    ↑heapN ⊆ E → heap_ctx ⊢ WP heap_e2 @ E {{ v, ⌜v = #2⌝ }}.
+
+  Lemma heap_e2_spec E : True ⊢ WP heap_e2 @ E {{ v, ⌜v = #2⌝ }}.
   Proof.
-    iIntros (HN) "#?". rewrite /heap_e2.
+    iIntros "". rewrite /heap_e2.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
     wp_load. wp_op. wp_store. wp_load. done.
   Qed.

tests/joining_existentials.v

@@ -66,19 +66,18 @@ Proof.
 Qed.
 
 Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
-  heapN ⊥ N →
-  heap_ctx ∗ P
+  P
   ∗ {{ P }} eM {{ _, ∃ x, Φ x }}
   ∗ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
   ∗ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
   ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
-  iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
+  iIntros "/= (HP & #He & #He1 & #He2)"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
-  wp_apply (newbarrier_spec N (barrier_res γ Φ) with "Hh"); auto.
+  wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
   iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I).
-  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[- $Hh]").
+  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post).
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
   - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
@@ -88,8 +87,7 @@ Proof.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iMod (recv_split with "Hr") as "[H1 H2]"; first done.
-    wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
-                     (λ _, barrier_res γ Ψ2)%I with "[-$Hh]").
+    wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I (λ _, barrier_res γ Ψ2)%I).
     iSplitL "H1"; [|iSplitL "H2"].
     + iApply worker_spec; auto.
     + iApply worker_spec; auto.