From 97946ce6540eb6a38ab40520cde92ea03c3789e8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Mar 2021 12:06:26 +0100
Subject: [PATCH] add GhostCell proof by Joshua Yanovski

---
 _CoqProject                     |   1 +
 theories/typing/lib/ghostcell.v | 709 ++++++++++++++++++++++++++++++++
 2 files changed, 710 insertions(+)
 create mode 100644 theories/typing/lib/ghostcell.v

diff --git a/_CoqProject b/_CoqProject
index b4ce7fe5..2580fe31 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,6 +70,7 @@ theories/typing/lib/arc.v
 theories/typing/lib/swap.v
 theories/typing/lib/diverging_static.v
 theories/typing/lib/brandedvec.v
+theories/typing/lib/ghostcell.v
 theories/typing/lib/mutex/mutex.v
 theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell.v
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
new file mode 100644
index 00000000..778e0c3d
--- /dev/null
+++ b/theories/typing/lib/ghostcell.v
@@ -0,0 +1,709 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import csum frac excl agree coPset.
+From iris.bi Require Import lib.fractional.
+From lrust.lang Require Import proofmode notation.
+From lrust.lifetime Require Import meta.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Definition ghostcellN := lrustN .@ "ghostcell".
+Definition ghosttokenN := lrustN .@ "ghosttoken".
+
+(* States:
+   Not borrowed, borrowed.
+
+   Shared states for all borrowed entities:
+     Not shared,
+     ((lifetime at which shared), borrow fraction).
+
+   "Is borrowed" should agree.
+*)
+
+Definition ghosttoken_stR :=
+  (csumR (exclR unitO) ((prodR (agreeR lftO) fracR))).
+
+Class ghostcellG Σ := GhostcellG {
+  ghostcell_inG :> inG Σ (ghosttoken_stR);
+  ghostcell_gsingletonG :> lft_metaG Σ;
+}.
+
+Definition ghostcellΣ : gFunctors
+  := #[GFunctor ghosttoken_stR ; lft_metaΣ].
+
+Instance subG_ghostcellΣ {Σ} : subG ghostcellΣ Σ → ghostcellG Σ.
+Proof. solve_inG. Qed.
+
+(* There are two possible states:
+   - None: The GhostToken is currently not used or used in some
+     GhostCell::borrow_mut, to get mutable access.
+   - Some: The GhostToken is currently used in many GhostCell::get, to get
+     shared access. *)
+Definition ghosttoken_st := option (lft * frac).
+
+Definition ghosttoken_st_to_R (st : ghosttoken_st) : ghosttoken_stR :=
+  (match st with
+        | None => Cinl (Excl ())
+        | Some p => Cinr ((to_agree p.1, p.2))
+        end).
+
+Section ghostcell.
+  Context `{!typeG Σ, !ghostcellG Σ}.
+  Implicit Types (α β: lft) (γ: gname) (q: Qp) (ty: type) (l: loc).
+
+  Local Instance ghosttoken_fractional γ κ' :
+    Fractional (λ q, own γ (ghosttoken_st_to_R (Some (κ',q))))%I.
+  Proof.
+    rewrite /Fractional=>q1 q2.
+    rewrite -own_op /ghosttoken_st_to_R /=. f_equiv.
+    rewrite -Cinr_op. f_equiv.
+    rewrite -pair_op. f_equiv.
+    rewrite agree_idemp. done.
+  Qed.
+
+  Program Definition ghosttoken α :=
+    tc_opaque
+    {| ty_size        := 0;
+       ty_own tid vl  :=
+         (⌜vl = []⌝ ∗ ∃ γ, lft_meta α γ ∗
+          own γ (ghosttoken_st_to_R None))%I;
+       ty_shr κ tid l :=
+         (∃ γ, lft_meta α γ ∗
+           ∃ κ', κ ⊑ κ' ∗
+             &frac{κ'}(λ q, own γ (ghosttoken_st_to_R (Some (κ',q)))))%I;
+    |}.
+  Next Obligation. by iIntros (??[|]) "[% ?]". Qed.
+  Next Obligation.
+    iIntros (α E κ l tid q ?) "#LFT Hvl Htok".
+    iMod (bor_exists with "LFT Hvl") as (vl) "Hvl"; first done.
+    iMod (bor_sep with "LFT Hvl") as "[Hvl Hset]"; first done.
+    iMod (bor_sep with "LFT Hset") as "[Hp Hset]"; first done.
+    iMod (bor_exists with "LFT Hset") as (γ) "Hset"; first done.
+    iMod (bor_sep with "LFT Hset") as "[Hidx Hset]"; first done.
+    iMod (bor_persistent with "LFT Hidx Htok") as "[>#Hidx Htok]"; first solve_ndisj.
+    iMod (bor_acc_strong with "LFT Hset Htok") as (κ') "(#Hκ & >Hset & Hclose)"; first done.
+    rewrite bi.sep_exist_r. iExists γ. iFrame "Hidx".
+    iMod (own_update _ _ (ghosttoken_st_to_R (Some (κ', 1%Qp))) with "Hset") as "Hset".
+    { rewrite /ghosttoken_st_to_R /=. apply cmra_update_exclusive. done. }
+    iMod ("Hclose" with "[] Hset") as "[Hset $]".
+    { iIntros "!> >Hset _".
+      iMod (own_update _ _ (ghosttoken_st_to_R None) with "Hset") as "Hset".
+      { rewrite /ghosttoken_st_to_R /=. apply cmra_update_exclusive. done. }
+      done. }
+    iExists κ'. iMod (bor_fracture with "LFT [Hset]") as "$"; first done.
+    { done. }
+    eauto.
+  Qed.
+  Next Obligation.
+    iIntros (?????) "#Hκ H".
+    iDestruct "H" as (γ) "[#? H]".
+    iDestruct "H" as (κ'') "[? ?]".
+    iExists _. iFrame "#".
+    iExists κ''.
+    by iSplit; first iApply lft_incl_trans.
+  Qed.
+ 
+  Global Instance ghosttoken_wf α : TyWf (ghosttoken α) :=
+    { ty_lfts := [α]; ty_wf_E := [] }.
+
+  Global Instance ghosttoken_ne : NonExpansive ghosttoken := _.
+
+  Global Instance ghosttoken_send α :
+    Send (ghosttoken α).
+  Proof. done. Qed.
+
+  Global Instance ghosttoken_sync α :
+    Sync (ghosttoken α).
+  Proof. done. Qed.
+
+  Global Instance ghosttoken_mono E L :
+    Proper (lctx_lft_eq E L ==> subtype E L) ghosttoken.
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic.
+              It would easily gain from some automation. *)
+    iIntros (α1 α2 [EQ1 EQ2] qmax qL) "HL".
+    iDestruct (EQ1 with "HL") as "#EQ1'".
+    iDestruct (EQ2 with "HL") as "#EQ2'".
+    iIntros "!# #HE".
+    iDestruct ("EQ1'" with "HE") as %EQ1'.
+    iDestruct ("EQ2'" with "HE") as %EQ2'.
+    iSplit; [|iSplit; iIntros "!# * H"]; simpl.
+    - iPureIntro; congruence.
+    - solve_proper_prepare.
+      iDestruct "H" as "[$ H]".
+      iDestruct "H" as (γ) "H".
+      iExists γ; iDestruct "H" as "[H $]".
+      by rewrite (lft_incl_syn_anti_symm _ _ EQ1' EQ2').
+    - iDestruct "H" as (γ) "H".
+      iExists γ; iDestruct "H" as "[H  $]".
+      by rewrite (lft_incl_syn_anti_symm _ _ EQ1' EQ2').
+  Qed.
+
+  Global Instance ghosttoken_mono'
+    E L : Proper (lctx_lft_eq E L ==> eqtype E L) ghosttoken.
+  Proof.
+    intros.
+    split; by apply ghosttoken_mono.
+  Qed.
+
+  (** β is the total sharing lifetime of the GhostCell.
+      (In the proofs below, β is often something else!) *)
+  Definition ghostcell_inv tid l β α ty : iProp Σ :=
+    (∃ st',
+      match st' with
+      | None => &{β}(l ↦∗: ty.(ty_own) tid) (* ghostcell is not currently being accessed *)
+      | Some rw => ∃ γ, lft_meta α γ ∗
+          match rw with
+          | true => (* ghostcell is currently being write-accessed *)
+              (* The κ' will be set to the lifetime β in borrow_mut, the lifetime
+              for which we exclusively have the borrow token.  If we own the
+              ghost token fragment (in any state), then at any time either κ'
+              still runs (so we get a contradiction when opening the borrow
+              here) or we can run the inheritance to get back the full
+              borrow. *)
+              ∃ κ', &{κ'} (own γ (ghosttoken_st_to_R None)) ∗
+                    ([†κ'] ={↑lftN}=∗ &{β} (l ↦∗: ty_own ty tid))
+          | false => (* ghostcell is currently being read-accessed *)
+              (* The κ' will be set to the total lifetime for which the token is
+              shared.  If we own the ghost token fragment in [None] state, then
+              we can deduce κ' is dead and we get back the full borrow. If we
+              own it in [Some] state we know the κ' is equal to the one in our
+              token, which outlives the lifetime of the token borrow that we got
+              (that is ensures in the GhostToken sharing interpretation), which
+              means it lives long enough to return it to the caller at that
+              lifetime. *)
+              ∃ κ', &frac{κ'} (λ q', own γ (ghosttoken_st_to_R (Some (κ', q')))) ∗
+                    ([†κ'] ={↑lftN}=∗ &{β}(l ↦∗: ty.(ty_own) tid)) ∗
+                    ty.(ty_shr) (β ⊓ κ') tid l
+          end
+      end)%I.
+
+  Global Instance ghostcell_inv_type_ne n tid l β α :
+    Proper (type_dist2 n ==> dist n) (ghostcell_inv tid l β α).
+  Proof.
+    solve_proper_core
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance ghostcell_inv_ne tid l β α : NonExpansive (ghostcell_inv tid l β α).
+  Proof.
+    intros n ???. by eapply ghostcell_inv_type_ne, type_dist_dist2.
+  Qed.
+
+  Lemma ghostcell_inv_proper E L κ1 κ2 ty1 ty2 qmax qL :
+    lctx_lft_eq E L κ1 κ2 →
+    eqtype E L ty1 ty2 →
+    llctx_interp_noend qmax L qL -∗ ∀ tid l β, □ (elctx_interp E -∗
+    ghostcell_inv tid l β κ1 ty1 -∗ ghostcell_inv tid l β κ2 ty2).
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic. *)
+    (*             It would easily gain from some automation. *)
+    rewrite eqtype_unfold. iIntros ([Hlft1 Hlft2] Hty) "HL".
+    iDestruct (Hty with "HL") as "#Hty".
+    iDestruct (Hlft1 with "HL") as "#Hlft1".
+    iDestruct (Hlft2 with "HL") as "#Hlft2".
+    iIntros (tid l β) "!# #HE H".
+    iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
+    iDestruct ("Hlft1" with "HE") as %Hκ1.
+    iDestruct ("Hlft2" with "HE") as %Hκ2.
+    iAssert (□ (&{β}(l ↦∗: ty_own ty1 tid) -∗
+                &{β}(l ↦∗: ty_own ty2 tid)))%I as "#Hb".
+    { iIntros "!# H". iApply bor_iff; last done.
+      iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iFrame; by iApply "Hown". }
+    iDestruct "H" as (rw) "H"; iExists rw; destruct rw as [rw|]; iFrame "∗";
+      last by iApply "Hb"; last first.
+    iDestruct "H" as (γc) "(#Hsing&H)".
+    iExists γc.
+    iSplitR.
+    { by rewrite (lft_incl_syn_anti_symm _ _ Hκ1 Hκ2). }
+    destruct rw.
+    { iDestruct "H" as (κ') "H'".
+      iExists κ'; iDestruct "H'" as "($ & H')".
+      iIntros "Hκ'". iMod ("H'" with "Hκ'"). by iApply "Hb". }
+    iDestruct "H" as (κ') "(Hag&Hh&H)"; iExists κ'; iFrame "Hag".
+    iSplitL "Hh"; last by iApply "Hshr".
+    iIntros "Hν". iMod ("Hh" with "Hν") as "Hh".
+    by iApply "Hb".
+  Qed.
+
+  (* Idea:
+     Ghostcell is basically a refcell/rwlock.  Main difference being that current r/w state is
+     not directly tied to any physical state (for ty_shr); in other words, you can't really do
+     anything with just a ghostcell.  The ghosttoken is responsible for tracking the r/w state of any
+     ghostcells that are currently open.  A share of a ghosttoken always tracks the exact fraction
+     that it is sharing.  It may not actually be necessary for the ghosttoken to track these things
+     explicitly, since a read borrow is the same as a regular borrow.
+
+     Key point: you don't really need to prove you can go from a borrow back to the original
+     resource under normal circumstances.  For atomic borrows you just need to show that the
+     thing inside the atomic borrow holds initially (which can just be the original borrow you
+     got plus some ownership of ghost state, if you want).  To *update* an atomic borrow, you
+     just have to show you can go back to the original resource *or* the token is dead.
+     To update an original borrow (and not change the mask) you need to show that the token is
+     alive initially, and that the resource to which you want to update it can move back to P
+     with the empty mask and no access to the token you povided.  bor_acc_atomic and friends do
+     other stuff.
+
+    (when the lifetime is dead it can
+     be removed from the track set).
+  *)
+  Program Definition ghostcell (α : lft) (ty : type) :=
+    tc_opaque
+    {| ty_size        := ty.(ty_size);
+       ty_own tid vl  := ty.(ty_own) tid vl;
+       ty_shr κ tid l :=
+         (∃ β, κ ⊑ β ∗ &at{β, ghostcellN}(ghostcell_inv tid l β α ty))%I |}.
+  Next Obligation.
+    iIntros (????) "H". by rewrite ty_size_eq.
+  Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q ?) "#LFT Hvl [Htok Htok']".
+    iAssert ((q / 2).[κ] ∗ ▷ ghostcell_inv tid l κ α ty)%I with "[> -Htok]"
+      as "[$ HQ]"; last first.
+    { iFrame "Htok".
+      iExists κ.
+      iSplitR; first by iApply lft_incl_refl.
+      iMod (bor_create _ κ with "LFT HQ") as "[HQ HQ']"; first done.
+      iApply bor_share; first solve_ndisj.
+      iFrame "∗". }
+    iFrame. iExists None. by iFrame.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#Hκ H". iDestruct "H" as (β) "H".
+    iExists β; iDestruct "H" as "[? $]".
+    by iApply lft_incl_trans.
+  Qed.
+
+  Global Instance ghostcell_wf α `{!TyWf ty} : TyWf (ghostcell α ty) :=
+    { ty_lfts := α::ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Global Instance ghostcell_type_ne α : TypeNonExpansive (ghostcell α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(
+        fun _ => exact: type_dist2_S || (eapply ghostcell_inv_type_ne; try reflexivity) ||
+                        (eapply ghostcell_inv_proj_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance ghostcell_ne α : NonExpansive (ghostcell α).
+  Proof.
+    constructor; solve_proper_core ltac:(
+                   fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  Global Instance ghostcell_mono E L : Proper (lctx_lft_eq E L ==> eqtype E L ==> subtype E L)
+                                               (ghostcell).
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic.
+              It would easily gain from some automation. *)
+    iIntros (κ κ' [EQ1 EQ1'] ty1 ty2 EQ2 qmax qL) "HL". generalize EQ2. rewrite eqtype_unfold=>EQ'2.
+    iDestruct (EQ1 with "HL") as "#EQ1".
+    iDestruct (EQ1' with "HL") as "#EQ1'".
+    iDestruct (EQ'2 with "HL") as "#EQ'".
+    iDestruct (ghostcell_inv_proper _ _ κ κ' with "HL") as "#Hty1ty2"; [done|done|].
+    iDestruct (ghostcell_inv_proper _ _ κ' κ with "HL") as "#Hty2ty1"; [done|by symmetry|].
+    iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
+    iSplit; [|iSplit; iIntros "!# * H"]; simpl.
+    - iPureIntro; congruence.
+    - by iApply "Hown".
+    - iDestruct "H" as (a) "H".
+      iExists a; iDestruct "H" as "[$ H]".
+      iApply at_bor_iff; last done.
+      iNext; iModIntro; iSplit; iIntros "H"; by [iApply "Hty1ty2"|iApply "Hty2ty1"].
+  Qed.
+
+  Lemma ghostcell_mono' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_eq E L κ1 κ2 →
+    eqtype E L ty1 ty2 →
+    subtype E L (ghostcell κ1 ty1) (ghostcell κ2 ty2).
+  Proof. intros. by eapply ghostcell_mono. Qed.
+
+  Global Instance ghostcell_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) ghostcell.
+  Proof. by split; apply ghostcell_mono. Qed.
+
+  Lemma ghostcell_proper' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_eq E L κ1 κ2 →
+    eqtype E L ty1 ty2 →
+    eqtype E L (ghostcell κ1 ty1) (ghostcell κ2 ty2).
+  Proof. intros. by apply ghostcell_proper. Qed.
+
+  Hint Resolve ghostcell_mono' ghostcell_proper' : lrust_typing.
+
+  Global Instance ghostcell_send α ty :
+    Send ty → Send (ghostcell α ty).
+  Proof. by unfold ghostcell, Send. Qed.
+
+  Global Instance ghostcell_sync α ty :
+    Send ty → Sync ty → Sync (ghostcell α ty).
+  Proof.
+    intros Hsend Hsync ????.
+    solve_proper_prepare.
+    do 3 f_equiv.
+    unfold ghostcell_inv.
+    rewrite at_bor_proper; first done.
+    do 7 f_equiv.
+    - do 9 f_equiv. iApply send_change_tid'.
+    - do 4 f_equiv; last by iApply sync_change_tid'.
+      do 6 f_equiv. iApply send_change_tid'.
+    - iApply send_change_tid'.
+  Qed.
+
+  Definition ghosttoken_new (call_once : val) (R_F : type) : val :=
+    funrec: <> ["f"] :=
+      let: "call_once" := call_once in
+      let: "n" := new [ #0] in
+      letcall: "r" := "call_once" ["f";"n"]%E in
+      letalloc: "r'" <-{ R_F.(ty_size)} !"r" in
+      delete [ #R_F.(ty_size); "r"];;
+      return: ["r'"].
+
+  Lemma ghosttoken_new_type F R_F call_once `{!TyWf F, !TyWf R_F} :
+    typed_val call_once (fn(∀ α, ∅; F, ghosttoken α) → R_F) →
+    typed_val (ghosttoken_new call_once R_F) (fn(∅; F) → R_F).
+  Proof.
+    iIntros (Hf E L). iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (_ ϝ ret args). inv_vec args=>env. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (f); simpl_subst.
+    iApply type_new_subtype; [solve_typing..|].
+    iIntros (n).
+    simpl_subst.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hc (Hn & Hf & Henv & _)".
+    iMod (lctx_lft_alive_tok (ϝ) with "HE HL")
+      as (qϝf) "(Hϝf & HL & Hclosef)"; [solve_typing..|].
+    iMod (own_alloc (ghosttoken_st_to_R None)) as (γ) "Hown"; first done.
+    iMod (lft_create_meta γ with "LFT") as (α) "[#Hidx [Htok #Hα]]"; first done.
+    wp_let.
+    rewrite !tctx_hasty_val.
+    iDestruct (lft_intersect_acc with "Htok Hϝf") as (?) "[Hαϝ Hcloseα]".
+    iApply (type_call_iris _ [α; ϝ] (α) [_;_] _ _ _ _
+              with "LFT HE Hna [Hαϝ] Hf [Hn Henv Hown]"); try solve_typing.
+    + by rewrite /= (right_id static).
+    + rewrite /= (right_id emp%I) !tctx_hasty_val ownptr_uninit_own.
+      iFrame "Henv".
+      rewrite ownptr_own.
+      iDestruct "Hn" as (l vl) "(% & Hl & Hfree)".
+      iExists l, vl.
+      iSplit; first done.
+      simpl_subst.
+      iFrame.
+      iSplit; first by refine (match vl with Vector.nil => _ end).
+      iExists γ.
+      by iFrame "Hidx Hown".
+    + iIntros (r) "Hna Hf Hown".
+      simpl_subst.
+      iDestruct ("Hcloseα" with "[Hf]") as "[Htok Hf]"; first by rewrite right_id.
+      iMod ("Hclosef" with "Hf HL") as "HL".
+      wp_let.
+      iApply (type_type _ _ _ [ r ◁ box R_F ] with "[] LFT HE Hna HL Hc"); try solve_typing;
+        last by rewrite !tctx_interp_singleton tctx_hasty_val.
+      iApply type_letalloc_n; [solve_typing..|].
+      iIntros (r').
+      simpl_subst.
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+
+  Definition ghostcell_new : val :=
+    funrec: <> ["n"] :=
+      return: ["n"].
+
+  Lemma ghostcell_new_type `{!TyWf ty} :
+    typed_val ghostcell_new (fn(∀ α, ∅; ty) → (ghostcell α ty))%T.
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret args). inv_vec args=>n. simpl_subst.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk Hn".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iAssert (ty_own (box (ghostcell α ty)) tid [n])%I with "[Hn]" as "Hn".
+    { rewrite !ownptr_own.
+      iDestruct "Hn" as (l vl) "(% & Hl & Hown & Hfree)".
+      by iExists l, vl; simpl; iFrame "Hl Hown Hfree". }
+    rewrite -tctx_hasty_val -tctx_interp_singleton.
+    iApply (type_type with "[] LFT HE Hna HL Hk Hn").
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition ghostcell_borrow : val :=
+    funrec: <> ["c";"s"] :=
+      (* Skips needed for laters *)
+      Skip ;; Skip ;;
+      return: ["c"].
+
+  Lemma ghostcell_share E qβ β κ' tid lc γ κ α ty :
+    ↑lftN ⊆ E →
+    ⊢ (lft_ctx -∗
+    β ⊑ κ -∗
+    β ⊑ κ' -∗
+    &frac{κ'} (λ q : Qp, own γ (ghosttoken_st_to_R (Some (κ', q)))) -∗
+    (qβ).[β] -∗
+    lft_meta α γ -∗
+    &{κ} (lc ↦∗: ty_own ty tid) ={E}=∗
+      ▷ ghostcell_inv tid lc κ α ty ∗
+      ty_shr ty β tid lc ∗ (qβ).[β]).
+  Proof.
+    iIntros (HE) "#LFT #Hκ #Hβκ' #Hfractok [Hβ1 Hβ2] Hsing Hst'".
+    iMod (fupd_mask_subseteq (↑lftN)) as "Hclose"; first solve_ndisj.
+    iMod (lft_incl_acc with "Hκ Hβ1") as (q''2) "[Hq'' Hcloseq'']"; first solve_ndisj.
+    iMod (lft_incl_acc with "Hβκ' Hβ2") as (q''2_2) "[Hq''_2 Hcloseq''_2]";
+      first solve_ndisj.
+    iMod (rebor _ _ (κ ⊓ κ') (lc ↦∗: ty_own ty tid)%I with "LFT [] [Hst']")
+      as "[Hvl Hh]"; [done|iApply lft_intersect_incl_l|done|].
+    iDestruct (lft_intersect_acc with "Hq'' Hq''_2") as (q''3) "[Hq'' Hcloseq''2]".
+    iMod (ty_share with "LFT Hvl Hq''") as "[#Hshr Hq'']"; first solve_ndisj.
+    iDestruct ("Hcloseq''2" with "Hq''") as "[Hq'' Hq''_2]".
+    iMod ("Hcloseq''" with "Hq''") as "$".
+    iMod ("Hcloseq''_2" with "Hq''_2") as "$".
+    iDestruct (ty_shr_mono with "[] Hshr") as "$"; first by iApply lft_incl_glb.
+    iMod "Hclose" as "_".
+    iExists (Some false), γ; iFrame "Hsing".
+    iExists κ'; iFrame "#∗". iIntros "!> !> Htok".
+    iApply "Hh". iApply lft_dead_or. by iRight.
+  Qed.
+
+  Lemma ghostcell_borrow_type `{!TyWf ty} :
+    typed_val ghostcell_borrow
+              (fn(∀ '(α, β), ∅; &shr{β} (ghostcell α ty), &shr{β} (ghosttoken α)) →
+                  &shr{β} ty)%T.
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros ([α β] ϝ ret args). inv_vec args=>c s. simpl_subst.
+    iIntros (tid qmax) "#LFT #HE Hna HL HC (Hc & Hs & _)".
+    rewrite !tctx_hasty_val.
+    iMod (lctx_lft_alive_tok β with "HE HL")
+      as (qβ) "([Hβ1 [Hβ2 Hβ3]] & HL & Hclose)"; [solve_typing..|].
+    iAssert (▷ |={⊤}[⊤∖↑ghostcellN]▷=> (ty_own (box (&shr{β} ty)) tid [c] ∗ (qβ).[β]))%I
+      with "[Hβ1 Hβ2 Hβ3 Hs Hc]"as "Hc".
+    { iClear "HE".
+      rewrite (ownptr_own (_ (_ (ghostcell _ _))))
+              (ownptr_own (_ (&shr{β} ty)))%T.
+      rewrite ownptr_own.
+      iDestruct "Hs" as (l' vl') "(_ & _ & Hats & _)".
+      iDestruct "Hc" as (l vl) "(% & Hl & Hatc & Hfree)".
+      subst.
+      inv_vec vl'=>ls'.
+      iAssert _ with "Hats" as "#Hats'".
+      iDestruct (shr_is_ptr with "Hats'") as (ls) "> H". iDestruct "H" as %H.
+      inversion H; subst; iClear (H) "Hats'".
+      inv_vec vl=>lc'.
+      iAssert _ with "Hatc" as "#Hatc'".
+      iDestruct (shr_is_ptr with "Hatc'") as (lc)  "> H". iDestruct "H" as %H.
+      inversion H; simpl_subst; iClear (H) "Hatc'".
+      iDestruct "Hats" as (γ) "[Hsing Hats]".
+      iDestruct "Hats" as (κ') "[#Hβκ' #Hats]".
+      iDestruct "Hatc" as (κ) "[#Hκ Hatc]".
+      iDestruct (at_bor_shorten with "Hκ Hatc") as "Hatc'".
+      iIntros "!>".
+      iMod (at_bor_acc_tok with "LFT Hatc' Hβ1") as "[Hcell Hclosec]"; [solve_ndisj..|].
+      iDestruct "Hcell" as (st') "Hst'".
+      destruct st' as [rw|].
+      { iDestruct "Hst'" as (γ') "(>Hsing' & Hst')".
+        iDestruct (lft_meta_agree with "Hsing Hsing'") as %<-.
+        iClear "Hsing'".
+        iIntros "!> !>".
+        iMod (fupd_mask_subseteq (↑lftN)) as "Hclose"; first solve_ndisj.
+        iDestruct (frac_bor_shorten with "Hβκ' Hats") as "Hats'".
+        iMod (frac_bor_acc with "LFT Hats' Hβ2") as (q') "[>Hset Hcloses] {Hats'}"; [solve_ndisj..|].
+        destruct rw as[|].
+        { iDestruct "Hst'" as (κ'0) "(Hbor & Hdead)".
+          iMod (bor_acc_atomic with "LFT Hbor") as "[[> Hst' Hcloseb]|[H† Hcloseb]]"; first done.
+          - iDestruct (own_valid_2 with "Hset Hst'") as %[].
+          - iMod "Hcloseb" as "_".
+            iMod ("Hdead" with "H†") as "Hst'".
+            iMod ("Hcloses" with "Hset") as "Hβ2".
+            iMod "Hclose" as "_".
+            iMod (ghostcell_share with "LFT Hκ Hβκ' Hats Hβ3 Hsing Hst'")
+              as "(Hinv' & Hshr & Hβ3)"; first solve_ndisj.
+            iMod ("Hclosec" with "Hinv'") as "$".
+            iFrame "Hβ3 Hβ2".
+            iModIntro.
+            iExists l, (Vector.cons #lc Vector.nil).
+            by iFrame "Hshr Hl Hfree". }
+        iDestruct "Hst'" as (κ'0) "(Hκ'0bor & Hνκ & #Hshrκ)".
+        iMod (frac_bor_atomic_acc with "LFT Hκ'0bor")
+          as "[Hsucc|[Hκ'0† >_]]"; first done; last first.
+        { iMod ("Hνκ" with "Hκ'0†") as "Hst'".
+          iClear "Hshrκ".
+          iMod ("Hcloses" with "Hset") as "Hβ2".
+          iMod "Hclose" as "_".
+          iMod (ghostcell_share with "LFT Hκ Hβκ' Hats Hβ3 Hsing Hst'")
+            as "(Hinv' & Hshr & Hβ3)"; first solve_ndisj.
+          iMod ("Hclosec" with "Hinv'") as "$".
+          iFrame "Hβ3 Hβ2".
+          iModIntro.
+          iExists l, (Vector.cons #lc Vector.nil).
+          by iFrame "Hshr Hl Hfree". }
+        iDestruct "Hsucc" as (q'0) "[>Hownκ'0 Hcloseκ'0]".
+        iDestruct (own_valid_2 with "Hset Hownκ'0") as %Hvalidκ'0.
+        (* Argue that we have the same κ' here as the already existing sharing protocol. *)
+        assert (Hκ'κ'0 : κ' = κ'0).
+        { move: Hvalidκ'0. rewrite /ghosttoken_st_to_R /=.
+          rewrite -Cinr_op /valid /cmra_valid /=.
+          rewrite pair_valid /=.
+          intros [?%to_agree_op_inv_L _]. done. }
+        subst κ'0.
+        iMod ("Hcloseκ'0" with "Hownκ'0") as "_".
+        iDestruct (ty_shr_mono with "[] Hshrκ") as "Hshrβ"; first by iApply lft_incl_glb.
+        iMod ("Hcloses" with "Hset") as "Hβ2".
+        iMod "Hclose" as "_".
+        iMod ("Hclosec" with "[Hνκ Hsing]") as "$".
+        { iNext.
+          iExists (Some false).
+          iExists γ.
+          iFrame "Hsing".
+          iExists κ'.
+          by iFrame "Hνκ Hshrκ". }
+        iFrame "Hβ3 Hβ2".
+        iExists l, (Vector.cons #lc Vector.nil).
+        by iFrame "Hshrβ Hl Hfree". }
+      iIntros "!> !>".
+      iMod (fupd_mask_subseteq (↑lftN)) as "Hclose"; first solve_ndisj.
+      iMod "Hclose" as "_".
+      iMod (ghostcell_share with "LFT Hκ Hβκ' Hats Hβ3 Hsing Hst'")
+        as "(Hinv' & Hshr & Hβ3)"; first solve_ndisj.
+      iMod ("Hclosec" with "Hinv'") as "$".
+      iFrame "Hβ3 Hβ2".
+      iModIntro.
+      iExists l, (Vector.cons #lc Vector.nil).
+      by iFrame "Hshr Hl Hfree". }
+    wp_let.
+    iApply lifting.wp_pure_step_fupd; first done.
+    iMod "Hc".
+    iIntros "!> !>".
+    iMod "Hc".
+    iDestruct "Hc" as "[Hshr Hβ]".
+    iMod ("Hclose" with "Hβ HL") as "HL".
+    iIntros "!>".
+    do 2 wp_let.
+    iApply (type_type _ _ _ [c ◁  box (&shr{β} ty)]
+              with "[] LFT HE Hna HL HC [Hshr]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition ghostcell_borrow_mut : val :=
+    funrec: <> ["c";"s"] :=
+      (* Skips needed for laters *)
+      Skip ;; Skip ;;
+      return: ["c"].
+
+  Lemma ghostcell_borrow_mut_type `{!TyWf ty} :
+    typed_val ghostcell_borrow_mut
+              (fn(∀ '(α, β), ∅; &shr{β} (ghostcell α ty), &uniq{β} (ghosttoken α)) →
+                  &uniq{β} ty)%T.
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros ([α β] ϝ ret args). inv_vec args=>c s. simpl_subst.
+    iIntros (tid qmax) "#LFT #HE Hna HL HC (Hc & Hs & _)".
+    rewrite !tctx_hasty_val.
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "([Hβ1 [Hβ2 Hβ3]] & HL & Hclose)";
+      [solve_typing..|].
+    iAssert (▷ |={⊤}[⊤∖↑ghostcellN]▷=> (ty_own (box (&uniq{β} ty)) tid [c] ∗ (qβ).[β]))%I
+      with "[Hβ1 Hβ2 Hβ3 Hs Hc]"as "Hc".
+    { iClear "HE".
+      rewrite (ownptr_own (_ (_ (ghostcell _ _))))
+              (ownptr_own (_ (&uniq{β} ty)))%T.
+      rewrite ownptr_own.
+      iDestruct "Hs" as (l' vl') "(_ & _ & Hats & _)".
+      iDestruct "Hc" as (l vl) "(% & Hl & Hatc & Hfree)".
+      subst.
+      inv_vec vl'=>ls'.
+      destruct ls' as [[|ls|]|]; try by iDestruct "Hats" as "> []".
+      inv_vec vl=>lc'.
+      iAssert _ with "Hatc" as "#Hatc'".
+      iDestruct (shr_is_ptr with "Hatc'") as (lc) "> H". iDestruct "H" as %H.
+      inversion H; simpl_subst; iClear (H) "Hatc'".
+      iDestruct "Hatc" as (κ) "[#Hκ Hatc]".
+      iDestruct (at_bor_shorten with "Hκ Hatc") as "Hatc'".
+      iIntros "!>".
+      iMod (at_bor_acc_tok with "LFT Hatc' Hβ1") as "[Hcell Hclosec]"; [solve_ndisj..|].
+      iDestruct "Hcell" as (st') "Hst'".
+      iMod (bor_acc_strong with "LFT Hats Hβ2") as (κ'1) "[#Hκ'κ'1 [Hats Hcloses]]"; first solve_ndisj.
+      iDestruct "Hats" as (vl) "(> Hls & > % & >Hats)".
+      subst vl.
+      iDestruct "Hats" as (γ) "[#Hsing Hset]".
+      iAssert ((|={⊤ ∖ ↑ghostcellN}▷=>
+                own γ (Cinl (Excl ())) ∗
+                 (&{κ} (lc ↦∗: ty_own ty tid))) (* ∨
+               (_ ∗ ▷ ghostcell_inv tid lc κ α ty ∗ |={⊤}▷=> ▷ ▷ False) *) )%I
+        with "[Hst' Hset]" as "Hown".
+      { destruct st' as [rw|]; last first.
+        { eauto with iFrame. }
+        iDestruct "Hst'" as (γ') "(>Hsing' & Hst')".
+        iDestruct (lft_meta_agree with "Hsing Hsing'") as %<-.
+        iClear "Hsing'".
+        iIntros "!> !>".
+        iMod (fupd_mask_subseteq (↑lftN)) as "Hclose"; first solve_ndisj.
+        destruct rw as [|].
+        { iDestruct "Hst'" as (κ'0) "(Hbor & Hdead)".
+          iMod (bor_acc_atomic with "LFT Hbor") as "[[> Hst' Hcloseb]|[H† Hcloseb]]";
+            first done.
+          { iDestruct (own_valid_2 with "Hset Hst'") as %[]. }
+          iMod "Hcloseb" as "_".
+          iMod ("Hdead" with "H†") as "Hst'".
+          iFrame. done. }
+        iDestruct "Hst'" as (κ') "(Hst' & Hνκ & #Hshrκ)".
+        iDestruct "Hst'" as "Hκ'0bor".
+        iClear "Hshrκ".
+        iMod (frac_bor_atomic_acc with "LFT Hκ'0bor") as "[Hsucc|[H Hcloseb]]"; first done.
+        { iDestruct "Hsucc" as (q) "[>Htok _]".
+          iDestruct (own_valid_2 with "Hset Htok") as %[]. }
+        iMod "Hcloseb" as "_".
+        iMod ("Hνκ" with "H") as "$".
+        iMod "Hclose".
+        by iFrame. }
+      iMod "Hown".
+      iIntros "!> !>".
+      iMod "Hown" as "[Hset Hown]".
+      iMod ("Hcloses" $! (own γ (ghosttoken_st_to_R None)) with "[Hls] Hset") as "[Hset Hβ]".
+      { iIntros "!> >Hset _". iExists []. eauto 10 with iFrame. }
+      iMod (fupd_mask_subseteq (↑lftN)) as "Hclose"; first solve_ndisj.
+      iMod (rebor with "LFT Hκ Hown") as "[Hbor Hcloseβ]"; first solve_ndisj.
+      iMod "Hclose" as "_".
+      iMod ("Hclosec" with "[Hcloseβ Hset]") as "$".
+      { iExists (Some true), γ.
+        iFrame "Hsing". iExists β; iFrame. iNext.
+        iApply bor_shorten; last done. done.
+      }
+      iFrame "Hβ3 Hβ".
+      iExists l, (Vector.cons #lc Vector.nil).
+      iAssert (⌜#l = #l⌝)%I as "$"; first done.
+      by iFrame "Hl Hfree Hbor". }
+    wp_let.
+    iApply lifting.wp_pure_step_fupd; first done.
+    iMod "Hc".
+    iIntros "!> !>".
+    iMod "Hc".
+    iDestruct "Hc" as "[Hshr Hβ]".
+    iMod ("Hclose" with "Hβ HL") as "HL".
+    iIntros "!>".
+    do 2 wp_let.
+    iApply (type_type _ _ _ [c ◁  box (&uniq{β} ty)]
+              with "[] LFT HE Hna HL HC [Hshr]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition ghostcell_as_mut : val :=
+    funrec: <> ["c"] :=
+      return: ["c"].
+
+  Lemma ghostcell_as_mut_type `{!TyWf ty} :
+    typed_val ghostcell_as_mut (fn(∀ '(α, β), ∅; &uniq{β} (ghostcell α ty)) →
+                                  &uniq{β} ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros ([α β] ϝ ret args). inv_vec args=>c. simpl_subst.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk Hc".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iAssert (ty_own (box (&uniq{β} ty)) tid [c])%I with "[Hc]" as "Hc".
+    { rewrite !ownptr_own.
+      iDestruct "Hc" as (l vl) "(% & Hl & Hown & Hfree)".
+      iExists l, vl; rewrite /ty_own /=. by iFrame "Hl Hown Hfree". }
+    rewrite -tctx_hasty_val -tctx_interp_singleton.
+    iApply (type_type with "[] LFT HE Hna HL Hk Hc").
+    iApply type_jump; solve_typing.
+  Qed.
+
+End ghostcell.
-- 
GitLab