Expose atomic lifetimes opaquely in the API

This extends the lifetime signature to expose the notion of atomic
lifetimes and how they can embed into normal lifetimes. This allows for
a future lemma where I will state that a particular new lifetime is
atomic, thus allowing for the application of the lifetime-ending lemma
at a later point.

This has been done opaquely rather than exposing directly the definition
of `atomic_lft` to try to keep the API clean.

lifetime/lifetime.v

@@ -34,9 +34,9 @@ Lemma lft_create E :
   lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
-  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "H"=>//;
+  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//;
     [by apply pred_infinite_True|].
-  by auto.
+  by iApply lft_kill_atomic.
 Qed.
 
 (* Deriving this just to prove that it can be derived.

lifetime/lifetime_sig.v

@@ -38,15 +38,22 @@ Module Type lifetime_sig.
   Parameter idx_bor_own : ∀ `{!lftGS Σ userE} (q : frac) (i : bor_idx), iProp Σ.
   Parameter idx_bor : ∀ `{!invGS Σ, !lftGS Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
+  Parameter atomic_lft : Type.
+  Parameter atomic_lft_to_lft : atomic_lft → lft.
+
   (** 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.
+  [positive] to an atomic lifetime. *)
+  Parameter positive_to_atomic_lft : positive → atomic_lft.
+  Notation positive_to_lft p := (atomic_lft_to_lft (positive_to_atomic_lft p)).
 
   (** * Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
       (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
+  Notation "q .[@ Λ ]" := (lft_tok q (atomic_lft_to_lft Λ))
+      (format "q .[@ Λ ]", at level 2, left associativity) : bi_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
+  Notation "[†@ Λ ]" := (lft_dead (atomic_lft_to_lft Λ)) (format "[†@ Λ ]"): bi_scope.
 
   Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
   Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope.
@@ -100,7 +107,11 @@ Module Type lifetime_sig.
     FrameFractionalQp q1 q2 q →
     Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
 
-  Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
+  Global Declare Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
+  Global Declare Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
+
+  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
+  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
 
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
@@ -116,14 +127,16 @@ Module Type lifetime_sig.
      [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 ∪ userE}[userE]▷=∗ [†κ]).
+    ∃ p : positive, let Λ := positive_to_atomic_lft p in ⌜P p⌝ ∗ (1).[@Λ].
   (** Given two lifetimes [κ] and [κ'], find a lower bound on atomic lifetimes [m]
      such that [m ⊓ κ'] is syntactically different from [κ].
      This is useful in conjunction with [lft_create_strong] to generate
      fresh lifetimes when using lifetimes as keys to index into a map. *)
   Parameter lft_fresh : ∀ κ κ', ∃ i : positive,
     ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+  Parameter lft_kill_atomic : ∀ Λ, lft_ctx -∗ □ ((1).[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
+  Parameter lft_kill_atomics : ∀ Λs,
+    lft_ctx -∗ □ (([∗ set] Λ ∈ Λs, (1).[@Λ]) ={↑lftN ∪ userE}[userE]▷=∗ [∗ set] Λ∈Λs, [†@Λ]).
 
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).

lifetime/meta.v

@@ -44,6 +44,7 @@ Section lft_meta.
       as (? [Etok [Hinf ->]]) "Hown".
     iMod (lft_create_strong (.∈ Etok) with "LFT") as (p HEtok) "Hκ"; [done..|].
     iExists (positive_to_lft p). iFrame "Hκ".
+    iDestruct (lft_kill_atomic with "LFT") as "$".
     iMod (own_update with "Hown") as "Hown".
     { eapply (dyn_reservation_map_alloc _ p (to_agree γ)); done. }
     iModIntro. iExists p. eauto.
@@ -55,7 +56,7 @@ Section lft_meta.
     iIntros "Hidx1 Hidx2".
     iDestruct "Hidx1" as (p1) "(% & Hidx1)". subst κ.
     iDestruct "Hidx2" as (p2) "(Hlft & Hidx2)".
-    iDestruct "Hlft" as %<-%(inj positive_to_lft).
+    iDestruct "Hlft" as %<-%(inj atomic_lft_to_lft)%(inj positive_to_atomic_lft).
     iCombine "Hidx1 Hidx2" as "Hidx".
     iDestruct (own_valid with "Hidx") as %Hval.
     rewrite ->(dyn_reservation_map_data_valid (A:=agreeR gnameO)) in Hval.

lifetime/model/creation.v

@@ -121,13 +121,12 @@ Proof.
   - rewrite lookup_union_r !lookup_gset_to_gmap !option_guard_False //= He1 //.
 Qed.
 
-Lemma lft_kill_atomics :
+Lemma lft_kill_atomics (Λs : gset atomic_lft) :
   lft_ctx -∗
-  ∀ (Λs : gset atomic_lft),
-    □(([∗ set] Λ∈Λs, 1.[positive_to_lft Λ]) ={↑lftN ∪ userE}[userE]▷=∗
-      ([∗ set] Λ∈Λs, [†positive_to_lft Λ])).
+    □(([∗ set] Λ∈Λs, 1.[@Λ]) ={↑lftN ∪ userE}[userE]▷=∗
+      ([∗ set] Λ∈Λs, [†@Λ])).
 Proof.
-  assert (userE_lftN_disj:=userE_lftN_disj). iIntros "#LFT" (Λs) "!> HΛs".
+  assert (userE_lftN_disj:=userE_lftN_disj). iIntros "#LFT !> HΛs".
   destruct (decide (Λs = ∅)) as [->|Hne].
   { rewrite !big_sepS_empty.
     iApply fupd_mask_intro; [set_solver|iIntros "$"].
@@ -198,21 +197,19 @@ Proof.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_union_false.
 Qed.
 
-Lemma lft_kill_atomic :
-  lft_ctx -∗
-  ∀ (Λ : atomic_lft), □(1.[positive_to_lft Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†positive_to_lft Λ]).
+Lemma lft_kill_atomic (Λ : atomic_lft) :
+  lft_ctx -∗ □(1.[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
 Proof.
-  iIntros "#LFT" (?).
-  rewrite -(big_sepS_singleton (λ x, 1.[positive_to_lft x])%I)
-          -(big_sepS_singleton (λ x, [†positive_to_lft x])%I).
+  iIntros "#LFT".
+  rewrite -(big_sepS_singleton (λ x, 1.[@x])%I)
+          -(big_sepS_singleton (λ x, [†@x])%I).
   by iApply (lft_kill_atomics with "LFT").
 Qed.
 
 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 ∪ userE}[userE]▷=∗ [†κ]).
+  ∃ p : positive, let Λ := positive_to_atomic_lft p in ⌜P p⌝ ∗ (1).[@Λ].
 Proof.
   assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -230,12 +227,10 @@ Proof.
     - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
   iModIntro; iExists Λ.
   rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
-  clear I A HΛ.
-  iApply (lft_kill_atomic with "LFT").
 Qed.
 
 Lemma lft_fresh κ κ' :
-  ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+  ∃ i : positive, ∀ m : positive, (i < m)%positive → (atomic_lft_to_lft (positive_to_atomic_lft m)) ⊓ κ' ≠ κ.
 Proof.
   unfold meet, lft_intersect.
   destruct (minimal_exists (flip Pos.le) (dom κ)) as (i & Ha).

lifetime/model/definitions.v

@@ -19,7 +19,8 @@ End lft_notation.
 Definition static : lft := (∅ : gmultiset _).
 Global Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
-Definition positive_to_lft (p : positive) : lft := {[+ p +]}.
+Definition positive_to_atomic_lft (p : positive) : atomic_lft := p.
+Definition atomic_lft_to_lft (Λ : atomic_lft) : lft := {[+ Λ +]}.
 
 Inductive bor_state :=
   | Bor_in
@@ -209,7 +210,10 @@ Global Instance bor_params : Params (@bor) 4 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
+Notation "q .[@ Λ ]" := (lft_tok q (atomic_lft_to_lft Λ))
+    (format "q .[@ Λ ]", at level 2, left associativity) : bi_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
+Notation "[†@ Λ ]" := (lft_dead (atomic_lft_to_lft Λ)) (format "[†@ Λ ]"): bi_scope.
 
 Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
 Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope.
@@ -339,10 +343,17 @@ 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.
+Global Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
 Proof.
-  unfold positive_to_lft. intros x y Hxy.
+  unfold atomic_lft_to_lft. intros x y Hxy.
   apply gmultiset_elem_of_singleton. rewrite -Hxy.
   set_solver.
 Qed.
+
+Global Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
+Proof. apply _. Qed.
+
+Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
+Global Definition atomic_lft_countable : Countable atomic_lft := _.
+
 End basic_properties.