diff --git a/_CoqProject b/_CoqProject
index 057a066767d41b490c1f88420619414efdfbf56c..c03b2e2b60c556cb12f90154d5edf63677a55baa 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..8387ee2b15f036b048d76fb1248f4b40cdb260e3
--- /dev/null
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -0,0 +1,314 @@
+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.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
new file mode 100644
index 0000000000000000000000000000000000000000..adbce4bcc86b875a8d21ccf15b3cee55873557e6
--- /dev/null
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -0,0 +1,133 @@
+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.