finish rwlock, build with iris's fupd_step_wp branch and gpfsl's step_fupd branch

_CoqProject

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

theories/lang/lock.v

@@ -143,11 +143,11 @@ Section proof.
     { iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
       - iIntros (?? _). by iApply lock_interp_comparable.
       - by iIntros (??)"_ #$".
-      - iFrame "rTrue". iNext. rewrite /= -(bi.True_sep' (∀ _, _)%I).
+      - iFrame "rTrue". rewrite /= -(bi.True_sep' (∀ _, _)%I).
         iApply (rel_sep_objectively with "[$rTrue]").
-        iModIntro. iIntros ([] _). iSplit; [|by iIntros (?) "??"].
-        iIntros "_ F _". iModIntro. rewrite /lock_interp /=.
-        iExists (). iSplitL ""; [done|]. iDestruct "F" as (b) "[Eq R0]".
+        iModIntro. iIntros ([] _). iSplit; [|iNext; by iIntros (?) "??"].
+        iIntros "_ F _". iDestruct "F" as (b) "[>Eq R0]".
+        iModIntro. rewrite /lock_interp /=. iExists (). iSplitL ""; [done|].
         iDestruct "Eq" as %Eq. destruct b; [by inversion Eq|].
         iFrame "R0". iSplit; by iExists true. }
     iNext. iIntros (b v' s') "(inv & _ & CASE)"; simpl.

theories/typing/lib/rwlock/rwlock_code.v

@@ -206,31 +206,14 @@ Section rwlock_functions.
               (∃ qν ν, (qν).[ν] ∗
                  (□ tyS (β ⊓ ν)) ∗
                  rwown γs (reading_st qν ν) ∗
-                 ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+                 (□ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])) ∗
                ∃ n, GPS_SWSharedReader lx (() : unitProtocol) #n qν γ))%I.
       set R : () → lit → vProp Σ := (λ _ _, True)%I.
       set P : vProp Σ := (<obj> (qβ / 2).[β])%I.
-      set T : () → () → vProp Σ :=
-        (λ _ _, (qβ / 2).[β] ∗
-        □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
-        ∃ ν q' st2, (q').[ν] ∗
-          rwown γs (reading_st (q'/2) ν) ∗
-          rwown γs (st_global st2) ∗
-         □ tyS (β ⊓ ν) ∗
-         □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
-          (∃ n', GPS_SWSharedReader lx (() : unitProtocol) #n' q' γ) ∗
-          ( (∃ q, ⌜st2 = (Some (inr (ν, (q + q'/2)%Qp,
-                                    (Z.to_pos (Z_of_rwlock_st st') + 1)%positive)))
-                 ∧ 0 < Z_of_rwlock_st st'
-                 ∧ (q + q')%Qp = 1%Qp⌝ ∗
-              ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO))
-         ∨ (⌜st2 = (Some (inr (ν, (1 / 2)%Qp, 1%positive))) ∧ q' = 1%Qp
-                 ∧ 0 = Z_of_rwlock_st st'⌝ ∗
-              ([†β ⊓ ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO))))%I.
       iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
       iApply (GPS_SWSharedWriter_CAS_int (rwlock_interp γs β tyO tyS) _
                 rwlock_noCAS _ _ _ (Z_of_rwlock_st st') #(Z_of_rwlock_st st' + 1)
-                () _ _ P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
+                () _ _ P Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
         with "[$R' $INV Hβtok2 rTrue]");
         [done|solve_ndisj|by left|done|by right
         |by left|iSplitL ""; last iSplitL ""|..].
@@ -239,68 +222,51 @@ Section rwlock_functions.
       { simpl. iSplitL ""; last first.
         { rewrite -{2}(bi.True_sep' P).
           iApply (rel_sep_objectively with "[$rTrue Hβtok2]"). by iModIntro. }
-        iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+        rewrite -(bi.True_sep' (∀ _ : (), _)%I).
         iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
-        iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
-        iSplit.
+        iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"]. iSplit.
         { rewrite /rwlock_noCAS. iIntros "_" (Eq) "_".
           inversion Eq as [Eq1]. rewrite Eq1 in Hm1. exfalso. by apply Hm1. }
-        iSplitL "".
-        - iIntros "Hβtok2". iDestruct 1 as (st2) "[Eqst [g INT]]".
-          iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
-          iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
-          destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
-          + exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
-          + iDestruct 1 as (?) "[_ #Share]". iDestruct "INT" as "[W INT]".
-            iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & Rs)".
-            iDestruct "Hqq'" as %Hqq'.
-            iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
-            iModIntro. iExists (). iSplitL ""; [done|].
-            iSplitR "W"; last by rewrite Eqst2.
-            iFrame "Share Hβtok2". iExists ν, q', _. rewrite Eqst2.
-            iFrame "Hν g rst Hshr H† Rs". iLeft. iExists q. by iFrame "Hh".
-          + iDestruct 1 as (?) "[_ #Share]".
-            iDestruct "INT" as "(Hown & W & Rs)".
-            iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
-            iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
-            iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
-            iApply (fupd_mask_mono (↑lftN ∪ ↑histN)).
-            { apply union_subseteq; split; solve_ndisj. }
-            iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
-              [apply union_subseteq_l|iApply lft_intersect_incl_l|].
-            iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
-            iDestruct ("Hclose" with "Htok") as "[Hβtok2 Htok2]".
-            iCombine "Htok1" "Htok2" as "Htok".
-            iModIntro. iExists (). iSplitL ""; [done|].
-            iSplitR "W"; last by rewrite Eqst2.
-            iFrame "Share Hβtok2". iExists ν, 1%Qp, _. rewrite Eqst2.
-            iFrame "Htok g rst Hshr Hhν Rs". iRight. by iFrame "Hh".
-        - iIntros ([] _) "[Hβtok2 [#Share T]] W". iModIntro.
-          iDestruct "T" as (ν q' st2)
-            "([Htok1 Htok2] & rst & g & #Hshr & #H† & R & [T|T])".
-          + iDestruct "R" as (vR') "[R1 R2]".
-            iDestruct "T" as (q (? & Post' & Hqq')) "Hh". iFrame "Hβtok2".
-            have Eqst: Z_of_rwlock_st st'+1 = Z.pos (Z.to_pos (Z_of_rwlock_st st')+1).
-            { by rewrite -Pos2Z.add_pos_pos Z2Pos.id. }
-            iSplitL "Htok2 rst R1"; last iSplitR "".
-            * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
-            * iExists st2. subst st2. rewrite /= -Eqst. iSplitL ""; [done|].
-              iFrame "g W". iExists _. iFrame "H† Hh Hshr Htok1".
-              rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
-            * iExists st2. subst st2. rewrite /= -Eqst. by iFrame "Share".
-          + iDestruct "R" as (vR') "[R1 R2]".
-            iDestruct "T" as ((Post' & Eq' & Eqst)) "Hh". iFrame "Hβtok2".
-            subst q'. rewrite -Eqst /=. iSplitL "Htok2 rst R1"; last iSplitR "".
-            * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
-            * iExists st2. subst st2. simpl. iSplitL ""; [done|].
-              iFrame "g W". iExists _. iFrame "H† Hshr Htok1".
-              iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
-              rewrite Qp_div_2. iSplitL ""; [done|by iExists _].
-            * iExists st2. subst st2. rewrite /=. by iFrame "Share". }
+        iIntros "Hβtok2". iDestruct 1 as (st2) "[Eqst [g INT]]".
+        iDestruct 1 as (?) "[_ #Share]".
+        iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
+        iDestruct "Eqst" as ">Eqst". iDestruct "Eqst" as %Eqst.
+        inversion Eqst as [Eqst2]. clear Eqst.
+        iModIntro. iExists (). iSplitL ""; [done|].
+        destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
+        - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
+        - rewrite Eqst2. iDestruct "INT" as "[$ INT]". iIntros "W' !> !>".
+          iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & [Htok1 Htok2] & R)".
+          iDestruct "Hqq'" as %Hqq'. iDestruct "R" as (vR') "[R1 R2]".
+          iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
+          iModIntro. iSplitL "Htok2 rst R1 Hβtok2 H†".
+          + iFrame "Hβtok2". iExists _,_. iFrame "Htok2 Hshr rst H†". by iExists _.
+          + iSplitR ""; iExists (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive)));
+              [|by iFrame "Share"]. iSplitL ""; [done|]. iFrame "g W'".
+            iExists _. iFrame "H† Hh Hshr Htok1".
+            rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
+        - rewrite Eqst2. iDestruct "INT" as "(Hown & $ & R)". iIntros "W' !> !>".
+          iDestruct "R" as (vR') "[R1 R2]". 
+          iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #H†]". solve_ndisj.
+          iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
+          iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+          iApply (fupd_mask_mono (↑lftN ∪ ↑histN)).
+          { apply union_subseteq; split; solve_ndisj. }
+          iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
+            [apply union_subseteq_l|iApply lft_intersect_incl_l|].
+          iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
+          iDestruct ("Hclose" with "Htok") as "[Hβtok2 Htok2]".
+          iModIntro. iSplitL "Htok2 rst R1 Hβtok2".
+          + iFrame "Hβtok2". iExists _,_. iFrame "Htok2 Hshr rst H†". by iExists _.
+          + iSplitR ""; iExists (Some (inr (ν, (1 / 2)%Qp, 1%positive)));
+              [|by iFrame "Share"]. iSplitL ""; [done|]. iFrame "g W'".
+            iExists _. iFrame "H† Hshr Htok1".
+            iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+            rewrite Qp_div_2. iSplitL ""; [done|by iExists _]. }
 
       iNext. simpl.
-      iIntros (b v' []) "(INV & _ &[([%%] & R2 & Hβtok2 & Hβ) | ([% Neq] & R2 & _ & P)])".
-      + subst b v'. iDestruct "Hβ" as (q' ν) "(Hν & Hshr & Hreading & H† & R3)".
+      iIntros (b v' []) "(INV&_&[([%%]&_& Hβtok2 & Hβ) | ([% Neq] &_&_& P)])".
+      + subst b v'. iDestruct "Hβ" as (q' ν) "(Hν & Hshr & Hreading & #H† & R3)".
         iMod ("Hclose''" with "INV") as "Hβtok1".
         iModIntro. wp_case.
         iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -375,14 +341,9 @@ Section rwlock_functions.
          (∃ n' : lit, GPS_SWSharedReader lx (() : unitProtocol) #n' 1 γ))%I.
     set R : () → lit → vProp Σ := (λ _ _, True)%I.
     set P : vProp Σ := True%I.
-    set T : () → () → vProp Σ :=
-        (λ _ _, rwown γs (st_global None) ∗
-        □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
-        &{β} tyO ∗
-        (∃ n', GPS_SWSharedReader lx (() : unitProtocol) #n' 1 γ))%I.
     iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
     iApply (GPS_SWSharedWriter_CAS_int (rwlock_interp γs β tyO tyS) _
-                rwlock_noCAS _ _ _ 0 #(-1) () _ _ P T Q R _ Vb _ (⊤ ∖ ↑rwlockN)
+                rwlock_noCAS _ _ _ 0 #(-1) () _ _ P Q R _ Vb _ (⊤ ∖ ↑rwlockN)
                 with "[$R $INV rTrue]");
       [done|solve_ndisj|by left|done|by right|by left|iSplitL ""; last iSplitL ""|..].
     { iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
@@ -390,26 +351,23 @@ Section rwlock_functions.
     { simpl. iSplitL ""; last first.
       { rewrite -(bi.True_sep' P). iApply (rel_sep_objectively with "[$rTrue]").
         by iModIntro. }
-      iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+      rewrite -(bi.True_sep' (∀ _ : (), _)%I).
       iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
-      iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
+      iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"].
       iSplit. { rewrite /rwlock_noCAS. iIntros "_" (Eq) "_". by inversion Eq. }
-      iSplitL "".
-      - iIntros "_". iDestruct 1 as (st2) "[Eqst [g INT]]".
-        iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
-        destruct st2 as [[[]|[[]]]|]; simpl in Eqst2; [done|done|..].
-        iDestruct 1 as (?) "[_ #Share]". iExists (). iSplitL ""; [done|].
-        iDestruct "INT" as "(Hown & $ & R)". by iFrame "g Share Hown R".
-      - iIntros ([] _) "(g & #Share & Hown & R) W".
-        iMod (rwown_update_write with "g") as "[g wst]".
-        iModIntro. iSplitR "g"; last iSplitR "".
-        + by iFrame "Hown wst W R".
-        + iExists (Some (inl ())). by iFrame "g".
-        + iExists (Some (inl ())). by iFrame "Share". }
+      iIntros "_". iDestruct 1 as (st2) "[Eqst [g INT]]".
+      iDestruct 1 as (?) "[_ #Share]". iDestruct "Eqst" as ">Eqst".
+      iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
+      iExists (). iSplitL ""; [done|].
+      destruct st2 as [[[]|[[]]]|]; simpl in Eqst2; [done|done|..].
+      iDestruct "INT" as "(Hown & $ & R)". iIntros "!> W' !> !>".
+      iMod (rwown_update_write with "g") as "[g wst]". iModIntro.
+      iFrame "Hown wst W' R".
+      iSplitR""; iExists (Some (inl ())); [by iFrame "g"|by iFrame "Share"]. }
 
     iNext. simpl.
     iIntros (b v' [])
-            "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% Neq] & R' & _ & _)])".
+            "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% _] & _)])".
     - subst b v'.
       iDestruct "R'" as (?) "R'".
       iMod (GPS_SWSharedWriter_revert with "W R' INV") as "[W INV]".

theories/typing/lib/rwlock/rwlockreadguard.v

@@ -23,7 +23,7 @@ Section rwlockreadguard.
          | [ #(LitLoc l) ] =>
            ∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ q.[ν] ∗ rwown γs (reading_st q ν) ∗
-             (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+             □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
              (∃ γ tyO tyS, (∃ n, GPS_SWSharedReader l () #n q γ) ∗
                   rwlock_proto_lc l γ tyO tyS tid ty ∗
                   &at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))

theories/typing/lib/rwlock/rwlockreadguard_code.v

@@ -73,8 +73,8 @@ Section rwlockreadguard_functions.
     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) "(R & (EqO & EqS & _) & #Hinv)".
+    iDestruct "Hx'" as (ν q γs β) "(#Hx' & #Hαβ & Hν & H◯ & #H† & Hinv)".
+    iDestruct "Hinv" as (γ tyO tyS) "(R & (#EqO & #EqS & _) & #Hinv)".
     iDestruct "R" as (vR) "R".
     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.
@@ -93,60 +93,46 @@ Section rwlockreadguard_functions.
     set P : vProp Σ := (rwown γs (reading_st q ν) ∗ (q).[ν])%I.
     set Q : () → vProp Σ := (λ _, True)%I.
     set R : () → lit → vProp Σ := (λ _ _, True)%I.
-    set T : () → () → vProp Σ :=
-      (λ _ _, (q).[ν] ∗
-      □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
-      rwown γs (reading_st q ν) ∗
-      ∃ q' n,
-       ⌜Z_of_rwlock_st st2 = Z.pos n ∧
-        (q' = q ∧ n = 1%positive ∨
-          (∃ q0 : Qp, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝ ∗
-       rwown γs (st_global (Some (inr (ν,q',n)))) ∗
-       (∃ qr, □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
-          ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO) ∗
-          □ tyS (β ⊓ ν)  ∗
-          ⌜(q' + qr)%Qp = 1%Qp⌝ ∗
-          (qr).[ν] ∗
-          (∃ n', GPS_SWSharedReader lx' ((): unitProtocol) #n' qr γ)))%I.
     iApply (GPS_SWSharedWriter_CAS_int_strong (rwlock_interp γs β tyO tyS) _
               rwlock_noCAS _ _ _ _ #(Z_of_rwlock_st st2 - 1) () _ _ _
-              P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
-              with "[$R $INV H◯ Hν]");
-      [done|solve_ndisj|by left|done|by left|by right|iSplitL ""; last iSplitL ""|..].
+              P Q R _ Vb' _ ∅ with "[$R $INV H◯ Hν]");
+      [solve_ndisj|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 "H◯ Hν"; last iFrame "∗".
-      iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"]. iSplitL "".
-      - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [H● INT]]".
-        iDestruct "Eqst" as %Eqst.
-        iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
-        subst st2'. simpl in Eqst. iDestruct 1 as (?) "[_ #Share]". iModIntro.
-        iExists (). rewrite Eqst /=. iSplitL ""; [done|].
-        iDestruct "INT" as "[$ INT]". rewrite /T. iFrame "Hν Share H◯".
-        iExists _,_. iFrame "H●". iSplitL""; [by inversion Eqst|]. iFrame "INT".
-      - iIntros ([] _) "(Hν & #Share & H◯ & T) W R". iSplitL ""; [done|].
-        iDestruct "T" as (q' n [Eqst Eq']) "[H● T]".
-        iDestruct "T" as (qr) "(#H† & Hh & #Hshr & Hqrq' & Hqr & Rm)".
-        iDestruct "Hqrq'" as %Hqrq'.
-        iDestruct "Rm" as (?) "Rm".
+      iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"].
+      iIntros "(H◯ & Hν) INT". iDestruct 1 as (?) "[_ #Share]".
+      iDestruct "INT" as (st2') "[>Eqst [>H● INT]]". iDestruct "Eqst" as %Eqst.
+      iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
+      subst st2'. simpl in Eqst. iExists (). rewrite Eqst /=. iSplitL ""; [done|].
+      iDestruct "INT" as "[$ INT]".
+      iDestruct "INT" as (qr) "(_ & Hh & #Hshr & >Hqrq' & >Hqr & Rm)".
+      iDestruct "Hqrq'" as %Hqrq'. iCombine "Hν" "Hqr" as "Hν".
+      destruct CASE as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
+      - rewrite Hqrq'. iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●".
+        iIntros "!> W R".
+        iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ _ (↑histN));
+          [solve_ndisj|apply union_least; solve_ndisj|..].
+        iMod ("H†" with "Hν") as "Hν". iIntros "!> !>". iMod "Hν".
+        iMod ("Hh" with "Hν") as "Hb". iModIntro.
+        inversion Eqst as [Eqst1]. rewrite Eqst1 /=. iSplitL""; [done|].
+        iSplitR ""; iExists None; [|by iFrame "Share"]. iSplitL ""; [done|].
+        iFrame "H● Hb W". iDestruct "Rm" as (?) "Rm".
         iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
-        iCombine "Hν" "Hqr" as "Hν".
-        destruct Eq' as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
-        + rewrite Hqrq'.
-          iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●". iModIntro.
-          rewrite Eqst /=. iSplitR ""; iExists None; [|by iFrame "Share"].
-          iSplitL ""; [done|]. iFrame "H● W". iSplitR "R"; [|by iExists _].
-          admit.
-          (* iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
-          iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame. *)
-        + rewrite Eqn Qp_plus_comm Eqst.
-          iMod (rwown_update_read_dealloc with "H● H◯") as "H●". iModIntro.
-          have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
-          { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
-          iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
-          iSplitL ""; [done|]. iFrame "H● W".
-          iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν". iSplitR "R"; [|by iExists _].
-          by rewrite Qp_plus_assoc (Qp_plus_comm q0). }
+        rewrite Hqrq'. by iExists _.
+      - inversion Eqst as [Eqst1]. rewrite Eqn Qp_plus_comm Eqst1.
+        iMod (rwown_update_read_dealloc with "H● H◯") as "H●".
+        iIntros "!> W R". iApply step_fupd_intro; [solve_ndisj|].
+        iIntros "!>". iSplitL ""; [done|].
+        have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
+        { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
+        iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
+        iSplitL ""; [done|]. iFrame "H● W".
+        iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν".
+        iSplitR "R Rm"; [by rewrite Qp_plus_assoc (Qp_plus_comm q0)|].
+        iDestruct "Rm" as (?) "Rm".
+        iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R". by iExists _. }
 
     iNext. iIntros (b v' []) "(INV & _ & CASE)".
     iDestruct "CASE" as "[[[% %] _]|[[% NE] [R' [_ [H◯ Hν]]]]]".
@@ -170,5 +156,5 @@ Section rwlockreadguard_functions.
         iExists _,_,_. iSplitL "R'"; [by iExists _|]. iFrame "EqO EqS Hinv".
         iExists _. by iFrame "RR". }
       iApply type_jump; solve_typing.
-  Admitted.
+  Qed.
 End rwlockreadguard_functions.