theories/typing/lft_contexts.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import fractional.
-From lrust.lifetime Require Import frac_borrow.
-Set Default Proof Using "Type".
-
-Inductive elctx_elt : Type :=
-| ELCtx_Alive (κ : lft)
-| ELCtx_Incl (κ κ' : lft).
-Notation elctx := (list elctx_elt).
-
-Delimit Scope lrust_elctx_scope with EL.
-(* We need to define [elctx] and [llctx] as notations to make eauto
-   work. But then, Coq is not able to bind them to their
-   notations, so we have to use [Arguments] everywhere. *)
-Bind Scope lrust_elctx_scope with elctx_elt.
-
-Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
-Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
-
-Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
-  (at level 60, right associativity) : lrust_elctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons elctx_elt x1%EL (@cons elctx_elt x2%EL
-        (..(@cons elctx_elt xn%EL (@nil elctx_elt))..))) : lrust_elctx_scope.
-Notation "[ x ]" := (@cons elctx_elt x%EL (@nil elctx_elt)) : lrust_elctx_scope.
-
-Definition llctx_elt : Type := lft * list lft.
-Notation llctx := (list llctx_elt).
-
-Delimit Scope lrust_llctx_scope with LL.
-Bind Scope lrust_llctx_scope with llctx_elt.
-
-Notation "κ ⊑ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
-
-Notation "a :: b" := (@cons llctx_elt a%LL b%LL)
-  (at level 60, right associativity) : lrust_llctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons llctx_elt x1%LL (@cons llctx_elt x2%LL
-        (..(@cons llctx_elt xn%LL (@nil llctx_elt))..))) : lrust_llctx_scope.
-Notation "[ x ]" := (@cons llctx_elt x%LL (@nil llctx_elt)) : lrust_llctx_scope.
-
-Section lft_contexts.
-  Context `{invG Σ, lftG Σ}.
-  Implicit Type (κ : lft).
-
-  (* External lifetime contexts. *)
-  Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
-    match x with
-    | ☀ κ => q.[κ]%I
-    | κ ⊑ κ' => (κ ⊑ κ')%I
-    end%EL.
-  Global Instance elctx_elt_interp_fractional x:
-    Fractional (elctx_elt_interp x).
-  Proof. destruct x; unfold elctx_elt_interp; apply _. Qed.
-  Typeclasses Opaque elctx_elt_interp.
-  Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
-    match x with
-    | ☀ κ => True%I
-    | κ ⊑ κ' => (κ ⊑ κ')%I
-    end%EL.
-  Global Instance elctx_elt_interp_0_persistent x:
-    PersistentP (elctx_elt_interp_0 x).
-  Proof. destruct x; apply _. Qed.
-  Typeclasses Opaque elctx_elt_interp_0.
-
-  Lemma elctx_elt_interp_persist x q :
-    elctx_elt_interp x q -∗ elctx_elt_interp_0 x.
-  Proof. destruct x; by iIntros "?/=". Qed.
-
-  Definition elctx_interp (E : elctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ E, elctx_elt_interp x q)%I.
-  Global Arguments elctx_interp _%EL _%Qp.
-  Global Instance elctx_interp_fractional E:
-    Fractional (elctx_interp E).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance elctx_interp_as_fractional E q:
-    AsFractional (elctx_interp E q) (elctx_interp E) q.
-  Proof. split. done. apply _. Qed.
-  Global Instance elctx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) elctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque elctx_interp.
-
-  Definition elctx_interp_0 (E : elctx) : iProp Σ :=
-    ([∗ list] x ∈ E, elctx_elt_interp_0 x)%I.
-  Global Arguments elctx_interp_0 _%EL.
-  Global Instance elctx_interp_0_persistent E:
-    PersistentP (elctx_interp_0 E).
-  Proof. apply _. Qed.
-  Global Instance elctx_interp_0_permut:
-    Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp_0.
-  Proof. intros ???. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque elctx_interp_0.
-
-  Lemma elctx_interp_persist x q :
-    elctx_interp x q -∗ elctx_interp_0 x.
-  Proof.
-    unfold elctx_interp, elctx_interp_0. f_equiv. intros _ ?.
-    apply elctx_elt_interp_persist.
-  Qed.
-
-  (* Local lifetime contexts. *)
-
-  Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
-    let κ' := foldr (∪) static (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={⊤,⊤∖↑lftN}▷=∗ [†κ0]))%I.
-  Global Instance llctx_elt_interp_fractional x :
-    Fractional (llctx_elt_interp x).
-  Proof.
-    destruct x as [κ κs]. iIntros (q q'). iSplit; iIntros "H".
-    - iDestruct "H" as (κ0) "(% & [Hq Hq'] & #?)".
-      iSplitL "Hq"; iExists _; by iFrame "∗%".
-    - iDestruct "H" as "[Hq Hq']".
-      iDestruct "Hq" as (κ0) "(% & Hq & #?)".
-      iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
-      rewrite (inj (union (foldr (∪) static κs)) κ0' κ0); last congruence.
-      iExists κ0. by iFrame "∗%".
-  Qed.
-  Typeclasses Opaque llctx_elt_interp.
-
-  Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
-    let κ' := foldr (∪) static (x.2) in (∃ κ0, x.1 = κ' ∪ κ0).
-  Lemma llctx_elt_interp_persist x q :
-    llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 x⌝.
-  Proof.
-    iIntros "H". unfold llctx_elt_interp.
-    iDestruct "H" as (κ0) "[% _]". by iExists κ0.
-  Qed.
-
-  Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
-  Global Arguments llctx_interp _%LL _%Qp.
-  Global Instance llctx_interp_fractional L:
-    Fractional (llctx_interp L).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance llctx_interp_as_fractional L q:
-    AsFractional (llctx_interp L q) (llctx_interp L) q.
-  Proof. split. done. apply _. Qed.
-  Global Instance llctx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque llctx_interp.
-
-  Definition llctx_interp_0 (L : llctx) : Prop :=
-    ∀ x, x ∈ L → llctx_elt_interp_0 x.
-  Global Arguments llctx_interp_0 _%LL.
-  Lemma llctx_interp_persist L q :
-    llctx_interp L q -∗ ⌜llctx_interp_0 L⌝.
-  Proof.
-    iIntros "H". iIntros (x ?). iApply llctx_elt_interp_persist.
-    unfold llctx_interp. by iApply (big_sepL_elem_of with "H").
-  Qed.
-
-  Lemma lctx_equalize_lft qE qL κ1 κ2 `{!frac_borG Σ} :
-    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ [κ2]%list) qL ={⊤}=∗
-      elctx_elt_interp (κ1 ⊑ κ2) qE ∗ elctx_elt_interp (κ2 ⊑ κ1) qE.
-  Proof.
-    iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
-    iDestruct "Hκ" as (κ) "(% & Hκ & _)".
-    iMod (bor_create _ κ2 with "LFT [Hκ]") as "[Hκ _]"; first done; first by iFrame.
-    iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
-    { rewrite Qp_mult_1_r. done. }
-    iModIntro. subst κ1. iSplit.
-    - iApply lft_le_incl.
-      rewrite <-!gmultiset_union_subseteq_l. done.
-    - iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
-      + iApply lft_incl_refl.
-      + iApply lft_incl_static.
-      + iApply (frac_bor_lft_incl with "LFT"). done.
-  Qed.
-
-  Context (E : elctx) (L : llctx).
-
-  (* Lifetime inclusion *)
-
-  Definition lctx_lft_incl κ κ' : Prop :=
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ κ ⊑ κ'.
-
-  Definition lctx_lft_eq κ κ' : Prop :=
-    lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
-
-  Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
-  Proof. iIntros "_ _". iApply lft_incl_refl. Qed.
-
-  Global Instance lctx_lft_incl_preorder : PreOrder lctx_lft_incl.
-  Proof.
-    split; first by intros ?; apply lctx_lft_incl_relf.
-    iIntros (??? H1 H2) "#HE #HL". iApply (lft_incl_trans with "[#] [#]").
-    iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
-  Qed.
-
-  Global Instance lctx_lft_incl_proper :
-    Proper (lctx_lft_eq ==> lctx_lft_eq ==> iff) lctx_lft_incl.
-  Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
-
-  Global Instance lctx_lft_eq_equivalence : Equivalence lctx_lft_eq.
-  Proof.
-    split.
-    - by split.
-    - intros ?? Heq; split; apply Heq.
-    - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
-  Qed.
-
-  Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
-  Proof. iIntros "_ _". iApply lft_incl_static. Qed.
-
-  Lemma lctx_lft_incl_local κ κ' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
-  Proof.
-    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
-    edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
-    iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
-    clear -Hκ'κs. induction Hκ'κs.
-    - apply gmultiset_union_subseteq_l.
-    - etrans. done. apply gmultiset_union_subseteq_r.
-  Qed.
-
-  Lemma lctx_lft_incl_local' κ κ' κ'' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
-  Proof. intros. etrans; last done. by eapply lctx_lft_incl_local. Qed.
-
-  Lemma lctx_lft_incl_external κ κ' : (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ κ'.
-  Proof.
-    iIntros (?) "H _".
-    rewrite /elctx_interp_0 /elctx_elt_interp_0 big_sepL_elem_of //. done.
-  Qed.
-
-  Lemma lctx_lft_incl_external' κ κ' κ'' :
-    (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
-  Proof. intros. etrans; last done. by eapply lctx_lft_incl_external. Qed.
-
-  (* Lifetime aliveness *)
-
-  Definition lctx_lft_alive (κ : lft) : Prop :=
-    ∀ F qE qL, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
-          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma lctx_lft_alive_static : lctx_lft_alive static.
-  Proof.
-    iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
-  Qed.
-
-  Lemma lctx_lft_alive_local κ κs:
-    (κ ⊑ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
-  Proof.
-    iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
-    iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
-    iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
-    iAssert (∃ q', q'.[foldr union static κs] ∗
-      (q'.[foldr union static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
-      with ">[HE HL1]" as "H".
-    { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
-      iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
-      - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
-      - iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
-        iMod (Hκ with "* HE1 HL1") as (q') "[Htok' Hclose]". done.
-        iMod ("IH" with "* HE2 HL2") as (q'') "[Htok'' Hclose']".
-        destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
-        iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
-        iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
-        iMod ("Hclose" with "[$Hκ $Hr']") as "[$$]". iApply "Hclose'". iFrame. }
-    iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
-    destruct (Qp_lower_bound q' (qL/2)) as (q0 & q'2 & q''2 & -> & ->).
-    iExists q0. rewrite -(lft_tok_sep q0). iDestruct "Htok" as "[$ Htok]".
-    iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
-    iMod ("Hclose'" with "[$Hfold $Htok']") as "[$$]".
-    rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
-  Qed.
-
-  Lemma lctx_lft_alive_external κ: (☀κ)%EL ∈ E → lctx_lft_alive κ.
-  Proof.
-    iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
-    rewrite /elctx_interp /elctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
-    iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
-  Qed.
-
-  Lemma lctx_lft_alive_incl κ κ':
-    lctx_lft_alive κ → lctx_lft_incl κ κ' → lctx_lft_alive κ'.
-  Proof.
-    iIntros (Hal Hinc F qE qL ?) "HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "[HE] [HL]").
-      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
-    iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
-    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
-    iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
-    by iApply "Hclose'".
-  Qed.
-
-  Lemma lctx_lft_alive_external' κ κ':
-    (☀κ)%EL ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
-  Proof.
-    intros. eapply lctx_lft_alive_incl, lctx_lft_incl_external; last done.
-    by apply lctx_lft_alive_external.
-  Qed.
-
-  (* External lifetime context satisfiability *)
-
-  Definition elctx_sat E' : Prop :=
-    ∀ qE qL F, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
-      ∃ qE', elctx_interp E' qE' ∗
-       (elctx_interp E' qE' ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma elctx_sat_nil : elctx_sat [].
-  Proof.
-    iIntros (qE qL F ?) "$$". iExists 1%Qp. rewrite /elctx_interp big_sepL_nil. auto.
-  Qed.
-
-  Lemma elctx_sat_alive E' κ :
-    lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E')%EL.
-  Proof.
-    iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
-    iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
-    iMod (HE' with "HE2 HL2") as (q') "[HE' Hclose']". done.
-    destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
-    rewrite {5 6}/elctx_interp big_sepL_cons /=.
-    iDestruct "Htok" as "[$ Htok]". iDestruct "HE'" as "[Hf HE']".
-    iSplitL "Hf". by rewrite /elctx_interp.
-    iIntros "!>[Htok' ?]". iMod ("Hclose" with "[$Htok $Htok']") as "[$$]".
-    iApply "Hclose'". iFrame. by rewrite /elctx_interp.
-  Qed.
-
-  Lemma elctx_sat_lft_incl E' κ κ' :
-    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
-  Proof.
-    iIntros (Hκκ' HE' qE qL F ?) "HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
-      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
-    iMod (HE' with "HE HL") as (q) "[HE' Hclose']". done.
-    iExists q. rewrite {1 2 4 5}/elctx_interp big_sepL_cons /=.
-    iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
-  Qed.
-End lft_contexts.
-
-Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
-Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
-
-Section elctx_incl.
-  (* External lifetime context inclusion, in a persistent context.
-     (Used for function types subtyping).
-     On paper, this corresponds to using only the inclusions from E, L
-     to show E1; [] |- E2.
-  *)
-
-  Context `{invG Σ, lftG Σ} (E : elctx) (L : llctx).
-
-  Definition elctx_incl E1 E2 : Prop :=
-    ∀ F, ↑lftN ⊆ F → elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-    ∀ qE1, elctx_interp E1 qE1 ={F}=∗ ∃ qE2, elctx_interp E2 qE2 ∗
-       (elctx_interp E2 qE2 ={F}=∗ elctx_interp E1 qE1).
-  Global Instance : RewriteRelation elctx_incl.
-  Arguments elctx_incl _%EL _%EL.
-
-  Global Instance elctx_incl_preorder : PreOrder elctx_incl.
-  Proof.
-    split.
-    - iIntros (???) "_ _ * ?". iExists _. iFrame. eauto.
-    - iIntros (x y z Hxy Hyz ??) "#HE #HL * HE1".
-      iMod (Hxy with "HE HL * HE1") as (qy) "[HE1 Hclose1]"; first done.
-      iMod (Hyz with "HE HL * HE1") as (qz) "[HE1 Hclose2]"; first done.
-      iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
-      iApply ("Hclose1" with ">"). iApply "Hclose2". done.
-  Qed.
-
-  Lemma elctx_incl_refl E' : elctx_incl E' E'.
-  Proof. reflexivity. Qed.
-
-  Lemma elctx_incl_nil E' : elctx_incl E' [].
-  Proof.
-    iIntros (??) "_ _ * $". iExists 1%Qp.
-    rewrite /elctx_interp big_sepL_nil. auto.
-  Qed.
-
-  Global Instance elctx_incl_app_proper :
-    Proper (elctx_incl ==> elctx_incl ==> elctx_incl) app.
-  Proof.
-    iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
-    iIntros "[HE1 HE2]".
-    iMod (HE1 with "HE HL * HE1") as (q1) "[HE1 Hclose1]"; first done.
-    iMod (HE2 with "HE HL * HE2") as (q2) "[HE2 Hclose2]"; first done.
-    destruct (Qp_lower_bound q1 q2) as (q & ? & ? & -> & ->).
-    iModIntro. iExists q. rewrite /elctx_interp !big_sepL_app.
-    iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]".
-    iIntros "[HE1' HE2']".
-    iMod ("Hclose1" with "[$HE1 $HE1']") as "$".
-    iMod ("Hclose2" with "[$HE2 $HE2']") as "$".
-    done.
-  Qed.
-  Global Instance elctx_incl_cons_proper x :
-    Proper (elctx_incl ==> elctx_incl) (cons x).
-  Proof. by apply (elctx_incl_app_proper [_] [_]). Qed.
-
-  Lemma elctx_incl_dup E1 :
-    elctx_incl E1 (E1 ++ E1).
-  Proof.
-    iIntros (??) "#HE #HL * [HE1 HE1']".
-    iModIntro. iExists (qE1 / 2)%Qp.
-    rewrite /elctx_interp !big_sepL_app. iFrame.
-    iIntros "[HE1 HE1']". by iFrame.
-  Qed.
-
-  Lemma elctx_sat_incl E1 E2 :
-    elctx_sat E1 [] E2 → elctx_incl E1 E2.
-   Proof.
-    iIntros (H12 ??) "#HE #HL * HE1".
-    iMod (H12 _ 1%Qp with "HE1 []") as (qE2) "[HE2 Hclose]". done.
-    { by rewrite /llctx_interp big_sepL_nil. }
-    iExists qE2. iFrame. iIntros "!> HE2".
-    by iMod ("Hclose" with "HE2") as "[$ _]".
-   Qed.
-
-  Lemma elctx_incl_lft_alive E1 E2 κ :
-    lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
-  Proof.
-    intros Hκ HE2. rewrite (elctx_incl_dup E1).
-    apply (elctx_incl_app_proper _ [_]); last done.
-    apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
-  Qed.
-
-  Lemma elctx_incl_lft_incl E1 E2 κ κ' :
-    lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
-    elctx_incl E1 ((κ ⊑ κ') :: E2).
-  Proof.
-    iIntros (Hκκ' HE2 ??) "#HE #HL * HE1".
-    iDestruct (elctx_interp_persist with "HE1") as "#HE1'".
-    iDestruct (Hκκ' with "[HE HE1'] HL") as "#Hκκ'".
-    { rewrite /elctx_interp_0 big_sepL_app. auto. }
-    iMod (HE2 with "HE HL * HE1") as (qE2) "[HE2 Hclose']". done.
-    iExists qE2. rewrite /elctx_interp big_sepL_cons /=. iFrame "∗#".
-    iIntros "!> [_ HE2']". by iApply "Hclose'".
-  Qed.
-End elctx_incl.
-
-Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
-
-Ltac solve_typing := eauto 100 with lrust_typing typeclass_instances || fail.
-
-Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve
-     lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
-     lctx_lft_incl_external'
-     lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
-     elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl
-     elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
-  : lrust_typing.
-
-Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
-
-Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
-  lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
-  elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
-Proof.
-  move=> ? /elctx_incl_lft_incl -> //.
-  apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
-Qed.

theories/typing/own.v

-From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From lrust.lang Require Export new_delete.
-From lrust.lang Require Import memcpy.
-From lrust.typing Require Export type.
-From lrust.typing Require Import 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 : TimelessP (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⌝)%I.
-  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_split n sz1 sz2 l :
-    freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc 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_loc_0.
-    - by rewrite right_id Nat.add_0_r.
-    - iSplit. by iIntros "[[]?]". by iIntros "[]".
-    - rewrite heap_freeable_op_eq. f_equiv. apply Qp_eq.
-      rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
-  Qed.
-
-  Program Definition own (n : nat) (ty : type) :=
-    {| ty_size := 1;
-       ty_own tid vl :=
-         (* 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:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗
-                   ▷ freeable_sz n ty.(ty_size) l)%I;
-       ty_shr κ tid l :=
-         (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
-    |}.
-  Next Obligation.
-    iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
-  Qed.
-  Next Obligation.
-    move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
-    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
-    iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
-    iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% $]". set_solver.
-    iExists l'. subst. rewrite heap_mapsto_vec_singleton.
-    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
-    rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l')%I
-          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later with "LFT [Hbtok]") as "Hb".
-      { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
-      { rewrite bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]".
-      { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
-      iApply "Hclose". auto.
-    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
-      iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
-  Qed.
-  Next Obligation.
-    intros _ ty κ κ' tid l. iIntros "#LFT #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∖↑lftN)). set_solver. set_solver.
-    iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
-    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
-    iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-    by iApply (ty.(ty_shr_mono) with "LFT Hκ").
-  Qed.
-
-  Global Instance own_mono E L n :
-    Proper (subtype E L ==> subtype E L) (own n).
-  Proof.
-    intros ty1 ty2 Hincl. iIntros. iSplit; first done.
-    iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
-    iSplit; iAlways.
-    - iIntros (??) "H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
-      iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
-      iDestruct (ty_size_eq with "Hown") as %<-.
-      iDestruct ("Ho" with "* Hown") as "Hown".
-      iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
-      iExists _. by iFrame.
-    - 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.
-  Lemma own_mono' E L n ty1 ty2 :
-    subtype E L ty1 ty2 → subtype E L (own n ty1) (own n ty2).
-  Proof. apply own_mono. Qed.
-  Global Instance own_proper E L n :
-    Proper (eqtype E L ==> eqtype E L) (own n).
-  Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
-  Lemma own_proper' E L n ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (own n ty1) (own n ty2).
-  Proof. apply own_proper. Qed.
-
-  Global Instance own_contractive n : Contractive (own n).
-  Proof.
-    intros m ?? EQ. split; [split|]; simpl.
-    - done.
-    - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
-    - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
-  Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
-  Proof. apply contractive_ne, _. Qed.
-
-  Global Instance own_send n ty :
-    Send ty → Send (own n ty).
-  Proof.
-    iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l) "[% [Hm H†]]". subst vl.
-    iExists _. iSplit; first done. iFrame "H†". iNext.
-    iApply (heap_mapsto_pred_wand with "Hm"). iIntros (vl) "?". by iApply Hsend.
-  Qed.
-
-  Global Instance own_sync n ty :
-    Sync ty → Sync (own 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.
-    iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
-    iMod "Hfin" as "[Hshr $]". by iApply Hsync.
-  Qed.
-End own.
-
-Section typing.
-  Context `{typeG Σ}.
-
-  (** Typing *)
-  Lemma write_own {E L} ty ty' n :
-    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
-  Proof.
-    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
-    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    (* This turns out to be the fastest way to apply a lemma below ▷ -- at
-    least if we're fine throwing away the premise even though the result
-    is persistent, which in this case, we are. *)
-    rewrite ty'.(ty_size_eq). iDestruct "Hown" as ">%". iModIntro.
-    iExists _, _. iFrame "H↦".
-    iSplit; first by rewrite Hsz. iIntros "Hown !>".
-    iExists _. iSplit; first done. rewrite Hsz. iFrame.
-  Qed.
-
-  Lemma read_own_copy E L ty n :
-    Copy ty → typed_read E L (own n ty) ty (own n ty).
-  Proof.
-    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
-    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
-    iExists l, _, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
-    iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
-  Qed.
-
-  Lemma read_own_move E L ty n :
-    typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
-  Proof.
-    iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
-    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-    { by iApply ty_size_eq. }
-    iModIntro. iExists l, vl, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
-    iExists _. iSplit; first done. iFrame "H†". iExists _. iFrame.
-    iApply uninit_own. auto.
-  Qed.
-
-  Lemma type_new {E L} (n : nat) :
-    typed_instruction_ty E L [] (new [ #n ]%E) (own n (uninit n)).
-  Proof.
-    iAlways. iIntros (tid eq) "#HEAP #LFT $ $ $ _".
-    iApply (wp_new with "HEAP"); try done; first omega. iModIntro.
-    iIntros (l vl) "(% & H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
-    iExists _. iSplit; first done. iNext. rewrite Nat2Z.id freeable_sz_full. iFrame.
-    iExists vl. iFrame.
-    match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
-    apply (inj Z.of_nat) in Hlen. subst.
-    iInduction vl as [|v vl] "IH". done.
-    iExists [v], vl. iSplit. done. by iSplit.
-  Qed.
-
-  Lemma type_delete {E L} ty n p :
-    ty.(ty_size) = n →
-    typed_instruction E L [p ◁ own n ty] (delete [ #n; p])%E (λ _, []).
-  Proof.
-    iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
-    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
-    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
-    iApply (wp_delete with "[-]"); try (by auto); [].
-    rewrite freeable_sz_full. by iFrame.
-  Qed.
-
-  Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
-    ty.(ty_size) = 1%nat →
-    Closed [] p → Closed (x :b: []) e →
-    tctx_extract_hasty E L p ty T T' →
-    (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
-    typed_body E L C T (letalloc: x := p in e).
-  Proof.
-    intros. eapply type_let'.
-    - rewrite /Closed /=. rewrite !andb_True.
-      eauto 10 using is_closed_weaken with set_solver.
-    - apply (type_new 1).
-    - solve_typing.
-    - move=>xv /=.
-      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. }
-      eapply type_let'.
-      + apply subst_is_closed; last done. apply is_closed_of_val.
-      + by apply (type_assign ty (own 1 (uninit 1))), write_own.
-      + solve_typing.
-      + move=>//=.
-  Qed.
-
-  Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
-    Closed [] p → Closed (x :b: []) e →
-    typed_read E L ty1 ty ty2 →
-    tctx_extract_hasty E L p ty1 T T' →
-    (∀ (v : val),
-        typed_body E L C ((v ◁ own (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.
-    intros. eapply type_let'.
-    - rewrite /Closed /=. rewrite !andb_True.
-      eauto 100 using is_closed_weaken with set_solver.
-    - apply type_new.
-    - solve_typing.
-    - move=>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 []). done. set_solver.
-        - by rewrite bool_decide_true.
-        - eapply is_closed_subst. done. set_solver. }
-      eapply type_let'.
-      + apply subst_is_closed; last done. apply is_closed_of_val.
-      + eapply type_memcpy; first done; last done.
-        (* 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 _ (uninit _)).
-      + solve_typing.
-      + move=>//=.
-  Qed.
-End typing.
-
-Hint Resolve own_mono' own_proper' : lrust_typing.

theories/typing/programs.v

-From iris.base_logic Require Import big_op.
-From lrust.lang Require Export notation.
-From lrust.lang Require Import proofmode memcpy.
-From lrust.typing Require Export type lft_contexts type_context cont_context.
-Set Default Proof Using "Type".
-
-Section typing.
-  Context `{typeG Σ}.
-
-  (** Function Body *)
-  (* This is an iProp because it is also used by the function type. *)
-  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
-                        (e : expr) : iProp Σ :=
-    (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
-               elctx_interp E qE -∗ llctx_interp L 1 -∗
-               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
-               WP e {{ _, cont_postcondition }})%I.
-  Global Arguments typed_body _%EL _%LL _%CC _%TC _%E.
-
-  Global Instance typed_body_llctx_permut E :
-    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
-  Proof.
-    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
-    by setoid_rewrite HL.
-  Qed.
-
-  Global Instance typed_body_elctx_permut :
-    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
-  Proof.
-    intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body.
-    by setoid_rewrite HE.
-  Qed.
-
-  Global Instance typed_body_mono E L:
-    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
-           (typed_body E L).
-  Proof.
-    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "#H !#".
-    iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
-    iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
-    iApply ("H" with "HEAP LFT Htl HE HL [HC] HT").
-    iIntros "HE". by iApply (HC with "LFT HC").
-  Qed.
-
-  Global Instance typed_body_mono_flip E L:
-    Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip (⊢))
-           (typed_body E L).
-  Proof. intros ?????????. by eapply typed_body_mono. Qed.
-
-  (** Instruction *)
-  Definition typed_instruction (E : elctx) (L : llctx)
-             (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
-    (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
-              elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
-              WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
-                         llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
-  Global Arguments typed_instruction _%EL _%LL _%TC _%E _%TC.
-
-  (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
-    (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
-      lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
-        ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
-          (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
-            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-  Global Arguments typed_write _%EL _%LL _%T _%T _%T.
-
-  (* Technically speaking, we could remvoe the vl quantifiaction here and use
-     mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
-     make work for some of the provers way harder, since they'd have to show
-     that nobody could possibly have changed the vl (because only half the
-     fraction was given). So we go with the definition that is easier to prove. *)
-  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
-    (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
-      lft_ctx -∗ na_own tid F -∗
-      elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
-        ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
-              (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
-                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-  Global Arguments typed_read _%EL _%LL _%T _%T _%T.
-End typing.
-
-Notation typed_instruction_ty E L T1 e ty :=
-  (typed_instruction E L T1 e (λ v : val, [v ◁ ty]%TC)).
-
-Section typing_rules.
-  Context `{typeG Σ}.
-
-  (* TODO: notation scopes need tuing to avoid the %list here. *)
-  (* TODO: Proof a version of this that substitutes into a compatible context...
-     if we really want to do that. *)
-  Lemma type_equivalize_lft E L C T κ1 κ2 e :
-    typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
-    typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
-  Proof.
-    iIntros (He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
-    rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
-    iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
-    iApply (He with "HEAP LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
-    - rewrite /elctx_interp !big_sepL_cons. by iFrame.
-    - rewrite /elctx_interp !big_sepL_cons. iIntros "(_ & _ & HE)".
-      iApply "HC". done.
-  Qed.
-
-  Lemma type_let E L T1 T2 (T : tctx) C xb e e' :
-    Closed (xb :b: []) e' →
-    typed_instruction E L T1 e T2 →
-    (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
-    typed_body E L C (T1 ++ T) (let: xb := e in e').
-  Proof.
-    iIntros (Hc He He') "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
-    iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
-    { iApply (He with "HEAP LFT Htl HE HL HT1"). }
-    iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
-    iModIntro. iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]").
-    rewrite tctx_interp_app. by iFrame.
-  Qed.
-
-  Lemma type_let' E L T T' T1 T2 C xb e e' :
-    Closed (xb :b: []) e' →
-    typed_instruction E L T1 e T2 →
-    tctx_extract_ctx E L T1 T T' →
-    (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) →
-    typed_body E L C T (let: xb := e in e').
-  Proof.
-    intros ?? HT ?. unfold tctx_extract_ctx in HT. rewrite ->HT.
-    by eapply type_let.
-  Qed.
-
-  Lemma typed_newlft E L C T κs e :
-    Closed [] e →
-    (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
-    typed_body E L C T (Newlft ;; e).
-  Proof.
-    iIntros (Hc He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
-    iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
-    set (κ' := foldr (∪) static κs). wp_seq.
-    iApply (He (κ' ∪ Λ) with "HEAP LFT Htl HE [HL Htk] HC HT").
-    rewrite /llctx_interp big_sepL_cons. iFrame "HL".
-    iExists Λ. iSplit; first done. iFrame. done.
-  Qed.
-
-  (* TODO: It should be possible to show this while taking only one step.
-     Right now, we could take two. *)
-  Lemma typed_endlft E L C T1 T2 κ κs e :
-    Closed [] e → UnblockTctx κ T1 T2 →
-    typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
-  Proof.
-    iIntros (Hc Hub He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
-    iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
-    iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
-    iApply (wp_fupd_step with "Hend"); try done. wp_seq.
-    iIntros "!> #Hdead !>". wp_seq. iApply (He with "HEAP LFT Htl HE HL HC >").
-    iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
-  Qed.
-
-  Lemma type_assign {E L} ty ty1 ty1' p1 p2 :
-    typed_write E L ty1 ty ty1' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']%TC).
-  Proof.
-    iIntros (Hwrt) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL".
-    rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
-    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
-    iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
-    subst v1. iAssert (⌜1%nat = ty_size ty⌝%I) with "[#]" as %Hsz.
-    { change (1%nat) with (length [v2]). by iApply ty_size_eq. }
-    rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_write.
-    rewrite -heap_mapsto_vec_singleton.
-    iMod ("Hclose" with "* [Hl Hown2]") as "($ & $ & Hown)".
-    { iExists _. iFrame. }
-    rewrite tctx_interp_singleton tctx_hasty_val' //.
-  Qed.
-
-  Lemma type_deref {E L} ty ty1 ty1' p :
-    ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
-    typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]%TC).
-  Proof.
-    iIntros (Hsz Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL Hp".
-    rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
-    iIntros (v) "% Hown".
-    iMod (Hread with "* [] LFT Htl HE HL Hown") as
-        (l vl q) "(% & Hl & Hown & Hclose)"; first done.
-    subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
-    { rewrite -Hsz. iApply ty_size_eq. done. }
-    destruct vl as [|v [|]]; try done.
-    rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
-    rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-    by iFrame.
-  Qed.
-
-  Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' n p1 p2 :
-    ty.(ty_size) = n →
-    typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
-    {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
-        tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
-      (p1 <⋯ !{n}p2)
-    {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
-                 tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
-  Proof.
-    iIntros (Hsz) "#Hwrt #Hread !#". iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
-    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
-    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
-    iMod ("Hwrt" with "* [] LFT HE1 HL1 Hown1")
-      as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
-    iMod ("Hread" with "* [] LFT Htl HE2 HL2 Hown2")
-      as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
-    iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
-    { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
-    iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
-    iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with ">"). rewrite !tctx_hasty_val' //.
-    iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
-    { iExists _. iFrame. }
-    iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
-  Qed.
-
-  Lemma type_memcpy {E L} ty ty1 ty1' ty2 ty2' n p1 p2 :
-    ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
-                      (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
-  Proof.
-    iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
-    iApply (type_memcpy_iris with "[] [] * [$HEAP $LFT $Htl $HE $HL HT]"); try done.
-    (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
-    { iPoseProof Hwrt as "Hwrt". done. }
-    { iPoseProof Hread as "Hread". done. }
-    { by rewrite tctx_interp_cons tctx_interp_singleton. }
-    rewrite tctx_interp_cons tctx_interp_singleton. auto.
-  Qed.
-End typing_rules.

theories/typing/tests/get_x.v

-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont.
-Set Default Proof Using "Type".
-
-Section get_x.
-  Context `{typeG Σ}.
-
-  Definition get_x :=
-    (funrec: <> ["p"] → "ret" :=
-       let: "p'" := !"p" in
-       letalloc: "r" := "p'" +ₗ #0 in
-       delete [ #1; "p"] ;; "ret" ["r":expr])%E.
-
-  Lemma get_x_type :
-    typed_instruction_ty [] [] [] get_x
-        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Π[int; int])])
-            (λ α, own 1 (&shr{α} int))).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret args. inv_vec args=>p args.
-    inv_vec args. simpl_subst.
-
-    eapply type_let'.
-    { apply _. }
-    { by eapply (type_deref (&uniq{α} _)), read_own_move. }
-    { solve_typing. }
-    intros p'. simpl_subst.
-
-    eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
-
-    eapply type_let'.
-    { apply _. }
-    { by eapply (type_delete (uninit 1) 1). }
-    { solve_typing. }
-    move=> /= _.
-
-    eapply type_jump with (args := [r]); solve_typing.
-  Qed.
-End get_x.

theories/typing/type.v

-From iris.base_logic.lib Require Export na_invariants.
-From iris.base_logic Require Import big_op.
-From lrust.lang Require Export proofmode notation.
-From lrust.lifetime Require Export frac_borrow.
-From lrust.typing Require Import lft_contexts.
-Set Default Proof Using "Type".
-
-Class typeG Σ := TypeG {
-  type_heapG :> heapG Σ;
-  type_lftG :> lftG Σ;
-  type_na_invG :> na_invG Σ;
-  type_frac_borrowG Σ :> frac_borG Σ
-}.
-
-Definition lftE := ↑lftN.
-Definition lrustN := nroot .@ "lrust".
-Definition shrN  := lrustN .@ "shr".
-
-Section type.
-  Context `{typeG Σ}.
-
-  Definition thread_id := na_inv_pool_name.
-
-  Record type :=
-    { ty_size : nat;
-      ty_own : thread_id → list val → iProp Σ;
-      ty_shr : lft → thread_id → loc → iProp Σ;
-
-      ty_shr_persistent κ tid l : PersistentP (ty_shr κ tid l);
-
-      ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
-      (* The mask for starting the sharing does /not/ include the
-         namespace N, for allowing more flexibility for the user of
-         this type (typically for the [own] type). AFAIK, there is no
-         fundamental reason for this.
-         This should not be harmful, since sharing typically creates
-         invariants, which does not need the mask.  Moreover, it is
-         more consistent with thread-local tokens, which we do not
-         give any.
-
-         The lifetime token is needed (a) to make the definition of simple types
-         nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
-         we can have emp == sum [].
-       *)
-      ty_share E κ l tid q : lftE ⊆ E →
-        lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
-        ty_shr κ tid l ∗ q.[κ];
-      ty_shr_mono κ κ' tid l :
-        lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
-    }.
-  Global Existing Instances ty_shr_persistent.
-
-  Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
-    match n with
-    | 0%nat => ∅
-    | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
-    end.
-
-  Lemma shr_locsE_shift l n m :
-    shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
-  Proof.
-    revert l; induction n; intros l.
-    - rewrite shift_loc_0. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
-      set_solver+.
-  Qed.
-
-  Lemma shr_locsE_disj l n m :
-    shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
-  Proof.
-    revert l; induction n; intros l.
-    - simpl. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
-      apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
-      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
-      rewrite shift_loc_assoc. apply disjoint_union_r. split.
-      + apply ndot_ne_disjoint. destruct l. intros [=]. omega.
-      + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
-  Qed.
-
-  Lemma shr_locsE_shrN l n :
-    shr_locsE l n ⊆ ↑shrN.
-  Proof.
-    revert l; induction n=>l /=; first by set_solver+.
-    apply union_least; last by auto. solve_ndisj.
-  Qed.
-
-  Lemma shr_locsE_subseteq l n m :
-    (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
-  Proof.
-    induction 1; first done. etrans; first done.
-    rewrite -Nat.add_1_l [(_ + _)%nat]comm_L shr_locsE_shift. set_solver+.
-  Qed.
-
-  Lemma shr_locsE_split_tok l n m tid :
-    na_own tid (shr_locsE l (n + m)) ⊣⊢
-      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
-  Proof.
-    rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
-  Qed.
-
-  (** Copy types *)
-  Class Copy (t : type) := {
-    copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
-    copy_shr_acc κ tid E F l q :
-      lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
-      lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
-         ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
-           ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
-        (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
-                                    ={E}=∗ na_own tid F ∗ q.[κ])
-  }.
-  Global Existing Instances copy_persistent.
-
-  Class LstCopy (tys : list type) := lst_copy : Forall Copy tys.
-  Global Instance lst_copy_nil : LstCopy [] := List.Forall_nil _.
-  Global Instance lst_copy_cons ty tys :
-    Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
-
-  (** Send and Sync types *)
-  Class Send (t : type) :=
-    send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
-
-  Class LstSend (tys : list type) := lst_send : Forall Send tys.
-  Global Instance lst_send_nil : LstSend [] := List.Forall_nil _.
-  Global Instance lst_send_cons ty tys :
-    Send ty → LstSend tys → LstSend (ty::tys) := List.Forall_cons _ _ _.
-
-  Class Sync (t : type) :=
-    sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
-
-  Class LstSync (tys : list type) := lst_sync : Forall Sync tys.
-  Global Instance lst_sync_nil : LstSync [] := List.Forall_nil _.
-  Global Instance lst_sync_cons ty tys :
-    Sync ty → LstSync tys → LstSync (ty::tys) := List.Forall_cons _ _ _.
-
-  (** Simple types *)
-  (* We are repeating the typeclass parameter here just to make sure
-     that simple_type does depend on it. Otherwise, the coercion defined
-     bellow will not be acceptable by Coq. *)
-  Record simple_type `{typeG Σ} :=
-    { st_own : thread_id → list val → iProp Σ;
-
-      st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
-      st_own_persistent tid vl : PersistentP (st_own tid vl) }.
-
-  Global Existing Instance st_own_persistent.
-
-  Program Definition ty_of_st (st : simple_type) : type :=
-    {| ty_size := 1; ty_own := st.(st_own);
-
-       (* [st.(st_own) tid vl] needs to be outside of the fractured
-          borrow, otherwise I do not know how to prove the shr part of
-          [subtype_shr_mono]. *)
-       ty_shr := λ κ tid l,
-                 (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
-                        ▷ st.(st_own) tid vl)%I
-    |}.
-  Next Obligation. intros. apply st_size_eq. Qed.
-  Next Obligation.
-    iIntros (st E κ l tid ??) "#LFT Hmt Hκ".
-    iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
-    iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
-    iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
-    - iFrame "Hκ". iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
-      { iExists vl. iFrame. auto. }
-      done. set_solver.
-    - iExFalso. iApply (lft_tok_dead with "Hκ"). done.
-  Qed.
-  Next Obligation.
-    intros st κ κ' tid l. iIntros "#LFT #Hord H".
-    iDestruct "H" as (vl) "[#Hf #Hown]".
-    iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
-  Qed.
-
-  Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
-  Next Obligation.
-    intros st κ tid E ? l q ? HF. iIntros "#LFT #Hshr Htok Hlft".
-    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
-    iDestruct "Hshr" as (vl) "[Hf Hown]".
-    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
-    iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
-    - iNext. iExists _. by iFrame.
-    - iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
-      iDestruct ("Htok" with "Htok2") as "$".
-      iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
-      { iNext. iDestruct (st_size_eq with "Hown") as %->.
-        iDestruct (st_size_eq with "Hown'") as %->. done. }
-      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
-      iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
-  Qed.
-
-  Global Instance ty_of_st_sync st :
-    Send (ty_of_st st) → Sync (ty_of_st st).
-  Proof.
-    iIntros (Hsend κ tid1 tid2 l) "H". iDestruct "H" as (vl) "[Hm Hown]".
-    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
-  Qed.
-End type.
-
-Coercion ty_of_st : simple_type >-> type.
-
-Delimit Scope lrust_type_scope with T.
-Bind Scope lrust_type_scope with type.
-
-(* OFE and COFE structures on types and simple types. *)
-Section ofe.
-  Context `{typeG Σ}.
-
-  Section def.
-    Definition tuple_of_type (ty : type) : prodC (prodC _ _) _ :=
-      (ty.(ty_size),
-       Next (ty.(ty_own) : _ -c> _ -c> _),
-       ty.(ty_shr) :  _ -c> _ -c> _ -c> _).
-
-    Instance type_equiv : Equiv type := λ ty1 ty2,
-       tuple_of_type ty1 ≡ tuple_of_type ty2.
-    Instance type_dist : Dist type := λ n ty1 ty2,
-       tuple_of_type ty1 ≡{n}≡ tuple_of_type ty2.
-
-    Definition type_ofe_mixin : OfeMixin type.
-    Proof.
-      split; [|split|]; unfold equiv, dist, type_equiv, type_dist.
-      - intros. apply equiv_dist.
-      - by intros ?.
-      - by intros ???.
-      - by intros ???->.
-      - by intros ????; apply dist_S.
-    Qed.
-
-    Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
-
-    Instance st_equiv : Equiv simple_type := λ st1 st2,
-      @Next (_ -c> _ -c> _) st1.(st_own) ≡ @Next (_ -c> _ -c> _) st2.(st_own).
-    Instance st_dist : Dist simple_type := λ n st1 st2,
-      @Next (_ -c> _ -c> _) st1.(st_own) ≡{n}≡ @Next (_ -c> _ -c> _) st2.(st_own).
-
-    Definition st_ofe_mixin : OfeMixin simple_type.
-    Proof.
-      split; [|split|]; unfold equiv, dist, st_equiv, st_dist.
-      - intros. apply equiv_dist.
-      - by intros ?.
-      - by intros ???.
-      - by intros ???->.
-      - by intros ????; apply dist_S.
-    Qed.
-
-    Canonical Structure simple_typeC : ofeT := OfeT simple_type st_ofe_mixin.
-  End def.
-
-  Lemma st_dist_unfold n (x y : simple_type) :
-    x ≡{n}≡ y ↔
-      @Next (_ -c> _ -c> _) x.(st_own) ≡{n}≡ @Next (_ -c> _ -c> _) y.(st_own).
-  Proof. done. Qed.
-
-  Global Instance ty_size_proper_d n:
-    Proper (dist n ==> eq) ty_size.
-  Proof. intros ?? EQ. apply EQ. Qed.
-  Global Instance ty_size_proper_e :
-    Proper ((≡) ==> eq) ty_size.
-  Proof. intros ?? EQ. apply EQ. Qed.
-  Global Instance ty_own_ne n:
-    Proper (dist (S n) ==> eq ==> eq ==> dist n) ty_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
-  Global Instance ty_own_proper_e:
-    Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
-  Global Instance ty_shr_ne n:
-    Proper (dist n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
-  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
-  Global Instance ty_shr_proper_e :
-    Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
-  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
-  Global Instance st_own_ne n:
-    Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
-  Global Instance st_own_proper_e :
-    Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
-
-  Global Program Instance type_cofe : Cofe typeC :=
-    {| compl c :=
-         let '(ty_size, Next ty_own, ty_shr) :=
-             compl {| chain_car := tuple_of_type ∘ c |}
-         in
-         {| ty_size := ty_size; ty_own := ty_own; ty_shr := ty_shr |}
-    |}.
-  Next Obligation. intros [c Hc]. apply Hc. Qed.
-  Next Obligation.
-    simpl. intros c _ _ shr [=_ _ ->] κ tid l.
-    apply uPred.equiv_entails, equiv_dist=>n.
-    by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=
-               uPred.always_always.
-  Qed.
-  Next Obligation.
-    simpl. intros c sz own _ [=-> -> _] tid vl.
-    apply uPred.entails_equiv_and, equiv_dist=>n.
-    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /= conv_compl /=.
-    apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
-  Qed.
-  Next Obligation.
-    simpl. intros c _ own shr [=_ -> ->] E κ l tid q ?.
-    apply uPred.entails_equiv_and, equiv_dist=>n.
-    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=.
-    setoid_rewrite (λ c vl, conv_compl (A:=_ -c> _ -c> _) n c tid vl). simpl.
-    etrans. { by apply equiv_dist, uPred.entails_equiv_and, (c n).(ty_share). }
-    simpl. destruct n; repeat (simpl; (f_contractive || f_equiv)).
-    rewrite (c.(chain_cauchy) (S n) (S (S n))) //. lia.
-  Qed.
-  Next Obligation.
-    simpl. intros c _ _ shr [=_ _ ->] κ κ' tid l.
-    apply uPred.entails_equiv_and, equiv_dist=>n.
-    rewrite !(λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c _ tid l) /=.
-    apply equiv_dist, uPred.entails_equiv_and. apply ty_shr_mono.
-  Qed.
-  Next Obligation.
-    intros n c. split; [split|]; simpl; try by rewrite conv_compl.
-    set (c n). f_contractive. rewrite conv_compl //.
-  Qed.
-
-  Global Instance ty_of_st_ne n : Proper (dist n ==> dist n) ty_of_st.
-  Proof.
-    intros [][]EQ. split;[split|]=>//= κ tid l.
-    repeat (f_contractive || f_equiv). apply EQ.
-  Qed.
-End ofe.
-
-Section subtyping.
-  Context `{typeG Σ}.
-  Definition type_incl (ty1 ty2 : type) : iProp Σ :=
-    (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
-     (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
-     (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
-
-  Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
-  (*  Typeclasses Opaque type_incl. *)
-
-  Lemma type_incl_refl ty : type_incl ty ty.
-  Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
-
-  Lemma type_incl_trans ty1 ty2 ty3 :
-    type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
-  Proof.
-    (* TODO: this iIntros takes suspiciously long. *)
-    iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
-    iSplit; first (iPureIntro; etrans; done).
-    iSplit; iAlways; iIntros.
-    - iApply "Ho23". iApply "Ho12". done.
-    - iApply "Hs23". iApply "Hs12". done.
-  Qed.
-
-  Context (E : elctx) (L : llctx).
-
-  Definition subtype (ty1 ty2 : type) : Prop :=
-    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-            type_incl ty1 ty2.
-
-  Lemma subtype_refl ty : subtype ty ty.
-  Proof. iIntros. iApply type_incl_refl. Qed.
-
-  Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
-  Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
-
-  Global Instance subtype_preorder : PreOrder subtype.
-  Proof.
-    split; first by intros ?; apply subtype_refl.
-    intros ty1 ty2 ty3 H12 H23. iIntros.
-    iApply (type_incl_trans with "[] []").
-    - iApply (H12 with "[] []"); done.
-    - iApply (H23 with "[] []"); done.
-  Qed.
-
-  (* TODO: The prelude should have a symmetric closure. *)
-  Definition eqtype (ty1 ty2 : type) : Prop :=
-    subtype ty1 ty2 ∧ subtype ty2 ty1.
-
-  Lemma eqtype_unfold ty1 ty2 :
-    eqtype ty1 ty2 ↔
-    (lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-      (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
-      (□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
-      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ↔ ty2.(ty_shr) κ tid l))%I).
-  Proof.
-    split.
-    - iIntros ([EQ1 EQ2]) "#LFT #HE #HL".
-      iDestruct (EQ1 with "LFT HE HL") as "[#Hsz [#H1own #H1shr]]".
-      iDestruct (EQ2 with "LFT HE HL") as "[_ [#H2own #H2shr]]".
-      iSplit; last iSplit.
-      + done.
-      + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
-      + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
-    - intros EQ. split; iIntros "#LFT #HE #HL"; (iSplit; last iSplit);
-      iDestruct (EQ with "LFT HE HL") as "[% [#Hown #Hshr]]".
-      + done.
-      + iIntros "!#* H". by iApply "Hown".
-      + iIntros "!#* H". by iApply "Hshr".
-      + done.
-      + iIntros "!#* H". by iApply "Hown".
-      + iIntros "!#* H". by iApply "Hshr".
-  Qed.
-
-  Lemma eqtype_refl ty : eqtype ty ty.
-  Proof. by split. Qed.
-
-  Lemma equiv_eqtype ty1 ty2 : ty1 ≡ ty2 → eqtype ty1 ty2.
-  Proof. by split; apply equiv_subtype. Qed.
-
-  Global Instance subtype_proper :
-    Proper (eqtype ==> eqtype ==> iff) subtype.
-  Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
-
-  Global Instance eqtype_equivalence : Equivalence eqtype.
-  Proof.
-    split.
-    - by split.
-    - intros ?? Heq; split; apply Heq.
-    - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
-  Qed.
-
-  Lemma subtype_simple_type (st1 st2 : simple_type) :
-    (∀ tid vl, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-                 st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
-    subtype st1 st2.
-  Proof.
-    intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
-    - iIntros. iApply (Hst with "* [] [] []"); done.
-    - iIntros (???) "H".
-      iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
-      by iApply (Hst with "* [] [] []").
-  Qed.
-End subtyping.
-
-Section weakening.
-  Context `{typeG Σ}.
-
-  Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
-    E1 `contains` E2 → L1 `contains` L2 →
-    subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
-  Proof.
-    (* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
-    iIntros (HE12 [L' HL12]%contains_Permutation Hsub) "#LFT HE HL".
-    iApply (Hsub with "LFT [HE] [HL]").
-    - rewrite /elctx_interp_0. by iApply big_sepL_contains.
-    - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
-      rewrite HL12. set_solver.
-  Qed.
-
-End weakening.
-
-Hint Resolve subtype_refl eqtype_refl : lrust_typing.

theories/typing/type_sum.v

-From iris.proofmode Require Import tactics.
-From lrust.lang Require Import heap memcpy.
-From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
-From lrust.typing Require Import lft_contexts type_context programs product.
-Set Default Proof Using "Type".
-
-Section case.
-  Context `{typeG Σ}.
-
-  (* FIXME : the doc does not give [p +ₗ #(S (ty.(ty_size))) ◁ ...]. *)
-  Lemma type_case_own E L C T p n tyl el :
-    Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
-         (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
-  Proof.
-    iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
-    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
-    iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
-    iDestruct "H↦" as (vl) "[H↦ Hown]".
-    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
-    simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
-    rewrite -Nat.add_1_l app_length -!freeable_sz_split
-            heap_mapsto_vec_cons heap_mapsto_vec_app.
-    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
-    iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
-    rewrite nth_lookup.
-    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
-    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
-    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
-    destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
-    - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
-      iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
-      + rewrite shift_loc_0. iExists _. iFrame. iSplit. done. iExists [ #i].
-        rewrite heap_mapsto_vec_singleton.
-        iFrame. iExists [_], []. auto.
-      + iExists _. iFrame. iSplit. done. iExists _. iFrame.
-      + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
-        iExists _. iFrame. iSplit. done. iExists _. iFrame. rewrite uninit_own. auto.
-    - iExists _. iSplit. done.
-      assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.
-      rewrite -EQlen app_length -freeable_sz_split. iFrame.
-      iExists (#i :: vl' ++ vl''). iNext.
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
-      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
-  Qed.
-
-  Lemma type_case_own' E L C T T' p n tyl el :
-    tctx_extract_hasty E L p (own n (sum tyl)) T T' →
-    Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
-         (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T') e) tyl el →
-    typed_body E L C T (case: !p of el).
-  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_own. Qed.
-
-  Lemma type_case_uniq E L C T p κ tyl el :
-    lctx_lft_alive E L κ →
-    Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
-  Proof.
-    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
-    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
-    iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
-    iMod (bor_iff with "LFT HP Hb") as "Hb". done.
-    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
-    iMod (bor_acc_cons with "LFT Hb Htok") as "[H↦ Hclose']". done.
-    iDestruct "H↦" as (vl) "[H↦ Hown]".
-    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
-    iDestruct "EQlen" as %[=EQlen].
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_app nth_lookup.
-    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
-    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
-    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
-    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
-    iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
-    destruct Hety as [Hety|Hety].
-    - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
-            with "[H↦vl' Hown] [H↦i H↦vl'']") as "[Hb Htok]".
-      { iExists vl'. iFrame. }
-      { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
-        iExists (#i::vl'2++vl''). iIntros "!>". iNext.
-        iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
-        iFrame. iExists _, _, _. iSplit. by auto.
-        rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
-      iMod ("Hclose" with "Htok") as "[HE HL]".
-      iApply (Hety with "HEAP LFT Hna HE HL HC").
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
-      iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
-    - iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
-        [|by iIntros "!>$"|].
-      { iExists (#i::vl'++vl'').
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
-        iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
-      iMod ("Hclose" with "Htok") as "[HE HL]".
-      iApply (Hety with "HEAP LFT Hna HE HL HC").
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
-      iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
-  Qed.
-
-  Lemma type_case_uniq' E L C T T' p κ tyl el :
-    tctx_extract_hasty E L p (&uniq{κ}sum tyl) T T' →
-    lctx_lft_alive E L κ →
-    Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
-      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
-    typed_body E L C T (case: !p of el).
-  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_uniq. Qed.
-
-  Lemma type_case_shr E L C T p κ tyl el:
-    lctx_lft_alive E L κ →
-    Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
-  Proof.
-    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
-    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
-    iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
-    iDestruct "Hl" as (i) "[#Hb Hshr]".
-    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
-    iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
-    rewrite nth_lookup.
-    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hshr" as "[]".
-    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
-    wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
-    iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
-    iMod ("Hclose" with "Htok") as "[HE HL]".
-    destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
-    - iExists _. auto.
-    - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
-  Qed.
-
-  Lemma type_case_shr' E L C T p κ tyl el :
-    (p ◁ &shr{κ}sum tyl)%TC ∈ T →
-    lctx_lft_alive E L κ →
-    Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
-    typed_body E L C T (case: !p of el).
-  Proof.
-    intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
-    apply type_case_shr; first done. eapply Forall2_impl; first done. auto.
-  Qed.
-
-  Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :
-    tyl !! i = Some ty →
-    typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
-  Proof.
-    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp".
-    rewrite tctx_interp_cons tctx_interp_singleton.
-    iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
-    iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
-    iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "* [] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
-    destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
-    wp_write. iApply wp_seq. done. iNext. wp_bind p1.
-    iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
-    iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
-    iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
-    destruct vl as [|? vl].
-    { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
-      - intros [= ->]. simpl in *. lia.
-      - apply IHtyl. simpl in *. lia. }
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
-    rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
-    iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
-    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
-  Qed.
-
-  Lemma type_sum_assign_unit {E L} (i : nat) tyl ty1 ty2 p :
-    tyl !! i = Some unit →
-    typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
-  Proof.
-    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
-    iMod (Hw with "* [] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
-    simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
-    wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
-    iApply "Hw". iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
-    iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
-  Qed.
-
-  Lemma type_sum_memcpy {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
-    tyl !! i = Some ty →
-    typed_write E L ty1 (sum tyl) ty1' →
-    typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
-               (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
-  Proof.
-    iIntros (Hty Hw Hr) "!# * #HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
-    rewrite tctx_interp_cons tctx_interp_singleton.
-    iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
-    iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
-    iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "* [] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
-    destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
-    iApply wp_seq. done. iNext. wp_bind p1.
-    iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
-    wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
-    iMod (Hr with "* [] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
-    assert (ty.(ty_size) ≤ length vl1).
-    { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
-      - intros [= ->]. lia.
-      - specialize (IHtyl i). intuition lia. }
-    rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
-    iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
-    iAssert (▷ ⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%". by rewrite -ty_size_eq.
-    iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); try done.
-    { rewrite take_length. lia. }
-    iNext; iIntros "[H↦vl1 H↦2]".
-    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-    iMod ("Hr" with "H↦2") as "($ & $ & $ & $)". iApply "Hw". iNext.
-    rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
-    iSplitL "H↦pad".
-    - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
-      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
-    - iExists _. iFrame.
-  Qed.
-End case.

theories/typing/uninit.v

-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.typing Require Import product.
-Set Default Proof Using "Type".
-
-Section uninit.
-  Context `{typeG Σ}.
-
-  Program Definition uninit_1 : type :=
-    {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
-  Next Obligation. done. Qed.
-
-  Global Instance uninit_1_send : Send uninit_1.
-  Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
-
-  Definition uninit0 (n : nat) : type :=
-    Π (replicate n uninit_1).
-
-  Lemma uninit0_sz n : ty_size (uninit0 n) = n.
-  Proof. induction n. done. simpl. by f_equal. Qed.
-
-  (* We redefine uninit as an alias of uninit0, so that the size
-     computes directly to [n] *)
-  Program Definition uninit (n : nat) : type :=
-    {| ty_size := n; ty_own := (uninit0 n).(ty_own);
-       ty_shr := (uninit0 n).(ty_shr) |}.
-  Next Obligation. intros. by rewrite ty_size_eq uninit0_sz. Qed.
-  Next Obligation. intros. by apply ty_share. Qed.
-  Next Obligation. intros. by apply ty_shr_mono. Qed.
-
-  Global Instance uninit_copy n : Copy (uninit n).
-  Proof.
-    destruct (product_copy (replicate n uninit_1)) as [A B].
-      by apply Forall_replicate, _.
-    rewrite uninit0_sz in B. by split.
-  Qed.
-
-  Global Instance uninit_send n : Send (uninit n).
-  Proof. apply product_send, Forall_replicate, _. Qed.
-
-  Global Instance uninit_sync n : Sync (uninit n).
-  Proof. apply product_sync, Forall_replicate, _. Qed.
-
-  Lemma uninit_uninit0_eqtype E L n :
-    eqtype E L (uninit0 n) (uninit n).
-  Proof. apply equiv_eqtype; (split; first split)=>//=. apply uninit0_sz. Qed.
-
-  Lemma uninit_product_eqtype E L ns :
-    eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
-  Proof.
-    rewrite -uninit_uninit0_eqtype. etrans; last first.
-    { apply product_proper. eapply Forall2_fmap, Forall_Forall2, Forall_forall.
-      intros. by rewrite -uninit_uninit0_eqtype. }
-    induction ns as [|n ns IH]=>//=. revert IH.
-    by rewrite /= /uninit0 replicate_plus prod_flatten_l -!prod_app=>->.
-  Qed.
-  Lemma uninit_product_eqtype' E L ns :
-    eqtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
-  Proof. symmetry; apply uninit_product_eqtype. Qed.
-  Lemma uninit_product_subtype E L ns :
-    subtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
-  Proof. apply uninit_product_eqtype'. Qed.
-  Lemma uninit_product_subtype' E L ns :
-    subtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
-  Proof. apply uninit_product_eqtype. Qed.
-
-  Lemma uninit_own n tid vl :
-    (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
-  Proof.
-    iSplit.
-    - rewrite ty_size_eq. auto.
-    - iInduction vl as [|v vl] "IH" forall (n).
-      + iIntros "%". destruct n; done.
-      + iIntros (Heq). destruct n; first done. simpl.
-        iExists [v], vl. iSplit; first done. iSplit; first done.
-        iApply "IH". by inversion Heq.
-  Qed.
-End uninit.
-
-Hint Resolve uninit_product_eqtype uninit_product_eqtype'
-     uninit_product_subtype uninit_product_subtype' : lrust_typing.

theories/typing/uniq_bor.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From lrust.lang Require Import heap.
-From lrust.typing Require Export type.
-From lrust.typing Require Import lft_contexts type_context shr_bor programs.
-Set Default Proof Using "Type".
-
-Section uniq_bor.
-  Context `{typeG Σ}.
-
-  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
-
-  Program Definition uniq_bor (κ:lft) (ty:type) :=
-    {| ty_size := 1;
-       (* We quantify over [P]s so that the Proper lemma
-          (wrt. subtyping) works without an update.
-
-          An obvious alternative definition would be to allow
-          an update in the ownership here, i.e. `|={lftE}=> &{κ} P`.
-          The trouble with this definition is that bor_unnest as proven is too
-          weak. The original unnesting with open borrows was strong enough. *)
-       ty_own tid vl :=
-         (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
-       ty_shr κ' tid l :=
-         (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ∪κ']
-                ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
-    |}.
-  Next Obligation.
-    iIntros (q ty tid vl) "H". iDestruct "H" as (l P) "[[% _] _]". by subst.
-  Qed.
-  Next Obligation.
-    move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
-    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (P) "Hb2". set_solver.
-    iMod (bor_sep with "LFT Hb2") as "[H Hb2]". set_solver.
-    iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HPiff] Htok]". set_solver.
-    iFrame "Htok". iExists l'.
-    subst. rewrite heap_mapsto_vec_singleton.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
-    rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
-          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb". solve_ndisj.
-      { iApply bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (bor_iff with "LFT [] Hb") as "Hb". solve_ndisj.
-      { by eauto. }
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". solve_ndisj.
-      iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod ("Hclose" with "[]") as "_". by eauto.
-      iApply step_fupd_intro. set_solver. auto.
-  Qed.
-  Next Obligation.
-    intros κ0 ty κ κ' tid l. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
-    { iApply (lft_incl_glb with "[] []").
-      - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
-      - iApply (lft_incl_trans with "[] Hκ").
-        iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
-    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
-    iIntros "!# * % Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
-    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first set_solver.
-    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
-    iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-    by iApply (ty_shr_mono with "LFT Hκ0").
-  Qed.
-
-  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 [Hty1 Hty2]. iIntros. iSplit; first done.
-    iDestruct (Hty1 with "* [] [] []") as "(_ & #Ho1 & #Hs1)"; [done..|clear Hty1].
-    iDestruct (Hty2 with "* [] [] []") as "(_ & #Ho2 & #Hs2)"; [done..|clear Hty2].
-    iDestruct (Hκ with "[] []") as "#Hκ"; [done..|].
-    iSplit; iAlways.
-    - iIntros (??) "H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
-      iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
-      iNext. iIntros "!#". iSplit; iIntros "H".
-      + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
-        by iApply "Ho1".
-      + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
-        by iApply "Ho2".
-    - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
-      { iApply (lft_incl_glb with "[] []").
-        - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
-          apply gmultiset_union_subseteq_l.
-        - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
-      iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
-      iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
-      iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
-      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
-  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_contractive κ : Contractive (uniq_bor κ).
-  Proof.
-    intros n ?? EQ. split; [split|]; simpl.
-    - done.
-    - destruct n=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
-    - intros κ' tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
-  Global Instance uniq_ne κ n : Proper (dist n ==> dist n) (uniq_bor κ).
-  Proof. apply contractive_ne, _. Qed.
-
-  Global Instance uniq_send κ ty :
-    Send ty → Send (uniq_bor κ ty).
-  Proof.
-    iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l P) "[[% #HPiff] H]".
-    iExists _, _. iFrame "H". iSplit; first done. iNext. iAlways. iSplit.
-    - iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
-      { by iApply "HPiff". }
-      clear dependent vl. iIntros (vl) "?". by iApply Hsend.
-    - iIntros "HP". iApply "HPiff". iApply (heap_mapsto_pred_wand with "HP").
-      clear dependent vl. iIntros (vl) "?". 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{ κ } ty" := (uniq_bor κ ty)
-  (format "&uniq{ κ } ty", at level 20, right associativity) : 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_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 !big_sepL_singleton /=.
-    iDestruct "Huniq" as (v) "[% Huniq]".
-    iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
-    iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
-    iIntros "!>/=". eauto.
-  Qed.
-
-  Lemma tctx_reborrow_uniq E L p ty κ κ' :
-    lctx_lft_incl E L κ' κ →
-    tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
-  Proof.
-    iIntros (Hκκ' tid ??) "#LFT HE HL H".
-    iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
-    iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
-    iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
-    iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
-    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
-    - iExists _. iSplit. done. iIntros "#H†". iMod ("Hext" with "H†") as "Hb".
-      iExists _, _. erewrite <-uPred.iff_refl. eauto.
-  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_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 (v tid F qE qL ?) "#LFT Htl HE HL Hown".
-    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
-    iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
-    iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
-    iMod (bor_acc with "LFT H↦ Hκ") as "[H↦ Hclose']"; first set_solver.
-    iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-     { by iApply ty.(ty_size_eq). }
-    iIntros "!>". iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
-    iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
-    iMod ("Hclose" with "Htok") as "($ & $ & $)".
-    iExists _, _. erewrite <-uPred.iff_refl. auto.
-  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 (p tid F qE qL ?) "#LFT HE HL Hown".
-    iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
-    iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
-    iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
-    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 "[Hbor Htok]". by iExists _; iFrame.
-    iMod ("Hclose" with "Htok") as "($ & $ & $)".
-    iExists _, _. erewrite <-uPred.iff_refl. auto.
-  Qed.
-End typing.
-
-Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share
-             tctx_extract_hasty_reborrow : lrust_typing.
-Hint Resolve tctx_extract_hasty_share_samelft | 0 : lrust_typing.