Permission for ending a lifetime. Ending a lifetime takes only one steps, and no longer two.

theories/derived.v

@@ -12,8 +12,8 @@ Notation SeqCtx e2 := (LetCtx BAnon e2).
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 Coercion lit_of_bool : bool >-> base_lit.
 Notation If e0 e1 e2 := (Case e0 [e2;e1]).
-Notation Newlft := (Lit LitUnit) (only parsing).
-Notation Endlft := (Seq Skip (Lit LitUnit)) (only parsing).
+Definition Newlft := Lit LitUnit.
+Definition Endlft := Skip.
 
 Section derived.
 Context `{irisG lrust_lang Σ}.

theories/lifetime.v

@@ -130,7 +130,7 @@ Section lft.
   Qed.
 
   Axiom lft_create :
-    ∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,∅}▷=∗ [†κ]).
+    ∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
 
   Axiom idx_borrow_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,

theories/perm.v

@@ -24,11 +24,15 @@ Section perm.
     from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
-    λ tid, ([†κ] ={lftN}=∗ ▷ ρ tid)%I.
+    λ tid, ([†κ] ={lftN}=∗ ρ tid)%I.
 
   Definition tok (κ : lifetime) (q : Qp) : perm :=
     λ _, q.[κ]%I.
 
+
+  Definition killable (κ : lifetime) : perm :=
+    λ _, (□ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]))%I.
+
   Definition incl (κ κ' : lifetime) : perm :=
     λ _, (κ ⊑ κ')%I.
 
@@ -55,6 +59,8 @@ Notation "κ ∋ ρ" := (extract κ ρ)
 
 Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope.
 
+Notation "† κ" := (killable κ) (format "† κ", at level 75).
+
 Infix "⊑" := incl (at level 60) : perm_scope.
 
 Notation "∃ x .. y , P" :=

theories/perm_incl.v

@@ -211,6 +211,17 @@ Section props.
     (* FIXME : namespaces problem. *)
   Admitted.
 
+  Lemma reborrow_shr_perm_incl κ κ' ν ty :
+    κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
+  Proof.
+    iIntros (tid) "[#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 "Hord Hκ'").
+  Qed.
+
   Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
     borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
   Proof.
@@ -247,24 +258,14 @@ Section props.
     iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
   Qed.
 
-  Lemma reborrow_shr_perm_incl κ κ' ν ty :
-    κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
-  Proof.
-    iIntros (tid) "[#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 "Hord Hκ'").
-  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.
+    iSplitL "Hbor". iApply frac_borrow_incl. done.
+    iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
   Qed.
 
 End props.

theories/typing.v

@@ -132,21 +132,18 @@ Section typing.
     typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
   Proof.
     iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_create as (α) "[?#?]". done.
-    iExists α. iFrame. iApply fupd_mask_mono. done.
-    iMod (borrow_create with "[]") as "[_?]". reflexivity. 2:by iIntros "!>". eauto.
+    iExists α. iFrame. iIntros "!>_!>". done.
   Qed.
 
-  (* TODO : lifetime ending permission. *)
-  (* Lemma typed_endlft κ ρ: *)
-  (*   typed_step (κ ∋ ρ ∗ 1.[κ]) Endlft (λ _, ρ)%P. *)
-  (* Proof. *)
-  (*   iIntros (tid) "!#(_&[Hextr Htok]&$)". wp_bind (#() ;; #())%E. *)
-  (*   iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr". *)
-  (*   iApply (wp_frame_step_l with "[-]"); try done. *)
-  (*   iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq. *)
-  (*   iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done. *)
-  (*   by wp_seq. *)
-  (* Qed. *)
+  Lemma typed_endlft κ ρ:
+    typed_step (κ ∋ ρ ∗ 1.[κ] ∗ †κ) Endlft (λ _, ρ)%P.
+  Proof.
+    iIntros (tid) "!#(_&(Hextr&Htok&Hend)&$)".
+    iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
+    iApply (wp_frame_step_l with "[-]"); try done.
+    iDestruct ("Hend" with "Htok") as "$". by wp_seq.
+    iIntros (v) "[#Hκ _]". by iApply fupd_mask_mono; last iApply "Hextr".
+  Qed.
 
   Lemma typed_alloc ρ (n : nat):
     0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).