Merge branch 'atomic_lft_promotion' into 'master'

Expose atomic lifetimes in the API, end many in a single step

See merge request !37

lifetime/lifetime.v

@@ -29,14 +29,31 @@ Section derived.
 Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
+Lemma lft_kill_atomic (Λ : atomic_lft) :
+  lft_ctx -∗ □(1.[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
+Proof.
+  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_atomic E :
+  ↑lftN ⊆ E →
+  lft_ctx ={E}=∗ ∃ Λ, 1.[@Λ].
+Proof.
+  iIntros (?) "#LFT".
+  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//.
+  by apply pred_infinite_True.
+Qed.
+
 Lemma lft_create E :
   ↑lftN ⊆ E →
   lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
-  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "H"=>//;
-    [by apply pred_infinite_True|].
-  by auto.
+  iMod (lft_create_atomic with "LFT") as "[% $]"=>//.
+  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,15 @@ 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_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

@@ -107,41 +107,46 @@ 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_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]▷=∗ [†κ]).
+Lemma lupd_gmap_mass_insert (Λs : gset atomic_lft) (m : alftUR) (x y : lft_stateR) `{!Exclusive x} : ✓ y →
+  (m, gset_to_gmap x Λs) ~l~> (gset_to_gmap y Λs ∪ m, gset_to_gmap y Λs).
 Proof.
-  assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
-  destruct (HP (dom 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Λ. }
-  iMod ("Hclose" with "[HA HI Hinv]") as "_".
-  { iNext. rewrite /lfts_inv /own_alft_auth.
-    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
-    iApply (@big_sepS_impl with "[$Hinv]").
-    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. iSplit; first done. iFrame "HΛ".
-  clear I A HΛ HPx HP.
-  (* From here on, we are proving that an atomic lifetime can be ended. *)
-  iIntros "!> HΛ".
+  intros ?.
+  apply gmap_local_update.
+  intros Λ; destruct (m !! Λ) as [|] eqn:He1, (decide (Λ ∈ Λs)) as [|].
+  - rewrite lookup_union_l' !lookup_gset_to_gmap !option_guard_True // He1.
+    by apply option_local_update, exclusive_local_update.
+  - rewrite lookup_union_r !lookup_gset_to_gmap !option_guard_False //= He1 //.
+  - rewrite lookup_union_l' !lookup_gset_to_gmap !option_guard_True // He1.
+    by apply alloc_option_local_update.
+  - rewrite lookup_union_r !lookup_gset_to_gmap !option_guard_False //= He1 //.
+Qed.
+
+Lemma lft_kill_atomics (Λs : gset atomic_lft) :
+  lft_ctx -∗
+    □(([∗ set] Λ∈Λs, 1.[@Λ]) ={↑lftN ∪ userE}[userE]▷=∗
+      ([∗ set] Λ∈Λs, [†@Λ])).
+Proof.
+  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 "$"].
+  }
   iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)); [solve_ndisj..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite /lft_tok big_sepMS_singleton.
-  iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
-  iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
-  { by eapply auth_update, singleton_local_update,
-      (exclusive_local_update _ (Cinr ())). }
-  iDestruct "HΛ" as "#HΛ". iModIntro; iNext. (* This is THE step *)
-  pose (K := kill_set I Λ).
+  rewrite /lft_tok.
+  iAssert (own alft_name (◯ gset_to_gmap (Cinl 1%Qp) Λs))%I with "[HΛs]" as "HΛs".
+  { setoid_rewrite big_sepMS_singleton.
+    iDestruct (big_opS_own _ _ _ Hne with "HΛs") as "HΛs".
+    rewrite -(big_opS_gset_to_gmap Λs (Cinl 1%Qp)) big_opS_auth_frag //. }
+  iDestruct (own_valid_2 with "HA HΛs")
+    as %[[s Hs] _]%auth_both_valid_discrete.
+  iMod (own_update_2 with "HA HΛs") as "[HA HΛs]".
+  { eapply auth_update.
+    by apply (lupd_gmap_mass_insert Λs _ _ (Cinr ())). }
+  rewrite -[in own alft_name (◯ _)]big_opS_gset_to_gmap big_opS_auth_frag big_opS_own //.
+  iDestruct "HΛs" as "#HΛs".
+  iModIntro; iNext.
+  pose (K := set_bind (λ Λ, kill_set I Λ) Λs).
   pose (K' := filter (lft_alive_in A) (dom I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom I))) as (K''&HI&HK'').
   { set_solver+. }
@@ -153,40 +158,70 @@ Proof.
     by iApply lft_inv_alive_in. }
   iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
-    iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
+    iIntros (κ [Λ [HΛ [? _]%elem_of_kill_set]]%elem_of_set_bind) "$".
+    rewrite /lft_dead.
+    by iDestruct (big_sepS_elem_of with "HΛs") as "$". }
   iApply fupd_trans.
   iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)); first solve_ndisj.
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { done. }
-  { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
+  { intros κ κ' [Λ [? [??]%elem_of_kill_set]]%elem_of_set_bind ??.
+    apply elem_of_set_bind; exists Λ; split; [assumption|].
+    apply elem_of_kill_set.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ ???. rewrite elem_of_difference elem_of_filter elem_of_dom. auto. }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
-  { iModIntro. rewrite /lft_dead. iExists Λ.
+  { iModIntro.
+    iApply (big_sepS_impl with "HΛs").
+    iIntros "!>" (Λ) "??".
+    rewrite /lft_dead. iExists Λ.
     rewrite gmultiset_elem_of_singleton. auto. }
-  iNext. iExists (<[Λ:=false]>A), I.
-  rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
+  iNext. iExists ((gset_to_gmap false Λs ∪ A) : gmap atomic_lft bool), I.
+  rewrite /own_alft_auth /to_alftUR map_fmap_union fmap_gset_to_gmap.
+  iFrame "HA HI".
   rewrite HI !big_sepS_union //.
   iSplitL "HinvK HinvD"; first iSplitL "HinvK".
   - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
-    iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
-    iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
+    iIntros (κ [Λ [? [? _]%elem_of_kill_set]]%elem_of_set_bind) "Hdead". rewrite /lft_inv.
+    iRight. iFrame. iPureIntro.  by eapply lft_dead_in_union_false'.
   - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!>".
     iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
     rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
-    apply lft_alive_in_insert_false; last done.
-    move: HκK. rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)). set_solver +HκI.
+    apply lft_alive_in_union_false; [|done].
+    set_solver.
   - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!>".
     rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
     + iLeft. iFrame. iPureIntro.
-      apply lft_alive_in_insert_false; last done. intros ?.
-      assert (κ ∈ K) by (rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)) HI elem_of_union; auto).
-      eapply HK'', Hκ. rewrite elem_of_union. auto.
-    + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
+      apply lft_alive_in_union_false; last done. intros ??.
+      set_solver.
+    + iRight. iFrame. iPureIntro. by apply lft_dead_in_union_false.
+Qed.
+
+Lemma lft_create_strong P E :
+  pred_infinite P → ↑lftN ⊆ E →
+  lft_ctx ={E}=∗
+  ∃ 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".
+  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
+  destruct (HP (dom 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Λ. }
+  iMod ("Hclose" with "[HA HI Hinv]") as "_".
+  { iNext. rewrite /lfts_inv /own_alft_auth.
+    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
+    iApply (@big_sepS_impl with "[$Hinv]").
+    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. iSplit; first done. iFrame "HΛ".
 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.

lifetime/model/primitive.v

@@ -221,6 +221,14 @@ Proof.
   intros HΛ Halive Λ' HΛ'.
   rewrite lookup_insert_ne; last (by intros ->); auto.
 Qed.
+Lemma lft_alive_in_union_false A κ Λs b :
+  (∀ Λ, Λ ∈ Λs → Λ ∉ κ) → lft_alive_in A κ → lft_alive_in (gset_to_gmap b Λs ∪ A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  rewrite lookup_union_r; [by apply Halive|].
+  apply lookup_gset_to_gmap_None.
+  by intros ?%HΛ.
+Qed.
 
 Lemma lft_dead_in_insert A κ Λ b :
   A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
@@ -236,8 +244,28 @@ Proof.
   - exists Λ. by rewrite lookup_insert.
   - exists Λ'. by rewrite lookup_insert_ne.
 Qed.
+Lemma lft_dead_in_union_false A κ Λs :
+  lft_dead_in A κ → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros (Λ&?&HΛ). destruct (decide (Λ ∈ Λs)) as [|].
+  - exists Λ. rewrite lookup_union_l'.
+    + by rewrite lookup_gset_to_gmap_Some.
+    + exists false; by rewrite lookup_gset_to_gmap_Some.
+  - exists Λ. rewrite lookup_union_r.
+    + done.
+    + by rewrite lookup_gset_to_gmap_None.
+Qed.
 Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
 Proof. exists Λ. by rewrite lookup_insert. Qed.
+Lemma lft_dead_in_union_false' A κ Λs Λ :
+  Λ ∈ κ → Λ ∈ Λs → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros HΛκ HΛ.
+  exists Λ; split; [done|].
+  rewrite lookup_union_l'.
+  - by apply lookup_gset_to_gmap_Some.
+  - exists false; by apply lookup_gset_to_gmap_Some.
+Qed.
 Lemma lft_dead_in_alive_in_union A κ κ' :
   lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
 Proof.