Document the subjective modality in the consequence VS of bor_acc_strong.

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.[κ].