Attempt at modeling closures. this does not work because of higher

order liftetime polymorphism in the ref::map function.

_CoqProject

@@ -50,6 +50,7 @@ theories/typing/soundness.v
 theories/typing/lib/option.v
 theories/typing/lib/fake_shared_box.v
 theories/typing/lib/cell.v
+theories/typing/lib/closures.v
 theories/typing/lib/spawn.v
 theories/typing/lib/rc.v
 theories/typing/lib/refcell/refcell.v

theories/typing/lib/closures.v

+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section defs.
+  Context `{typeG Σ}.
+
+  Fixpoint list_to_vec_tywflst {args} (WF : TyWfLst args) : TyWfLst (list_to_vec args) :=
+    match WF with
+    | tyl_wf_nil => tyl_wf_nil
+    | tyl_wf_cons ty tyl _ _ => tyl_wf_cons ty (list_to_vec tyl)
+    end.
+  Existing Instance list_to_vec_tywflst.
+
+  Class FnOnce (args : list type) (F : type) `{!TyWfLst args, !TyWf F} : Type :=
+    { Fn_output : type;
+      Fn_output_wf :> TyWf Fn_output;
+      call_once : val;
+      call_once_type :
+        typed_val call_once (fn (λ _ : (), FP_wf ∅ (F ::: list_to_vec args) Fn_output))
+    }.
+
+  Class FnMut (args : list type) (F : type)
+        `{!TyWfLst args, !TyWf F, !FnOnce args F} : Type :=
+    { call_mut : val;
+      call_mut_type :
+        typed_val call_mut (fn (λ α, FP_wf ∅ (&uniq{α} F ::: list_to_vec args) Fn_output))
+    }.
+
+  Class Fn (args : list type) (F : type)
+        `{!TyWfLst args, !TyWf F, !FnOnce args F, !FnMut args F} : Type :=
+    { call : val;
+      call_type :
+        typed_val call (fn (λ α, FP_wf ∅ (&shr{α} F ::: list_to_vec args) Fn_output))
+    }.
+End defs.
+
+Arguments Fn_output {_ _ _} _ {_ _ _}.
+Arguments call_once {_ _ _} _ {_ _ _}.
+Arguments call_mut {_ _ _} _ {_ _ _ _}.
+Arguments call {_ _ _} _ {_ _ _ _ _}.
+
+(* FIXME : these instances should be defined for any number of
+   parameters, but the typeclass search for [Closed] is not able to
+   support variable number of parameters. *)
+Program Instance FnOnce_shr_bor_0 `{typeG Σ} (α : lft) (F : type)
+        `{!TyWf F, !FnOnce [] F, !FnMut [] F, !Fn [] F} :
+  FnOnce [] (&shr{α}F) :=
+  {| Fn_output := Fn_output F;
+     call_once :=
+       funrec: <> ["x"] :=
+         let: "x'" := !"x" in
+         letalloc: "x''" <- "x'" in
+         let: "f" := call F in
+         letcall: "r" := "f" ["x''"]%E in
+         delete [ #1; "x"];; return: ["r"]
+  |}.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ϝ ret p).
+  inv_vec p=>x. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnOnce_shr_bor_1 `{typeG Σ} (α : lft) (tyarg1 : type) (F : type) 
+        `{!TyWfLst [tyarg1], !TyWf F, !FnOnce [tyarg1] F, !FnMut [tyarg1] F, !Fn [tyarg1] F} :
+    FnOnce [tyarg1] (&shr{α}F) :=
+  { Fn_output := Fn_output F;
+    call_once :=
+      funrec: <> ["x"; "a1"] :=
+        let: "x'" := !"x" in
+        letalloc: "x''" <- "x'" in
+        let: "f" := call F in
+        letcall: "r" := "f" ["x''"; "a1"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ϝ ret p).
+  inv_vec p=>x a1. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnMut_shr_bor_0 `{typeG Σ} (α : lft) (F : type)
+        `{!TyWf F, !FnOnce [] F, !FnMut [] F, !Fn [] F} :
+  FnMut [] (&shr{α}F) :=
+  { call_mut :=
+      funrec: <> ["x"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call F in
+        letcall: "r" := "f" ["x'''"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ϝ ret p).
+  inv_vec p=>x. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnMut_shr_bor_1 `{typeG Σ} (α : lft) (tyarg1 : type) (F : type)
+  `{!TyWfLst [tyarg1], !TyWf F, !FnOnce [tyarg1] F, !FnMut [tyarg1] F, !Fn [tyarg1] F} :
+  FnMut [tyarg1] (&shr{α}F) :=
+  { call_mut :=
+      funrec: <> ["x"; "a1"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call F in
+        letcall: "r" := "f" ["x'''"; "a1"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ϝ ret p).
+  inv_vec p=>x a1. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance Fn_shr_bor_0 `{typeG Σ} (α : lft) (F : type)
+        `{!TyWf F, !FnOnce [] F, !FnMut [] F, !Fn [] F} :
+  Fn [] (&shr{α}F) :=
+  { call :=
+      funrec: <> ["x"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call F in
+        letcall: "r" := "f" ["x'''"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ϝ ret p).
+  inv_vec p=>x. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance Fn_shr_bor_1 `{typeG Σ} (α : lft) (tyarg1 : type) (F : type)
+        `{!TyWfLst [tyarg1], !TyWf F, !FnOnce [tyarg1] F, !FnMut [tyarg1] F, !Fn [tyarg1] F} :
+  Fn [tyarg1] (&shr{α}F) :=
+  { call :=
+      funrec: <> ["x";"a1"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call F in
+        letcall: "r" := "f" ["x'''";"a1"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ϝ ret p).
+  inv_vec p=>x a1. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnOnce_uniq_bor_0 `{typeG Σ} (α : lft) (F : type)
+        `{!TyWf F, !FnOnce [] F, !FnMut [] F} :
+    FnOnce [] (&uniq{α}F) :=
+  { Fn_output := Fn_output F;
+    call_once :=
+      funrec: <> ["x"] :=
+        let: "x'" := !"x" in
+        letalloc: "x''" <- "x'" in
+        let: "f" := call_mut F in
+        letcall: "r" := "f" ["x''"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ϝ ret p).
+  inv_vec p=>x. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_let; [by apply call_mut_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnOnce_uniq_bor_1 `{typeG Σ} (α : lft) (tyarg1 : type) (F : type)
+        `{!TyWfLst [tyarg1], !TyWf F, !FnOnce [tyarg1] F, !FnMut [tyarg1] F} :
+  FnOnce [tyarg1] (&uniq{α}F) :=
+  { Fn_output := Fn_output F;
+    call_once :=
+      funrec: <> ["x";"a1"] :=
+        let: "x'" := !"x" in
+        letalloc: "x''" <- "x'" in
+        let: "f" := call_mut F in
+        letcall: "r" := "f" ["x''";"a1"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ϝ ret p).
+  inv_vec p=>x a1. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_let; [by apply call_mut_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnMut_uniq_bor_0 `{typeG Σ} (α : lft) (F : type)
+        `{!TyWf F, !FnOnce [] F, !FnMut [] F} :
+  FnMut [] (&uniq{α}F) :=
+  { call_mut :=
+      funrec: <> ["x"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call_mut F in
+        letcall: "r" := "f" ["x'''"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ret ϝ p).
+  inv_vec p=>x. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref_uniq_uniq; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_mut_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.
+
+Program Instance FnMut_uniq_bor_1 `{typeG Σ} (α : lft) (tyarg1 : type) (F : type)
+        `{!TyWfLst [tyarg1], !TyWf F, !FnOnce [tyarg1] F, !FnMut [tyarg1] F} :
+  FnMut [tyarg1] (&uniq{α}F) :=
+  { call_mut :=
+      funrec: <> ["x";"a1"] :=
+        let: "x'" := !"x" in
+        let: "x''" := !"x'" in
+        letalloc: "x'''" <- "x''" in
+        let: "f" := call_mut F in
+        letcall: "r" := "f" ["x'''";"a1"]%E in
+        delete [ #1; "x"];; return: ["r"]
+  }.
+Next Obligation.
+  intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (β ret ϝ p).
+  inv_vec p=>x a1. simpl_subst.
+  iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+  iApply type_deref_uniq_uniq; [solve_typing..|]. iIntros (x''). simpl_subst.
+  iApply type_letalloc_1; [solve_typing..|]. iIntros (x'''). simpl_subst.
+  iApply type_let; [by apply call_mut_type|solve_typing|]. iIntros (fc). simpl_subst.
+  iApply type_letcall; [solve_typing..|]. iIntros (r). simpl_subst.
+  iApply type_delete; [solve_typing..|].
+  iApply type_jump; solve_typing.
+Qed.

theories/typing/lib/refcell/ref_code.v

@@ -4,6 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
+From lrust.typing.lib Require Import closures.
 From lrust.typing.lib.refcell Require Import refcell ref.
 Set Default Proof Using "Type".
 
@@ -204,27 +205,25 @@ Section ref_functions.
   Qed.
 
   (* Apply a function within the ref, typically for accessing a component. *)
-  Definition ref_map : val :=
-    funrec: <> ["ref"; "f"; "env"] :=
-      let: "f'" := !"f" in
+  Definition ref_map F ty `{!TyWf F, !TyWf ty, !∀ α, FnOnce [&uniq{α}ty]%T F} : val :=
+    funrec: <> ["ref"; "env"] :=
+      let: "f" := call_once F in
       Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
-      letcall: "r" := "f'" ["env"; "x"]%E in
+      letcall: "r" := "f" ["env"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
       Endlft;;
       "ref" <- "r'";;
-      delete [ #1; "f"];; return: ["ref"].
+      return: ["ref"].
 
-  Lemma ref_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
-    typed_val ref_map
-      (fn(∀ β, ∅; ref β ty1, fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2, envty)
-       → ref β ty2).
+  Lemma ref_map_type F ty `{!TyWf F, !TyWf ty, !FnOnce [ty] F} :
+    typed_val (ref_map F ty) (fn(∀ β, ∅; ref β ty, F) → ref β (Fn_output F)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
-       inv_vec arg=>ref f env. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
-    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply call_once_type|solve_typing..|]. iIntros (f). simpl_subst.
+    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & Href & Henv)".
     rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
@@ -244,9 +243,8 @@ Section ref_functions.
     { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
     iApply (type_type ((κ ⊑ α ⊓ ν) :: (α ⊓ ν ⊑ α) :: _)%EL _
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]%CC
-        [ f' ◁ fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2;
-          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box envty ]%TC
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}(Fn_output F))])]%CC
+        [ f ◁ fn(∅; F, ty) → Fn_output F; #lx ◁ box (&shr{α ⊓ ν}ty); env ◁ box F ]%TC
        with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }

theories/typing/lib/spawn.v

@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
+From lrust.typing.lib Require Import closures.
 Set Default Proof Using "Type".
 
 Definition spawnN := lrustN .@ "spawn".
@@ -61,54 +62,40 @@ End join_handle.
 Section spawn.
   Context `{!typeG Σ, !spawnG Σ}.
 
-  Definition spawn : val :=
-    funrec: <> ["f"; "env"] :=
-      let: "f'" := !"f" in
+  Definition spawn F `{!TyWf F, !FnOnce [] F} : val :=
+    funrec: <> ["env"] :=
       let: "join" := spawn [λ: ["c"],
-                            letcall: "r" := "f'" ["env":expr] in
+                            let: "f" := call_once F in
+                            letcall: "r" := "f" ["env":expr] in
                             finish ["c"; "r"]] in
       letalloc: "r" <- "join" in
-      delete [ #1; "f"];; return: ["r"].
+      return: ["r"].
 
-  Lemma spawn_type envty retty `{!TyWf envty, !TyWf retty}
-        `(!Send envty, !Send retty) :
-    let E ϝ := envty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
-    typed_val spawn (fn(E; fn(∅; envty) → retty, envty) → join_handle retty).
+  Lemma spawn_type F `{!TyWf F, !FnOnce [] F} `(!Send F, !Send (Fn_output F)) :
+    let E ϝ := F.(ty_outlives_E) static ++ (Fn_output F).(ty_outlives_E) static in
+    typed_val (spawn F) (fn(E; F) → join_handle (Fn_output F)).
   Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ϝ ret arg). inv_vec arg=>f env. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
-    iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
-                     (λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_let _ _ _ _ ([x ◁ _]%TC)
+                     (λ j, [j ◁ join_handle (Fn_output F)]%TC)); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
-      iIntros (tid) "#LFT #HE $ $".
-      rewrite tctx_interp_cons tctx_interp_singleton.
-      iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv tid retty) with "[-]");
-                              first solve_to_val; last first; last simpl_subst.
+      iIntros (tid) "#LFT #HE $ $". rewrite tctx_interp_singleton. iIntros "Hx".
+      iApply (spawn_spec _ (join_inv tid (Fn_output F)) with "[-]");
+        first solve_to_val; last first; last simpl_subst.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
-        iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
-      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
-      (* FIXME this is horrible. *)
-      refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
-                (λ _:(), FP_wf ∅ [# envty] retty) in _).
-      specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
-      erewrite of_val_unlock in Hcall; last done.
-      iApply (Hcall with "LFT HE Htl [] [Hfin]").
-      - constructor.
-      - solve_typing.
-      - rewrite /llctx_interp big_sepL_nil. done.
-      - rewrite /cctx_interp. iIntros "* Hin".
-        iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
-        rewrite /cctx_elt_interp. iIntros "* ?? Hret". inv_vec args=>arg /=.
-        wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
-        rewrite tctx_interp_singleton tctx_hasty_val. by iApply @send_change_tid.
-      - rewrite tctx_interp_cons tctx_interp_singleton. iSplitL "Hf'".
-        + rewrite !tctx_hasty_val. by iApply @send_change_tid.
-        + rewrite !tctx_hasty_val. by iApply @send_change_tid. }
+        iIntros "?". iExists _. iFrame. iApply type_incl_refl. }
+      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let.
+      iApply (type_type _ [] [] [x ◁ box F]%TC with "[Hfin] LFT HE Htl").
+      - iApply type_let; [apply call_once_type|solve_typing|]. iIntros (f). simpl_subst.
+        iApply (type_letcall ()); [solve_typing..|]. simpl. iIntros (r). simpl_subst.
+        iIntros (tid'') "_ _ _ _ _ [Hr _]". rewrite tctx_hasty_val.
+        iApply (finish_spec with "[$Hfin Hr]"); last by auto. by iApply @send_change_tid.
+      - by rewrite /llctx_interp.
+      - by iApply cctx_interp_nil.
+      - rewrite tctx_interp_singleton !tctx_hasty_val. by iApply @send_change_tid. }
     iIntros (v). simpl_subst.
-    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_assign; [solve_typing..|].
-    iApply type_delete; [solve_typing..|].
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.
   Qed.