From dc36799f2ad1ab25a7b01da3736ef7fc679b321c Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 22 Dec 2016 10:03:56 +0100
Subject: [PATCH] show starting and ending a lifetime

also strengthen local lifetime context to not add laters in front of the inherited ownership
---
 theories/typing/borrow.v       | 20 --------------------
 theories/typing/lft_contexts.v |  2 +-
 theories/typing/programs.v     | 29 +++++++++++++++++++++++++++++
 theories/typing/shr_bor.v      |  2 +-
 theories/typing/type_context.v | 20 ++++++++++----------
 theories/typing/typing.v       | 17 -----------------
 theories/typing/uniq_bor.v     | 21 ++++++++++++++++++++-
 7 files changed, 61 insertions(+), 50 deletions(-)

diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 02ef4c9f..f835c2d5 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -25,26 +25,6 @@ Section borrow.
     - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
         by iMod ("Hext" with "H†") as "$".
   Qed.
-  
-  Lemma tctx_reborrow_uniq E L p ty κ κ' :
-    lctx_lft_incl E L κ' κ →
-    tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
-                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
-  Proof.
-    iIntros (Hκκ' tid ??) "#LFT HE HL H".
-    iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
-    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 typed_deref_uniq_bor_own ty ν κ κ' q q':
     typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 1ece0d6f..47bdfeee 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -74,7 +74,7 @@ Section lft_contexts.
 
   Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
     let κ' := foldr (∪) static (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[x.1] ={⊤,⊤∖↑lftN}▷=∗ [†x.1]))%I.
+    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={⊤,⊤∖↑lftN}▷=∗ [†κ0]))%I.
   Global Instance llctx_elt_interp_fractional x :
     Fractional (llctx_elt_interp x).
   Proof.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 35d93b86..acd7ed90 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -83,6 +83,35 @@ Section typing_rules.
     iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
     iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
   Qed.
+
+  Lemma typed_newlft E L C T κs e :
+    Closed [] e →
+    (∀ κ, typed_body E ((κ, κs) :: L) C T e) →
+    typed_body E L C T (Newlft ;; e).
+  Proof.
+    iIntros (Hc He tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
+    set (κ' := foldr (∪) static κs). wp_seq.
+    iApply (He (κ' ∪ Λ) with "HEAP LFT Htl HE [HL Htk] HC HT").
+    rewrite /llctx_interp big_sepL_cons. iFrame "HL".
+    iExists Λ. iSplit; first done. iFrame. done.
+  Qed.
+
+  (* TODO: It should be possible to show this while taking only one step.
+     Right now, we could take two. *)
+  Lemma typed_endlft E L C T κ κs e :
+    Closed [] e →
+    typed_body E L C (unblock_tctx κ T) e →
+    typed_body E ((κ, κs) :: L) C T (Endlft ;; e).
+  Proof.
+    iIntros (Hc He tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
+    iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
+    iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
+    iApply (wp_fupd_step with "Hend"); try done. wp_seq.
+    iIntros "!> #Hdead !>". wp_seq. iApply (He with "HEAP LFT Htl HE HL HC >").
+    iApply (unblock_tctx_interp with "[] HT").
+    simpl in *. subst κ. rewrite -lft_dead_or. auto.
+  Qed.
   
   Lemma type_assign E L ty1 ty ty1' p1 p2 :
     typed_write E L ty1 ty ty1' →
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 1e63f7aa..eb7f2f4c 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -59,7 +59,7 @@ Section typing.
     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 "_". iIntros "!> !>".
+    - iExists _. iSplit. done. iIntros "_". iIntros "!>".
       iExists _. auto.
   Qed.
 
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 0bac33bd..9fd47d5e 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -52,7 +52,7 @@ Section type_context.
     match x with
     | TCtx_hasty p ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
     | TCtx_blocked p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
-                             ([†κ] ={⊤}=∗ ▷ ty.(ty_own) tid [v])
+                             ([†κ] ={⊤}=∗ ty.(ty_own) tid [v])
     end%I.
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
@@ -184,16 +184,16 @@ Section type_context.
     iApply ("Ho" with "*"). done.
   Qed.
 
-  Definition deguard_tctx_elt κ x :=
+  Definition unblock_tctx_elt κ x :=
     match x with
     | TCtx_blocked p κ' ty =>
       if decide (κ = κ') then TCtx_hasty p ty else x
     | _ => x
     end.
 
-  Lemma deguard_tctx_elt_interp tid κ x :
+  Lemma unblock_tctx_elt_interp tid κ x :
     [†κ] -∗ tctx_elt_interp tid x ={⊤}=∗
-        ▷ tctx_elt_interp tid (deguard_tctx_elt κ x).
+        tctx_elt_interp tid (unblock_tctx_elt κ x).
   Proof.
     iIntros "H† H". destruct x as [|? κ' ?]; simpl. by auto.
     destruct (decide (κ = κ')) as [->|]; simpl; last by auto.
@@ -201,18 +201,18 @@ Section type_context.
     by iApply ("H" with "H†").
   Qed.
 
-  Definition deguard_tctx κ (T : tctx) : tctx :=
-    deguard_tctx_elt κ <$> T.
+  Definition unblock_tctx κ (T : tctx) : tctx :=
+    unblock_tctx_elt κ <$> T.
 
-  Lemma deguard_tctx_interp tid κ T :
+  Lemma unblock_tctx_interp tid κ T :
     [†κ] -∗ tctx_interp tid T ={⊤}=∗
-        ▷ tctx_interp tid (deguard_tctx κ T).
+        tctx_interp tid (unblock_tctx κ T).
   Proof.
     iIntros "#H† H". rewrite /tctx_interp big_sepL_fmap.
-    iApply (big_opL_forall (λ P Q, [†κ] -∗ P ={⊤}=∗ ▷ Q) with "H† H").
+    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†"). }
-    move=>/= _ ? _. by apply deguard_tctx_elt_interp.
+    move=>/= _ ? _. by apply unblock_tctx_elt_interp.
   Qed.
 End type_context.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 27feaf7d..0aadf6c9 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -22,23 +22,6 @@ Section typing.
   Definition typed_program (ρ : perm) e :=
     ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e {{ _, False }}.
 
-  Lemma typed_newlft ρ:
-    typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
-  Proof.
-    iIntros (tid) "!#(_&#LFT&_&$)". wp_value.
-    iMod (lft_create with "LFT") as (α) "[?#?]". done.
-    iExists α. iFrame. iIntros "!>_!>". done.
-  Qed.
-
-  Lemma typed_endlft κ ρ:
-    typed_step (κ ∋ ρ ∗ 1.[κ] ∗ †κ) Endlft (λ _, ρ)%P.
-  Proof.
-    rewrite /killable /extract. iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
-    iDestruct ("Hend" with "Htok") as "Hend".
-    iApply (wp_fupd_step with "Hend"); try done. wp_seq.
-    iIntros "!>H†". by iApply fupd_mask_mono; last iApply "Hextr".
-  Qed.
-
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, lftE ∪ ↑lrustN ⊆ E →
       lft_ctx -∗ ρ1 ν tid -∗ na_own tid ⊤ -∗
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 49a0718c..39f5e10b 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -132,7 +132,7 @@ Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma tctx_incl_share E L p κ ty :
+  Lemma tctx_share E L p κ ty :
     lctx_lft_alive E L κ → tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)] [TCtx_hasty p (&shr{κ}ty)].
   Proof.
     iIntros (Hκ ???) "#LFT HE HL Huniq".
@@ -145,6 +145,25 @@ Section typing.
     iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
     iIntros "!>/=". eauto.
   Qed.
+  
+  Lemma tctx_reborrow_uniq E L p ty κ κ' :
+    lctx_lft_incl E L κ' κ →
+    tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
+                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
+  Proof.
+    iIntros (Hκκ' tid ??) "#LFT HE HL H".
+    iDestruct (elctx_interp_persist with "HE") as "#HE'".
+    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
+    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.
 
   (* Old typing *)
   
-- 
GitLab