WIP: rwlock readguard code

_CoqProject

@@ -67,6 +67,7 @@ theories/typing/lib/rwlock/rwlock.v
 theories/typing/lib/rwlock/rwlockreadguard.v
 theories/typing/lib/rwlock/rwlockwriteguard.v
 theories/typing/lib/rwlock/rwlock_code.v
+theories/typing/lib/rwlock/rwlockwriteguard_code.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v

theories/typing/lib/rwlock/rwlock.v

@@ -111,9 +111,7 @@ Section rwlock_inv.
     iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
     apply prod_update; simpl; [|by apply rwown_agree_update].
     apply auth_update_alloc.
-    rewrite (_: Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive))
-                       = Some (Cinr (to_agree ν, (1/2)%Qp, 1%positive)) ⋅ ε);
-              [by apply op_local_update_discrete|by rewrite right_id_L].
+    rewrite -(right_id None op (Some _)). by apply op_local_update_discrete.
   Qed.
 
   Lemma rwown_update_read ν (n: positive) (q q': frac) γs
@@ -132,9 +130,7 @@ Section rwlock_inv.
     rewrite Pos.add_comm Qp_plus_comm -pos_op_plus
             -{2}(agree_idemp (to_agree _)) -frac_op'
             -2!pair_op -Cinr_op Some_op.
-    rewrite {2}(_: Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive))
-               = Some (Cinr (to_agree ν, (q' / 2)%Qp, 1%positive)) ⋅ ε);
-      [|by rewrite right_id_L].
+    rewrite -{2}(right_id None op (Some (Cinr (_, (q' /2)%Qp, _)))).
     apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
     - by rewrite /= agree_idemp.
     - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
@@ -153,8 +149,43 @@ Section rwlock_inv.
     iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
     apply prod_update; simpl; [|by apply rwown_agree_update].
     apply auth_update_alloc.
-    rewrite (_: Some (Cinl (Excl ())) = Some (Cinl (Excl ())) ⋅ ε);
-              [by apply op_local_update_discrete|by rewrite right_id_L].
+    rewrite -(right_id None op (Some _)). by apply op_local_update_discrete.
+  Qed.
+
+  Lemma rwown_update_write_dealloc γs :
+    let st : rwlock_st := Some (inl ()) in
+    rwown γs (main_st st) -∗ rwown γs (sub_st st) -∗ rwown γs writing_st
+    ==∗ rwown γs (main_st None) ∗ rwown γs (sub_st None).
+  Proof.
+    iIntros (st) "m s w".
+    rewrite -rwown_st_global_main_sub.
+    iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
+    iCombine "ms" "w" as "msw".
+    iMod (own_update (A:=rwlockR) with "msw") as "$"; [|done].
+    apply prod_update; simpl; [|by apply rwown_agree_update].
+    apply auth_update_dealloc.
+    rewrite -(right_id None op (Some _)). by apply cancel_local_update_unit, _.
+  Qed.
+
+  Lemma rown_main_reading_st st q ν γs:
+    rwown γs (main_st st) -∗  rwown γs (reading_st q ν) -∗ 
+    ⌜∃ q' n, st = Some (inr (ν,q',n))⌝.
+  Proof.
+    iIntros "m r". iCombine "m" "r" as "mr".
+    iDestruct (own_valid with "mr") as %[[INCL VAL]%auth_valid_discrete_2 ?].
+    iPureIntro. destruct st as [[[]|[[]]]|].
+    - move : INCL =>
+        /Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[?[?[?[??//]]]]]]].
+      inversion Eq.
+    - move : INCL =>
+        /Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[a[b[Eqa[Eqb INCL]]]]]]].
+      + inversion Eq as [| ?? Eq1 |]. inversion Eq1 as [Eq2].
+        inversion Eq2 as [Eq3 ]. simpl in Eq3. apply to_agree_inj in Eq3.
+        inversion Eq3. by do 2 eexists.
+      + inversion Eqa. inversion Eqb. subst a b.
+        apply prod_included in INCL as [[INCL%to_agree_included _]%prod_included _].
+        inversion INCL. by do 2 eexists.
+    - by apply option_included in INCL as [?|[?[?[?[??]]]]].
   Qed.
 
   (* GPS protocol definitions *)

theories/typing/lib/rwlock/rwlock_code.v

@@ -356,7 +356,7 @@ Section rwlock_functions.
     iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
     iDestruct (bi.later_exist_2 with "mst") as ">mst".
     set Q : () → vProp Σ :=
-      (λ _, (∃ st, rwown γs (main_st st) ∗ rwown γs (sub_st st)) ∗
+      (λ _, rwown γs (main_st (Some (inl ()))) ∗ rwown γs (sub_st (Some (inl ()))) ∗
              &{β}tyO ∗ rwown γs writing_st)%I.
     set R : () → lit → vProp Σ := (λ _ _, True)%I.
     set P : vProp Σ := ((∃ st, rwown γs (main_st st)))%I.
@@ -380,15 +380,15 @@ Section rwlock_functions.
       iDestruct (rwown_main_sub_agree with "mst sst") as %Eqst2. subst st.
       set st': rwlock_st := Some (inl ()).
       iMod (rwown_update_write γs with "mst sst") as "(mst'&sst'&wst)".
-      iModIntro. iFrame "Hst wst". iSplitR ""; [iExists _; by iFrame|].
+      iModIntro. iFrame "mst' sst' Hst wst".
       iSplitL ""; iExists st'; [done|by iFrame "Share"]. }
 
     iNext. simpl.
     iIntros (b v' [])
-            "(INV & _ &[([%%] & _ & mst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
-    - subst b v'. iDestruct "mst" as (st2) "[mst sst]".
+            "(INV & _ &[([%%] &_& mst & sst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
+    - subst b v'.
       iMod ("Hclose''" with "[mst INV]") as "Hβtok".
-      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists st2. }
+      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_case.
       iApply (type_type  _ _ _
@@ -398,7 +398,7 @@ Section rwlock_functions.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame "Hx Hr".
         iExists γs, β. iSplitL "Hβ"; [by iApply (bor_iff with "[$EqO] Hβ")|].
-        iFrame "Hαβ wst". iSplitL "sst"; [by iExists st2|].
+        iFrame "Hαβ wst sst".
         iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.

theories/typing/lib/rwlock/rwlockreadguard_code.v

+From Coq.QArith Require Import Qcanon.
+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 rwlockreadguard.
+From gpfsl.gps Require Import middleware.
+Set Default Proof Using "Type".
+
+Section rwlockreadguard_functions.
+  Context `{typeG Σ, rwlockG Σ}.
+
+  (* Turning a rwlockreadguard into a shared borrow. *)
+  Definition rwlockreadguard_deref : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" +ₗ #1 in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
+    typed_val rwlockreadguard_deref
+      (fn(∀ '(α, β), ∅; &shr{α}(rwlockreadguard β ty)) → &shr{α} 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').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+    rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
+    iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockreadguard β ty));
+                              #(l' +ₗ 1) ◁ &shr{α}ty]
+      with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
+      by iApply lft_incl_refl. }
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Dropping a rwlockreadguard and releasing the corresponding lock. *)
+  Definition rwlockreadguard_drop : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      let: "n" := !ʳˡˣ"x'" in
+      if: CAS "x'" "n" ("n" - #1) Relaxed Relaxed AcqRel then
+        delete [ #1; "x"];;
+        let: "r" := new [ #0] in return: ["r"]
+      else "loop" [].
+
+  Lemma rwlockreadguard_drop_type ty `{!TyWf ty} :
+    typed_val rwlockreadguard_drop (fn(∀ α, ∅; rwlockreadguard α ty) → unit).
+  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.
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ _; x' ◁ _]));
+      [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 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 γs β) "(Hx' & #Hαβ & Hν & H◯ & H† & #Hinv)".
+    iDestruct "Hinv" as (γ tyO tyS) "((EqO & EqS & PP) & Hinv)".
+    iDestruct "PP" as (vP) "PP".
+    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.
+    iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb) "[INV Hcloseβ]"; [done..|].
+    iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
+    iDestruct "mst" as (st1) ">mst".
+    iApply (GPS_PPRaw_read with "[$PP $INV]"); [solve_ndisj|by left|..].
+    { iNext. iIntros (? _). iLeft.
+      iIntros "!>" (?). by iApply rwlock_interp_duplicable. }
+    iNext. iIntros ([] v') "(_ & _ & INV & Int)".
+    iDestruct (rwlock_interp_read_acq with "Int") as (st2) "Int".
+    iDestruct "Int" as %?. subst v'.
+    iMod ("Hcloseβ" with "[mst INV]") as "Hβ".
+    { rewrite rwlock_proto_inv_split. iFrame "INV". by iExists _. }
+    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _ _ _ _).
+    iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb') "[INV Hcloseβ]"; [done..|].
+    iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
+    iDestruct (bi.later_exist_2 with "mst") as ">mst".
+    set Q : () → vProp Σ := (λ _, (∃ st, rwown γs (main_st st)))%I.
+    set R : () → lit → vProp Σ := (λ _ _, (∃ st, rwown γs (main_st st)))%I.
+    iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
+                  _ #(Z_of_rwlock_st st2 - 1) () True%I Q R _ _ Vb'
+              with "[$PP $INV mst H◯ Hx' Hν H†]");
+      [solve_ndisj|by left|done|by left|by right|iSplitL ""; last iSplitL ""|..].
+    { iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
+    { iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
+    { simpl. iSplitR ""; last done.
+      iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
+      iDestruct "mst" as (st3) "mst". iIntros "_".
+      iDestruct 1 as (st2') "[Eqst INT]". iDestruct "Eqst" as %Eqst.
+      destruct st2' as [[[]|[[ν' q'] n]]|].
+
+
+    wp_read.
+    iMod ("Hcloseβ" with "[H↦ INV]") as "Hβ"; first by iExists _; iFrame.
+    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
+    iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+    iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
+    destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
+    + iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}▷=>
+               (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv 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_valid_discrete_2.
+        - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
+          intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
+                 %(inj Cinr)%(inj2 pair).
+          iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
+          rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
+          iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
+          iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
+            last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|];
+            [apply union_least; solve_ndisj|].
+          iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
+          iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
+          iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
+          rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+        - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
+          apply csum_included in Hle.
+          destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
+            [by subst|].
+          destruct Hle as [[Hag [q0 Hq]]%prod_included Hn%pos_included].
+          iDestruct "Hst" as (ν' q'') "(EQν & H†' & Hh & Hshr & Hq & Hν')".
+          iDestruct "EQν" as %EQν. revert Hag Hq. rewrite /= EQν to_agree_included.
+          intros <-%leibniz_equiv ->%leibniz_equiv.
+          iExists (Some (Cinr (to_agree ν, q0, Pos.pred n))).
+          iSplitL "Hlx"; first by destruct n.
+          replace (q ⋅ q0 + q'')%Qp with (q0 + (q + q''))%Qp by
+              by rewrite (comm _ q q0) assoc. iCombine "Hν" "Hν'" as "Hν".
+          iSplitL "H● H◯"; last by eauto with iFrame.
+          iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
+          assert (n = 1%positive ⋅ Pos.pred n) as EQn.
+          { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
+          rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
+          apply (cancel_local_update_unit (reading_st q ν)) , _. }
+      iApply (wp_step_fupd with "INV"). done. set_solver.
+      iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
+      iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
+      iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iModIntro. wp_if.
+      iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_singleton tctx_hasty_val //. }
+      iApply type_delete; [solve_typing..|].
+      iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply type_jump; solve_typing.
+    + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
+      iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
+      iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iModIntro. wp_if.
+      iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
+              with "[] LFT HE Hna HL Hk"); first last.
+      { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
+                tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
+      iApply type_jump; solve_typing.
+  Qed.
+End rwlockreadguard_functions.

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -23,7 +23,7 @@ Section rwlockwriteguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ γs β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
-             α ⊑ β ∗ rwown γs writing_st ∗ (∃ st, rwown γs (sub_st st)) ∗
+             α ⊑ β ∗ rwown γs writing_st ∗ rwown γs (sub_st (Some (inl ()))) ∗
              (∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
                     &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
          | _ => False

theories/typing/lib/rwlock/rwlockwriteguard_code.v

+From Coq.QArith Require Import Qcanon.
+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 rwlockwriteguard.
+From gpfsl.gps Require Import middleware.
+Set Default Proof Using "Type".
+
+Section rwlockwriteguard_functions.
+  Context `{typeG Σ, rwlockG Σ}.
+
+  (* Turning a rwlockwriteguard into a shared borrow. *)
+  Definition rwlockwriteguard_deref : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" +ₗ #1 in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
+    typed_val rwlockwriteguard_deref
+      (fn(∀ '(α, β), ∅; &shr{α}(rwlockwriteguard β ty)) → &shr{α} 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').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
+      [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+    rewrite heap_mapsto_vec_singleton.
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
+      [solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
+         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
+    iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
+    iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
+    iMod ("Hclose" with "[$] HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockwriteguard β ty));
+                              #(l' +ₗ 1) ◁ &shr{α}ty]
+            with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
+        by iApply lft_incl_refl. }
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Turning a rwlockwriteguard into a unique borrow. *)
+  Definition rwlockwriteguard_derefmut : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" +ₗ #1 in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; return: ["r"].
+
+  Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
+    typed_val rwlockwriteguard_derefmut
+      (fn(∀ '(α, β), ∅; &uniq{α}(rwlockwriteguard β 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').
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
+    iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
+    iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    destruct vl as [|[[|l|]|][]];
+      try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
+    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_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.
+    iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+    wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
+    wp_read. wp_op. wp_let. iMod "Hb".
+    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(l +ₗ 1) ◁ &uniq{α}ty]
+            with "[] LFT HE Hna HL Hk"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
+      by iApply lft_incl_trans. by iApply lft_incl_refl. }
+    iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* Drop a rwlockwriteguard and release the lock. *)
+  Definition rwlockwriteguard_drop : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      "x'" <-ʳᵉˡ #0;;
+      delete [ #1; "x"];;
+      let: "r" := new [ #0] in return: ["r"].
+
+  Lemma rwlockwriteguard_drop_type ty `{!TyWf ty} :
+    typed_val rwlockwriteguard_drop
+              (fn(∀ α, ∅; rwlockwriteguard α ty) → unit).
+  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 Hk HT".
+    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 (γs β) "(Hx' & #Hαβ & wst & Hsst & #Hinv)".
+    iDestruct "Hinv" as (γ tyO tyS) "((EqO & EqS & PP) & Hinv)".
+    iDestruct "PP" as (vP) "PP".
+    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' <-ʳᵉˡ #0)%E.
+    iMod (at_bor_acc with "LFT Hinv Hβ") as (Vb) "[INV Hcloseβ]"; [done..|].
+    iDestruct (rwlock_proto_inv_split with "INV") as "[H● INV]".
+    iDestruct "H●" as (st1) ">H●".
+    iDestruct (rwown_main_sub_agree with "H● Hsst") as %?. subst st1.
+    iMod (rwown_update_write_dealloc with "H● Hsst wst") as "(mst & sst)".
+    iAssert (▷ □ (∀ κ q' E', ⌜lftE ⊆ E'⌝ -∗ &{κ} tyO -∗
+                      (q').[κ] ={E'}=∗ (□ tyS κ) ∗ (q').[κ]))%I as "#Share".
+    { iIntros "!> !#" (κ???) "tyO tok".
+      iMod (ty_share with "LFT [tyO] tok") as "[#tyS $]" ;[done|..].
+      - iApply (bor_iff with "EqO tyO").
+      - iIntros "!> !#". by iApply "EqS". }
+    iApply (GPS_PPRaw_write (rwlock_interp γs β tyO tyS) _ _ _ #0 _ ()
+      with "[$PP $INV sst Hx']"); [done|solve_ndisj|by right|..].
+    { simpl. iNext. iIntros "_ !>".
+      iSplitL "sst Hx'"; iExists None; [|by iFrame "Share"].
+      iSplitL ""; [done|]. iFrame "sst". iApply (bor_iff with "[] Hx'").
+      iIntros "!> !#". by iApply (bi_iff_sym with "EqO"). }
+    iNext. iIntros "[PP' INV]".
+    iMod ("Hcloseβ" with "[INV mst]") as "Hβ".
+    { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+
+    iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
+    iMod ("Hclose" with "Hα HL") as "HL".
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
+            with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val //. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+End rwlockwriteguard_functions.