Simply specs of spawn and join

theories/lang/spawn.v

@@ -59,36 +59,36 @@ Local Definition mp_inv_reclaim'_eq : @mp_inv_reclaim' = _ := seal_eq _.
 Local Definition mp_inv_reclaim γc γi c Ψ :=
   view_inv γi N (mp_inv_reclaim' γc γi c Ψ).
 
-Definition finish_handle γc c Ψ : vProp :=
-  (∃ γi t V v, (c >> 1) ↦ v ∗
+Definition finish_handle c Ψ : vProp :=
+  (∃ γc γi t V, (c >> 1) ↦ #☠ ∗
     c sw⊒{γc} {[t := (#0, V)]} ∗
     mp_inv_reclaim γc γi c Ψ  ∗
     view_tok γi (1/2)%Qp)%I.
 
-Definition join_handle γc c Ψ : vProp :=
-  (∃ γi (Ψ': val → vProp) t V,
+Definition join_handle c Ψ : vProp :=
+  (∃ γc γi (Ψ': val → vProp) t V,
     c sn⊒{γc} {[t := (#0, V)]}
     ∗ mp_inv_reclaim γc γi c Ψ'
     ∗ ⎡ † c … 2 ⎤
     ∗ view_tok γi (1/2)%Qp
     ∗ □ (∀ v, Ψ' v -∗ Ψ v))%I.
 
-Global Instance finish_handle_contractive n γc c :
-  Proper (pointwise_relation val (dist_later n) ==> dist n) (finish_handle γc c).
+Global Instance finish_handle_contractive n c :
+  Proper (pointwise_relation val (dist_later n) ==> dist n) (finish_handle c).
 Proof.
   rewrite /finish_handle /mp_inv_reclaim mp_inv_reclaim'_eq /mp_inv_reclaim'_def.
   solve_contractive.
 Qed.
-Global Instance join_handle_ne n γc c :
-  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle γc c).
+Global Instance join_handle_ne n c :
+  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle c).
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
 Lemma spawn_spec Ψ e (f : val) tid :
   IntoVal e f →
-  {{{ ∀ γc c tid', finish_handle γc c Ψ -∗ WP f [ #c] @ tid'; ⊤ {{ _, True }} }}}
+  {{{ ∀ c tid', finish_handle c Ψ -∗ WP f [ #c] @ tid'; ⊤ {{ _, True }} }}}
     spawn [e] @ tid; ⊤
-  {{{ γc c, RET #c; join_handle γc c Ψ }}}.
+  {{{ c, RET #c; join_handle c Ψ }}}.
 Proof.
   iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
   wp_let. wp_alloc c as "Hm" "Hl" "H†". wp_let.
@@ -101,18 +101,18 @@ Proof.
   iDestruct (AtomicSWriter_AtomicSeen with "SW") as "#R".
   wp_apply (wp_fork with "[SW Htok1 Hf Hd]"); [done|..].
   - iNext. iIntros (tid'). iApply "Hf". iExists _, _, _, _. by iFrame.
-  - iIntros "_". wp_seq. iApply ("HΦ" $! γc). iExists _, _, _, _.
+  - iIntros "_". wp_seq. iApply "HΦ". iExists _, _, _, _, _.
     iFrame "Inv R ∗". auto.
 Qed.
 
-Lemma finish_spec Ψ c v γc tid
+Lemma finish_spec Ψ c v tid
   (DISJ1: (↑histN) ## (↑N : coPset)) :
-  {{{ finish_handle γc c Ψ ∗ Ψ v }}}
+  {{{ finish_handle c Ψ ∗ Ψ v }}}
     finish [ #c; v] @ tid; ⊤
   {{{ RET #☠; True }}}.
 Proof.
   iIntros (Φ) "[Hfin HΨ] HΦ".
-  iDestruct "Hfin" as (γi t v0 V) "(Hd & SW & #Inv & vTok1)".
+  iDestruct "Hfin" as (γc γi t V) "(Hd & SW & #Inv & vTok1)".
   wp_lam. wp_op. wp_write.
   iMod (view_inv_acc_base' with "[$Inv $vTok1]") as "(vTok1 & INV) {Inv}"; [done|].
   iDestruct "INV" as (Vb) "[INV Close]".
@@ -139,12 +139,12 @@ Proof.
   iIntros "!>". by iApply "HΦ".
 Qed.
 
-Lemma join_spec Ψ c γc tid
+Lemma join_spec Ψ c tid
   (DISJ1: (↑histN) ## (↑N : coPset)) :
-  {{{ join_handle γc c Ψ }}} join [ #c] @ tid; ⊤ {{{ v, RET v; Ψ v }}}.
+  {{{ join_handle c Ψ }}} join [ #c] @ tid; ⊤ {{{ v, RET v; Ψ v }}}.
 Proof.
   iIntros (Φ) "H HΦ".
-  iDestruct "H" as (γi Ψ' t V) "(#R & #Inv & H† & vTok2 & #HΨ')".
+  iDestruct "H" as (γc γi Ψ' t V) "(#R & #Inv & H† & vTok2 & #HΨ')".
   iLöb as "IH". wp_rec. wp_bind (!ᵃᶜ _)%E.
 
   (* open shared invariant *)
@@ -217,11 +217,11 @@ Proof.
     wp_free; first done. iApply "HΦ". by iApply "HΨ'".
 Qed.
 
-Lemma join_handle_impl Ψ1 Ψ2 γc c :
-  □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle γc c Ψ1 -∗ join_handle γc c Ψ2.
+Lemma join_handle_impl Ψ1 Ψ2 c :
+  □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
 Proof.
-  iIntros "#HΨ Hdl". iDestruct "Hdl" as (γi Ψ' t V) "(? & ? & ? & ? & #HΨ')".
-  iExists γi, Ψ', t, _. iFrame "#∗". iIntros "!# * ?".
+  iIntros "#HΨ Hdl". iDestruct "Hdl" as (γc γi Ψ' t V) "(? & ? & ? & ? & #HΨ')".
+  iExists γc, γi, Ψ', t, _. iFrame "#∗". iIntros "!# * ?".
   iApply "HΨ". iApply "HΨ'". done.
 Qed.
 End proof.

theories/typing/lib/join.v

@@ -51,7 +51,7 @@ Section join.
     iApply ((spawn_spec joinN (λ v, (box R_A).(ty_own) tid [v] ∗ (qϝ1).[ϝ])%I) with "[HfA HenvA Hϝ1]");
       first simpl_subst.
     { (* The new thread. *)
-      iIntros (γc c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
+      iIntros (c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
       rewrite !tctx_hasty_val.
       iApply (type_call_iris _ [ϝ] () [_] _ (Build_thread_id tid2 tid') with "LFT HE Htl [Hϝ1] HfA [HenvA]").
       - rewrite outlives_product. solve_typing.
@@ -60,7 +60,7 @@ Section join.
       - iIntros (r) "Htl Hϝ1 Hret".
         wp_rec. iApply (finish_spec with "[$Hfin Hret Hϝ1]"); [solve_ndisj..| |auto].
         rewrite right_id. iFrame. by iApply @send_change_tid. }
-    iNext. iIntros (γc c) "Hjoin". wp_let. wp_let.
+    iNext. iIntros (c) "Hjoin". wp_let. wp_let.
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ2) "(Hϝ2 & HL & Hclose2)";
       [solve_typing..|].
     rewrite !tctx_hasty_val.

theories/typing/lib/spawn.v

@@ -16,7 +16,7 @@ Section join_handle.
     {| ty_size := 1;
        ty_own _ vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] => ∃ γc, join_handle spawnN γc l (join_inv ty)
+         | [ #(LitLoc l) ] => join_handle spawnN l (join_inv ty)
          | _ => False
          end%I;
        ty_shr κ _ l := True%I |}.
@@ -31,8 +31,7 @@ Section join_handle.
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
     iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
-      simpl. iDestruct "Hvl" as (γc) "Hvl". iExists γc.
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done. simpl.
       iApply (join_handle_impl with "[] Hvl"). iIntros "!> * Hown" (tid').
       iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
       iApply "Hincl". done.
@@ -94,8 +93,8 @@ Section spawn.
       iApply (spawn_spec _ (join_inv retty) with "[-]");
         last first; last simpl_subst.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
-        iIntros "?". iExists _. by iFrame. }
-      iIntros (γc c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
+        iIntros "?". by iFrame. }
+      iIntros (c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
       iApply (type_call_iris _ [] () [_] _ (Build_thread_id tid2 tid') with "LFT HE Htl [] Hf' [Henv]");
       (* The `solve_typing` here shows that, because we assume that `fty` and `retty`
          outlive `static`, the implicit requirmeents made by `call_once` are satisifed. *)
@@ -126,7 +125,7 @@ Section spawn.
                              (λ r, [r ◁ box retty])); try solve_typing; [|].
     { iIntros (tid qmax) "#LFT _ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
-      destruct c' as [[|c'|]|]; try done. iDestruct "Hc" as (?) "Hc".
+      destruct c' as [[|c'|]|]; try done.
       iApply (join_spec with "Hc"); [solve_ndisj..|]. iNext. iIntros "* Hret".
       rewrite tctx_interp_singleton tctx_hasty_val. done. }
     iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].