product_split, type_sum.

theories/typing/product_split.v

+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+Set Default Proof Using "Type".
+
+Section product_split.
+  Context `{typeG Σ}.
+
+  (** General splitting / merging for pointer types *)
+  Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
+    match tyl with
+    | [] => []
+    | ty :: tyl =>
+      (p +ₗ #off ◁ ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
+    end.
+
+  Lemma hasty_ptr_offsets_offset (l : loc) p (off1 off2 : nat) ptr tyl tid :
+    eval_path p = Some #l →
+    tctx_interp tid $ hasty_ptr_offsets (p +ₗ #off1) ptr tyl off2 ≡
+    tctx_interp tid $ hasty_ptr_offsets p ptr tyl (off1 + off2)%nat.
+  Proof.
+    intros Hp.
+    revert off1 off2; induction tyl; intros off1 off2; simpl; first done.
+    rewrite !tctx_interp_cons. f_equiv; last first.
+    { by rewrite IHtyl assoc_L. }
+    apply tctx_elt_interp_hasty_path. clear Hp. simpl.
+    clear. destruct (eval_path p); last done. destruct v; try done.
+    destruct l; try done. rewrite shift_nat_assoc Nat2Z.inj_add //.
+  Qed.
+
+  Lemma tctx_split_ptr_prod E L ptr tyl :
+    (∀ p ty1 ty2,
+        tctx_incl E L [p ◁ ptr $ product2 ty1 ty2]
+                      [p ◁ ptr ty1; p +ₗ #ty1.(ty_size) ◁ ptr ty2]) →
+    (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [VVal #l]⌝) →
+    ∀ p, tctx_incl E L [p ◁ ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
+  Proof.
+    iIntros (Hsplit Hloc p tid q) "#LFT #HE HL H".
+    iInduction tyl as [|ty tyl IH] "IH" forall (p).
+    { rewrite tctx_interp_nil. auto. }
+    rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HL & H)".
+    cbn -[tctx_elt_interp].
+    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
+    iDestruct (Hloc with "Hty") as %[l [=->]].
+    iAssert (tctx_elt_interp tid (p +ₗ #0 ◁ ptr ty)) with "[Hty]" as "$".
+    { iExists #l. iSplit; last done. simpl; by rewrite Hp shift_0. }
+    iMod ("IH" with "HL [Htyl]") as "($ & Htyl)".
+    { auto. }
+    iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
+  Qed.
+
+  Lemma tctx_merge_ptr_prod E L ptr tyl :
+    (Proper (eqtype E L ==> eqtype E L ) ptr) → tyl ≠ [] →
+    (∀ p ty1 ty2,
+        tctx_incl E L [p ◁ ptr ty1; p +ₗ #ty1.(ty_size) ◁ ptr ty2]
+                      [p ◁ ptr $ product2 ty1 ty2]) →
+    (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [VVal #l]⌝) →
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl].
+  Proof.
+    iIntros (Hptr Htyl Hmerge Hloc p tid q) "#LFT #HE HL H".
+    iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
+    rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
+    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
+    iDestruct "Hp" as %Hp. iDestruct (Hloc with "Hty") as %[l [=->]].
+    assert (eval_path p = Some #l) as Hp'.
+    { move:Hp. simpl. clear. destruct (eval_path p); last done.
+      destruct v; try done. destruct l0; try done. rewrite shift_0. done. }
+    clear Hp. destruct tyl.
+    { assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
+      { rewrite right_id. done. }
+      iDestruct (Hincl with "HL HE") as "#(_ & #Heq & _)".
+      iFrame. iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
+      by iApply "Heq". }
+    iMod ("IH" with "[] HL [Htyl]") as "(HL & Htyl)"; first done.
+    { change (ty_size ty) with (0+ty_size ty)%nat at 1.
+      rewrite plus_comm -hasty_ptr_offsets_offset //. }
+    iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
+                   last by rewrite tctx_interp_singleton.
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
+    iExists #l. iSplit; done.
+  Qed.
+
+  (** Owned pointers *)
+  Lemma tctx_split_own_prod2 E L p n ty1 ty2 :
+    tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
+                  [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
+    iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
+    iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
+    rewrite own_loc_na_vec_app -freeable_sz_split.
+    iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
+    iDestruct (ty_size_eq with "H1") as "#>EQ".
+    iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
+    + iExists _. iFrame "#∗". iExists _. by iFrame.
+    + iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
+      iFrame. iExists _. by iFrame.
+  Qed.
+
+  Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
+    tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
+                  [p ◁ own_ptr n $ product2 ty1 ty2].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
+    iDestruct "H1" as "(H↦1 & H†1)".
+    iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %Hρ1.
+    rewrite Hρ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
+    iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
+    iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
+    iExists (vl1 ++ vl2). rewrite own_loc_na_vec_app. iFrame.
+    iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
+    rewrite {3}/ty_own /=. auto 10 with iFrame.
+  Qed.
+
+  Lemma tctx_split_own_prod E L n tyl p :
+    tctx_incl E L [p ◁ own_ptr n $ product tyl] (hasty_ptr_offsets p (own_ptr n) tyl 0).
+  Proof.
+    apply tctx_split_ptr_prod.
+    - intros. apply tctx_split_own_prod2.
+    - iIntros (??[|[| |[[]|]][]]) "?"; eauto.
+  Qed.
+
+  Lemma tctx_merge_own_prod E L n tyl :
+    tyl ≠ [] →
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p (own_ptr n) tyl 0)
+                   [p ◁ own_ptr n $ product tyl].
+  Proof.
+    intros. apply tctx_merge_ptr_prod; try done.
+    - apply _.
+    - intros. apply tctx_merge_own_prod2.
+    - iIntros (??[|[| |[[]|]][]]) "?"; eauto.
+  Qed.
+
+  (** Unique borrows *)
+  Lemma tctx_split_uniq_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &uniq{κ}(product2 ty1 ty2)]
+                  [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
+    rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
+    rewrite /tctx_elt_interp /=.
+    iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
+  Qed.
+
+  Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
+                  [p ◁ &uniq{κ}(product2 ty1 ty2)].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
+    iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
+    iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
+    iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj. by rewrite /= split_prod_mt.
+  Qed.
+
+  Lemma uniq_is_ptr κ ty tid (vl : list value.val) :
+    ty_own (&uniq{κ}ty) tid vl -∗ ⌜∃ l : loc, vl = [VVal #l]⌝.
+  Proof. iIntros "H". destruct vl as [|[| |[[]|]][]]; eauto. Qed.
+
+  Lemma tctx_split_uniq_prod E L κ tyl p :
+    tctx_incl E L [p ◁ &uniq{κ}(product tyl)]
+                  (hasty_ptr_offsets p (uniq_bor κ) tyl 0).
+  Proof.
+    apply tctx_split_ptr_prod.
+    - intros. apply tctx_split_uniq_prod2.
+    - intros. apply uniq_is_ptr.
+  Qed.
+
+  Lemma tctx_merge_uniq_prod E L κ tyl :
+    tyl ≠ [] →
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p (uniq_bor κ) tyl 0)
+                   [p ◁ &uniq{κ}(product tyl)].
+  Proof.
+    intros. apply tctx_merge_ptr_prod; try done.
+    - apply _.
+    - intros. apply tctx_merge_uniq_prod2.
+    - intros. apply uniq_is_ptr.
+  Qed.
+
+  (** Shared borrows *)
+  Lemma tctx_split_shr_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &shr{κ}(product2 ty1 ty2)]
+                  [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
+    iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
+    by iSplitL "H1"; iExists _; (iSplitR; first by rewrite /= Hp).
+  Qed.
+
+  Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
+                  [p ◁ &shr{κ}(product2 ty1 ty2)].
+  Proof.
+    iIntros (tid q) "#LFT _ $ H".
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
+    iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
+    rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
+  Qed.
+
+  Lemma shr_is_ptr κ ty tid (vl : list value.val) :
+    ty_own (&shr{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [VVal #l]⌝.
+  Proof. iIntros "H". destruct vl as [|[| |[[]|]][]]; eauto. Qed.
+
+  Lemma tctx_split_shr_prod E L κ tyl p :
+    tctx_incl E L [p ◁ &shr{κ}(product tyl)]
+                  (hasty_ptr_offsets p (shr_bor κ) tyl 0).
+  Proof.
+    apply tctx_split_ptr_prod.
+    - intros. apply tctx_split_shr_prod2.
+    - intros. apply shr_is_ptr.
+  Qed.
+
+  Lemma tctx_merge_shr_prod E L κ tyl :
+    tyl ≠ [] →
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p (shr_bor κ) tyl 0)
+                   [p ◁ &shr{κ}(product tyl)].
+  Proof.
+    intros. apply tctx_merge_ptr_prod; try done.
+    - apply _.
+    - intros. apply tctx_merge_shr_prod2.
+    - intros. apply shr_is_ptr.
+  Qed.
+
+  (* Splitting with [tctx_extract]. *)
+
+  (* We do not state the extraction lemmas directly, because we want the
+     automation system to be able to perform e.g., borrowing or splitting after
+     splitting. *)
+  Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own_ptr n) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ own_ptr n $ Π tyl) :: T) (T' ++ T).
+  Proof.
+    intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_own_prod.
+  Qed.
+
+  Lemma tctx_extract_split_uniq_prod E L p p' κ ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (uniq_bor κ) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ}(Π tyl)) :: T) (T' ++ T).
+  Proof.
+    intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_uniq_prod.
+  Qed.
+
+  Lemma tctx_extract_split_shr_prod E L p p' κ ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (shr_bor κ) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &shr{κ}(Π tyl)) :: T) ((p ◁ &shr{κ}(Π tyl)) :: T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
+    rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]) //.
+    apply submseteq_skip, submseteq_nil_l.
+  Qed.
+
+  (* Merging with [tctx_extract]. *)
+
+  Fixpoint extract_tyl E L p (ptr: type → type) tyl (off : nat) T T' : Prop :=
+    match tyl with
+    | [] => T = T'
+    | ty :: tyl => ∃ T'',
+        tctx_extract_hasty E L (p +ₗ #off) (ptr ty) T T'' ∧
+        extract_tyl E L p ptr tyl (off + ty.(ty_size)) T'' T'
+    end.
+
+  Lemma tctx_extract_merge_ptr_prod E L p ptr tyl T T' :
+    tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl] →
+    extract_tyl E L p ptr tyl 0 T T' →
+    tctx_extract_hasty E L p (ptr (Π tyl)) T T'.
+  Proof.
+    rewrite /extract_tyl /tctx_extract_hasty=>Hi Htyl.
+    etrans; last by eapply (tctx_incl_frame_r T' _ [_]). revert T Htyl. clear.
+    generalize 0%nat. induction tyl=>[T n /= -> //|T n /= [T'' [-> Htyl]]]. f_equiv. auto.
+  Qed.
+
+  Lemma tctx_extract_merge_own_prod E L p n tyl T T' :
+    tyl ≠ [] →
+    extract_tyl E L p (own_ptr n) tyl 0 T T' →
+    tctx_extract_hasty E L p (own_ptr n (Π tyl)) T T'.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_own_prod. Qed.
+
+  Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
+    tyl ≠ [] →
+    extract_tyl E L p (uniq_bor κ) tyl 0 T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(Π tyl)) T T'.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_uniq_prod. Qed.
+
+  Lemma tctx_extract_merge_shr_prod E L p κ tyl T T' :
+    tyl ≠ [] →
+    extract_tyl E L p (shr_bor κ) tyl 0 T T' →
+    tctx_extract_hasty E L p (&shr{κ}(Π tyl)) T T'.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
+End product_split.
+
+(* We do not want unification to try to unify the definition of these
+   types with anything in order to try splitting or merging. *)
+Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
+
+(* We make sure that splitting is tried before borrowing, so that not
+   the entire product is borrowed when only a part is needed. *)
+Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
+    | 5 : lrust_typing.
+
+(* Merging is also tried after everything, except
+   [tctx_extract_hasty_further]. Moreover, it is placed in a
+   difference hint db. The reason is that it can make the proof search
+   diverge if the type is an evar.
+
+   Unfortunately, priorities are not taken into account accross hint
+   databases with [typeclasses eauto], so this is useless, and some
+   solve_typing get slow because of that. See:
+     https://coq.inria.fr/bugs/show_bug.cgi?id=5304
+*)
+Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
+    | 40 : lrust_typing_merge.
+Hint Unfold extract_tyl : lrust_typing.

theories/typing/type_sum.v

+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import memcpy.
+From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
+From lrust.typing Require Import lft_contexts type_context programs product.
+Set Default Proof Using "Type".
+
+Section case.
+  Context `{typeG Σ}.
+
+  (* FIXME : have a iris version of Forall2. *)
+  Lemma type_case_own' E L C T p n tyl el :
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit.uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+         (p +ₗ #(S (ty.(ty_size))) ◁
+            own_ptr n (uninit.uninit (max_list_with ty_size tyl - ty_size ty))) :: T) e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
+  Proof.
+    iIntros (Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as %[].
+    iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
+    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+    simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
+    rewrite -Nat.add_1_l app_length -!freeable_sz_split
+            own_loc_na_vec_cons own_loc_na_vec_app.
+    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+    iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
+    rewrite nth_lookup.
+    destruct (tyl !! i) as [ty|] eqn:EQty; last by iDestruct "Hown" as ">%".
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
+    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
+    - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+      iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
+      + rewrite shift_0. iFrame. iExists [VVal #i]. rewrite own_loc_na_vec_singleton.
+        iFrame. auto.
+      + iModIntro. eauto with iFrame.
+      + rewrite -EQlen app_length minus_plus -(shift_nat_assoc _ 1).
+        iFrame. iExists _. iFrame. auto.
+    - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+      iExists (VVal #i :: vl' ++ vl''). iNext.
+      rewrite own_loc_na_vec_cons own_loc_na_vec_app.
+      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=.
+      iModIntro. auto.
+  Qed.
+
+  Lemma type_case_own E L C T T' p n tyl el :
+    tctx_extract_hasty E L p (own_ptr n (sum tyl)) T T' →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit.uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+         (p +ₗ #(S (ty.(ty_size))) ◁
+            own_ptr n (uninit.uninit (max_list_with ty_size tyl - ty_size ty))) :: T') e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
+
+  Lemma type_case_uniq' E L C T p κ tyl el :
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
+      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
+  Proof.
+    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as %[].
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done. simpl.
+    iMod (bor_acc_cons with "[LFT //] Hp Htok") as "[H↦ Hclose']". done.
+    iDestruct "H↦" as (vl) "[H↦ Hown]".
+    iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+    iDestruct "EQlen" as %[=EQlen].
+    rewrite own_loc_na_vec_cons own_loc_na_vec_app nth_lookup.
+    iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+    destruct (tyl !! i) as [ty|] eqn:EQty; last by iDestruct "Hown" as ">%".
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
+    iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
+    destruct Hety as [Hety|Hety].
+    - iMod ("Hclose'" $! ((l >> 1) ↦∗: ty.(ty_own) tid)%I
+            with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
+      { iIntros "!>!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
+        iExists (VVal #i::vl'2++vl''). iIntros "!>". iNext.
+        iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
+        rewrite own_loc_na_vec_cons own_loc_na_vec_app EQlenvl' EQlenvl'2.
+        iFrame. iExists _, _, _. iSplit. by auto.
+        rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
+      { iExists vl'. iFrame. }
+      iMod ("Hclose" with "Htok") as "HL".
+      iApply (Hety with "LFT HE Hna HL HC").
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
+    - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
+        [by iIntros "!>!>$"| |].
+      { iExists (VVal #i::vl'++vl'').
+        rewrite own_loc_na_vec_cons own_loc_na_vec_app /= -EQlen. iFrame. iNext.
+        iExists i, vl', vl''. rewrite nth_lookup EQty. iModIntro. auto. }
+      iMod ("Hclose" with "Htok") as "HL".
+      iApply (Hety with "LFT HE Hna HL HC").
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
+  Qed.
+
+  Lemma type_case_uniq E L C T T' p κ tyl el :
+    tctx_extract_hasty E L p (&uniq{κ}(sum tyl)) T T' →
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
+      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
+
+  Lemma type_case_shr' E L C T p κ tyl el:
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e,
+      typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
+      typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
+  Proof.
+    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as %[].
+    iDestruct "Hp" as (i) "[#Hb Hshr]".
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
+    iMod (frac_bor_acc with "[LFT //] Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
+    rewrite nth_lookup.
+    destruct (tyl !! i) as [ty|] eqn:EQty; try by iDestruct "Hshr" as %[].
+    edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+    wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
+    iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
+    iMod ("Hclose" with "Htok") as "HL".
+    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame.
+    iExists _. rewrite ->nth_lookup, EQty. iModIntro. auto.
+  Qed.
+
+  Lemma type_case_shr E L C T p κ tyl el :
+    p ◁ &shr{κ}(sum tyl) ∈ T →
+    lctx_lft_alive E L κ →
+    Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
+    typed_body E L C T (case: !p of el).
+  Proof.
+    intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
+    apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
+  Qed.
+
+  Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
+  Proof.
+    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
+    iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
+    iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+    destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] [= ->]].
+    rewrite own_loc_na_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
+    iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
+    iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
+    destruct vl as [|? vl].
+    { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. simpl in *. lia.
+      - apply IHtyl. simpl in *. lia. }
+    rewrite own_loc_na_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
+    iExists (_::_::_). rewrite !own_loc_na_vec_cons. iFrame.
+    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. iModIntro. auto.
+  Qed.
+
+  Lemma type_sum_assign {E L} sty tyl i ty1 ty ty1' C T T' p1 p2 e:
+    Closed [] e →
+    0 ≤ i →
+    sty = sum tyl →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
+    tyl !! (Z.to_nat i) = Some ty →
+    typed_write E L ty1 sty ty1' →
+    typed_body E L C ((p1 ◁ ty1') :: T') e -∗
+    typed_body E L C T (p1 <-{Σ i} p2 ;; e).
+  Proof.
+    iIntros (??->) "* **". rewrite -(Z2Nat.id i) //.
+    iApply type_seq; [by eapply type_sum_assign_instr|done|done].
+  Qed.
+
+  Lemma type_sum_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
+    tyl !! i = Some unit →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
+  Proof.
+    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
+    iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] [= ->]].
+    rewrite own_loc_na_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
+    iApply "Hw". iModIntro. iExists (_::_). rewrite own_loc_na_vec_cons. iFrame.
+    iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
+  Qed.
+
+  Lemma type_sum_unit {E L} sty tyl i ty1 ty1' C T T' p e:
+    Closed [] e →
+    0 ≤ i →
+    sty = sum tyl →
+    tctx_extract_hasty E L p ty1 T T' →
+    tyl !! (Z.to_nat i) = Some unit →
+    typed_write E L ty1 sty ty1' →
+    typed_body E L C ((p ◁ ty1') :: T') e -∗
+    typed_body E L C T (p <-{Σ i} () ;; e).
+  Proof.
+    iIntros (??->) "* **". rewrite -(Z2Nat.id i) //.
+    iApply type_seq; [by eapply type_sum_unit_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty1' →
+    typed_read E L ty2 ty ty2' →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
+               (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
+  Proof.
+    iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
+    iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
+    iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] [=->]].
+    rewrite own_loc_na_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+    wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
+    wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
+    iMod (Hr with "[] LFT HE Htl HL2 Hty2") as (l2 vl2 q [= ->]) "(H↦2 & Hty & Hr)"=>//=.
+    assert (ty.(ty_size) ≤ length vl1).
+    { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. lia.
+      - specialize (IHtyl i). intuition lia. }
+    rewrite -(take_drop (ty.(ty_size)) vl1) own_loc_na_vec_app.
+    iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
+    iDestruct (ty_size_eq with "Hty") as "#>%".
+    iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
+    { rewrite take_length. lia. }
+    iNext; iIntros "[H↦vl1 H↦2]".
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
+    iMod ("Hr" with "H↦2") as "($ & $ & $)". iApply "Hw". iNext.
+    rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
+    iSplitL "H↦pad".
+    - rewrite (shift_nat_assoc _ 1) take_length Nat.min_l; last lia.
+      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
+    - iExists _. iFrame.
+  Qed.
+
+  Lemma type_sum_memcpy {E L} sty tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
+    Closed [] e →
+    0 ≤ i →
+    sty = sum tyl →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
+    tyl !! (Z.to_nat i) = Some ty →
+    typed_write E L ty1 sty ty1' →
+    typed_read E L ty2 ty ty2' →
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
+    typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
+  Proof.
+    iIntros (?? -> ??? Hr ?) "?". subst. rewrite -(Z2Nat.id i) //.
+    by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
+  Qed.
+
+  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : TyWfLst tyl} α:
+    elctx_sat E L (tyl_outlives_E tyl α) →
+    elctx_sat E L (ty_outlives_E (sum tyl) α).
+  Proof.
+    intro Hsat. eapply eq_ind; first done. clear Hsat. rewrite /ty_outlives_E /=.
+    induction Wf as [|ty [] ?? IH]=>//=. rewrite IH fmap_app //.
+  Qed.
+End case.
+
+Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.