Merge branch 'state_inv' into 'master'

State invariants in WP and the dead of heap_ctx.

This merge request changes the WP construction so that it takes _state interpretation_ as its parameter (part of the `irisG` type class), instead of building in the authoritative ownership of the entire state. When instantiating WP with a concrete language, one can choose the state interpretation. For example, for `heap_lang` we directly use `auth (gmap loc (frac * dec_agree val))`, and avoid the indirection through an invariant managing ownership of the entire state.

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

See merge request !25

_CoqProject

@@ -92,13 +92,13 @@ program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
+program_logic/gen_heap.v
+program_logic/ownp.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
-heap_lang/lifting.v
-heap_lang/derived.v
+heap_lang/rules.v
 heap_lang/notation.v
-heap_lang/heap.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v

base_logic/lib/cancelable_invariants.v

@@ -37,11 +37,14 @@ Section proofs.
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. done. Qed.
 
-  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed.
+  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp.
+  Proof. apply (own_valid_2 γ q1 q2). Qed.
 
-  Lemma cinv_own_1_l γ q : cinv_own γ 1 ∗ cinv_own γ q ⊢ False.
-  Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.
+  Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
+  Qed.
 
   Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
   Proof.
@@ -54,7 +57,7 @@ Section proofs.
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
-    iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
+    iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
   Qed.
 
   Lemma cinv_open E N γ p P :
@@ -62,8 +65,8 @@ Section proofs.
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
-    iInv N as "[$|>Hγ']" "Hclose".
+    iInv N as "[$ | >Hγ']" "Hclose".
     - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
-    - iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
+    - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
   Qed.
 End proofs.

heap_lang/adequacy.v

-From iris.program_logic Require Export weakestpre adequacy.
-From iris.heap_lang Require Export heap.
+From iris.program_logic Require Export weakestpre adequacy gen_heap.
+From iris.heap_lang Require Export rules.
 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 :> gen_heapPreG loc val Σ
 }.
 
-Definition heapΣ : gFunctors :=
-  #[irisΣ state; authΣ heapUR].
+Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?]%subG_inv. split; apply _. Qed.
+Proof. intros [? ?]%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_gen_heap σ)) as (γ) "Hh".
+  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+  iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+  set (Hheap := GenHeapG loc val Σ _ _ _ _ γ).
+  iApply (Hwp (HeapG _ _ _)).
 Qed.

heap_lang/derived.v

-From iris.heap_lang Require Export lifting.
-Import uPred.
-
-(** Define some derived forms, and derived lemmas about them. *)
-Notation Lam x e := (Rec BAnon x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV x e := (RecV BAnon x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
-
-Section derived.
-Context `{irisG heap_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E x elam e1 e2 Φ :
-  e1 = Lam x elam →
-  is_Some (to_val e2) →
-  Closed (x :b: []) elam →
-  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
-
-Lemma wp_let E x e1 e2 Φ :
-  is_Some (to_val e1) → Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. by apply wp_lam. Qed.
-
-Lemma wp_seq E e1 e2 Φ :
-  is_Some (to_val e1) → Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. intros ??. by rewrite -wp_let. Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
-
-Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
-  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
-
-Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
-  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-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))) →
-  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
-Qed.
-
-Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
-  P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
-Qed.
-
-Lemma wp_eq E e1 e2 v1 v2 P Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (v1 ≠ v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
-  P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (v1 = v2)); by eauto.
-Qed.
-End derived.

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.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)).
-
-(** The CMRA we need. *)
-Class heapG Σ := HeapG {
-  heapG_iris_inG :> irisG heap_lang Σ;
-  heap_inG :> authG Σ heapUR;
-  heap_name : gname
-}.
-
-Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
-
-Section definitions.
-  Context `{heapG Σ}.
-
-  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    auth_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.
-
-Notation "l ↦{ q } v" := (heap_mapsto l q v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
-
-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.
-
-Section heap.
-  Context {Σ : gFunctors}.
-  Implicit Types P Q : iProp Σ.
-  Implicit Types Φ : val → iProp Σ.
-  Implicit Types σ : state.
-  Implicit Types h g : heapUR.
-
-  (** Conversion to heaps and back *)
-  Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
-  Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
-  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
-  Lemma heap_singleton_included σ l q v :
-    {[l := (q, DecAgree v)]} ≼ to_heap σ → σ !! l = Some v.
-  Proof.
-    rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
-    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.
-
-  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.
-  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⌝.
-  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.
-  Qed.
-
-  Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
-  Proof.
-    intros p q. iSplit.
-    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
-    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
-      iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
-  Qed.
-  Global Instance heap_ex_mapsto_as_fractional l q :
-    AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
-  Proof. done. Qed.
-
-  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 [??].
-  Qed.
-  Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof.
-    iIntros "[H1 H2]". iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->.
-    iApply (heap_mapsto_valid l _ v2). by iFrame.
-  Qed.
-
-  (** 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 }}}.
-  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. }
-    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 }}}.
-  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Φ".
-  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 }}}.
-  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Φ".
-  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
-    {{{ 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Φ".
-  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
-    {{{ 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Φ".
-  Qed.
-End heap.

heap_lang/lang.v

@@ -402,3 +402,13 @@ Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
+
+(** Define some derived forms *)
+Notation Lam x e := (Rec BAnon x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Notation Seq e1 e2 := (Let BAnon e1 e2).
+Notation LamV x e := (RecV BAnon x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).

heap_lang/lib/assert.v

@@ -9,7 +9,7 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
-  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
+  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.

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.
@@ -73,11 +73,11 @@ Proof. solve_proper. Qed.
 (** Helper lemmas *)
 Lemma ress_split i i1 i2 Q R1 R2 P I :
   i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  saved_prop_own i Q ∗ saved_prop_own i1 R1 ∗ saved_prop_own i2 R2 ∗
-    (Q -∗ R1 ∗ R2) ∗ ress P I
-  ⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}).
+  saved_prop_own i Q -∗ saved_prop_own i1 R1 -∗ saved_prop_own i2 R2 -∗
+  (Q -∗ R1 ∗ R2) -∗ ress P I -∗
+  ress P ({[i1;i2]} ∪ I ∖ {[i]}).
 Proof.
-  iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
+  iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
   iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
   iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
   - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
@@ -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]".
@@ -176,7 +175,7 @@ Proof.
                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
   { iSplit; first by eauto using split_step.
     rewrite {2}/barrier_inv /=. iNext. iFrame "Hl".
-    iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
+    by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
     ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
@@ -191,8 +190,7 @@ Qed.
 
 Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
 Proof.
-  rewrite /recv.
-  iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
+  rewrite /recv. iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
   iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
   iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
 Qed.

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).
+    (∀ 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

 From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
@@ -24,18 +25,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 +45,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 +69,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 +96,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 +107,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 +122,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 +143,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 +155,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

-From iris.heap_lang Require Import heap notation.
+From iris.heap_lang Require Export rules notation.
+From iris.base_logic.lib Require Export invariants.
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operations -- *)
@@ -14,11 +15,10 @@ Structure lock Σ `{!heapG Σ} := Lock {
   is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
   is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
   locked_timeless γ : TimelessP (locked γ);
-  locked_exclusive γ : locked γ ∗ locked γ ⊢ False;
+  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 }} ∗
-   ▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
-  ⊢ WP par e {{ Φ }}.
+  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 }} ∗
-   ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
-  ⊢ WP e1 ||| e2 {{ Φ }}.
+  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.
-  iSplitL "H1"; by wp_let.
+  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done.
+  by wp_let. by wp_let. auto.
 Qed.
 End proof.

heap_lang/lib/spawn.v

 From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
@@ -32,8 +33,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 +47,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 +64,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|].
@@ -73,7 +72,7 @@ Proof.
   - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
       iModIntro. wp_match. by iApply "HΦ".
-    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
+    + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.
 

heap_lang/lib/spin_lock.v

@@ -26,12 +26,12 @@ 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 ()).
 
-  Lemma locked_exclusive (γ : gname) : locked γ ∗ locked γ ⊢ False.
-  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
 
   Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
   Proof. solve_proper. Qed.
@@ -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,13 +46,11 @@ 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.
+       ⌜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) ∧
+       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R) ∗
        own γ (◯ (∅, GSet {[ x ]})))%I.
 
   Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
@@ -67,17 +65,16 @@ Section proof.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γ : gname) : (locked γ ∗ locked γ ⊢ False)%I.
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
-    iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2".
-    iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
+    iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
+    iDestruct (own_valid_2 with "H1 H2") as %[[] _].
   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/notation.v

-From iris.heap_lang Require Export derived.
-Export heap_lang.
+From iris.program_logic Require Import language.
+From iris.heap_lang Require Export lang tactics.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
@@ -91,15 +91,15 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL #()).
-Notation SOME x := (InjR x).
+Notation NONE := (InjL #()) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
 
-Notation NONEV := (InjLV #()).
-Notation SOMEV x := (InjRV x).
+Notation NONEV := (InjLV #()) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
 
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
-  (e0, e1, x, e2 at level 200) : expr_scope.
+  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.

heap_lang/proofmode.v

 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
-From iris.heap_lang Require Export wp_tactics heap.
+From iris.heap_lang Require Export wp_tactics rules.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
@@ -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 "↦ ?"

heap_lang/lifting.v → heap_lang/rules.v

-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre gen_heap.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
@@ -6,6 +6,25 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
 Import uPred.
 
+Class heapG Σ := HeapG {
+  heapG_invG : invG Σ;
+  heapG_gen_heapG :> gen_heapG loc val Σ
+}.
+
+Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
+  iris_invG := heapG_invG;
+  state_interp := gen_heap_ctx
+}.
+
+(** Override the notations so that scopes and coercions work out *)
+Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
+Notation "l ↦ v" :=
+  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
+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.
+
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
 simplifies hypothesis related to conversions from and to values, and finite map
@@ -15,6 +34,8 @@ Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : _ = of_val ?v |- _ =>
+     is_var v; destruct v; first[discriminate H|injection H as H]
   | H : head_step ?e _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
@@ -28,8 +49,8 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Section lifting.
-Context `{irisG heap_lang Σ}.
+Section rules.
+Context `{heapG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
@@ -45,52 +66,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 +81,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 +91,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 +101,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 +109,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 +125,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 +134,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 +143,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 +152,125 @@ 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 *)
+Lemma wp_alloc E e v :
+  to_val e = Some v →
+  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+Proof.
+  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 (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_load E l q v :
+  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  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 →
+  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
+Proof.
+  iIntros (<-%of_to_val Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. 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 →
+  {{{ ▷ 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 ? Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  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 →
+  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ RET LitV (LitBool true); l ↦ v2 }}}.
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
+
+(** Proof rules for derived constructs *)
+Lemma wp_lam E x elam e1 e2 Φ :
+  e1 = Lam x elam →
+  is_Some (to_val e2) →
+  Closed (x :b: []) elam →
+  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
+
+Lemma wp_let E x e1 e2 Φ :
+  is_Some (to_val e1) → Closed (x :b: []) e2 →
+  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
+Proof. by apply wp_lam. Qed.
+
+Lemma wp_seq E e1 e2 Φ :
+  is_Some (to_val e1) → Closed [] e2 →
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
+Proof. intros ??. by rewrite -wp_let. Qed.
+
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
+Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
+
+Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
+  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
+
+Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
+  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+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))) →
+  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
+Qed.
+
+Lemma wp_lt E (n1 n2 : Z) P Φ :
+  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
+Qed.
+
+Lemma wp_eq E e1 e2 v1 v2 P Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (v1 ≠ v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (v1 = v2)); by eauto.
+Qed.
+End rules.

heap_lang/wp_tactics.v

-From iris.heap_lang Require Export tactics derived.
+From iris.heap_lang Require Export tactics rules.
 Import uPred.
 
 (** wp-specific helper tactics *)

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,57 @@ 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 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⌝.
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ 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 "[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σ [$Hw $HE]") as "> (_ & _ & $)"; auto.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
-  (∀ `{irisG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+  (∀ `{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 φ Φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ1 ∗ WP e {{ Φ }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
   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 & Hwp & Hclose)".
+  iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto.
+  iFrame "Hw HE Hwp HIstate Hclose". by iApply big_sepL_nil.
 Qed.