more flexible masks for sts_alloc and heap_alloc

heap_lang/heap.v

@@ -62,13 +62,14 @@ Section heap.
   Qed.
 
   (** Allocation *)
-  Lemma heap_alloc N σ :
-    authG heap_lang Σ heapRA →
-    ownP σ ⊑ pvs N N (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto).
+  Lemma heap_alloc E N σ :
+    authG heap_lang Σ heapRA → nclose N ⊆ E →
+    ownP σ ⊑ pvs E E (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto).
   Proof.
-    rewrite -{1}(from_to_heap σ). etransitivity.
+    intros. rewrite -{1}(from_to_heap σ). etransitivity.
     { rewrite [ownP _]later_intro.
-      apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid. }
+      apply (auth_alloc (ownP ∘ of_heap) E N (to_heap σ)); last done.
+      apply to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
     induction σ as [|l v σ Hl IH] using map_ind.

program_logic/auth.v

@@ -41,12 +41,13 @@ Section auth.
   Lemma auto_own_valid γ a : auth_own γ a ⊑ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
-  Lemma auth_alloc N a :
-    ✓ a → ▷ φ a ⊑ pvs N N (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
+  Lemma auth_alloc E N a :
+    ✓ a → nclose N ⊆ E →
+    ▷ φ a ⊑ pvs E E (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
-    intros Ha. eapply sep_elim_True_r.
+    intros Ha HN. eapply sep_elim_True_r.
     { by eapply (own_alloc (Auth (Excl a) a) N). }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
+    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.

program_logic/sts.v

@@ -63,13 +63,15 @@ Section sts.
     sts_own γ s T ⊑ pvs E E (sts_ownS γ S T).
   Proof. intros. by apply own_update, sts_update_frag_up. Qed.
 
-  Lemma sts_alloc N s :
-    ▷ φ s ⊑ pvs N N (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
+  Lemma sts_alloc E N s :
+    nclose N ⊆ E →
+    ▷ φ s ⊑ pvs E E (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
-    eapply sep_elim_True_r.
+    intros HN. eapply sep_elim_True_r.
     { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N).
       apply sts_auth_valid; solve_elem_of. }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
+    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
+    apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.