prove Send instances for lock guards

theories/lang/lib/lock.v

@@ -23,6 +23,8 @@ Section proof.
 
   Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
   Proof. solve_proper. Qed.
+  Global Instance lock_proto_proper l : Proper ((≡) ==> (≡)) (lock_proto l).
+  Proof. apply ne_proper, _. Qed.
 
   Lemma lock_proto_iff l R R' :
     □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.

theories/typing/lib/mutex/mutexguard.v

@@ -125,8 +125,18 @@ Section mguard.
   Qed.
 
   (* POSIX requires the unlock to occur from the thread that acquired
-     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
-     prove this. *)
+     the lock, so Rust does not implement Send for MutexGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance mutexguard_send α ty :
+    Send ty → Send (mutexguard α ty).
+  Proof.
+    iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat match goal with
+           | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
+           | |- _ => f_equiv
+           end.
+  Qed.
 End mguard.
 
 Section code.

theories/typing/lib/rwlock/rwlock.v

@@ -80,6 +80,16 @@ Section rwlock_inv.
     iFrame. iSplitR. done. iSplitL "Hh"; last by iApply "Hshr".
     iIntros "Hν". iApply "Hb". iApply ("Hh" with "Hν").
   Qed.
+
+  Lemma rwlock_inv_change_tid tid1 tid2 l γ α ty :
+    Send ty → Sync ty →
+    rwlock_inv tid1 l γ α ty ≡ rwlock_inv tid2 l γ α ty.
+  Proof.
+    intros ??. apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+    - do 5 f_equiv. iApply send_change_tid'.
+    - iApply sync_change_tid'.
+    - iApply send_change_tid'.
+  Qed.
 End rwlock_inv.
 
 Section rwlock.
@@ -200,11 +210,7 @@ Section rwlock.
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
     move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
-    iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
-    apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
-    - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid.
-    - apply bi.equiv_spec; split; iApply sync_change_tid.
-    - apply bi.equiv_spec; split; iApply send_change_tid.
+    apply bi.equiv_spec. f_equiv. apply: rwlock_inv_change_tid.
   Qed.
 End rwlock.
 

theories/typing/lib/rwlock/rwlockreadguard.v

@@ -121,8 +121,19 @@ Section rwlockreadguard.
   Qed.
 
   (* POSIX requires the unlock to occur from the thread that acquired
-     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
-     prove this. *)
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance rwlockreadguard_send α ty :
+    Send ty → Sync ty → Send (rwlockreadguard α ty).
+  Proof.
+    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat lazymatch goal with
+           | |- (ty_shr _ _ _ _) ≡ (ty_shr _ _ _ _) => by apply sync_change_tid'
+           | |- (rwlock_inv _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid
+           | |- _ => f_equiv
+           end.
+  Qed.
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -125,8 +125,19 @@ Section rwlockwriteguard.
   Qed.
 
   (* POSIX requires the unlock to occur from the thread that acquired
-     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
-     prove this. *)
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We can
+     prove this for our spinlock implementation, however. *)
+  Global Instance rwlockwriteguard_send α ty :
+    Send ty → Sync ty → Send (rwlockwriteguard α ty).
+  Proof.
+    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    repeat lazymatch goal with
+           | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
+           | |- (rwlock_inv _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid
+           | |- _ => f_equiv
+           end.
+  Qed.
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.

theories/typing/type.v

@@ -519,6 +519,18 @@ Section type.
     iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
     iExists vl. iFrame "Hm". iNext. by iApply Hsend.
   Qed.
+
+  Lemma send_change_tid' t tid1 tid2 vl :
+    Send t → t.(ty_own) tid1 vl ≡ t.(ty_own) tid2 vl.
+  Proof.
+    intros ?. apply: anti_symm; apply send_change_tid.
+  Qed.
+
+  Lemma sync_change_tid' t κ tid1 tid2 l :
+    Sync t → t.(ty_shr) κ tid1 l ≡ t.(ty_shr) κ tid2 l.
+  Proof.
+    intros ?. apply: anti_symm; apply sync_change_tid.
+  Qed.
 End type.
 
 Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=