diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 804bd1bb2bc2e17b994ab6f8d32c6d418893a7c6..b10c64c85f77d7393b623edbba0a9b4ba62bc7db 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -286,8 +286,12 @@ Lemma map_updateP_alloc' m x :
 Proof. eauto using map_updateP_alloc. Qed.
 End freshness.
 
-(* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
-   then the frame could always own "unit x", and prevent deallocation. *)
+(* Allocation is a local update: Just use composition with a singleton map. *)
+(* Deallocation is *not* a local update. The trouble is that if we
+   own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent
+   deallocation. *)
+
+(* Applying a local update at a position we own is a local update. *)
 Global Instance map_alter_update `{!LocalUpdate Lv L} i :
   LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i).
 Proof.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index be85330e5b742f7d2a70271934def391567bf724..58261a80354ca4bc37e6c72d7b6e1782b01cbc23 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -77,21 +77,21 @@ Section auth.
   (* Notice how the user has to prove that `bâ‹…a'` is valid at all
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
-  Lemma auth_pvs `{!LocalUpdate Lv L} E P Q γ a :
+  Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
+        `{!LocalUpdate Lv L} E P (Q : X → iProp Λ (globalC Σ)) γ a :
     nclose N ⊆ E →
     (auth_ctx γ ★ auth_own γ a ★ (∀ a', ▷φ (a ⋅ a') -★
-          pvs (E ∖ nclose N) (E ∖ nclose N)
-            (■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Q))))
-      ⊑ pvs E E Q.
+        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Q x))))
+      ⊑ FSA E Q.
   Proof.
     rewrite /auth_ctx=>HN.
-    rewrite -[pvs E E _]pvs_open_close; last eassumption.
+    rewrite -inv_fsa; last eassumption.
     apply sep_mono; first done. apply wand_intro_l.
     rewrite associative auth_opened !pvs_frame_r !sep_exist_r.
-    apply pvs_strip_pvs. apply exist_elim=>a'.
+    apply fsa_strip_pvs; first done. apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]commutative.
-    rewrite -[((_ ★ ▷_) ★ _)%I]associative wand_elim_r pvs_frame_l.
-    apply pvs_strip_pvs. rewrite commutative -!associative.
+    rewrite -[((_ ★ ▷_) ★ _)%I]associative wand_elim_r fsa_frame_l.
+    apply fsa_mono_pvs; first done. intros x. rewrite commutative -!associative.
     apply const_elim_sep_l=>-[HL Hv].
     rewrite associative [(_ ★ (_ -★ _))%I]commutative -associative.
     rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 2b24b5284dd4bdaf52f9f61f7b4310ecd9ba9a3e..f5a2f0994777d0cd63dea16464c2218e3e2459bc 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -64,50 +64,39 @@ Proof. rewrite /inv; apply _. Qed.
 Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
 Proof. by rewrite always_always. Qed.
 
-(* There is not really a way to provide versions of pvs_openI and pvs_closeI
-   that work with inv. The issue is that these rules track the exact current
-   mask too precisely. However, we *can* provide abstract rules by
-   performing both the opening and the closing of the invariant in the rule,
-   and then implicitly framing all the unused invariants around the
-   "inner" view shift provided by the client. *)
-
-Lemma pvs_open_close E N P Q :
+(** Invariants can be opened around any frame-shifting assertion. *)
+Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
+      E N P (Q : A → iProp Λ Σ) :
   nclose N ⊆ E →
-  (inv N P ★ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q.
+  (inv N P ★ (▷P -★ FSA (E ∖ nclose N) (λ a, ▷P ★ Q a))) ⊑ FSA E Q.
 Proof.
   move=>HN.
   rewrite /inv sep_exist_r. apply exist_elim=>i.
   rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
-  rewrite -(pvs_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
+  rewrite -(fsa_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
   (* Add this to the local context, so that solve_elem_of finds it. *)
   assert ({[encode i]} ⊆ nclose N) by eauto.
   rewrite (always_sep_dup' (ownI _ _)).
   rewrite {1}pvs_openI !pvs_frame_r.
   apply pvs_mask_frame_mono ; [solve_elem_of..|].
-  rewrite (commutative _ (â–·_)%I) -associative wand_elim_r pvs_frame_l.
-  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  rewrite (commutative _ (â–·_)%I) -associative wand_elim_r fsa_frame_l.
+  apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
   rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
   apply pvs_mask_frame'; solve_elem_of.
 Qed.
 
+(* Derive the concrete forms for pvs and wp, because they are useful. *)
+
+Lemma pvs_open_close E N P Q :
+  nclose N ⊆ E →
+  (inv N P ★ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q.
+Proof. move=>HN. by rewrite (inv_fsa pvs_fsa). Qed.
+
 Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) :
   atomic e → nclose N ⊆ E →
   (inv N P ★ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
 Proof.
-  move=>He HN.
-  rewrite /inv sep_exist_r. apply exist_elim=>i.
-  rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
-  rewrite -(wp_atomic E (E ∖ {[encode i]})) //; last by solve_elem_of+.
-  (* Add this to the local context, so that solve_elem_of finds it. *)
-  assert ({[encode i]} ⊆ nclose N) by eauto.
-  rewrite (always_sep_dup' (ownI _ _)).
-  rewrite {1}pvs_openI !pvs_frame_r.
-  apply pvs_mask_frame_mono; [solve_elem_of..|].
-  rewrite (commutative _ (â–·_)%I) -associative wand_elim_r wp_frame_l.
-  apply wp_mask_frame_mono; [solve_elem_of..|]=>v.
-  rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
-  apply pvs_mask_frame'; solve_elem_of.
-Qed.
+  move=>He HN. by rewrite (inv_fsa (wp_fsa e _)). Qed.
 
 Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 6184683cf218223c82f694d6e16d85c638c1911a..663090b3b7ed8b374cf34c2b59408e69b7f45cf0 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -179,3 +179,61 @@ Proof.
 Qed.
 
 End pvs.
+
+(** * Frame Shift Assertions. *)
+Section fsa.
+Context {Λ : language} {Σ : iFunctor} {A : Type}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : A → iProp Λ Σ.
+
+(* Yes, the name is horrible...
+   Frame Shift Assertions take a mask and a predicate over some type (that's
+   their "postcondition"). They support weakening the mask, framing resources
+   into the postcondition, and composition witn mask-changing view shifts. *)
+Class FrameShiftAssertion (FSA : coPset → (A → iProp Λ Σ) → iProp Λ Σ) := {
+  fsa_mask_frame_mono E1 E2 Q Q' :> E1 ⊆ E2 →
+                                 (∀ a, Q a ⊑ Q' a) → FSA E1 Q ⊑ FSA E2 Q';
+  fsa_trans3 E1 E2 Q : E2 ⊆ E1 →
+                     pvs E1 E2 (FSA E2 (λ a, pvs E2 E1 (Q a))) ⊑ FSA E1 Q;
+  fsa_frame_r E P Q : (FSA E Q ★ P) ⊑ FSA E (λ a, Q a ★ P)
+}.
+
+Context FSA `{FrameShiftAssertion FSA}.
+Lemma fsa_mono E Q Q' : (∀ a, Q a ⊑ Q' a) → FSA E Q ⊑ FSA E Q'.
+Proof. apply fsa_mask_frame_mono; auto. Qed.
+Lemma fsa_mask_weaken E1 E2 Q : E1 ⊆ E2 → FSA E1 Q ⊑ FSA E2 Q.
+Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
+Lemma fsa_frame_l E P Q :
+  (P ★ FSA E Q) ⊑ FSA E (λ a, P ★ Q a).
+Proof.
+  rewrite commutative fsa_frame_r. apply fsa_mono=>a.
+  by rewrite commutative.
+Qed.
+Lemma fsa_strip_pvs E P Q : P ⊑ FSA E Q → pvs E E P ⊑ FSA E Q.
+Proof.
+  move=>->. rewrite -{2}fsa_trans3; last reflexivity.
+  apply pvs_mono, fsa_mono=>a. apply pvs_intro.  
+Qed.
+Lemma fsa_mono_pvs E Q Q' : (∀ a, Q a ⊑ pvs E E (Q' a)) → FSA E Q ⊑ FSA E Q'.
+Proof.
+  move=>HQ. rewrite -[FSA E Q']fsa_trans3; last reflexivity.
+  rewrite -pvs_intro. by apply fsa_mono.
+Qed.
+
+End fsa.
+
+(** View shifts are a FSA. *)
+Section pvs_fsa.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : () → iProp Λ Σ.
+
+Global Instance pvs_fsa : FrameShiftAssertion (λ E Q, pvs E E (Q ())).
+Proof.
+  split; intros.
+  - apply pvs_mask_frame_mono; auto.
+  - apply pvs_trans3; auto.
+  - apply pvs_frame_r; auto.
+Qed.
+
+End pvs_fsa.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 1f03296f35da1c82a894ca553c699f54724911a4..6ceabb531197317345df46764d73c776c21dbf4c 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -194,7 +194,7 @@ Proof.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.
 
-(* Derived rules *)
+(** * Derived rules *)
 Opaque uPred_holds.
 Import uPred.
 Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2.
@@ -227,4 +227,16 @@ Proof.
 Qed.
 Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.
 Proof. by rewrite commutative wp_impl_l. Qed.
+Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
+Proof. auto using wp_mask_frame_mono. Qed.
+
+(** * Weakest-pre is a FSA. *)
+Global Instance wp_fsa e : atomic e → FrameShiftAssertion (λ E Q, wp E e Q).
+Proof.
+  split; intros.
+  - apply wp_mask_frame_mono; auto.
+  - apply wp_atomic; auto.
+  - apply wp_frame_r; auto.
+Qed.
+
 End wp.