diff --git a/_CoqProject b/_CoqProject
index efc7417bbd939698809ab8f625944231452cc529..fa79b28ebeda86a8891de91f33faaa04af197296 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,6 +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/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 52065d8e1a37e78441076b287db0e4667af60788..f4a10deca3c51a66b35192adc4588e1cfa518b73 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -2,7 +2,7 @@ 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.
 Set Default Proof Using "Type".
 
 Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
@@ -26,7 +26,7 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{noprolG Σ, lockG Σ}.
+  Context `{noprolG Σ, !lftG view_Lat (↑histN) Σ, lockG Σ}.
 
   Implicit Types (l : loc).
   Local Notation vProp := (vProp Σ).
@@ -35,33 +35,42 @@ Section proof.
     (λ pb _ _ _ _ v, ∃ b : bool, ⌜v = #b⌝ ∗
                  if pb then (if b then True else R) else True)%I.
 
-  Definition lock_proto_inv l γ (R0 : vProp): vProp :=
-    (GPS_PPInv (lock_interp R0) l γ)%I.
-
-  Definition lock_proto_lc l γ (R0 R : vProp): vProp :=
-    (□ (R ↔ R0) ∗ ∃ t v, GPS_PP_Local l t () v γ)%I.
+  Definition lock_proto N l γ κ (R : vProp): vProp :=
+    (∃ R0, □ (R ↔ R0) ∗ ∃ t v, GPS_PP N (lock_interp R0) l κ t () v γ)%I.
 
-  Global Instance lock_proto_inv_ne l γ: NonExpansive (lock_proto_inv l γ).
-  Proof. rewrite /lock_proto_inv =>????. apply GPS_PPInv_ne. solve_proper. Qed.
-  Global Instance lock_proto_lc_ne l γ R: NonExpansive (lock_proto_lc l γ R).
-  Proof. rewrite /lock_proto_lc =>????. solve_proper. Qed.
+  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.
+  Global Instance lock_proto_persistent N l γ κ R:
+    Persistent (lock_proto N l γ κ R) := _.
 
-  Global Instance lock_proto_lc_persistent: Persistent (lock_proto_lc l γ R0 R) := _.
+  Lemma lock_proto_lft_mono N l γ κ κ' R:
+    κ' ⊑ κ -∗ lock_proto N l γ κ R -∗ lock_proto N l γ κ' R.
+  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.
+  Qed.
 
-  Lemma lock_proto_lc_iff l γ R0 R R' :
-    □ (R ↔ R') -∗ lock_proto_lc l γ R0 R -∗ lock_proto_lc l γ R0 R'.
+  Lemma lock_proto_iff N l γ κ R R' :
+    □ (R ↔ R') -∗ lock_proto N l γ κ R -∗ lock_proto N l γ κ R'.
   Proof.
-    iIntros "#Eq1". iDestruct 1 as "[#Eq2 $]".
+    iIntros "#Eq1". iDestruct 1 as (R0) "[#Eq2 PP]".
+    iExists R0. iFrame "PP".
     iIntros "!#". iSplit; iIntros "?".
     - iApply "Eq2". by iApply "Eq1".
     - iApply "Eq1". by iApply "Eq2".
   Qed.
 
-  Lemma lock_proto_lc_iff_proper l γ R0 R R' :
-    □ (R ↔ R') -∗ □ (lock_proto_lc l γ R0 R ↔ lock_proto_lc l γ R0 R').
+  Lemma lock_proto_iff_proper N l γ κ R R' :
+    □ (R ↔ R') -∗ □ (lock_proto N l γ κ R ↔ lock_proto N l γ κ R').
   Proof.
     iIntros "#HR !#".
-    iSplit; iIntros "Hlck"; iApply (lock_proto_lc_iff with "[HR] Hlck"); [done|].
+    iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck"); [done|].
     iAlways; iSplit; iIntros; by iApply "HR".
   Qed.
 
@@ -78,69 +87,46 @@ Section proof.
   Proof. iDestruct (1) as (b') "[#Eq _]". iExists b'. iFrame "Eq". Qed.
 
   (** The main proofs. *)
-  Lemma lock_proto_create (R : vProp) l (b bl : bool) :
-    l ↦ #b -∗ (if b then True else ▷?bl R) ==∗
-      ∃ γ, lock_proto_lc l γ R R ∗ ▷?bl lock_proto_inv l γ R.
-  Proof.
-    iIntros "Hl R".
-    iMod (GPS_PPRaw_Init_vs (lock_interp R) _ bl _ () with "Hl [R]")
-      as (γ t) "[lc inv]".
-    { iIntros (??). rewrite /lock_interp. iExists b.
-      iSplit; [done|by destruct b]. }
-    iExists γ. iFrame "inv". iSplitR "lc"; [|by iExists _, _].
-    iIntros "!> !#". by iApply (bi.iff_refl True%I).
-  Qed.
-
-  Lemma lock_proto_destroy bl l jγ R E (SUB: ↑histN ⊆ E) :
-    ⎡ hist_inv ⎤ -∗ ▷?bl lock_proto_inv l jγ R
-    ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷?bl R.
-  Proof.
-    iIntros "#hInv inv".
-    iMod (GPS_PPInv_dealloc with "hInv inv") as (t s v) "[Hl F]"; [done|].
-    iDestruct "F" as (b) "[>% R]". subst v. iExists b. iFrame "Hl". by destruct b.
-  Qed.
-
-  Lemma mklock_unlocked_spec b l R tid E :
-    ↑histN ⊆ E →
-    {{{ l ↦ ? ∗ ▷?b R }}}
-      mklock_unlocked [ #l ] in tid @ E
-    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷?b lock_proto_inv l γ R }}}.
-  Proof.
-    iIntros (? Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
-    iMod (lock_proto_create R _ false b with "Hl [$HR]") as (γ) "?".
-    by iApply "HΦ".
-  Qed.
-
-  Lemma mklock_locked_spec b l R tid E :
-    ↑histN ⊆ E →
-    {{{ l ↦ ? }}}
-      mklock_locked [ #l ] in tid @ E
-    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷?b lock_proto_inv l γ R }}}.
+  Lemma lock_proto_create N l q κ (R : vProp) E
+    (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+    ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
+    &{κ}(∃ b: bool, l ↦ #b) -∗ ▷ R ={E}=∗
+      (q).[κ] ∗ ∃ γ, lock_proto N l γ κ R.
   Proof.
-    iIntros (? Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
-    iMod (lock_proto_create R _ true with "Hl [//]") as (γ) "?".
-    by iApply "HΦ".
+    iIntros "#LFT Htok #HINV Hl R".
+    iMod (bor_acc_cons with "LFT Hl Htok") as "[Hl Hclose]"; first done.
+    iMod ("Hclose" $! (∃ v, l ↦ v ∗ ⌜∃ b: bool, v = #b⌝)%I with "[] [Hl]")
+      as "[Hl Htok]".
+    { 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)
+          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 _. }
+    iDestruct "Hproto" as (γ t v) "Hproto".
+    iModIntro. iExists γ, R. iSplit; [|by iExists _, _].
+    iIntros "!#". by iApply (bi.iff_refl True%I).
   Qed.
 
   (* At this point, it'd be really nice to have some sugar for symmetric
      accessors. *)
-  Lemma try_acquire_spec l (R P: vProp) tid E1 E2 :
-    ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
-                  ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
-                  ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
-    {{{ P }}} try_acquire [ #l ] in tid @ E2
-    {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
+  Lemma try_acquire_spec N l γ κ R q tid E
+    (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
+    ⎡ lft_ctx ⎤ -∗
+    {{{ lock_proto N l γ κ R ∗ (q).[κ] }}} try_acquire [ #l ] in tid @ E
+    {{{ b, RET #b; (if b is true then R else True) ∗ (q).[κ] }}}.
   Proof.
-    iIntros (??) "#Hproto !# * HP HΦ".
-    wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
-    iDestruct "lc" as (t ?) "lc".
+    iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". wp_rec.
+    iDestruct "Hproto" as (R0) "[#Eq Hproto]".
+    iDestruct "Hproto" as (t v) "PP".
     iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
-    iApply (GPS_PPRaw_Local_CAS_int_simple (lock_interp R0) _ _ _ _ _
-                (Z_of_bool false) #true t () True%I (λ _ _, R0)%I
+    iApply (GPS_PP_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
-        with "[$lc $inv]");[done|by left|by right|by left|..].
+      with "[$LFT $PP $Htok]");
+      [done|done|solve_ndisj|done|by left|by right|by left|..].
     { iSplitL ""; [iNext; iModIntro..|].
       - iIntros (??? _). by iApply lock_interp_comparable.
       - simpl. iFrame "rTrue". rewrite /= -(bi.True_sep' (∀ _, _)%I).
@@ -152,42 +138,41 @@ Section proof.
         iIntros "_ R0". iExists (). iSplitL ""; [done|].
         iIntros "!>" (t'' Ext'') "PP' !>". iSplitL ""; [by iIntros "!> $"|].
         iIntros "!> !> !>". iFrame "R0". by iExists true. }
-    iNext. iIntros (b t' v' s') "(inv & _ & CASE)"; simpl.
-    iMod ("Hclose" with "inv") as "P".
-    iModIntro. iApply "HΦ". iFrame "P".
+    iNext. iIntros (b t' v' s') "(Htok & _ & CASE)"; simpl.
+    iApply ("HΦ" $! b with "[- $Htok]").
     iDestruct "CASE" as "[[[% _] [_ ?]]|[[% _]_]]"; subst b; [by iApply "Eq"|done].
   Qed.
 
-  Lemma acquire_spec l (R P: vProp) tid E1 E2 :
-    ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
-                  ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
-                  ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
-    {{{ P }}} acquire [ #l ] in tid @ E2 {{{ RET #☠; R ∗ P }}}.
+  Lemma acquire_spec N l γ κ R q tid E
+    (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
+    ⎡ lft_ctx ⎤ -∗
+    {{{ lock_proto N l γ κ R ∗ (q).[κ] }}}
+      acquire [ #l ] in tid @ E
+    {{{ RET #☠; R ∗ (q).[κ] }}}.
   Proof.
-    iIntros (??) "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "Hproto HP"); [done..|by etrans|].
+    iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "LFT [$Hproto $Htok]"); [done..|by etrans|].
     iIntros ([]).
-    - iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
-    - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
+    - iIntros "[HR Htok]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "[_ Htok]". wp_if. iApply ("IH" with "Htok HΦ").
   Qed.
 
-  Lemma release_spec l (R P: vProp) tid E1 E2 :
-    ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
-                  ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
-                  ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
-    {{{ R ∗ P }}} release [ #l ] in tid @ E2 {{{ RET #☠; P }}}.
+  Lemma release_spec N l γ κ R q tid E
+    (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
+    ⎡ lft_ctx ⎤ -∗
+    {{{ R ∗ lock_proto N l γ κ R ∗ (q).[κ] }}}
+      release [ #l ] in tid @ E
+    {{{ RET #☠; (q).[κ] }}}.
   Proof.
-    iIntros (??) "#Hproto !# * (HR & HP) HΦ". wp_let.
-    iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
-    iDestruct "lc" as (t v) "lc".
-    iApply (GPS_PPRaw_Local_Write (lock_interp R0) _ _ t _ #(Z_of_bool false)
-              _ () with "[$lc $inv HR]"); [by move => []|done|by right|..].
+    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) _ ()
+              with "[$LFT $Htok $PP HR]"); [by move => []|done..|by right| |].
     { simpl. iIntros "!>" (t' Ext') "PP' !>". iExists false.
       iSplit; [done|by iApply "Eq"]. }
-    iIntros "!>" (t') "[? inv]". iMod ("Hclose" with "inv"). by iApply "HΦ".
+    iIntros "!>" (t') "[PP' Htok]". by iApply "HΦ".
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto_inv lock_proto_lc.
+Typeclasses Opaque lock_proto.
diff --git a/theories/lifetime/gps.v b/theories/lifetime/gps.v
index a5cad5f57c1bb46ee603f30132ac3293c948af8b..56509b807432efa631720eff8626dd04e26d70ba 100644
--- a/theories/lifetime/gps.v
+++ b/theories/lifetime/gps.v
@@ -13,27 +13,34 @@ Implicit Types (IP : interpC Σ Prtcl) (l : loc)
                (κ : lft) (γ : gname).
 
 Definition GPS_PP IP l κ t s v γ : vProp :=
-  (GPS_PPRaw l t s v γ ∗ &at{κ, N} (GPS_PPInv IP l γ))%I.
+  (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 γ).
 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 γ) := _.
 
-Lemma GPS_PP_Init IP l κ s q E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
-  ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗
-  &{κ} (⎡ hist_inv ⎤ ∗ ∃ v, l ↦ v) -∗ (∀ t γ v, IP true l γ t s v)
-  ={E}=∗ (q).[κ] ∗ ∃ γ t v, GPS_PP 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 γ.
+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):
+  ⎡ 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 γ.
 Proof.
-  iIntros "#LFT Htok Hl HP".
-  iMod (bor_acc_cons with "LFT Hl Htok") as "[[#HINV Hl] Hclose]"; first done.
-  iDestruct "Hl" as (v) ">Hl".
+  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]".
   iMod (GPS_PPRaw_Init_vs IP l true with "Hl [HP]") as (γ t) "[PP Inv]".
-  { iIntros (t γ) "!>". by iApply "HP". }
+  { iIntros (t γ). by iApply "HP". }
   iMod ("Hclose" with "[] Inv") as "[Hl Htok]".
   { iIntros "!> Inv".
     iMod (GPS_PPInv_dealloc IP l true with "HINV Inv")
-      as (t' s' v') "[Hl _]"; [done|].
-    iFrame "HINV". iIntros "!> !>". by iExists _. }
+      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 "PP Hl".
 Qed.
@@ -42,8 +49,9 @@ 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 →
-  let VS : vProp := (∀ t' : time, ⌜(t < t')%positive⌝ -∗
-                      GPS_PP IP l κ t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
+  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 γ
       ∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
     Write o #l v' in tid @ E
@@ -51,10 +59,59 @@ Lemma GPS_PP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
 Proof.
   iIntros (RLX VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
   iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
-  iApply (GPS_PPRaw_write IP l o t v v' s s' γ Vb tid _ FIN
-          with "[$Hlc $Hproto VS]"); [solve_ndisj|done|..].
-  { iNext. case_decide.
-    - iIntros (t' Ext') "PP". iApply ("VS" $! t' Ext' with "[$PP $Hshr]").
-Abort.
+  iApply (GPS_PPRaw_Local_Write IP l o t v v' s s' γ Vb tid _ FIN
+          with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
+  iNext. iIntros (t') "[Hlc' Hproto]".
+  iMod ("Hclose1" with "Hproto") as "Htok".
+  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 γ
+  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)
+  (OR: or = Relaxed ∨ or = AcqRel) (OW: ow = Relaxed ∨ ow = AcqRel):
+  let VSC : vProp :=
+    (<obj> ∀ t' s' v', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
+                  (IP true l γ t' s' v' ∨ IP false l γ t' s' v') -∗
+                  ⌜∃ vl, v' = #vl ∧ lit_comparable vr vl⌝)%I in
+  let VS : vProp :=
+    (∀ t' s', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
+      ((<obj> (▷ IP true l γ t' s' #vr ={E ∖ ↑N}=∗ ▷ Q1 t' s' ∗ ▷ Q2 t' s')) ∗
+       (P -∗ ▷ Q2 t' s' ={E ∖ ↑N}=∗ ∃ s'', ⌜s' ⊑ s''⌝ ∗
+          (∀ t , ⌜(t' < t)%positive⌝ -∗ ▷ (GPS_PP_Local l t s'' vw γ) ={E ∖ ↑N}=∗
+              (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
+              |={E ∖ ↑N}▷=> Q t s'' ∗ IP true l γ t s'' vw)) ) ∧
+      (▷ ∀ (v: lit), ⌜lit_neq vr v⌝ -∗
+          <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))))%I in
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP 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 ) }}}
+    CAS #l #vr vw orf or ow in tid @ E
+  {{{ (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 γ
+              ∗ 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' γ
+              ∗ (if decide (AcqRel ⊑ orf)%stdpp
+                 then R t' s' v' else ▽{tid} (R t' s' v'))
+              ∗ (if decide (AcqRel ⊑ ow)%stdpp
+                 then P  else △{tid} P ))) }}}.
+Proof.
+  iIntros (VSC VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VSC & VS & P) Post".
+  iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+  iApply (GPS_PPRaw_Local_CAS_int_simple IP l orf or ow v vr vw t s P Q Q1 Q2 R
+            γ tid Vb with "[$Hlc $Hproto $VSC $VS $P]"); [done..|].
+  iIntros "!>" (b t' s' v') "(Hproto & Ext & CASE)".
+  iMod ("Hclose1" with "Hproto") as "Htok".
+  iApply ("Post" $! b t' s' v' with "[$Htok $Ext CASE]").
+  iDestruct "CASE" as "[?|?]"; [iLeft|iRight]; by iFrame "Hshr".
+Qed.
 
 End gps_at_bor.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index e84610d0be9a9ebc2cce77f790fc77955b33907b..64a0971483e72d5e8b8088a49ad49f1abcb18a44 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -31,8 +31,7 @@ Section mutex.
                          ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
                        | _ => False end;
        ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
-        ∃ γ R, lock_proto_lc l γ R (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid))
-                ∗ &at{κ, mutexN} (lock_proto_inv l γ R)
+        ∃ γ, lock_proto mutexN l γ κ (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid))
     |}%I.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[? []]". rewrite ty_size_eq.
@@ -54,24 +53,17 @@ Section mutex.
     { iNext. iSplitL "Hl"; first by eauto.
       iExists vl. iFrame. }
     clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
-    iMod (bor_acc_cons with "LFT Hl Htok") as "[>Hl Hclose]"; first done.
-    iDestruct "Hl" as (b) "Hl".
-    iMod (lock_proto_create _ _ _ false with "Hl [Hbor]") as (γ) "[Hlc Hproto]".
-    { destruct b; [done|by iExact "Hbor"]. }
-    iMod ("Hclose" with "[] Hproto") as "[Hl Htok]".
-    { clear b. iIntros "!> Hproto". simpl.
-      iMod (lock_proto_destroy true with "hInv Hproto") as (b) "[Hl _]"; [done|].
-      iExists _. by iFrame. }
-    iFrame "Htok". iExists κ.
-    iMod (bor_share mutexN with "Hl") as "Hl"; [solve_ndisj..|].
-    iSplitL ""; [iApply lft_incl_refl|]. iExists γ, _. by iFrame.
+    iMod (lock_proto_create mutexN l q κ (&{κ}((l +ₗ 1) ↦∗: ty.(ty_own) tid))%I
+            with "LFT Htok hInv Hl [Hbor]")
+       as "[$ Hproto]"; [solve_ndisj|done..|].
+    iExists κ. iFrame "Hproto ". by iApply lft_incl_refl.
   Qed.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H".
     iDestruct "H" as (κ'') "(#Hlft & #Hlck)".
-    iDestruct "Hlck" as (γ R) "[Hlc Hproto]".
+    iDestruct "Hlck" as (γ) "Hproto".
     iExists _. iSplit; [by iApply lft_incl_trans|].
-    iExists _, _. iFrame "Hlc". by iApply at_bor_shorten.
+    iExists γ. by iApply lock_proto_lft_mono.
   Qed.
 
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
@@ -99,9 +91,9 @@ Section mutex.
     - iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
       simpl. iDestruct "Hvl" as "[$ [$ Hvl]]". by iApply "Howni".
     - iIntros "!# * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
-      iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ R) "[Hlc Hbor]".
-      iExists γ, R. iFrame "Hbor".
-      iApply lock_proto_lc_iff_proper; [|iFrame].
+      iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
+      iExists γ.
+      iApply lock_proto_iff_proper; [|iFrame].
       iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
       iNext. iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
   Qed.
@@ -121,9 +113,8 @@ Section mutex.
     Send ty → Sync (mutex ty).
   Proof.
     iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
-    iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ R) "[Hlc Hbor]".
-    iExists γ, R. iFrame "Hbor".
-    iApply lock_proto_lc_iff_proper; [|iFrame].
+    iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
+    iExists γ. iApply lock_proto_iff_proper; [|iFrame].
     iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
     iNext. iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index ba0694ce458b93158314d50cc3f32a60b95fe71e..8e2e99a858bafad4987595ace5a82d2715e99e8d 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -32,8 +32,7 @@ Section mguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ β, α ⊑ β ∗
-             (∃ γ R, lock_proto_lc l γ R (&{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid))
-              ∗ &at{α, mutexN} (lock_proto_inv l γ R))
+             (∃ γ, lock_proto mutexN l γ α (&{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid)))
              ∗ &{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid)
          | _ => False end;
        ty_shr κ tid l :=
@@ -95,14 +94,11 @@ Section mguard.
       iDestruct "H" as (β) "(#H⊑ & Hinv & Hown)".
       iExists β. iFrame. iSplit; last iSplit.
       + by iApply lft_incl_trans.
-      + iDestruct "Hinv" as (γ R) "[Hlc Hinv]".
-        iExists γ, R. iSplitL "Hlc".
-        * iApply lock_proto_lc_iff_proper; [|iFrame].
-          iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
-          iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
-        * iApply (at_bor_shorten with "Hα").
-          iApply (at_bor_iff with "[] Hinv"). iIntros "!> !#".
-          by iApply (bi.iff_refl True%I).
+      + iDestruct "Hinv" as (γ) "Hproto".
+        iExists γ. iApply (lock_proto_lft_mono with "Hα").
+        iApply lock_proto_iff_proper; [|iFrame].
+        iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
+        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
       + iApply bor_iff; last done. iIntros "!>".
         iApply heap_mapsto_pred_iff_proper.
         iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
@@ -135,27 +131,6 @@ End mguard.
 Section code.
   Context `{!typeG Σ, !lockG Σ}.
 
-  Lemma mutex_acc E l ty tid q α κ :
-    ↑histN ⊆ E → ↑lftN ⊆ E → ↑mutexN ⊆ E →
-    let R := (&{κ}((l +ₗ 1) ↦∗: ty_own ty tid))%I in
-    ⎡ lft_ctx ⎤ -∗
-    (∃ γ R0, lock_proto_lc l γ R0 R
-              ∗ &at{α, mutexN} (lock_proto_inv l γ R0))%I -∗
-    α ⊑ κ -∗
-    □ ((q).[α] ={E,↑histN}=∗
-            ∃ γ R0 Vb, lock_proto_lc l γ R0 R
-                  ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
-                  ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={↑histN,E}=∗ (q).[α]))%I.
-  Proof.
-    iIntros (??? R) "#LFT #Hshr #Hlincl !# Htok".
-    iDestruct "Hshr" as (γ R0) "[Hlc Hshr]". iExists γ, R0.
-    iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
-    iExists Vb. iFrame "Hlc Hproto".
-    iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
-    iIntros "Hproto". iMod "Hclose2" as "_".
-    iMod ("Hclose1" with "Hproto") as "$". done.
-  Qed.
-
   Definition mutex_lock : val :=
     funrec: <> ["mutex"] :=
       let: "m" := !"mutex" in
@@ -179,8 +154,8 @@ Section code.
     subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
-    wp_apply (acquire_spec with "[] Hα");
-      [reflexivity|done|by iApply (mutex_acc with "LFT Hshr Hακ'")|..].
+    iDestruct "Hshr" as (γ) "Hshr".
+    wp_apply (acquire_spec with "LFT [$Hshr $Hα]"); [solve_ndisj|done..|].
     iIntros "[Hcont Htok]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
     iMod ("Hclose1" with "Htok HL") as "HL".
     (* Switch back to typing mode. *)
@@ -189,7 +164,7 @@ Section code.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
-      iExists _. iFrame "#∗". }
+      iExists _. iFrame "#∗". iExists _. iFrame "#". }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -299,8 +274,8 @@ Section code.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (β) "(#Hαβ & #Hshr & Hcnt)".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
-    wp_apply (release_spec with "[] [Hα Hcnt]");
-      [reflexivity|done|by iApply (mutex_acc with "LFT Hshr Hαβ")|by iFrame|..].
+    iDestruct "Hshr" as (γ) "Hshr".
+    wp_apply (release_spec with "LFT [$Hshr $Hα $Hcnt]"); [solve_ndisj|done..|].
     iIntros "Htok". wp_seq. iMod ("Hclose1" with "Htok HL") as "HL".
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _ ]