fn, int, bool are Send and Sync

theories/typing/bool.v

@@ -9,6 +9,9 @@ Section bool.
     {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance bool_send : Send bool.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.

theories/typing/function.v

@@ -18,6 +18,9 @@ Section fn.
     iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
+  Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma fn_subtype_ty A n E0 L0 E tys1 tys2 ty1 ty2 :
     (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ _) (tys1 x : vec _ _)) →
     (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →

theories/typing/int.v

@@ -9,6 +9,9 @@ Section int.
     {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance int_send : Send int.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.

theories/typing/type.v

@@ -178,6 +178,13 @@ Section type.
       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.