From 20cb1c6816812bd2edfe1185d4ed36f703cffd5f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 8 Nov 2016 13:38:42 +0100
Subject: [PATCH] Atomic, strong accessor for borrows. Fracturing and freezing
 do no longer need tokens. lft_incl_borrowing is provable.

---
 theories/lifetime.v  | 57 +++++++++++++++++++++-----------------------
 theories/perm_incl.v | 28 +++++++---------------
 theories/type.v      | 32 ++++++++++++-------------
 theories/typing.v    |  4 ++--
 4 files changed, 52 insertions(+), 69 deletions(-)

diff --git a/theories/lifetime.v b/theories/lifetime.v
index a0c79716..097ceae6 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -136,7 +136,6 @@ Section lft.
     ∀ `(nclose lftN ⊆ E) q κ i P,
       idx_borrow κ i P ⊢ idx_borrow_own 1 i ∗ q.[κ] ={E}=∗ ▷ P ∗
                                  (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
-  (* TODO : Can't we give back ▷ P ∨ [†κ] in all cases?  *)
   Axiom idx_borrow_atomic_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
       idx_borrow κ i P ⊢ idx_borrow_own q i
@@ -155,11 +154,14 @@ Section lft.
     ∀ `(nclose lftN ⊆ E) q κ P,
       &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗
       ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
+  Axiom borrow_acc_atomic_strong :
+    ∀ `(nclose lftN ⊆ E) κ P,
+      &{κ}P ={E,E∖lftN}=∗
+        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E∖lftN,E}=∗ &{κ}Q) ∨
+        [†κ] ∗ ∀ Q, |={E∖lftN,E}=> &{κ}Q.
   Axiom borrow_reborrow' :
     ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
       &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-  (* FIXME : the document says that we need κ tokens here. Why so?
-     Why not κ' tokens also?*)
   Axiom borrow_unnest :
     ∀ `(nclose lftN ⊆ E) κ κ' P, &{κ'}&{κ}P ⊢ |={E}▷=> &{κ ⋅ κ'}P.
 
@@ -226,20 +228,19 @@ Section lft.
     iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>[_$]".
   Qed.
 
-  Lemma borrow_exists {A} `(nclose lftN ⊆ E)
-        κ q (Φ : A → iProp Σ) {_:Inhabited A}:
-    &{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=∗ ∃ x, &{κ}Φ x ∗ q.[κ].
+  Lemma borrow_exists {A} `(nclose lftN ⊆ E) κ (Φ : A → iProp Σ) {_:Inhabited A}:
+    &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Proof.
-    iIntros "Hb Htok".
-    iMod (borrow_acc_strong with "Hb Htok") as "[HΦ Hob]". done.
-    iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hob". iIntros "{$HΦ}!>[_?]". eauto.
+    iIntros "Hb". iMod (borrow_acc_atomic_strong with "Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
+    - iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>[_?]". eauto.
+    - iExists inhabitant. iApply "Hclose".
   Qed.
 
-  Lemma borrow_or `(nclose lftN ⊆ E) κ q P Q:
-    &{κ}(P ∨ Q) ⊢ q.[κ] ={E}=∗ (&{κ}P ∨ &{κ}Q) ∗ q.[κ].
+  Lemma borrow_or `(nclose lftN ⊆ E) κ P Q:
+    &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
   Proof.
-    iIntros "H Htok". rewrite uPred.or_alt.
-    iMod (borrow_exists with "H Htok") as ([]) "[H $]"; auto.
+    iIntros "H". rewrite uPred.or_alt.
+    iMod (borrow_exists with "H") as ([]) "H"; auto.
   Qed.
 
   Lemma borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
@@ -250,11 +251,6 @@ Section lft.
     by iMod ("Hob" with "HP") as "[_$]".
   Qed.
 
-  (* TODO : is this derivable (problem with masks of inheritance)? *)
-  (* Lemma borrow_unnest' `(nclose lftN ⊆ E) κ κ' q P: *)
-  (*   &{κ'}&{κ}P ⊢ q.[κ'] ={E}▷=∗ q.[κ'] ∗ &{κ ⋅ κ'}P. *)
-  (* Proof. *)
-
 End lft.
 
 Typeclasses Opaque borrow.
@@ -420,19 +416,20 @@ Section frac_borrow.
   Proof. solve_proper. Qed.
   Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
 
-  (* FIXME : we shall not use tokens for κ here. *)
-  Lemma borrow_fracture φ `(nclose lftN ⊆ E) q κ:
-    &{κ}(φ 1%Qp) ∗ q.[κ] ={E}=∗ &frac{κ}φ ∗ q.[κ].
+  Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
+    &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
-    iIntros "[Hφ Hκ]". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (borrow_acc_strong with "Hφ Hκ") as "[Hφ Hclose]". done.
-    iMod ("Hclose" with "*[-]") as "[Hφ$]"; last first.
-    { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
-      iApply lft_incl_refl. }
-    iSplitL. by iExists 1%Qp; iFrame; auto.
-    iIntros "!>[H† Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
-    iDestruct "Hκ" as (q'') "[_ Hκ]".
-    iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]".
+    iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+    iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
+      { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
+        iApply lft_incl_refl. }
+      iSplitL. by iExists 1%Qp; iFrame; auto.
+      iIntros "!>[H† Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+      iDestruct "Hκ" as (q'') "[_ Hκ]".
+      iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]".
+    - iMod ("Hclose" with "*") as "Hφ"; last first.
+      iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ"). iApply lft_incl_refl.
   Qed.
 
   Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 2b1dce5a..4ecad12a 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -258,25 +258,13 @@ Section props.
     by iApply (ty_shr_mono with "Hord Hκ'").
   Qed.
 
-  (* TODO *)
-  (* Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ'). *)
-  (* Proof. *)
-  (*   iIntros (tid) "_ Htok". iApply fupd_mask_mono. done. *)
-  (*   iDestruct "Htok" as "[Htok1 Htok2]". *)
-  (*   iMod (borrow_create with "[Htok1]") as "[Hbor Hclose]". reflexivity. *)
-  (*   { iIntros "!>". iExact "Htok1". } *)
-  (*   iMod (borrow_fracture (λ q', (q / 2 * q').[κ'])%I with "[Hbor $Htok2]") *)
-  (*     as "[Hbor Htok]". done. *)
-  (*   { by rewrite Qp_mult_1_r. } *)
-  (*   iIntros "{$Htok}!>". iSplitL "Hbor". *)
-  (*   iApply frac_borrow_incl. done. frac_borrow_incl *)
-
-  (*     iExact "Hclose". iFrame. *)
-
-  (*   iMod (frac_borrow_incl with "[-]"). *)
-  (*   iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#". *)
-  (*   iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'". *)
-  (*   iApply lft_extract_combine. done. by iFrame. *)
-  (* Qed. *)
+  Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
+  Proof.
+    iIntros (tid) "_ Htok". iApply fupd_mask_mono. done.
+    iMod (borrow_create with "[$Htok]") as "[Hbor Hclose]". reflexivity.
+    iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "[Hbor]") as "Hbor". done.
+    { by rewrite Qp_mult_1_r. }
+    iSplitL "Hbor". iApply frac_borrow_incl. done. eauto.
+  Qed.
 
 End props.
diff --git a/theories/type.v b/theories/type.v
index 3b4c221b..be61b1d5 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -66,10 +66,10 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
   intros Σ ??? st E N κ l tid q ??. iIntros "Hmt Htok".
-  iMod (borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
+  iMod (borrow_exists with "Hmt") as (vl) "Hmt". set_solver.
   iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
-  iMod (borrow_persistent with "Hown Htok") as "[Hown Htok]". set_solver.
-  iMod (borrow_fracture with "[Hmt $Htok]") as "[Hfrac $]"; last first.
+  iMod (borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
+  iMod (borrow_fracture with "[Hmt]") as "Hfrac"; last first.
   { iExists vl. by iFrame. }
   done. set_solver.
 Qed.
@@ -114,7 +114,7 @@ Section types.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
-    iMod (borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_exists with "Hb") as (vl) "Hb". set_solver.
     iMod (borrow_split with "Hb") as "[_ Hb]". set_solver.
     iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
   Qed.
@@ -156,15 +156,14 @@ Section types.
   Qed.
   Next Obligation.
     move=> q ty E N κ l tid q' ?? /=. iIntros "Hshr Htok".
-    iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_exists with "Hshr") as (vl) "Hb". set_solver.
     iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
+    iMod (borrow_exists with "Hb2") as (l') "Hb2". set_solver.
     iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
     iMod (borrow_split with "Hb2") as "[_ Hb2]". set_solver.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]") as "[Hbf $]".
-      set_solver.
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver.
     rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
@@ -208,14 +207,13 @@ Section types.
   Qed.
   Next Obligation.
     move=> κ ty E N κ' l tid q' ??/=. iIntros "Hshr Htok".
-    iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_exists with "Hshr") as (vl) "Hb". set_solver.
     iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
+    iMod (borrow_exists with "Hb2") as (l') "Hb2". set_solver.
     iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]")
-      as "[Hbf $]". set_solver.
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver.
     rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
     iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
@@ -437,10 +435,10 @@ Section types.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
-    iMod (borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
+    iMod (borrow_exists with "Hown") as (i) "Hown". set_solver.
     iMod (borrow_split with "Hown") as "[Hmt Hown]". set_solver.
-    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr Htok]"; try done.
-    iMod (borrow_fracture with "[-]") as "[H $]"; last by eauto. set_solver. iFrame.
+    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr $]"; try done.
+    iMod (borrow_fracture with "[-]") as "H"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
     intros n tyl Hn κ κ' tid N l. iIntros "#Hord H".
diff --git a/theories/typing.v b/theories/typing.v
index fa9f0f24..0c4ee46a 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -304,9 +304,9 @@ Section typing.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
-    iMod (borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
+    iMod (borrow_exists with "H↦") as (vl) "Hbor". done.
     iMod (borrow_split with "Hbor") as "[H↦ Hbor]". done.
-    iMod (borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done.
+    iMod (borrow_exists with "Hbor") as (l') "Hbor". done.
     iMod (borrow_split with "Hbor") as "[Heq Hbor]". done.
     iMod (borrow_unnest with "Hbor") as "Hbor". done.
     iMod (borrow_persistent with "Heq Htok") as "[>% Htok]". done. subst.
-- 
GitLab