Borrowing and reborrowing. Also removed some old stuff.

theories/typing/perm.v

@@ -48,9 +48,6 @@ Section perm.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
-
-  Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx -∗ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ extract κ ρ1 tid.
 End perm.
 
 Delimit Scope perm_scope with P.
@@ -177,21 +174,4 @@ Section perm_incl.
 
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
   Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
-
-  Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
-    borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
-  Proof.
-    iIntros (Hbor tid) "LFT (Hρ&Hθ&Hρ1)". iMod (Hbor with "LFT Hρ Hρ1") as "[$ Hρ1]".
-    iIntros "!>#H†". iSplitL "Hθ". by iApply "Hθ". by iApply "Hρ1".
-  Qed.
-
-  Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
-  Proof.
-    iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
-    iMod (bor_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
-    { by rewrite Qp_mult_1_r. }
-    iSplitL "Hbor". iApply (frac_bor_lft_incl with "LFT Hbor").
-    iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
-  Qed.
 End perm_incl.

theories/typing/shr_bor.v

@@ -49,14 +49,18 @@ Section typing.
     iIntros "!>/=". eauto.
   Qed.
 
-  Lemma rebor_shr_perm_incl κ κ' ν ty :
-    κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
+  Lemma tctx_reborrow_shr E L p ty κ κ' :
+    incl E L κ' κ →
+    tctx_incl E L [TCtx_holds p (&shr{κ}ty)]
+                  [TCtx_holds p (&shr{κ'}ty); TCtx_guarded p κ (&shr{κ}ty)].
   Proof.
-    iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
-    destruct (eval_expr ν) as [[[|l|]|]|];
-      try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
-    iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
-    iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hord Hκ'").
+    iIntros (Hκκ' tid) "#LFT #HE #HL H". iDestruct (Hκκ' with "HE HL") as "Hκκ'".
+    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iDestruct "H" as (v) "[% #H]". iDestruct "H" as (l) "[EQ Hshr]".
+    iDestruct "EQ" as %[=->]. simpl. iModIntro. iSplit.
+    - iExists _. iSplit. done. iExists _. iSplit. done.
+      by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
+    - iExists _. iSplit. done. iIntros "_". eauto.
   Qed.
 
   Lemma consumes_copy_shr_bor ty κ κ' q:

theories/typing/type_context.v

@@ -28,7 +28,7 @@ Section type_context.
     match x with
     | TCtx_holds p ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
     | TCtx_guarded p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
-        ∀ E, ⌜↑lftN ⊆ E⌝ -∗ [†κ] ={E}=∗ ▷ ty.(ty_own) tid [v]
+                             ([†κ] ={⊤}=∗ ▷ ty.(ty_own) tid [v])
     end%I.
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
@@ -83,25 +83,25 @@ Section type_context.
     | _ => x
     end.
 
-  Lemma deguard_tctx_elt_interp tid E κ x :
-    ↑lftN ⊆ E → [†κ] -∗ tctx_elt_interp tid x ={E}=∗
+  Lemma deguard_tctx_elt_interp tid κ x :
+    [†κ] -∗ tctx_elt_interp tid x ={⊤}=∗
         ▷ tctx_elt_interp tid (deguard_tctx_elt κ x).
   Proof.
-    iIntros (?) "H† H". destruct x as [|? κ' ?]; simpl. by auto.
+    iIntros "H† H". destruct x as [|? κ' ?]; simpl. by auto.
     destruct (decide (κ = κ')) as [->|]; simpl; last by auto.
     iDestruct "H" as (v) "[% H]". iExists v. iSplitR. by auto.
-    by iApply ("H" with "[] H†").
+    by iApply ("H" with "H†").
   Qed.
 
   Definition deguard_tctx κ (T : tctx) : tctx :=
     deguard_tctx_elt κ <$> T.
 
-  Lemma deguard_tctx_interp tid E κ T :
-    ↑lftN ⊆ E → [†κ] -∗ tctx_interp tid T ={E}=∗
+  Lemma deguard_tctx_interp tid κ T :
+    [†κ] -∗ tctx_interp tid T ={⊤}=∗
         ▷ tctx_interp tid (deguard_tctx κ T).
   Proof.
-    iIntros (?) "#H† H". rewrite /tctx_interp big_sepL_fmap.
-    iApply (big_opL_forall (λ P Q, [†κ] -∗ P ={E}=∗ ▷ Q) with "H† H").
+    iIntros "#H† H". rewrite /tctx_interp big_sepL_fmap.
+    iApply (big_opL_forall (λ P Q, [†κ] -∗ P ={⊤}=∗ ▷ Q) with "H† H").
     { by iIntros (?) "_ $". }
     { iIntros (?? A ?? B) "#H† [H1 H2]". iSplitL "H1".
         by iApply (A with "H†"). by iApply (B with "H†"). }

theories/typing/uniq_bor.v

 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts typing own.
+From lrust.typing Require Import perm lft_contexts type_context typing own.
 
 Section uniq_bor.
   Context `{typeG Σ}.
@@ -102,33 +103,34 @@ Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma own_uniq_borrowing ν q ty κ :
-    borrowing κ ⊤ (ν ◁ own q ty) (ν ◁ &uniq{κ} ty).
+  Lemma tctx_borrow E L p n ty κ :
+    tctx_incl E L [TCtx_holds p (own n ty)]
+                  [TCtx_holds p (&uniq{κ}ty); TCtx_guarded p κ (own n ty)].
   Proof.
-    iIntros (tid) "#LFT _ Hown". unfold has_type.
-    destruct (eval_expr ν) as [[[|l|]|]|];
-      try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
-    iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
-    iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done. iSplitL "Hbor".
-    { iExists _, _. erewrite <-uPred.iff_refl. auto. }
-    iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
+    iIntros (tid) "#LFT _ _ H".
+    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
+    iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+    iModIntro. iSplitL "Hbor".
+    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
+    - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
+        by iMod ("Hext" with "H†") as "$".
   Qed.
 
-  Lemma rebor_uniq_borrowing κ κ' ν ty :
-    borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
+  Lemma tctx_reborrow_uniq E L p ty κ κ' :
+    incl E L κ' κ →
+    tctx_incl E L [TCtx_holds p (&uniq{κ}ty)]
+                  [TCtx_holds p (&uniq{κ'}ty); TCtx_guarded p κ (&uniq{κ}ty)].
   Proof.
-    iIntros (tid) "#LFT #Hord H". unfold has_type.
-    destruct (eval_expr ν) as [[[|l|]|]|];
-      try by (iDestruct "H" as "[]" || iDestruct "H" as (l P) "[[% _] _]").
-    iDestruct "H" as (l' P) "[[EQ #HPiff] H]". iDestruct "EQ" as %[=]. subst l'.
-    iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (bor_iff with "LFT [] H") as "H". done. by eauto.
-    iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
-    iModIntro. iSplitL "H".
-    - iExists _, _. erewrite <-uPred.iff_refl. auto.
-    - iIntros "H†". iExists _, _. iMod ("Hextr" with "H†") as "$".
-      iSplitR. done. iIntros "!>!#". apply uPred.iff_refl.
+    iIntros (Hκκ' tid) "#LFT #HE #HL H". iDestruct (Hκκ' with "HE HL") as "Hκκ'".
+    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
+    iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
+    iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
+    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
+    - iExists _. iSplit. done. iIntros "#H†".
+      iMod ("Hext" with ">[]") as "Hb". by iApply (lft_incl_dead with "Hκκ' H†").
+      iExists _, _. erewrite <-uPred.iff_refl. eauto.
   Qed.
 
   Lemma consumes_copy_uniq_bor `(!Copy ty) κ κ' q: