diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 171c5c3a05da8e073915003dda7321e97e209804..013e4b85d771863c2253a8159e5391494d6f1071 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-10-03.0.63d7ad95") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-12-06.1.197f500e") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index b86777e524bab87cb30f230557356d29a89e590c..d8b6b66ea4922fb649d8e09acdac37146e1a22f8 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -2,9 +2,11 @@ From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl csum frac auth agree.
 From iris.base_logic.lib Require Import invariants.
+
 From gpfsl.gps Require Import middleware protocols.
 From gpfsl.logic Require Import view_invariants.
 From lrust.lang Require Import notation new_delete arc_cmra.
+
 Set Default Proof Using "Type".
 
 (* Rust Arc has a maximum number of clones to prevent overflow. We currently
@@ -132,12 +134,12 @@ Section ArcInv.
      this is the lifetime token), and P2 is the thing that is owned by the
      protocol when only weak references are left (in practice, P2 is the
      ownership of the underlying memory incl. deallocation). *)
-  Context `{noprolG Σ, arcG Σ, view_invG Σ}
+  Context `{!noprolG Σ, !arcG Σ, !view_invG Σ}
           (P1 : Qp → vProp Σ) (P2 : vProp Σ) (N : namespace).
   Local Notation vProp := (vProp Σ).
 
   Definition SeenActs γ l (Mt: gset time) : vProp :=
-    (∃ t v, GPS_SWReader l t () v γ ∗ ⌜∀ t', t' ∈ Mt → t' ⊑ t⌝)%I.
+    (∃ t v, GPS_Reader l t () v γ ∗ ⌜∀ t', t' ∈ Mt → t' ⊑ t⌝)%I.
 
   Definition WkResources lw ls t v γi γw γs γsw q Ut : vProp :=
     (* writer permission and remaining reader permission *)
@@ -246,13 +248,13 @@ Section ArcInv.
 
   Definition strong_arc_acc l t γi γs γw γsw P E : vProp :=
     (□ (P ={E,↑histN}=∗ ∃ Vb q,
-          (monPred_in Vb → ▷ strong_arc t q l γi γs γw γsw) ∗
-          ((monPred_in Vb → ▷ strong_arc t q l γi γs γw γsw) ={↑histN,E}=∗ P)))%I.
+          (⊒Vb → ▷ strong_arc t q l γi γs γw γsw) ∗
+          ((⊒Vb → ▷ strong_arc t q l γi γs γw γsw) ={↑histN,E}=∗ P)))%I.
 
   Definition weak_arc_acc l t γi γs γw γsw P E : vProp :=
     (□ (P ={E,↑histN}=∗ ∃ Vb q,
-      (monPred_in Vb → ▷ weak_arc t q l γi γs γw γsw) ∗
-      ((monPred_in Vb → ▷ weak_arc t q l γi γs γw γsw) ={↑histN,E}=∗ P)))%I.
+      (⊒Vb → ▷ weak_arc t q l γi γs γw γsw) ∗
+      ((⊒Vb → ▷ weak_arc t q l γi γs γw γsw) ={↑histN,E}=∗ P)))%I.
 
   Definition arc_inv γi γs γw γsw (l : loc) : vProp :=
     (((∃ Mt, StrongMoveAuth γsw Mt) ∗
@@ -274,7 +276,7 @@ Section arc.
      this is the lifetime token), and P2 is the thing that is owned by the
      protocol when only weak references are left (in practice, P2 is the
      ownership of the underlying memory incl. deallocation). *)
-  Context `{noprolG Σ, arcG Σ, view_invG Σ}
+  Context `{!noprolG Σ, !arcG Σ, !view_invG Σ}
           (P1 : Qp → vProp Σ)
           (P2 : vProp Σ) (N : namespace).
   Local Notation vProp := (vProp Σ).
@@ -352,13 +354,13 @@ Section arc.
   Qed.
 
   Lemma arc_inv_split Vb γi γs γw γsw l E:
-    (monPred_in Vb → ▷ arc_inv P1 P2 γi γs γw γsw l)
+    (⊒Vb → ▷ arc_inv P1 P2 γi γs γw γsw l)
     ={E}=∗ ((∃ Mt, StrongMoveAuth γsw Mt) ∗
             (∃ Dt, StrongDownAuth γsw Dt) ∗
             (∃ Ut, WeakUpAuth γsw Ut)) ∗
-      (monPred_in Vb →
+      (⊒Vb →
         ▷ GPS_INV (strong_interp P1 (l >> 1) γi γw γsw) l strong_noCAS γs) ∗
-      (monPred_in Vb →
+      (⊒Vb →
         ▷ GPS_INV (weak_interp P2 l γi γs γsw) (l >> 1) (weak_noCAS γsw) γw).
   Proof.
     rewrite -!view_join_unfold !view_join_later.
@@ -373,11 +375,11 @@ Section arc.
   Lemma arc_inv_join Vb γi γs γw γsw l :
     (∃ Mt, StrongMoveAuth γsw Mt) -∗ (∃ Dt, StrongDownAuth γsw Dt) -∗
       (∃ Ut, WeakUpAuth γsw Ut) -∗
-      (monPred_in Vb →
+      (⊒Vb →
         ▷ GPS_INV (strong_interp P1 (l >> 1) γi γw γsw) l strong_noCAS γs) -∗
-      (monPred_in Vb →
+      (⊒Vb →
         ▷ GPS_INV (weak_interp P2 l γi γs γsw) (l >> 1) (weak_noCAS γsw) γw) -∗
-    (monPred_in Vb → ▷ arc_inv P1 P2 γi γs γw γsw l).
+    (⊒Vb → ▷ arc_inv P1 P2 γi γs γw γsw l).
   Proof.
     iIntros "SMA SDA WUA IS IW #In". iFrame "SMA SDA WUA".
     iDestruct ("IS" with "In") as "$". by iDestruct ("IW" with "In") as "$".
@@ -386,13 +388,13 @@ Section arc.
   Lemma strong_arc_acc_open l t γi γs γw γsw P E :
     P -∗ strong_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Mt Dt, (StrongTok γsw q ∗
-      (monPred_in Vb → view_tok γi (q / 2)) ∗
-      (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
+      (⊒Vb → view_tok γi (q / 2)) ∗
+      (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
       StrMoves γsw q Mt ∗ StrDowns γsw q Dt ∗ StrWkTok γsw q) ∗
       (∀ Mt' Dt',
         StrongTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
-        (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
+        (⊒Vb → view_tok γi (q / 2)) -∗
+        (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
         StrMoves γsw q (Mt ∪ Mt') -∗
         (if decide (Mt' = ∅) then True else SeenActs γs l Mt') -∗
         StrDowns γsw q (Dt ∪ Dt') -∗
@@ -425,12 +427,12 @@ Section arc.
   Lemma strong_arc_acc_open_no_change l t γi γs γw γsw P E :
     P -∗ strong_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Mt Dt, (StrongTok γsw q ∗
-      (monPred_in Vb → view_tok γi (q / 2)) ∗
-      (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
+      (⊒Vb → view_tok γi (q / 2)) ∗
+      (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
       StrMoves γsw q Mt ∗ StrDowns γsw q Dt ∗ StrWkTok γsw q) ∗
       (StrongTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
-        (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
+        (⊒Vb → view_tok γi (q / 2)) -∗
+        (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
         StrMoves γsw q Mt -∗ StrDowns γsw q Dt -∗
         StrWkTok γsw q ={↑histN,E}=∗ P).
   Proof.
@@ -445,12 +447,12 @@ Section arc.
   Lemma strong_arc_acc_open_2 l t γi γs γw γsw P E :
     P -∗ strong_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Mt Dt, (StrongTok γsw q ∗
-      (monPred_in Vb → view_tok γi (q / 2)) ∗
-      (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
+      (⊒Vb → view_tok γi (q / 2)) ∗
+      (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
       StrMoves γsw q Mt ∗ StrDowns γsw q Dt ∗ StrWkTok γsw q) ∗
       (∀ Mt' Dt',
          StrongTok γsw q -∗
-         (monPred_in Vb → view_tok γi (q / 2)) -∗
+         (⊒Vb → view_tok γi (q / 2)) -∗
         (∃ v, GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
         StrMoves γsw q (Mt ∪ Mt') -∗
         (if decide (Mt' = ∅) then True else SeenActs γs l Mt') -∗
@@ -469,11 +471,11 @@ Section arc.
   Lemma strong_arc_acc_open_no_change_2 l t γi γs γw γsw P E :
     P -∗ strong_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Mt Dt, (StrongTok γsw q ∗
-      (monPred_in Vb → view_tok γi (q / 2)) ∗
-      (∃ v, monPred_in Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
+      (⊒Vb → view_tok γi (q / 2)) ∗
+      (∃ v, ⊒Vb → GPS_SWSharedReader l t ((): unitProtocol) v q γs) ∗
       StrMoves γsw q Mt ∗ StrDowns γsw q Dt ∗ StrWkTok γsw q) ∗
       (StrongTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
+        (⊒Vb → view_tok γi (q / 2)) -∗
         (∃ v, GPS_SWSharedReader l t ((): unitProtocol) v q γs) -∗
         StrMoves γsw q Mt -∗ StrDowns γsw q Dt -∗
         StrWkTok γsw q ={↑histN,E}=∗ P).
@@ -488,13 +490,13 @@ Section arc.
   Lemma weak_arc_acc_open l t γi γs γw γsw P E :
     P -∗ weak_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Ut, (WeakTok γsw q ∗
-        (monPred_in Vb → view_tok γi (q / 2)) ∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) ∗
+        (∃ v, ⊒Vb →
                 GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) ∗
         WkUps γsw q Ut) ∗
       (∀ Ut', WeakTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) -∗
+        (∃ v, ⊒Vb →
                 GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) -∗
         WkUps γsw q (Ut ∪ Ut') -∗
         (if decide (Ut' = ∅) then True else SeenActs γs l Ut') ={↑histN,E}=∗ P).
@@ -519,13 +521,13 @@ Section arc.
   Lemma weak_arc_acc_open_no_change l t γi γs γw γsw P E :
     P -∗ weak_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Ut, (WeakTok γsw q ∗
-        (monPred_in Vb → view_tok γi (q / 2)) ∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) ∗
+        (∃ v, ⊒Vb →
                 GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) ∗
         WkUps γsw q Ut) ∗
       (WeakTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) -∗
+        (∃ v, ⊒Vb →
               GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) -∗
          WkUps γsw q Ut ={↑histN,E}=∗ P).
   Proof.
@@ -539,12 +541,12 @@ Section arc.
   Lemma weak_arc_acc_open_2 l t γi γs γw γsw P E :
     P -∗ weak_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Ut, (WeakTok γsw q ∗
-        (monPred_in Vb → view_tok γi (q / 2)) ∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) ∗
+        (∃ v, ⊒Vb →
                 GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) ∗
         WkUps γsw q Ut) ∗
       (∀ Ut', WeakTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
+        (⊒Vb → view_tok γi (q / 2)) -∗
         (∃ v, GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) -∗
         WkUps γsw q (Ut ∪ Ut') -∗
         (if decide (Ut' = ∅) then True else SeenActs γs l Ut') ={↑histN,E}=∗ P).
@@ -560,12 +562,12 @@ Section arc.
   Lemma weak_arc_acc_open_no_change_2 l t γi γs γw γsw P E :
     P -∗ weak_arc_acc l t γi γs γw γsw P E ={E,↑histN}=∗
       ∃ Vb q Ut, (WeakTok γsw q ∗
-        (monPred_in Vb → view_tok γi (q / 2)) ∗
-        (∃ v, monPred_in Vb →
+        (⊒Vb → view_tok γi (q / 2)) ∗
+        (∃ v, ⊒Vb →
                 GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) ∗
         WkUps γsw q Ut) ∗
       (WeakTok γsw q -∗
-        (monPred_in Vb → view_tok γi (q / 2)) -∗
+        (⊒Vb → view_tok γi (q / 2)) -∗
         (∃ v, GPS_SWSharedReader (l >> 1) t ((): unitProtocol) v q γw) -∗
         WkUps γsw q Ut ={↑histN,E}=∗ P).
   Proof.
@@ -610,8 +612,8 @@ Section arc.
     set Qs : time → time → gname → gname → vProp :=
       (λ ts tw γs γw,
         GPS_SWSharedReader l ts (() : unitProtocol) #1 (1/2)%Qp γs ∗
-        GPS_SWReader l ts (() : unitProtocol) #1 γs ∗
-        GPS_SWReader  (l >> 1) tw (() : unitProtocol) #1 γw)%I.
+        GPS_Reader l ts (() : unitProtocol) #1 γs ∗
+        GPS_Reader  (l >> 1) tw (() : unitProtocol) #1 γw)%I.
     iMod (GPS_SWRaw_Init_vs_strong_2 _ _
           (λ γw, strong_interp P1 (l >> 1) γi γw γsw)
           (λ γs, weak_interp P2 l γi γs γsw) true _ _ () () Qs
@@ -666,8 +668,8 @@ Section arc.
     set Qs : time → time → gname → gname → vProp :=
       (λ ts tw γs γw,
         GPS_SWSharedReader (l >> 1) tw (() : unitProtocol) #1 (1 / 2)%Qp γw ∗
-        GPS_SWReader l ts (() : unitProtocol) #0 γs ∗
-        GPS_SWReader  (l >> 1) tw (() : unitProtocol) #1 γw)%I.
+        GPS_Reader l ts (() : unitProtocol) #0 γs ∗
+        GPS_Reader  (l >> 1) tw (() : unitProtocol) #1 γw)%I.
     iMod (GPS_SWRaw_Init_vs_strong_2 _ _
             (λ γw, strong_interp P1 (l >> 1) γi γw γsw)
             (λ γs, weak_interp P2 l γi γs γsw) true _ _ () () Qs
@@ -694,7 +696,7 @@ Section arc.
 
   Lemma strong_count_spec γi γs γw γsw l t v (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    {{{ GPS_SWReader l t () v γs ∗ P }}}
+    {{{ GPS_Reader l t () v γs ∗ P }}}
       strong_count [ #l] @ tid; ⊤
     {{{ (c : Z), RET #c; P ∗ ⌜0 < c⌝ }}}.
   Proof.
@@ -746,7 +748,7 @@ Section arc.
   Lemma weak_count_spec γi γs γw γsw l t v ts (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗
     strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    GPS_SWReader (l >> 1) t () v γw -∗
+    GPS_Reader (l >> 1) t () v γw -∗
     {{{ P }}}
       weak_count [ #l] @ tid; ⊤
     {{{ (c : Z), RET #c; P ∗ ⌜-1 ≤ c⌝ }}}.
@@ -806,8 +808,8 @@ Section arc.
 
   Lemma clone_arc_spec {HPn: HP1} γi γs γw γsw l t v (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    (∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
-    GPS_SWReader l t () v γs -∗
+    (∃ t' v', GPS_Reader (l >> 1) t' () v' γw) -∗
+    GPS_Reader l t () v γs -∗
     {{{ P }}} clone_arc [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ strong_arc t' q' l γi γs γw γsw ∗ P1 q' }}}.
   Proof.
@@ -1028,7 +1030,7 @@ Section arc.
 
   Lemma downgrade_spec γi γs γw γsw l t v ts (P : vProp) tid:
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    GPS_SWReader (l >> 1) t () v γw -∗
+    GPS_Reader (l >> 1) t () v γw -∗
     {{{ P }}} downgrade [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
   Proof.
@@ -1110,7 +1112,7 @@ Section arc.
       iIntros "!>" (t' [] [_ Ext']). iSplit; last first.
       { iIntros (??) "!> !>". iSplit; last iSplit;
           iIntros "$ !>"; iFrame "SDA oW"; by rewrite /StrDowns. }
-      iSplitL "". { iIntros "!> _ [Eq ?]". iDestruct "Eq" as %Eq1. by inversion Eq1. }
+      iSplitL "". { iIntros "_ [>%Eq1 ?]". by inversion Eq1. }
       iSplitL "". { by iIntros "!> $". } iIntros "_".
       iDestruct 1 as ([iS st]) "[>Eq [>WA WI]]".
       iDestruct "Eq" as %Eq'. inversion Eq'. subst z. clear Eq'.
@@ -1196,8 +1198,8 @@ Section arc.
 
   Lemma clone_weak_spec γi γs γw γsw l t v (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    (∃ t' v', GPS_SWReader l t' () v' γs) -∗
-    GPS_SWReader (l >> 1) t () v γw -∗
+    (∃ t' v', GPS_Reader l t' () v' γs) -∗
+    GPS_Reader (l >> 1) t () v γw -∗
     {{{ P }}} clone_weak [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
   Proof.
@@ -1380,8 +1382,8 @@ Section arc.
 
   Lemma upgrade_spec {HPn: HP1} γi γs γw γsw l t v tw (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l tw γi γs γw γsw P (⊤ ∖ ↑N) -∗
-    (∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
-    GPS_SWReader l t () v γs -∗
+    (∃ t' v', GPS_Reader (l >> 1) t' () v' γw) -∗
+    GPS_Reader l t () v γs -∗
     {{{ P }}} upgrade [ #l] @ tid; ⊤
     {{{ (b : bool) q, RET #b;
         P ∗ if b then ∃ ts, strong_arc ts q l γi γs γw γsw ∗ P1 q else True }}}.
@@ -1459,7 +1461,7 @@ Section arc.
       iIntros "!>" (t' [] [_ Ext']). iSplit; last first.
       { iIntros (??) "!> !>". iSplit; last iSplit; iIntros "$ !>";
                                 iFrame "WUA"; by rewrite /WkUps. } iSplitL "".
-      { iNext. iIntros "_ Eq". iDestruct "Eq" as %Eq. by inversion Eq. }
+      { iIntros "_ >%Eq". by inversion Eq. }
       iSplitL "". { by iIntros "!> $". } iIntros "_".
       iDestruct 1 as (st) "[>Eq [>SA SI]]". iDestruct "Eq" as %Eq.
       inversion Eq. subst z. clear Eq. destruct st as [[q' n]|]; [|done].
@@ -1580,7 +1582,7 @@ Section arc.
       (WeakTok γsw q ∗ WkUps γsw q Ut ∗ (∃ Dt, StrongDownAuth γsw Dt)
         ∗ if decide (z = 1) then True else view_tok γi (q / 2))%I.
     set P' : vProp :=
-      (monPred_in Vb →
+      (⊒Vb →
             ▷ GPS_INV (strong_interp P1 (l >> 1) γi γw γsw) l strong_noCAS γs)%I.
     set Q: time → unitProtocol → vProp :=
       (λ t'' _, (∃ Dt, StrongDownAuth γsw Dt) ∗
@@ -1604,8 +1606,8 @@ Section arc.
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_view_strong (weak_interp P2 l γi γs γsw)
               _ (weak_noCAS γsw) true _ _ z #(z-1) _ _ _ _ _ P P' Q
-              (λ _ _ _, True)%I _ Vb _ (↑histN) with "[$WR $IW $IS Wt WU SDA tok]");
-      [solve_ndisj|solve_ndisj|by left|by left|..].
+              (λ _ _ _, True)%I _ Vb with "[$WR $IW $IS Wt WU SDA tok]");
+      [solve_ndisj|by left|by left|..].
     { iSplitL "".  { iIntros "!>!>" (??? _). by iApply arc_weak_interp_comparable. }
       iSplitR "Wt WU SDA tok"; [|iSplitL""]; [..|by iFrame]; last first.
       { iIntros (????) "!> !>". by iSplit; iIntros "$". }
@@ -1846,7 +1848,7 @@ Section arc.
        StrongDownAuth γsw Dt ∗
        if decide (z = 1) then True else view_tok γi (1 / 2))%I.
     set P' : vProp :=
-      (monPred_in Vb →
+      (⊒Vb →
             ▷ GPS_INV (strong_interp P1 (l >> 1) γi γw γsw) l strong_noCAS γs)%I.
     set Q: time → unitProtocol → vProp :=
       (λ t'' _, (∃ Dt', StrongDownAuth γsw Dt') ∗
@@ -1870,13 +1872,13 @@ Section arc.
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_view_weak (weak_interp P2 l γi γs γsw) _
             (weak_noCAS γsw) _ _ z #(z-1) _ _ _ _ P P' Q (λ _ _ _, True)%I _ Vb
-            _ (↑histN) with "[$WR $IW $IS SDA HP2 SW SM SD oW tok]");
-      [solve_ndisj|solve_ndisj|by left|by left|..].
+            with "[$WR $IW $IS SDA HP2 SW SM SD oW tok]");
+      [solve_ndisj|by left|by left|..].
     { iSplitL "".  { iIntros "!>!>" (??? _). by iApply arc_weak_interp_comparable_2. }
       iSplitR "HP2 SW SM SD oW SDA tok"; [|iSplitL""]; [..|by iFrame]; last first.
       { iIntros (t2 [] [_ Ext2]). iSplit.
-        - iIntros "!> (_&_&_&_&_&SDA&_)".
-          iDestruct 1 as "[Eq NO]". iDestruct "NO" as (t3 Lt3) "Cert".
+        - iIntros "(_&_&_&_&_&SDA&_) >[Eq NO]".
+          iDestruct "NO" as (t3 Lt3) "Cert".
           iDestruct (StrongDownAuth_Cert_include with "[$SDA $Cert]")
             as %Le3%elem_of_subseteq_singleton%MAX. exfalso.
           apply (irreflexive_eq (R:=Pos.lt) t1 t1); [done|].
@@ -2048,7 +2050,7 @@ Section arc.
                       (∃ Mt', StrongMoveAuth γsw Mt') ∗
                       if decide (z = 1) then True else view_tok γi (q / 2))%I.
     set P' : vProp :=
-      (monPred_in Vb →
+      (⊒Vb →
             ▷ GPS_INV (weak_interp P2 l γi γs γsw) (l >> 1) (weak_noCAS γsw) γw)%I.
     set Q: time → unitProtocol → vProp :=
       (λ t'' _, (∃ Mt', StrongMoveAuth γsw Mt') ∗
@@ -2072,8 +2074,8 @@ Section arc.
     iApply (GPS_SWRaw_SharedWriter_CAS_int_view_strong
             (strong_interp P1 (l >> 1) γi γw γsw) _
             strong_noCAS true _ _ z #(z-1) _ _ _ _ _ P P' Q (λ _ _ _, True)%I _ Vb
-            _ (↑histN) with "[$SR $IS $IW St SM SD SMA HP1 oW tok]");
-      [solve_ndisj|solve_ndisj|by left|by left|..].
+            with "[$SR $IS $IW St SM SD SMA HP1 oW tok]");
+      [solve_ndisj|by left|by left|..].
     { iSplitL "". { iIntros "!>!>" (??? _). by iApply arc_strong_interp_comparable. }
       iSplitR "HP1 St SM SD oW SMA tok"; [|iSplitL""]; [..|by iFrame]; last first.
       { iIntros (????) "!> !>". by iSplit; iIntros "$". }
@@ -2389,9 +2391,9 @@ Section arc.
       iIntros "!>" (t' [] [_ Ext']). iSplit; last first.
       { iIntros (??) "!> !>". iSplit; last iSplit;
           iIntros "$ !>"; iFrame "SDA oW"; by rewrite /StrDowns. }
-      iSplitL "". { iIntros "!> _ [Eq _]". iDestruct "Eq" as %Eq. by inversion Eq. }
+      iSplitL "". { iIntros "_ [>%Eq _]". by inversion Eq. }
       iSplitL "". { by iIntros "!> $". } iIntros "_".
-      iDestruct 1 as ([iS st]) "[>Eq [>WA WI]]". iDestruct "Eq" as %Eq'.
+      iDestruct 1 as ([iS st]) "[>%Eq' [>WA WI]]".
       iDestruct (WeakAuth_strong with "[$WA $oW]") as %[qs ?]. subst iS.
       destruct st as [[[q' n]| | ]|];
         [exfalso; inversion Eq'; lia|by exfalso|by exfalso|]. clear Eq'.
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 9c215c85bf8ee1b7ea47d84afc402f841b7d389f..f12ad7aab7d81466f424e57e211bcc2369271bc7 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -72,9 +72,10 @@ Definition arcUR :=
 Class arcG Σ := {
   ArcStG :> inG Σ arcUR;
   ArcPrt_gpsG :> gpsG Σ unitProtocol;
+  Arc_atomG :> atomicG Σ;
   Arc_viewInv :> view_invG Σ;
 }.
-Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol; view_invΣ].
+Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol; atomicΣ; view_invΣ].
 Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index f6d611875027432a3f7f23a9724535c155bf92e3..097f97db2a11615c9c5949d5745cf559b41fd676 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -17,17 +17,16 @@ Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false.
 
 Class lockG Σ := LockG {
   lock_gpsG :> gpsG Σ unitProtocol;
-  lock_gpsExAgG :> gpsExAgG Σ;
+  lock_atomG :> atomicG Σ;
 }.
 
-Definition lockΣ : gFunctors :=
-  #[gpsΣ unitProtocol; GFunctor (agreeR (leibnizO time))].
+Definition lockΣ : gFunctors := #[gpsΣ unitProtocol; atomicΣ].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{noprolG Σ, !lftG Σ view_Lat lft_userE, lockG Σ}.
+  Context `{!noprolG Σ, !lftG Σ view_Lat lft_userE, !lockG Σ}.
 
   Implicit Types (l : loc).
   Local Notation vProp := (vProp Σ).
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 4c98f13b1e58ba11b5ed48e34912dac24b9acc30..337873260e8e4a3b232ebe1f4f8099dfc5693a75 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -32,9 +32,11 @@ Definition join : val :=
 Class spawnG Σ := SpawnG {
   spawn_tokG :> inG Σ (exclR unitO);
   spawn_gpsG :> gpsG Σ unitProtocol;
+  spawn_atomG :> atomicG Σ;
   spawn_viewG :> view_invG Σ }.
 
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO); gpsΣ unitProtocol; view_invΣ].
+Definition spawnΣ : gFunctors :=
+   #[GFunctor (exclR unitO); gpsΣ unitProtocol; atomicΣ; view_invΣ].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index fc832ef3492ccba6863d88af9be9283a0d54990b..f4bf46be77042abaf759f806990de6326e372aa1 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -4,7 +4,8 @@ From lrust.lifetime Require Import at_borrow.
 From gpfsl.gps Require Import middleware.
 
 Section gps_at_bor_SP.
-Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG Σ view_Lat lft_userE} (N: namespace).
+Context `{!noprolG Σ, !atomicG Σ, !gpsG Σ Prtcl, !lftG Σ view_Lat lft_userE}
+        (N: namespace).
 Local Notation vProp := (vProp Σ).
 
 Implicit Types (IP : interpO Σ Prtcl) (IPC: interpCasO Σ Prtcl) (l : loc)
@@ -12,7 +13,7 @@ Implicit Types (IP : interpO Σ Prtcl) (IPC: interpCasO Σ Prtcl) (l : loc)
                (κ : lft) (γ : gname).
 
 Definition GPS_aSP_Reader IP IPC l κ t s v γ : vProp :=
-  (GPS_SWReader l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
+  (GPS_Reader l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
 Definition GPS_aSP_Writer IP IPC l κ t s v γ : vProp :=
   (GPS_SWWriter l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
 Definition GPS_aSP_SharedReader IP IPC l κ t s v q γ : vProp :=
@@ -32,7 +33,7 @@ Proof.
   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.
+    (λ t γ, Q t v γ ∗ GPS_Reader l t s v γ)%I.
   iMod (GPS_SWRaw_Init_vs_strong IP l IPC true _ s Q' with "Hl [HP P]")
     as (γ t) "[Inv [Q R]]".
   { iIntros (t γ) "W". iDestruct (GPS_SWWriter_Reader with "W") as "#$".
@@ -126,7 +127,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
             ⌜∃ vl, v' = #vl ∧ lit_comparable vr vl⌝)%I in
   let VS : vProp :=
     (∀ t' s', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
-        ((▷ (P -∗ IPC l γ t' s' #vr ={E ∖ ↑N}=∗ False)) ∧
+        (((P -∗ ▷ IPC l γ t' s' #vr ={E ∖ ↑N}=∗ False)) ∧
          ((<obj> (▷ IP true l γ t' s' #vr ={E ∖ ↑N}=∗ ▷ Q1 t' s' ∗ ▷ Q2 t' s')) ∗
          (P -∗ ▷ Q2 t' s' ={E ∖ ↑N}=∗ ▷ GPS_SWSharedWriter l t' s' #vr γ ∗
             ∃ s'', ⌜s' ⊑ s''⌝ ∗
@@ -231,7 +232,7 @@ Qed.
 End gps_at_bor_SP.
 
 Section gps_at_bor_PP.
-Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG Σ view_Lat lft_userE}
+Context `{!noprolG Σ, !atomicG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG Σ view_Lat lft_userE}
         (N: namespace).
 Local Notation vProp := (vProp Σ).
 
@@ -240,7 +241,7 @@ Implicit Types (IP : interpO Σ Prtcl) (l : loc)
                (κ : lft) (γ : gname).
 
 Definition GPS_aPP IP l κ t s v γ : vProp :=
-  (GPS_PP_Local l t s v γ ∗ &at{κ, N} (GPS_PPInv IP l γ))%I.
+  (GPS_Reader l t s v γ ∗ &at{κ, N} (GPS_PPInv IP l γ))%I.
 
 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.
@@ -288,7 +289,7 @@ Lemma GPS_aPP_Read IP l κ q R (o: memOrder) t s v γ tid E
 Proof.
   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
+  iApply (GPS_PPRaw_Read IP l 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".
@@ -301,7 +302,7 @@ Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid 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
+          GPS_Reader l t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
   {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
       ∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
     Write o #l v' @ tid; E
@@ -309,7 +310,7 @@ Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
 Proof.
   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
+  iApply (GPS_PPRaw_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".
@@ -329,7 +330,7 @@ Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
     (∀ 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}=∗
+          (∀ t , ⌜(t' < t)%positive⌝ -∗ ▷ (GPS_Reader 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⌝ -∗
@@ -356,7 +357,7 @@ Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
 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
+  iApply (GPS_PPRaw_CAS_int 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".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index e976a095de860622c8e6f6ce03f34cf44a6cdb80..d844b74516c494d47d40b06aeda6051031fd8f8c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -71,7 +71,7 @@ Section arc.
   Qed.
 
   Definition shared_arc_local l γs γw ts tw :=
-    (∃ vs vw, GPS_SWReader l ts () vs γs ∗ GPS_SWReader (l +ₗ 1) tw () vw γw)%I.
+    (∃ vs vw, GPS_Reader l ts () vs γs ∗ GPS_Reader (l +ₗ 1) tw () vw γw)%I.
   Global Instance shared_arc_local_persistent l γs γw ts tw :
     Persistent (shared_arc_local l γs γw ts tw) := _.
   Lemma strong_shared_arc_local t q l γi γs γw γsw:
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index f1e71df7614e22d29f0f3a8da9aa9628741fc8dc..d7e916651c5ae42fefe7a771345d3be44a3a4e70 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -15,9 +15,10 @@ Definition rwlockR := authR rwlock_stR.
 Class rwlockG Σ := RwLockG {
   rwlock_stateG :> inG Σ rwlockR ;
   rwlock_gpsG :> gpsG Σ unitProtocol;
+  rwlock_atomG :> atomicG Σ;
 }.
 
-Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol].
+Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol; atomicΣ].
 Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 6931f4b6cbed8665333e23aec5d7030ebe8bb146..d34eb9ccfd3d9afbbd0c9392958920bd44e5eb1e 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -235,7 +235,7 @@ Section rwlock_functions.
         iApply (rel_sep_objectively with "[$rTrue]").
         iIntros "!>" (t1 [] [_ Ext1]). iSplit; last first; last iSplitL ""; last iSplitL "".
         { iIntros "!>" (v ?) "!>". iSplit; last iSplit; by iIntros "$". }
-        { rewrite /rwlock_noCAS. iIntros "!> _" (Eq).
+        { rewrite /rwlock_noCAS. iIntros "_ >%Eq".
           inversion Eq as [Eq1]. rewrite Eq1 in Hm1. exfalso. by apply Hm1. }
         { iIntros "!>". iDestruct 1 as (st2) "(>#Eq & #Share & F)".
           iIntros "!>". iSplitL ""; iNext; iExists st2; by iFrame "Eq Share". }
@@ -373,7 +373,7 @@ Section rwlock_functions.
       iApply (rel_sep_objectively with "[$rTrue]").
       iIntros "!>" (t1 [] [_ Ext1]). iSplit; last first; last iSplitL ""; last iSplitL "".
       { iIntros "!>" (v ?) "!>". iSplit; last iSplit; by iIntros "$". }
-      { rewrite /rwlock_noCAS. iIntros "!> _" (Eq). by inversion Eq. }
+      { rewrite /rwlock_noCAS. iIntros "_ >%Eq". by inversion Eq. }
       { iIntros "!>". iDestruct 1 as (st2) "(>#Eq & #Share & F)".
         iIntros "!>". iSplitL ""; iNext; iExists st2; by iFrame "Eq Share". }
       iIntros "_". iDestruct 1 as (st2) "(>Eqst & #Share & g & INT)".