add derived 'meta' mechanism to lifetime logic: associate a lifetime with metadata (via a gname)

_CoqProject

@@ -18,6 +18,7 @@ theories/lifetime/lifetime.v
 theories/lifetime/at_borrow.v
 theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
+theories/lifetime/meta.v
 theories/lang/adequacy.v
 theories/lang/heap.v
 theories/lang/lang.v

theories/lifetime/lifetime.v

@@ -29,6 +29,16 @@ Section derived.
 Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma lft_create E :
+  ↑lftN ⊆ E →
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+Proof.
+  iIntros (?) "#LFT".
+  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "H"=>//;
+    [by apply pred_infinite_True|].
+  by auto.
+Qed.
+
 (* Deriving this just to prove that it can be derived.
 (It is in the signature only for code sharing reasons.) *)
 Lemma bor_shorten_ κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.

theories/lifetime/lifetime_sig.v

@@ -38,6 +38,11 @@ Module Type lifetime_sig.
   Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
   Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
+  (** Our lifetime creation lemma offers allocating a lifetime that is defined
+  by a [positive] in some given infinite set. This operation converts the
+  [positive] to a lifetime. *)
+  Parameter positive_to_lft : positive → lft.
+
   (** * Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
       (format "q .[ κ ]", at level 0) : bi_scope.
@@ -88,6 +93,8 @@ Module Type lifetime_sig.
   Global Declare Instance idx_bor_own_as_fractional i q :
     AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 
+  Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
+
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
   Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
@@ -96,8 +103,13 @@ Module Type lifetime_sig.
   Parameter lft_dead_static : [† static] -∗ False.
   Parameter lft_intersect_static_cancel_l : ∀ κ κ', κ ⊓ κ' = static → κ = static.
 
-  Parameter lft_create : ∀ E, ↑lftN ⊆ E →
-    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+  (** Create a lifetime in some given set of names [P]. This lemma statement
+     requires exposing [atomic_lft], because [P] restricted to the image of
+     [atomic_to_lft] might well not be infinite. *)
+  Parameter lft_create_strong : ∀ P E, pred_infinite P → ↑lftN ⊆ E →
+    lft_ctx ={E}=∗
+    ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
+         (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,

theories/lifetime/meta.v

+From iris.algebra Require Import dyn_reservation_map agree.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Export lifetime.
+Set Default Proof Using "Type".
+
+(** This module provides support for attaching metadata (specifically, a
+[gname]) to a lifetime (as is required for types using branding). *)
+
+Class lft_metaG Σ := LftMetaG {
+  lft_meta_inG :> inG Σ (dyn_reservation_mapR (agreeR gnameO));
+}.
+Definition lft_metaΣ : gFunctors :=
+  #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
+Instance subG_lft_meta Σ :
+  subG (lft_metaΣ) Σ → lft_metaG Σ.
+Proof. solve_inG. Qed.
+
+(** We need some global ghost state, but we do not actually care about the name:
+we always use a frame-preserving update starting from ε to obtain the ownership
+we need. In other words, we use [own_unit] instead of [own_alloc]. As a result
+we can just hard-code an arbitrary name here. *)
+Local Definition lft_meta_gname : gname := 42%positive.
+
+Definition lft_meta `{!lftG Σ, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
+  ∃ p : positive, ⌜κ = positive_to_lft p⌝ ∗
+    own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
+
+Section lft_meta.
+  Context `{!invG Σ, !lftG Σ, lft_metaG Σ}.
+
+  Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
+  Proof. apply _. Qed.
+  Global Instance lft_meta_persistent κ γ : Persistent (lft_meta κ γ).
+  Proof. apply _. Qed.
+
+  Lemma lft_create_meta {E : coPset} (γ : gname) :
+    ↑lftN ⊆ E →
+    lft_ctx ={E}=∗
+    ∃ κ, lft_meta κ γ ∗ (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+  Proof.
+    iIntros (HE) "#LFT".
+    iMod (own_unit (dyn_reservation_mapUR (agreeR gnameO)) lft_meta_gname) as "Hown".
+    iMod (own_updateP _ _ _ dyn_reservation_map_reserve' with "Hown")
+      as (? [Etok [Hinf ->]]) "Hown".
+    iMod (lft_create_strong (.∈ Etok) with "LFT") as (p HEtok) "Hκ"; [done..|].
+    iExists (positive_to_lft p). iFrame "Hκ".
+    iMod (own_update with "Hown") as "Hown".
+    { eapply (dyn_reservation_map_alloc _ p (to_agree γ)); done. }
+    iModIntro. iExists p. eauto.
+  Qed.
+
+  Lemma lft_meta_agree (κ : lft) (γ1 γ2 : gname) :
+    lft_meta κ γ1 -∗ lft_meta κ γ2 -∗ ⌜γ1 = γ2⌝.
+  Proof.
+    iIntros "Hidx1 Hidx2".
+    iDestruct "Hidx1" as (p1) "(% & Hidx1)". subst κ.
+    iDestruct "Hidx2" as (p2) "(Hlft & Hidx2)".
+    iDestruct "Hlft" as %<-%(inj positive_to_lft).
+    iCombine "Hidx1 Hidx2" as "Hidx".
+    iDestruct (own_valid with "Hidx") as %Hval.
+    rewrite ->(dyn_reservation_map_data_valid (A:=agreeR gnameO)) in Hval.
+    apply to_agree_op_inv_L in Hval.
+    done.
+  Qed.
+End lft_meta.
+
+Typeclasses Opaque lft_meta.

theories/lifetime/model/creation.v

@@ -108,13 +108,16 @@ Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
 Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
 Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
 
-Lemma lft_create E :
-  ↑lftN ⊆ E →
-  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+Lemma lft_create_strong P E :
+  pred_infinite P → ↑lftN ⊆ E →
+  lft_ctx ={E}=∗
+  ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
+       (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
 Proof.
-  iIntros (?) "#LFT".
+  iIntros (HP ?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  destruct (exist_fresh (dom (gset atomic_lft) A)) as [Λ HΛ%not_elem_of_dom].
+  rewrite ->pred_infinite_set in HP.
+  destruct (HP (dom (gset _) A)) as [Λ [HPx HΛ%not_elem_of_dom]].
   iMod (own_update with "HA") as "[HA HΛ]".
   { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
     by rewrite lookup_fmap HΛ. }
@@ -125,8 +128,8 @@ Proof.
     iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
     - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
     - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
-  iModIntro; iExists {[ Λ ]}.
-  rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
+  iModIntro; iExists Λ.
+  rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
   clear I A HΛ. iIntros "!# HΛ".
   iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
   { (* FIXME solve_ndisj should really handle this... *)

theories/lifetime/model/definitions.v

@@ -19,6 +19,8 @@ End lft_notation.
 Definition static : lft := (∅ : gmultiset _).
 Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
+Definition positive_to_lft (p : positive) : lft := {[ p ]}.
+
 Inductive bor_state :=
   | Bor_in
   | Bor_open (q : frac)
@@ -335,4 +337,11 @@ Proof. rewrite /idx_bor_own. apply _. Qed.
 
 Global Instance lft_ctx_persistent : Persistent lft_ctx.
 Proof. rewrite /lft_ctx. apply _. Qed.
+
+Global Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
+Proof.
+  unfold positive_to_lft. intros x y Hxy.
+  apply (elem_of_singleton_1 (C := lft)). rewrite -Hxy.
+  set_solver.
+Qed.
 End basic_properties.