diff --git a/_CoqProject b/_CoqProject
index fa79b28ebeda86a8891de91f33faaa04af197296..be7647368063cef1afc9f4e946a7c6536a1151e2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,7 +15,7 @@ theories/lifetime/lifetime.v
 theories/lifetime/at_borrow.v
 theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
-theories/lifetime/gps.v
+theories/logic/gps.v
 theories/lang/notation.v
 theories/lang/memcpy.v
 theories/lang/new_delete.v
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index f4a10deca3c51a66b35192adc4588e1cfa518b73..c6c36d42f421d048e184ac40cc11efb774d05217 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -2,7 +2,8 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import notation.
 From gpfsl.gps Require Import middleware protocols.
-From lrust.lifetime Require Import gps at_borrow.
+From lrust.logic Require Import gps.
+From lrust.lifetime Require Import at_borrow.
 Set Default Proof Using "Type".
 
 Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
@@ -36,15 +37,10 @@ Section proof.
                  if pb then (if b then True else R) else True)%I.
 
   Definition lock_proto N l γ κ (R : vProp): vProp :=
-    (∃ R0, □ (R ↔ R0) ∗ ∃ t v, GPS_PP N (lock_interp R0) l κ t () v γ)%I.
+    (∃ R0, □ (R ↔ R0) ∗ ∃ t v, GPS_aPP N (lock_interp R0) l κ t () v γ)%I.
 
   Global Instance lock_proto_ne N l γ κ: NonExpansive (lock_proto N l γ κ).
-  Proof.
-    rewrite /lock_proto =>????. apply bi.exist_ne => ?.
-    apply bi.sep_ne; first solve_proper.
-    do 2 (apply bi.exist_ne => ?). apply bi.sep_ne; [done|].
-    apply at_bor_ne, GPS_PPInv_ne. solve_proper.
-  Qed.
+  Proof. solve_proper. Qed.
   Global Instance lock_proto_persistent N l γ κ R:
     Persistent (lock_proto N l γ κ R) := _.
 
@@ -53,7 +49,7 @@ Section proof.
   Proof.
     iIntros "#Hincl". iDestruct 1 as (R0) "[#Eq Hproto]".
     iDestruct "Hproto" as (t v) "Hproto".
-    iExists R0. iFrame "Eq". iExists t, v. by iApply GPS_PP_lft_mono.
+    iExists R0. iFrame "Eq". iExists t, v. by iApply GPS_aPP_lft_mono.
   Qed.
 
   Lemma lock_proto_iff N l γ κ R R' :
@@ -100,7 +96,7 @@ Section proof.
     { iIntros "!>". iDestruct 1 as (v) "[Hl >Eq]". iDestruct "Eq" as (b) "%".
        subst v. by iExists _. }
     { iDestruct "Hl" as (b) "Hl". iExists _. iFrame. by iExists _. }
-    iMod (GPS_PP_Init N (lock_interp R) l κ () q (λ v, ∃ b : bool, v = #b)
+    iMod (GPS_aPP_Init N (lock_interp R) l κ () q (λ v, ∃ b : bool, v = #b)
           with "LFT Htok HINV Hl [R] []") as "[$ Hproto]"; [done|done|..].
     { iIntros (t γ v [b ?]). subst v. iExists b. iSplit; [done|]. by destruct b. }
     { iIntros "!>" (??? v). iDestruct 1 as (b) "[>? ?]". by iExists _. }
@@ -121,7 +117,7 @@ Section proof.
     iDestruct "Hproto" as (R0) "[#Eq Hproto]".
     iDestruct "Hproto" as (t v) "PP".
     iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
-    iApply (GPS_PP_CAS_int_simple N (lock_interp R0) l κ q t () _
+    iApply (GPS_aPP_CAS_int_simple N (lock_interp R0) l κ q t () _
                 (Z_of_bool false) #true _ _ _ γ True%I (λ _ _, R0)%I
                 (λ t _, lock_interp R0 false l γ t () #false)
                 (λ _ _, R0)%I (λ _ _ _, True)%I
@@ -167,7 +163,7 @@ Section proof.
     iIntros "#LFT !#" (Φ) "(HR & #Hproto & Htok) HΦ". wp_let.
     iDestruct "Hproto" as (R0) "[#Eq Hproto]".
     iDestruct "Hproto" as (t v) "PP".
-    iApply (GPS_PP_Write N (lock_interp R0) l κ q _ t _ #(Z_of_bool false) _ ()
+    iApply (GPS_aPP_Write N (lock_interp R0) l κ q _ t _ #(Z_of_bool false) _ ()
               with "[$LFT $Htok $PP HR]"); [by move => []|done..|by right| |].
     { simpl. iIntros "!>" (t' Ext') "PP' !>". iExists false.
       iSplit; [done|by iApply "Eq"]. }
diff --git a/theories/lifetime/gps.v b/theories/logic/gps.v
similarity index 54%
rename from theories/lifetime/gps.v
rename to theories/logic/gps.v
index abb13c8d6c482834b5bf31fc1d191e4b72449a9d..6fa5917e9fa814e793e2731f7967195be2fd8c06 100644
--- a/theories/lifetime/gps.v
+++ b/theories/logic/gps.v
@@ -3,11 +3,11 @@ From lrust.lang Require Import notation.
 From lrust.lifetime Require Import at_borrow.
 From gpfsl.gps Require Import middleware.
 
-Section gps_at_bor_SW.
+Section gps_at_bor_SP.
 Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG view_Lat (↑histN) Σ} (N: namespace).
 Local Notation vProp := (vProp Σ).
 
-Implicit Types (IP : interpC Σ Prtcl) (l : loc)
+Implicit Types (IP : interpC Σ Prtcl) (IPC: interpCasC Σ Prtcl) (l : loc)
                (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
                (κ : lft) (γ : gname).
 
@@ -20,7 +20,89 @@ Definition GPS_aSP_SharedReader IP IPC l κ t s v q γ : vProp :=
 Definition GPS_aSP_SharedWriter IP IPC l κ t s v γ : vProp :=
   (GPS_SWSharedWriter l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
 
-End gps_at_bor_SW.
+Lemma GPS_aSP_Init IP IPC l κ s q P (Q: time → val → gname → vProp) E
+  (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+  ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
+  &{κ} (∃ v, l ↦ v ∗ ⌜P v⌝) -∗
+  (∀ t γ v, ⌜P v⌝ -∗ GPS_SWWriter l t s v γ -∗ ▷ IP true l γ t s v ∗ Q t v γ) -∗
+  (□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ⌜P v⌝) ={E}=∗
+  (q).[κ] ∗ ∃ γ t v, GPS_aSP_Reader IP IPC l κ t s v γ ∗ Q t v γ.
+Proof.
+  iIntros "#LFT Htok #HINV Hl HP #HP2".
+  iMod (bor_acc_cons with "LFT Hl Htok") as "[Hl Hclose]"; first done.
+  iDestruct "Hl" as (v) ">[Hl #P]".
+  set Q' : time → gname → vProp :=
+    (λ t γ, Q t v γ ∗ GPS_SWReader l t s v γ)%I.
+  iMod (GPS_SWRaw_Init_vs_strong IP l IPC true _ _ Q' with "Hl [HP]")
+    as (γ t) "[Inv [Q R]]".
+  { iIntros (t γ) "W". iDestruct (GPS_SWWriter_Reader with "W") as "#$".
+    by iApply ("HP" with "P W"). }
+  iMod ("Hclose" with "[] Inv") as "[Hl Htok]".
+  { iIntros "!> Inv".
+    iMod (GPS_INV_dealloc IP l IPC true with "HINV Inv")
+      as (t' s' v') "[Hl IP]"; [done|].
+    iMod ("HP2" with "IP") as "P'".
+    iIntros "!> !>". iExists _. by iFrame. }
+  iMod (bor_share N with "Hl") as "Hl"; [done|].
+  iFrame "Htok". iExists γ, t, v. by iFrame "∗".
+Qed.
+
+Lemma GPS_aSP_Read IP IPC l κ q R (o: memOrder) t s v γ tid E
+  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+  (RLX: o = Relaxed ∨ o = AcqRel) :
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Reader IP IPC l κ t s v γ
+      ∗ (▷ ∀ t' s' v', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
+           <obj> ((IP false l γ t' s' v' ={E ∖ ↑N}=∗
+                      IP false l γ t' s' v' ∗ R t' s' v') ∧
+                  (IP true l γ t' s' v' ={E ∖ ↑N}=∗
+                      IP true l γ t' s' v' ∗ R t' s' v') ∧
+                  (IPC l γ t' s' v' ={E ∖ ↑N}=∗
+                      IPC l γ t' s' v' ∗ R t' s' v'))) }}}
+    Read o #l in tid @ E
+  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝
+      ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ ∗ (q).[κ]
+      ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
+Proof.
+  iIntros (Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+  iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+  iApply (GPS_SWRaw_Read IP l IPC R o t s v γ tid Vb
+          with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
+  iNext. iIntros (t' s' v') "(Ext & Hlc' & Hproto & R)".
+  iMod ("Hclose1" with "Hproto") as "Htok".
+  iApply ("Post" $! t' s' v' with "[$Ext $Hlc' $Hshr $Htok $R]").
+Qed.
+
+Lemma GPS_aSP_SWWrite_rel IP IPC l κ q Q Q1 Q2 t s s' v v' γ tid E
+  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+  (Exts: s ⊑ s') :
+  let WVS: vProp :=
+  (∀ t', ⌜(t < t')%positive⌝ -∗ GPS_SWWriter l t' s' v' γ -∗ Q2
+              ={E ∖ ↑N}=∗ (<obj> (Q1 ={E ∖ ↑N}=∗ IPC l γ t s v)) ∗
+                     |={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
+      ∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
+    Write AcqRel #l v' in tid @ E
+  {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ
+      ∗ (q).[κ] ∗ Q t' }}}.
+Proof.
+  iIntros (VS Φ) "(#LFT & Htok & [W #Hshr] & VS) Post".
+  iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+  iApply (GPS_SWRaw_SWWrite_rel IP l IPC Q Q1 Q2 t s s' v v' γ tid Vb
+          with "[$W $Hproto $VS]"); [done|solve_ndisj|..].
+  iNext. iIntros (t') "(Ext & R' & Hproto & Q)".
+  iMod ("Hclose1" with "Hproto") as "Htok".
+  iApply ("Post" $! t' with "[$Ext $R' $Hshr $Htok $Q]").
+Qed.
+
+(*
+GPS_SWRaw_SharedWriter_CAS_int_weak
+GPS_SWRaw_SharedWriter_revert
+GPS_SWRaw_SharedWriter_CAS_int_strong
+GPS_SWSharedReaders_join
+GPS_SWWriter_shared
+*)
+
+End gps_at_bor_SP.
 
 Section gps_at_bor_PP.
 Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG view_Lat (↑histN) Σ}
@@ -31,23 +113,23 @@ Implicit Types (IP : interpC Σ Prtcl) (l : loc)
                (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
                (κ : lft) (γ : gname).
 
-Definition GPS_PP IP l κ t s v γ : vProp :=
+Definition GPS_aPP IP l κ t s v γ : vProp :=
   (GPS_PP_Local l t s v γ ∗ &at{κ, N} (GPS_PPInv IP l γ))%I.
 
-Global Instance GPS_PP_ne l κ t s v γ: NonExpansive (λ IP, GPS_PP IP l κ t s v γ).
+Global Instance GPS_aPP_ne l κ t s v γ: NonExpansive (λ IP, GPS_aPP IP l κ t s v γ).
 Proof. move => ????. apply bi.sep_ne; [done|]. by apply at_bor_ne, GPS_PPInv_ne. Qed.
-Global Instance GPS_PP_ne_persistent: Persistent (GPS_PP IP l κ t s v γ) := _.
+Global Instance GPS_aPP_ne_persistent: Persistent (GPS_aPP IP l κ t s v γ) := _.
 
-Lemma GPS_PP_lft_mono IP l κ κ' t s v γ :
-  κ' ⊑ κ -∗ GPS_PP IP l κ t s v γ -∗ GPS_PP IP l κ' t s v γ.
+Lemma GPS_aPP_lft_mono IP l κ κ' t s v γ :
+  κ' ⊑ κ -∗ GPS_aPP IP l κ t s v γ -∗ GPS_aPP IP l κ' t s v γ.
 Proof. iIntros "#Hincl". iDestruct 1 as "[$ Inv]". by iApply at_bor_shorten. Qed.
 
-Lemma GPS_PP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+Lemma GPS_aPP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
   ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
   &{κ} (∃ v, l ↦ v ∗ ⌜P v⌝) -∗
   (∀ t γ v, ⌜P v⌝ -∗ ▷ IP true l γ t s v) -∗
   (□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ⌜P v⌝) ={E}=∗
-  (q).[κ] ∗ ∃ γ t v, GPS_PP IP l κ t s v γ.
+  (q).[κ] ∗ ∃ γ t v, GPS_aPP IP l κ t s v γ.
 Proof.
   iIntros "#LFT Htok #HINV Hl HP #HP2".
   iMod (bor_acc_cons with "LFT Hl Htok") as "[Hl Hclose]"; first done.
@@ -64,21 +146,20 @@ Proof.
   iFrame "Htok". iExists γ, t, v. by iFrame "PP Hl".
 Qed.
 
-
-Lemma GPS_PP_Read IP l κ q R (o: memOrder) t s v γ tid E
-  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E):
-  o = Relaxed ∨ o = AcqRel →
-  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+Lemma GPS_aPP_Read IP l κ q R (o: memOrder) t s v γ tid E
+  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+  (RLX: o = Relaxed ∨ o = AcqRel) :
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
       ∗ (▷ ∀ t' s' v', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
              <obj> ((IP false l γ t' s' v' ={E ∖ ↑N}=∗
                         IP false l γ t' s' v' ∗ R t' s' v') ∧
                     (IP true l γ t' s' v' ={E ∖ ↑N}=∗
                         IP true l γ t' s' v' ∗ R t' s' v'))) }}}
     Read o #l in tid @ E
-  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗ GPS_PP IP l κ t' s' v' γ ∗ (q).[κ]
+  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗ GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ]
       ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
 Proof.
-  iIntros (RLX Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+  iIntros (Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
   iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
   iApply (GPS_PPRaw_Local_Read IP l R o t s v γ tid Vb
           with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
@@ -87,19 +168,19 @@ Proof.
   iApply ("Post" $! t' s' v' with "[$Ext $Hlc' $Hshr $Htok $R]").
 Qed.
 
-Lemma GPS_PP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
-  (FIN: model.final_st s')
-  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E):
-  o = Relaxed ∨ o = AcqRel →
+Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
+  (FIN: model.final_st s') (DISJ: histN ## N)
+  (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+  (RLX: o = Relaxed ∨ o = AcqRel) :
   let VS : vProp :=
     (∀ t' : time, ⌜(t < t')%positive⌝ -∗
           GPS_PP_Local l t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
-  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
       ∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
     Write o #l v' in tid @ E
-  {{{ t', RET #☠; GPS_PP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
+  {{{ t', RET #☠; GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
 Proof.
-  iIntros (RLX VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+  iIntros (VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
   iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
   iApply (GPS_PPRaw_Local_Write IP l o t v v' s s' γ Vb tid _ FIN
           with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
@@ -108,7 +189,7 @@ Proof.
   iApply ("Post" $! t' with "[$Hlc' $Hshr $Htok]").
 Qed.
 
-Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
+Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
   P Q Q1 Q2 R tid E
   (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E ∖ ↑N) (SUB3: ↑N ⊆ E)
   (ORF: orf = Relaxed ∨ orf = AcqRel)
@@ -129,7 +210,7 @@ Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
                     IP false l γ t' s' #v ∗ R t' s' v) ∧
                  (IP true l γ t' s' #v ={E ∖ ↑N}=∗
                     IP true l γ t' s' #v ∗ R t' s' v))))%I in
-  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
       ∗ ▷ VSC
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then P  else △{tid} P ) }}}
@@ -137,10 +218,10 @@ Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
   {{{ (b: bool) t' s' (v': lit), RET #b;
         (q).[κ] ∗ ⌜s ⊑ s'⌝
         ∗ ( (⌜b = true  ∧ v' = LitInt vr ∧ (t < t')%positive⌝
-              ∗ GPS_PP IP l κ t' s' vw γ
+              ∗ GPS_aPP IP l κ t' s' vw γ
               ∗ if decide (AcqRel ⊑ or)%stdpp then Q t' s' else ▽{tid} Q t' s')
           ∨ (⌜b = false ∧ lit_neq vr v' ∧ (t ≤ t')%positive⌝
-              ∗ GPS_PP IP l κ t' s' #v' γ
+              ∗ GPS_aPP IP l κ t' s' #v' γ
               ∗ (if decide (AcqRel ⊑ orf)%stdpp
                  then R t' s' v' else ▽{tid} (R t' s' v'))
               ∗ (if decide (AcqRel ⊑ ow)%stdpp
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 4aa1f9da21cc54af5d4d5e945035a60f59d3dde5..cb3ab63ca2298bd21a86a07db39bc7d7c9663464 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -5,6 +5,7 @@ From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
 From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 Definition rwlock_st := option (() + lft * frac * positive).
@@ -189,12 +190,13 @@ Section rwlock_inv.
   Definition rwlock_noCAS : interpCasC Σ unitProtocol :=
     (λ _ _ _ _ v, ⌜v = #(-1)⌝)%I.
 
-  Definition rwlock_proto_inv l γ γs α tyO tyS : vProp :=
-    GPS_INV (rwlock_interp γs α tyO tyS) l rwlock_noCAS γ.
-  Definition rwlock_proto_lc l γ (tyO: vProp) (tyS: lft → vProp) tid ty: vProp :=
+  Definition rwlock_proto' l γ γs κ (tyO: vProp) (tyS: lft → vProp): vProp :=
+    (∃ t v, GPS_aSP_Reader rwlockN (rwlock_interp γs κ tyO tyS)
+                           rwlock_noCAS l κ t () v γ)%I.
+  Definition rwlock_proto l γ γs κ tyO tyS tid ty: vProp :=
     ((▷ □ (tyO ↔ (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
      (▷ □ (∀ α, tyS α ↔ ty.(ty_shr) α tid (l +ₗ 1))) ∗
-      (∃ t v, GPS_SWReader l t () v γ))%I.
+      rwlock_proto' l γ γs κ tyO tyS)%I.
 
   Lemma rwlock_interp_comparable γs α tyO tyS l γ t s v (n: Z):
     rwlock_interp γs α tyO tyS true l γ t s v ∨
@@ -206,11 +208,11 @@ Section rwlock_inv.
       iExists _; iPureIntro ;(split; [done|by constructor]).
   Qed.
 
-  Global Instance rwlock_proto_lc_persistent:
-    Persistent (rwlock_proto_lc l γ tyO tyS tid ty) := _.
+  Global Instance rwlock_proto_persistent:
+    Persistent (rwlock_proto l γ γs κ tyO tyS tid ty) := _.
 
-  Global Instance rwlock_proto_lc_type_ne n l γ tyO tyS tid :
-    Proper (type_dist2 n ==> dist n) (rwlock_proto_lc l γ tyO tyS tid).
+  Global Instance rwlock_proto_type_ne n l γ γs κ tyO tyS tid :
+    Proper (type_dist2 n ==> dist n) (rwlock_proto l γ γs κ tyO tyS tid).
   Proof.
     move => ???.
     apply bi.sep_ne; [|apply bi.sep_ne]; [..|done];
@@ -222,16 +224,16 @@ Section rwlock_inv.
       apply bi.iff_ne; [done|apply ty_shr_type_dist]; [by apply type_dist2_S|done..].
   Qed.
 
-  Global Instance rwlock_proto_lc_ne l γ tyO tyS tid :
-    NonExpansive (rwlock_proto_lc l γ tyO tyS tid).
+  Global Instance rwlock_proto_ne l γ γs κ tyO tyS tid :
+    NonExpansive (rwlock_proto  l γ γs κ tyO tyS tid).
   Proof.
-    intros n ???. eapply rwlock_proto_lc_type_ne, type_dist_dist2. done.
+    intros n ???. by eapply rwlock_proto_type_ne, type_dist_dist2.
   Qed.
 
-  Lemma rwlock_proto_lc_proper E L ty1 ty2 q :
+  Lemma rwlock_proto_proper E L ty1 ty2 q :
     eqtype E L ty1 ty2 →
-    llctx_interp L q -∗ ∀ l γ tyO tyS tid, □ (elctx_interp E -∗
-    rwlock_proto_lc l γ tyO tyS tid ty1 -∗ rwlock_proto_lc l γ tyO tyS tid ty2).
+    llctx_interp L q -∗ ∀ l γ γs κ tyO tyS tid, □ (elctx_interp E -∗
+    rwlock_proto l γ γs κ tyO tyS tid ty1 -∗ rwlock_proto l γ γs κ tyO tyS tid ty2).
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
@@ -254,8 +256,7 @@ Section rwlock_inv.
     (q / 2).[α] -∗
     &{α} ((l +ₗ 1) ↦∗{1}: ty_own ty tid)%I -∗
     ▷ (∃ n : Z, l ↦{1} #n ∗ ⌜-1 ≤ n⌝) ={E}=∗
-    (q / 2).[α] ∗ (∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
-                             ∗ ▷ rwlock_proto_inv l γ γs α tyO tyS).
+    (q / 2).[α] ∗ (∃ γ γs tyO tyS, rwlock_proto l γ γs α tyO tyS tid ty).
   Proof.
     iIntros "#LFT Htok Hvl H".
     set tyO : vProp := ((l +ₗ 1) ↦∗{1}: ty.(ty_own) tid)%I.