theories/typing/tests/lazy_lft.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section lazy_lft.
-  Context `{typeG Σ}.
-
-  Definition lazy_lft : val :=
-    funrec: <> [] :=
-      Newlft;;
-      let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
-      let: "42" := #42 in "f" <- "42";;
-      "t" +ₗ #0 <- "f";; "t" +ₗ #1 <- "f";;
-      let: "t0'" := !("t" +ₗ #0) in "t0'";;
-      let: "23" := #23 in "g" <- "23";;
-      "t" +ₗ #1 <- "g";;
-      let: "r" := new [ #0] in
-      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
-
-  Lemma lazy_lft_type :
-    typed_instruction_ty [] [] [] lazy_lft
-        (fn (λ _, [])%EL (λ _, [#]) (λ _:(), box unit)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
-    eapply (type_newlft []); [solve_typing|]=>α.
-    eapply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
-      intros t. simpl_subst.
-    eapply type_new; [solve_typing..|]=>f. simpl_subst.
-    eapply type_new; [solve_typing..|]=>g. simpl_subst.
-    eapply type_int; [solve_typing|]=>v42. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_own_copy|done|]=>t0'. simpl_subst.
-    eapply type_letpath; [solve_typing..|]=>dummy. simpl_subst.
-    eapply type_int; [solve_typing|]=>v23. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
-    eapply type_new; [solve_typing..|] =>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End lazy_lft.

theories/typing/tests/option_as_mut.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section option_as_mut.
-  Context `{typeG Σ}.
-
-  Definition option_as_mut : val :=
-    funrec: <> ["o"] :=
-      let: "o'" := !"o" in case: !"o'" of
-        [ let: "r" := new [ #2 ] in "r" <-{0} ☇;; "k" ["r"];
-          let: "r" := new [ #2 ] in "r" <-{1} "o'" +ₗ #1;; "k" ["r"] ]
-      cont: "k" ["r"] :=
-        delete [ #1; "o"];; "return" ["r"].
-
-  Lemma option_as_mut_type τ :
-    typed_instruction_ty [] [] [] option_as_mut
-        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}Σ[unit; τ])]) (λ α, box (Σ[unit; &uniq{α}τ]))).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
-    - intros k. simpl_subst.
-      eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
-      eapply type_case_uniq; [solve_typing..|]. constructor; last constructor; last constructor.
-      + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
-        eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
-        eapply (type_jump [_]); solve_typing.
-      + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
-        eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
-        eapply (type_jump [_]); solve_typing.
-    - move=>/= k r. inv_vec r=>r. simpl_subst.
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-  Qed.
-End option_as_mut.

theories/typing/tests/rebor.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section rebor.
-  Context `{typeG Σ}.
-
-  Definition rebor : val :=
-    funrec: <> ["t1"; "t2"] :=
-       Newlft;;
-       letalloc: "x" <- "t1" in
-       let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
-       "x" <- "t2";;
-       let: "y'" := !"y" in
-       letalloc: "r" <- "y'" in
-       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
-                 delete [ #1; "x"] ;; "return" ["r"].
-
-  Lemma rebor_type :
-    typed_instruction_ty [] [] [] rebor
-        (fn (λ _, []) (λ _, [# box (Π[int; int]); box (Π[int; int])])
-            (λ (_ : ()), box int)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
-    eapply (type_newlft []). apply _. move=> α.
-    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply (type_letpath (&uniq{α}int)); [solve_typing..|]=>y. simpl_subst.
-    eapply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|by apply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_uniq; solve_typing|done|]=>y'. simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End rebor.

theories/typing/tests/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/tests/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/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 := (&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.
-  Qed.
-  Next Obligation.
-    iIntros (ty ?? tid l) "#LFT". iApply na_bor_shorten.
-  Qed.
-
-  (* TODO: non-expansiveness, proper wrt. eqtype *)
-
-  Global Instance cell_type :
-    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".
-    iMod ("Hclose" with "Hown Htl") as "[$ $]". done.
-  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 Σ}.
-
-  (* All of these are of course actual code in Rust, but somehow this is more fun. *)
-
-  (* Constructing a cell is a coercion. *)
-  Lemma tctx_mk_cell E L ty p :
-    tctx_incl E L [p ◁ ty] [p ◁ cell ty].
-  Proof.
-    iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
-  Qed.
-
-  (* Same for the other direction *)
-  Lemma tctx_unmk_cell E L ty p :
-    tctx_incl E L [p ◁ ty] [p ◁ cell ty].
-  Proof.
-    iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
-  Qed.
-
-  Lemma read_cell E L κ ty :
-    Copy ty → lctx_lft_alive E L κ →
-    typed_read E L (&shr{κ} cell ty) ty (&shr{κ} cell ty).
-  Proof. intros ??. exact: read_shr. Qed.
-
-  (* Writing actually needs code; typed_write can't have thread tokens. *)
-  Definition cell_write 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_write_type ty :
-    typed_instruction_ty [] [] [] (cell_write 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 "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 "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' //.
-      iSplitR; iModIntro.
-      - iExists _. iSplit; done.
-      - 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.
-
-  (* TODO: get_mut *)
-End typing.