make *_ctx more opaque; use another opportunity for sep_split

heap_lang/heap.v

@@ -21,17 +21,22 @@ Definition to_heap : state → heapR := fmap (λ v, Frac 1 (DecAgree v)).
 Definition of_heap : heapR → state :=
   omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
 
-(* heap_mapsto is defined strongly opaquely, to prevent unification from
-matching it against other forms of ownership. *)
-Definition heap_mapsto `{heapG Σ}
-    (l : loc)(q : Qp) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
-Typeclasses Opaque heap_mapsto.
-
-Definition heap_inv `{i : heapG Σ} (h : heapR) : iPropG heap_lang Σ :=
-  ownP (of_heap h).
-Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
-  auth_ctx heap_name N heap_inv.
+Section definitions.
+  Context `{i : heapG Σ}.
+
+  Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
+    auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
+  Definition heap_inv (h : heapR) : iPropG heap_lang Σ :=
+    ownP (of_heap h).
+  Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
+    auth_ctx heap_name N heap_inv.
+
+  Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
+  Proof. solve_proper. Qed.
+  Global Instance heap_ctx_always_stable N : AlwaysStable (heap_ctx N).
+  Proof. apply _. Qed.
+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.
@@ -99,7 +104,7 @@ Section heap.
       apply (auth_alloc (ownP ∘ of_heap) N E (to_heap σ)); last done.
       apply to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
-    rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
+    rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
     rewrite /heap_mapsto /heap_name.
     induction σ as [|l v σ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
@@ -112,10 +117,6 @@ Section heap.
 
   Context `{heapG Σ}.
 
-  (** Propers *)
-  Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
-  Proof. solve_proper. Qed.
-
   (** General properties of mapsto *)
   Lemma heap_mapsto_op_eq l q1 q2 v :
     (l ↦{q1} v ★ l ↦{q2} v)%I ≡ (l ↦{q1+q2} v)%I.

heap_lang/spawn.v

@@ -70,9 +70,8 @@ Proof.
     cancel [l ↦ InjLV #0]%I. apply or_intro_l'. by rewrite const_equiv. }
   rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
   ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
-  rewrite !assoc [(_ ★ (own _ _))%I]comm !assoc [(_ ★ (inv _ _))%I]comm.
-  rewrite !assoc [(_ ★ (_ -★ _))%I]comm. rewrite -!assoc 3!assoc. apply sep_mono.
-  - wp_seq. rewrite -!assoc. eapply wand_apply_l; [done..|].
+  sep_split left: [_ -★ _; inv _ _; own _ _; heap_ctx _]%I.
+  - wp_seq. eapply wand_apply_l; [done..|].
     rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
     solve_sep_entails.
   - wp_focus (f _). rewrite wp_frame_r wp_frame_l.

program_logic/auth.v

@@ -13,17 +13,26 @@ Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
   `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
-Definition auth_own `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
-  own γ (◯ a).
-Typeclasses Opaque auth_own.
+Section definitions.
+  Context `{authG Λ Σ A} (γ : gname).
+  Definition auth_own  (a : A) : iPropG Λ Σ :=
+    own γ (◯ a).
+  Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    (∃ a, own γ (● a) ★ φ a)%I.
+  Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    inv N (auth_inv φ).
 
-Definition auth_inv `{authG Λ Σ A}
-    (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-  (∃ a, own γ (● a) ★ φ a)%I.
-Definition auth_ctx`{authG Λ Σ A}
-    (γ : gname) (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-  inv N (auth_inv γ φ).
+  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
+  Proof. solve_proper. Qed.
+  Global Instance auth_own_proper : Proper ((≡) ==> (≡)) auth_own.
+  Proof. solve_proper. Qed.
+  Global Instance auth_own_timeless a : TimelessP (auth_own a).
+  Proof. apply _. Qed.
+  Global Instance auth_ctx_always_stable N φ : AlwaysStable (auth_ctx N φ).
+  Proof. apply _. Qed.
+End definitions.
 
+Typeclasses Opaque auth_own auth_ctx.
 Instance: Params (@auth_inv) 6.
 Instance: Params (@auth_own) 6.
 Instance: Params (@auth_ctx) 7.
@@ -36,13 +45,6 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
-  Proof. solve_proper. Qed.
-  Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
-  Proof. solve_proper. Qed.
-  Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
-  Proof. rewrite /auth_own. apply _. Qed.
-
   Lemma auth_own_op γ a b :
     auth_own γ (a ⋅ b) ≡ (auth_own γ a ★ auth_own γ b)%I.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.

program_logic/sts.v

@@ -13,21 +13,37 @@ Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
-Definition sts_ownS `{i : stsG Λ Σ sts} (γ : gname)
-    (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
-  own γ (sts_frag S T).
-Definition sts_own `{i : stsG Λ Σ sts} (γ : gname)
-    (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
-  own γ (sts_frag_up s T).
-Typeclasses Opaque sts_own sts_ownS.
-
-Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
-    (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
-  (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
-Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
-    (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
-  inv N (sts_inv γ φ).
-
+Section definitions.
+  Context `{i : stsG Λ Σ sts} (γ : gname).
+  Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
+    own γ (sts_frag S T).
+  Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
+    own γ (sts_frag_up s T).
+  Definition sts_inv (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
+  Definition sts_ctx (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    inv N (sts_inv φ).
+
+  Global Instance sts_inv_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
+  Proof. solve_proper. Qed.
+  Global Instance sts_inv_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡)) sts_inv.
+  Proof. solve_proper. Qed.
+  Global Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (≡)) sts_ownS.
+  Proof. solve_proper. Qed.
+  Global Instance sts_own_proper s : Proper ((≡) ==> (≡)) (sts_own s).
+  Proof. solve_proper. Qed.
+  Global Instance sts_ctx_ne n N :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
+  Proof. solve_proper. Qed.
+  Global Instance sts_ctx_proper N :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx N).
+  Proof. solve_proper. Qed.
+  Global Instance sts_ctx_always_stable N φ : AlwaysStable (sts_ctx N φ).
+  Proof. apply _. Qed.
+End definitions.
+Typeclasses Opaque sts_own sts_ownS sts_ctx.
 Instance: Params (@sts_inv) 5.
 Instance: Params (@sts_ownS) 5.
 Instance: Params (@sts_own) 6.
@@ -42,22 +58,6 @@ Section sts.
   Implicit Types T : sts.tokens sts.
 
   (** Setoids *)
-  Global Instance sts_inv_ne n γ :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
-  Proof. solve_proper. Qed.
-  Global Instance sts_inv_proper γ :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv γ).
-  Proof. solve_proper. Qed.
-  Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ).
-  Proof. solve_proper. Qed.
-  Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_own γ s).
-  Proof. solve_proper. Qed.
-  Global Instance sts_ctx_ne n γ N :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
-  Proof. solve_proper. Qed.
-  Global Instance sts_ctx_proper γ N :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx γ N).
-  Proof. solve_proper. Qed.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)