rwlockreadguard type

_CoqProject

@@ -64,6 +64,7 @@ theories/typing/lib/refcell/refmut_code.v
 theories/typing/lib/refcell/refmut.v
 theories/typing/lib/refcell/ref.v
 theories/typing/lib/rwlock/rwlock.v
+theories/typing/lib/rwlock/rwlockreadguard.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v

theories/typing/lib/rwlock/rwlockreadguard.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lifetime Require Import at_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.lib.rwlock Require Import rwlock.
+From gpfsl.gps Require Import middleware.
+Set Default Proof Using "Type".
+
+Section rwlockreadguard.
+  Context `{typeG Σ, rwlockG Σ}.
+
+  (* Original Rust type:
+    pub struct RwLockReadGuard<'a, T: ?Sized + 'a> {
+        __lock: &'a RwLock<T>,
+    }
+  *)
+
+  Program Definition rwlockreadguard (α : lft) (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] =>
+           ∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+             α ⊑ β ∗ q.[ν] ∗ ⎡ own γs (◯ reading_st q ν) ⎤ ∗
+             (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
+             (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
+                    &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS) ∗
+                    (∃ vl, GPS_SWSharedReader l () vl q γ))
+         | _ => False
+         end;
+       ty_shr κ tid l :=
+         ∃ (l' : loc),
+           &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+           ▷ ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) |}%I.
+  Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
+    iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+    destruct vl as [|[[|l'|]|][]];
+      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 (q') "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (γs) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (β) "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.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+    iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
+    iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
+    { iApply bor_fracture; try done. constructor; [by rewrite Qp_mult_1_r|apply _]. }
+    iExists _. iFrame "#". iApply ty_shr_mono; last done.
+    iApply lft_intersect_mono; last done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (α ty κ κ' tid l) "#Hκ'κ H". iDestruct "H" as (l') "[#Hf #Hshr]".
+    iExists l'. iSplit; first by iApply frac_bor_shorten.
+    iApply ty_shr_mono; last done. iApply lft_intersect_mono; last done.
+    iApply lft_incl_refl.
+  Qed.
+
+  Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+  Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_proto_lc_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+  Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  (* The rust type is not covariant, although it probably could (cf. refcell).
+     This would require changing the definition of the type, though. *)
+  Global Instance rwlockreadguard_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockreadguard.
+  Proof.
+    iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
+    iDestruct (proj1 Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
+    iDestruct (rwlock_proto_lc_proper with "HL") as "#Hty1ty2"; first done.
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    - done.
+    - iIntros (tid [|[[]|][]]) "H"; try done.
+      iDestruct "H" as (ν q' γs β) "(#Hshr & #H⊑ & Htok & Hown & Hinh & Hinv)".
+      iExists ν, q', γs, β. 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.
+      + iDestruct "Hinv" as (γ tyO tyS) "(lc & inv & R)".
+        iExists γ, tyO, tyS. iFrame "R inv". by iApply ("Hty1ty2" with "HE lc").
+    - iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
+      iFrame. iApply ty_shr_mono; last by iApply "Hs".
+      iApply lft_intersect_mono. done. iApply lft_incl_refl.
+  Qed.
+  Global Instance rwlockreadguard_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L))
+           rwlockreadguard.
+  Proof. intros ??????. by apply rwlockreadguard_mono. Qed.
+  Lemma rwlockreadguard_mono' E L α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    subtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
+  Proof. intros. by eapply rwlockreadguard_mono. Qed.
+  Global Instance rwlockreadguard_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) rwlockreadguard.
+  Proof. intros ??[]?? EQ. split; apply rwlockreadguard_mono'; try done; apply EQ. Qed.
+  Lemma rwlockreadguard_proper' E L α1 α2 ty1 ty2 :
+    lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
+    eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
+  Proof. intros. by eapply rwlockreadguard_proper. Qed.
+
+  (* Rust requires the type to also be Send.  Not sure why. *)
+  Global Instance rwlockreadguard_sync α ty :
+    Sync ty → Sync (rwlockreadguard α ty).
+  Proof.
+    move=>?????/=. apply bi.exist_mono=>?. by rewrite sync_change_tid.
+  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. *)
+End rwlockreadguard.
+
+Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.