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

CHANGELOG.md

@@ -10,8 +10,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   backwards compatibility and will be removed in a future version of Iris.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
-  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
-  is proven in the logic.
+  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre is
+  proven in the logic. [#] The old ownership of the entire physical state is
+  replaced by a user-selected predicate over physical state that is maintained
+  by weakestpre.
 * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.

_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

algebra/auth.v

@@ -275,7 +275,7 @@ Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
-  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
+  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
 Qed.
 Instance auth_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).

algebra/cmra.v

@@ -1250,11 +1250,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.
 
 Instance optionURF_contractive F :

algebra/gmap.v

@@ -475,11 +475,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
 Qed.
 Instance gmapCF_contractive K `{Countable K} F :
   cFunctorContractive F → cFunctorContractive (gmapCF K F).
@@ -496,11 +496,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).

algebra/list.v

@@ -108,11 +108,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply cFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance listCF_contractive F :
@@ -452,11 +452,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply urFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply urFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
 Qed.
 
 Instance listURF_contractive F :

algebra/ofe.v

@@ -820,11 +820,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance optionCF_contractive F :

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.