From 6d6532db1db3a29055909e2c7ec66f71fecb36ff Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 May 2024 11:05:15 +0200
Subject: [PATCH] some comments on lifetime ending

---
 lifetime/model/creation.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/lifetime/model/creation.v b/lifetime/model/creation.v
index 726fd1ef..71de1bbb 100644
--- a/lifetime/model/creation.v
+++ b/lifetime/model/creation.v
@@ -129,7 +129,9 @@ 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Λ. iIntros "!> HΛ".
+  clear I A HΛ HPx HP.
+  (* From here on, we are proving that an atomic lifetime can be ended. *)
+  iIntros "!> HΛ".
   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.
@@ -138,7 +140,7 @@ Proof.
   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.
+  iDestruct "HΛ" as "#HΛ". iModIntro; iNext. (* This is THE step *)
   pose (K := kill_set I Λ).
   pose (K' := filter (lft_alive_in A) (dom I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom I))) as (K''&HI&HK'').
-- 
GitLab