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

This turns out to be useful for my borrow-checker proofs, which require the ability to mass-end lifetimes to model loan termination without generating an inordinate number of laters.

This extracts the proof that atomic lifetimes can end from lft_create_strong as a standalone lemma, and then proves a stronger version of that lemma that terminates arbitrarily many atomic lifetimes at the same time (which is allowed because they don't overlap.) In fact, I think this generalises to being allowed to terminate any number of lifetimes at in the same step, but that requires some more set/multiset theory to prove, I think.

To prove this, I require a few data structure lemmas which I am trying to upstream. Two are going into iris!1049 (merged). The gset_to_map mass-update lemma is harder to generalise - I thought about including it upstream, but it's rather specific here and it doesn't seem to have a nice "kernel" to extract out that would keep the proof burden in these changes small.

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).