From 518bc894876e2348bc289cb317f394f4e2b285fa Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 21 May 2021 13:00:30 +0200
Subject: [PATCH] Document the subjective modality in the consequence VS of
 bor_acc_strong.

---
 theories/lifetime/lifetime_sig.v | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index f0b98b8a..04373ae2 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -157,7 +157,21 @@ Module Type lifetime_sig.
         (∀ Vtok', ⌜Vtok ⊑ Vtok'⌝ -∗ ▷ P (Vtok' ⊔ V)
                   ={E}=∗ idx_bor_own i (Vtok' ⊔ V) ∗ q.[κ] Vtok').
   (* We have to expose κ' here as without [lftN] in the mask of the Q-to-P view
-     shift, we cannot turn [†κ'] into [†κ]. *)
+     shift, we cannot turn [†κ'] into [†κ].
+
+     The reason why [†κ'] is under a subjective modality is because of what
+     happens when a non-atomic lifetime dies (a non-atomic lifetime is the
+     intersection of other lifetimes). Indeed, a non-atomic lifetime can die
+     "several times", once for each component, and each of these death can
+     occur at non-comparable views. The only relevant view that we would pass
+     to the consequence view-shift is the view used for the inheritance of
+     the borrow, but that view is not necessarily well-defined since the
+     borrow can be the result of a merging of other borrows.
+
+     TODO : It would be great to get rid of that modality, because this should
+     allow giving a model to GhostCell under weak memory. See the comment in
+     ghostcell.v in the master SC branch.
+ *)
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     ⎡lft_ctx⎤ -∗ &{κ}P -∗ q.[κ] ={E}=∗ ∃ κ', (κ ⊑ κ') ∗ ▷ P ∗
       ∀ Q, ▷ (▷ Q -∗ <subj>[†κ'] ={userE}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'}Q ∗ q.[κ].
-- 
GitLab