Creating and faking borrows.

_CoqProject

@@ -5,3 +5,4 @@ theories/lifetime/derived.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/todo.v
+theories/lifetime/borrow.v

iris @ ff96075a

-Subproject commit 020acf846aaf5fa367761cff22e7b74160ddc4b0
+Subproject commit ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b

theories/lifetime/definitions.v

@@ -27,6 +27,9 @@ Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
 
+Instance to_lft_stateR_inj : Inj eq eq to_lft_stateR.
+Proof. by intros [] []. Qed.
+
 Record lft_names := LftNames {
   bor_name : gname;
   cnt_name : gname;
@@ -136,9 +139,9 @@ Section defs.
       lft_inh κ true P)%I.
 
   Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∀ Λ, Λ ∈ κ → A !! Λ = Some true.
+    ∀ Λ:atomic_lft, Λ ∈ κ → A !! Λ = Some true.
   Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∃ Λ, Λ ∈ κ ∧ A !! Λ = Some false.
+    ∃ Λ:atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
 
   Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
     (lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨

theories/lifetime/derived.v

-From lrust.lifetime Require Export primitive todo.
+From lrust.lifetime Require Export primitive borrow todo.
 From iris.proofmode Require Import tactics.
 
 Section derived.
@@ -59,27 +59,6 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
-Proof. (*
-  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
-  - iIntros (q). rewrite -lft_tok_op. iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
-  - iIntros "? !>". iApply lft_dead_or. auto.
-Qed. *) Admitted.
-
-Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
-Proof. by apply lft_le_incl. Qed.
-
-Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
-Proof.
-  rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
-  - iIntros (q) "Hκ".
-    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
-    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
-    iExists q''. iIntros "{$Hκ''} !> Hκ''".
-    iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
-  - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
-Qed.
-
 Lemma bor_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
 Proof.
   iIntros "Hκκ' H". rewrite /bor. iDestruct "H" as (i) "[??]".

theories/lifetime/primitive.v

@@ -178,6 +178,18 @@ Proof.
   simplify_map_eq; simplify_option_eq; eauto.
 Qed.
 
+Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
+  own_alft_auth A ⊢
+    own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
+Proof.
+  iIntros "HA HΛ". iDestruct (own_valid_2 with "HA HΛ")
+    as %[[? [Heq Hle]]%singleton_included _]%auth_valid_discrete_2.
+  simplify_map_eq. destruct (A!!Λ) as [b'|]; last done. inversion Heq. subst x.
+  apply Some_included in Hle. destruct Hle as [->%leibniz_equiv%(inj _)|Hle]. done.
+  apply csum_included in Hle.
+  destruct Hle as [Hle|[(?&?&?&?&?)|(?&?&?&?&?)]], b, b'; try done.
+Qed.
+
 Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
@@ -295,4 +307,27 @@ Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 
 Lemma lft_dead_static : [† static] ⊢ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
+
+Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
+Proof.
+  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+  - iIntros (q). rewrite <-lft_tok_op. iIntros "[H Hf]". iExists q. iFrame.
+    rewrite <-lft_tok_op. by iIntros "!>{$Hf}$".
+  - iIntros "? !>". iApply lft_dead_or. auto.
+Qed.
+
+Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
+Proof. by apply lft_le_incl. Qed.
+
+Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
+Proof.
+  rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
+  - iIntros (q) "Hκ".
+    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
+    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
+    iExists q''. iIntros "{$Hκ''} !> Hκ''".
+    iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
+  - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
+Qed.
+
 End primitive.

theories/lifetime/todo.v

@@ -5,15 +5,6 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 (** Basic borrows  *)
-Lemma bor_create E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-Proof. Admitted.
-Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
-Proof.
-Admitted.
 Lemma bor_sep E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.

theories/tl_borrow.v

@@ -6,21 +6,21 @@ Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
            (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
   (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
 
-Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
-  (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
+Notation "&tl{ κ , tid , N } P" := (tl_borrow κ tid N P)
+  (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
 
 Section tl_borrow.
   Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
           (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _.
+  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
   Global Instance tl_borrow_proper κ :
     Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
   Proof.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
@@ -28,7 +28,7 @@ Section tl_borrow.
 
   Lemma tl_borrow_acc q κ E F :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
-    lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
+    lft_ctx ⊢ &tl{κ,tid,N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
             ▷P ∗ tl_own tid (F ∖ N) ∗
             (▷P -∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
@@ -40,7 +40,7 @@ Section tl_borrow.
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
+  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (idx_borrow_shorten with "Hκκ' H").