prove 'strong' allocation of ghost state, with more control over the name that has been picked

algebra/fin_maps.v

@@ -295,16 +295,22 @@ Proof. eauto using map_singleton_updateP_empty. Qed.
 
 Section freshness.
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
-  ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
+Lemma map_updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
+  ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
 Proof.
-  intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))).
-  assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??].
-  { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
-  exists (<[i:=x]>m); split; first by apply HQ, not_elem_of_dom.
+  intros ? HQ mf n Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
+  assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
+  { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. }
+  exists (<[i:=x]>m). split; first by (apply HQ; last done; apply not_elem_of_dom).
   rewrite -map_insert_op_None; last by apply not_elem_of_dom.
   by apply map_insert_validN; [apply cmra_valid_validN|].
 Qed.
+Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
+  ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
+Proof. move=>??. eapply map_updateP_alloc_strong with (I:=∅); by eauto. Qed.
+Lemma map_updateP_alloc_strong' m x (I : gset K) :
+  ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
+Proof. eauto using map_updateP_alloc_strong. Qed.
 Lemma map_updateP_alloc' m x :
   ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
 Proof. eauto using map_updateP_alloc. Qed.

program_logic/auth.v

@@ -82,17 +82,19 @@ 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_fsa {B C} (fsa : FSA Λ (globalF Σ) B) `{!FrameShiftAssertion fsaV fsa}
-       L {Lv} {LU : ∀ c:C, LocalUpdate (Lv c) (L c)} N E P (Q : B → iPropG Λ Σ) γ a :
+     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 :
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
     P ⊑ (auth_own AuthI γ a ★ (∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
-            ∃ c, ■ (Lv c a ∧ ✓(L c a⋅a')) ★ ▷ φ (L c a ⋅ a') ★
-            (auth_own AuthI γ (L c a) -★ Q x)))) →
+            ∃ i, ■ (Lv i a ∧ ✓(L i a⋅a')) ★ ▷ φ (L i a ⋅ a') ★
+            (auth_own AuthI γ (L i a) -★ Q x)))) →
     P ⊑ fsa E Q.
   Proof.
     rewrite /auth_ctx=>? HN Hinv Hinner.
@@ -104,7 +106,7 @@ Section auth.
     (* 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=>c.
+    apply (fsa_mono_pvs fsa)=> x. rewrite sep_exist_l. apply exist_elim=>i.
     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.

program_logic/ghost_ownership.v

@@ -82,14 +82,19 @@ Proof. unfold own; apply _. Qed.
 
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
-Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own i γ a).
+Lemma own_alloc_strong a E (G : gset gname) : ✓ a → True ⊑ pvs E E (∃ γ, ■(γ ∉ G) ∧ own i γ a).
 Proof.
   intros Ha.
-  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, m = to_globalF i γ a) ∧ ownG m)%I).
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF i γ a) ∧ ownG m)%I).
   * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
-      first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
-  * apply exist_elim=>m; apply const_elim_l=>-[γ ->].
-    by rewrite -(exist_intro γ).
+      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha); naive_solver.
+  * apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
+    by rewrite -(exist_intro γ) const_equiv.
+Qed.
+Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own i γ a).
+Proof.
+  intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono.
+  apply exist_mono=>?. eauto with I.
 Qed.
 
 Lemma own_updateP P γ a E :

program_logic/saved_prop.v

@@ -15,6 +15,10 @@ Section saved_prop.
   Implicit Types P Q : iPropG Λ Σ.
   Implicit Types γ : gname.
 
+  Lemma saved_prop_alloc_strong N P (G : gset gname) :
+    True ⊑ pvs N N (∃ γ, ■(γ ∉ G) ∧ saved_prop_own SPI γ P).
+  Proof. by apply own_alloc_strong. Qed.
+
   Lemma saved_prop_alloc N P :
     True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
   Proof. by apply own_alloc. Qed.