From e7e16b65c42f1eb5cb09076e154d13810a1a5a0a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 25 Feb 2017 23:13:09 +0100
Subject: [PATCH] Proove that RWlock is safe.
FIXME : we need to be able to end a lifetime when an invariant is still open.
---
_CoqProject | 6 +
theories/typing/unsafe/rwlock/rwlock.v | 194 +++++++++++
theories/typing/unsafe/rwlock/rwlock_code.v | 313 ++++++++++++++++++
.../typing/unsafe/rwlock/rwlockreadguard.v | 112 +++++++
.../unsafe/rwlock/rwlockreadguard_code.v | 148 +++++++++
.../typing/unsafe/rwlock/rwlockwriteguard.v | 129 ++++++++
.../unsafe/rwlock/rwlockwriteguard_code.v | 146 ++++++++
7 files changed, 1048 insertions(+)
create mode 100644 theories/typing/unsafe/rwlock/rwlock.v
create mode 100644 theories/typing/unsafe/rwlock/rwlock_code.v
create mode 100644 theories/typing/unsafe/rwlock/rwlockreadguard.v
create mode 100644 theories/typing/unsafe/rwlock/rwlockreadguard_code.v
create mode 100644 theories/typing/unsafe/rwlock/rwlockwriteguard.v
create mode 100644 theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
diff --git a/_CoqProject b/_CoqProject
index 07bbce45..093c42e1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -54,6 +54,12 @@ theories/typing/unsafe/refcell/refmut.v
theories/typing/unsafe/refcell/refcell_code.v
theories/typing/unsafe/refcell/ref_code.v
theories/typing/unsafe/refcell/refmut_code.v
+theories/typing/unsafe/rwlock/rwlock.v
+theories/typing/unsafe/rwlock/rwlockreadguard.v
+theories/typing/unsafe/rwlock/rwlockwriteguard.v
+theories/typing/unsafe/rwlock/rwlock_code.v
+theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
new file mode 100644
index 00000000..dc70a67c
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -0,0 +1,194 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import shr_borrow.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Definition rwlock_stR :=
+ optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
+Class rwlockG Σ :=
+ RwLockG :> inG Σ (authR rwlock_stR).
+Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
+Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
+Proof. solve_inG. Qed.
+
+Definition Z_of_rwlock_st (st : rwlock_stR) : Z :=
+ match st with
+ | None => 0
+ | Some (Cinr (_, _, n)) => Zpos n
+ | Some _ => -1
+ end.
+
+Definition reading_st (q : frac) (ν : lft) : rwlock_stR :=
+ Some (Cinr (to_agree ν, q, xH)).
+Definition writing_st : rwlock_stR :=
+ Some (Cinl (Excl ())).
+
+Definition rwlockN := lrustN .@ "rwlock".
+
+Section rwlock_inv.
+ Context `{typeG Σ, rwlockG Σ}.
+
+ Definition rwlock_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
+ (∃ st, l ↦ #(Z_of_rwlock_st st) ∗ own γ (◠st) ∗
+ match st return _ with
+ | None =>
+ (* Not locked. *)
+ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+ | Some (Cinr (agν, q, n)) =>
+ (* Locked for read. *)
+ ∃ (ν : lft) q', agν ≡ to_agree ν ∗
+ □ (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ [†ν]) ∗
+ ([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+ ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
+ | _ => (* Locked for write. *) True
+ end)%I.
+
+ Global Instance rwlock_inv_ne n tid l γ α :
+ Proper (dist n ==> dist n) (rwlock_inv tid l γ α).
+ Proof.
+ intros ty1 ty2 Hty. unfold rwlock_inv.
+ repeat (f_contractive || f_equiv || apply Hty || apply dist_S).
+ Qed.
+
+ Lemma rwlock_inv_proper E L tid l γ α ty1 ty2 :
+ eqtype E L ty1 ty2 →
+ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
+ rwlock_inv tid l γ α ty1 -∗ rwlock_inv tid l γ α ty2.
+ Proof.
+ (* TODO : this proof is essentially [solve_proper], but within the logic.
+ It would easily gain from some automation. *)
+ iIntros (Hty%eqtype_unfold) "#HE #HL H". unfold rwlock_inv.
+ iDestruct (Hty with "HE HL") as "(% & Hown & Hshr)".
+ iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
+ &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
+ { iIntros "!# H". iApply bor_iff; last done.
+ iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+ iFrame; by iApply "Hown". }
+ iDestruct "H" as (st) "H"; iExists st;
+ iDestruct "H" as "($&$&H)"; destruct st as [[|[[agν ?]?]|]|]; try done;
+ last by iApply "Hb".
+ iDestruct "H" as (ν q') "(Hag & #Hend & Hh & ? & ? & ?)". iExists ν, q'.
+ iFrame. iSplitR. done. iSplitL "Hh"; last by iApply "Hshr".
+ iIntros "Hν". iApply "Hb". iApply ("Hh" with "Hν").
+ Qed.
+End rwlock_inv.
+
+Section rwlock.
+ Context `{typeG Σ, rwlockG Σ}.
+
+ (* Original Rust type (we ignore poisoning):
+ pub struct RwLock<T: ?Sized> {
+ inner: Box<sys::RWLock>,
+ poison: poison::Flag,
+ data: UnsafeCell<T>,
+ }
+ *)
+
+ Program Definition rwlock (ty : type) :=
+ {| ty_size := S ty.(ty_size);
+ ty_own tid vl :=
+ match vl return _ with
+ | #(LitInt z) :: vl' => ⌜-1 ≤ z⌠∗ ty.(ty_own) tid vl'
+ | _ => False
+ end%I;
+ ty_shr κ tid l := (∃ α γ, κ ⊑ α ∗ &shr{α,rwlockN}(rwlock_inv tid l γ α ty))%I |}.
+ Next Obligation.
+ iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
+ iIntros "[_ %] !% /=". congruence.
+ Qed.
+ Next Obligation.
+ iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+ iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
+ iDestruct "H" as "[>% Hown]".
+ iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ nâŒ) ∗
+ shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[-] []")%I as "[H [Htok Htok']]".
+ { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+ iSplitL "Hn"; [eauto|iExists _; iFrame]. }
+ { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
+ iDestruct "Hvl" as (vl') "[H↦ Hvl]".
+ iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. 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]"
+ as "[$ HQ]"; last first.
+ { iMod ("Hclose" with "HQ []") as "[Hb $]".
+ - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
+ iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
+ - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
+ iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.
+ solve_ndisj. }
+ clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
+ - iFrame. iMod (own_alloc (◠None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ iMod (own_alloc (◠Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
+ { by apply auth_auth_valid. }
+ iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+ iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
+ iDestruct ("Hclose" with "Htok") as "[$ Htok]".
+ iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Hshr}".
+ iSplitR; first by auto. iFrame "Htok2". iSplitR; first done.
+ rewrite Qp_div_2. iSplitL; last by auto.
+ iIntros "!> !> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
+ - iMod (own_alloc (◠writing_st)) as (γ) "Hst". { by apply auth_auth_valid. }
+ iFrame. iExists _, _. eauto with iFrame.
+ Qed.
+ Next Obligation.
+ iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
+ iExists _, _. iFrame. iApply lft_incl_trans; auto.
+ Qed.
+
+ Global Instance rwlock_ne n : Proper (dist n ==> dist n) rwlock.
+ Proof.
+ move=>ty1 ty2 Hty. constructor; simpl.
+ - f_equiv. apply Hty.
+ - intros tid vl. destruct n as [|n]=>//=. repeat f_equiv. apply Hty.
+ - intros κ tid l. by repeat f_equiv.
+ Qed.
+
+ Global Instance rwlock_mono E L : Proper (eqtype E L ==> subtype E L) rwlock.
+ Proof.
+ (* TODO : this proof is essentially [solve_proper], but within the logic.
+ It would easily gain from some automation. *)
+ iIntros (ty1 ty2 EQ) "#HE #HL". pose proof EQ as EQ'%eqtype_unfold.
+ iDestruct (EQ' with "HE HL") as "(% & #Hown & #Hshr)".
+ iSplit; [|iSplit; iIntros "!# * H"].
+ - iPureIntro. simpl. congruence.
+ - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
+ - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
+ iApply shr_bor_iff; last done.
+ iSplit; iIntros "!>!# H"; by iApply rwlock_inv_proper.
+ Qed.
+ Lemma rwlock_mono' E L ty1 ty2 :
+ eqtype E L ty1 ty2 → subtype E L (rwlock ty1) (rwlock ty2).
+ Proof. eapply rwlock_mono. Qed.
+ Global Instance rwlock_proper E L : Proper (eqtype E L ==> eqtype E L) rwlock.
+ Proof. by split; apply rwlock_mono. Qed.
+ Lemma rwlock_proper' E L ty1 ty2 :
+ eqtype E L ty1 ty2 → eqtype E L (rwlock ty1) (rwlock ty2).
+ Proof. eapply rwlock_proper. Qed.
+
+ (* TODO : apparently, we don't need to require ty to be sync,
+ contrarily to Rust's implementation. *)
+ Global Instance rwlock_send :
+ Send ty → Send (rwlock ty).
+ Proof. move=>????[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
+
+ Global Instance rwlock_sync :
+ Send ty → Sync ty → Sync (rwlock ty).
+ Proof.
+ move=>???????/=. do 2 apply uPred.exist_mono=>?. apply uPred.sep_mono_r.
+ iApply shr_bor_iff. iIntros "!> !#". iApply uPred.equiv_iff.
+ apply uPred.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+ - do 5 f_equiv. apply uPred.equiv_spec; split; iApply send_change_tid.
+ - apply uPred.equiv_spec; split; iApply sync_change_tid.
+ - apply uPred.equiv_spec; split; iApply send_change_tid.
+ Qed.
+End rwlock.
+
+Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/unsafe/rwlock/rwlock_code.v
new file mode 100644
index 00000000..620554eb
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlock_code.v
@@ -0,0 +1,313 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lang Require Import memcpy.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing option.
+From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
+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 :
+ typed_instruction_ty [] [] [] (rwlock_new ty)
+ (fn (λ _, []) (λ _, [# ty]) (λ _:(), rwlock ty)).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_new; [solve_typing..|].
+ iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+ rewrite (Nat2Z.id (S ty.(ty_size))) 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 (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (rwlock ty)]%TC
+ with "[] LFT Hna HE 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. 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 :
+ typed_instruction_ty [] [] [] (rwlock_into_inner ty)
+ (fn (λ _, []) (λ _, [# rwlock ty]) (λ _:(), ty)).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_new; [solve_typing..|].
+ iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+ rewrite (Nat2Z.id (ty.(ty_size))) 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]"; 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]%TC
+ with "[] LFT Hna HE 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 :
+ typed_instruction_ty [] [] [] rwlock_get_mut
+ (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (rwlock ty)])%T (λ α, &uniq{α} ty)%T).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
+ iIntros (x'). simpl_subst.
+ iIntros (tid qE) "#LFT Hna HE 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 (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ zâŒ) ∗
+ (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with ">[Hx']" as "[_ Hx']".
+ { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
+ - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
+ iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
+ - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try iDestruct "H" as "[]".
+ rewrite heap_mapsto_vec_cons.
+ 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); #(shift_loc lx' 1) ◠&uniq{α}ty]%TC
+ with "[] LFT Hna HE 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..|exact: write_own|].
+ 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
+ ("loop" []
+ cont: "loop" [] :=
+ let: "n" := !ˢᶜ"x'" in
+ if: "n" ≤ #-1 then
+ "r" <-{Σ 0} ();;
+ "k" ["r"]
+ else
+ if: CAS "x'" "n" ("n" + #1) then
+ "r" <-{Σ 1} "x'";;
+ "k" ["r"]
+ else "loop" [])
+ cont: "k" ["r"] :=
+ delete [ #1; "x"];; "return" ["r"].
+
+ Lemma rwlock_try_read_type ty :
+ typed_instruction_ty [] [] [] rwlock_try_read
+ (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
+ (λ α, option (rwlockreadguard α ty))%T).
+ Proof.
+ 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 (rwlockreadguard α ty))])%TC);
+ [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..|apply read_own_copy, _|done|].
+ iIntros (x'). simpl_subst.
+ iApply (type_cont [] [] (λ _, [x ◠_; x' ◠_; r ◠_])%TC);
+ [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
+ simpl_subst.
+ { iApply (type_jump []); solve_typing. }
+ iIntros (tid qE) "#LFT Hna HE 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]".
+ rewrite {1}/elctx_interp big_sepL_singleton.
+ iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
+ wp_bind (!ˢᶜ(LitV lx))%E.
+ iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
+ iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
+ iMod ("Hclose'" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
+ iModIntro. wp_let. wp_op=>Hm1; wp_if.
+ - iApply (type_type _ _ _
+ [ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2) ]%TC
+ with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+ iApply (type_sum_assign_unit [unit; rwlockreadguard α ty]);
+ [solve_typing..|by eapply write_own|]; first last.
+ simpl. iApply (type_jump [_]); solve_typing.
+ - wp_op. wp_bind (CAS _ _ _).
+ iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try 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"); first done. iNext. iIntros "Hlx".
+ iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
+ ty_shr ty (β ∪ ν) tid (shift_loc 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.
+ - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. 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_glb_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_le_incl. apply gmultiset_union_subseteq_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. iSplitR; first done. iSplitL; last done.
+ iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+ iMod ("Hclose'" with "[$INV]") as "Hβtok1".
+ iApply (wp_if _ true). iIntros "!>!>".
+ iMod ("Hclose" with "[$Hβtok1 $Hβtok2]") as "HE".
+ iApply (type_type _ _ _
+ [ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2);
+ #lx ◠rwlockreadguard α ty]%TC
+ with "[] LFT Hna >[HE] 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_glb_mono; first done. iApply lft_incl_refl. }
+ { rewrite {1}/elctx_interp big_sepL_singleton //. }
+ iApply (type_sum_assign [unit; rwlockreadguard α ty]);
+ [solve_typing..|by eapply write_own|].
+ 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. iApply (wp_if _ false). iNext.
+ iMod ("Hclose" with "[$Hβtok1 $Hβtok2]") as "HE".
+ iSpecialize ("Hk" with "[HE] []").
+ { by rewrite {1}/elctx_interp big_sepL_singleton. } 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"] :=
+ let: "r" := new [ #2 ] in
+ let: "x'" := !"x" in
+ if: CAS "x'" #0 #(-1) then
+ "r" <-{Σ 1} "x'";;
+ "k" ["r"]
+ else
+ "r" <-{Σ 0} ();;
+ "k" ["r"]
+ cont: "k" ["r"] :=
+ delete [ #1; "x"];; "return" ["r"].
+
+ Lemma rwlock_try_write_type ty :
+ typed_instruction_ty [] [] [] rwlock_try_write
+ (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
+ (λ α, option (rwlockwriteguard α ty))%T).
+ Proof.
+ 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))])%TC);
+ [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..|apply read_own_copy, _|done|].
+ iIntros (x' tid qE) "#LFT Hna HE 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]".
+ rewrite {1}/elctx_interp big_sepL_singleton.
+ iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
+ wp_bind (CAS _ _ _).
+ iMod (shr_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"). done. by destruct c as [|[[]]|].
+ iNext. iIntros "Hlx".
+ iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+ iModIntro. iApply (wp_if _ false). iNext.
+ iApply (type_type _ _ _
+ [ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2) ]%TC
+ with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+ iApply (type_sum_assign_unit [unit; rwlockwriteguard α ty]);
+ [solve_typing..|by eapply write_own|]; first last.
+ rewrite /option /=. iApply (type_jump [_]); solve_typing.
+ - iApply (wp_cas_int_suc with "Hlx"). done. 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. iApply (wp_if _ true). iNext. iMod ("Hclose" with "Hβtok") as "HE".
+ iApply (type_type _ _ _
+ [ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2);
+ #lx ◠rwlockwriteguard α ty]%TC
+ with "[] LFT Hna >[HE] HL Hk"); first last.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. iFrame. iExists _, _. iFrame "∗#". }
+ { rewrite {1}/elctx_interp big_sepL_singleton //. }
+ iApply (type_sum_assign [unit; rwlockwriteguard α ty]);
+ [solve_typing..|by eapply write_own|].
+ simpl. iApply (type_jump [_]); solve_typing.
+ Qed.
+End rwlock_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/unsafe/rwlock/rwlockreadguard.v
new file mode 100644
index 00000000..d35d40f8
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard.v
@@ -0,0 +1,112 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.rwlock Require Import rwlock.
+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 γ β, ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+ q.[ν] ∗ own γ (◯ reading_st q ν) ∗
+ (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ [†ν])
+ | _ => False
+ end;
+ ty_shr κ tid l :=
+ ∃ (l' : loc),
+ &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+ ▷ ty.(ty_shr) (α ∪ κ) tid (shift_loc 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_tok 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 (γ) "Hb". done.
+ iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
+ iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
+ iMod (bor_persistent_tok with "LFT Hshr Htok") as "[#Hshr Htok]". done.
+ iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
+ iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
+ iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
+ iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". 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. by rewrite Qp_mult_1_r. }
+ iExists _. iFrame "#". iApply ty_shr_mono; last done.
+ iApply lft_glb_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_glb_mono; last done.
+ iApply lft_incl_refl.
+ Qed.
+
+ Global Instance rwlockreadguard_contractive α : Contractive (rwlockreadguard α).
+ Proof.
+ intros n ?? EQ. unfold rwlockreadguard. constructor=>//=.
+ - intros tid vl. destruct n as [|n]=>//=. by repeat f_equiv.
+ - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
+ Qed.
+ Global Instance rwlockreadguard_ne n α : Proper (dist n ==> dist n) (rwlockreadguard α).
+ Proof. apply 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) "#HE #HL".
+ iDestruct (proj1 Hty with "HE HL") as "(%&#Ho&#Hs)".
+ iDestruct (Hα with "HE HL") as "Hα1α2".
+ iSplit; [|iSplit; iAlways].
+ - done.
+ - iIntros (tid [|[[]|][]]) "H"; try done.
+ iDestruct "H" as (ν q γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
+ iExists ν, q, γ, β. iFrame "∗#". iSplit; last iSplit.
+ + iApply ty_shr_mono; last by iApply "Hs".
+ iApply lft_glb_mono. done. iApply lft_incl_refl.
+ + by iApply lft_incl_trans.
+ + iApply (shr_bor_iff with "[] Hinv").
+ iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
+ - iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
+ iFrame. iApply ty_shr_mono; last by iApply "Hs".
+ iApply lft_glb_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.
+End rwlockreadguard.
+
+Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
new file mode 100644
index 00000000..becd1f18
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
@@ -0,0 +1,148 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import lifetime na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard.
+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 :
+ typed_instruction_ty [] [] [] rwlockreadguard_deref
+ (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
+ (fun '(α, β) => [# &shr{α}(rwlockreadguard β ty)]%T)
+ (fun '(α, β) => &shr{α}ty)%T).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+ iIntros (tid qE) "#LFT Hna HE 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]".
+ rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
+ iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
+ 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α".
+ iApply (type_type _ _ _ [ x ◠box (uninit 1); #(shift_loc l' 1) ◠&shr{α}ty]%TC
+ with "[] LFT Hna [Hα Hβ Hαβ] 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. done.
+ iApply lft_incl_refl. }
+ { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+ 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
+ ("loop" []
+ cont: "loop" [] :=
+ let: "n" := !ˢᶜ"x'" in
+ if: CAS "x'" "n" ("n" - #1) then
+ delete [ #1; "x"];;
+ let: "r" := new [ #0] in "return" ["r"]
+ else "loop" []).
+
+ Lemma rwlockreadguard_drop_type ty :
+ typed_instruction_ty [] [] [] rwlockreadguard_drop
+ (fn(∀ α, [☀α]; rwlockreadguard α ty) → unit).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+ iIntros (x'). simpl_subst.
+ iApply (type_cont [] [] (λ _, [x ◠_; x' ◠_])%TC);
+ [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
+ simpl_subst.
+ { iApply (type_jump []); solve_typing. }
+ iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
+ rewrite {1}/elctx_interp big_sepL_singleton 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†)".
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ wp_bind (!ˢᶜ#lx')%E.
+ iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+ iDestruct "INV" as (st) "[H↦ INV]". wp_read.
+ iMod ("Hcloseβ" with "[H↦ INV]") as "Hβ"; first by iExists _; iFrame.
+ iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
+ iMod (shr_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 %->.
+ (* FIXME : here, I REALLY need to end a lifetime while an
+ invariant is still open. *)
+ iAssert (|={⊤,⊤ ∖ ↑lftN}▷=> lx' ↦ #0 ==∗ rwlock_inv tid lx' γ β ty)%I
+ with "[-]" as "?"; last admit.
+ iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
+ iApply fupd_mask_mono; last iMod ("Hh" with "H†") as "Hb". done.
+ 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_empty, _.
+ - 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_empty (reading_st q ν)) , _. }
+ iApply (wp_fupd_step 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 "HE". iApply (wp_if _ true). iIntros "!>!>".
+ iApply (type_type _ _ _ [ x â— box (uninit 1)]%TC
+ with "[] LFT Hna [HE] HL Hk"); first last.
+ { rewrite tctx_interp_singleton tctx_hasty_val //. }
+ { rewrite /elctx_interp big_sepL_singleton //. }
+ 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 "HE". iApply (wp_if _ false). iIntros "!> !>".
+ iApply (type_type _ _ _ [ x ◠box (uninit 1); #lx' ◠rwlockreadguard α ty]%TC
+ with "[] LFT Hna [HE] HL Hk"); first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
+ tctx_hasty_val' //. iFrame. iExists _, _, _, _. iFrame "∗#". }
+ { rewrite /elctx_interp big_sepL_singleton //. }
+ iApply (type_jump []); solve_typing.
+ Admitted.
+End rwlockreadguard_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
new file mode 100644
index 00000000..15ad051c
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
@@ -0,0 +1,129 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.rwlock Require Import rwlock.
+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) ] =>
+ ∃ γ β, &{β}(shift_loc l 1 ↦∗: ty.(ty_own) tid) ∗
+ α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+ own γ (◯ writing_st)
+ | _ => False
+ end;
+ ty_shr κ tid l :=
+ ∃ (l' : loc),
+ &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ∪ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
+ ty.(ty_shr) (α ∪ κ) tid (shift_loc 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_tok 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_sep with "LFT Hb") as "[Hb H]". done.
+ iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
+ iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+ iExists _. iFrame "H↦". rewrite {1}bor_unfold_idx.
+ iDestruct "Hb" as (i) "[#Hpb Hpbown]".
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid (shift_loc l' 1))%I
+ with "[Hpbown]") as "#Hinv"; first by eauto.
+ iIntros "!> !# * % Htok". clear HE.
+ iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+ iDestruct "INV" as "[>Hbtok|#Hshr]".
+ - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
+ { iApply bor_unfold_idx. eauto. }
+ iModIntro. iNext. iMod "Hb".
+ iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
+ { iApply (bor_shorten with "[] Hb"). iApply lft_glb_mono. done.
+ iApply lft_incl_refl. }
+ iMod ("Hclose" with "[]") as "_"; auto.
+ - iMod ("Hclose" with "[]") as "_". by eauto.
+ iApply step_fupd_intro. set_solver. auto.
+ 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]". set_solver.
+ { iApply lft_glb_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_glb_mono. iApply lft_incl_refl. done.
+ Qed.
+
+ Global Instance rwlockwriteguard_contractive α : Contractive (rwlockwriteguard α).
+ Proof.
+ intros n ?? EQ. unfold rwlockwriteguard. constructor=>//=.
+ - intros tid vl. destruct n as [|n]=>//=.
+ do 9 f_equiv. solve_contractive. by repeat f_equiv.
+ - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
+ Qed.
+ Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
+ Proof. apply contractive_ne, _. Qed.
+
+ Global Instance rwlockwriteguard_mono E L :
+ Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockwriteguard.
+ Proof.
+ iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
+ pose proof Hty as Hty'%eqtype_unfold.
+ iDestruct (Hty' with "HE HL") as "(%&#Ho&#Hs)".
+ iDestruct (Hα with "HE HL") as "Hα1α2".
+ iSplit; [|iSplit; iAlways].
+ - done.
+ - iIntros (tid [|[[]|][]]) "H"; try done.
+ iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
+ iExists γ, β. iFrame "∗#". iSplit; last iSplit.
+ + iApply bor_iff; last done.
+ iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+ iExists vl; iFrame; by iApply "Ho".
+ + by iApply lft_incl_trans.
+ + iApply shr_bor_iff; try done.
+ iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
+ - 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]". set_solver.
+ { iApply lft_glb_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_glb_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.
+End rwlockwriteguard.
+
+Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
new file mode 100644
index 00000000..fd7c6436
--- /dev/null
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
@@ -0,0 +1,146 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.rwlock Require Import rwlock rwlockwriteguard.
+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 :
+ typed_instruction_ty [] [] [] rwlockwriteguard_deref
+ (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
+ (fun '(α, β) => [# &shr{α}(rwlockwriteguard β ty)]%T)
+ (fun '(α, β) => &shr{α}ty)%T).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+ iIntros (tid qE) "#LFT Hna HE 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]".
+ rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
+ iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ rewrite heap_mapsto_vec_singleton.
+ iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+ wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step 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".
+ iApply (type_type _ _ _ [ x ◠box (uninit 1); #(shift_loc l' 1) ◠&shr{α}ty]%TC
+ with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] 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.
+ iApply lft_incl_refl. }
+ { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+ 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 :
+ typed_instruction_ty [] [] [] rwlockwriteguard_derefmut
+ (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
+ (fun '(α, β) => [# &uniq{α}(rwlockwriteguard β ty)]%T)
+ (fun '(α, β) => &uniq{α}ty)%T).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+ iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iDestruct "HT" as "[Hx Hx']".
+ rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
+ iDestruct "HE" as "(Hα & Hβ & #Hαβ)". 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.
+ destruct vl as [|[[|l|]|][]];
+ try by iMod (bor_persistent_tok 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_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
+ iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+ wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hb]");
+ [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
+ wp_read. iIntros "Hb !>". wp_op. wp_let.
+ iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
+ iApply (type_type _ _ _ [ x ◠box (uninit 1); #(shift_loc l 1) ◠&uniq{α}ty]%TC
+ with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+ iFrame. iApply (bor_shorten with "[] Hb").
+ by iApply lft_incl_glb; [iApply lft_incl_trans|iApply lft_incl_refl]. }
+ { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+ 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 :
+ typed_instruction_ty [] [] [] rwlockwriteguard_drop
+ (fn(∀ α, [☀α]; rwlockwriteguard α ty) → unit).
+ Proof.
+ iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ inv_vec arg=>x. simpl_subst.
+ iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+ iIntros (x'). simpl_subst.
+ iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
+ rewrite {1}/elctx_interp big_sepL_singleton 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◯)".
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ wp_bind (#lx' <-ˢᶜ #0)%E.
+ iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+ iDestruct "INV" as (st) "(H↦ & H◠& INV)". wp_write.
+ iMod ("Hcloseβ" with ">[H↦ H◠H◯ INV Hx']") as "Hβ".
+ { iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> &
+ [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2;
+ last by destruct (exclusive_included _ _ Hle).
+ destruct st0 as [[[]|]| |]; try by inversion Heq.
+ iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
+ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
+ apply cancel_local_update_empty, _. }
+ iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "HE".
+ iApply (type_type _ _ _ [ x â— box (uninit 1)]%TC
+ with "[] LFT Hna [HE] HL Hk"); first last.
+ { rewrite tctx_interp_singleton tctx_hasty_val //. }
+ { rewrite /elctx_interp big_sepL_singleton //. }
+ iApply type_delete; [solve_typing..|].
+ iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply (type_jump [_]); solve_typing.
+ Qed.
+End rwlockwriteguard_functions.
--
GitLab