From 4404030fe9ef4be0375ccb93e4af1f051ef588b4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 21 Nov 2020 18:22:52 +0100
Subject: [PATCH] Prove more precise Sync/Send instances for RwLock guards.

---
 theories/typing/lib/rwlock/rwlock.v           | 50 ++++++++++++-------
 theories/typing/lib/rwlock/rwlock_code.v      |  6 +--
 theories/typing/lib/rwlock/rwlockreadguard.v  | 15 +++---
 .../typing/lib/rwlock/rwlockreadguard_code.v  |  4 +-
 theories/typing/lib/rwlock/rwlockwriteguard.v | 15 +++---
 .../typing/lib/rwlock/rwlockwriteguard_code.v |  3 +-
 6 files changed, 54 insertions(+), 39 deletions(-)

diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 38434666..b5f64b88 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -30,46 +30,49 @@ Definition rwlockN := lrustN .@ "rwlock".
 Section rwlock_inv.
   Context `{!typeG Σ, !rwlockG Σ}.
 
-  Definition rwlock_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
+  Definition rwlock_inv tid_own tid_shr (l : loc) (γ : gname) (α : lft) ty
+    : iProp Σ :=
     (∃ st, l ↦ #(Z_of_rwlock_st st) ∗ own γ (● st) ∗
       match st return _ with
       | None =>
         (* Not locked. *)
-        &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
+        &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid_own)
       | Some (Cinr (agν, q, n)) =>
         (* Locked for read. *)
         ∃ (ν : lft) q', agν ≡ to_agree ν ∗
                 □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]) ∗
-                ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
-                ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+                ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid_own)) ∗
+                ty.(ty_shr) (α ⊓ ν) tid_shr (l +ₗ 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
       | _ => (* Locked for write. *) True
       end)%I.
 
-  Global Instance rwlock_inv_type_ne n tid l γ α :
-    Proper (type_dist2 n ==> dist n) (rwlock_inv tid l γ α).
+  Global Instance rwlock_inv_type_ne n tid_own tid_shr l γ α :
+    Proper (type_dist2 n ==> dist n) (rwlock_inv tid_own tid_shr l γ α).
   Proof.
     solve_proper_core
       ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
-  Global Instance rwlock_inv_ne tid l γ α : NonExpansive (rwlock_inv tid l γ α).
+  Global Instance rwlock_inv_ne tid_own tid_shr l γ α :
+    NonExpansive (rwlock_inv tid_own tid_shr l γ α).
   Proof.
     intros n ???. eapply rwlock_inv_type_ne, type_dist_dist2. done.
   Qed.
 
   Lemma rwlock_inv_proper E L ty1 ty2 q :
     eqtype E L ty1 ty2 →
-    llctx_interp L q -∗ ∀ tid l γ α, □ (elctx_interp E -∗
-    rwlock_inv tid l γ α ty1 -∗ rwlock_inv tid l γ α ty2).
+    llctx_interp L q -∗ ∀ tid_own tid_shr l γ α, □ (elctx_interp E -∗
+    rwlock_inv tid_own tid_shr l γ α ty1 -∗
+    rwlock_inv tid_own tid_shr l γ α ty2).
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
-                &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
+    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid_own) -∗
+                &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid_own)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
@@ -81,15 +84,22 @@ Section rwlock_inv.
     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.
+  Lemma rwlock_inv_change_tid_own tid_own1 tid_own2 tid_shr l γ α ty :
+    Send ty →
+    rwlock_inv tid_own1 tid_shr l γ α ty ≡ rwlock_inv tid_own2 tid_shr l γ α ty.
   Proof.
-    intros ??. apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+    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.
+
+  Lemma rwlock_inv_change_tid_shr tid_own tid_shr1 tid_shr2 l γ α ty :
+    Sync ty →
+    rwlock_inv tid_own tid_shr1 l γ α ty ≡ rwlock_inv tid_own tid_shr2 l γ α ty.
+  Proof.
+    intros ?. apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+    iApply sync_change_tid'.
+  Qed.
 End rwlock_inv.
 
 Section rwlock.
@@ -110,7 +120,8 @@ Section rwlock.
          | #(LitInt z) :: vl' => ⌜-1 ≤ z⌝ ∗ ty.(ty_own) tid vl'
          | _ => False
          end%I;
-       ty_shr κ tid l := (∃ α γ, κ ⊑ α ∗ &at{α,rwlockN}(rwlock_inv tid l γ α ty))%I |}.
+       ty_shr κ tid l :=
+         (∃ α γ, κ ⊑ α ∗ &at{α,rwlockN}(rwlock_inv tid tid l γ α ty))%I |}.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
     iIntros "[_ %] !% /=". congruence.
@@ -129,7 +140,7 @@ Section rwlock.
       iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
-    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with "[> -Hclose]"
+    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
@@ -210,7 +221,8 @@ Section rwlock.
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
     move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
-    apply bi.equiv_spec. f_equiv. apply: rwlock_inv_change_tid.
+    apply bi.equiv_spec. f_equiv.
+    by rewrite rwlock_inv_change_tid_own rwlock_inv_change_tid_shr.
   Qed.
 End rwlock.
 
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index c3fbbc38..c75f3fd4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -181,7 +181,7 @@ Section rwlock_functions.
       + iApply (wp_cas_int_suc with "Hlx"). iNext. iIntros "Hlx".
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                          ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
-                         own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
+                         own γ (◯ reading_st qν ν) ∗ rwlock_inv tid tid lx γ β ty ∗
                          ((1).[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I
           with "[> Hlx Hownst Hst Hβtok2]"
           as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
@@ -220,7 +220,7 @@ Section rwlock_functions.
               with "[] LFT HE Hna HL Hk"); first last.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                   tctx_hasty_val' //. iFrame.
-          iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
+          iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
         simpl. iApply type_jump; solve_typing.
@@ -294,7 +294,7 @@ Section rwlock_functions.
                      #lx ◁ rwlockwriteguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
+                tctx_hasty_val' //. iFrame.  iExists _, _, _. iFrame "∗#". }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 35b4be01..55ffb196 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -20,8 +20,8 @@ Section rwlockreadguard.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc l) ] =>
-           ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
-             α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+           ∃ ν q γ β tid_own, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+             α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid_own tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
              (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν])
          | _ => False
@@ -42,6 +42,7 @@ Section rwlockreadguard.
     iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (tid_own) "Hb". done.
     iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
     iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
     iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
@@ -86,8 +87,8 @@ Section rwlockreadguard.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
-      iDestruct "H" as (ν q' γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
-      iExists ν, q', γ, β. iFrame "∗#". iSplit; last iSplit.
+      iDestruct "H" as (ν q' γ β tid_own) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
+      iExists ν, q', γ, β, tid_own. iFrame "∗#". iSplit; last iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
         iApply lft_intersect_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.
@@ -124,13 +125,13 @@ Section rwlockreadguard.
      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).
+    Sync ty → Send (rwlockreadguard α ty).
   Proof.
-    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    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
+           | |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_shr
            | |- _ => f_equiv
            end.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 83babbae..d4115119 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -71,7 +71,7 @@ Section rwlockreadguard_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
-    iDestruct "Hx'" as (ν q γ β) "(Hx' & #Hαβ & #Hinv & Hν & H◯ & H†)".
+    iDestruct "Hx'" as (ν q γ β tid_own) "(Hx' & #Hαβ & #Hinv & Hν & H◯ & H†)".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     wp_bind (!ˢᶜ#lx')%E.
@@ -83,7 +83,7 @@ Section rwlockreadguard_functions.
     iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
     destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
     + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ ↑lft_userN]▷=>
-               (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
+               (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid_own tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
       { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
            %option_included Hv]%auth_both_valid_discrete.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 80a197ec..651ff4df 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -21,8 +21,8 @@ Section rwlockwriteguard.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc l) ] =>
-           ∃ γ β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
-             α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+           ∃ γ β tid_shr, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
+             α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid tid_shr l γ β ty) ∗
              own γ (◯ writing_st)
          | _ => False
          end;
@@ -41,6 +41,7 @@ Section rwlockwriteguard.
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (tid_shr) "Hb". done.
     iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
     iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
@@ -84,8 +85,8 @@ Section rwlockwriteguard.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
-      iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
-      iExists γ, β. iFrame "∗#". iSplit; last iSplit.
+      iDestruct "H" as (γ β tid_shr) "(Hb & #H⊑ & #Hinv & Hown)".
+      iExists γ, β, tid_shr. iFrame "∗#". iSplit; last iSplit.
       + iApply bor_iff; last done.
         iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".
@@ -128,13 +129,13 @@ Section rwlockwriteguard.
      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).
+    Send ty → Send (rwlockwriteguard α ty).
   Proof.
-    iIntros (???? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
+    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
+           | |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_own
            | |- _ => f_equiv
            end.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index df241116..15cb2bee 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -79,6 +79,7 @@ Section rwlockwriteguard_functions.
     rewrite heap_mapsto_vec_singleton.
     iMod (bor_exists with "LFT H") as (γ) "H". done.
     iMod (bor_exists with "LFT H") as (δ) "H". done.
+    iMod (bor_exists with "LFT H") as (tid_shr) "H". done.
     iMod (bor_sep with "LFT H") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
     iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
@@ -116,7 +117,7 @@ Section rwlockwriteguard_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
-    iDestruct "Hx'" as (γ β) "(Hx' & #Hαβ & #Hinv & H◯)".
+    iDestruct "Hx'" as (γ β tid_own) "(Hx' & #Hαβ & #Hinv & H◯)".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
       [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
-- 
GitLab