From 98942d65ab07c1e1cb5a41d9d1e0a5338e086923 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 26 Apr 2017 13:30:33 +0200
Subject: [PATCH] Starting the work on arc.

---
 _CoqProject                 |   1 +
 theories/lang/lib/arc.v     | 224 ++++++----
 theories/typing/lib/arc.v   | 810 ++++++++++++++++++++++++++++++++++++
 theories/typing/lib/rc/rc.v |   2 +
 4 files changed, 948 insertions(+), 89 deletions(-)
 create mode 100644 theories/typing/lib/arc.v

diff --git a/_CoqProject b/_CoqProject
index 3c87ace3..e7edaf13 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
+theories/typing/lib/arc.v
 theories/typing/lib/mutex/mutex.v
 theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell.v
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index dc1211c5..09727506 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -7,7 +7,7 @@ From iris.algebra Require Import excl csum frac auth.
 From lrust.lang Require Import lang proofmode notation new_delete.
 Set Default Proof Using "Type".
 
-(* TODO : get_mut, make_mut, try_unwrap *)
+(* TODO : get_mut, make_mut *)
 
 Definition clone_arc : val :=
   rec: "clone" ["l"] :=
@@ -32,25 +32,32 @@ Definition upgrade : val :=
       if: CAS "l" "strong" ("strong" + #1) then #true
       else "upgrade" ["l"].
 
-Definition drop_weak dealloc `{Closed [] dealloc} : val :=
-  rec: "drop" ["l"] :=
+Definition drop_weak : val :=
+  rec: "drop" ["l"; "dealloc"] :=
     let: "weak" := !ˢᶜ("l" +ₗ #1) in
     if: CAS ("l" +â‚— #1) "weak" ("weak" - #1) then
-      if: "weak" = #1 then dealloc else #()
-    else "drop" ["l"].
+      if: "weak" = #1 then "dealloc" [] else #()
+    else "drop" ["l"; "dealloc"].
 
-Definition drop_arc drop dealloc `{Closed [] drop, Closed [] dealloc} : val :=
-  rec: "drop" ["l"] :=
+Definition drop_arc : val :=
+  rec: "drop_arc" ["l"; "drop"; "dealloc"] :=
     let: "strong" := !ˢᶜ"l" in
     if: CAS "l" "strong" ("strong" - #1) then
       if: "strong" = #1 then
-        drop;;
-        drop_weak dealloc ["l"]
+        "drop" [];;
+        drop_weak ["l"; "dealloc"]
       else #()
-    else "drop" ["l"].
+    else "drop_arc" ["l"; "drop"; "dealloc"].
 
 Definition try_unwrap : val :=
-  rec: "try_unwrap" ["l"] := CAS "l" #1 #0.
+  λ: ["l"], CAS "l" #1 #0.
+
+Definition try_unwrap_full : val :=
+  λ: ["l"],
+    if: CAS "l" #1 #0 then
+      if: !ˢᶜ("l" +ₗ #1) = #1 then #0
+      else "l" <- #1;; #1
+    else #2.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -62,19 +69,16 @@ Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
 Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
-Definition arc_tok q : authR arc_stR :=
-  â—¯ (Some $ Cinl (q, 1%positive), 0%nat).
-Definition arc_dropping_tok : authR arc_stR :=
-  â—¯ (Some $ Cinr $ Excl (), 0%nat).
-Definition weak_tok : authR arc_stR := â—¯ (None, 1%nat).
+Section def.
+  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
 
-Section arc.
-  Context `{!lrustG Σ, !arcG Σ} (N : namespace) (P1 : Qp → iProp Σ)
-          {HP1:Fractional P1} (P2 : iProp Σ).
-  Set Default Proof Using "HP1".
+  Definition arc_tok γ q : iProp Σ :=
+    own γ (◯ (Some $ Cinl (q, 1%positive), 0%nat)).
+  Definition weak_tok γ : iProp Σ :=
+    own γ (◯ (None, 1%nat)).
 
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
-  Proof. done. Qed.
+  Global Instance arc_tok_timeless γ q : TimelessP (arc_tok γ q) := _.
+  Global Instance weak_tok_timeless γ : TimelessP (weak_tok γ) := _.
 
   Definition arc_inv (γ : gname) (l : loc) : iProp Σ :=
     (∃ st : arc_stR, own γ (● st) ∗
@@ -92,22 +96,50 @@ Section arc.
   Definition is_arc (γ : gname) (l : loc) : iProp Σ :=
     inv N (arc_inv γ l).
 
+  Global Instance is_arc_persistent γ l : PersistentP (is_arc γ l) := _.
+
   Definition arc_tok_acc (γ : gname) P E : iProp Σ :=
-    (□ (P ={E,∅}=∗ ∃ q, own γ (arc_tok q) ∗ (own γ (arc_tok q) ={∅,E}=∗ P)))%I.
+    (□ (P ={E,∅}=∗ ∃ q, arc_tok γ q ∗ (arc_tok γ q ={∅,E}=∗ P)))%I.
 
   Definition weak_tok_acc (γ : gname) P E : iProp Σ :=
-    (□ (P ={E,∅}=∗ own γ weak_tok ∗ (own γ weak_tok ={∅,E}=∗ P)))%I.
+    (□ (P ={E,∅}=∗ weak_tok γ ∗ (weak_tok γ ={∅,E}=∗ P)))%I.
+
+  Definition dealloc_spec l (dealloc : val) P : iProp Σ :=
+    ({{{ P ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0 ∗ P2}}} dealloc []
+     {{{ RET #(); P }}})%I.
+
+  Definition drop_spec (drop : val) P : iProp Σ :=
+    ({{{ P ∗ P1 1 }}} drop [] {{{ RET #(); P ∗ P2 }}})%I.
+End def.
+
+Section arc.
+  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+          (P2 : iProp Σ) (N : namespace).
+
+  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Proof using HP1. done. Qed.
 
-  Definition dealloc_spec dealloc P : iProp Σ :=
-    ({{{ P ∗ P2 }}} dealloc {{{ RET #(); P }}})%I.
+  Global Instance arc_inv_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n ==> eq ==> eq ==> dist n)
+           arc_inv.
+  Proof. solve_proper. Qed.
+  Global Instance arc_inv_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> (≡))
+           arc_inv.
+  Proof. solve_proper. Qed.
 
-  Definition unwrap_spec unwrap P : iProp Σ :=
-    ({{{ P ∗ P1 1 }}} unwrap {{{ RET #(); P ∗ P2 }}})%I.
+  Global Instance is_arc_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist_later n ==> eq ==> eq ==> eq ==> dist n)
+           is_arc.
+  Proof. solve_contractive. Qed.
+  Global Instance is_arc_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> eq ==> (≡)) is_arc.
+  Proof. solve_proper. Qed.
 
   Lemma create_arc E l :
-    l ↦ #1 -∗ shift_loc l 1 ↦ #1 -∗ P1 1 ={E}=∗
-      ∃ γ q, is_arc γ l ∗ P1 q ∗ own γ (arc_tok q).
-  Proof.
+    l ↦ #1 -∗ shift_loc l 1 ↦ #1 -∗ P1 1%Qp ={E}=∗
+      ∃ γ q, is_arc P1 P2 N γ l ∗ P1 q ∗ arc_tok γ q.
+  Proof using HP1.
     iIntros "Hl1 Hl2 [HP1 HP1']".
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH), O) ⋅
                       ◯ (Some $ Cinl ((1/2)%Qp, xH), O)))) as (γ) "[H● H◯]"; first done.
@@ -116,44 +148,45 @@ Section arc.
   Qed.
 
   Lemma create_weak E l :
-    l ↦ #0 -∗ shift_loc l 1 ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc γ l ∗ own γ weak_tok.
+    l ↦ #0 -∗ shift_loc l 1 ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
   Proof.
     iIntros "Hl1 Hl2 HP2".
     iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]"; first done.
     iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
   Qed.
 
-  Lemma arc_tok_auth_val st q :
-    ✓ (● st ⋅ arc_tok q) →
-    ∃ q' strong weak, st = (Some $ Cinl (q', strong), weak) ∧
-                      if decide (strong = xH) then q = q'
-                      else ∃ q'', (q' = q + q'')%Qp.
+  Lemma arc_tok_auth_val st γ q :
+    own γ (● st) -∗ arc_tok γ q -∗
+    ⌜∃ q' strong weak, st = (Some $ Cinl (q', strong), weak) ∧
+                       if decide (strong = xH) then q = q'
+                        else ∃ q'', q' = (q + q'')%Qp⌝.
   Proof.
-    move=>/auth_valid_discrete_2 [/prod_included [/option_included Hincl _] [Hval _]].
+    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
     destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
       simpl in *; subst.
-    - setoid_subst. eexists _, _, _. by split.
+    - setoid_subst. iExists _, _, _. by iSplit.
     - destruct Hincl as [->|[(?&[]&[=<-]&->&
              [[??]%frac_included%Qp_lt_sum  ?%pos_included]%prod_included)|
         (?&?&[=]&?)]]; first done.
-      eexists _, _, _. split=>//. simpl in *. destruct decide; [subst;lia|eauto].
+      iExists _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
   Qed.
 
   Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
     {{{ P }}} clone_arc [ #l]
-    {{{ q', RET #(); P ∗ own γ (arc_tok q') ∗ P1 q' }}}.
-  Proof.
+    {{{ q', RET #(); P ∗ arc_tok γ q' ∗ P1 q' }}}.
+  Proof using HP1.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
     iInv N as (st) "[>H● H]" "Hclose1".
     iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (own_valid_2 with "H● Hown") as %(?& strong &?&[-> _])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&[-> _]).
     iDestruct "H" as (?) "[H H']". wp_read. iMod ("Hclose2" with "Hown") as "HP".
     iModIntro. iMod ("Hclose1" with "[H H' H●]") as "_".
     { iExists _. auto with iFrame. }
     iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
     iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (own_valid_2 with "H● Hown") as %(?&strong'&?&[-> _])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&[-> _]).
     iDestruct "H" as (q) "(Hl & Hl1 & >Heq & [HP1 HP1'])". iDestruct "Heq" as %Heq.
     destruct (decide (strong = strong')) as [->|?].
     - wp_apply (wp_cas_int_suc with "Hl"); first done. iIntros "Hl".
@@ -175,21 +208,21 @@ Section arc.
       iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
   Qed.
 
-  Lemma downgrade_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} downgrade [ #l] {{{ RET #(); P ∗ own γ weak_tok }}}.
+  Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} downgrade [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
   Proof.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
     iInv N as (st) "[>H● H]" "Hclose1".
     iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (own_valid_2 with "H● Hown") as %(?&?& weak &[-> _])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& weak &[-> _]).
     iDestruct "H" as (?) "(H & H' & H'')". wp_read. iMod ("Hclose2" with "Hown") as "HP".
     iModIntro. iMod ("Hclose1" with "[H H' H'' H●]") as "_".
     { iExists _. auto with iFrame. }
     iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). wp_op.
     iInv N as (st) "[>H● H]" "Hclose1".
     iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (own_valid_2 with "H● Hown") as %(?&?& weak' &[-> _])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& weak' &[-> _]).
     iDestruct "H" as (q) "(Hl & Hl1 & >Heq & HP1)". iDestruct "Heq" as %Heq.
     destruct (decide (weak = weak')) as [<-|Hw].
     - wp_apply (wp_cas_int_suc with "Hl1"); first done. iIntros "Hl1".
@@ -209,25 +242,26 @@ Section arc.
       iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
   Qed.
 
-  Lemma weak_tok_auth_val st :
-    ✓ (● st ⋅ weak_tok) → ∃ st' weak, st = (st', S weak) ∧ ✓ st'.
+  Lemma weak_tok_auth_val γ st :
+    own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
   Proof.
-    move=>/auth_valid_discrete_2 [/prod_included
-                [/option_included Hincl /nat_included Hincl'] [Hval _]].
+    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+        %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
+         %auth_valid_discrete_2.
     destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
   Qed.
 
   Lemma clone_weak_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ own γ weak_tok }}}.
+    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
   Proof.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
     iAssert (□ (P ={⊤,∅}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
-              (shift_loc l 1 ↦ #(w + 1) ={∅,⊤}=∗ P ∗ own γ weak_tok) ∧
+              (shift_loc l 1 ↦ #(w + 1) ={∅,⊤}=∗ P ∗ weak_tok γ) ∧
               (shift_loc l 1 ↦ #w ={∅,⊤}=∗ P)))%I as "#Hproto".
     { iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
       iMod ("Hacc" with "HP") as "[Hown Hclose2]".
-      iDestruct (own_valid_2 with "H● Hown") as %(st' & weak & -> & Hval)%weak_tok_auth_val.
+      iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
       destruct st' as [[[]| |]|]; try done; iExists _.
       - iDestruct "H" as (?) "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?";
         iMod ("Hclose2" with "Hown") as "HP".
@@ -265,18 +299,18 @@ Section arc.
       iModIntro. wp_apply (wp_if _ false). by iApply ("IH" with "Hown").
   Qed.
 
-  Lemma upgrade_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
+  Lemma upgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
     {{{ P }}} upgrade [ #l]
-    {{{ (b : bool) q, RET #b; P ∗ if b then own γ (arc_tok q) ∗ P1 q else True }}}.
-  Proof.
+    {{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
+  Proof using HP1.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
     iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
-              (⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ own γ (arc_tok q) ∗ ▷ P1 q) ∧
+              (⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
               (l ↦ #s ={∅,⊤}=∗ P)))%I as "#Hproto".
     { iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
       iMod ("Hacc" with "HP") as "[Hown Hclose2]".
-      iDestruct (own_valid_2 with "H● Hown") as %(st' & weak & -> & Hval)%weak_tok_auth_val.
+      iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
       destruct st' as [[[]| |]|]; try done; iExists _.
       - iDestruct "H" as (q) "(>$ & ? & >Heq & [HP1 HP1'])". iDestruct "Heq" as %Heq.
         iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
@@ -311,17 +345,18 @@ Section arc.
         iModIntro. wp_apply (wp_if _ false). by iApply ("IH" with "Hown").
   Qed.
 
-  Lemma drop_weak_spec dealloc `{Closed [] dealloc} (γ : gname) (l : loc) P :
-    is_arc γ l -∗ dealloc_spec dealloc P -∗
-    {{{ P ∗ own γ weak_tok }}} drop_weak dealloc [ #l] {{{ RET #() ; P }}}.
+  Lemma drop_weak_spec (dealloc : val) (γ : gname) (l : loc) P :
+    is_arc P1 P2 N γ l -∗ dealloc_spec P2 l dealloc P -∗
+    {{{ P ∗ weak_tok γ }}} drop_weak [ #l; dealloc] {{{ RET #() ; P }}}.
   Proof.
     iIntros "#INV #Hdealloc !# * [HP Hown] HΦ". iLöb as "IH". wp_rec. wp_op.
     wp_bind (!ˢᶜ_)%E.
-    iAssert (□ (own γ weak_tok ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
-              (shift_loc l 1 ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨ ▷ P2) ∧
-              (shift_loc l 1 ↦ #w ={⊤ ∖ ↑N,⊤}=∗ own γ weak_tok)))%I as "#Hproto".
+    iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
+              (shift_loc l 1 ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
+               ▷ P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0) ∧
+              (shift_loc l 1 ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
     { iIntros "!# Hown". iInv N as (st) "[>H● H]" "Hclose1".
-      iDestruct (own_valid_2 with "H● Hown") as %(st' & weak & -> & Hval)%weak_tok_auth_val.
+      iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
       destruct st' as [[[]| |]|]; try done; iExists _.
       - iDestruct "H" as (q) "(? & >$ & >Heq & HP1)". iIntros "!>"; iSplit; iIntros "Hl1".
         + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
@@ -337,12 +372,13 @@ Section arc.
                   (cancel_local_update_empty 1%nat), _. }
           iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
         + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
-      - iDestruct "H" as "(? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
+      - iDestruct "H" as "(>? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
         + iMod (own_update_2 with "H● Hown") as "H●".
           { apply auth_update_dealloc, prod_local_update_2,
                   (cancel_local_update_empty 1%nat), _. }
           destruct weak as [|weak].
-          * iMod ("Hclose1" with "[-HP2]") as "_"; last by auto. iExists _. iFrame.
+          * iMod ("Hclose1" with "[-HP2 H Hl1]") as "_"; last by auto with iFrame.
+            iExists _. iFrame.
           * iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
             iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
         + iFrame. iApply "Hclose1". iExists _. auto with iFrame. }
@@ -353,26 +389,26 @@ Section arc.
     - wp_apply (wp_cas_int_suc with "Hw"); first done. iIntros "Hw".
       iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hw") as "HP2". iModIntro.
       wp_apply (wp_if _ true). wp_op=>[->|?]; wp_if; last by iApply "HΦ".
-      iDestruct "HP2" as "[%|HP2]"; first done. by iApply ("Hdealloc" with "[$HP $HP2]").
+      iDestruct "HP2" as "[%|(? & ? & ? )]"; first done.
+      iApply ("Hdealloc" with "[-HΦ]"); iFrame.
     - wp_apply (wp_cas_int_fail with "Hw"); try done. iIntros "Hw".
       iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown". iModIntro.
       wp_apply (wp_if _ false). by iApply ("IH" with "HP Hown").
   Qed.
 
-  Lemma drop_arc_spec drop dealloc `{Closed [] drop, Closed [] dealloc}
-        (γ : gname) (q: Qp) (l : loc) P :
-    is_arc γ l -∗ unwrap_spec drop P -∗ dealloc_spec dealloc P -∗
-    {{{ P ∗ own γ (arc_tok q) ∗ P1 q }}} drop_arc drop dealloc [ #l]
+  Lemma drop_arc_spec (drop dealloc : val) (γ : gname) (q: Qp) (l : loc) P :
+    is_arc P1 P2 N γ l -∗ drop_spec P1 P2 drop P -∗ dealloc_spec P2 l dealloc P -∗
+    {{{ P ∗ arc_tok γ q ∗ P1 q }}} drop_arc  [ #l; drop; dealloc]
     {{{ RET #() ; P }}}.
-  Proof.
+  Proof using HP1.
     iIntros "#INV #Hdrop #Hdealloc !# * (HP & Hown & HP1) HΦ". iLöb as "IH".
     wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (own_valid_2 with "H● Hown") as %(?& s &?&[-> _])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&[-> _]).
     iDestruct "H" as (?) "[H H']". wp_read. iMod ("Hclose" with "[H H' H●]") as "_".
     { iExists _. auto with iFrame. }
     iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
     iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (own_valid_2 with "H● Hown") as %(q' & s' & w &[-> Hqq'])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & w &[-> Hqq']).
     iDestruct "H" as (q'') "(Hs & Hw & >Hq'' & HP1')". iDestruct "Hq''" as %Hq''.
     destruct (decide (s = s')) as [<-|?].
     - wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
@@ -384,7 +420,7 @@ Section arc.
           by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
         iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
         iModIntro. wp_apply (wp_if _ true). wp_op=>[_|//]; wp_if.
-        rewrite -Hq''. wp_apply ("Hdrop" with "[$HP1 $HP1' $HP]"). iIntros "[HP HP2]".
+        rewrite -{1}Hq''. wp_apply ("Hdrop" with "[$HP1 $HP1' $HP]"). iIntros "[HP HP2]".
         wp_seq. iApply (drop_weak_spec with "INV Hdealloc [> -HΦ] HΦ").
         iInv N as ([st ?]) "[>H● H]" "Hclose".
         iDestruct (own_valid_2 with "H● H◯")
@@ -411,14 +447,13 @@ Section arc.
   Qed.
 
   Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) :
-    is_arc γ l -∗
-    {{{ own γ (arc_tok q) ∗ P1 q }}} try_unwrap [ #l]
+    is_arc P1 P2 N γ l -∗
+    {{{ arc_tok γ q ∗ P1 q }}} try_unwrap [ #l]
     {{{ (b : bool), RET #b ;
-        if b then P1 1 ∗ (P2 ={⊤}=∗ own γ weak_tok)
-        else own γ (arc_tok q) ∗ P1 q }}}.
-  Proof.
+        if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
+  Proof using HP1.
     iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (own_valid_2 with "H● Hown") as %(q' & s & w &[-> Hqq'])%arc_tok_auth_val.
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & w &[-> Hqq']).
     iDestruct "H" as (q'') "(Hs & Hw & >Hq'' & HP1')". iDestruct "Hq''" as %Hq''.
     destruct (decide (s = xH)) as [->|?].
     - wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
@@ -442,4 +477,15 @@ Section arc.
       iMod ("Hclose" with "[Hs Hw HP1' H●]") as "_"; first by iExists _; auto with iFrame.
       iApply ("HΦ" $! false). by iFrame.
   Qed.
-End arc.
\ No newline at end of file
+
+  (* Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) : *)
+  (*   is_arc γ l -∗ *)
+  (*   {{{ own γ (arc_tok q) ∗ P1 q }}} get_mut [ #l] *)
+  (*   {{{ (b : bool), RET #b ; *)
+  (*       if b then P1 1 ∗ (P1 1 ={⊤}=∗ ∃ γ' q', own γ' (arc_tok q') ∗ P1 q') *)
+  (*       else own γ (arc_tok q) ∗ P1 q }}}. *)
+  (* Proof. *)
+
+End arc.
+
+Typeclasses Opaque is_arc arc_tok weak_tok.
\ No newline at end of file
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
new file mode 100644
index 00000000..98a939c1
--- /dev/null
+++ b/theories/typing/lib/arc.v
@@ -0,0 +1,810 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lang.lib Require Import memcpy arc.
+From lrust.lifetime Require Import shr_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+Set Default Proof Using "Type".
+
+(* TODO : get_mut make_mut weak_count strong_count *)
+
+Definition arcN := lrustN .@ "arc".
+Definition arc_invN := arcN .@ "inv".
+Definition arc_shrN := arcN .@ "shr".
+Definition arc_endN := arcN .@ "end".
+
+Section arc.
+  Context `{!typeG Σ, !arcG Σ}.
+
+  (* Preliminary definitions. *)
+  Let P1 ν q := (q.[ν])%I.
+  Instance P1_fractional ν : Fractional (P1 ν).
+  Proof. unfold P1. apply _. Qed.
+  Let P2 l n := († l…(2 + n) ∗ shift_loc l 2 ↦∗: λ vl, ⌜length vl = n⌝)%I.
+  Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
+    (is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γ l ∗
+     (* We use this disjunction, and not simply [ty_shr] here, *)
+     (*    because [weak_new] cannot prove ty_shr, even for a dead *)
+     (*    lifetime. *)
+     (ty.(ty_shr) ν tid (shift_loc l 2) ∨ [†ν]) ∗
+     □ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
+          [†ν] ∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
+
+  Global Instance arc_persist_ne tid ν γ l n :
+    Proper (type_dist2 n ==> dist n) (arc_persist tid ν γ l).
+  Proof.
+    unfold arc_persist, P1, P2.
+    solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+                                     f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Lemma arc_persist_type_incl tid ν γ l ty1 ty2:
+    type_incl ty1 ty2 -∗ arc_persist tid ν γ l ty1 -∗ arc_persist tid ν γ l ty2.
+  Proof.
+    iIntros "#(Heqsz & Hinclo & Hincls) #(?& Hs & Hvs)".
+    iDestruct "Heqsz" as %->. iFrame "#". iSplit.
+    - iDestruct "Hs" as "[?|?]"; last auto. iLeft. by iApply "Hincls".
+    - iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+      iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "[??]". iExists _.
+      iFrame. by iApply "Hinclo".
+  Qed.
+
+  Lemma arc_persist_send tid tid' ν γ l ty `{!Send ty,!Sync ty} :
+    arc_persist tid ν γ l ty -∗ arc_persist tid' ν γ l ty.
+  Proof.
+    iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
+    iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+    iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "?". iExists _.
+    by rewrite send_change_tid.
+  Qed.
+
+  (* Model of arc *)
+  (* The ty_own part of the arc type cointains either the
+     shared protocol or the full ownership of the
+     content. The reason is that get_mut does not have the
+     masks to rebuild the invariants. *)
+  Definition full_arc_own l ty tid : iProp Σ:=
+    (l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
+       ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid)%I.
+  Definition shared_arc_own l ty tid : iProp Σ:=
+    (∃ γ ν q, arc_persist tid ν γ l ty ∗ arc_tok γ q ∗ q.[ν])%I.
+  Lemma arc_own_share E l ty tid :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ full_arc_own l ty tid ={E}=∗ shared_arc_own l ty tid.
+  Proof.
+    iIntros (?) "#LFT (Hl1 & Hl2 & H† & Hown)".
+    iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"=>//.
+    (* TODO: We should consider changing the statement of
+       bor_create to dis-entangle the two masks such that this is no
+      longer necessary. *)
+    iApply fupd_trans. iApply (fupd_mask_mono (↑lftN))=>//.
+    iMod (bor_create _ ν with "LFT Hown") as "[HP HPend]"=>//. iModIntro.
+    iMod (ty_share with "LFT HP Hν") as "[#? Hν]"; first solve_ndisj.
+    iMod (create_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN with "Hl1 Hl2 Hν")
+      as (γ q') "(#? & ? & ?)".
+    iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H".
+    iMod (inv_alloc arc_endN _ ([†ν] ∨ _)%I with "[H]") as "#INV";
+      first by iRight; iApply "H". iIntros "!> !# Hν".
+    iMod (inv_open with "INV") as "[[H†|[$ Hvs]] Hclose]";
+      [set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
+    rewrite difference_union_distr_l_L difference_diag_L right_id_L
+            difference_disjoint_L; last solve_ndisj.
+    iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
+    iMod "H" as "#Hν". iMod ("Hvs" with "Hν") as "$". iIntros "{$Hν} !>".
+    iApply "Hclose". auto.
+  Qed.
+
+  Program Definition arc (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] => full_arc_own l ty tid ∨ shared_arc_own l ty tid
+         | _ => False end;
+       ty_shr κ tid l :=
+         ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
+                arc_persist tid ν γ l' ty ∗
+                &shr{κ, arc_shrN}(arc_tok γ q')
+    |}%I.
+  Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+    (* Ideally, we'd change ty_shr to say "l ↦{q} #l" in the fractured borrow,
+       but that would be additional work here... *)
+    iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
+    destruct vl as [|[[|l'|]|][|]];
+      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+    setoid_rewrite heap_mapsto_vec_singleton.
+    iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
+    iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
+    set (C := (∃ _ _ _, _ ∗ _ ∗ &shr{_,_} _)%I).
+    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
+          with "[Hpbown]") as "#Hinv"; first by iLeft.
+    iIntros "!> !# * % Htok".
+    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iDestruct "INV" as "[>Hbtok|#Hshr]".
+    - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
+      { rewrite bor_unfold_idx. iExists _. by iFrame. }
+      iClear "H↦ Hinv Hpb".
+      iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
+      iModIntro. iNext. iAssert (shared_arc_own l' ty tid)%I with "[>HP]" as "HX".
+      { iDestruct "HP" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
+      iDestruct "HX" as (γ ν q') "[#Hpersist H]".
+      iMod ("Hclose2" with "[] H") as "[HX $]"; first by unfold shared_arc_own; auto 10.
+      iAssert C with "[>HX]" as "#$".
+      { iExists _, _, _. iFrame "Hpersist".
+        iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
+        iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
+        { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
+        iApply (bor_share with "Hrc"); solve_ndisj. }
+      iApply ("Hclose1" with "[]"). by auto.
+    - iMod ("Hclose1" with "[]") as "_"; first by auto.
+      iApply step_fupd_intro; first solve_ndisj. by iFrame.
+  Qed.
+  Next Obligation.
+    iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
+    iExists _. iSplit; first by iApply frac_bor_shorten.
+    iAlways. iIntros (F q) "% Htok".
+    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
+    iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
+    iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν ?) "(? & ? & ?)".
+    iExists _, _, _. iModIntro. iFrame. iSplit.
+    - by iApply lft_incl_trans.
+    - by iApply shr_bor_shorten.
+  Qed.
+
+  Global Instance arc_wf ty `{!TyWf ty} : TyWf (arc ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Global Instance arc_type_contractive : TypeContractive arc.
+  Proof.
+    constructor=>/=; unfold arc, full_arc_own, shared_arc_own;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+                                       f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance arc_ne : NonExpansive arc.
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Lemma arc_subtype ty1 ty2 :
+    type_incl ty1 ty2 -∗ type_incl (arc ty1) (arc ty2).
+  Proof.
+    iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
+    iSplit; first done. iSplit; iAlways.
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+      iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
+      { iLeft. iFrame. iDestruct "Hsz" as %->.
+        iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
+      iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
+      iRight. iExists _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
+    - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
+      iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+      iModIntro. iNext. iMod "H" as "[$ H]".
+      iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
+      iExists _, _, _. iFrame. by iApply arc_persist_type_incl.
+  Qed.
+
+  Global Instance arc_mono E L :
+    Proper (subtype E L ==> subtype E L) arc.
+  Proof.
+    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros "!# #HE". iApply arc_subtype. by iApply "Hsub".
+  Qed.
+  Global Instance arc_proper E L :
+    Proper (eqtype E L ==> eqtype E L) arc.
+  Proof. intros ??[]. by split; apply arc_mono. Qed.
+
+  Global Instance arc_send ty :
+    Send ty → Sync ty → Send (arc ty).
+  Proof.
+    intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
+    unfold full_arc_own, shared_arc_own.
+    repeat (apply send_change_tid || apply uPred.exist_mono ||
+            (apply arc_persist_send; apply _) || f_equiv || intros ?).
+  Qed.
+
+  Global Instance arc_sync ty :
+    Send ty → Sync ty → Sync (arc ty).
+  Proof.
+    intros Hse Hsy ν tid tid' l.
+    repeat (apply send_change_tid || apply uPred.exist_mono ||
+            (apply arc_persist_send; apply _) || f_equiv || intros ?).
+  Qed.
+
+  (* Model of weak *)
+  Program Definition weak (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] => ∃ γ ν, arc_persist tid ν γ l ty ∗ weak_tok γ
+         | _ => False end;
+       ty_shr κ tid l :=
+         ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν,
+                arc_persist tid ν γ l' ty ∗ &shr{κ, arc_shrN}(weak_tok γ)
+    |}%I.
+  Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+    (* Ideally, we'd change ty_shr to say "l ↦{q} #l" in the fractured borrow,
+       but that would be additional work here... *)
+    iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
+    destruct vl as [|[[|l'|]|][|]];
+      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+    setoid_rewrite heap_mapsto_vec_singleton.
+    iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
+    iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
+    set (C := (∃ _ _, _ ∗ &shr{_,_} _)%I).
+    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
+          with "[Hpbown]") as "#Hinv"; first by iLeft.
+    iIntros "!> !# * % Htok".
+    iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
+    iDestruct "INV" as "[>Hbtok|#Hshr]".
+    - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
+      { rewrite bor_unfold_idx. iExists _. by iFrame. }
+      iClear "H↦ Hinv Hpb".
+      iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
+      iDestruct "HP" as (γ ν) "[#Hpersist H]".
+      iMod ("Hclose2" with "[] H") as "[HX $]"; first by auto 10.
+      iModIntro. iNext. iAssert C with "[>HX]" as "#$".
+      { iExists _, _. iFrame "Hpersist". iApply bor_share; solve_ndisj. }
+      iApply ("Hclose1" with "[]"). by auto.
+    - iMod ("Hclose1" with "[]") as "_"; first by auto.
+      iApply step_fupd_intro; first solve_ndisj. by iFrame.
+  Qed.
+  Next Obligation.
+    iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
+    iExists _. iSplit; first by iApply frac_bor_shorten.
+    iAlways. iIntros (F q) "% Htok".
+    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
+    iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
+    iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν) "[??]".
+    iExists _, _. iModIntro. iFrame. by iApply shr_bor_shorten.
+  Qed.
+
+  Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Global Instance weak_type_contractive : TypeContractive weak.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+                                       f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance weak_ne : NonExpansive weak.
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Lemma weak_subtype ty1 ty2 :
+    type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
+  Proof.
+    iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
+    iSplit; first done. iSplit; iAlways.
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+      iDestruct "Hvl" as (γ ν) "(#Hpersist & Htk)".
+      iExists _, _. iFrame "#∗". by iApply arc_persist_type_incl.
+    - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
+      iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+      iModIntro. iNext. iMod "H" as "[$ H]". iDestruct "H" as (γ ν) "[Hpersist Hna]".
+      iExists _, _. iFrame. by iApply arc_persist_type_incl.
+  Qed.
+
+  Global Instance weak_mono E L :
+    Proper (subtype E L ==> subtype E L) weak.
+  Proof.
+    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros "!# #HE". iApply weak_subtype. by iApply "Hsub".
+  Qed.
+  Global Instance weak_proper E L :
+    Proper (eqtype E L ==> eqtype E L) weak.
+  Proof. intros ??[]. by split; apply weak_mono. Qed.
+
+  Global Instance weak_send ty :
+    Send ty → Sync ty → Send (weak ty).
+  Proof.
+    intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
+    repeat (apply send_change_tid || apply uPred.exist_mono ||
+            (apply arc_persist_send; apply _) || f_equiv || intros ?).
+  Qed.
+
+  Global Instance weak_sync ty :
+    Send ty → Sync ty → Sync (weak ty).
+  Proof.
+    intros Hse Hsy ν tid tid' l.
+    repeat (apply send_change_tid || apply uPred.exist_mono ||
+            (apply arc_persist_send; apply _) || f_equiv || intros ?).
+  Qed.
+
+  (* Code : constructors *)
+  Definition arc_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+      let: "arc" := new [ #1 ] in
+      "arcbox" +â‚— #0 <- #1;;
+      "arcbox" +â‚— #1 <- #1;;
+      "arcbox" +â‚— #2 <-{ty.(ty_size)} !"x";;
+      "arc" <- "arcbox";;
+      delete [ #ty.(ty_size); "x"];; return: ["arc"].
+
+  Lemma arc_new_type ty `{!TyWf ty} :
+    typed_val (arc_new ty) (fn(∅; ty) → arc ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
+    rewrite !tctx_hasty_val.
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
+    iDestruct (ownptr_uninit_own with "Hrcbox")
+      as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    rewrite shift_loc_assoc.
+    iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
+    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+    (* All right, we are done preparing our context. Let's get going. *)
+    wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
+    wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+    wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using vec_to_list_length..|].
+    iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write.
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (arc ty)]
+        with "[] LFT HE Hna HL Hk [>-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+      iSplitL "Hx↦"; first by iExists _; rewrite ->uninit_own; auto.
+      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iLeft.
+      rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition weak_new ty : val :=
+    funrec: <> [] :=
+      let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+      let: "w" := new [ #1 ] in
+      "arcbox" +â‚— #0 <- #0;;
+      "arcbox" +â‚— #1 <- #1;;
+      "w" <- "arcbox";;
+      return: ["w"].
+
+  Lemma weak_new_type ty `{!TyWf ty} :
+    typed_val (weak_new ty) (fn(∅) → weak ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox _]]". rewrite !tctx_hasty_val.
+    iDestruct (ownptr_uninit_own with "Hrcbox")
+      as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    rewrite shift_loc_assoc.
+    iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
+    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
+    wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
+    iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [solve_ndisj..|].
+    wp_op. iIntros "#H† !>". rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_write.
+    iApply (type_type _ _ _ [ #lrc ◁ box (weak ty)]
+            with "[] LFT HE Hna HL Hk [>-]"); last first.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
+      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
+            with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
+      { rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
+        by rewrite vec_to_list_length. }
+      iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!# Hν".
+      iDestruct (lft_tok_dead with "Hν H†") as "[]". }
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Code : deref *)
+  Definition arc_deref : val :=
+    funrec: <> ["arc"] :=
+      let: "x" := new [ #1 ] in
+      let: "arc'" := !"arc" in
+      "x" <- (!"arc'" +â‚— #2);;
+      delete [ #1; "arc" ];; return: ["x"].
+
+  Lemma arc_deref_type ty `{!TyWf ty} :
+    typed_val arc_deref (fn(∀ α, ∅; &shr{α} arc ty) → &shr{α} ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
+    rewrite !tctx_hasty_val [[rcx]]lock.
+    iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
+    subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
+    destruct rc' as [[|rc'|]|]; try done. simpl of_val.
+    iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+    wp_bind (!_)%E.
+    iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_step_fupd with "Hdelay"); [done..|].
+    iMod (frac_bor_acc with "LFT Hrc' Hα2") as (q') "[Hrc'↦ Hclose2]"; first solve_ndisj.
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose2" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 #Hproto] !>".
+    iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & _)".
+    iDestruct "Hpersist" as "(_ & [Hshr|Hν†] & _)"; last first.
+    { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†". done.
+      iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
+    wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} arc ty); #lrc2 ◁ box (&shr{α} ty)]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      iFrame "Hx". by iApply ty_shr_mono. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Code : clone, [up/down]grade. *)
+  Definition arc_clone : val :=
+    funrec: <> ["arc"] :=
+      let: "r" := new [ #1 ] in
+      let: "arc'" := !"arc" in
+      let: "arc''" := !"arc'" in
+      clone_arc ["arc''"];;
+      "r" <- "arc''";;
+      delete [ #1; "arc" ];; return: ["r"].
+
+  Lemma arc_clone_type ty `{!TyWf ty} :
+    typed_val arc_clone (fn(∀ α, ∅; &shr{α} arc ty) → arc ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+      [solve_typing..|]. wp_bind (!_)%E.
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+    iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
+    iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
+    wp_apply (clone_arc_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
+       with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
+    { iIntros "!# Hα".
+      iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
+    iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ arc ty; r ◁ box (uninit 1)]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. simpl. unfold shared_arc_own. auto 10 with iFrame. }
+    iApply type_assign; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition weak_clone : val :=
+    funrec: <> ["w"] :=
+      let: "r" := new [ #1 ] in
+      let: "w'" := !"w" in
+      let: "w''" := !"w'" in
+      clone_weak ["w''"];;
+      "r" <- "w''";;
+      delete [ #1; "w" ];; return: ["r"].
+
+  Lemma weak_clone_type ty `{!TyWf ty} :
+    typed_val weak_clone (fn(∀ α, ∅; &shr{α} weak ty) → weak ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+      [solve_typing..|]. wp_bind (!_)%E.
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+    iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
+    iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
+    wp_apply (clone_weak_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
+       with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
+    { iIntros "!# Hα".
+      iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
+      iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
+    iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. simpl. eauto 10 with iFrame. }
+    iApply type_assign; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition downgrade : val :=
+    funrec: <> ["arc"] :=
+      let: "r" := new [ #1 ] in
+      let: "arc'" := !"arc" in
+      let: "arc''" := !"arc'" in
+      downgrade ["arc''"];;
+      "r" <- "arc''";;
+      delete [ #1; "arc" ];; return: ["r"].
+
+  Lemma downgrade_type ty `{!TyWf ty} :
+    typed_val downgrade (fn(∀ α, ∅; &shr{α} arc ty) → weak ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+      [solve_typing..|]. wp_bind (!_)%E.
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+    iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
+    iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
+    wp_apply (downgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
+              with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
+    { iIntros "!# Hα".
+      iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
+    iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame. simpl. eauto 10 with iFrame. }
+    iApply type_assign; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition upgrade : val :=
+    funrec: <> ["w"] :=
+      let: "r" := new [ #2 ] in
+      let: "w'" := !"w" in
+      let: "w''" := !"w'" in
+      if: upgrade ["w''"] then
+        "r" <-{Σ some} "w''";;
+        delete [ #1; "w" ];; return: ["r"]
+      else
+        "r" <-{Σ none} ();;
+        delete [ #1; "w" ];; return: ["r"].
+
+  Lemma upgrade_type ty `{!TyWf ty} :
+    typed_val upgrade (fn(∀ α, ∅; &shr{α} weak ty) → option (arc ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+      [solve_typing..|]. wp_bind (!_)%E.
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
+    iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". clear q'. iIntros "!> [Hα1 Hproto]".
+    iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
+    wp_apply (upgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
+              with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
+    { iIntros "!# Hα".
+      iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
+      iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
+    iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
+    - (* Finish up the proof (sucess). *)
+      iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ arc ty;
+                                r ◁ box (uninit 2) ]
+              with "[] LFT HE Hna HL Hk [-]"); last first.
+      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+        unlock. iFrame. simpl. unfold shared_arc_own. eauto 10 with iFrame. }
+      iApply (type_sum_assign (option (arc ty))); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+    - (* Finish up the proof (fail). *)
+      iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); r ◁ box (uninit 2) ]
+              with "[] LFT HE Hna HL Hk [-]"); last first.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+        unlock. iFrame. }
+      iApply (type_sum_unit (option (arc ty))); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+
+  (* Code : drop *)
+  Definition arc_drop ty : val :=
+    funrec: <> ["arc"] :=
+      let: "r" := new [ #(option ty).(ty_size) ] in
+      let: "arc'" := !"arc" in
+      "r" <-{Σ none} ();;
+      drop_arc ["arc'";
+                λ: [], "r" <-{ty.(ty_size),Σ some} !("arc'" +ₗ #2);
+                λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+      delete [ #1; "arc"];; return: ["r"].
+
+  Lemma arc_drop_type ty `{!TyWf ty} :
+    typed_val (arc_drop ty) (fn(∅; arc ty) → option ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iApply (type_sum_unit (option ty)); [solve_typing..|].
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hr [Hrcx [Hrc' _]]]".
+    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
+    { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
+    iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
+    wp_bind (drop_arc _). erewrite <-2!(of_to_val (λ: [], _)%E); [|solve_to_val..].
+    iApply (drop_arc_spec with "[] [] [] [Hν Hr Htok]");
+      [by iDestruct "Hpersist" as "[$?]"| | |by iSplitL "Hr"; [iApply "Hr"|iFrame]|].
+    { iIntros "/= !# * [Hr Hν] HΦ". unlock. destruct r as [[]|]=>//=. wp_lam.
+      iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
+        first by iDestruct "Hown" as (???) "[% ?]".
+      rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
+      iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
+      iSpecialize ("H†" with "Hν").
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); try solve_ndisj.
+      iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
+      wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
+      iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
+      iDestruct "Hlen" as %[= ?]. iApply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
+      iNext. iIntros "[? Hrc']". iApply "HΦ". iFrame. iSplitR "Hrc'"; last by eauto.
+      iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iExists 1%nat, _, [].
+      iFrame. rewrite app_nil_r. iSplit; first by auto. rewrite /= Max.max_0_r. auto. }
+    { iIntros "/= !# * [Hr [H↦0 [H↦1 [H† H]]]] HΦ". wp_lam.
+      iDestruct "H" as (vl) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
+      iApply (wp_delete _ _ _ (_::_::vl) with "[H↦0 H↦1 H↦ H†]");
+        [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
+    iIntros "!> Hr". wp_seq.
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (option ty) ]
+            with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
+      by rewrite tctx_hasty_val. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition weak_drop ty : val :=
+    funrec: <> ["arc"] :=
+      let: "r" := new [ #0] in
+      let: "arc'" := !"arc" in
+      drop_weak ["arc'"; λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+      delete [ #1; "arc"];; return: ["r"].
+
+  Lemma weak_drop_type ty `{!TyWf ty} :
+    typed_val (weak_drop ty) (fn(∅; weak ty) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    iApply (type_new 0); [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
+    erewrite <-(of_to_val (λ: [], _)%E); [|solve_to_val..].
+    iApply (drop_weak_spec _ _ _ _ _ _ True with "[] [] [Htok]");
+      [by iDestruct "Hpersist" as "[$?]"| |by auto|].
+    { iIntros "/= !# * [_ [H↦0 [H↦1 [H† H]]]] HΦ". wp_lam.
+      iDestruct "H" as (vl) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
+      iApply (wp_delete _ _ _ (_::_::vl) with "[H↦0 H↦1 H↦ H†]");
+        [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
+    iIntros "!> _". wp_seq.
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box unit ]
+            with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
+      by rewrite tctx_hasty_val. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Code : other primitives *)
+  Definition arc_try_unwrap ty : val :=
+    funrec: <> ["arc"] :=
+      let: "r" := new [ #(Σ[ ty; arc ty ]).(ty_size) ] in
+      let: "arc'" := !"arc" in
+      if: try_unwrap ["arc'"] then
+        (* Return content *)
+        "r" <-{ty.(ty_size),Σ 0} !("arc'" +ₗ #2);;
+        (* Decrement the "strong weak reference" *)
+        drop_weak ["arc'"; λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+        delete [ #1; "arc"];; return: ["r"]
+      else
+        "r" <-{Σ 1} "arc'";;
+        delete [ #1; "arc"];; return: ["r"].
+
+  Lemma arc_try_unwrap_type ty `{!TyWf ty} :
+    typed_val (arc_try_unwrap ty) (fn(∅; arc ty) → Σ[ ty; arc ty ]).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    iApply (type_new (Σ[ ty; arc ty ]).(ty_size));
+      [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
+    { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
+    iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
+    wp_apply (try_unwrap_spec with "[] [Hν Htok]");
+      [by iDestruct "Hpersist" as "[$?]"|iFrame|].
+    iIntros ([]) "H"; wp_if.
+    - iDestruct "H" as "[Hν Hend]". rewrite -(lock [r]). destruct r as [[|r|]|]=>//=.
+      iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
+      rewrite uninit_own. iDestruct "Hown" as ">Hlen".
+      destruct vl0 as [|? vl0]=>//; iDestruct "Hlen" as %[=Hlen0].
+      rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
+      iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
+      iSpecialize ("H†" with "Hν").
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); try solve_ndisj.
+      wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
+      rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
+      iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
+      iDestruct (ty_size_eq with "Hown") as %Hlen.
+      iApply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite ?firstn_length_le; try lia.
+      iIntros "!> [Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
+      iMod ("Hend" with "[$H† Hrc']") as "Htok"; first by eauto.
+      erewrite <-(of_to_val (λ: [], _)%E); [|solve_to_val..].
+      iApply (drop_weak_spec _ _ _ _ _ _ True with "Ha [] [Htok]"); [|by auto|].
+      { iIntros "/= !# * [_ [H↦0 [H↦1 [H† H]]]] HΦ". wp_lam.
+        iDestruct "H" as (vl1) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
+        iApply (wp_delete _ _ _ (_::_::vl1) with "[H↦0 H↦1 H↦ H†]");
+          [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
+        rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
+      iIntros "!> _". wp_seq.
+      iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #r ◁ box (Σ[ ty; arc ty ]) ]
+              with "[] LFT HE Hna HL Hk [-]"); last first.
+      { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+        iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
+        rewrite -[in shift_loc _ ty.(ty_size)]Hlen -heap_mapsto_vec_app
+                -heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+        iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
+        rewrite app_length drop_length. lia. }
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+    - iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #rc' ◁ arc ty;
+                                r ◁ box (uninit (Σ[ ty; arc ty ]).(ty_size)) ]
+              with "[] LFT HE Hna HL Hk [-]"); last first.
+      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+        unlock. iFrame. iRight. iExists _, _, _. auto with iFrame. }
+      iApply (type_sum_assign Σ[ ty; arc ty ]); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+End arc.
\ No newline at end of file
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 5f0f0056..25ba131d 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -8,6 +8,8 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing option.
 Set Default Proof Using "Type".
 
+(* TODO : weak_count strong_count *)
+
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
 Class rcG Σ :=
-- 
GitLab