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 own 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 ◁ box (ty x)])]
-                       (zip_with (TCtx_hasty ∘ of_val) xl
-                                 ((λ ty, box ty) <$> (vec_to_list (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 /=. repeat f_equiv. apply Hty.
-      by rewrite (ty_size_proper_d _ _ _ (Hty _)).
-    - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
-      cut (∀ n tid p i, Proper (dist (S n) ==> dist n)
-        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
-      { intros Hprop. apply Hprop, list_fmap_ne, Htys. intros ty1 ty2 Hty12.
-        rewrite (ty_size_proper_d _ _ _ Hty12). by rewrite Hty12. }
-      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".
-      assert (Hst : subtype (E0 ++ E x) L0 (box (ty x)) (box (ty' x)))
-        by by rewrite ->Hty.
-      iDestruct (Hst 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.
-      assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
-        by by rewrite ->Htys.
-      iDestruct (Hst 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 ◁ box (ty x)) :: T)]
-               ((p ◁ fn E' tys ty) ::
-                zip_with TCtx_hasty ps ((λ ty, box ty) <$> (vec_to_list (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 ◁ box 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
-                                   ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
-    (k ◁cont(L, T''))%CC ∈ C →
-    (∀ ret : val, tctx_incl E L ((ret ◁ box (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
-                                   ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ box (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 ◁ box (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 ◁ box (ty x)])]
-                   ((f ◁ fn E' tys ty) ::
-                      zip_with (TCtx_hasty ∘ of_val) args
-                               ((λ ty, box ty) <$> vec_to_list (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 ◁ box (ty x)])]
-                   (zip_with (TCtx_hasty ∘ of_val) args
-                             ((λ ty, box ty) <$> vec_to_list (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 (qL).[κ] 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.
-  Definition ctx_eq {A} (x1 x2 : A) : Prop :=
-    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
-
-  Lemma subtype_refl ty : subtype ty ty.
-  Proof. iIntros. iApply type_incl_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.
-
-  Lemma ctx_eq_refl {A} (x : A) : ctx_eq x x.
-  Proof. by iIntros "_ _ _". Qed.
-  Global Instance ctx_eq_equivalent {A} : Equivalence (@ctx_eq A).
-  Proof.
-    split.
-    - by iIntros (?) "_ _ _".
-    - iIntros (x y Hxy) "LFT HE HL". by iDestruct (Hxy with "LFT HE HL") as %->.
-    - iIntros (x y z Hxy Hyz) "LFT HE HL".
-      iDestruct (Hxy with "LFT HE HL") as %->. by iApply (Hyz with "LFT HE HL").
-  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 ty_size_proper : Proper (subtype ==> ctx_eq) ty_size.
-  Proof. iIntros (?? Hst) "LFT HE HL". iDestruct (Hst with "LFT HE HL") as "[$ ?]". Qed.
-  Global Instance ty_size_proper_flip : Proper (flip subtype ==> ctx_eq) ty_size.
-  Proof. by intros ?? ->. Qed.
-  Lemma ty_size_proper' ty1 ty2 :
-    subtype ty1 ty2 → ctx_eq (ty_size ty1) (ty_size ty2).
-  Proof. apply ty_size_proper. Qed.
-  Lemma ty_size_proper_flip' ty1 ty2 :
-    subtype ty2 ty1 → ctx_eq (ty_size ty1) (ty_size ty2).
-  Proof. apply ty_size_proper_flip. 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.
-
-  Global Instance ty_size_proper_eq : Proper (eqtype ==> ctx_eq) ty_size.
-  Proof. by intros ?? [-> _]. 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 ctx_eq_refl ty_size_proper'
-             ty_size_proper_flip': lrust_typing.
-Hint Opaque ctx_eq subtype eqtype : lrust_typing.
\ No newline at end of file

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 := (&na{κ, tid, shrN.@l}l ↦∗: ty.(ty_own) tid)%I |}.
-  Next Obligation. apply ty_size_eq. Qed.
-  Next Obligation.
-    iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
-  Qed.
-  Next Obligation.
-    iIntros (ty ?? tid l) "#LFT #H⊑ H". 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").
-    - iApply na_bor_iff_proper; last done. iSplit; iIntros "!>!# H";
-      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 *.
-    (* 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 "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 "[$ $]".
-      { 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 "($ & Htl & Hclose)"; [solve_ndisj..|].
-    iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
-    iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
-    by iMod ("Hclose" with "Hown Htl") as "[$ $]".
-  Qed.
-
-  Global Instance cell_send :
-    Send ty → Send (cell ty).
-  Proof. by unfold cell, Send. 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 (λ _, [# ty]) (λ _:(), 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.
-
-  (* The other direction: getting ownership out of a cell. *)
-  Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
-
-  Lemma cell_into_inner_type ty :
-    typed_instruction_ty [] [] [] cell_into_inner
-        (fn (λ _, [])%EL (λ _, [# cell ty]) (λ _:(), 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.
-
-  Definition cell_get_mut : val :=
-    funrec: <> ["x"] := "return" ["x"].
-
-  Lemma cell_get_mut_type `(!Copy ty) :
-    typed_instruction_ty [] [] [] cell_get_mut
-      (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &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.
-
-  (* 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 (λ α, [# &shr{α} (cell ty)])%T (λ _, 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 (λ α, [# &shr{α} cell ty; ty]%T) (λ α, 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 d. simpl_subst.
-    eapply type_let with (T1 := [d ◁ _; x ◁ _]%TC)
-                         (T2 := λ _, [d ◁ &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 "[#Hshr Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
-      destruct d as [[]|]; try iDestruct "Hshr" as "[]".
-      destruct x as [[]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hown >H†]".
-      iDestruct "Hown" as (vl') "[>H↦' Hown']".
-      iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
-      iDestruct ("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 "[$ $]".
-      { iExists vl'. by iFrame. }
-      rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-      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.
-End typing.
-
-Hint Resolve cell_mono' cell_proper' : lrust_typing.

theories/typing/unsafe/refcell.v

-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
-From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Definition refcell_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR (leibnizC lft)) fracR) posR)).
-Class refcellG Σ :=
-  RefCellG :> inG Σ (authR refcell_stR).
-
-Definition Z_of_refcell_st (st : refcell_stR) : Z :=
-  match st with
-  | None => 0
-  | Some (Cinr (_, _, n)) => Zpos n
-  | Some _ => -1
-  end.
-
-Definition reading_st (q : frac) (κ : lft) : refcell_stR :=
-  Some (Cinr (to_agree (κ : leibnizC lft), q, xH)).
-Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
-
-Definition refcellN := nroot .@ "refcell".
-Definition refcell_invN := refcellN .@ "inv".
-
-Section refcell_inv.
-  Context `{typeG Σ, refcellG Σ}.
-
-  Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
-    (∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (● st) ∗
-      match st return _ with
-      | None => &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
-      | Some (Cinr (agν, q, n)) =>
-        ∃ q' ν, agν ≡ to_agree ν ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
-                ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
-                (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
-      | Some _ => True
-      end)%I.
-
-  Global Instance refcell_inv_ne n tid l γ α :
-    Proper (dist n ==> dist n) (refcell_inv tid l γ α).
-  Proof.
-    intros ty1 ty2 Hty. unfold refcell_inv.
-    repeat (f_contractive || f_equiv || apply Hty || apply dist_S).
-  Qed.
-
-  Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
-    eqtype E L ty1 ty2 →
-    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-    refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2.
-  Proof.
-    (* TODO : this proof is essentially [solve_proper], but within the logic.
-              It would easily gain from some automation. *)
-    iIntros (Hty%eqtype_unfold) "#LFT #HE #HL H". unfold refcell_inv.
-    iDestruct (Hty with "LFT HE HL") as "(% & Hown & Hshr)".
-    iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
-                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
-    { iIntros "!# H". iApply bor_iff_proper; last done.
-      iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
-      iFrame; by iApply "Hown". }
-    iDestruct "H" as (st) "H"; iExists st;
-      iDestruct "H" as "($&$&H)"; destruct st as [[|[[]]|]|]; try done;
-      last by iApply "Hb".
-    iDestruct "H" as (q' ν) "(Hag & Heq & Htok & Hs & Hh)". iExists q', ν.
-    iDestruct ("Hshr" with "Hs") as "$". iFrame. iIntros "H†".
-    iMod ("Hh" with "H†") as "Hh". iModIntro. iNext. iMod "Hh". by iApply "Hb".
-  Qed.
-End refcell_inv.
-
-Section refcell.
-  Context `{typeG Σ, refcellG Σ}.
-
-  Program Definition refcell (ty : type) :=
-    {| ty_size := S ty.(ty_size);
-       ty_own tid vl :=
-         match vl return _ with
-         | #(LitInt z) :: vl' => ⌜-1 ≤ z⌝ ∗ ty.(ty_own) tid vl'
-         | _ => False
-         end%I;
-       ty_shr κ tid l :=
-         (∃ α γ, κ ⊑ α ∗ &na{α, tid, refcell_invN}(refcell_inv tid l γ α ty))%I |}.
-  Next Obligation.
-    iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
-    iIntros "[_ %]!%/=". congruence.
-  Qed.
-  Next Obligation.
-    iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
-    iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
-    iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
-    iDestruct "H" as "[>% Hown]".
-    iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
-            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[-] []")%I as "[H [Htok Htok']]".
-    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
-      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
-    { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
-      iDestruct "Hvl" as (vl') "[H↦ Hvl]".
-      iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
-    iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
-    iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
-    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with ">[-Hclose]"
-      as "[$ HQ]"; last first.
-    { iMod ("Hclose" with "HQ []") as "[Hb $]".
-      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
-        iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
-      - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
-        iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
-    clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
-    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
-    - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
-      iMod (own_alloc
-         (● Some (Cinr (to_agree (ν : leibnizC _), (1/2)%Qp, n)))) as (γ) "Hst".
-      { by apply auth_auth_valid. }
-      iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
-      { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
-      iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
-      iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
-      iDestruct ("Hclose" with "Htok") as "[$ Htok]".
-      iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Htok2 $Hshr}!>!>".
-      rewrite Qp_div_2. iSplit; first done. iSplit; first done. iIntros "Hν".
-      iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
-      iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
-    - iMod (own_alloc (● Some (Cinl (Excl ())))) as (γ) "Hst".
-      { by apply auth_auth_valid. }
-      iFrame. iExists _, _. by iFrame.
-  Qed.
-  Next Obligation.
-    iIntros (?????) "LFT #Hκ H". iDestruct "H" as (α γ) "[#??]".
-    iExists _, _. iFrame. iApply lft_incl_trans; auto.
-  Qed.
-
-  Global Instance refcell_ne n : Proper (dist n ==> dist n) refcell.
-  Proof.
-    move=>ty1 ty2 Hty. split; [split|]; simpl.
-    - f_equiv. apply Hty.
-    - f_contractive=>tid vl. repeat f_equiv. apply Hty.
-    - intros κ tid l. by repeat f_equiv.
-  Qed.
-
-  Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
-  Proof.
-    (* TODO : this proof is essentially [solve_proper], but within the logic.
-              It would easily gain from some automation. *)
-    iIntros (ty1 ty2 EQ) "#LFT #HE #HL". pose proof EQ as EQ'%eqtype_unfold.
-    iDestruct (EQ' with "LFT HE HL") as "(% & #Hown & #Hshr)".
-    iSplit; [|iSplit; iIntros "!# * H"].
-    - iPureIntro. simpl. congruence.
-    - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
-    - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff_proper; last done.
-      iSplit; iIntros "!>!# H"; by iApply refcell_inv_proper.
-  Qed.
-  Lemma refcell_mono' E L ty1 ty2 :
-    eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).
-  Proof. eapply refcell_mono. Qed.
-  Global Instance refcell_proper E L : Proper (eqtype E L ==> eqtype E L) refcell.
-  Proof. by split; apply refcell_mono. Qed.
-  Lemma refcell_proper' E L ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (refcell ty1) (refcell ty2).
-  Proof. eapply refcell_proper. Qed.
-
-  Global Instance refcell_send :
-    Send ty → Send (refcell ty).
-  Proof. move=>????[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
-End refcell.
-
-Hint Resolve refcell_mono' refcell_proper' : lrust_typing.

theories/typing/unsafe/refcell_code.v

-From Coq.QArith Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
-From lrust.lang Require Import memcpy.
-From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
-From lrust.typing.unsafe Require Import refcell ref refmut.
-Set Default Proof Using "Type".
-
-Section refcell_functions.
-  Context `{typeG Σ, refcellG Σ}.
-
-  (* Constructing a refcell. *)
-  Definition refcell_new ty : val :=
-    funrec: <> ["x"] :=
-      let: "r" := new [ #(S ty.(ty_size))] in
-      "r" +ₗ #0 <- #0;;
-      "r" +ₗ #1 <-{ty.(ty_size)} !"x";;
-       delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
-
-  Lemma refcell_new_type ty :
-    typed_instruction_ty [] [] [] (refcell_new ty)
-        (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_new; [solve_typing..|].
-    iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]".
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct "Hx" as (vl) "[Hx↦ Hx]".
-    destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
-    iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
-    rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
-    rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦1 $Hx↦]"); [done..|].
-    iIntros "!> [Hr↦1 Hx↦]". wp_seq.
-    iApply (type_delete _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
-        with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
-      iSplitL "Hx↦".
-      - iExists _. rewrite uninit_own. auto.
-      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
-    eapply (type_jump [ #_]); solve_typing.
-  Qed.
-
-  (* The other direction: getting ownership out of a refcell. *)
-  Definition refcell_into_inner ty : val :=
-    funrec: <> ["x"] :=
-      let: "r" := new [ #ty.(ty_size)] in
-      "r" <-{ty.(ty_size)} !"x" +ₗ #1;;
-       delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
-
-  Lemma refcell_into_inner_type ty :
-    typed_instruction_ty [] [] [] (refcell_into_inner ty)
-        (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_new; [solve_typing..|].
-    iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]".
-    iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
-    destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
-    iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
-    iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦ $Hx↦1]"); [done..|].
-    iIntros "!> [Hr↦ Hx↦1]". wp_seq.
-    iApply (type_delete _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
-        with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
-      - iExists vl. iFrame. }
-    eapply (type_jump [ #_]); solve_typing.
-  Qed.
-
-  Definition refcell_get_mut : val :=
-    funrec: <> ["x"] :=
-      let: "x'" := !"x" in
-      "x" <- "x'" +ₗ #1;;
-      "return" ["x"].
-
-  Lemma refcell_get_mut_type ty :
-    typed_instruction_ty [] [] [] refcell_get_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by eapply read_own_move|done|]=>x'. simpl_subst.
-    iIntros "!# * #HEAP #LFT Hna HE HL HC HT".
-    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
-    iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
-        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with ">[Hx']" as "[_ Hx']".
-    { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
-      - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
-        iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
-      - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try iDestruct "H" as "[]".
-        rewrite heap_mapsto_vec_cons.
-        iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
-        iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
-    iApply (type_assign _ _ _ _
-            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
-            with "HEAP LFT Hna HE HL HC [-]");
-      [solve_typing..|by apply write_own| |]; last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iNext. iExists _. rewrite uninit_own. iFrame. }
-    eapply (type_jump [ #_]); solve_typing.
-  Qed.
-
-  (* Shared borrowing. *)
-  Definition refcell_try_borrow : val :=
-    funrec: <> ["x"] :=
-      let: "r" := new [ #3 ] in
-      let: "x'" := !"x" in
-      let: "n" := !"x'" in
-      if: "n" ≤ #-1 then
-        "r" <-{Σ 1} ();;
-        "k" ["r"]
-      else
-        "x'" <- "n" + #1;;
-        let: "ref" := new [ #2 ] in
-        "ref" <- "x'" +ₗ #1;;
-        "ref" +ₗ #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
-        delete [ #2; "ref"];;
-        "k" ["r"]
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
-
-  Lemma refcell_try_borrow_type ty :
-    typed_instruction_ty [] [] [] refcell_try_borrow
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[ref α ty; unit]])%TC);
-      [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
-    { eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing. }
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
-    iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
-    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "(Hx & Hx' & Hr)".
-    destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
-    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
-    iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose')"; try done.
-    iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
-    - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
-        first by iExists st; iFrame.
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [ref α ty; unit] _ _ _ _
-              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "HEAP LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|done| |]; first last.
-      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      simpl. eapply (type_jump [_]); solve_typing.
-    - wp_op. wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
-      iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
-      destruct vl as [|?[|?[]]]; try done. wp_let.
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-      iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
-      iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
-                       ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
-                       own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
-        with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
-      { destruct st as [[|[[agν q] n]|]|]; try done.
-        - iDestruct "Hst" as (q' ν) "(Hag & #Hqq' & [Hν1 Hν2] & #Hshr & H†)".
-          iExists _, _. iFrame "Hν1". iDestruct "Hag" as %Hag. iDestruct "Hqq'" as %Hqq'.
-          iMod (own_update with "Hownst") as "[Hownst ?]".
-          { apply auth_update_alloc,
-               (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[[Hagv _]_].
-            split; [split|].
-            - by rewrite -Hag /= agree_idemp.
-            - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-              apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
-              apply Qcplus_le_mono_r, Qp_ge_0.
-            - done. }
-          iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _. iFrame.
-          rewrite /= Hag agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2
-                  (comm Qp_plus). auto.
-        - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
-          iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
-            auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
-          rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
-          iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
-          iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". done.
-          { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
-          iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
-          iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
-          iExists _, _. iFrame. rewrite Qp_div_2. iSplitR; first done. iSplitR; first done.
-          iIntros "{$Hshr} !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
-          iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
-      iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [ref α ty; unit] _ _ _ _ _ _ _ _
-        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
-              with "HEAP LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
-        first last.
-      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
-        rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
-        iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-        iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
-        iApply lft_glb_mono. done. iApply lft_incl_refl. }
-      simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
-  Qed.
-
-  (* Unique borrowing. *)
-  Definition refcell_try_borrow_mut : val :=
-    funrec: <> ["x"] :=
-      let: "r" := new [ #3 ] in
-      let: "x'" := !"x" in
-      let: "n" := !"x'" in
-      if: "n" = #0 then
-        "x'" <- #(-1);;
-        let: "ref" := new [ #2 ] in
-        "ref" <- "x'" +ₗ #1;;
-        "ref" +ₗ #1 <- "x'";;
-        "r" <-{2,Σ 0} !"ref";;
-        delete [ #2; "ref"];;
-        "k" ["r"]
-      else
-        "r" <-{Σ 1} ();;
-        "k" ["r"]
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
-
-  Lemma refcell_try_borrow_mut_type ty :
-    typed_instruction_ty [] [] [] refcell_try_borrow_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
-  Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box Σ[refmut α ty; unit]])%TC);
-      [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
-    { eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing. }
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
-    iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
-    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "(Hx & Hx' & Hr)".
-    destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
-    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
-    iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose')"; try done.
-    iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
-    - wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
-      iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
-      destruct vl as [|?[|?[]]]; try done. wp_let.
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-      iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
-      destruct st as [[|[[]]|]|]; try done.
-      iMod (own_update with "Hownst") as "[Hownst ?]".
-      { apply auth_update_alloc, (op_local_update_discrete _ _ writing_st)=>//. }
-      iMod ("Hclose'" with "[Hlx Hownst] Hna") as "[Hβtok Hna]";
-        first by iExists _; iFrame.
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [refmut α ty; unit] _ _ _ _ _ _ _ _
-        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
-              with "HEAP LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
-        first last.
-      { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
-        rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
-        iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-        iFrame. iExists _, _, _. iFrame "∗#". }
-      simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
-    - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok Hna]";
-        first by iExists st; iFrame.
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [refmut α ty; unit] _ _ _ _
-              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "HEAP LFT Hna HE HL Hk");
-        [solve_typing..|by eapply write_own|done| |]; first last.
-      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      simpl. eapply (type_jump [_]); solve_typing.
-  Qed.
-End refcell_functions.