make join_handle Send/Sync

theories/lang/lib/spawn.v

@@ -47,7 +47,8 @@ Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ γf γj v, own γf (Excl ()) ∗ shift_loc c 1 ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
 
 Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (∃ γf γj, own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ))%I.
+  (∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
+   □ (∀ v, Ψ' v -∗ Ψ v))%I.
 
 Global Instance spawn_inv_ne n γf γj c :
   Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γf γj c).
@@ -96,7 +97,7 @@ Qed.
 Lemma join_spec (Ψ : val → iProp Σ) c :
   {{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
 Proof.
-  iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj) "(Hj & H† & #?)".
+  iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
   iLöb as "IH". wp_rec.
   wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
   { iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
@@ -112,8 +113,17 @@ Proof.
   iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
   iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
   { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
-  wp_free; first done. iApply "HΦ". done.
+  wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
 Qed.
+
+Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
+  □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
+Proof.
+  iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+  iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
+  iApply "HΨ". iApply "HΨ'". done.
+Qed.
+
 End proof.
 
 Typeclasses Opaque finish_handle join_handle.

theories/typing/lib/spawn.v

@@ -17,8 +17,7 @@ Section join_handle.
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] =>
-           ∃ ty', ▷ type_incl ty' ty ∗ join_handle spawnN l (join_inv tid ty')
+         | [ #(LitLoc l) ] =>join_handle spawnN l (join_inv tid ty)
          | _ => False
          end%I;
        ty_shr κ tid l := True%I |}.
@@ -34,8 +33,9 @@ Section join_handle.
   Proof.
     iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
-      iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
-      iApply (type_incl_trans with "Hincl'"). done.
+      simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown".
+      iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
+      iApply "Hincl". done.
     - iIntros "* _". auto.
   Qed.
 
@@ -57,8 +57,22 @@ Section join_handle.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
 
-  (* TODO: Looks like in Rust, we have T: Send -> JoinHandle<T>: Send and
-     T:Sync -> JoinHandle<T>: Sync. *)
+  Global Instance join_handle_send ty :
+    Send ty → Send (join_handle ty).
+  Proof.
+    iIntros (??? vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hv".
+    unfold join_inv. iApply own_send. (* FIXME: Why does "iApply send_change_tid" not work? *)
+    done.
+  Qed.
+
+  Global Instance join_handle_sync ty :
+    Sync (join_handle ty).
+  Proof.
+    iIntros (????) "**". (* FIXME: Why did it throw away the assumption we should have gotten? *)
+    done.
+  Qed.
+
 End join_handle.
 
 Section spawn.
@@ -88,7 +102,7 @@ Section spawn.
       iApply (spawn_spec _ (join_inv tid retty) 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 "?". by iFrame. }
       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]
@@ -129,12 +143,10 @@ Section spawn.
     iApply (type_let _ _ _ _ ([c' ◁ _])
                              (λ r, [r ◁ box retty])); try solve_typing; [|].
     { iIntros (tid) "#LFT _ $ $".
-      rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
-      destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
-      iApply (join_spec with "Hc'"). iNext. iIntros "* Hret".
-      rewrite tctx_interp_singleton tctx_hasty_val.
-      iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
-      iApply "Hincl". done. }
+      rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
+      destruct c' as [[|c'|]|]; try done.
+      iApply (join_spec with "Hc"). iNext. iIntros "* Hret".
+      rewrite tctx_interp_singleton tctx_hasty_val. done. }
     iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.