Introduce the notion of "Frame Shift Assertions", and use to prove the rules...

Introduce the notion of "Frame Shift Assertions", and use to prove the rules about inv and auth at once for pvs and wp

Yeah, the name is horrible... but on the plus side, I think it should be possible to show that atomic triples and atomic shifts are also frame shift assertions, and then we get all this stuff for them for free.

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.

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.

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.

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.

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.