Change auth_fsa to have an existential quantifier for the update.

This works better with class interference.

heap_lang/heap.v

@@ -77,23 +77,23 @@ Section heap.
     P ⊑ wp E (Alloc e) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros HN Hval Hctx HP.
-    set (LU (l : loc) := local_update_op (A:=heapRA) ({[ l ↦ Excl v ]})).
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) _ (LU := LU)); simpl.
-    { by eauto. } { by eauto. } { by eauto. }
+    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _)); simpl; eauto.
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
     rewrite {1}[(▷ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
     rewrite -wp_alloc_pst; first (apply sep_mono; first done); try done; [].
     apply later_mono, forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
-    rewrite -(exist_intro l) !left_id. rewrite always_and_sep_l -assoc.
+    rewrite -(exist_intro (op {[ l ↦ Excl v ]})).
+    repeat erewrite <-exist_intro by apply _; simpl.
+    rewrite always_and_sep_l -assoc.
     apply const_elim_sep_l=>Hfresh.
     assert (σ !! l = None) as Hfresh_σ.
     { move: Hfresh (Hv 0%nat l). rewrite /from_heap /to_heap lookup_omap.
       rewrite lookup_op !lookup_fmap.
       case _:(σ !! l)=>[v'|]/=; case _:(hf !! l)=>[[?||]|]/=; done. }
     rewrite const_equiv // const_equiv; last first.
-    { move=>n l'. move:(Hv n l') Hfresh.
+    { split; first done. move=>n l'. move:(Hv n l') Hfresh.
       rewrite /from_heap /to_heap !lookup_omap !lookup_op !lookup_fmap !Hfresh_σ /=.
       destruct (decide (l=l')).
       - subst l'. rewrite lookup_singleton !Hfresh_σ.
@@ -116,14 +116,13 @@ Section heap.
   Lemma wp_alloc N E γ e v P Q :
     nclose N ⊆ E →  to_val e = Some v →
     P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (▷ (∀ l, heap_mapsto HeapI γ l v -★ Q (LocV l))) →
+    P ⊑ ▷ (∀ l, heap_mapsto HeapI γ l v -★ Q (LocV l)) →
     P ⊑ wp E (Alloc e) Q.
   Proof.
     intros HN ? Hctx HP. eapply sep_elim_True_r.
-    { eapply (auth_empty γ). }
+    { eapply (auth_empty E γ). }
     rewrite pvs_frame_l. apply wp_strip_pvs.
-    eapply wp_alloc_heap with (σ:=∅); try done; [|].
-    { eauto with I. }
+    eapply wp_alloc_heap with N γ ∅ v; eauto with I.
     rewrite HP comm. apply sep_mono.
     - rewrite /heap_own. f_equiv. apply: map_eq=>l. by rewrite lookup_fmap !lookup_empty.
     - apply later_mono, forall_mono=>l. apply wand_mono; last done. eauto with I.
@@ -137,7 +136,7 @@ Section heap.
     P ⊑ wp E (Load (Loc l)) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros Hl HN Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
+    eapply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id); simpl; eauto.
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
@@ -146,7 +145,7 @@ Section heap.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
-    rewrite -(exist_intro ()) left_id const_equiv // left_id.
+    rewrite left_id const_equiv // left_id.
     by rewrite -later_intro.
   Qed.
 
@@ -168,8 +167,7 @@ Section heap.
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros Hl Hval HN Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _)
-                     (λ _:(), alter (λ _, Excl v) l)); simpl; eauto.
+    eapply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v) l)); simpl; eauto.
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
@@ -178,7 +176,7 @@ Section heap.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
-    rewrite -(exist_intro ()) const_equiv //; last first.
+    rewrite const_equiv //; last first.
     (* TODO I think there are some general fin_map lemmas hiding in here. *)
     { split.
       - exists (Excl v'). by rewrite lookup_fmap Hl.
@@ -222,7 +220,7 @@ Section heap.
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros He1 He2 Hl Hne HN Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), id)); simpl; eauto.
+    eapply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id); simpl; eauto.
     { split_ands; eexists; eauto. }
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
@@ -232,7 +230,7 @@ Section heap.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
-    rewrite -(exist_intro ()) left_id const_equiv // left_id.
+    rewrite left_id const_equiv // left_id.
     by rewrite -later_intro.
   Qed.
 
@@ -255,7 +253,7 @@ Section heap.
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros Hv1 Hv2 Hl HN Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), alter (λ _, Excl v2) l)); simpl; eauto.
+    eapply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v2) l)); simpl; eauto.
     { split_ands; eexists; eauto. }
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
@@ -265,7 +263,7 @@ Section heap.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
-    rewrite -(exist_intro ()) const_equiv //; last first.
+    rewrite const_equiv //; last first.
     (* TODO I think there are some general fin_map lemmas hiding in here. *)
     { split.
       - exists (Excl v1). by rewrite lookup_fmap Hl.

program_logic/auth.v

@@ -11,7 +11,8 @@ Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
 (* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
    constantly valid. *)
 Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
-  (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := (∃ a, (■✓a ∧ own i γ (● a)) ★ φ a)%I.
+    (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+  (∃ a, (■ ✓ a ∧ own i γ (● a)) ★ φ a)%I.
 Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
   (γ : gname) (a : A) : iPropG Λ Σ := own i γ (◯ a).
 Definition auth_ctx {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
@@ -29,6 +30,10 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
+  Lemma auto_own_op γ a b :
+    auth_own AuthI γ (a ⋅ b) ≡ (auth_own AuthI γ a ★ auth_own AuthI γ b)%I.
+  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
+
   Lemma auth_alloc N a :
     ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx AuthI γ N φ ∧ auth_own AuthI γ a).
   Proof.
@@ -45,12 +50,12 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma auth_empty γ E : True ⊑ pvs E E (auth_own AuthI γ ∅).
+  Lemma auth_empty E γ : True ⊑ pvs E E (auth_own AuthI γ ∅).
   Proof. by rewrite own_update_empty /auth_own. Qed.
 
-  Lemma auth_opened E a γ :
+  Lemma auth_opened E γ a :
     (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ a)
-    ⊑ pvs E E (∃ a', ■✓(a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
+    ⊑ pvs E E (∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -59,8 +64,7 @@ Section auth.
     rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
     apply exist_elim=>a'.
     rewrite left_id -(exist_intro a').
-    apply (eq_rewrite b (a ⋅ a')
-              (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
+    apply (eq_rewrite b (a ⋅ a') (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
     { by move=>n ? ? /timeless_iff ->. }
     { by eauto with I. }
     rewrite const_equiv // left_id comm.
@@ -68,7 +72,7 @@ Section auth.
     by rewrite sep_elim_l.
   Qed.
 
-  Lemma auth_closing E `{!LocalUpdate Lv L} a a' γ :
+  Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
     Lv a → ✓ (L a ⋅ a') →
     (▷ φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
     ⊑ pvs E E (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ (L a)).
@@ -80,36 +84,55 @@ Section auth.
     by apply own_update, (auth_local_update_l L).
   Qed.
 
+  Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
+
   (* 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.
-     "I" here is an index type, so that the proof can still have some influence on
-     which concrete action is executed *after* it saw the full, authoritative state. *)
-  Lemma auth_fsa {B I} (fsa : FSA Λ (globalF Σ) B) `{!FrameShiftAssertion fsaV fsa}
-       L {Lv} {LU : ∀ i:I, LocalUpdate (Lv i) (L i)} N E P (Q : B → iPropG Λ Σ) γ a :
+     a restriction. *)
+  Lemma auth_fsa E N P (Q : V → iPropG Λ Σ) γ a :
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (auth_own AuthI γ a ★ (∀ a',
+    P ⊑ (auth_own AuthI γ a ★ ∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
-          fsa (E ∖ nclose N) (λ x,
-            ∃ i, ■ (Lv i a ∧ ✓(L i a⋅a')) ★ ▷ φ (L i a ⋅ a') ★
-            (auth_own AuthI γ (L i a) -★ Q x)))) →
+          fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
+            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+            (auth_own AuthI γ (L a) -★ Q x))) →
     P ⊑ fsa E Q.
   Proof.
     rewrite /auth_ctx=>? HN Hinv Hinner.
     eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P}.
-    apply wand_intro_l.
-    rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
+    apply wand_intro_l. rewrite assoc.
+    rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> x. rewrite sep_exist_l. apply exist_elim=>i.
+    apply (fsa_mono_pvs fsa)=> b.
+    rewrite sep_exist_l; apply exist_elim=> L.
+    rewrite sep_exist_l; apply exist_elim=> Lv.
+    rewrite sep_exist_l; apply exist_elim=> ?.
     rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
     rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.
+    rewrite (auth_closing (E ∖ N)) //; [].
+    rewrite pvs_frame_l. apply pvs_mono.
     by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
   Qed.
+  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Q: V → iPropG Λ Σ) γ a :
+    fsaV →
+    nclose N ⊆ E →
+    P ⊑ auth_ctx AuthI γ N φ →
+    P ⊑ (auth_own AuthI γ a ★ (∀ a',
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          fsa (E ∖ nclose N) (λ x,
+            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+            (auth_own AuthI γ (L a) -★ Q x)))) →
+    P ⊑ fsa E Q.
+  Proof.
+    intros ??? HP. eapply auth_fsa with N γ a; eauto.
+    rewrite HP; apply sep_mono; first done; apply forall_mono=> a'.
+    apply wand_mono; first done. apply (fsa_mono fsa)=> b.
+    rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
+  Qed.
 End auth.