diff --git a/Makefile.coq b/Makefile.coq
index eeb6ec48fa33d391aecdbc51f88f00e762356fe4..bf0a23e325f8bcd7c9f47e9a15f232a026c0c1b5 100644
--- a/Makefile.coq
+++ b/Makefile.coq
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.5pl2     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.5pl3     ##
 #############################################################################
 
 # WARNING
diff --git a/atomic.v b/atomic.v
index feec3e8be07c461a835cfbea29b3d8d8e980b736..e765fa87c44b8802ef9aed0287aae95ecf1da087 100644
--- a/atomic.v
+++ b/atomic.v
@@ -1,12 +1,16 @@
 (* Logically atomic triple *)
 
-From iris.program_logic Require Export hoare weakestpre pviewshifts.
+From iris.base_logic Require Export fancy_updates.
+From iris.program_logic Require Export hoare weakestpre.
 From iris.prelude Require Export coPset.
 Import uPred.
 
 Section atomic.
   Context `{irisG Λ Σ} (A: Type).
 
+  (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
+  (* TODO RJ: Don't define atomic_triple_base; everybody should only ever use atomic_triple anyway. *)
+  (* TODO RJ: We probably will want to make `A` an implicit parameter. *)
   Definition atomic_triple_base
              (α: A → iProp Σ) (* atomic pre-condition *)
              (β: A → val _ → iProp Σ) (* atomic post-condition *)
diff --git a/atomic_incr.v b/atomic_incr.v
index 8d96d7c78372f446c71b8853230f7dceb4e472ea..03e6825737f2b41658a79bf883a1ec369a122ca3 100644
--- a/atomic_incr.v
+++ b/atomic_incr.v
@@ -1,8 +1,9 @@
-From iris.program_logic Require Export weakestpre wsat.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris_atomic Require Import atomic.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import coPset.
+From iris.heap_lang.lib Require Import par.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
@@ -34,26 +35,25 @@ Section incr.
     iIntros "!# HP".
     wp_rec.
     wp_bind (! _)%E.
-    iVs ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
+    iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
     wp_load.
-    iVs ("Hvs'" with "Hl") as "HP".
-    iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
-    iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
+    iMod ("Hvs'" with "Hl") as "HP".
+    iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
+    iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
     destruct (decide (x = x')).
     - subst.
       iDestruct "Hvs'" as "[_ Hvs']".
       iSpecialize ("Hvs'" $! #x').
       wp_cas_suc.
-      iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iVsIntro. wp_if. iVsIntro. by iExists x'.
+      iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
+      iModIntro. wp_if. iModIntro. by iExists x'.
     - iDestruct "Hvs'" as "[Hvs' _]".
       wp_cas_fail.
-      iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
-      iVsIntro. wp_if. by iApply "IH".
+      iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
+      iModIntro. wp_if. by iApply "IH".
   Qed.
 End incr.
 
-From iris.heap_lang.lib Require Import par.
 
 Section user.
   Context `{!heapG Σ, !spawnG Σ} (N : namespace).
@@ -72,7 +72,7 @@ Section user.
     rewrite /incr_2.
     wp_let.
     wp_alloc l as "Hl".
-    iVs (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+    iMod (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
     wp_let.
     wp_bind (_ || _)%E.
     iApply (wp_par (λ _, True%I) (λ _, True%I)).
@@ -85,14 +85,14 @@ Section user.
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
       (* mask magic *)
-      iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
-      iVsIntro. iExists x'. iFrame "Hl'". iSplit.
+      iMod (fupd_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
+      iModIntro. iExists x'. iFrame "Hl'". iSplit.
       + (* provide a way to rollback *)
         iIntros "Hl'".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
       + (* provide a way to commit *)
         iIntros (v) "[Heq Hl']".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
     - iDestruct "Hincr" as "#HIncr".
       iSplitL; [|iSplitL];
         try (iApply wp_wand_r; iSplitL; [by iApply "HIncr"|auto]).
diff --git a/atomic_pcas.v b/atomic_pcas.v
index e3d02147d7e90de97cf23f6a9757f35dba6f12a1..316a0dafcbdffbeaac08738e8b25e8e8767407ce 100644
--- a/atomic_pcas.v
+++ b/atomic_pcas.v
@@ -35,7 +35,7 @@ Section atomic_pair.
   
   Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β ⊤.
   Proof.
-    iIntros (_ l) "!# _". wp_seq. iVsIntro. iPureIntro.
+    iIntros (_ l) "!# _". wp_seq. iModIntro. iPureIntro.
     iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
     iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
     iDestruct "Hα" as (a b) "%".
diff --git a/atomic_sync.v b/atomic_sync.v
index 5e5711d85a0fa7f3d9124b8243c372858e9559ee..3e68efb3440ef4bb699325a073f57e7c3a5c4717 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -54,7 +54,7 @@ Section atomic_sync.
         ⊢ WP (sync mk_syncer) f_seq l {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
   Proof.
     iIntros (g0 HN Hseq Hsync) "[#Hh HÏ•]".
-    iVs (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
+    iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
     { by rewrite pair_op dec_agree_idemp. }
     repeat wp_let. wp_bind (mk_syncer _).
     iApply (Hsync (∃ g: A, ϕ l g ★ gHalf γ g)%I)=>//. iFrame "Hh".
@@ -75,23 +75,23 @@ Section atomic_sync.
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[HÏ• Hg1]".
       (* we should view shift at this point *)
-      iDestruct ("Hvss" with "HP") as "Hvss'". iApply pvs_wp.
-      iVs "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
+      iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
+      iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
       iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. subst.
-      iVs ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
-      iVsIntro. iApply H=>//.
+      iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
+      iModIntro. iApply H=>//.
       iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
-      iVs ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
+      iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
       iSpecialize ("Hvs2" $! ret).
       iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
       rewrite Qp_div_2.
-      iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I
-              with "[Hg]" as "==>[Hg1 Hg2]".
+      iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I
+              with "[Hg]" as ">[Hg1 Hg2]".
       { iApply own_update; last by iAssumption.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
-      iVs ("Hvs2" with "[Hg1 Hβ]").
+      iMod ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iVsIntro. iSplitL "Hg2 HÏ•'"; last done.
+      iModIntro. iSplitL "Hg2 HÏ•'"; last done.
       iExists g'. by iFrame.
     - iIntros (?) "?". by iExists g0.
   Qed.
diff --git a/evmap.v b/evmap.v
index f00d9adc772610d321c429cd508b858551d2dc1c..8010da28badb71b701077e5e3d8d1b1386e88bfc 100644
--- a/evmap.v
+++ b/evmap.v
@@ -1,5 +1,6 @@
 (* evmap.v -- generalized heap-like monoid composite *)
-From iris.program_logic Require Export invariants weakestpre.
+From iris.base_logic Require Export invariants.
+From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Export auth frac gmap dec_agree.
 From iris.proofmode Require Import tactics.
 
@@ -58,7 +59,7 @@ Section evmapR.
   (* Alloc a new mapsto *)
   Lemma evmap_alloc γm m k v:
     m !! k = None →
-    own γm (● m) ⊢ |=r=> own γm (● (<[ k := ((), DecAgree v) ]> m) ⋅ ◯ {[ k := ((), DecAgree v) ]}).
+    own γm (● m) ⊢ |==> own γm (● (<[ k := ((), DecAgree v) ]> m) ⋅ ◯ {[ k := ((), DecAgree v) ]}).
   Proof.
     iIntros (?) "Hm".
     iDestruct (own_update with "Hm") as "?"; last by iAssumption.
diff --git a/flat.v b/flat.v
index 3906ebea5d695e73e9a4d47a4fcdd909fa8124a2..6fc1ee8a216b6a070f2031d710630f5eaf47ab00 100644
--- a/flat.v
+++ b/flat.v
@@ -1,10 +1,11 @@
 (* Flat Combiner *)
 
-From iris.program_logic Require Export weakestpre saved_prop.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import auth upred frac agree excl dec_agree upred_big_op gset gmap.
+From iris.algebra Require Import auth frac agree excl dec_agree gset gmap.
+From iris.base_logic Require Import big_op saved_prop.
 From iris_atomic Require Import misc peritem sync evmap.
 
 Definition doOp : val :=
@@ -145,12 +146,12 @@ Section proof.
   Proof.
     iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
     wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
-    iApply pvs_wp.
-    iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
-    iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
-    iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
-    iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
-    iVs (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
+    iApply fupd_wp.
+    iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
+    iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
+    iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
+    iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
+    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
     iInv N as "[Hrs >Hm]" "Hclose".
     iDestruct "Hm" as (m) "[Hm HRm]".
     destruct (m !! p) eqn:Heqn.
@@ -158,19 +159,19 @@ Section proof.
       iDestruct (big_sepM_delete (fun p _ => ∃ v : val, p ↦{1 / 2} v)%I m with "HRm") as "[Hp HRm]"=>//.
       iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hh Hl Hp". auto.
     - (* fresh name *)
-      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 #Hm2]"=>//.
+      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as ">[Hm1 #Hm2]"=>//.
       iDestruct "Hl" as "[Hl1 Hl2]".
-      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
+      iMod ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
       + iNext. iFrame. iExists (<[p := (∅, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
         iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
         iSplitL "Hl1"; last by iAssumption. eauto.
-      + iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
-        iVsIntro. wp_let. wp_bind ((push _) _).
+      + iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
+        iModIntro. wp_let. wp_bind ((push _) _).
         iApply install_push_spec=>//.
         iFrame "#". rewrite /evm /installed_s. iFrame.
         iSplitL "Hpx Hf".
         { iExists P, Q. by iFrame. }
-        iIntros "Hhd". wp_seq. iVsIntro.
+        iIntros "Hhd". wp_seq. iModIntro.
         iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
         { rewrite /installed_recp. iFrame. iFrame "#". }
         by iApply ("HΦ" with "[]").
@@ -199,34 +200,34 @@ Section proof.
       iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst.
       iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
       + iDestruct "Hp" as (y) "(>Hp & Hs)".
-        wp_load. iVs ("Hclose" with "[-Hor HR Hev HΦ']").
+        wp_load. iMod ("Hclose" with "[-Hor HR Hev HΦ']").
         { iNext. iFrame. iExists gxs, ghd.
           iFrame "Hghd Hgxs". iExists m.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
           iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
-        iVsIntro. wp_match. iVsIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
+        iModIntro. wp_match. iModIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
       + iDestruct "Hp" as (f' x') "(Hp & Hs)".
         wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
         iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
-        iAssert (|=r=> own γx (((1/2/2)%Qp, DecAgree x') ⋅
-                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as "==>[Hx1 Hx2]".
+        iAssert (|==> own γx (((1/2/2)%Qp, DecAgree x') ⋅
+                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
         { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
           rewrite -{1}(Qp_div_2 (1/2)%Qp).
           by apply pair_l_frac_op'. }
-        iVs ("Hclose" with "[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
+        iMod ("Hclose" with "[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
         { iNext. iFrame. iExists gxs, ghd.
           iFrame "Hghd Hgxs". iExists m.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
           iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
           iFrame "#". iRight. iRight. iLeft. iExists f', x'. iFrame. }
-        iVsIntro. wp_match.
+        iModIntro. wp_match.
         wp_proj. wp_proj.
         wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
         { iApply "Hf'". iFrame. }
         iIntros (v) "[HR HQ]".
-        wp_value. iVsIntro. iInv N as "[Hs >Hm]" "Hclose".
+        wp_value. iModIntro. iInv N as "[Hs >Hm]" "Hclose".
         iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
         iDestruct "HRs" as (m') "[>Hom HRs]".
         iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
@@ -251,7 +252,7 @@ Section proof.
             rewrite Qp_div_2. wp_store.
             (* now close the invariant *)
             iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
-            subst. rewrite Qp_div_2. iVs ("Hclose" with "[-HR Hor HΦ']").
+            subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ']").
             { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
               iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
               { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
@@ -276,14 +277,14 @@ Section proof.
         iApply excl_falso. iFrame.
       + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
         iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
-        wp_load. iVs ("Hclose" with "[-HΦ' HR Hor]").
+        wp_load. iMod ("Hclose" with "[-HΦ' HR Hor]").
         { iNext. iFrame. iExists gxs, ghd.
           iFrame "Hghd Hgxs". iExists m.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
           iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
           iExists Q. iFrame. }
-        iVsIntro. wp_match.
+        iModIntro. wp_match.
         iApply "HΦ'". iFrame.
     - apply to_of_val.
     - iFrame "#". iFrame. iIntros "[Hor HR]".
@@ -310,17 +311,17 @@ Section proof.
     wp_if. wp_bind (! _)%E.
     iInv N as "[H >Hm]" "Hclose".
     iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
-    wp_load. iDestruct (dup_is_list' with "[Hxs]") as "==>[Hxs1 Hxs2]"; first by iFrame.
-    iVs ("Hclose" with "[Hs Hxs1 HRs Hm]").
+    wp_load. iDestruct (dup_is_list' with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
+    iMod ("Hclose" with "[Hs Hxs1 HRs Hm]").
     { iNext. iFrame. iExists xs', hd'. by iFrame. }
-    iVsIntro. wp_let.
+    iModIntro. wp_let.
     wp_bind (iter _ _).
     iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
     { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ★ R ★ v = #()))%I=>//.      
       iFrame "#". iFrame. iIntros "? ?". by iFrame. }
     iIntros (f') "[Ho [HR %]]". subst.
     wp_let. iApply release_spec. iFrame "#".
-    iFrame.
+    iFrame. iNext. iIntros. done.
   Qed.
 
   Lemma loop_spec R (p s: loc) (lk: val)
@@ -350,38 +351,38 @@ Section proof.
       + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
         iApply excl_falso. iFrame.
       + iDestruct "Hp" as (f x) "(>Hp & Hs')".
-        wp_load. iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
+        wp_load. iMod ("Hclose" with "[-Ho3 HΦ Hhd]").
         { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
           iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p.
           iSplitR; first auto. iFrame.
           iRight. iLeft. iExists f, x. iFrame. }
-        iVsIntro. wp_match.
+        iModIntro. wp_match.
         wp_bind (try_srv _ _). iApply try_srv_spec=>//.
         iFrame "#". wp_seq.
         iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
         by iApply ("IH" with "Ho3 Hhd").
       + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
         wp_load.
-        iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
+        iMod ("Hclose" with "[-Ho3 HΦ Hhd]").
         { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
           iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
           iSplitR; first auto. iFrame.
           iRight. iRight. iLeft. iExists f, x. iFrame. }
-        iVsIntro. wp_match.
+        iModIntro. wp_match.
         wp_bind (try_srv _ _). iApply try_srv_spec=>//.
         iFrame "#". wp_seq.
         iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
         by iApply ("IH" with "Ho3 Hhd").
        + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
-          wp_load. iVs ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
+          wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
           { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
             iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
             iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
             iSplitR; first auto. iFrame.
             iLeft. iExists y. iFrame. }
-          iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
+          iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
           iExists Q. iFrame.
     - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
       rewrite /ev. eauto.
@@ -390,19 +391,19 @@ Section proof.
   Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
   Proof.
     iIntros (R Φ HN) "(#Hh & HR & HΦ)".
-    iVs (own_alloc (Excl ())) as (γr) "Ho2"; first done.
-    iVs (own_alloc (● (∅: tokmR) ⋅ ◯ ∅)) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
+    iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
+    iMod (own_alloc (● (∅: tokmR) ⋅ ◯ ∅)) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
     iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
     { iExists ∅. iFrame. by rewrite big_sepM_empty. }
     wp_seq. wp_bind (newlock _).
     iApply (newlock_spec _ (own γr (Excl ()) ★ R))%I=>//.
-    iFrame "Hh Ho2 HR". iIntros (lk γlk) "#Hlk".
+    iFrame "Hh Ho2 HR". iNext. iIntros (lk γlk) "#Hlk".
     wp_let. wp_bind (new_stack _).
     iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
     iFrame "Hh Hm". iIntros (γ s) "#Hss".
-    wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
+    wp_let. iModIntro. iApply "HΦ". rewrite /synced.
     iAlways.
-    iIntros (f). wp_let. iVsIntro. iAlways.
+    iIntros (f). wp_let. iModIntro. iAlways.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let.
     wp_bind (install _ _ _).
diff --git a/misc.v b/misc.v
index 3b3d2f23b0c260e5dfb40b477f49ef23a0ff64c5..0a559fd772ff3744ad23875a3540da27bcd22fd0 100644
--- a/misc.v
+++ b/misc.v
@@ -2,9 +2,9 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap dec_agree upred_big_op.
+From iris.algebra Require Import auth frac gmap dec_agree.
 From iris.prelude Require Import countable.
-From iris.program_logic Require Import auth.
+From iris.base_logic Require Import big_op auth.
 Import uPred.
 
 Section lemmas.
diff --git a/peritem.v b/peritem.v
index 4c6e12924f876700d571a0999f3e8b24561bef8d..ae09eb76f96ff83a74653e48d95e3748c79e1d42 100644
--- a/peritem.v
+++ b/peritem.v
@@ -1,7 +1,8 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth upred gmap dec_agree upred_big_op csum.
+From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.base_logic Require Import big_op.
 From iris_atomic Require Export treiber misc evmap.
 
 Section defs.
@@ -50,27 +51,27 @@ Section defs.
   Proof. apply _. Qed.
 
   Lemma dup_is_list' γ : ∀ xs hd,
-    heap_ctx ★ is_list' γ hd xs ⊢ |=r=> is_list' γ hd xs ★ is_list' γ hd xs.
+    heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list' γ hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "(#? & Hs)".
       simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
     - iIntros (hd) "(#? & Hs)". simpl.
       iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hev & Hs')".
-      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
-      iVsIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
+      iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
+      iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
 
   Lemma extract_is_list γ : ∀ xs hd,
-    heap_ctx ★ is_list' γ hd xs ⊢ |=r=> is_list' γ hd xs ★ is_list hd xs.
+    heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "(#? & Hs)".
       simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
     - iIntros (hd) "(#? & Hs)". simpl.
       iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hev & Hs')".
-      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
-      iVsIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
+      iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
+      iModIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
 
   Definition f_spec γ (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) :=
@@ -92,7 +93,7 @@ Lemma new_stack_spec' Φ RI:
     ⊢ WP new_stack #() {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & HR & HΦ)".
-    iVs (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
+    iMod (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
     { apply auth_valid_discrete_2. done. }
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
     wp_alloc s as "Hs".
@@ -100,7 +101,7 @@ Lemma new_stack_spec' Φ RI:
     { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl".
       - eauto.
       - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). }
-    iVs (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
+    iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
     by iApply "HΦ".
   Qed.
     
@@ -114,10 +115,10 @@ Lemma new_stack_spec' Φ RI:
     induction xs as [|x xs' IHxs'].
     - simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (q) "Hhd".
-      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
+      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
     - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
-      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. wp_proj.
       wp_bind (f' _). iApply Hf=>//. iFrame "#".
       iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
@@ -137,20 +138,20 @@ Lemma new_stack_spec' Φ RI:
       (* open the invariant *)
       iInv N as "[IH1 ?]" "Hclose".
       iDestruct "IH1" as (xs hd) "[>Hs [>Hxs HR]]".
-      iDestruct (extract_is_list with "[Hxs]") as "==>[Hxs Hxs']"; first by iFrame.
+      iDestruct (extract_is_list with "[Hxs]") as ">[Hxs Hxs']"; first by iFrame.
       iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
       (* mask magic *)
-      iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
-      iVsIntro. iExists (xs, hd).
+      iMod (fupd_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
+      iModIntro. iExists (xs, hd).
       iFrame "Hs Hxs'1". iSplit.
       + (* provide a way to rollback *)
         iIntros "[Hs Hl']".
-        iVs "Hvs". iVs ("Hclose" with "[-Rx]"); last done.
+        iMod "Hvs". iMod ("Hclose" with "[-Rx]"); last done.
         { iNext. iFrame. iExists xs. iExists hd. by iFrame. }
       + (* provide a way to commit *)
         iIntros (v) "Hs".
         iDestruct "Hs" as (hd') "[% [Hs [[Hhd'1 Hhd'2] Hxs']]]". subst.
-        iVs "Hvs".
+        iMod "Hvs".
         iDestruct "HR" as (m) "[>Hom HRm]".
         destruct (m !! hd') eqn:Heqn.
         * iDestruct (big_sepM_delete_later (perR R) m with "HRm") as "[Hx ?]"=>//.
@@ -161,9 +162,9 @@ Lemma new_stack_spec' Φ RI:
           iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
           iFrame "#". iFrame.
         * iAssert (evs γ hd' x ★ ▷ (allR R γ))%I
-                  with "==>[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
+                  with ">[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
           {
-            iDestruct (evmap_alloc _ _ _ m with "[Hom]") as "==>[Hom Hox]"=>//.
+            iDestruct (evmap_alloc _ _ _ m with "[Hom]") as ">[Hom Hox]"=>//.
             iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//.
             iSplitL "Hox".
             { rewrite /evs /ev. eauto. }
@@ -171,12 +172,12 @@ Lemma new_stack_spec' Φ RI:
             iFrame. iApply "H". iFrame. iExists x.
             iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto.
           }
-          iVs ("Hclose" with "[-]").
+          iMod ("Hclose" with "[-]").
           { iNext. iFrame. iExists (x::xs).
             iExists hd'. iFrame.
             iExists hd, (1/2)%Qp. by iFrame.
           }
-        iVsIntro. iSplitL; last auto. by iExists hd'.
+        iModIntro. iSplitL; last auto. by iExists hd'.
     - iApply wp_wand_r. iSplitL "HRx Hpush".
       + by iApply "Hpush".
       + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
diff --git a/simple_sync.v b/simple_sync.v
index 861e678175fc0ad49c225a3bd81da4547691843d..a8b8a073bbe4ef2bfb10a64705897f8e54d46d30 100644
--- a/simple_sync.v
+++ b/simple_sync.v
@@ -26,18 +26,17 @@ Section syncer.
     iIntros (R Φ HN) "(#Hh & HR & HΦ)".
     wp_seq. wp_bind (newlock _).
     iApply newlock_spec; first done.
-    iSplitR "HR HΦ"; first done.
-    iFrame "HR".
+    iSplitL "HR"; first by iFrame. iNext.
     iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    iIntros (f). wp_let. iVsIntro. iAlways.
+    iIntros (f). wp_let. iModIntro. iAlways.
     iIntros (P Q x) "#Hf !# HP".
     wp_let. wp_bind (acquire _).
-    iApply acquire_spec. iSplit; first done.
-    iIntros "Hlocked R". wp_seq. wp_bind (f _).
+    iApply acquire_spec. iSplit; first done. iNext.
+    iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
     iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
     iApply wp_wand_r.  iSplitL "Hf'"; first done.
     iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
-    iApply release_spec. iFrame "HR". iSplitR; first done.
-    iFrame. by wp_seq.
+    iApply release_spec. iFrame "HR Hl Hlocked".
+    iNext. iIntros "_". by wp_seq.
   Qed.
 End syncer.
diff --git a/treiber.v b/treiber.v
index 3480de629516c0ef2fb20c84b9423d21812cceda..1a436b007ca96ece4d5ed5ca06333da56f5e6577 100644
--- a/treiber.v
+++ b/treiber.v
@@ -1,7 +1,8 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth upred gmap dec_agree upred_big_op csum.
+From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.base_logic Require Import big_op.
 From iris_atomic Require Import atomic misc.
 
 Definition new_stack: val := λ: <>, ref (ref NONE).
@@ -123,20 +124,20 @@ Section proof.
     iIntros (P Q) "#Hvs".
     iLöb as "IH". iIntros "!# HP". wp_rec.
     wp_let. wp_bind (! _)%E.
-    iVs ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
-    wp_load. iVs ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
-    iVsIntro. wp_let. wp_alloc l as "Hl". wp_let.
+    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
+    wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
+    iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
     wp_bind (CAS _ _ _)%E.
-    iVs ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
+    iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
     destruct (decide (hd = hd')) as [->|Hneq].
     * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
-      iVs ("Hvs'" $! #() with "[-]") as "HQ".
+      iMod ("Hvs'" $! #() with "[-]") as "HQ".
       { iExists l. iSplitR; first done. by iFrame. }
-      iVsIntro. wp_if. iVsIntro. eauto.
+      iModIntro. wp_if. iModIntro. eauto.
     * wp_cas_fail.
       iDestruct "Hvs'" as "[Hvs' _]".
-      iVs ("Hvs'" with "[-]") as "HP"; first by iFrame.
-      iVsIntro. wp_if. by iApply "IH".
+      iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
+      iModIntro. wp_if. by iApply "IH".
   Qed.
 
   Definition pop_triple (s: loc) :=
@@ -159,24 +160,24 @@ Section proof.
     iIntros (P Q) "#Hvs".
     iLöb as "IH". iIntros "!# HP". wp_rec.
     wp_bind (! _)%E.
-    iVs ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
+    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
     destruct xs as [|y' xs'].
     - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
       iDestruct "Hhd" as (q) "[Hhd Hhd']".
-      iVs ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
+      iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
       { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
-      iVsIntro. wp_let. wp_load. wp_match.
-      iVsIntro. eauto.
+      iModIntro. wp_let. wp_load. wp_match.
+      iModIntro. eauto.
     - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
       iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
       wp_load. iDestruct "Hvs'" as "[Hvs' _]".
-      iVs ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
+      iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
       { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
-      iVsIntro. wp_let. wp_load. wp_match. wp_proj.
-      wp_bind (CAS _ _ _). iVs ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
+      iModIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_bind (CAS _ _ _). iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
       destruct (decide (hd = hd'')) as [->|Hneq].
       + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
-        iVs ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
+        iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
         { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
           destruct xs as [|x' xs''].
           - simpl. iDestruct "Hhd''" as (?) "H".
@@ -190,10 +191,10 @@ Section proof.
             iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
             repeat (iSplitR "Hxs1 Hs"; first done).
             iFrame. }
-        iVsIntro. wp_if. wp_proj. eauto.
+        iModIntro. wp_if. wp_proj. eauto.
       + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
-        iVs ("Hvs'" with "[-]") as "HP"; first by iFrame.
-        iVsIntro. wp_if. by iApply "IH".
+        iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
+        iModIntro. wp_if. by iApply "IH".
   Qed.
 
 End proof.