theories/typing/examples/unbox.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unbox.
-  Context `{typeG Σ}.
-
-  Definition unbox : val :=
-    funrec: <> ["b"] :=
-       let: "b'" := !"b" in let: "bx" := !"b'" in
-       letalloc: "r" <- "bx" +ₗ #0 in
-       delete [ #1; "b"] ;; "return" ["r"].
-
-  Lemma ubox_type :
-    typed_instruction_ty [] [] [] unbox
-        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}box (Π[int; int]))]) (λ α, box (&uniq{α} int))).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-    intros b'; simpl_subst.
-    eapply type_deref_uniq_own; [solve_typing..|]=>bx; simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End unbox.

theories/typing/examples/unwrap_or.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unwrap_or.
-  Context `{typeG Σ}.
-
-  Definition unwrap_or τ : val :=
-    funrec: <> ["o"; "def"] :=
-      case: !"o" of
-      [ delete [ #(S τ.(ty_size)); "o"];; "return" ["def"];
-        letalloc: "r" <-{τ.(ty_size)} !("o" +ₗ #1) in
-        delete [ #(S τ.(ty_size)); "o"];; delete [ #τ.(ty_size); "def"];; "return" ["r"]].
-
-  Lemma unwrap_or_type τ :
-    typed_instruction_ty [] [] [] (unwrap_or τ)
-        (fn (λ _, [])%EL (λ _, [# box (Σ[unit; τ]); box τ]) (λ _:(), box τ)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
-    eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
-    + right. eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-    + left. eapply type_letalloc_n; [solve_typing..|by apply read_own_move|solve_typing|]=>r.
-        simpl_subst.
-      eapply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-  Qed.
-End unwrap_or.

theories/typing/fixpoint.v

-From lrust.lang Require Import proofmode.
-From lrust.typing Require Export lft_contexts type bool.
-Set Default Proof Using "Type".
-
-Section fixpoint.
-  Context `{typeG Σ}.
-
-  Global Instance type_inhabited : Inhabited type := populate bool.
-
-  Context (T : type → type) `{Contractive T}.
-
-  Global Instance fixpoint_copy :
-    (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ??[[EQsz%leibniz_equiv EQown]EQshr].
-      specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
-      simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
-      + revert Hp. by rewrite /PersistentP -EQown.
-      + intros F l q. rewrite -EQsz -EQshr. setoid_rewrite <-EQown. auto.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc. split.
-      + intros tid vl. apply uPred.equiv_entails, equiv_dist=>n.
-        by rewrite conv_compl uPred.always_always.
-      + intros κ tid E F l q ? ?.
-        apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
-        { apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
-            by rewrite -conv_compl. }
-        symmetry.               (* FIXME : this is too slow *)
-        do 2 f_equiv; first by rewrite conv_compl. set (cn:=c n).
-        repeat (apply (conv_compl n c) || f_contractive || f_equiv);
-          by rewrite conv_compl.
-  Qed.
-
-  Global Instance fixpoint_send :
-    (∀ `(!Send ty), Send (T ty)) → Send (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ????. by rewrite -EQ.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc ???. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
-  Qed.
-
-  Global Instance fixpoint_sync :
-    (∀ `(!Sync ty), Sync (T ty)) → Sync (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ?????. by rewrite -EQ.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc ????. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
-  Qed.
-
-  Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
-  Proof.
-    unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
-    split; iIntros "_ _ _"; (iSplit; first done); iSplit; iIntros "!#*$".
-  Qed.
-End fixpoint.
-
-Section subtyping.
-  Context `{typeG Σ} (E : elctx) (L : llctx).
-
-  (* TODO : is there a way to declare these as a [Proper] instances ? *)
-  Lemma fixpoint_mono T1 `{Contractive T1} T2 `{Contractive T2} :
-    (∀ ty1 ty2, subtype E L ty1 ty2 → subtype E L (T1 ty1) (T2 ty2)) →
-    subtype E L (fixpoint T1) (fixpoint T2).
-  Proof.
-    intros H12. apply fixpoint_ind.
-    - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
-    - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc.
-      assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
-      assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
-      iIntros "LFT HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "LFT HE HL").
-      + iApply (Hown with "LFT HE HL").
-      + iApply (Hshr with "LFT HE HL").
-  Qed.
-
-  Lemma fixpoint_proper T1 `{Contractive T1} T2 `{Contractive T2} :
-    (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
-    eqtype E L (fixpoint T1) (fixpoint T2).
-  Proof.
-    intros H12. apply fixpoint_ind.
-    - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
-    - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. setoid_rewrite eqtype_unfold in Hc. rewrite eqtype_unfold.
-      assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
-      assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl ↔ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l ↔ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
-      iIntros "LFT HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "LFT HE HL").
-      + iApply (Hown with "LFT HE HL").
-      + iApply (Hshr with "LFT HE HL").
-  Qed.
-
-  Lemma fixpoint_unfold_subtype_l ty T `{Contractive T} :
-    subtype E L ty (T (fixpoint T)) → subtype E L ty (fixpoint T).
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_subtype_r ty T `{Contractive T} :
-    subtype E L (T (fixpoint T)) ty → subtype E L (fixpoint T) ty.
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_l ty T `{Contractive T} :
-    eqtype E L ty (T (fixpoint T)) → eqtype E L ty (fixpoint T).
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_r ty T `{Contractive T} :
-    eqtype E L (T (fixpoint T)) ty → eqtype E L (fixpoint T) ty.
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-End subtyping.
-
-Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
-
-(* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
-   not been tried before, so we give them a high cost *)
-Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.

theories/typing/function.v

-From iris.base_logic Require Import big_op.
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import vector.
-From lrust.typing Require Export type.
-From lrust.typing Require Import programs cont.
-Set Default Proof Using "Type".
-
-Section fn.
-  Context `{typeG Σ} {A : Type} {n : nat}.
-
-  Program Definition fn (E : A → elctx)
-          (tys : A → vec type n) (ty : A → type) : type :=
-    {| st_own tid vl := (∃ fb kb xb e H,
-         ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-         ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
-            typed_body (E x) []
-                       [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                       (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
-                       (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
-  Next Obligation.
-    iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
-  Qed.
-
-  Global Instance fn_send E tys ty : Send (fn E tys ty).
-  Proof. iIntros (tid1 tid2 vl). done. Qed.
-
-  Lemma fn_contractive n' E :
-    Proper (pointwise_relation A (dist_later n') ==>
-            pointwise_relation A (dist_later n') ==> dist n') (fn E).
-  Proof.
-    intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
-    f_contractive=>tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive. do 18 f_equiv.
-    - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
-    - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
-      assert (Hprop : ∀ n tid p i, Proper (dist (S n) ==> dist n)
-        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I);
-        last by apply Hprop, Htys.
-      clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
-      specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
-        inversion_clear Hxy; last done.
-      transitivity (tctx_elt_interp tid (p ◁ tyx));
-        last transitivity (tctx_elt_interp tid (p ◁ tyy)); last 2 first.
-      + unfold tctx_elt_interp. do 3 f_equiv. by apply ty_own_ne.
-      + apply equiv_dist. iSplit.
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
-        * iIntros "H". by iApply "H".
-      + apply equiv_dist. iSplit.
-        * iIntros "H". by iApply "H".
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
-  Qed.
-  Global Existing Instance fn_contractive.
-
-  Global Instance fn_ne n' E :
-    Proper (pointwise_relation A (dist n') ==>
-            pointwise_relation A (dist n') ==> dist n') (fn E).
-  Proof.
-    intros ?? H1 ?? H2.
-    apply fn_contractive=>u; (destruct n'; [done|apply dist_S]);
-      [apply (H1 u)|apply (H2 u)].
-  Qed.
-End fn.
-
-Section typing.
-  Context `{typeG Σ}.
-
-  Lemma fn_subtype_full {A n} E0 L0 E E' (tys tys' : A → vec type n) ty ty' :
-    (∀ x, elctx_incl E0 L0 (E x) (E' x)) →
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys' x) (tys x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty x) (ty' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
-  Proof.
-    intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
-    rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
-    iDestruct (elctx_interp_persist with "HE") as "#HEp".
-    iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
-    iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
-    - iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
-      iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
-      iMod ("Hclose" with "HE'") as "HE".
-      iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
-      iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] * Htl HL >").
-      { by apply elem_of_list_singleton. }
-      rewrite /tctx_interp !big_sepL_singleton /=.
-      iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
-      iDestruct (Hty x with "LFT [HE0 HEp] HL0") as "(_ & #Hty & _)".
-      { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
-      by iApply "Hty".
-    - rewrite /tctx_interp
-         -(fst_zip (tys x) (tys' x)) ?vec_to_list_length //
-         -{1}(snd_zip (tys x) (tys' x)) ?vec_to_list_length //
-         !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
-      iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
-      iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
-      iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
-      rewrite !lookup_zip_with.
-      iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
-        (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
-      specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
-      iDestruct (Htys with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
-      + rewrite /elctx_interp_0 big_sepL_app. by iSplit.
-      + by iApply "Ho".
-  Qed.
-
-  Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x) (tys1 x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
-    subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
-  Proof. intros. by apply fn_subtype_full. Qed.
-
-  (* This proper and the next can probably not be inferred, but oh well. *)
-  Global Instance fn_subtype_ty' {A n} E0 L0 E :
-    Proper (flip (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (subtype E0 L0) v1 v2)) ==>
-            pointwise_relation A (subtype E0 L0) ==> subtype E0 L0) (fn E).
-  Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
-    - intros. eapply Forall2_impl; first eapply Htys. intros ??.
-      eapply subtype_weaken; last done. by apply submseteq_inserts_r.
-    - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
-  Qed.
-
-  Global Instance fn_eqtype_ty' {A n} E0 L0 E :
-    Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
-            pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
-  Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
-      intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
-  Qed.
-
-  Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
-    (∀ x, elctx_sat (E x) [] (E' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys ty).
-  Proof.
-    intros. apply fn_subtype_full; try done. by intros; apply elctx_sat_incl.
-  Qed.
-
-  Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
-    lctx_lft_incl E0 L0 κ κ' →
-    subtype E0 L0 (fn (λ x, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
-  Proof.
-    intros Hκκ'. apply fn_subtype_full; try done. intros.
-    apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
-    iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
-    rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
-  Qed.
-
-  Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
-    subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
-  Proof.
-    apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
-    rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
-  Qed.
-
-  Lemma type_call' {A} E L E' T p (ps : list path)
-                         (tys : A → vec type (length ps)) ty k x :
-    elctx_sat E L (E' x) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
-               ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
-               (call: p ps → k).
-  Proof.
-    iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
-    rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
-    wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
-               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ ty)) (tys x))%I
-            with "* [Hargs]"); first wp_done.
-    - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
-      clear dependent ty k p.
-      rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
-              (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
-      iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
-      iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
-    - simpl. change (@length expr ps) with (length ps).
-      iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
-      iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
-      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl tys.
-      rewrite <-EQl=>vl tys. iApply wp_rec; try done.
-      { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-      { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
-      iNext. iSpecialize ("Hf" $! x k vl).
-      iMod (HE with "HE HL") as (q') "[HE' Hclose]"; first done.
-      iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT]").
-      + by rewrite /llctx_interp big_sepL_nil.
-      + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
-        iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
-        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ Hret".
-        iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! args with "Htl HL").
-        rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
-      + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
-                (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
-        iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
-  Qed.
-
-  Lemma type_call {A} x E L E' C T T' T'' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty k :
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
-    (k ◁cont(L, T''))%CC ∈ C →
-    (∀ ret : val, tctx_incl E L ((ret ◁ ty x)::T') (T'' [# ret])) →
-    typed_body E L C T (call: p ps → k).
-  Proof.
-    intros Hfn HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
-    - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
-      apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
-    - etrans; last by apply (tctx_incl_frame_l [_]).
-      apply copy_elem_of_tctx_incl; last done. apply _.
-  Qed.
-
-  Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty b e :
-    Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ ty x)::T') (subst' b ret e)) →
-    typed_body E L C T (letcall: b := p ps in e).
-  Proof.
-    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ ty x) :: T')%TC).
-    - (* TODO : make [solve_closed] work here. *)
-      eapply is_closed_weaken; first done. set_solver+.
-    - (* TODO : make [solve_closed] work here. *)
-      rewrite /Closed /= !andb_True. split.
-      + by eapply is_closed_weaken, list_subseteq_nil.
-      + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
-        intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
-    - intros.
-      (* TODO : make [simpl_subst] work here. *)
-      change (subst' "_k" k (p (Var "_k" :: ps))) with
-             ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
-      rewrite is_closed_nil_subst //.
-      assert (map (subst "_k" k) ps = ps) as ->.
-      { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
-      eapply type_call; try done. constructor. done.
-    - move=>/= k ret. inv_vec ret=>ret. rewrite /subst_v /=.
-      rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
-      apply subst'_is_closed; last done. apply is_closed_of_val.
-  Qed.
-
-  Lemma type_rec {A} E L E' fb (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
-        T `{!CopyC T, !SendC T} :
-    Closed (fb :b: "return" :b: argsb +b+ []) e →
-    (∀ x (f : val) k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                   ((f ◁ fn E' tys ty) ::
-                      zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                   (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty).
-  Proof.
-    iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value.
-    { simpl. rewrite ->(decide_left Hc). done. }
-    rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
-    { simpl. rewrite decide_left. done. }
-    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
-    iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
-    iApply (Hbody with "* HEAP LFT Htl HE HL HC").
-    rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
-    by iApply sendc_change_tid.
-  Qed.
-
-  Lemma type_fn {A} E L E' (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
-        T `{!CopyC T, !SendC T} :
-    Closed ("return" :b: argsb +b+ []) e →
-    (∀ x k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                   (zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                   (subst_v (BNamed "return" :: argsb) (k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: <> argsb := e) (fn E' tys ty).
-  Proof.
-    intros. apply type_rec; try done. intros. rewrite -typed_body_mono //=.
-    eapply contains_tctx_incl. by constructor.
-  Qed.
-End typing.
-
-Hint Resolve fn_subtype_full : lrust_typing.

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.
-
-(* We first try to solve everything without the merging rules, and
-   then start from scratch with them.
-
-   The reason is that we want we want the search proof search for
-   [tctx_extract_hasty] to suceed even if the type is an evar, and
-   merging makes it diverge in this case. *)
-Ltac solve_typing :=
-  (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
-  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-Create HintDb lrust_typing discriminated.
-Create HintDb lrust_typing_merge discriminated.
-
-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.
-
-Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : 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/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.
-
-  (** Copy types *)
-  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.
-
-  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 ⊆+ E2 → L1 ⊆+ 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]%submseteq_Permutation Hsub) "#LFT HE HL".
-    iApply (Hsub with "LFT [HE] [HL]").
-    - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
-    - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
-      rewrite HL12. set_solver.
-  Qed.
-End weakening.
-
-Hint Resolve subtype_refl eqtype_refl : lrust_typing.
-Hint Opaque subtype eqtype : lrust_typing.
\ No newline at end of file

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_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_singleton tctx_interp_cons tctx_interp_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]".
-    iDestruct (ty_size_eq with "Hown") as "#>%". 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' : lrust_typing.
-Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.

theories/typing/unsafe/cell.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From lrust.lang Require Import memcpy.
-From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Export type.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section cell.
-  Context `{typeG Σ}.
-  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
-
-  Program Definition cell (ty : type) :=
-    {| ty_size := ty.(ty_size);
-       ty_own := ty.(ty_own);
-       ty_shr κ tid l :=
-         (∃ P, ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid) ∗ &na{κ, tid, shrN.@l}P)%I |}.
-  Next Obligation. apply ty_size_eq. Qed.
-  Next Obligation.
-    iIntros (ty E κ l tid q ?) "#LFT Hown $". iExists _.
-    iMod (bor_na with "Hown") as "$". set_solver. iIntros "!>!>!#". iSplit; auto.
-  Qed.
-  Next Obligation.
-    iIntros (ty ?? tid l) "#LFT #H⊑ H". iDestruct "H" as (P) "[??]".
-    iExists _. iFrame. by iApply (na_bor_shorten with "H⊑").
-  Qed.
-
-  Global Instance cell_ne n : Proper (dist n ==> dist n) cell.
-  Proof.
-    intros ?? EQ. split; [split|]; simpl; try apply EQ.
-    intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
-
-  Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
-  Proof.
-    iIntros (?? EQ%eqtype_unfold) "#LFT #HE #HL".
-    iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
-    iSplit; [done|iSplit; iIntros "!# * H"].
-    - iApply ("Hown" with "H").
-    - iDestruct "H" as (P) "[#HP H]". iExists P. iFrame. iSplit; iNext; iIntros "!# H".
-      + iDestruct ("HP" with "H") as (vl) "[??]". iExists vl. iFrame. by iApply "Hown".
-      + iApply "HP". iDestruct "H" as (vl) "[??]". iExists vl. iFrame. by iApply "Hown".
-  Qed.
-  Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
-  Proof. eapply cell_mono. Qed.
-  Global Instance cell_proper E L : Proper (eqtype E L ==> eqtype E L) cell.
-  Proof. by split; apply cell_mono. Qed.
-  Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
-  Proof. eapply cell_proper. Qed.
-
-  Global Instance cell_copy :
-    Copy ty → Copy (cell ty).
-  Proof.
-    intros ty Hcopy. split; first by intros; simpl; apply _.
-    iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
-    iDestruct "Hshr" as (P) "[HP Hshr]".
-    (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
-    destruct (ty_size ty) as [|sz] eqn:Hsz.
-    { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
-      iDestruct ("HP" with "Hown") as (vl) "[H↦ #Hown]".
-      simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
-      iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
-      iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
-      { iApply "HP". iExists vl. by iFrame. }
-      iModIntro. iSplitL "".
-      { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
-        by iApply heap_mapsto_vec_nil. }
-      by iIntros "$ _". }
-    (* Now we are in the non-0 case. *)
-    iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(H & Htl & Hclose)"; [solve_ndisj..|].
-    iDestruct ("HP" with "H") as "$".
-    iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
-    iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
-    iMod ("Hclose" with "[Hown] Htl") as "[$ $]"; last done. by iApply "HP".
-  Qed.
-
-  Global Instance cell_send :
-    Send ty → Send (cell ty).
-  Proof. intros. split. simpl. apply send_change_tid. Qed.
-End cell.
-
-Section typing.
-  Context `{typeG Σ}.
-
-  (* Constructing a cell. *)
-  Definition cell_new : val := funrec: <> ["x"] := "return" ["x"].
-
-  Lemma cell_new_type ty :
-    typed_instruction_ty [] [] [] cell_new
-        (fn (λ _, [])%EL (λ _, [# box ty]) (λ _:(), box (cell ty))).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]); first solve_typing.
-    iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
-  Qed.
-
-  (* Same for the other direction.
-     FIXME : this does not exist in Rust.*)
-  Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
-
-  Lemma cell_into_inner_type ty :
-    typed_instruction_ty [] [] [] cell_into_inner
-        (fn (λ _, [])%EL (λ _, [# box (cell ty)]) (λ _:(), box ty)).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]); first solve_typing.
-    iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
-  Qed.
-
-  (* Reading from a cell *)
-  Definition cell_get ty : val :=
-    funrec: <> ["x"] :=
-      let: "x'" := !"x" in
-      letalloc: "r" <-{ty.(ty_size)} !"x'" in
-      delete [ #1; "x"];; "return" ["r"].
-
-  Lemma cell_get_type `(!Copy ty) :
-    typed_instruction_ty [] [] [] (cell_get ty)
-        (fn (λ α, [☀α])%EL (λ α, [# box (&shr{α} (cell ty))])%T (λ _, box ty)).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply type_letalloc_n; [solve_typing..| |solve_typing|intros r; simpl_subst].
-    { apply (read_shr _ _ _ (cell ty)); solve_typing. }
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-
-  (* Writing to a cell *)
-  Definition cell_set ty : val :=
-    funrec: <> ["c"; "x"] :=
-       let: "c'" := !"c" in
-       "c'" <-{ty.(ty_size)} !"x";;
-       let: "r" := new [ #0 ] in
-       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
-
-  Lemma cell_set_type ty :
-    typed_instruction_ty [] [] [] (cell_set ty)
-        (fn (λ α, [☀α])%EL (λ α, [# box (&shr{α} cell ty); box ty])
-            (λ α, box unit)).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-    intros c'. simpl_subst.
-    eapply type_let with (T1 := [c' ◁ _; x ◁ _]%TC)
-                         (T2 := λ _, [c' ◁ &shr{α} cell ty;
-                                      x ◁ box (uninit ty.(ty_size))]%TC); try solve_typing; [|].
-    { (* The core of the proof: Showing that the assignment is safe. *)
-      iAlways. iIntros (tid qE) "#HEAP #LFT Htl HE $".
-      rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-      iIntros "[Hc' Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
-      iDestruct "Hc'" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
-      iDestruct "Hshr" as (P) "[#HP #Hshr]".
-      iDestruct "Hx" as (l') "[EQ [Hown >H†]]". iDestruct "EQ" as %[=->].
-      iDestruct "Hown" as (vl') "[>H↦' Hown']".
-      iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
-      iDestruct ("HP" with "Hown") as (vl) "[>H↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as "#>%".
-      iDestruct (ty_size_eq with "Hown'") as "#>%".
-      iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done..|].
-      iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
-      iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
-      { iApply "HP". iExists vl'. by iFrame. }
-      rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-      iSplitR; iModIntro.
-      - iExists _. simpl. eauto.
-      - iExists _. iSplit; first done. iFrame. iExists _. iFrame.
-        rewrite uninit_own. auto. }
-    intros v. simpl_subst. clear v.
-    eapply type_new; [solve_typing..|].
-    intros r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-
-  (* Reading from a cell *)
-  Definition cell_get_mut : val :=
-    funrec: <> ["x"] := "return" ["x"].
-
-  Lemma cell_get_mut_type `(!Copy ty) :
-    typed_instruction_ty [] [] [] cell_get_mut
-      (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α} (cell ty))])%T
-          (λ α, box (&uniq{α} ty))%T).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
-    iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
-    by iIntros "$".
-  Qed.
-End typing.
-
-Hint Resolve cell_mono' cell_proper' : lrust_typing.