WIP: rwlock code

_CoqProject

@@ -65,6 +65,7 @@ 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/lib/rwlock/rwlockwriteguard.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v

theories/typing/lib/rwlock/rwlock_code.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import at_borrow.
+From lrust.typing Require Import typing option.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
+From gpfsl.gps Require Import middleware.
+Set Default Proof Using "Type".
+
+Section rwlock_functions.
+  Context `{typeG Σ, rwlockG Σ}.
+
+  (* Constructing a rwlock. *)
+  Definition rwlock_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #(S ty.(ty_size))] in
+      "r" +ₗ #0 <- #0;;
+      "r" +ₗ #1 <-{ty.(ty_size)} !"x";;
+       delete [ #ty.(ty_size) ; "x"];; return: ["r"].
+
+  Lemma rwlock_new_type ty `{!TyWf ty} :
+    typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
+    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
+    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
+    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
+    iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
+    rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
+    rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
+    iIntros "[Hr↦1 Hx↦]". wp_seq.
+    iApply wp_hist_inv; [done|iIntros "HI"].
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (rwlock ty)]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+      iSplitL "Hx↦".
+      - iExists _. rewrite uninit_own. auto.
+      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* The other direction: getting ownership out of a rwlock.
+     Note: as we ignore poisonning, this cannot fail. *)
+  Definition rwlock_into_inner ty : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #ty.(ty_size)] in
+      "r" <-{ty.(ty_size)} !("x" +ₗ #1);;
+       delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
+
+  Lemma rwlock_into_inner_type ty `{!TyWf ty} :
+    typed_val (rwlock_into_inner ty) (fn(∅; rwlock ty) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
+    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
+    iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ [HI Hx]]"; try iDestruct "Hx" as ">[]".
+    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
+    iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
+    iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+    wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
+    iIntros "[Hr↦ Hx↦1]". wp_seq.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+      iSplitR "Hr↦ Hx".
+      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
+      - iExists vl. iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition rwlock_get_mut : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      "x" <- "x'" +ₗ #1;;
+      return: ["x"].
+
+  Lemma rwlock_get_mut_type ty `{!TyWf ty} :
+    typed_val rwlock_get_mut (fn(∀ α, ∅; &uniq{α} (rwlock ty)) → &uniq{α} ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iIntros (tid) "#LFT HE Hna HL HC HT".
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
+    iAssert (&{α} (⎡ hist_inv ⎤ ∗ ∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
+        (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
+    { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
+      - iIntros "[H1 H2]". iDestruct "H1" as "[? H1]".
+        iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
+        iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
+      - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ [HI H]]"; try done.
+        rewrite heap_mapsto_vec_cons. iFrame "HI".
+        iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
+        iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
+    iApply (type_type _ _ _
+            [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
+            with "[] LFT HE Hna HL HC [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+      iNext. iExists _. rewrite uninit_own. iFrame. }
+    iApply type_assign; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Acquiring a read lock. *)
+  Definition rwlock_try_read : val :=
+    funrec: <> ["x"] :=
+      let: "r" := new [ #2 ] in
+      let: "x'" := !"x" in
+    withcont: "k":
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      let: "n" := !ʳˡˣ"x'" in
+        if: "n" ≤ #-1 then
+          "r" <-{Σ none} ();;
+          "k" []
+        else
+          if: CAS "x'" "n" ("n" + #1) AcqRel Relaxed then
+            "r" <-{Σ some} "x'";;
+            "k" []
+          else "loop" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma rwlock_try_read_type ty `{!TyWf ty} :
+    typed_val rwlock_try_read
+        (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(rwlock ty));
+                                            r ◁ box (option (rwlockreadguard α ty))]));
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
+      simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|].
+      iApply type_jump; solve_typing. }
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ _; x' ◁ _; r ◁ _]));
+      [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
+      simpl_subst.
+    { iApply type_jump; solve_typing. }
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
+    iDestruct "Hx'" as (β) "#[Hαβ Hinv]".
+    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βtok1 Hβtok2] Hclose']". done.
+    iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & R) & Hinv)".
+    iDestruct "R" as (vR) "R".
+    wp_bind (!ʳˡˣ(LitV lx))%E.
+    iMod (at_bor_acc with "LFT Hinv Hβtok1") as (Vb) "[INV Hclose'']"; [done..|].
+    iApply (GPS_SWRawReader_read with "[$R $INV]"); [solve_ndisj|by left|..].
+    { iNext. iIntros (? _). iLeft. iModIntro.
+      iIntros (?). by iApply rwlock_interp_duplicable. }
+    iNext. iIntros ([] v') "(_ & R' & INV & Int)".
+    iDestruct (acq_exist with "Int") as (st) "Int".
+    iDestruct (acq_sep_elim with "Int") as "[Int _]".
+    iDestruct (acq_pure_elim with "Int") as %?. subst v'.
+    iMod ("Hclose''" with "INV") as "Hβtok1".
+    iModIntro. wp_let. wp_op; case_bool_decide as Hm1; wp_if.
+    - iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type _ _ _
+              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      iApply (type_sum_unit (option $ rwlockreadguard α ty));
+        [solve_typing..|]; first last.
+      simpl. iApply type_jump; solve_typing.
+    - wp_op. wp_bind (CAS _ _ _ _ _).
+      iMod (at_bor_acc with "LFT Hinv Hβtok1") as (Vb') "[INV Hclose'']"; [done..|].
+
+      iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
+      destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+      + 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 ∗
+                         ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
+          with "[> Hlx Hownst Hst Hβtok2]"
+          as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
+        { destruct st' as [[|[[agν q] n]|]|]; try done.
+          - iDestruct "Hst" as (ν q') "(Hag & #H† & Hh & #Hshr & #Hqq' & [Hν1 Hν2])".
+            iExists _, _. iFrame "Hν1". iDestruct "Hag" as %Hag. iDestruct "Hqq'" as %Hqq'.
+            iMod (own_update with "Hownst") as "[Hownst ?]".
+            { apply auth_update_alloc,
+              (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
+              split; [split|].
+              - by rewrite /= Hag agree_idemp.
+              - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+                apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
+                apply Qcplus_le_mono_r, Qp_ge_0.
+              - done. }
+            iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
+            iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
+            rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
+          - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
+            iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
+              auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
+            rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
+            iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+            iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
+            iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
+            { iApply lft_intersect_incl_l. }
+            iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". solve_ndisj.
+            iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
+            iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
+            rewrite Qp_div_2. iSplitL; last done.
+            iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+        iMod ("Hclose''" with "[$INV]") as "Hβtok1". iModIntro. wp_case.
+        iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+        iApply (type_type  _ _ _
+                   [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
+                     #lx ◁ rwlockreadguard α 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 "∗#". 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.
+      + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
+        iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
+        iModIntro. wp_case. iMod ("Hclose'" with "[$]") as "Hα".
+        iMod ("Hclose" with "Hα HL") as "HL".
+        iSpecialize ("Hk" with "[]"); first solve_typing.
+        iApply ("Hk" $! [#] with "Hna HL").
+        rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
+        iExists _. iSplit. done. simpl. eauto.
+  Qed.
+
+  (* Acquiring a write lock. *)
+  Definition rwlock_try_write : val :=
+    funrec: <> ["x"] :=
+    withcont: "k":
+      let: "r" := new [ #2 ] in
+      let: "x'" := !"x" in
+      if: CAS "x'" #0 #(-1) then
+        "r" <-{Σ some} "x'";;
+        "k" ["r"]
+      else
+        "r" <-{Σ none} ();;
+        "k" ["r"]
+    cont: "k" ["r"] :=
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma rwlock_try_write_type ty `{!TyWf ty} :
+    typed_val rwlock_try_write
+        (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α}(rwlock ty));
+                                        r!!!0 ◁ box (option (rwlockwriteguard α ty))]));
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
+      simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_deref; [solve_typing..|].
+    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
+    iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+    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βtok Hclose']". done.
+    wp_bind (CAS _ _ _).
+    iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
+    iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
+    - iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
+      iNext. iIntros "Hlx".
+      iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iModIntro. wp_case.
+      iApply (type_type _ _ _
+              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+      iApply (type_sum_unit (option $ rwlockwriteguard α ty));
+        [solve_typing..|]; first last.
+      rewrite /option /=. iApply type_jump; solve_typing.
+    - iApply (wp_cas_int_suc with "Hlx"). iIntros "!> Hlx".
+      iMod (own_update with "Hownst") as "[Hownst ?]".
+      { by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
+      iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
+      iModIntro. wp_case. iMod ("Hclose'" with "Hβtok") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type  _ _ _
+                   [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
+                     #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 "∗#". }
+      iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
+      simpl. iApply type_jump; solve_typing.
+  Qed.
+End rwlock_functions.

theories/typing/lib/rwlock/rwlockwriteguard.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 util typing.
+From lrust.typing.lib.rwlock Require Import rwlock.
+From gpfsl.gps Require Import middleware.
+Set Default Proof Using "Type".
+
+Section rwlockwriteguard.
+  Context `{typeG Σ, rwlockG Σ}.
+
+  (* Original Rust type (we ignore poisoning):
+      pub struct RwLockWriteGuard<'a, T: ?Sized + 'a> {
+          __lock: &'a RwLock<T>,
+          __poison: poison::Guard,
+      }
+  *)
+
+  Program Definition rwlockwriteguard (α : lft) (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] =>
+           ∃ γs β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
+             α ⊑ β ∗ ⎡ own γs (◯ writing_st) ⎤ ∗
+             (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
+                    &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS) ∗
+                    GPS_SWRawReader l () #(-1) γ)
+         | _ => False
+         end;
+       ty_shr κ tid l :=
+         ∃ (l' : loc),
+           &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
+               ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) ∗ q.[α ⊓ κ] |}%I.
+  Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q HE) "#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 (γs) "Hb". done.
+    iMod (bor_exists with "LFT Hb") as (β) "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.
+    iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
+       goal, as does "iApply (lft_intersect_mono with ">")". *)
+    iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
+    iExists _. iSplit.
+    - by iApply frac_bor_shorten.
+    - iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+  Qed.
+
+  Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+  Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
+  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 rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance rwlockwriteguard_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockwriteguard.
+  Proof.
+    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
+    iDestruct (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; [done|iSplit; iAlways].
+    - iIntros (tid [|[[]|][]]) "H"; try done.
+      iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hinv)".
+      iExists γs, β. iFrame "Hown". iSplit; last iSplit.
+      + iApply bor_iff; last done.
+        iIntros "!>!#". iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+        iExists vl; iFrame; by iApply "Ho".
+      + 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') "H". iExists l'.
+      iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      by iApply "Hs".
+  Qed.
+  Global Instance rwlockwriteguard_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) rwlockwriteguard.
+  Proof. intros ??????. by apply rwlockwriteguard_mono. Qed.
+  Lemma rwlockwriteguard_mono' E L α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    subtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2) .
+  Proof. intros. by eapply rwlockwriteguard_mono. Qed.
+  Global Instance rwlockwriteguard_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E  L) rwlockwriteguard.
+  Proof. intros ??[]???. split; by apply rwlockwriteguard_mono'. Qed.
+  Lemma rwlockwriteguard_proper' E L α1 α2 ty1 ty2 :
+    lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
+    eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
+  Proof. intros. by eapply rwlockwriteguard_proper. Qed.
+
+  (* Rust requires the type to also be Send.  Not sure why. *)
+  Global Instance rwlockwriteguard_sync α ty :
+    Sync ty → Sync (rwlockwriteguard α ty).
+  Proof.
+    move=>?????/=. apply bi.exist_mono=>?. do 6 f_equiv.
+    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 rwlockwriteguard.
+
+Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.