diff --git a/_CoqProject b/_CoqProject
index 7ca49608cbe4c27225e61bf699fe63c55955476f..9d4134e7cbc428bd8b0b0a20cc61cf615ef8e347 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -51,3 +51,9 @@ theories/typing/lib/swap.v
 theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
+theories/typing/lib/refcell/refcell_code.v
+theories/typing/lib/refcell/refcell.v
+theories/typing/lib/refcell/ref_code.v
+theories/typing/lib/refcell/refmut_code.v
+theories/typing/lib/refcell/refmut.v
+theories/typing/lib/refcell/ref.v
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
new file mode 100644
index 0000000000000000000000000000000000000000..10ad4c8781cb0c17043f41a806dcc686825e7a80
--- /dev/null
+++ b/theories/typing/lib/refcell/ref.v
@@ -0,0 +1,114 @@
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.lib.refcell Require Import refcell.
+Set Default Proof Using "Type".
+
+Definition refcell_refN := refcellN .@ "ref".
+
+Section ref.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct Ref<'b, T: ?Sized + 'b> {
+       value: &'b T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+  *)
+
+  Program Definition ref (α : lft) (ty : type) :=
+    {| ty_size := 2;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
+           ∃ ν q γ β ty', ty.(ty_shr) (α ⊓ ν) tid lv ∗
+             α ⊑ β ∗ &na{β, tid.(tid_na_inv_pool), refcell_invN}(refcell_inv tid lrc γ β ty') ∗
+             q.[ν] ∗ ⎡own γ (◯ reading_st q ν)⎤
+         | _ => False
+         end;
+       ty_shr κ tid l :=
+          ∃ ν q γ β ty' (lv lrc : loc),
+             κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
+             ▷ ty.(ty_shr) (α ⊓ ν) tid lv ∗
+             ▷ (α ⊑ β) ∗ ▷ &na{β, tid.(tid_na_inv_pool), refcell_invN}(refcell_inv tid lrc γ β ty') ∗
+             &na{κ, tid.(tid_na_inv_pool), refcell_refN}⎡own γ (◯ reading_st q ν)⎤ |}%I.
+  Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
+    iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+    destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
+    iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
+    iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
+    iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
+    iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
+    iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
+    iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
+    iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
+    iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
+    { iApply bor_fracture; try done. split. by rewrite Qp_mult_1_r. apply _. }
+    iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
+    iExists _, _, _, _, _, _, _. iDestruct "H" as "#(? & ? & $ & $ & $ & ?)".
+    iSplit; last iSplit.
+    - by iApply lft_incl_trans.
+    - by iApply frac_bor_shorten.
+    - by iApply na_bor_shorten.
+  Qed.
+
+  Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+  Global Instance ref_type_contractive α : TypeContractive (ref α).
+  Proof. solve_type_proper. Qed.
+  Global Instance ref_ne α : NonExpansive (ref α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance ref_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
+  Proof.
+    iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    - done.
+    - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
+      iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
+      iExists ν, q', γ, β, ty'. iFrame "∗#". iSplit.
+      + iApply ty_shr_mono; last by iApply "Hs".
+        iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      + by iApply lft_incl_trans.
+    - iIntros (κ tid l) "H". iDestruct "H" as (ν q' γ β ty' lv lrc) "H".
+      iExists ν, q', γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
+      + iApply ty_shr_mono; last by iApply "Hs".
+        iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      + by iApply lft_incl_trans.
+  Qed.
+  Global Instance ref_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) ref.
+  Proof. intros ??????. by apply ref_mono. Qed.
+  Lemma ref_mono' E L α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → subtype E L ty1 ty2 →
+    subtype E L (ref α1 ty1) (ref α2 ty2).
+  Proof. intros. by eapply ref_mono. Qed.
+  Global Instance ref_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) ref.
+  Proof. intros ??[]?? EQ. split; apply ref_mono'; try done; apply EQ. Qed.
+  Lemma ref_proper' E L α1 α2 ty1 ty2 :
+    lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
+    eqtype E L (ref α1 ty1) (ref α2 ty2).
+  Proof. intros. by eapply ref_proper. Qed.
+End ref.
+
+Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..bf2ea78c865c279f84efdf1cbbbe14d669207c37
--- /dev/null
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -0,0 +1,266 @@
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import lifetime na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.lib.refcell Require Import refcell ref.
+Set Default Proof Using "Type".
+
+Section ref_functions.
+  Context `{typeG Σ, refcellG Σ}.
+
+  Lemma refcell_inv_reading_inv tid l γ α ty q ν :
+    refcell_inv tid l γ α ty -∗
+    ⎡own γ (◯ reading_st q ν)⎤ -∗
+    ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
+            ⎡own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν)⎤ ∗
+            ty.(ty_shr) (α ⊓ ν) tid (l >> 1) ∗
+            ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l >> 1) ↦∗: ty_own ty tid)) ∗
+            ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
+  Proof.
+    iIntros "INV H◯".
+    iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
+    iAssert (∃ q' n, st ≡ Some (to_agree ν, Cinr (q', n)) ∗ ⌜q ≤ q'⌝%Qc)%I with
+       "[#]" as (q' n) "[Hst %]".
+    { iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
+       (? & [agν st'] & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
+      - iExists q, xH. iSplit; iPureIntro. by constructor. done.
+      - iClear "∗#".
+        revert Hle Hv=>/prod_included [/= /agree_included Hag /csum_included
+              [-> [//] | [[?[?[//]]] | [?[[q' n] [Heq [-> Hle]]]]]]] [Hagok _].
+        revert Heq. intros [= <-]. revert Hle=>/prod_included [/= Hqq' _].
+        iExists q', n. iSplit.
+        + iPureIntro. rewrite (agree_op_inv agν) //. by rewrite comm -Hag.
+        + by revert Hqq'=>/frac_included_weak. }
+    iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
+    destruct st' as [?[|[]|]]; destruct Hst' as [Hag Hst']; try by inversion Hst'.
+    apply (inj Cinr), (inj2 pair) in Hst'.
+    destruct Hst' as [<-%leibniz_equiv <-%leibniz_equiv]. simpl in *.
+    setoid_rewrite <-Hag. iDestruct "INV" as (ν') "(Hag & Hν & Hshr & Hq')".
+    iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
+    iExists q', n. rewrite own_op. by iFrame.
+  Qed.
+
+  (* Cloning a ref. We need to increment the counter. *)
+  Definition ref_clone : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "rc" := !("x'" +ₗ #1) in
+      let: "n" := !"rc" in
+      "rc" <- "n" + #1;;
+      letalloc: "r" <-{2} !"x'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  (* FIXME : using λ instead of fun triggers an anomaly.
+     See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
+  Lemma ref_clone_type ty `{!TyWf ty} :
+    typed_val ref_clone (fn (fun '(α, β) =>
+                FP_wf ∅ [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
+    wp_op.
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
+    iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
+      [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+    iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
+    iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
+    rewrite {1}own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
+    iDestruct (refcell_inv_reading_inv with "INV H◯")
+      as (q' n) "(H↦lrc & _ & [H● H◯] & Hshr' & H† & Hq')".
+    wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
+    iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
+    { apply auth_update_alloc,
+         (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
+      split; [|split; last done].
+      - by rewrite /= agree_idemp.
+      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+        apply Qcplus_le_mono_r, Qp_ge_0. }
+    wp_apply wp_new; [done..|]. iIntros (lr) "(H†lr&Hlr)".
+    iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
+    { rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
+    wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
+    iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
+    iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
+    { iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
+      - rewrite /= agree_idemp. auto.
+      - iExists _. iFrame.
+        rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+    iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
+    iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
+    iApply (type_type _ _ _
+           [ x ◁ box (&shr{α}(ref β ty)); #lr ◁ box(ref β ty)]
+        with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      rewrite /= freeable_sz_full. iFrame. iSplitR "H†lr".
+      - iExists _. iFrame. iExists _, _, _, _, _. iFrame "∗#".
+      - iDestruct "H†lr" as "[?|%]". by iLeft. by iRight. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Turning a ref into a shared borrow. *)
+  Definition ref_deref : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma ref_deref_type ty `{!TyWf ty} :
+    typed_val ref_deref
+      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+    rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
+    iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _
+        [ x ◁ box (&shr{α}(ref β ty)); #lv ◁ &shr{α}ty]
+        with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Dropping a ref and decrement the count in the corresponding refcell. *)
+  Definition ref_drop : val :=
+    funrec: <> ["x"] :=
+      let: "rc" := !("x" +ₗ #1) in
+      let: "n" := !"rc" in
+      "rc" <- "n" - #1;;
+      Endlft;;
+      delete [ #2; "x"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma ref_drop_type ty `{!TyWf ty} :
+    typed_val ref_drop (fn(∀ α, ∅; ref α ty) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
+    rewrite {1}own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
+    iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+    iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
+    iDestruct (refcell_inv_reading_inv with "INV [$H◯]")
+      as (q' n) "(H↦lrc & >% & H●◯ & Hshr & H† & Hq')". iDestruct "Hq'" as (q'') ">[% Hν']".
+    wp_read. wp_let. wp_op. wp_write.
+    iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I
+      with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
+    { iDestruct (own_valid with "H●◯") as %[[ _ [Heq%(inj Cinr)|Hincl%csum_included]
+        %Some_included]%Some_pair_included [_ Hv]]%auth_valid_discrete_2.
+      - destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
+        iExists None. iFrame. iMod (own_update with "H●◯") as "$".
+        { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
+          apply cancel_local_update_unit, _. }
+        iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
+      - destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
+        destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
+        iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "H↦lrc".
+        { destruct n'; [|done..]. by rewrite /= Pos.pred_double_succ. }
+        iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
+        { apply auth_update_dealloc.
+          rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
+          apply (cancel_local_update_unit (reading_st q ν)), _. }
+        iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
+        iSplitR; first done. iExists (q+q'')%Qp. iFrame.
+        by rewrite assoc (comm _ q0 q). }
+    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
+    iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
+    iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
+    iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk");
+      first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
+      rewrite own_loc_na_vec_cons own_loc_na_vec_singleton uninit_own. iFrame. auto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Apply a function within the ref, typically for accessing a component. *)
+  Definition ref_map (call_once : val) : val :=
+    funrec: <> ["ref"; "f"] :=
+      let: "call_once" := call_once in
+      let: "x'" := !"ref" in
+      letalloc: "x" <- "x'" in
+      letcall: "r" := "call_once" ["f"; "x"]%E in
+      let: "r'" := !"r" in delete [ #1; "r"];;
+      "ref" <- "r'";;
+      return: ["ref"].
+
+  Lemma ref_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
+    (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) →
+    typed_val (ref_map call_once) (fn(∀ α, ∅; ref α ty1, fty) → ref α ty2).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+    iDestruct "Href" as "[Href Href†]".
+    iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
+      try iDestruct "Href" as "[_ >[]]".
+    rewrite {1}own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
+    iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
+    wp_read. wp_let. wp_apply wp_new; try done.
+    iIntros (lx) "(H† & Hlx)". rewrite own_loc_na_vec_singleton.
+    wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
+    iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ lft_intersect).
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
+       with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
+    { rewrite bi.big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+      iSplitR "H†".
+      - iExists [_]. rewrite own_loc_na_vec_singleton. by iFrame.
+      - iDestruct "H†" as "[?|%]". by iLeft. by iRight. }
+    iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
+    iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
+    iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
+    iMod ("Hclose2" with "Hϝ HL") as "HL". iMod ("Hclose1" with "Hα HL") as "HL".
+    wp_rec. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as ([|r'[]]) "[Hr #Hr']";
+      try by iDestruct (ty_size_eq with "Hr'") as "%".
+    rewrite own_loc_na_vec_singleton. wp_read. wp_let.
+    wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
+    { rewrite own_loc_na_vec_singleton freeable_sz_full. iFrame.
+      iDestruct "Hr†" as "[?|%]". by iLeft. by iRight. }
+    iIntros "_". wp_seq. wp_write.
+    iApply (type_type _ [_] _ [ #lref ◁ box (ref α ty2) ]
+       with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame.
+      iExists [_;_]. rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+      iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
+    iApply type_jump; solve_typing.
+  Qed.
+End ref_functions.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
new file mode 100644
index 0000000000000000000000000000000000000000..5bdaeadac6729534d7c3f5f1f5a441cde268fb64
--- /dev/null
+++ b/theories/typing/lib/refcell/refcell.v
@@ -0,0 +1,204 @@
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Definition refcell_stR :=
+  optionUR (prodR (agreeR lftC) (csumR (exclR unitC) (prodR fracR positiveR))).
+Class refcellG Σ :=
+  RefCellG :> inG Σ (authR refcell_stR).
+Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
+Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
+Proof. solve_inG. Qed.
+
+Definition Z_of_refcell_st (st : refcell_stR) : Z :=
+  match st with
+  | None => 0
+  | Some (_, Cinr (_, n)) => Zpos n
+  | Some _ => -1
+  end.
+
+Definition reading_st (q : frac) (ν : lft) : refcell_stR :=
+  Some (to_agree ν, Cinr (q, xH)).
+Definition writing_st (ν : lft) : refcell_stR :=
+  Some (to_agree ν, Cinl (Excl ())).
+
+Definition refcellN := lrustN .@ "refcell".
+Definition refcell_invN := refcellN .@ "inv".
+
+Section refcell_inv.
+  Context `{typeG Σ, refcellG Σ}.
+
+  Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : vProp Σ :=
+    (∃ st, l ↦ #(Z_of_refcell_st st) ∗ ⎡own γ (● st)⎤ ∗
+      match st return _ with
+      | None =>
+        (* Not borrowed. *)
+        &{α}((l >> 1) ↦∗: ty.(ty_own) tid)
+      | Some (agν, st) =>
+        ∃ ν, agν ≡ to_agree ν ∗
+             (1.[ν] ={↑lftN,∅}▷=∗ &{α}((l >> 1) ↦∗: ty.(ty_own) tid)) ∗
+             match st with
+             | Cinr (q, n) =>
+               (* Immutably borrowed. *)
+               ty.(ty_shr) (α ⊓ ν) tid (l >> 1) ∗
+               ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
+             | _ => (* Mutably borrowed. *) True
+             end
+      end)%I.
+
+  Global Instance refcell_inv_type_ne n tid l γ α :
+    Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
+  Proof.
+    solve_proper_core
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
+  Proof.
+    intros n ???. (* TODO: f_equiv takes forever here, what is going on? *)
+    eapply refcell_inv_type_ne, type_dist_dist2. done.
+  Qed.
+
+  Lemma refcell_inv_proper E L ty1 ty2 q :
+    eqtype E L ty1 ty2 →
+    llctx_interp L q -∗ ∀ tid l γ α, □ (elctx_interp E -∗
+    refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2).
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic. *)
+  (*             It would easily gain from some automation. *)
+    rewrite eqtype_unfold. iIntros (Hty) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
+    iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
+    iAssert (□ (&{α}((l >> 1) ↦∗: ty_own ty1 tid) -∗
+                &{α}((l >> 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
+    { iIntros "!# H". iApply bor_iff; last done.
+      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iFrame; by iApply "Hown". }
+    iDestruct "H" as (st) "H"; iExists st;
+      iDestruct "H" as "($&$&H)"; destruct st as [[agν st]|]; try done;
+      last by iApply "Hb".
+    iDestruct "H" as (ν) "(Hag & Hh & H)". iExists ν. iFrame. iSplitL "Hh".
+    { iIntros "Hν". iMod ("Hh" with "Hν") as "Hh". iModIntro. iNext.
+      iMod "Hh". by iApply "Hb". }
+    destruct st as [|[]|]; try done. iDestruct "H" as "[H $]". by iApply "Hshr".
+  Qed.
+End refcell_inv.
+
+Section refcell.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* Original Rust type:
+     pub struct RefCell<T: ?Sized> {
+       borrow: Cell<BorrowFlag>,
+       value: UnsafeCell<T>,
+     }
+  *)
+
+  Program Definition refcell (ty : type) :=
+    {| ty_size := S ty.(ty_size);
+       ty_own tid vl :=
+         match vl return _ with
+         | #(LitInt z) :: vl' => ⌜-1 ≤ z⌝ ∗ ty.(ty_own) tid vl'
+         | _ => False
+         end%I;
+       ty_shr κ tid l :=
+         (∃ α γ, κ ⊑ α ∗
+            &na{α, tid.(tid_na_inv_pool), refcell_invN}(refcell_inv tid l γ α ty))%I |}.
+  Next Obligation.
+    iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
+    iIntros "[_ %] !% /=". congruence.
+  Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
+    iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+    iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
+    iDestruct "H" as "[>% Hown]".
+    iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
+            (l >> 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
+    { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
+      iDestruct "Hvl" as (vl') "[H↦ Hvl]".
+      iExists (#n'::vl'). rewrite own_loc_na_vec_cons. iFrame "∗%". }
+    { iNext. rewrite own_loc_na_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
+    iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
+    iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
+    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
+      as "[$ HQ]"; last first.
+    { iMod ("Hclose" with "[] HQ") as "[Hb $]".
+      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
+        iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
+      - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
+        iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
+    clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
+    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+    - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+      iMod (own_alloc (● Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
+      { by apply auth_auth_valid. }
+      iApply (fupd_mask_mono (↑lftN)); first done.
+      iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+      { iApply lft_intersect_incl_l. }
+      iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+      iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
+      iDestruct ("Hclose" with "Htok") as "[$ Htok]".
+      iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Hshr}".
+      iSplitR; first by auto. iSplitR "Htok2"; last first.
+      { iExists _. iFrame. rewrite Qp_div_2. auto. }
+      iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
+      iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
+    - iMod (own_alloc (● writing_st static)) as (γ) "Hst". { by apply auth_auth_valid. }
+      iFrame. iExists _, _. iFrame. iExists _. iSplitR; first by auto.
+      iIntros "!>!> _". iApply step_fupd_intro; [set_solver|auto].
+  Qed.
+  Next Obligation.
+    iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
+    iExists _, _. iFrame. iApply lft_incl_trans; auto.
+  Qed.
+
+  Global Instance refcell_wf ty `{!TyWf ty} : TyWf (refcell ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Global Instance refcell_type_ne : TypeNonExpansive refcell.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply refcell_inv_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance refcell_ne : NonExpansive refcell.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic.
+              It would easily gain from some automation. *)
+    iIntros (ty1 ty2 EQ qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
+    iDestruct (EQ' with "HL") as "#EQ'".
+    iDestruct (refcell_inv_proper with "HL") as "#Hty1ty2"; first done.
+    iDestruct (refcell_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
+    iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
+    iSplit; [|iSplit; iIntros "!# * H"].
+    - iPureIntro. simpl. congruence.
+    - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
+    - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
+      iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
+      by iApply "Hty1ty2". by iApply "Hty2ty1".
+  Qed.
+  Lemma refcell_mono' E L ty1 ty2 :
+    eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).
+  Proof. eapply refcell_mono. Qed.
+  Global Instance refcell_proper E L : Proper (eqtype E L ==> eqtype E L) refcell.
+  Proof. by split; apply refcell_mono. Qed.
+  Lemma refcell_proper' E L ty1 ty2 :
+    eqtype E L ty1 ty2 → eqtype E L (refcell ty1) (refcell ty2).
+  Proof. eapply refcell_proper. Qed.
+
+  Global Instance refcell_send :
+    Send ty → Send (refcell ty).
+  Proof. move=>????[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
+End refcell.
+
+Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..5d912160c2d021a29c7965c4643e14c82a0ee2ff
--- /dev/null
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -0,0 +1,308 @@
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing option.
+From lrust.typing.lib.refcell Require Import refcell ref refmut.
+Set Default Proof Using "Type".
+
+Section refcell_functions.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* Constructing a refcell. *)
+  Definition refcell_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #(S ty.(ty_size))] in
+      "r" +ₗ #0 <- #0;;
+      "r" +ₗ #1 <-{ty.(ty_size)} !"x";;
+      delete [ #ty.(ty_size) ; "x"];; return: ["r"].
+
+  Lemma refcell_new_type ty `{!TyWf ty} :
+    typed_val (refcell_new ty) (fn(∅; ty) → refcell ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
+    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hr Hx]".
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
+    iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
+    inv_vec vlr=>??. iDestruct (own_loc_na_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
+    rewrite shift_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
+    iIntros "[Hr↦1 Hx↦]". wp_seq.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+      iSplitL "Hx↦".
+      - iExists _. rewrite uninit_own. auto.
+      - iExists (_::_). rewrite own_loc_na_vec_cons. iFrame. simpl. iFrame. auto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* The other direction: getting ownership out of a refcell. *)
+  Definition refcell_into_inner ty : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #ty.(ty_size)] in
+      "r" <-{ty.(ty_size)} !("x" +ₗ #1);;
+          (* TODO: Can we make it so that the parenthesis above are mandatory?
+             Leaving them away is inconsistent with `let ... := !"x" +ₗ #1`. *)
+       delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
+
+  Lemma refcell_into_inner_type ty `{!TyWf ty} :
+    typed_val (refcell_into_inner ty) (fn(∅; refcell ty) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
+    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hr Hx]".
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
+    inv_vec vlx=>-[[|?|?]|????] vl; try iDestruct "Hx" as ">[]". simpl vec_to_list.
+    iDestruct "Hx" as "[>% Hx]".
+    iDestruct (own_loc_na_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
+    iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
+    wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
+    iIntros "[Hr↦ Hx↦1]". wp_seq.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+      iSplitR "Hr↦ Hx".
+      - iExists (_::_). rewrite own_loc_na_vec_cons uninit_own. iFrame.
+        rewrite /= vec_to_list_length. auto.
+      - iExists vl. iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition refcell_get_mut : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      "x" <- "x'" +ₗ #1;;
+      return: ["x"].
+
+  Lemma refcell_get_mut_type ty `{!TyWf ty} :
+    typed_val refcell_get_mut
+              (fn(∀ α, ∅; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL HC HT".
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
+    iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
+        (&uniq{α} ty).(ty_own) tid [ #(lx' >> 1)])%I with "[> Hx']" as "[_ Hx']".
+    { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
+      - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
+        iExists (_::_). rewrite own_loc_na_vec_cons. iFrame. iFrame.
+      - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try iDestruct "H" as "[]".
+        rewrite own_loc_na_vec_cons.
+        iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
+        iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
+    iApply (type_type _ _ _
+            [ #lx ◁ box (uninit 1); #(lx' >> 1) ◁ &uniq{α}ty]
+            with "[] LFT HE Hna HL HC [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+      iNext. iExists _. rewrite uninit_own. iFrame. }
+    iApply type_assign; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Shared borrowing. *)
+  Definition refcell_try_borrow : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #3 ] in
+    withcont: "k":
+      let: "x'" := !"x" in
+      let: "n" := !"x'" in
+      if: "n" ≤ #-1 then
+        "r" <-{Σ none} ();;
+        "k" []
+      else
+        "x'" <- "n" + #1;;
+        let: "ref" := new [ #2 ] in
+        "ref" <- "x'" +ₗ #1;;
+        "ref" +ₗ #1 <- "x'";;
+        "r" <-{2,Σ some} !"ref";;
+        delete [ #2; "ref"];;
+        "k" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma refcell_try_borrow_type ty `{!TyWf ty} :
+    typed_val refcell_try_borrow
+      (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (ref α ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
+                                         r ◁ box (option (ref α ty))]));
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing. }
+    iApply type_deref; [solve_typing..|].
+    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
+    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
+    iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
+    iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
+    - iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
+        first by iExists st; iFrame.
+      iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type _ _ _
+              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
+      simpl. iApply type_jump; solve_typing.
+    - wp_op. wp_write. wp_apply wp_new; [done..|].
+      iIntros (lref) "(H† & Hlref)". wp_let.
+      rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+      iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
+      iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
+                       ty_shr ty (β ⊓ ν) tid (lx >> 1) ∗
+                       ⎡own γ (◯ reading_st qν ν)⎤ ∗ refcell_inv tid lx γ β ty)%I
+        with "[> Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
+      { destruct st as [[agν [|[q n]|]]|]; try done.
+        - iDestruct "Hst" as (ν) "(Hag & H† & #Hshr & Hst)".
+          iDestruct "Hst" as (q') "(#Hqq' & [Hν1 Hν2])".
+          iExists _, _. iFrame "Hν1". iDestruct "Hag" as %Hag. iDestruct "Hqq'" as %Hqq'.
+          iMod (own_update with "Hownst") as "[Hownst ?]".
+          { apply auth_update_alloc,
+            (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
+            split; [|split].
+            - by rewrite /= -Hag agree_idemp.
+            - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+              apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
+              apply Qcplus_le_mono_r, Qp_ge_0.
+            - done. }
+          iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _. iFrame.
+          iSplitR; first by rewrite /= Hag agree_idemp. iFrame "Hshr". iExists _. iFrame.
+          rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
+        - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+          iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
+            auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
+          rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
+          iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+          iApply (fupd_mask_mono (↑lftN)); first done.
+          iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+          { iApply lft_intersect_incl_l. }
+          iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
+          iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
+          iExists _. iSplitR; first done. iFrame "Hshr". iSplitR "Htok2".
+          + iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
+            iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
+          + iExists _. iFrame. by rewrite Qp_div_2. }
+      iMod ("Hclose''" with "[$INV] Hna") as "[Hβtok1 Hna]".
+      iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type  _ _ _
+        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
+        rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
+        iSplitR "H†".
+        - iExists [_; _]. rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+          iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
+          iApply lft_intersect_mono. done. iApply lft_incl_refl.
+        - iDestruct "H†" as "[?|%]". by iLeft. by iRight. }
+      iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
+      simpl. iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+  Qed.
+
+  (* Unique borrowing. *)
+  Definition refcell_try_borrow_mut : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #3 ] in
+    withcont: "k":
+      let: "x'" := !"x" in
+      let: "n" := !"x'" in
+      if: "n" = #0 then
+        "x'" <- #(-1);;
+        let: "ref" := new [ #2 ] in
+        "ref" <- "x'" +ₗ #1;;
+        "ref" +ₗ #1 <- "x'";;
+        "r" <-{2,Σ some} !"ref";;
+        delete [ #2; "ref"];;
+        "k" []
+      else
+        "r" <-{Σ none} ();;
+        "k" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma refcell_try_borrow_mut_type ty `{!TyWf ty} :
+    typed_val refcell_try_borrow_mut
+              (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (refmut α ty))%T.
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
+                                            r ◁ box (option (refmut α ty))]));
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
+      simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing. }
+    iApply type_deref; [solve_typing..|].
+    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
+    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+    iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
+    iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
+    - wp_write. wp_apply wp_new; [done..|].
+      iIntros (lref) "(H† & Hlref)". wp_let.
+      rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+      iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
+      destruct st as [[?[|[]|]]|]; try done.
+      iMod (lft_create with "LFT") as (ν) "[Htok #Hhν]". done.
+      iMod (own_update with "Hownst") as "[Hownst ?]".
+      { by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
+      iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
+      iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+      { iApply lft_intersect_incl_l. }
+      iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
+      { iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
+        iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
+        iApply "Hbh". rewrite -lft_dead_or. auto. }
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type _ _ _
+        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
+        rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
+        iSplitR "H†".
+        - iExists [_; _]. rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+          iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
+          iApply lft_intersect_mono; first done. iApply lft_incl_refl.
+        - iDestruct "H†" as "[?|%]". by iLeft. by iRight. }
+      iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
+      simpl. iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing.
+    - iMod ("Hclose''" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
+        first by iExists st; iFrame.
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type _ _ _
+              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
+      simpl. iApply type_jump; solve_typing.
+  Qed.
+End refcell_functions.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
new file mode 100644
index 0000000000000000000000000000000000000000..bc84d27f37fa78a29039f487d083bcab68b9ff5b
--- /dev/null
+++ b/theories/typing/lib/refcell/refmut.v
@@ -0,0 +1,123 @@
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing util.
+From lrust.typing.lib.refcell Require Import refcell.
+Set Default Proof Using "Type".
+
+Section refmut.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct RefMut<'b, T: ?Sized + 'b> {
+       value: &'b mut T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+
+     In other words, we have a pointer to the data, and a pointer
+     to the refcount field of the RefCell. *)
+
+  Program Definition refmut (α : lft) (ty : type) :=
+    {| ty_size := 2;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
+           ∃ ν γ β ty', &{α ⊓ ν}(lv ↦∗: ty.(ty_own) tid) ∗
+             α ⊑ β ∗ &na{β, tid.(tid_na_inv_pool), refcell_invN}(refcell_inv tid lrc γ β ty') ∗
+             1.[ν] ∗ ⎡own γ (◯ writing_st ν)⎤
+         | _ => False
+         end;
+       ty_shr κ tid l :=
+         ∃ (lv lrc : loc),
+           &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ]
+             ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
+  Next Obligation.
+    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
+  Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
+    iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+    destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
+    iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
+    rewrite (assoc _ _ (α ⊑ β)%I). iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
+    rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
+    iMod (bor_sep with "LFT H") as "[_ H]". done.
+    unshelve (iMod (bor_fracture _ (λ q, (1 * q).[ν])%I with "LFT H") as "H"=>//).
+    { apply _. } { split. by rewrite Qp_mult_1_r. apply _. }
+    iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
+    iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+    iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
+    iApply lft_incl_glb; first done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
+    iExists _, _. iSplit.
+    - by iApply frac_bor_shorten.
+    - iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+  Qed.
+
+  Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+  Global Instance refmut_type_contractive α : TypeContractive (refmut α).
+  Proof. solve_type_proper. Qed.
+  Global Instance refmut_ne α : NonExpansive (refmut α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance refmut_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
+  Proof.
+    intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    - done.
+    - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
+      iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
+      iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+      + iApply bor_shorten; last iApply bor_iff; last done.
+        * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
+        * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+          iExists vl; iFrame; by iApply "Ho".
+      + by iApply lft_incl_trans.
+    - iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
+      iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      by iApply "Hs".
+  Qed.
+  Global Instance refmut_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) refmut.
+  Proof. intros ??????. by apply refmut_mono. Qed.
+  Lemma refmut_mono' E L α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    subtype E L (refmut α1 ty1) (refmut α2 ty2) .
+  Proof. intros. by eapply refmut_mono. Qed.
+  Global Instance refmut_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E  L) refmut.
+  Proof. intros ??[]???. split; by apply refmut_mono'. Qed.
+  Lemma refmut_proper' E L α1 α2 ty1 ty2 :
+    lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
+    eqtype E L (refmut α1 ty1) (refmut α2 ty2).
+  Proof. intros. by eapply refmut_proper. Qed.
+End refmut.
+
+Hint Resolve refmut_mono' refmut_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..6f340f025d84421a24a32e131a35eef8f6a111ef
--- /dev/null
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -0,0 +1,211 @@
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.lib.refcell Require Import refcell refmut.
+Set Default Proof Using "Type".
+
+Section refmut_functions.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* Turning a refmut into a shared borrow. *)
+  Definition refmut_deref : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma refmut_deref_type ty `{!TyWf ty} :
+    typed_val refmut_deref (fn (fun '(α, β) =>
+       FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
+      [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+    rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
+      [solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
+         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
+    iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
+    iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
+    iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(refmut β ty)); #lv ◁ &shr{α}ty]
+            with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (ty_shr_mono with "[] Hshr'").
+      by iApply lft_incl_glb; last iApply lft_incl_refl. }
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Turning a refmut into a unique borrow. *)
+  Definition refmut_derefmut : val := refmut_deref.
+
+  Lemma refmut_derefmut_type ty `{!TyWf ty} :
+    typed_val refmut_derefmut (fn (fun '(α, β) =>
+      FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
+   Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
+    iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
+      [solve_typing..|].
+    destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
+      try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
+    iMod (bor_exists with "LFT H") as (ν) "H". done.
+    iMod (bor_exists with "LFT H") as (γ) "H". done.
+    iMod (bor_exists with "LFT H") as (δ) "H". done.
+    iMod (bor_exists with "LFT H") as (ty') "H". done.
+    iMod (bor_sep with "LFT H") as "[Hb H]". done.
+    iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
+    iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
+    rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
+    iMod (bor_sep with "LFT H") as "[_ H]". done.
+    unshelve (iMod (bor_fracture _ (λ q, (1 * q).[ν])%I with "LFT H") as "H"=>//).
+    { apply _. } { split. by rewrite Qp_mult_1_l. apply _. } { done. }
+    iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hαν". iClear "H".
+    rewrite own_loc_na_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
+    iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+    wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
+    wp_read. wp_let. iMod "Hb".
+    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]
+            with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (bor_shorten with "[] Hb").
+      by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
+    iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
+  Definition refmut_drop : val :=
+    funrec: <> ["x"] :=
+      let: "rc" := !("x" +ₗ #1) in
+      "rc" <- #0;;
+      Endlft;;
+      delete [ #2; "x"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma refmut_drop_type ty `{!TyWf ty} :
+    typed_val refmut_drop (fn(∀ α, ∅; refmut α ty) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
+    rewrite {1}own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
+    iDestruct "Hx" as (ν γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
+      [solve_typing..|].
+    iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+    iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
+    iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_write.
+    iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & [agν st'] & [=<-] & -> &
+      [[Hag Heq]|[_ Hle]%prod_included])]%option_included []]%auth_valid_discrete_2;
+      last first.
+    { by destruct (exclusive_included (Cinl (Excl ())) st'). }
+    setoid_subst. iDestruct "INV" as (ν') "(Hνν' & H† & _)".
+    iDestruct "Hνν'" as %<-%(inj to_agree)%leibniz_equiv.
+    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
+    iApply (wp_step_fupd with "[H† Hν]");
+      [done| |iApply ("H†" with "Hν")|]; first set_solver.
+    wp_seq. iIntros "{Hb} Hb !>".
+    iMod ("Hcloseβ" with "[> H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
+    { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
+      apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
+      apply cancel_local_update_unit, _. }
+    iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
+            with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
+      rewrite own_loc_na_vec_cons own_loc_na_vec_singleton uninit_own. iFrame. auto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Apply a function within the refmut, typically for accessing a component. *)
+  Definition refmut_map (call_once : val) : val :=
+    funrec: <> ["ref"; "f"] :=
+      let: "call_once" := call_once in
+      let: "x'" := !"ref" in
+      letalloc: "x" <- "x'" in
+      letcall: "r" := "call_once" ["f"; "x"]%E in
+      let: "r'" := !"r" in delete [ #1; "r"];;
+      "ref" <- "r'";;
+      return: ["ref"].
+
+  Lemma refmut_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
+    (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) →
+    typed_val (refmut_map call_once) (fn(∀ α, ∅; refmut α ty1, fty) → refmut α ty2).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+    iDestruct "Href" as "[Href Href†]".
+    iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
+      try iDestruct "Href" as "[_ >[]]".
+    rewrite {1}own_loc_na_vec_cons own_loc_na_vec_singleton.
+    iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
+    iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
+    wp_read. wp_let. wp_apply wp_new; first done. done.
+    iIntros (lx) "(H† & Hlx)". rewrite own_loc_na_vec_singleton.
+    wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
+    iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ lft_intersect).
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
+            with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
+    { rewrite bi.big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+      iSplitR "H†".
+      - iFrame. iExists [_]. rewrite own_loc_na_vec_singleton. by iFrame.
+      - iDestruct "H†" as "[?|%]". by iLeft. by iRight. }
+    iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
+    iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
+    iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
+    iMod ("Hclose2" with "Hϝ HL") as "HL". iMod ("Hclose1" with "Hα HL") as "HL".
+    wp_rec. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as ([|r'[]]) "[Hr Hr']";
+      try by iDestruct (ty_size_eq with "Hr'") as "%".
+    rewrite own_loc_na_vec_singleton. wp_read. wp_let.
+    wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
+    { rewrite own_loc_na_vec_singleton freeable_sz_full. iFrame.
+      iDestruct "Hr†" as "[?|%]". by iLeft. by iRight. }
+    iIntros "_". wp_seq. wp_write.
+    iApply (type_type _ [_] _ [ #lref ◁ box (refmut α ty2) ]
+       with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame.
+      iExists [_;_]. rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+      iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
+    iApply type_jump; solve_typing.
+  Qed.
+End refmut_functions.