show that pointer types are Send/Sync

theories/lang/heap.v

@@ -186,7 +186,7 @@ Section heap.
     - by iIntros "[% [$ Hl2]]"; subst.
   Qed.
 
-  Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
+  Lemma heap_mapsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
     (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
     l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
   Proof.
@@ -201,6 +201,13 @@ Section heap.
       iSplitL "Hmt1 Hown"; iExists _; by iFrame.
   Qed.
 
+  Lemma heap_mapsto_pred_wand l q Φ1 Φ2 :
+    l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
+  Proof.
+    iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
+    iFrame "Hm". iApply "Hwand". done.
+  Qed.
+
   Lemma heap_mapsto_vec_combine l q vl :
     vl ≠ [] →
     l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
@@ -210,7 +217,7 @@ Section heap.
     by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
   Qed.
 
-  Global Instance heap_mapsto_vec_pred_fractional l (P : list val → iProp Σ):
+  Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
     (∀ vl, PersistentP (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
   Proof.
     intros p q q'. iSplit.
@@ -233,7 +240,7 @@ Section heap.
         { rewrite -Heq /ll. done. }
         rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
   Qed.
-  Global Instance heap_mapsto_vec_pred_as_fractional l q (P : list val → iProp Σ):
+  Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
     (∀ vl, PersistentP (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
   Proof. split. done. apply _. Qed.
 

theories/typing/own.v

@@ -4,7 +4,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm typing uniq_bor type_context.
+From lrust.typing Require Import uniq_bor type_context.
 
 Section own.
   Context `{typeG Σ}.
@@ -116,6 +116,24 @@ Section own.
     Proper (eqtype E L ==> eqtype E L) (own n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
+  Global Instance own_send n ty :
+    Send ty → Send (own n ty).
+  Proof.
+    iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l) "[% [Hm H†]]". subst vl.
+    iExists _. iSplit; first done. iFrame "H†". iNext.
+    iApply (heap_mapsto_pred_wand with "Hm"). iIntros (vl) "?". by iApply Hsend.
+  Qed.
+
+  Global Instance own_sync n ty :
+    Sync ty → Sync (own n ty).
+  Proof.
+    iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
+    iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iMod ("Hshr" with "* [] Htok") as "Hfin"; first done. iModIntro. iNext.
+    iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
+    iMod "Hfin" as "[Hshr $]". by iApply Hsync.
+  Qed.
+
   (** Typing *)
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [TCtx_hasty p (own n ty)]

theories/typing/shr_bor.v

@@ -30,6 +30,13 @@ Section shr_bor.
   Global Instance subtype_shr_bor_proper E L κ :
     Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
   Proof. intros ??[]. by split; apply subtype_shr_bor_mono. Qed.
+
+  Global Instance shr_send κ ty :
+    Sync ty → Send (shr_bor κ ty).
+  Proof.
+    iIntros (Hsync tid1 tid2 vl) "H". iDestruct "H" as (l) "[% Hshr]".
+    iExists _. iSplit; first done. by iApply Hsync.
+  Qed.
 End shr_bor.
 
 Notation "&shr{ κ } ty" := (shr_bor κ ty)

theories/typing/sum.v

@@ -170,7 +170,7 @@ Section sum.
       { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
         apply shr_locsE_subseteq. omega. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-      rewrite -(heap_mapsto_vec_prop_op _ q' q'02); last (by intros; apply ty_size_eq).
+      rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
       iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
       iExists q'. iModIntro. iSplitL "Hown1 HownC1".

theories/typing/uniq_bor.v

@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import lft_contexts type_context shr_bor perm typing.
+From lrust.typing Require Import lft_contexts type_context shr_bor.
 
 Section uniq_bor.
   Context `{typeG Σ}.
@@ -103,6 +103,27 @@ Section uniq_bor.
   Global Instance subtype_uniq_proper E L κ :
     Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
   Proof. split; by apply subtype_uniq_mono. Qed.
+
+  Global Instance uniq_send κ ty :
+    Send ty → Send (uniq_bor κ ty).
+  Proof.
+    iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l P) "[[% #HPiff] H]".
+    iExists _, _. iFrame "H". iSplit; first done. iAlways. iSplit.
+    - iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
+      { by iApply "HPiff". }
+      clear dependent vl. iIntros (vl) "?". by iApply Hsend.
+    - iIntros "HP". iApply "HPiff". iApply (heap_mapsto_pred_wand with "HP").
+      clear dependent vl. iIntros (vl) "?". by iApply Hsend.
+  Qed.
+
+  Global Instance uniq_sync κ ty :
+    Sync ty → Sync (uniq_bor κ ty).
+  Proof.
+    iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
+    iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iMod ("Hshr" with "* [] Htok") as "Hfin"; first done. iClear "Hshr".
+    iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
+  Qed.
 End uniq_bor.
 
 Notation "&uniq{ κ } ty" := (uniq_bor κ ty)