Continue porting files.

_CoqProject

@@ -17,6 +17,7 @@ theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
 theories/lang/notation.v
 theories/lang/memcpy.v
+theories/lang/new_delete.v
 theories/typing/base.v
 theories/typing/lft_contexts.v
 theories/typing/type.v
@@ -29,3 +30,7 @@ theories/typing/uninit.v
 theories/typing/programs.v
 theories/typing/bool.v
 theories/typing/int.v
+theories/typing/uniq_bor.v
+theories/typing/shr_bor.v
+theories/typing/own.v
+theories/typing/borrow.v

opam

@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-04-23.3.1dfd6ae7") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-04-24.1.b6c8bb32") | (= "dev") }
 ]

theories/lang/new_delete.v

+From gpfsl.lang Require Import proofmode.
+From lrust.lang Require Export notation.
+From lrust.lang Require Import memcpy.
+Set Default Proof Using "Type".
+
+Definition new : val :=
+  λ: ["n"],
+    if: "n" ≤ #0 then #((42%positive, 1337):loc)
+    else Alloc "n".
+
+Definition delete : val :=
+  λ: ["n"; "loc"],
+    if: "n" ≤ #0 then #☠
+    else Free "n" "loc".
+
+Section specs.
+  Context `{noprolG Σ}.
+
+  Lemma wp_new E (n : Z):
+    (0 ≤ n)%Z →
+    {{{ True }}} new [ #n ] @ E
+    {{{ l, RET LitV $ LitLoc l;
+        (⎡†l…(Z.to_nat n)⎤ ∨ ⌜n = 0⌝) ∗ ⎡l ↦∗ repeat AVal (Z.to_nat n)⎤ }}}.
+  Proof.
+    iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
+    - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
+      rewrite own_loc_na_vec_nil. auto.
+    - wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz. iFrame.
+  Qed.
+
+  Lemma wp_delete E (n:Z) l vl :
+    n = length vl →
+    {{{ ⎡l ↦∗ vl⎤ ∗ (⎡†l…(length vl)⎤ ∨ ⌜n = 0⌝) }}}
+      delete [ #n; #l] @ E
+    {{{ RET #☠; True }}}.
+  Proof.
+    iIntros (? Φ) "[H↦ [H†|%]] HΦ";
+      wp_lam; wp_op; case_bool_decide; try lia;
+      wp_if; try wp_free; by iApply "HΦ".
+  Qed.
+End specs.
+
+(* FIXME : why are these notations not pretty-printed? *)
+Notation "'letalloc:' x <- e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
+  (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
+Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V%L} !e1 ;; e2)) [new [ #n]])%E
+  (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.

theories/typing/borrow.v

+From iris.proofmode Require Import tactics.
+From gpfsl.lang Require Import proofmode.
+From lrust.typing Require Export uniq_bor shr_bor own.
+From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
+
+(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
+  a separate file so make sure that own.v and uniq_bor.v can be compiled
+  concurrently. *)
+
+Section borrow.
+  Context `{typeG Σ}.
+
+  Lemma tctx_borrow E L p n ty κ :
+    tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
+  Proof.
+    iIntros (tid ?)  "#LFT _ $ [H _]".
+    iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
+    iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+    iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
+    - iExists _. auto.
+    - iExists _. iSplit. done. by iFrame.
+  Qed.
+
+  Lemma tctx_share E L p κ ty :
+    lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
+  Proof.
+    iIntros (Hκ ??) "#LFT #HE HL Huniq".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
+    rewrite !tctx_interp_singleton /=.
+    iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
+    iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
+    iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
+  Qed.
+
+  (* When sharing during extraction, we do the (arbitrary) choice of
+     sharing at the lifetime requested (κ). In some cases, we could
+     actually desire a longer lifetime and then use subtyping, because
+     then we get, in the environment, a shared borrow at this longer
+     lifetime.
+
+     In the case the user wants to do the sharing at a longer
+     lifetime, she has to manually perform the extraction herself at
+     the desired lifetime. *)
+  Lemma tctx_extract_hasty_share E L p ty ty' κ κ' T :
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]).
+    rewrite tctx_reborrow_uniq //. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
+  Lemma tctx_extract_hasty_share_samelft E L p ty ty' κ T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
+                                         ((p ◁ &shr{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
+  Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
+    subtype E L ty' ty →
+    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁{κ} own_ptr n ty)::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
+    by apply tctx_borrow. by f_equiv.
+  Qed.
+
+  (* See the comment above [tctx_extract_hasty_share]. *)
+  Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own_ptr n ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
+    apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
+  Qed.
+
+  Lemma type_deref_uniq_own_instr {E L} κ p n ty :
+    lctx_lft_alive E L κ →
+    typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
+  Proof.
+    iIntros (Hκ tid) "#LFT HE $ HL Hp".
+    rewrite tctx_interp_singleton.
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try by iDestruct "Hown" as %[].
+    iMod (bor_acc_cons with "[LFT //] Hown Htok") as "[H↦ Hclose']". done.
+    iDestruct "H↦" as ([|[| |[[|l'|]|]] []]) "[>H↦ Hown]";
+      try by iDestruct "Hown" as ">%".
+    iDestruct "Hown" as "[Hown H†]". rewrite own_loc_na_vec_singleton -wp_fupd. wp_read.
+    iMod ("Hclose'" $! (l↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
+          with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
+    - iMod (bor_sep with "[LFT //] Hbor") as "[_ Hbor]". done.
+      iMod (bor_sep with "[LFT //] Hbor") as "[_ Hbor]". done.
+      iMod ("Hclose" with "Htok") as "($ & $)".
+      by rewrite tctx_interp_singleton tctx_hasty_val' //=.
+    - iIntros "!> !> (?&?&?) !>". iNext. iExists _.
+      rewrite -own_loc_na_vec_singleton. iFrame. by iFrame.
+    - iFrame.
+  Qed.
+
+  Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ}(own_ptr n ty)) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := !p in e).
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_own_instr|solve_typing|done]. Qed.
+
+  Lemma type_deref_shr_own_instr {E L} κ p n ty :
+    lctx_lft_alive E L κ →
+    typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
+  Proof.
+    iIntros (Hκ tid) "#LFT HE $ HL Hp".
+    rewrite tctx_interp_singleton.
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try iDestruct "Hown" as %[].
+    iDestruct "Hown" as (l') "#[H↦b #Hown]".
+    iMod (frac_bor_acc with "[LFT //] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
+    - iMod ("Hown" with "[%] Htok2") as "H"; first solve_ndisj. iModIntro.
+      iNext. iMod "H". iApply "H".
+    - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
+      iMod ("Hclose'" with "[$H↦]") as "Htok1".
+      iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
+      rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
+  Qed.
+
+  Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ}(own_ptr n ty)) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := !p in e).
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_own_instr|solve_typing|done]. Qed.
+
+  Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
+  Proof.
+    iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
+    rewrite tctx_interp_singleton.
+    iDestruct (Hincl with "HL HE") as "#Hincl".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try by iDestruct "Hown" as %[].
+    iMod (bor_exists (A:=list _) with "[LFT //] Hown") as (vl) "Hbor". done.
+    iMod (bor_sep with "[LFT //] Hbor") as "[H↦ Hbor]". done.
+    destruct vl as [|[| |[[]|]][]];
+      try by iMod (bor_persistent with "[LFT //] Hbor Htok") as "[>% _]".
+    iMod (bor_acc with "[LFT //] H↦ Htok") as "[>H↦ Hclose']". done.
+    rewrite own_loc_na_vec_singleton.
+    iMod (bor_unnest with "[LFT //] Hbor") as "Hbor"; [done|].
+    iApply wp_fupd. wp_read.
+    iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
+    iMod ("Hclose" with "Htok") as "($ & $)".
+    rewrite tctx_interp_singleton tctx_hasty_val' //.
+    iMod (bor_shorten with "[] Hbor") as "$"; [|done].
+    iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
+  Qed.
+
+  Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ}(&uniq{κ'}ty))%T T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := !p in e).
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_uniq_instr|solve_typing|done]. Qed.
+
+  Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
+  Proof.
+    iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
+    iDestruct (Hincl with "HL HE") as "#Hincl".
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try by iDestruct "Hshr" as %[].
+    iDestruct "Hshr" as (l') "[H↦ Hown]".
+    iMod (frac_bor_acc with "[LFT //] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iAssert ⎡κ ⊑ κ' ⊓ κ⎤%I as "#Hincl'".
+    { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
+    iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
+    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
+    - iMod ("Hown" with "[%] Htok2") as "Hown"; first solve_ndisj. iModIntro. iNext.
+      iMod "Hown". iApply "Hown".
+    - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
+      iMod ("Hclose''" with "Htok2") as "Htok2".
+      iMod ("Hclose'" with "[$H↦]") as "Htok1".
+      iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
+      rewrite tctx_interp_singleton tctx_hasty_val' //.
+      by iApply (ty_shr_mono with "Hincl' Hshr").
+  Qed.
+
+  Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ}(&uniq{κ'}ty))%T T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ}ty) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := !p in e).
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
+End borrow.
+
+Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
+               | 10 : lrust_typing.
+Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
+Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.

theories/typing/own.v

+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import new_delete memcpy.
+From lrust.typing Require Export type.
+From lrust.typing Require Import util uninit type_context programs.
+Set Default Proof Using "Type".
+
+Section own.
+  Context `{typeG Σ}.
+
+  Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
+    match sz, n return _ with
+    | 0%nat, _ => True
+    | _, 0%nat => False
+    | sz, n => †{mk_Qp (sz / n) _}l…sz
+    end%I.
+  Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
+  Arguments freeable_sz : simpl never.
+  Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
+  Proof. destruct sz, n; apply _. Qed.
+
+  Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
+  Proof.
+    destruct n.
+    - iSplit; iIntros "H /="; auto.
+    - assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
+      rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= Qcmult_inv_r //.
+  Qed.
+
+  Lemma freeable_sz_full_S n l : freeable_sz (S n) (S n) l ⊣⊢ †{1}l…(S n).
+  Proof. rewrite freeable_sz_full. iSplit; auto. iIntros "[$|%]"; done. Qed.
+
+  Lemma freeable_sz_split n sz1 sz2 l :
+    freeable_sz n sz1 l ∗ freeable_sz n sz2 (l >> sz1) ⊣⊢
+                freeable_sz n (sz1 + sz2) l.
+  Proof.
+    destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
+    - by rewrite left_id shift_0.
+    - by rewrite right_id Nat.add_0_r.
+    - iSplit. by iIntros "[[]?]". by iIntros "[]".
+    - rewrite hist_freeable_op_eq. f_equiv. apply Qp_eq.
+      rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
+  Qed.
+
+  (* Make sure 'simpl' doesn't unfold. *)
+  Global Opaque freeable_sz.
+
+  Program Definition own_ptr (n : nat) (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitLoc l) ] =>
+         (* We put a later in front of the †{q}, because we cannot use
+            [ty_size_eq] on [ty] at step index 0, which would in turn
+            prevent us to prove [subtype_own].
+
+            Since this assertion is timeless, this should not cause
+            problems. *)
+           ▷ (l ↦∗: ty.(ty_own) tid ∗ ⎡freeable_sz n ty.(ty_size) l⎤)
+         | _ => False
+         end%I;
+       ty_shr κ tid l :=
+         (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
+            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN}▷=∗
+                            ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}.
+  Next Obligation. by iIntros (q ty tid [|[| |[[]|]] []]) "H". Qed.
+  Next Obligation.
+    move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
+    iMod (bor_exists with "LFT Hshr") as (vl) "Hb"; first solve_ndisj.
+    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
+    destruct vl as [|[| |[[|l'|]|]] []];
+      try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
+    iFrame. iExists l'. rewrite own_loc_na_vec_singleton.
+    rewrite bi.later_sep.
+    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
+    iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
+    iApply delay_sharing_later; done.
+  Qed.
+  Next Obligation.
+    intros _ ty κ κ' tid l. iIntros "#Hκ #H".
+    iDestruct "H" as (l') "[Hfb #Hvs]".
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
+    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); [solve_ndisj..|].
+    iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
+    iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+    by iApply (ty.(ty_shr_mono) with "Hκ").
+  Qed.
+
+  Global Instance own_ptr_wf n ty `{!TyWf ty} : TyWf (own_ptr n ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Lemma own_type_incl n m ty1 ty2 :
+    ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
+  Proof.
+    iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
+    - iIntros (?[|[| |[[]|]] []]) "H"; try done. simpl.
+      iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
+      iDestruct "Heq" as %->. iFrame. iApply (own_loc_na_pred_wand with "Hmt").
+      iApply "Ho".
+    - iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
+      iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
+      iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
+      iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
+  Qed.
+
+  Global Instance own_mono E L n :
+    Proper (subtype E L ==> subtype E L) (own_ptr n).
+  Proof.
+    intros ty1 ty2 Hincl. iIntros (qL) "HL".
+    iDestruct (Hincl with "HL") as "#Hincl".
+    iClear "∗". iIntros "!# #HE".
+    iApply own_type_incl; first by auto. iApply "Hincl"; auto.
+  Qed.
+  Lemma own_mono' E L n1 n2 ty1 ty2 :
+    n1 = n2 → subtype E L ty1 ty2 → subtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+  Proof. intros -> *. by apply own_mono. Qed.
+  Global Instance own_proper E L n :
+    Proper (eqtype E L ==> eqtype E L) (own_ptr n).
+  Proof. intros ??[]; split; by apply own_mono. Qed.
+  Lemma own_proper' E L n1 n2 ty1 ty2 :
+    n1 = n2 → eqtype E L ty1 ty2 → eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+  Proof. intros -> *. by apply own_proper. Qed.
+
+  Global Instance own_type_contractive n : TypeContractive (own_ptr n).
+  Proof. solve_type_proper. Qed.
+
+  Global Instance own_ne n : NonExpansive (own_ptr n).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance own_send n ty :
+    Send ty → Send (own_ptr n ty).
+  Proof.
+    iIntros (Hsend tid1 tid2 [|[| |[[]|]] []]) "H"; try done.
+    iDestruct "H" as "[Hm $]". iNext. iApply (own_loc_na_pred_wand with "Hm").
+    iIntros (vl) "?". by iApply Hsend.
+  Qed.
+
+  Global Instance own_sync n ty :
+    Sync ty → Sync (own_ptr n ty).
+  Proof.
+    iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
+    iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
+    iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
+  Qed.
+End own.
+
+Section box.
+  Context `{typeG Σ}.
+
+  Definition box ty := own_ptr ty.(ty_size) ty.
+
+  Lemma box_type_incl ty1 ty2 :
+    ▷ type_incl ty1 ty2 -∗ type_incl (box ty1) (box ty2).
+  Proof.
+    iIntros "#Hincl". iApply own_type_incl; last done.
+    iDestruct "Hincl" as "(? & _ & _)". done.
+  Qed.
+
+  Global Instance box_mono E L :
+    Proper (subtype E L ==> subtype E L) box.
+  Proof.
+    intros ty1 ty2 Hincl. iIntros (qL) "HL".
+    iDestruct (Hincl with "HL") as "#Hincl".
+    iClear "∗". iIntros "!# #HE".
+    iApply box_type_incl. iApply "Hincl"; auto.
+  Qed.
+  Lemma box_mono' E L ty1 ty2 :
+    subtype E L ty1 ty2 → subtype E L (box ty1) (box ty2).
+  Proof. intros. by apply box_mono. Qed.
+  Global Instance box_proper E L :
+    Proper (eqtype E L ==> eqtype E L) box.
+  Proof. intros ??[]; split; by apply box_mono. Qed.
+  Lemma box_proper' E L ty1 ty2 :
+    eqtype E L ty1 ty2 → eqtype E L (box ty1) (box ty2).
+  Proof. intros. by apply box_proper. Qed.
+
+  Global Instance box_type_contractive : TypeContractive box.
+  Proof. solve_type_proper. Qed.
+
+  Global Instance box_ne : NonExpansive box.
+  Proof. apply type_contractive_ne, _. Qed.
+End box.
+
+Section util.
+  Context `{typeG Σ}.
+
+  Lemma ownptr_own n ty tid v :
+    (own_ptr n ty).(ty_own) tid [v] ⊣⊢
+       ∃ (l : loc) (vl : vec value.val ty.(ty_size)),
+         ⌜v = VVal #l⌝ ∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗
+                         ▷ ⎡freeable_sz n ty.(ty_size) l⎤.
+  Proof.
+    iSplit.
+    - iIntros "Hown". destruct v as [| |[[|l|]|]]; try done.
+      iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
+      iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
+    - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
+      iFrame. iExists _. iFrame.
+  Qed.
+
+  Lemma ownptr_uninit_own n m tid v :
+    (own_ptr n (uninit m)).(ty_own) tid [v] ⊣⊢
+         ∃ (l : loc) (vl' : vec value.val m),
+           ⌜v = VVal #l⌝ ∗ ▷ l ↦∗ vl' ∗ ▷ ⎡freeable_sz n m l⎤.
+  Proof.
+    rewrite ownptr_own. apply bi.exist_proper=>l. iSplit.
+    (* FIXME: The goals here look rather confusing:  One cannot tell that we are looking at
+       a statement in Iris; the top-level → could just as well be a Coq implication. *)
+    - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
+      iExists vl. iSplit; done.
+    - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
+      iExists vl. rewrite /= vec_to_list_length.
+      eauto with iFrame.
+  Qed.
+End util.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  (** Typing *)
+  Lemma write_own {E L} ty ty' n :
+    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
+  Proof.
+    iIntros (Hsz) "!#".
+    iIntros ([| |[[]|]] tid F qL ?) "_ _ $ Hown"; try iDestruct "Hown" as %[].
+    rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
+  Qed.
+
+  Lemma read_own_copy E L ty n :
+    Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
+  Proof.
+    iIntros (Hsz) "!#".
+    iIntros ([| |[[]|]] tid F qL ?) "_ _ $ $ Hown"; try iDestruct "Hown" as %[].
+    iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
+    iExists _. iModIntro. auto.
+  Qed.
+
+  Lemma read_own_move E L ty n :
+    typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
+  Proof.
+    iIntros "!#" ([| |[[]|]] tid F qL ?) "_ _ $ $ Hown"; try iDestruct "Hown" as %[].
+    iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    iDestruct (ty_size_eq with "Hown") as "#>%".
+    iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
+    iExists _. iFrame. done.
+  Qed.
+
+  Lemma type_new_instr {E L} (n : Z) :
+    0 ≤ n →
+    let n' := Z.to_nat n in
+    typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
+  Proof.
+    iIntros (? tid) "#LFT #HE $ $ _".
+    iApply wp_new; try done. iModIntro.
+    iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
+    iNext. rewrite freeable_sz_full Z2Nat.id //.
+    iSplitR "H†".
+    - iExists (repeat AVal (Z.to_nat n)). iFrame. by rewrite /= repeat_length.
+    - by iDestruct "H†" as "[?|%]"; [iLeft|iRight].
+  Qed.
+
+  Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
+    Closed (x :b: []) e →
+    0 ≤ n →
+    n' = Z.to_nat n →
+    (∀ (v : val),
+        typed_body E L C ((v ◁ own_ptr n' (uninit n')) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := new [ #n ] in e).
+  Proof. iIntros. subst. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
+
+  Lemma type_new_subtype ty E L C T x (n : Z) e :
+    Closed (x :b: []) e →
+    0 ≤ n →
+    let n' := Z.to_nat n in
+    subtype E L (uninit n') ty →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr n' ty) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := new [ #n ] in e).
+  Proof.
+    iIntros (????) "Htyp". iApply type_let; [by apply type_new_instr|solve_typing|].
+    iIntros (v). iApply typed_body_mono; last iApply "Htyp"; try done.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
+  Qed.
+
+  Lemma type_delete_instr {E L} ty (n : Z) p :
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_instruction E L [p ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
+  Proof.
+    iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
+    wp_bind p. iApply (wp_hasty with "Hp").
+    iIntros ([[]|]) "_ Hown"; try by iDestruct "Hown" as %[].
+    iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
+    iDestruct (ty_size_eq with "Hown") as "#>EQ".
+    iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto.
+    - iFrame "H↦". rewrite freeable_sz_full. iDestruct "H†" as "[?|%]"; auto.
+    - rewrite /tctx_interp /=. by iIntros "!> _ !>".
+  Qed.
+
+  Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
+    Closed [] e →
+    tctx_extract_hasty E L p (own_ptr n' ty) T T' →
+    n = n' → Z.of_nat (ty.(ty_size)) = n →
+    typed_body E L C T' e -∗
+    typed_body E L C T (delete [ #n; p ] ;; e).
+  Proof.
+    iIntros (?? -> Hlen) "?". iApply type_seq; [by apply type_delete_instr| |done].
+    by rewrite (inj _ _ _ Hlen).
+  Qed.
+
+  Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
+    Closed [] p → Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty T T' →
+    ty.(ty_size) = 1%nat →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr 1 ty)::T') (subst x v e)) -∗
+    typed_body E L C T (letalloc: x <- p in e).
+  Proof.
+    iIntros (??? Hsz) "**". iApply type_new.
+    - rewrite /Closed /=. rewrite !andb_True.
+      eauto 10 using is_closed_weaken with set_solver.
+    - done.
+    - solve_typing.
+    - iIntros (xv) "/=". rewrite -Hsz.
+      assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
+      { (* TODO : simpl_subst should be able to do this. *)
+        unfold subst=>/=. repeat f_equal.
+        - by rewrite bool_decide_true.
+        - eapply is_closed_subst. done. set_solver. }
+      iApply type_assign; [|solve_typing|by eapply write_own|solve_typing].
+      apply subst_is_closed; last done. apply is_closed_of_val.
+  Qed.
+
+  Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
+    Closed [] p → Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty1 T T' →
+    typed_read E L ty1 ty ty2 →
+    (∀ (v : val),
+        typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) -∗
+    typed_body E L C T (letalloc: x <-{ty.(ty_size)} !p in e).
+  Proof.
+    iIntros. iApply type_new.
+    - rewrite /Closed /=. rewrite !andb_True.
+      eauto 10 using is_closed_of_val, is_closed_weaken with set_solver.
+    - lia.
+    - done.
+    - iIntros (xv) "/=".
+      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
+              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
+      { (* TODO : simpl_subst should be able to do this. *)
+        unfold subst=>/=. repeat f_equal.
+        - eapply (is_closed_subst []). apply is_closed_of_val. set_solver.
+        - by rewrite bool_decide_true.
+        - eapply is_closed_subst. done. set_solver. }
+      rewrite Nat2Z.id. iApply type_memcpy.
+      + apply subst_is_closed; last done. apply is_closed_of_val.
+      + solve_typing.
+      + (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
+           I guess that's caused by it trying to unify typed_read and typed_write,
+           but considering that the Iris connectives are all sealed, why does
+           that take so long? *)
+        by eapply (write_own ty (uninit _)).
+      + solve_typing.
+      + done.
+      + done.
+  Qed.
+End typing.
+
+Hint Resolve own_mono' own_proper' box_mono' box_proper'
+             write_own read_own_copy : lrust_typing.
+(* By setting the priority high, we make sure copying is tried before
+   moving. *)
+Hint Resolve read_own_move | 100 : lrust_typing.
+
+Hint Extern 100 (_ ≤ _) => simpl; lia : lrust_typing.
+Hint Extern 100 (@eq Z _ _) => simpl; lia : lrust_typing.
+Hint Extern 100 (@eq nat _ _) => simpl; lia : lrust_typing.

theories/typing/shr_bor.v

+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
+
+Section shr_bor.
+  Context `{typeG Σ}.
+
+  Program Definition shr_bor (κ : lft) (ty : type) : type :=
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitLoc l) ] => ty.(ty_shr) κ tid l
+         | _ => False
+         end%I |}.
+  Next Obligation. by iIntros (κ ty tid [|[| |[[]|]] []]) "H". Qed.
+  Next Obligation. intros κ ty tid [|[| |[[]|]] []]; apply _. Qed.
+
+  Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
+  Lemma shr_type_incl κ1 κ2 ty1 ty2 :
+    κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
+  Proof.
+    iIntros "#Hκ #[_ [_ Hty]]". iApply type_incl_simple_type. simpl.
+    iIntros "!#" (tid [|[| |[[]|]] []]) "H"; try done. iApply "Hty".
+    iApply (ty1.(ty_shr_mono) with "Hκ"). done.
+  Qed.
+
+  Global Instance shr_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
+  Proof.
+    intros κ1 κ2 Hκ ty1 ty2 Hty.
+    iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
+    iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
+    iApply shr_type_incl.
+    - by iApply "Hincl".
+    - by iApply "Hty".
+  Qed.
+  Global Instance shr_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
+  Proof. intros ??????. by apply shr_mono. Qed.
+  Global Instance shr_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) shr_bor.
+  Proof. intros ??[] ??[]. by split; apply shr_mono. Qed.
+
+  Global Instance shr_type_contractive κ : TypeContractive (shr_bor κ).
+  Proof.
+    intros n ???. apply: ty_of_st_type_ne. destruct n; first done.
+    solve_type_proper.
+  Qed.
+
+  Global Instance shr_ne κ : NonExpansive (shr_bor κ).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance shr_send κ ty :
+    Sync ty → Send (shr_bor κ ty).
+  Proof. by iIntros (Hsync tid1 tid2 [|[| |[[]|]] []]) "H"; try iApply Hsync. Qed.
+End shr_bor.
+
+Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
+    subtype E L (&shr{κ1}ty1) (&shr{κ2}ty2).
+  Proof. by intros; apply shr_mono. Qed.
+  Lemma shr_proper' E L κ ty1 ty2 :
+    eqtype E L ty1 ty2 → eqtype E L (&shr{κ}ty1) (&shr{κ}ty2).
+  Proof. by intros; apply shr_proper. Qed.
+
+  Lemma tctx_reborrow_shr E L p ty κ κ' :
+    lctx_lft_incl E L κ' κ →
+    tctx_incl E L [p ◁ &shr{κ}ty] [p ◁ &shr{κ'}ty; p ◁{κ} &shr{κ}ty].
+  Proof.
+    iIntros (Hκκ' tid ?) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iFrame. rewrite /tctx_interp /=.
+    iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
+    - iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
+    - iSplit=> //. iExists _. auto.
+  Qed.
+
+  Lemma read_shr E L κ ty :
+    Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
+  Proof.
+    iIntros (Hcopy Halive) "!#".
+    iIntros ([| |[[]|]] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try iDestruct "Hshr" as %[].
+    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
+    iMod (copy_shr_acc with "[LFT //] Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)";
+      first solve_ndisj.
+    { rewrite ->shr_locsE_shrN. solve_ndisj. }
+    iDestruct "H↦" as (vl) "[>Hmt #Hown]". iModIntro. iExists _, _, _.
+    iFrame "∗#". iSplit; first done. iIntros "Hmt".
+    iMod ("Hcl" with "Htl [Hmt]") as "[$ Hκ]"; first by iExists _; iFrame.
+    by iMod ("Hclose" with "Hκ") as "$".
+  Qed.
+End typing.
+
+Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.

theories/typing/uniq_bor.v

+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import util lft_contexts type_context programs.
+Set Default Proof Using "Type".
+
+Section uniq_bor.
+  Context `{typeG Σ}.
+
+  Program Definition uniq_bor (κ:lft) (ty:type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitLoc l) ] => &{κ} (l ↦∗: ty.(ty_own) tid)
+         | _ => False
+         end;
+       ty_shr κ' tid l :=
+         ∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ⊓κ']
+               ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
+    |}%I.
+  Next Obligation. by iIntros (q ty tid [|[| |[[]|]] []]) "H". Qed.
+  Next Obligation.
+    move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
+    iMod (bor_exists with "LFT Hshr") as ([|[| |[[|l'|]|]] []]) "Hb"; first solve_ndisj;
+      (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
+      try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
+    iFrame. iExists l'. rewrite own_loc_na_vec_singleton.
+    iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
+    iApply delay_sharing_nested; try done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
+    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
+    { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
+    iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); try solve_ndisj.
+    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
+    iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+    by iApply (ty_shr_mono with "Hκ0").
+  Qed.
+
+  Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
+  Global Instance uniq_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
+  Proof.
+    intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (?) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
+    iIntros "!# #HE". iSplit; first done.
+    iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
+    iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
+    - iIntros (?  [|[| |[[]|]] []]) "H"; try done.
+      iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
+      iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+      iExists vl; iFrame; by iApply "Ho".
+    - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
+      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
+      iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; [done..|]. by iApply "Hs".
+  Qed.
+  Global Instance uniq_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
+  Proof. intros ??????. apply uniq_mono. done. by symmetry. Qed.
+  Global Instance uniq_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) uniq_bor.
+  Proof. intros ??[]; split; by apply uniq_mono. Qed.
+
+  Global Instance uniq_type_contractive κ : TypeContractive (uniq_bor κ).
+  Proof. solve_type_proper. Qed.
+
+  Global Instance uniq_ne κ : NonExpansive (uniq_bor κ).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance uniq_send κ ty :
+    Send ty → Send (uniq_bor κ ty).
+  Proof.
+    iIntros (Hsend tid1 tid2 [|[| |[[]|]] []]) "H"; try done.
+    iApply bor_iff; last done. iNext. iAlways. iApply bi.equiv_iff.
+    do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
+  Qed.
+
+  Global Instance uniq_sync κ ty :
+    Sync ty → Sync (uniq_bor κ ty).
+  Proof.
+    iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
+    iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iClear "Hshr".
+    iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
+  Qed.
+End uniq_bor.
+
+Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
+    subtype E L (&uniq{κ1}ty1) (&uniq{κ2}ty2).
+  Proof. by intros; apply uniq_mono. Qed.
+  Lemma uniq_proper' E L κ ty1 ty2 :
+    eqtype E L ty1 ty2 → eqtype E L (&uniq{κ}ty1) (&uniq{κ}ty2).
+  Proof. by intros; apply uniq_proper. Qed.
+
+  Lemma tctx_reborrow_uniq E L p ty κ κ' :
+    lctx_lft_incl E L κ' κ →
+    tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
+  Proof.
+    iIntros (Hκκ' tid ?) "#LFT HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as ([[]|]) "[% Hb]"; try done.
+    iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
+    iSplitL "Hb"; iExists _; auto.
+  Qed.
+
+  Lemma tctx_extract_hasty_reborrow E L p ty ty' κ κ' T :
+    lctx_lft_incl E L κ' κ → eqtype E L ty ty' →
+    tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
+                       ((p ◁{κ'} &uniq{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, uniq_mono'.
+  Qed.
+
+  Lemma read_uniq E L κ ty :
+    Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+  Proof.
+    iIntros (Hcopy Halive) "!#".
+    iIntros ([| |[[]|]] tid F qL ?) "#LFT #HE Htl HL Hown"; try iDestruct "Hown" as %[].
+    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
+    iMod (bor_acc with "[LFT //] Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
+    iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
+    iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
+    iMod ("Hclose'" with "[H↦]") as "[$ Htok]". by iExists _; iFrame.
+    by iMod ("Hclose" with "Htok") as "($ & $ & $)".
+  Qed.
+
+  Lemma write_uniq E L κ ty :
+    lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+  Proof.
+    iIntros (Halive) "!#".
+    iIntros ([| |[[]|]] tid F qL ?) "#LFT HE HL Hown"; try iDestruct "Hown" as %[].
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    iMod (bor_acc with "[LFT //] Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.
+    iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
+    iDestruct "Hown" as ">%". iModIntro. iExists _, _. iSplit; first done.
+    iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
+    iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]". by iExists _; iFrame.
+    by iMod ("Hclose" with "Htok") as "($ & $ & $)".
+  Qed.
+End typing.
+
+Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
+Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.