diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 3b12c56bc..fdf07eb96 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -39,10 +39,14 @@ jobs:
             startGroup "Install dependencies"
               opam install odoc -y
               apt-get install rsync -y
+              opam pin add -y rocq-stdpp 1.13.0
+              opam pin add -y rocq-iris.dev  git+https://gitlab.mpi-sws.org/iris/iris.git#93c7df745a0485cebcb97ca77e7d263e5c920d4f --ignore-constraints-on=rocq-stdpp
               opam pin add -n -y -k path $PACKAGE $WORKDIR
               opam update -y
               opam reinstall --forget-pending --yes
-              opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only --with-doc
+              opam install --confirm-level=unsafe-yes -j 2 rocq-stdpp.1.13.0
+              opam install --confirm-level=unsafe-yes -j 2 \
+                --ignore-constraints-on=rocq-stdpp $PACKAGE --deps-only --with-doc
             endGroup
           script: |
             startGroup Build
diff --git a/dune-project b/dune-project
index 21462fb80..2ca827de0 100644
--- a/dune-project
+++ b/dune-project
@@ -2,9 +2,9 @@
 
 (using rocq 0.11)
 
-; (name clutch)
+(name rocq-clutch)
 
-(generate_opam_files true)
+(generate_opam_files false)
 
 (source (github logsem/clutch))
 
@@ -33,7 +33,7 @@
   ; at least rocq 9.1 is needed to work with dune's rocq-lang feature
   (rocq-core (and (>= 9.1.1) (< "9.2~")))
   (rocq-stdlib (and (>= 9.0.0) (< "9.2~")))
-  (rocq-iris (= "4.5.0"))
+  (rocq-iris (= "dev"))
   (rocq-stdpp (= "1.13.0"))
   (coq-coquelicot (= "3.4.4"))
   (coq-autosubst (= "dev"))
diff --git a/rocq-clutch.opam b/rocq-clutch.opam
index 5a3734db1..90cf26a1d 100644
--- a/rocq-clutch.opam
+++ b/rocq-clutch.opam
@@ -1,4 +1,3 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Higher-order probabilistic separation logics"
 maintainer: ["Simon Oddershede Gregersen <s.gregersen@nyu.edu>"]
@@ -20,7 +19,11 @@ depends: [
   "ocaml" {>= "5.4.0" & < "5.5~"}
   "rocq-core" {>= "9.1.1" & < "9.2~"}
   "rocq-stdlib" {>= "9.0.0" & < "9.2~"}
-  "rocq-iris" {= "4.5.0"}
+  # NOTE: Mainline iris pinned to the merge of MR 1217.
+  # main iris opam declares a strict stdpp dev constraint, but its
+  # Rocq source is compatible with stdpp 1.13.0.
+  # Install with: [opam install . --ignore-constraints-on=rocq-stdpp]
+  "rocq-iris" {= "dev"}
   "rocq-stdpp" {= "1.13.0"}
   "coq-coquelicot" {= "3.4.4"}
   "coq-autosubst" {= "dev"}
diff --git a/theories/approxis/primitive_laws.v b/theories/approxis/primitive_laws.v
index 6769d6b4a..b7238201a 100644
--- a/theories/approxis/primitive_laws.v
+++ b/theories/approxis/primitive_laws.v
@@ -47,7 +47,7 @@ Definition tapes_auth `{approxisGS Σ} :=
 
 Global Instance approxisGS_irisGS `{!approxisGS Σ} : approxisWpGS prob_lang Σ := {
   approxisWpGS_invGS := approxisGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
   err_interp := ec_supply;
 }.
 
diff --git a/theories/caliper/primitive_laws.v b/theories/caliper/primitive_laws.v
index 39739d299..f1fc02f41 100644
--- a/theories/caliper/primitive_laws.v
+++ b/theories/caliper/primitive_laws.v
@@ -46,7 +46,7 @@ Definition tapes_auth `{caliperG δ Σ} :=
 #[export] Instance caliperG_caliperWpG `{caliperG δ Σ} : caliperWpG δ prob_lang Σ := {
   caliperWpG_invGS := caliperG_invG;
 
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
 }.
 
 (** Heap *)
diff --git a/theories/clutch/examples/keyed_hash.v b/theories/clutch/examples/keyed_hash.v
index 4c7a81b3f..33fba83fd 100644
--- a/theories/clutch/examples/keyed_hash.v
+++ b/theories/clutch/examples/keyed_hash.v
@@ -294,13 +294,13 @@ Section keyed_hash.
   Definition keyed_hash_auth (γ : gname) (f : val) : iProp Σ :=
     ∃ (f0 : val) (mphys : gmap nat bool) (mghost : gmap fin_hash_dom_space (option bool)),
       keyed_hash_auth_pure f f0 mphys mghost ∗
-      ghost_map_auth γ 1 mghost ∗
+      ghost_map_auth γ (DfracOwn 1) mghost ∗
       hashfun' MAX_HASH_DOM f0 mphys.
 
   Definition skeyed_hash_auth (γ : gname) (f : val) : iProp Σ :=
     ∃ (f0 : val) (mphys : gmap nat bool) (mghost : gmap fin_hash_dom_space (option bool)),
       keyed_hash_auth_pure f f0 mphys mghost ∗
-      ghost_map_auth γ 1 mghost ∗
+      ghost_map_auth γ (DfracOwn 1) mghost ∗
       shashfun' MAX_HASH_DOM f0 mphys.
 
   Section timeless_spec.
diff --git a/theories/clutch/primitive_laws.v b/theories/clutch/primitive_laws.v
index 7adf8c2ee..7ea037a03 100644
--- a/theories/clutch/primitive_laws.v
+++ b/theories/clutch/primitive_laws.v
@@ -43,7 +43,7 @@ Definition tapes_auth `{clutchGS Σ} :=
 
 #[global] Instance clutchGS_clutchWpGS `{!clutchGS Σ} : clutchWpGS prob_lang Σ := {
   clutchWpGS_invGS := clutchGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
 }.
 
 (** Heap *)
diff --git a/theories/con_prob_lang/spec/spec_ra.v b/theories/con_prob_lang/spec/spec_ra.v
index c21b97c4c..c7e7d0009 100644
--- a/theories/con_prob_lang/spec/spec_ra.v
+++ b/theories/con_prob_lang/spec/spec_ra.v
@@ -66,11 +66,11 @@ Qed.
 Section resources.
   Context `{!specG_con_prob_lang Σ}.
   Definition spec_prog_auth :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_prog specG_con_prob_lang_prog_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_prog specG_con_prob_lang_prog_name (DfracOwn 1).
   Definition spec_heap_auth :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_heap specG_con_prob_lang_heap_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_heap specG_con_prob_lang_heap_name (DfracOwn 1).
   Definition spec_tapes_auth  :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_tapes specG_con_prob_lang_tapes_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_tapes specG_con_prob_lang_tapes_name (DfracOwn 1).
 
   Definition spec_auth (ρ : cfg) : iProp Σ :=
     spec_prog_auth (to_tpool ρ.1) ∗
diff --git a/theories/coneris/examples/con_two_add.v b/theories/coneris/examples/con_two_add.v
index 09f14cdfe..0e9aadda3 100644
--- a/theories/coneris/examples/con_two_add.v
+++ b/theories/coneris/examples/con_two_add.v
@@ -98,7 +98,7 @@ Section complex'.
      form of the paper *)
 
   Definition parallel_add_inv' (γ1 γ2: gname) l: iProp Σ :=
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2) s1 ∗ ghost_var γ2 (1/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2)) s2 ∗
       (((l ↦ #0 ∗ ⌜ no_thread_added s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ one_thread_added n s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ ⌜ both_threads_added n s1 s2 ⌝)) ∗
@@ -138,9 +138,9 @@ Section complex'.
   Qed.
 
   Lemma rand_step γ1 γ2 l:
-    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (1/2) S0 }}}
+    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (DfracOwn (1/2)) S0 }}}
       rand #3
-      {{{ (n: nat), RET #n; ghost_var γ1 (1/2) (S1 n) }}}.
+      {{{ (n: nat), RET #n; ghost_var γ1 (DfracOwn (1/2)) (S1 n) }}}.
   Proof.
     iIntros (Φ) "(#I&Hfrag1) HΦ".
     iInv "I" as ">(%s1&%s2&Hauth1&Hauth2&Hstate&Hsamp)".
@@ -194,9 +194,9 @@ Section complex'.
   Qed.
 
   Lemma faa_step γ1 γ2 l (n: nat) :
-    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (1/2) (S1 n) }}}
+    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (DfracOwn (1/2)) (S1 n) }}}
       FAA #l #n
-    {{{ (v : val), RET v; ghost_var γ1 (1/2) (S2 n) }}}.
+    {{{ (v : val), RET v; ghost_var γ1 (DfracOwn (1/2)) (S2 n) }}}.
   Proof.
     iIntros (Φ) "(#I&Hfrag1) HΦ".
     iInv "I" as ">(%s1&%s2&Hauth1&Hauth2&Hstate&Hsamp)".
@@ -272,8 +272,8 @@ Section complex'.
       { iPureIntro. left. by eauto. }
       { iLeft. iFrame. }
     }
-    wp_apply (wp_par (λ _, ∃ (n:nat), ghost_var γ1 (1/2) (S2 n))%I
-                (λ _, ∃ (n:nat), ghost_var γ2 (1/2) (S2 n))%I with "[Hfrag1][Hfrag2]").
+    wp_apply (wp_par (λ _, ∃ (n:nat), ghost_var γ1 (DfracOwn (1/2)) (S2 n))%I
+                (λ _, ∃ (n:nat), ghost_var γ2 (DfracOwn (1/2)) (S2 n))%I with "[Hfrag1][Hfrag2]").
     - wp_apply (rand_step with "[$]").
       iIntros (n) "Hfrag1".
       wp_apply (faa_step with "[$]").
@@ -305,7 +305,7 @@ Section complex'.
   Qed.
 
   Definition gs γ1 γ2 P : iProp Σ :=
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗ ⌜ P s1 s2 ⌝.
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗ ⌜ P s1 s2 ⌝.
 
   (* In the paper we do not have leading existentials in the descriptions of the invariant.
      This alternate version matching the paper is defined next . It is equivalent to what
@@ -327,7 +327,7 @@ Section complex'.
          (∃ n : nat, l ↦ #n ∗ gs γ1 γ2 (one_thread_added n)) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ gs γ1 γ2 (both_threads_added n)))
    -∗
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗
       (((l ↦ #0 ∗ ⌜ no_thread_added s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ one_thread_added n s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ ⌜ both_threads_added n s1 s2 ⌝))).
@@ -342,7 +342,7 @@ Section complex'.
      (↯(1) ∗ gs γ1 γ2 (λ _ _, True : Prop)) ∨
      (↯(0) ∗ gs γ1 γ2 at_least_one_thread_sampled_non_zero))
    -∗
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗
        ((↯(1/16) ∗ ⌜ no_thread_sampled s1 s2 ⌝) ∨
          (↯(1/4) ∗ ⌜ one_thread_sampled_zero s1 s2 ⌝) ∨
          (↯(1) (* both_thread_sampled_zero *)) ∨
diff --git a/theories/coneris/examples/hash/con_hash_impl1.v b/theories/coneris/examples/hash/con_hash_impl1.v
index 6a4757cf9..b19661fd0 100644
--- a/theories/coneris/examples/hash/con_hash_impl1.v
+++ b/theories/coneris/examples/hash/con_hash_impl1.v
@@ -24,7 +24,7 @@ Section con_hash_impl1.
 
   
   Definition hash_set_frag v (γ:gname) :=(v ↪[γ]□ ())%I.
-  Definition hash_set s γ:=(ghost_map_auth γ 1 (gset_to_gmap () s) ∗
+  Definition hash_set s γ:=(ghost_map_auth γ (DfracOwn 1) (gset_to_gmap () s) ∗
                               ⌜ ∀ x, x∈s-> (x < S val_size)%nat⌝ ∗
                                      [∗ set] x∈s, hash_set_frag x γ
                              )%I.
diff --git a/theories/coneris/examples/hash/con_hash_impl2.v b/theories/coneris/examples/hash/con_hash_impl2.v
index aa64fa963..6d5e2fe0f 100644
--- a/theories/coneris/examples/hash/con_hash_impl2.v
+++ b/theories/coneris/examples/hash/con_hash_impl2.v
@@ -24,7 +24,7 @@ Section con_hash_impl2.
   
   Definition hash_set_frag v γ_set γ_set' := (hash_set_frag1 v γ_set∗ (v ↪[γ_set'] ()))%I.
   Definition hash_set n γ γ':=
-    (∃ s, ⌜size s = n⌝ ∗ hash_set1 s γ ∗ ghost_map_auth γ' 1 (gset_to_gmap () s))%I.
+    (∃ s, ⌜size s = n⌝ ∗ hash_set1 s γ ∗ ghost_map_auth γ' (DfracOwn 1) (gset_to_gmap () s))%I.
   
   Definition hash_auth m γ1 γ2 γ4 γ5:=
     (hv_auth (L:=Hhv) m γ4 ∗
diff --git a/theories/coneris/examples/hash/con_hash_impl4.v b/theories/coneris/examples/hash/con_hash_impl4.v
index 5c0d1b663..9dfb80877 100644
--- a/theories/coneris/examples/hash/con_hash_impl4.v
+++ b/theories/coneris/examples/hash/con_hash_impl4.v
@@ -124,7 +124,7 @@ Section con_hash_impl.
 
   Definition hashfunI (γs : gname * gname * gname) (val_size : nat) : iProp Σ :=
     ∃ (m : gmap nat (option nat)),
-      ghost_map_auth γs.1.1 1 m ∗
+      ghost_map_auth γs.1.1 (DfracOwn 1) m ∗
       [∗ map] k ↦ o ∈ m,
         ∃ α : loc, k ↪[γs.1.2]□ α ∗
            if o is Some n then α ↪N (val_size; [n]) ∨ k ↪[γs.2]□ n
@@ -140,8 +140,8 @@ Section con_hash_impl.
        ⌜f = compute_hash_specialized #val_size #lvm #ltm ⌝ ∗
        map_list lvm ((λ (n : nat), LitV (LitInt n)) <$> vm) ∗
        map_list ltm ((λ (α : loc), LitV (LitLbl α)) <$> tm) ∗
-       ghost_map_auth γs.1.2 1 tm ∗
-       ghost_map_auth γs.2   1 vm ∗
+       ghost_map_auth γs.1.2 (DfracOwn 1) tm ∗
+       ghost_map_auth γs.2   (DfracOwn 1) vm ∗
        ([∗ map] k ↦ n ∈ vm, k ↪[γs.1.1]□ (Some n)).
 
   Lemma wp_init_hash_state N val_size max :
diff --git a/theories/coneris/examples/hash/hash_view_impl.v b/theories/coneris/examples/hash/hash_view_impl.v
index de58ae4c4..d4d710d53 100644
--- a/theories/coneris/examples/hash/hash_view_impl.v
+++ b/theories/coneris/examples/hash/hash_view_impl.v
@@ -9,7 +9,7 @@ Section hash_view_impl.
   Context `{Hcon:conerisGS Σ,
               HinG: ghost_mapG Σ nat nat}.
   
-  Definition hash_view_auth m γ := (ghost_map_auth γ 1 m ∗
+  Definition hash_view_auth m γ := (ghost_map_auth γ (DfracOwn 1) m ∗
                                    [∗ map] k↦v ∈m, (k ↪[γ]□ v))%I
   .
   Definition hash_view_frag k v γ := (k ↪[γ]□ v)%I.
diff --git a/theories/coneris/examples/lazy_rand/lazy_rand_impl.v b/theories/coneris/examples/lazy_rand/lazy_rand_impl.v
index 9d53540ee..c87b3c3dd 100644
--- a/theories/coneris/examples/lazy_rand/lazy_rand_impl.v
+++ b/theories/coneris/examples/lazy_rand/lazy_rand_impl.v
@@ -69,7 +69,7 @@ Section impl.
     end.
   
   Definition rand_auth (n:option (nat*nat)) γ :=
-    (ghost_map_auth γ 1 (option_to_gmap n) ∗
+    (ghost_map_auth γ (DfracOwn 1) (option_to_gmap n) ∗
      option_duplicate n γ ∗
      ⌜option_valid n⌝)%I.
 
diff --git a/theories/coneris/lib/abstract_tape.v b/theories/coneris/lib/abstract_tape.v
index 4e1e4bf71..b11c254c1 100644
--- a/theories/coneris/lib/abstract_tape.v
+++ b/theories/coneris/lib/abstract_tape.v
@@ -15,7 +15,7 @@ Notation "α ◯↪N ( M ; ns ) @ γ":= (α ↪[ γ ] (M,ns))%I
                                     (at level 20, format "α ◯↪N ( M ; ns ) @ γ") : bi_scope.
 
 #[warning="-notation-incompatible-prefix"]
-Notation "● m @ γ" := (ghost_map_auth γ 1 m) (at level 20) : bi_scope.
+Notation "● m @ γ" := (ghost_map_auth γ (DfracOwn 1) m) (at level 20) : bi_scope.
 
 Section tapes_lemmas.
   Context `{!conerisGS Σ, !abstract_tapesGS Σ}.
diff --git a/theories/coneris/lib/hocap_rand_alt.v b/theories/coneris/lib/hocap_rand_alt.v
index 7ce08a85c..50dbac8e7 100644
--- a/theories/coneris/lib/hocap_rand_alt.v
+++ b/theories/coneris/lib/hocap_rand_alt.v
@@ -117,7 +117,7 @@ Section impl1.
   (* (** Instantiate rand *) *)
   Local Definition rand_inv_pred1  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (tb, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (tb; ns) ))
     )%I.
@@ -241,7 +241,7 @@ Section impl2.
   (** simulating a rand 3 with two flips *)
   Local Definition rand_inv_pred2  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (1, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (1; ns) ))
     )%I.
@@ -442,7 +442,7 @@ Section impl3.
   (* (** Instantiate rand *) *)
   Local Definition rand_inv_pred3  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (S tb, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (S tb; ns) ))
     )%I.
diff --git a/theories/coneris/primitive_laws.v b/theories/coneris/primitive_laws.v
index f45bdf0b5..266e9fde8 100644
--- a/theories/coneris/primitive_laws.v
+++ b/theories/coneris/primitive_laws.v
@@ -34,7 +34,7 @@ Definition tapes_auth `{conerisGS Σ} :=
 
 Global Instance conerisGS_conerisWpGS `{!conerisGS Σ} : conerisWpGS con_prob_lang Σ := {
   conerisWpGS_invGS := conerisGS_invG;
-    state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+    state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
     fork_post := (λ _, True%I);
     err_interp ε := (ec_supply ε);
     
@@ -112,7 +112,7 @@ Section tape_interface.
   Qed.
 
   Lemma tapeN_lookup α N ns m: 
-    tapes_auth 1 m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝.
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝.
   Proof.
     iIntros "? (%&%&?)".
     iDestruct (ghost_map_lookup with "[$][$]") as "%".
@@ -120,7 +120,7 @@ Section tape_interface.
   Qed.
 
   Lemma tapeN_update_append α N ns m (x : fin (S N)):
-    tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]).
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]).
   Proof.
     iIntros "? (%&%&?)".
     iMod (ghost_map_update with "[$][$]") as "[??]".
@@ -129,7 +129,7 @@ Section tape_interface.
   Qed. 
 
   Lemma tapeN_update_append' α N m (ns ns':list (fin (S N))):
-    tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')).
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')).
   Proof.
     iIntros "? (%&%&?)".
     iMod (ghost_map_update with "[$][$]") as "[??]".
diff --git a/theories/diffpriv/examples/report_noisy_max_lemmas.v b/theories/diffpriv/examples/report_noisy_max_lemmas.v
index b06695c51..777755967 100644
--- a/theories/diffpriv/examples/report_noisy_max_lemmas.v
+++ b/theories/diffpriv/examples/report_noisy_max_lemmas.v
@@ -791,12 +791,12 @@ Section coupling_rule.
     length zs' = length xιs ->
     ls = zip (zip xιs.*2 xιs.*1) (replicate (length xιs) []) ->
     ls' =zip (zip xιs'.*2 xιs'.*1) (replicate (length xιs) []) ->
-    tapes_laplace_auth 1 (tapes_laplace σ) -∗
+    tapes_laplace_auth (DfracOwn 1) (tapes_laplace σ) -∗
     spec_tapes_laplace_auth (tapes_laplace σ') -∗
     ([∗ list] '(x, ι);'(x', ι') ∈ xιs;xιs', ι ↪L (num,2 * den,x; []) ∗
             ι' ↪Lₛ (num,2 * den,x'; []) ∗ ⌜(Rabs (IZR (x - x')) <= 1)%R⌝)
     ==∗
-    (tapes_laplace_auth 1 (tapes_laplace (replace_laplace_tape num (2 * den) σ (zip ls zs)))) ∗
+    (tapes_laplace_auth (DfracOwn 1) (tapes_laplace (replace_laplace_tape num (2 * den) σ (zip ls zs)))) ∗
      spec_tapes_laplace_auth (tapes_laplace (replace_laplace_tape num (2 * den) σ' (zip ls' zs'))) ∗
     ([∗ list] k↦'(x, ι);'(x', ι') ∈ xιs;xιs', ι ↪L (num,2 * den,x; [
                                                     zs !!! k]) ∗ ι' ↪Lₛ (num,2 * den,x'; [zs' !!! k]) ∗ ⌜(Rabs (IZR (x - x')) <= 1)%R⌝).
diff --git a/theories/diffpriv/primitive_laws.v b/theories/diffpriv/primitive_laws.v
index 2d4c49b5f..ee21c5632 100644
--- a/theories/diffpriv/primitive_laws.v
+++ b/theories/diffpriv/primitive_laws.v
@@ -60,7 +60,7 @@ Definition add_ec_supply `{diffprivGS Σ} :=
 
 Global Instance diffprivGS_irisGS `{!diffprivGS Σ} : diffprivWpGS prob_lang Σ := {
   diffprivWpGS_invGS := diffprivGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes) ∗ tapes_laplace_auth 1 σ.(tapes_laplace))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes) ∗ tapes_laplace_auth (DfracOwn 1) σ.(tapes_laplace))%I;
   err_interp ε δ := ((mult_ec_supply ε) ∗ (add_ec_supply δ))%I;
 }.
 
diff --git a/theories/elton/examples/generic_group.v b/theories/elton/examples/generic_group.v
index 188e2a1c2..9f7275fa5 100644
--- a/theories/elton/examples/generic_group.v
+++ b/theories/elton/examples/generic_group.v
@@ -574,7 +574,7 @@ Section prog.
           ⌜dom m = set_seq 0 k⌝ ∗
           ⌜map_Forall (λ _ x, base_lit_type_check x = Some BLTInt) m⌝ ∗
           ⌜is_valid_urn (urn_unif s)⌝ ∗
-          mono_nat_auth_own γ2 1 (k-1) ∗
+          mono_nat_auth_own γ2 (DfracOwn 1) (k-1) ∗
           ⌜dom m = dom m'⌝ ∗ 
           ⌜map_Forall (λ _ x, 0<=x.1<p/\0<=x.2<p) m'⌝ ∗
           ⌜map_match m m' l⌝  ∗
@@ -634,8 +634,8 @@ Section prog.
         wp_pures.
 
         
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag1]") as "%".
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag2]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag1]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag2]") as "%".
         assert (n1 ∈ dom m) as Hlookup1.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }
@@ -921,7 +921,7 @@ Section prog.
         wp_pures.
 
         
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag']") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag']") as "%".
         assert (n ∈ dom m) as Hlookup.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }
@@ -1181,8 +1181,8 @@ Section prog.
         iInv "Hinv" as ">(%m&%k&%s'&%m'&Hurn&%Hs&Harr&%&Htries&Hm&%Hdom&%Hforall&%&Hauth&%Hdom'&%Hforall2&%Hmatch&Hor)" "Hclose".
 
         
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag1]") as "%".
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag2]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag1]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag2]") as "%".
         assert (n1 ∈ dom m) as Hlookup1.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }
diff --git a/theories/elton/primitive_laws.v b/theories/elton/primitive_laws.v
index adc32aee5..cf380dd96 100644
--- a/theories/elton/primitive_laws.v
+++ b/theories/elton/primitive_laws.v
@@ -34,7 +34,7 @@ Definition urns_auth `{eltonGS Σ} :=
 
 Global Instance eltonGS_eltonWpGS `{!eltonGS Σ} : eltonWpGS d_prob_lang Σ := {
   eltonWpGS_invGS := eltonGS_invG;
-    state_interp σ := (heap_auth 1 σ.(heap) ∗ urns_auth 1 σ.(urns))%I;
+    state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ urns_auth (DfracOwn 1) σ.(urns))%I;
     err_interp ε := (ec_supply ε);
     
 }.
@@ -111,7 +111,7 @@ Notation "l ↪ v" := (l ↪{ DfracOwn 1 } v)%I
 (*   Qed. *)
 
 (*   Lemma tapeN_lookup α N ns m:  *)
-(*     tapes_auth 1 m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝. *)
+(*     tapes_auth (DfracOwn 1) m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝. *)
 (*   Proof. *)
 (*     iIntros "? (%&%&?)". *)
 (*     iDestruct (ghost_map_lookup with "[$][$]") as "%". *)
@@ -119,7 +119,7 @@ Notation "l ↪ v" := (l ↪{ DfracOwn 1 } v)%I
 (*   Qed. *)
 
 (*   Lemma tapeN_update_append α N ns m (x : fin (S N)): *)
-(*     tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]). *)
+(*     tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]). *)
 (*   Proof. *)
 (*     iIntros "? (%&%&?)". *)
 (*     iMod (ghost_map_update with "[$][$]") as "[??]". *)
@@ -128,7 +128,7 @@ Notation "l ↪ v" := (l ↪{ DfracOwn 1 } v)%I
 (*   Qed.  *)
 
 (*   Lemma tapeN_update_append' α N m (ns ns':list (fin (S N))): *)
-(*     tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')). *)
+(*     tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')). *)
 (*   Proof. *)
 (*     iIntros "? (%&%&?)". *)
 (*     iMod (ghost_map_update with "[$][$]") as "[??]". *)
diff --git a/theories/eris/adequacy.v b/theories/eris/adequacy.v
index b3d71181c..cb92a6342 100644
--- a/theories/eris/adequacy.v
+++ b/theories/eris/adequacy.v
@@ -15,22 +15,42 @@ Import uPred.
 Section adequacy.
   Context `{!erisGS Σ}.
 
-  Lemma step_fupd_fupdN_S n (P : iProp Σ) :  ((|={∅}▷=>^(S n) P) ⊣⊢ (|={∅}=> |={∅}▷=>^(S n) P))%I.
-  Proof. iSplit; iIntros; simpl; iApply fupd_idemp; iFrame. Qed.
+  (** Pure-monotonicity through [▷^k ◇ ⌜·⌝]. *)
+  Local Lemma laterN_except_0_pure_mono k (P Q : Prop) :
+    (P → Q) → ((▷^k ◇ ⌜P⌝ : iProp Σ)%I ⊢ ▷^k ◇ ⌜Q⌝).
+  Proof. intros HPQ. apply bi.laterN_mono, bi.except_0_mono, bi.pure_mono, HPQ. Qed.
+
+  (** Push [∀] through [|={∅}▷=>^n] of plain pure props (via [fupd_finally]). *)
+  Lemma step_fupdN_pure_forall_intro {A} (Φ : A → Prop) n E :
+    (∀ a, |={E|}=> ▷^n ◇ ⌜Φ a⌝) ⊢ |={E|}=> ▷^n ◇ ⌜∀ a, Φ a⌝ : iProp Σ.
+  Proof.
+    iIntros "H".
+    iApply (fupd_finally_mono _ _ (▷^n ◇ ⌜∀ a, Φ a⌝)%I); last first.
+    { iApply fupd_finally_forall. iIntros (a). iApply "H". }
+    rewrite -laterN_forall. apply bi.laterN_mono.
+    rewrite -except_0_forall. apply bi.except_0_mono.
+    apply pure_forall_2.
+  Qed.
 
   Lemma pgl_dbind' `{Countable A, Countable A'}
     (f : A → distr A') (μ : distr A) (R : A → Prop) (T : A' → Prop) ε ε' n :
     ⌜ 0 <= ε ⌝ -∗
     ⌜ 0 <= ε' ⌝ -∗
     ⌜pgl μ R ε⌝ -∗
-    (∀ a , ⌜R a⌝ ={∅}▷=∗^(S n) ⌜pgl (f a) T ε'⌝) -∗
-    |={∅}▷=>^(S n) ⌜pgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
+    (∀ a, ⌜R a⌝ -∗ |={∅|}=> ▷^(S n) ◇ ⌜pgl (f a) T ε'⌝) -∗
+    |={∅|}=> ▷^(S n) ◇ ⌜pgl (dbind f μ) T (ε + ε')⌝.
   Proof.
-    iIntros (???) "H".
-    iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T ε')⌝)).
-    { iIntros (?). iPureIntro. eapply pgl_dbind; eauto. }
-    iIntros (???) "/=".
-    iMod ("H" with "[//]"); auto.
+    iIntros (Hε Hε' Hpgl) "H".
+    iAssert (∀ a, |={∅|}=> ▷^(S n) ◇ ⌜R a → pgl (f a) T ε'⌝)%I with "[H]" as "H".
+    { iIntros (a). destruct (ExcludedMiddle (R a)) as [HR|HnR].
+      - iSpecialize ("H" $! a with "[//]").
+        iApply (fupd_finally_mono with "H").
+        apply (laterN_except_0_pure_mono (S n)). by intros.
+      - iApply fupd_finally_intro. iPureIntro. by intros. }
+    iPoseProof (step_fupdN_pure_forall_intro _ (S n) ∅ with "H") as "H".
+    iApply (fupd_finally_mono with "H").
+    apply (laterN_except_0_pure_mono (S n)). intros Hall.
+    eapply pgl_dbind; eauto.
   Qed.
 
   Lemma pgl_dbind_adv' `{Countable A, Countable A'}
@@ -38,278 +58,354 @@ Section adequacy.
     ⌜ 0 <= ε ⌝ -∗
     ⌜ exists r, forall a, 0 <= ε' a <= r ⌝ -∗
     ⌜pgl μ R ε⌝ -∗
-    (∀ a , ⌜R a⌝ ={∅}▷=∗^(S n) ⌜pgl (f a) T (ε' a)⌝) -∗
-    |={∅}▷=>^(S n) ⌜pgl (dbind f μ) T (ε + SeriesC (λ a : A, (μ a * ε' a)%R))⌝ : iProp Σ.
+    (∀ a, ⌜R a⌝ -∗ |={∅|}=> ▷^(S n) ◇ ⌜pgl (f a) T (ε' a)⌝) -∗
+    |={∅|}=> ▷^(S n) ◇ ⌜pgl (dbind f μ) T (ε + SeriesC (λ a : A, (μ a * ε' a)%R))⌝.
+  Proof.
+    iIntros (Hε [r Hr] Hpgl) "H".
+    iAssert (∀ a, |={∅|}=> ▷^(S n) ◇ ⌜R a → pgl (f a) T (ε' a)⌝)%I with "[H]" as "H".
+    { iIntros (a). destruct (ExcludedMiddle (R a)) as [HR|HnR].
+      - iSpecialize ("H" $! a with "[//]").
+        iApply (fupd_finally_mono with "H").
+        apply (laterN_except_0_pure_mono (S n)). by intros.
+      - iApply fupd_finally_intro. iPureIntro. by intros. }
+    iPoseProof (step_fupdN_pure_forall_intro _ (S n) ∅ with "H") as "H".
+    iApply (fupd_finally_mono with "H").
+    apply (laterN_except_0_pure_mono (S n)). intros Hall.
+    eapply pgl_dbind_adv; [done|exists r; done|done|done].
+  Qed.
+
+  Local Definition cfgO := (prodO exprO stateO).
+
+  (** ** Compatibility shims for the old [|={l; E|}=> ▷^k ◇ P] (hfupd)
+       interface, expressed in terms of the new [fupd_finally] modality
+       [|={E|}=> ▷^k ◇ P].  These keep the call sites below close to their
+       pre-MR-1217 form. *)
+
+  Notation hfupd_mono := fupd_finally_mono (only parsing).
+
+  Lemma hfupd_intro {E} (P : iProp Σ) `{!Plain P} :
+    P -∗ |={E|}=> P.
+  Proof.
+    iIntros "HP".
+    iAssert (■ P)%I with "[HP]" as "#HP'"; [by iApply plain_plainly|].
+    by iApply fupd_finally_intro.
+  Qed.
+
+  Lemma hfupd_intro_pure {E n} (φ : Prop) :
+    φ → ⊢ |={E|}=> ▷^n ◇ ⌜φ⌝ : iProp Σ.
+  Proof.
+    intros Hφ. iApply fupd_finally_intro. by iPureIntro.
+  Qed.
+
+  Lemma laterN_hfupd l {E} k (P : iProp Σ) :
+    ▷^l (|={E|}=> ▷^k ◇ P) ⊢ |={E|}=> ▷^(l + k) ◇ P.
   Proof.
-    iIntros (???) "H".
-    iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T (ε' a))⌝)).
-    { iIntros (?). iPureIntro. eapply pgl_dbind_adv; eauto. }
-    iIntros (???) "/=".
-    iMod ("H" with "[//]"); auto.
+    induction l as [|l IH]; simpl.
+    - iIntros "H". by iApply (fupd_finally_mono with "H").
+    - iIntros "H". rewrite IH. rewrite fupd_finally_later.
+      iApply (fupd_finally_mono with "H"). iIntros "H".
+      by rewrite except_0_laterN except_0_idemp.
   Qed.
 
+  Lemma elim_fupd_hfupd_plain (k l : nat) (E1 E2 : coPset) (P Q : iProp Σ) :
+    l ≤ k →
+    (|={E1, E2}=> P) ∗ (∀ l', ⌜l' = l⌝ -∗ P -∗ |={E2|}=> ▷^(k - l') ◇ Q)
+    ⊢ |={E1|}=> ▷^k ◇ Q.
+  Proof.
+    iIntros (Hlk) "[H1 H2]". iMod "H1" as "HP".
+    iSpecialize ("H2" $! l with "[//] HP").
+    iApply (fupd_finally_mono with "H2").
+    replace k with (l + (k - l))%nat at 2 by lia.
+    rewrite laterN_add. iIntros "H". by iApply laterN_intro.
+  Qed.
+
+  Lemma fupd_plain_hfupd' (l : nat) (E1 E2 : coPset) {P : iProp Σ} `{!Plain P} :
+    (|={E1, E2}=> P) ⊢ |={E1|}=> ▷^l ◇ P.
+  Proof.
+    iIntros "H". iMod "H" as "HP". by iApply hfupd_intro.
+  Qed.
 
+  (** [glm_erasure] in fupd_finally form. *)
   Lemma glm_erasure (e : expr) (σ : state) (n : nat) φ (ε : nonnegreal) :
     to_val e = None →
     glm e σ ε (λ '(e2, σ2) ε',
-        |={∅}▷=>^(S n) ⌜pgl (exec n (e2, σ2)) φ ε'⌝)
-      ⊢ |={∅}▷=>^(S n) ⌜pgl (exec (S n) (e, σ)) φ ε⌝.
+        |={∅|}=> ▷^(S n) ◇ ⌜pgl (exec n (e2, σ2)) φ ε'⌝)
+      ⊢ |={∅|}=> ▷^(S n) ◇ ⌜pgl (exec (S n) (e, σ)) φ ε⌝.
   Proof.
     iIntros (Hv) "Hexec".
     iAssert (⌜to_val e = None⌝)%I as "-#H"; [done|]. iRevert "Hexec H".
     rewrite /glm /glm'.
     set (Φ := (λ '((e1, σ1), ε''),
-                (⌜to_val e1 = None⌝ ={∅}▷=∗^(S n)
-                                              ⌜pgl (exec (S n) (e1, σ1)) φ ε''⌝)%I) :
+                (⌜to_val e1 = None⌝ -∗
+                  |={∅|}=> ▷^(S n) ◇ ⌜pgl (exec (S n) (e1, σ1)) φ ε''⌝)%I) :
            prodO cfgO NNRO → iPropI Σ).
     assert (NonExpansive Φ).
     { intros m ((?&?)&?) ((?&?)&?) [[[=] [=]] [=]]. by simplify_eq. }
     set (F := (glm_pre (λ '(e2, σ2) ε',
-                   |={∅}▷=>^(S n) ⌜pgl (exec n (e2, σ2)) φ ε'⌝)%I)).
+                   |={∅|}=> ▷^(S n) ◇ ⌜pgl (exec n (e2, σ2)) φ ε'⌝)%I)).
     iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
     { iIntros "Hfix %".
-      by iMod ("H" $! ((_, _)) with "Hfix [//]").
-    }
-    clear.
+      by iApply ("H" $! ((_, _)) with "Hfix"). }
+    clear Hv.
     iIntros "!#" ([[e1 σ1] ε'']). rewrite /Φ/F/glm_pre.
-    iIntros " [H | [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & % & %Hlift & H)|H]] %Hv".
+    iIntros " [H | [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & %Hsum & %Hlift & H)|H]] %Hv".
 
-    - iApply step_fupdN_mono.
-      {
-        apply pure_mono.
+    (* Case 1: thin air ε-inflation. Mirrors the original step_fupdN proof,
+       with [hfupd_mono] doing the role of [step_fupdN_mono] and
+       [elim_fupd_hfupd_plain] doing the role of [step_fupd_fupdN_S; iMod ...]. *)
+    - iApply (hfupd_mono _ (▷^(S n) ◇ ⌜∀ ε' : nonnegreal,
+          (ε'' < ε')%R → pgl (exec (S n) (e1, σ1)) φ ε'⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)). intros Hall.
         eapply pgl_epsilon_limit; auto.
-        apply Rle_ge.
-        apply cond_nonneg.
-      }
+        - apply Rle_ge, cond_nonneg.
+        - intros ε' Hε'.
+          apply (Hall (mknonnegreal ε' (Rle_trans _ _ _ (cond_nonneg _) (Rlt_le _ _ Hε'))) Hε'). }
       iIntros (ε' Hε').
-      destruct (decide (ε' < 1)); last first.
-      {
-        iApply step_fupdN_mono.
-        - apply pure_mono.
-          intros ?.
-          apply pgl_1.
-          lra.
-        - iApply step_fupdN_intro; auto.
-      }
-      iApply step_fupd_fupdN_S.
-      iMod ("H" $! (mknonnegreal ε' _) with "[]") as "H".
-      {
-        iPureIntro.
-        simpl in *. simpl.
-        lra.
-      }
-      iDestruct "H" as "[%R' [%ε1' [%ε2' (%Hsum' & %Hlift' & Hwand')]]]".
-      iModIntro.
-      rewrite -(dret_id_left' (fun _ : () => (exec (S n) _)) tt).
-      epose proof (step_fupdN_mono _ _ _ ⌜(pgl _ _ (ε1' + ε2')) ⌝) as h.
-      iApply h.
-      { iIntros "%H'"; iPureIntro. eapply pgl_mon_grading; eauto. }
-      iApply (pgl_dbind').
-      * iPureIntro; apply cond_nonneg.
-      * iPureIntro; apply cond_nonneg.
-      * iPureIntro.
-        apply tgl_implies_pgl in Hlift'.
-        eapply Hlift'.
-      * iIntros (? Hcont).
-        replace tt with a; [| by destruct a].
-        iSpecialize ("Hwand'" with "[]"); [iPureIntro; eauto|].
-        rewrite (dret_id_left').
-        iApply step_fupd_fupdN_S.
-        iMod ("Hwand'" with "[//]"); iModIntro; iFrame.
-        iModIntro; eauto.
-      Unshelve.
-      pose proof (cond_nonneg ε'').
-      simpl in *.
-      lra.
-    - iApply step_fupdN_mono.
-      { apply pure_mono.
-        eapply pgl_mon_grading; eauto. }
-      rewrite exec_Sn_not_final; [|eauto].
+      destruct (decide (ε' < 1)%R) as [Hε'1|Hε'1]; last first.
+      { iApply hfupd_intro. iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro. apply pgl_1. lra. }
+      iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅ _
+        ⌜pgl (exec (S n) (e1, σ1)) φ ε'⌝); [lia|].
+      iSplitL "H"; [iApply ("H" $! ε' with "[//]")|].
+      iIntros (l Hl) "Hst". assert (l = 0%nat) as -> by lia.
+      try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+      iDestruct "Hst" as "(%R' & %ε1' & %ε2' & %Hsum' & %Hlift' & Hwand')".
+      rewrite -(dret_id_left' (λ _ : (), exec (S n) (e1, σ1)) tt).
+      iApply (hfupd_mono _
+        (▷^(S n) ◇ ⌜pgl (dret tt ≫= λ _ : (), exec (S n) (e1, σ1)) φ (ε1' + ε2')⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)).
+        intros Hpgl. eapply pgl_mon_grading; [|exact Hpgl]. exact Hsum'. }
+      iApply (pgl_dbind' _ (dret tt) R' (λ x, φ x) ε1' ε2' n).
+      { iPureIntro. apply cond_nonneg. }
+      { iPureIntro. apply cond_nonneg. }
+      { iPureIntro. apply tgl_implies_pgl, Hlift'. }
+      iIntros (a HRa). destruct a.
+      iSpecialize ("Hwand'" with "[//]").
+      iSpecialize ("Hwand'" with "[//]").
+      rewrite dret_id_left.
+      iApply "Hwand'".
+
+    (* Case 2: prim_step with adv composition. *)
+    - rewrite exec_Sn_not_final; [|by rewrite /is_final /= Hv].
+      iApply (hfupd_mono _ (▷^(S n) ◇ ⌜pgl (prim_step e1 σ1 ≫= exec n) φ
+        (ε1 + SeriesC (λ ρ, (prim_step e1 σ1 ρ) * ε2 ρ))%R⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)). intros Hpgl.
+        eapply pgl_mon_grading; [|exact Hpgl]. done. }
       iApply pgl_dbind_adv'.
-      + iPureIntro; apply cond_nonneg.
-      + iPureIntro. exists r. split; auto. 
-      + done.
-      + iIntros ([] ?).
-        iApply step_fupd_fupdN_S.
-        iMod ("H" $! e s with "[]") as "H";  [iPureIntro; eauto| iModIntro ].
-        iDestruct "H" as "[%R' [%ε1' [%ε2' (%Hsum' & %Hlift' & Hwand')]]]".
-        rewrite -(dret_id_left' (fun _ : () => (exec n (e, s))) tt).
-        epose proof (step_fupdN_mono _ _ _ ⌜(pgl _ _ (ε1' + ε2')) ⌝) as h.
-        iApply h.
-        { iIntros "%H'"; iPureIntro. eapply pgl_mon_grading; eauto. }
-        iApply (pgl_dbind').
-        * iPureIntro; apply cond_nonneg.
-        * iPureIntro; apply cond_nonneg.
-        * iPureIntro.
-          apply tgl_implies_pgl in Hlift'.
-          eapply Hlift'.
-        * iIntros (? Hcont).
-          replace tt with a; [| by destruct a].
-          iSpecialize ("Hwand'" with "[]"); [iPureIntro; eauto|].
-          rewrite (dret_id_left').
-          iApply step_fupd_fupdN_S.
-          iFrame.
-          iModIntro.
-          eauto.
-    - rewrite exec_Sn_not_final; [|eauto].
-      iDestruct (big_orL_mono _ (λ _ _,
-                     |={∅}▷=>^(S n)
-                       ⌜pgl (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
+      { iPureIntro. apply cond_nonneg. }
+      { iPureIntro. exists r. intros a. split; [apply cond_nonneg | apply Hr]. }
+      { done. }
+      iIntros ([e' σ'] HRes).
+      iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅ _
+        ⌜pgl (exec n (e', σ')) φ (ε2 (e', σ'))⌝); [lia|].
+      iSplitL "H"; [iApply ("H" with "[//]")|].
+      iIntros (l Hl) "Hst". assert (l = 0%nat) as -> by lia.
+      try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+      iDestruct "Hst" as "(%R' & %ε1' & %ε2' & %Hsum' & %Hlift' & Hwand')".
+      rewrite -(dret_id_left' (λ _ : (), exec n (e', σ')) tt).
+      iApply (hfupd_mono _ (▷^(S n) ◇
+        ⌜pgl (dret tt ≫= λ _ : (), exec n (e', σ')) φ (ε1' + ε2')⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)).
+        intros Hpgl. eapply pgl_mon_grading; [|exact Hpgl]. exact Hsum'. }
+      iApply (pgl_dbind' _ (dret tt) R' (λ x, φ x) ε1' ε2' n).
+      { iPureIntro. apply cond_nonneg. }
+      { iPureIntro. apply cond_nonneg. }
+      { iPureIntro. apply tgl_implies_pgl, Hlift'. }
+      iIntros (a HRa). destruct a.
+      iSpecialize ("Hwand'" with "[//]").
+      rewrite dret_id_left.
+      iApply "Hwand'".
+
+    (* Case 3: state_step with adv composition. eris has tapes, so [get_active]
+       can be non-empty. We pick a tape α and erase the [state_step] step into the
+       outer execution via [prim_coupl_step_prim]. *)
+    - iDestruct (big_orL_mono _ (λ _ _,
+                     |={∅|}=> ▷^(S n)
+                       ◇ ⌜pgl (exec (S n) (e1, σ1)) φ ε''⌝)%I
                   with "H") as "H".
       { iIntros (i α Hα%list_elem_of_lookup_2) "(% & %ε1 & %ε2 & %Hε'' & %Hleq & %Hlift & H)".
-        replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
-        rewrite -exec_Sn_not_final; [|eauto].
-        iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 , R2 σ2 → pgl (exec (S n) (e1, σ2)) φ (ε2 (e1, σ2))⌝)%I).
-        - iIntros (?). iPureIntro.
+        iApply (hfupd_mono _ (▷^(S n) ◇
+          ⌜∀ σ2, R2 σ2 → pgl (exec (S n) (e1, σ2)) φ (ε2 (e1, σ2))⌝)%I).
+        { apply (laterN_except_0_pure_mono (S n)). intros Hall.
           rewrite /= /get_active in Hα.
           apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
           erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
           apply (pgl_mon_grading _ _
-                   (ε1 + (SeriesC (λ ρ : language.state prob_lang, language.state_step σ1 α ρ * ε2 (e1, ρ))))) => //.
+                   (ε1 + (SeriesC (λ ρ : language.state prob_lang,
+                              language.state_step σ1 α ρ * ε2 (e1, ρ))))) => //.
           eapply pgl_dbind_adv; eauto; [by destruct ε1|].
           destruct Hε'' as [r Hr]; exists r.
-          intros a.
-          split; [by destruct (ε2 _) | by apply Hr].
-        - iIntros (e s).
-          iApply step_fupd_fupdN_S.
-          iMod ("H" with "[//]") as "H"; iModIntro.
-          iDestruct "H" as "[%R' [%ε1' [%ε2' (%Hsum' & %Hlift' & Hwand')]]]".
-          rewrite -(dret_id_left' (fun _ : () => (exec (S n) _)) tt).
-          epose proof (step_fupdN_mono _ _ _ ⌜(pgl _ _ (ε1' + ε2')) ⌝) as h.
-          iApply h.
-          { iIntros "%H'"; iPureIntro. eapply pgl_mon_grading; eauto. }
-          iApply (pgl_dbind').
-          * iPureIntro; apply cond_nonneg.
-          * iPureIntro; apply cond_nonneg.
-          * iPureIntro.
-            apply tgl_implies_pgl in Hlift'.
-            eapply Hlift'.
-          * iIntros (? Hcont).
-            replace tt with a; [| by destruct a].
-            iSpecialize ("Hwand'" with "[]"); [iPureIntro; eauto|].
-            rewrite (dret_id_left').
-            iApply step_fupd_fupdN_S.
-            iMod ("Hwand'" with "[//]"); iModIntro; iFrame.
-            iModIntro; eauto. }
+          intros a. split; [by destruct (ε2 _) | by apply Hr]. }
+        iIntros (σ2 HR2).
+        iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅ _
+          ⌜pgl (exec (S n) (e1, σ2)) φ (ε2 (e1, σ2))⌝); [lia|].
+        iSplitL "H".
+        { iApply ("H" $! σ2 with "[//]"). }
+        iIntros (l Hl) "Hst". assert (l = 0%nat) as -> by lia.
+        try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+        iDestruct "Hst" as "(%R' & %ε1' & %ε2' & %Hsum' & %Hlift' & Hwand')".
+        rewrite -(dret_id_left' (λ _ : (), exec (S n) (e1, σ2)) tt).
+        iApply (hfupd_mono _ (▷^(S n) ◇
+          ⌜pgl (dret tt ≫= λ _ : (), exec (S n) (e1, σ2)) φ (ε1' + ε2')⌝)%I).
+        { apply (laterN_except_0_pure_mono (S n)).
+          intros Hpgl. eapply pgl_mon_grading; [|exact Hpgl]. exact Hsum'. }
+        iApply (pgl_dbind' _ (dret tt) R' (λ x, φ x) ε1' ε2' n).
+        { iPureIntro. apply cond_nonneg. }
+        { iPureIntro. apply cond_nonneg. }
+        { iPureIntro. apply tgl_implies_pgl, Hlift'. }
+        iIntros (a HRa). destruct a.
+        iSpecialize ("Hwand'" with "[//]").
+        iSpecialize ("Hwand'" with "[//]").
+        rewrite dret_id_left.
+        iApply "Hwand'". }
       iInduction (language.get_active σ1) as [| α] "IH"; [done|].
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
+      Unshelve.
+       
   Qed.
 
-  Theorem wp_refRcoupl_step_fupdN (ε : nonnegreal) (e : expr) (σ : state) n φ :
-    state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
-    |={⊤,∅}=> |={∅}▷=>^n ⌜pgl (exec n (e, σ)) φ ε⌝.
+  Theorem wp_refRcoupl_hfupd k (ε : nonnegreal) (e : expr) (σ : state) n φ :
+    (∀ m, num_laters_per_step m = 0%nat) →
+    £ n ∗ state_interp k σ ∗ err_interp ε ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+    |={⊤|}=> ▷^n ◇ ⌜pgl (exec n (e, σ)) φ ε⌝.
   Proof.
-    iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
+    iIntros (Hnls).
+    iInduction n as [|n] "IH" forall (k e σ ε); iIntros "(Hlc & Hσ & Hε & Hwp)".
     - rewrite /exec /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
-        rewrite pgl_wp_value_fupd.
-        iMod "Hwp" as "%".
-        iApply fupd_mask_intro; [set_solver|]; iIntros.
+        rewrite pgl_wp_value_fupd'.
+        iApply (fupd_plain_hfupd' 0 ⊤ ⊤).
+        iMod "Hwp" as "%". iModIntro.
         iPureIntro.
-        apply (pgl_mon_grading _ _ 0); [apply cond_nonneg | ].
+        apply (pgl_mon_grading _ _ 0); [apply cond_nonneg|].
         apply pgl_dret; auto.
-      + iApply fupd_mask_intro; [set_solver|]; iIntros "_".
-        iPureIntro.
-        apply pgl_dzero,
-        Rle_ge,
-        cond_nonneg.
-    - rewrite exec_Sn /step_or_final /=.
-      destruct (to_val e) eqn:Heq.
+      + iApply hfupd_intro. simpl.
+        rewrite /bi_except_0. iRight.
+        iPureIntro. apply pgl_dzero, Rle_ge, cond_nonneg.
+    - destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
-        rewrite pgl_wp_value_fupd.
-        iMod "Hwp" as "%".
-        iApply fupd_mask_intro; [set_solver|]; iIntros "_".
-        iApply step_fupdN_intro; [done|]. do 4 iModIntro.
-        iPureIntro.
-        rewrite exec_unfold dret_id_left /=.
-        apply (pgl_mon_grading _ _ 0); [apply cond_nonneg | ].
+        rewrite pgl_wp_value_fupd'.
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ⊤ ⌜φ v⌝
+          ⌜pgl (exec (S n) (of_val v, σ)) φ ε⌝); [lia|].
+        iSplitL "Hwp"; [iApply "Hwp"|].
+        iIntros (l Hl) "Hpure". assert (l = 0%nat) as -> by lia.
+        iApply hfupd_intro.
+        iDestruct "Hpure" as %Hφv.
+        iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro.
+        erewrite exec_is_final; [|by simpl].
+        apply (pgl_mon_grading _ _ 0); [apply cond_nonneg|].
         apply pgl_dret; auto.
       + rewrite pgl_wp_unfold /pgl_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "Hlift".
-        iModIntro.
+        iSpecialize ("Hwp" $! k with "[$Hσ $Hε]").
+        iDestruct (lc_succ with "Hlc") as "[Hcred Hlc]".
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ∅ _
+          ⌜pgl (prim_step e σ ≫= exec n) φ ε⌝
+          with "[$Hwp Hcred Hlc]"); first lia.
+        iIntros (l Hl) "Hlift". assert (l = 0%nat) as -> by lia.
+        try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
         iPoseProof
-          (glm_mono _ (λ '(e2, σ2) ε', |={∅}▷=>^(S n)
-             ⌜pgl (exec n (e2, σ2)) φ ε'⌝)%I
-            with "[%] [] Hlift") as "H".
+          (glm_mono _ (λ '(e2, σ2) ε2, |={∅|}=> ▷^(S n)
+             ◇ ⌜pgl (exec n (e2, σ2)) φ ε2⌝)%I
+            with "[%] [Hcred Hlc] Hlift") as "H".
         { apply Rle_refl. }
-        { iIntros ([] ?) "H !> !>".
-          iMod "H" as "(Hstate & Herr_auth & Hwp)".
-          iMod ("IH" with "[$]") as "H".
-          iModIntro. done. }
-        assert ((prim_step e σ) = (step (e, σ))) as h => //.
-        rewrite h. clear h.
-        rewrite -exec_Sn_not_final; [|eauto].
+        { iIntros ([e' σ'] ε') "H".
+          (* The instance gives [num_laters_per_step _ := 0]; Coq has
+             already reduced [S (num_laters_per_step k)] to [1], so [H]
+             is [£1 -∗ |={∅,∅}=> ▷ |={∅,∅}=> |={∅,⊤}=> ...]. *)
+          iSpecialize ("H" with "Hcred").
+          iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅
+            (▷ |={∅,∅}=> |={∅,⊤}=>
+                (state_interp (S k) σ' ∗ err_interp ε' ∗
+                   WP e' {{ v, ⌜φ v⌝ }}))%I
+            ⌜pgl (exec n (e', σ')) φ ε'⌝); first lia.
+          iSplitL "H"; [iApply "H"|].
+          iIntros (l' Hl') "H". assert (l' = 0%nat) as -> by lia.
+          try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+          iApply (laterN_hfupd 1). iNext.
+          iApply (elim_fupd_hfupd_plain n 0 ∅ ⊤
+            (state_interp (S k) σ' ∗ err_interp ε' ∗ WP e' {{ v, ⌜φ v⌝ }})%I
+            ⌜pgl (exec n (e', σ')) φ ε'⌝); first lia.
+          iSplitL "H".
+          { iMod "H". iMod "H". iModIntro. iExact "H". }
+          iIntros (l'' Hl'') "(Hσ' & Hε' & Hwp')".
+          assert (l'' = 0%nat) as -> by lia.
+          try rewrite Nat.add_0_r; replace (n - 0)%nat with n by lia.
+          iApply ("IH" $! (S k) with "[$Hlc $Hσ' $Hε' $Hwp']"). }
+        replace (prim_step e σ) with (step (e, σ)) by reflexivity.
+        rewrite -exec_Sn_not_final; last by rewrite /is_final /to_final /= Heq.
         by iApply (glm_erasure with "H").
   Qed.
 
-  (** safety *)
+  (** [glm_erasure_safety] in hfupd form: erases a [glm] derivation about safety
+      mass into a single hfupd-wrapped pure mass-bound. *)
   Lemma glm_erasure_safety (e : expr) (σ : state) (n : nat) (ε : nonnegreal) :
     to_val e = None →
     glm e σ ε (λ '(e2, σ2) ε',
-                     |={∅}▷=>^(S n) ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)
-    ⊢ |={∅}▷=>^(S n) ⌜SeriesC (iterM (S n) prim_step_or_val (e, σ)) >= 1 - ε⌝.
+        |={∅|}=> ▷^(S n) ◇ ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)
+      ⊢ |={∅|}=> ▷^(S n) ◇
+          ⌜SeriesC (iterM (S n) prim_step_or_val (e, σ)) >= 1 - ε⌝.
   Proof.
     iIntros (Hv) "Hexec".
     iAssert (⌜to_val e = None⌝)%I as "-#H"; [done|]. iRevert "Hexec H".
-    rewrite /glm/glm'.
+    rewrite /glm /glm'.
     set (Φ := (λ '((e1, σ1), ε''),
-                (⌜to_val e1 = None⌝ ={∅}▷=∗^(S n)
-                 ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε''⌝)%I) :
+                (⌜to_val e1 = None⌝ -∗
+                 |={∅|}=> ▷^(S n) ◇
+                   ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε''⌝)%I) :
            prodO cfgO NNRO → iPropI Σ).
     assert (NonExpansive Φ).
     { intros m ((?&?)&?) ((?&?)&?) [[[=] [=]] [=]]. by simplify_eq. }
     set (F := (glm_pre (λ '(e2, σ2) ε',
-                   |={∅}▷=>^(S n) ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)%I)).
+                   |={∅|}=> ▷^(S n) ◇
+                     ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)%I)).
     iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
     { iIntros "Hfix %".
-      iMod ("H" $! ((_, _)) with "Hfix [//]"). done.
-    }
-    clear.
+      by iApply ("H" $! ((_, _)) with "Hfix"). }
+    clear Hv.
     iIntros "!#" ([[e1 σ1] ε'']). rewrite /Φ/F/glm_pre.
-    iIntros " [ H | [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & % & %Hlift & H)|H]] %Hv".
-    - iApply (step_fupdN_mono _ _ _ (⌜∀ ε', ε'' < ε'  -> SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε'⌝ )).
-      {
-        apply pure_mono.
-        intros ?.
-        apply Rle_ge.
-        apply real_le_limit.
-        intros ε Hε.
-        apply Rge_le.
-        replace (1 - ε'' - ε) with (1 - (ε'' + ε)) by lra.
-        apply H.
-        lra.
-      }
+    iIntros " [ H | [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & %Hsum & %Hlift & H)|H]] %Hv".
+    - iApply (hfupd_mono _ (▷^(S n) ◇
+          ⌜∀ ε' : nonnegreal, (ε'' < ε')%R →
+            SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε'⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)). intros Hall.
+        apply Rle_ge, real_le_limit. intros δ Hδ.
+        apply Rge_le. replace (1 - ε'' - δ) with (1 - (ε'' + δ)) by lra.
+        destruct ε'' as [ε'' Hε''nn]. simpl in *.
+        assert (0 <= ε'' + δ)%R as Hsum_nn by lra.
+        specialize (Hall (mknonnegreal (ε'' + δ) Hsum_nn)).
+        simpl in Hall. apply Hall. lra. }
       iIntros (ε' Hε').
-      iMod ("H" $! (mknonnegreal ε' _) with "[]") as "H".
-      {
-        iPureIntro.
-        simpl in *. simpl.
-        lra.
-      }
-      iApply step_fupd_fupdN_S.
-      iDestruct (exec_stutter_compat_1 with "[][$]") as "[%H'|H2]".
-      { iIntros (???) "H %".
-        iDestruct ("H" with "[//]") as "H".
-        iApply step_fupdN_mono; last done.
-        iPureIntro. intros. trans (1-ε); try lra.
-        simpl. lra. }
-        + iApply step_fupdN_intro; first done.
-          iPureIntro.
-          trans 0; last first.
-          * simpl. apply Rle_ge. apply Rle_minus. done.
-          * apply Rle_ge; auto.
-        + iDestruct ("H2" with "[//]") as "H2". done.
-    Unshelve.
-    pose proof (cond_nonneg ε'').
-    simpl in *.
-    lra.
-    - iApply (step_fupdN_mono _ _ _ (⌜∀ ρ, R ρ -> SeriesC (iterM n prim_step_or_val ρ) >= 1 - (ε2 ρ)⌝)).
-      { apply pure_mono.
-        intros H1.
+      iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅
+        (exec_stutter (λ ε0 : nonnegreal, (⌜to_val e1 = None⌝ -∗
+          |={∅|}=> ▷^(S n) ◇
+            ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε0⌝)%I) ε')
+        ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε'⌝); [lia|].
+      iSplitL "H"; [iApply ("H" $! ε' with "[//]")|].
+      iIntros (l Hl) "Hexecs".
+      assert (l = 0%nat) as -> by lia.
+      try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+      iDestruct (exec_stutter_compat_1 _ _ with "[] Hexecs") as "[%H'|H2]".
+      { iIntros (εa εb Hle) "H %Hto".
+        iSpecialize ("H" with "[//]").
+        iApply (hfupd_mono _ _ with "H").
+        apply (laterN_except_0_pure_mono (S n)). intros Hge.
+        apply Rle_ge. eapply Rle_trans; [|by apply Rge_le].
+        apply Rplus_le_compat_l, Ropp_le_contravar. exact Hle. }
+      + iApply hfupd_intro. iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro.
+        apply Rle_ge. trans 0%R.
+        { destruct ε' as [? ?]; simpl in *. lra. }
+        apply SeriesC_ge_0'. intros; auto.
+      + iApply ("H2" with "[//]").
+
+    (* Case 2: prim_step *)
+    - iApply (hfupd_mono _ (▷^(S n) ◇
+        ⌜∀ ρ, R ρ → SeriesC (iterM n prim_step_or_val ρ) >= 1 - (ε2 ρ)⌝)%I).
+      { apply (laterN_except_0_pure_mono (S n)). intros Hall.
         apply Rle_ge.
         simpl.
         rewrite /dbind/dbind_pmf{1}/pmf.
@@ -325,8 +421,7 @@ Section adequacy.
           rewrite !Rcomplements.Rle_minus_l.
           replace 1 with (SeriesC (prim_step e1 σ1)); last first.
           { eapply mixin_prim_step_mass; last auto.
-            apply ectx_lang_mixin.
-          }
+            apply ectx_lang_mixin. }
           assert (ex_seriesC (λ a : language.cfg prob_lang, prim_step e1 σ1 a * SeriesC (iterM n prim_step_or_val a))).
           { apply pmf_ex_seriesC_mult_fn. naive_solver. }
           assert (ex_seriesC (λ ρ : expr * state, prim_step e1 σ1 ρ * ε2 ρ) ).
@@ -347,31 +442,41 @@ Section adequacy.
             apply Rge_le. naive_solver.
           + apply Rle_plus_r; first done.
             apply Rplus_le_le_0_compat; first real_solver.
-            apply Rmult_le_pos; auto.
-      }
-      iIntros ([e s] ?).
-      iMod ("H" with "[//]") as "H".
-      iDestruct (exec_stutter_compat_1 with "[][$]") as "[%H'|H]".
-      { iIntros.
-        iApply step_fupdN_mono; last done.
-        iPureIntro. intros. trans (1-ε); try lra.
-        simpl. lra. }
-      + iApply step_fupdN_intro; first done.
-        iPureIntro.
-        trans 0; last (simpl in *; lra).
-        apply Rle_ge.
-        auto.
-      + done.
+            apply Rmult_le_pos; auto. }
+      iIntros ([e' σ'] HR).
+      iSpecialize ("H" $! e' σ' with "[//]").
+      iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅
+        (exec_stutter (λ ε0 : nonnegreal,
+          (|={∅|}=> ▷^(S n) ◇
+            ⌜SeriesC (iterM n prim_step_or_val (e', σ')) >= 1 - ε0⌝)%I)
+          (ε2 (e', σ')))
+        ⌜SeriesC (iterM n prim_step_or_val (e', σ')) >= 1 - (ε2 (e', σ'))⌝); [lia|].
+      iSplitL "H"; [iApply "H"|].
+      iIntros (l Hl) "Hst". assert (l = 0%nat) as -> by lia.
+      try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+      iDestruct (exec_stutter_compat_1 _ _ with "[] Hst") as "[%H'|H2]".
+      { iIntros (εa εb Hle) "H".
+        iApply (hfupd_mono _ _ with "H").
+        apply (laterN_except_0_pure_mono (S n)). intros Hge.
+        apply Rle_ge. eapply Rle_trans; [|by apply Rge_le].
+        apply Rplus_le_compat_l, Ropp_le_contravar. exact Hle. }
+      + iApply hfupd_intro. iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro.
+        apply Rle_ge. trans 0%R.
+        { destruct (ε2 (e', σ')) as [? ?]; simpl in *. lra. }
+        apply SeriesC_ge_0'. intros; auto.
+      + iApply "H2".
+
+    (* Case 3: state_step *)
     - iDestruct (big_orL_mono _ (λ _ _,
-                     |={∅}▷=>^(S n)
+                     |={∅|}=> ▷^(S n) ◇
                        ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) >= 1 - ε''⌝)%I
                   with "H") as "H".
       { iIntros (i α Hα%list_elem_of_lookup_2) "(% & %ε1 & %ε2 & %Hε'' & %Hleq & %Hlift & H)".
-        iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 , R2 σ2 → SeriesC (iterM (S n) prim_step_or_val (e1, σ2)) >= 1 - (ε2 (e1, σ2))⌝)%I).
-        {
-          iPureIntro.
-          intros H.
+        iApply (hfupd_mono _ (▷^(S n) ◇
+          ⌜∀ σ2, R2 σ2 →
+            SeriesC (iterM (S n) prim_step_or_val (e1, σ2)) >= 1 - (ε2 (e1, σ2))⌝)%I).
+        { apply (laterN_except_0_pure_mono (S n)). intros Hall.
           assert (SeriesC (iterM (S n) prim_step_or_val (e1, σ1)) =
                   SeriesC (state_step σ1 α ≫= λ σ1', iterM (S n) prim_step_or_val (e1, σ1'))) as ->.
           { erewrite (SeriesC_ext _ (pexec (S n) (e1, σ1))); last first.
@@ -382,8 +487,7 @@ Section adequacy.
             eapply Rcoupl_mass_eq.
             rewrite /=/get_active elem_of_elements elem_of_dom in Hα.
             destruct Hα as [??].
-            by eapply pexec_coupl_step_pexec.
-          }
+            by eapply pexec_coupl_step_pexec. }
           simpl. apply Rle_ge.
           setoid_rewrite prim_step_or_val_no_val; last done.
           simpl. simpl in *.
@@ -402,8 +506,7 @@ Section adequacy.
           rewrite !Rcomplements.Rle_minus_l.
           replace 1 with (SeriesC (state_step σ1 α)); last first.
           { apply state_step_mass. rewrite /get_active in Hα.
-            rewrite elem_of_elements in Hα. done.
-          }
+            rewrite elem_of_elements in Hα. done. }
           assert (ex_seriesC (λ a : state, state_step σ1 α a * SeriesC (prim_step e1 a ≫= iterM n prim_step_or_val)) ).
           { apply pmf_ex_seriesC_mult_fn. exists 1. intros; auto. }
           eassert (ex_seriesC (λ σ2 : state, state_step σ1 α σ2 * ε2 (e1, σ2))).
@@ -418,117 +521,110 @@ Section adequacy.
           case_bool_decide; simpl.
           - rewrite -Rmult_plus_distr_l.
             cut (state_step σ1 α x *1 <=
-  state_step σ1 α x * (SeriesC (prim_step e1 x ≫= iterM n prim_step_or_val) + ε2 (e1, x))).
+                  state_step σ1 α x * (SeriesC (prim_step e1 x ≫= iterM n prim_step_or_val) + ε2 (e1, x))).
             { rewrite Rmult_1_r. rewrite Rplus_0_r. intros; done. }
             apply Rmult_le_compat_l; auto.
             rewrite -Rcomplements.Rle_minus_l.
             apply Rge_le. simpl.
-            setoid_rewrite prim_step_or_val_no_val in H; last auto.
-            apply H. naive_solver.
+            setoid_rewrite prim_step_or_val_no_val in Hall; last auto.
+            apply Hall. naive_solver.
           - apply Rle_plus_r; first done.
             apply Rplus_le_le_0_compat; first real_solver.
-            apply Rmult_le_pos; auto.
-        }
-        iIntros (e s).
-        iApply step_fupd_fupdN_S.
-        iMod ("H" with "[//]") as "H"; iModIntro.
-        iDestruct (exec_stutter_compat_1 with "[][$]") as "[%H'|H]".
-        { iIntros (???) "H %".
-          iDestruct ("H" with "[//]") as "H".
-          iApply step_fupdN_mono; last done.
-          iPureIntro. intros. trans (1-ε); try lra.
-          simpl. lra. }
-        + iApply step_fupdN_intro; first done.
-          iPureIntro.
-          trans 0; last first.
-          * simpl. apply Rle_ge. apply Rle_minus. done.
-          * apply Rle_ge; auto.
-        + iDestruct ("H" with "[//]") as "H". done.
-      }
+            apply Rmult_le_pos; auto. }
+        iIntros (σ2 HR2).
+        iSpecialize ("H" $! σ2 with "[//]").
+        iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅
+          (exec_stutter (λ ε0 : nonnegreal,
+            (⌜to_val e1 = None⌝ -∗
+             |={∅|}=> ▷^(S n) ◇
+               ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ2)) >= 1 - ε0⌝)%I)
+            (ε2 (e1, σ2)))
+          ⌜SeriesC (iterM (S n) prim_step_or_val (e1, σ2)) >= 1 - (ε2 (e1, σ2))⌝); [lia|].
+        iSplitL "H"; [iApply "H"|].
+        iIntros (l Hl) "Hst". assert (l = 0%nat) as -> by lia.
+        try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+        iDestruct (exec_stutter_compat_1 _ _ with "[] Hst") as "[%H'|H2]".
+        { iIntros (εa εb Hle) "H %Hto".
+          iSpecialize ("H" with "[//]").
+          iApply (hfupd_mono _ _ with "H").
+          apply (laterN_except_0_pure_mono (S n)). intros Hge.
+          apply Rle_ge. eapply Rle_trans; [|by apply Rge_le].
+          apply Rplus_le_compat_l, Ropp_le_contravar. exact Hle. }
+        + iApply hfupd_intro. iApply laterN_intro.
+          rewrite /bi_except_0. iRight. iPureIntro.
+          apply Rle_ge. trans 0%R.
+          { destruct (ε2 (e1, σ2)) as [? ?]; simpl in *. lra. }
+          apply SeriesC_ge_0'. intros; auto.
+        + iApply ("H2" with "[//]"). }
       iInduction (language.get_active σ1) as [| α] "IH"; [done|].
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
   Qed.
 
-  Theorem wp_safety_fupdN (ε : nonnegreal) (e : expr) (σ : state) n φ  :
-    state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
-    |={⊤,∅}=> |={∅}▷=>^n ⌜SeriesC (pexec n (e, σ)) >= 1 - ε⌝.
+  Theorem wp_safety_hfupd k (ε : nonnegreal) (e : expr) (σ : state) n φ :
+    (∀ m, num_laters_per_step m = 0%nat) →
+    £ n ∗ state_interp k σ ∗ err_interp ε ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+    |={⊤|}=> ▷^n ◇ ⌜SeriesC (pexec n (e, σ)) >= 1 - ε⌝.
   Proof.
-    iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
-    - rewrite /=.
-      iApply fupd_mask_intro; [set_solver|]; iIntros.
-      iPureIntro.
+    iIntros (Hnls).
+    iInduction n as [|n] "IH" forall (k e σ ε); iIntros "(Hlc & Hσ & Hε & Hwp)".
+    - iApply hfupd_intro. simpl.
+      rewrite /bi_except_0. iRight. iPureIntro.
       trans 1; last first.
       { pose proof cond_nonneg ε. lra. }
       apply Rle_ge. rewrite dret_mass. done.
     - destruct (to_val e) eqn:Heq.
-      + simpl.
-        rewrite /dbind/dbind_pmf{2}/pmf/=.
-        apply of_to_val in Heq as <-.
-        rewrite pgl_wp_value_fupd.
-        iMod "Hwp" as "%".
-        iApply fupd_mask_intro; [set_solver|]; iIntros "_".
-        iApply step_fupdN_intro; [done|]. do 4 iModIntro.
-        iPureIntro.
-        apply Rle_ge. trans 1.
-        { pose proof cond_nonneg ε. lra. }
-        erewrite SeriesC_ext; last first.
-        { intros. setoid_rewrite prim_step_or_val_is_val; last done.
-          done.
-        }
-        erewrite (SeriesC_ext _ (λ n0, if bool_decide (n0 = (of_val v, σ)) then 1 else 0)); last first.
-        * intros []. case_bool_decide as H0.
-          -- simplify_eq. etrans; last eapply (SeriesC_singleton' (of_val v, σ)).
-             apply SeriesC_ext.
-             intros. case_bool_decide.
-             ++ subst. rewrite dret_1_1; last done.
-                rewrite Rmult_1_l.
-                induction n; simpl.
-                ** rewrite dret_1_1; [lra|done].
-                ** rewrite /dbind/dbind_pmf{1}/pmf/=.
-                   etrans; last eapply (SeriesC_singleton' (of_val v, σ)).
-                   apply SeriesC_ext.
-                   intros. case_bool_decide; subst; simpl.
-                   --- rewrite IHn. rewrite step_or_final_is_final; first rewrite dret_1_1; [lra|done|].
-                       rewrite /is_final. simpl. done.
-                   --- simpl. rewrite step_or_final_is_final; last by rewrite /is_final.
-                       rewrite dret_0; last done. lra.
-             ++ rewrite dret_0; last done. lra.
-          -- apply SeriesC_0.
-             intros.
-             rewrite /dret/dret_pmf{1}/pmf.
-             case_bool_decide; subst; last lra.
-             rewrite Rmult_1_l.
-             revert e s v σ H H0.
-             induction n.
-             ++ simpl. intros. rewrite dret_0; done.
-             ++ intros. simpl. rewrite /dbind/dbind_pmf{1}/pmf/=.
-                apply SeriesC_0.
-                intros. destruct (decide (x = (of_val v, σ))).
-                ** subst. rewrite IHn; try done. lra.
-                ** rewrite step_or_final_is_final; last by rewrite /is_final.
-                   rewrite dret_0; last done.
-                   lra.
-        * rewrite SeriesC_singleton. lra.
+      + apply of_to_val in Heq as <-.
+        rewrite pgl_wp_value_fupd'.
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ⊤ ⌜φ v⌝
+          ⌜SeriesC (pexec (S n) (of_val v, σ)) >= 1 - ε⌝); [lia|].
+        iSplitL "Hwp"; [iApply "Hwp"|].
+        iIntros (l Hl) "_". assert (l = 0%nat) as -> by lia.
+        iApply hfupd_intro.
+        iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro.
+        erewrite pexec_is_final; last by rewrite /is_final /to_final /=; eexists.
+        rewrite dret_mass.
+        destruct ε as [ε ?]; simpl in *. apply Rle_ge. lra.
       + rewrite pgl_wp_unfold /pgl_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "Hlift".
-        iModIntro.
+        iSpecialize ("Hwp" $! k with "[$Hσ $Hε]").
+        iDestruct (lc_succ with "Hlc") as "[Hcred Hlc]".
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ∅ _
+          ⌜SeriesC (iterM (S n) prim_step_or_val (e, σ)) >= 1 - ε⌝
+          with "[$Hwp Hcred Hlc]"); first lia.
+        iIntros (l Hl) "Hlift". assert (l = 0%nat) as -> by lia.
+        try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
         iPoseProof
-          (glm_mono _ (λ '(e2, σ2) ε', |={∅}▷=>^(S n)
-             ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)%I
-            with "[%] [] Hlift") as "H".
+          (glm_mono _ (λ '(e2, σ2) ε2, |={∅|}=> ▷^(S n) ◇
+             ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε2⌝)%I
+            with "[%] [Hcred Hlc] Hlift") as "H".
         { apply Rle_refl. }
-        { iIntros ([] ?) "H !> !>".
-          iMod "H" as "(Hstate & Herr_auth & Hwp)".
-          iMod ("IH" with "[$]") as "H".
-          iModIntro. done. }
+        { iIntros ([e' σ'] ε') "H".
+          iSpecialize ("H" with "Hcred").
+          iApply (elim_fupd_hfupd_plain (S n) 0 ∅ ∅
+            (▷ |={∅,∅}=> |={∅,⊤}=>
+                (state_interp (S k) σ' ∗ err_interp ε' ∗
+                   WP e' {{ v, ⌜φ v⌝ }}))%I
+            ⌜SeriesC (iterM n prim_step_or_val (e', σ')) >= 1 - ε'⌝); first lia.
+          iSplitL "H"; [iApply "H"|].
+          iIntros (l' Hl') "H". assert (l' = 0%nat) as -> by lia.
+          try rewrite Nat.add_0_r; replace (S n - 0)%nat with (S n) by lia.
+          iApply (laterN_hfupd 1). iNext.
+          iApply (elim_fupd_hfupd_plain n 0 ∅ ⊤
+            (state_interp (S k) σ' ∗ err_interp ε' ∗ WP e' {{ v, ⌜φ v⌝ }})%I
+            ⌜SeriesC (iterM n prim_step_or_val (e', σ')) >= 1 - ε'⌝); first lia.
+          iSplitL "H".
+          { iMod "H". iMod "H". iModIntro. iExact "H". }
+          iIntros (l'' Hl'') "(Hσ' & Hε' & Hwp')".
+          assert (l'' = 0%nat) as -> by lia.
+          try rewrite Nat.add_0_r; replace (n - 0)%nat with n by lia.
+          iApply ("IH" $! (S k) with "[$Hlc $Hσ' $Hε' $Hwp']"). }
         by iApply (glm_erasure_safety with "H").
   Qed.
 
 End adequacy.
 
-
 Class erisGpreS Σ := ErisGpreS {
   erisGpreS_iris  :: invGpreS Σ;
   erisGpreS_heap  :: ghost_mapG Σ loc val;
@@ -549,29 +645,26 @@ Theorem wp_pgl Σ `{erisGpreS Σ} (e : expr) (σ : state) n (ε : R) φ :
   pgl (exec n (e, σ)) φ ε.
 Proof.
   intros Hε Hwp.
-  eapply pure_soundness, (step_fupdN_soundness_no_lc _ n 0).
-  iIntros (Hinv) "_".
-  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
-  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
-  (* Handle the trivial 1 <= ε case *)
+  apply (pure_soundness (PROP:=iPropI Σ)).
+  apply (laterN_soundness _ (S n)).
+  rewrite laterN_later -except_0_into_later.
   destruct (decide (ε < 1)) as [Hcr|Hcr]; last first.
-  { iClear "Hh Ht".
-    iApply (fupd_mask_intro); [eauto|].
-    iIntros "_".
-    iApply step_fupdN_intro; [eauto|].
-    iApply laterN_intro; iPureIntro.
+  { iApply laterN_intro. iApply except_0_intro. iPureIntro.
     apply not_Rlt, Rge_le in Hcr.
-    rewrite /pgl; intros.
-    eapply Rle_trans; [eapply prob_le_1|done]. }
+    rewrite /pgl. intros. eapply Rle_trans; [apply prob_le_1|done]. }
+  apply (fupd_finally_soundness HasLc n ⊤).
+  iIntros (Hinv) "Hlc".
+  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
+  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
   set ε' := mknonnegreal _ Hε.
-  iMod (ec_alloc ε') as (?) "[? ?]"; [done|].
+  iMod (ec_alloc ε') as (Hec) "[Hs Hf]"; [done|].
   set (HclutchGS := HeapG Σ _ _ _ γH γT _).
-  epose proof (wp_refRcoupl_step_fupdN ε') as h.
-  iApply h.
-  iFrame.
-  iApply Hwp.
-  done.
-  Unshelve. apply _.
+  change ε with (nonneg ε').
+  iPoseProof (wp_refRcoupl_hfupd O ε' e σ n φ (λ _, eq_refl)
+                with "[Hlc Hs Hh Ht Hf]") as "H".
+  { iFrame "Hlc Hs". rewrite /state_interp /=. iFrame "Hh Ht".
+    iApply Hwp. iApply "Hf". }
+  iApply "H".
 Qed.
 
 Lemma pgl_closed_lim (e : expr) (σ : state) (ε : R) φ :
@@ -615,27 +708,28 @@ Theorem wp_safety Σ `{erisGpreS Σ} (e : expr) (σ : state) (ε : R) φ n:
   SeriesC (pexec n (e, σ)) >= 1 - ε.
 Proof.
   intros Hε Hwp.
-  eapply pure_soundness, (step_fupdN_soundness_no_lc _ n 0).
-  iIntros (Hinv) "_".
-  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
-  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
-  (* Handle the trivial 1 <= ε case *)
+  apply (pure_soundness (PROP:=iPropI Σ)).
+  apply (laterN_soundness _ (S n)).
+  rewrite laterN_later -except_0_into_later.
   destruct (decide (ε < 1)) as [Hcr|Hcr]; last first.
-  { iClear "Hh Ht".
-    iApply (fupd_mask_intro); [eauto|].
-    iIntros "_".
-    iApply step_fupdN_intro; [eauto|].
-    iApply laterN_intro; iPureIntro.
+  { iApply laterN_intro. iApply except_0_intro. iPureIntro.
     apply not_Rlt, Rge_le in Hcr.
-    trans 0.
-    - apply Rle_ge. apply SeriesC_ge_0'. intros. auto.
-    - simpl. lra. }
+    trans 0%R; last first.
+    { lra. }
+    apply Rle_ge, SeriesC_ge_0'. intros. auto. }
+  apply (fupd_finally_soundness HasLc n ⊤).
+  iIntros (Hinv) "Hlc".
+  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
+  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
   set ε' := mknonnegreal _ Hε.
-  iMod (ec_alloc ε') as (?) "[? ?]"; [done|].
+  iMod (ec_alloc ε') as (Hec) "[Hs Hf]"; [done|].
   set (HclutchGS := HeapG Σ _ _ _ γH γT _).
-  epose proof (wp_safety_fupdN ε') as h. iApply h. iFrame.
-  iApply Hwp. done.
-  Unshelve. apply _.
+  change ε with (nonneg ε').
+  iPoseProof (wp_safety_hfupd O ε' e σ n φ (λ _, eq_refl)
+                with "[Hlc Hs Hh Ht Hf]") as "H".
+  { iFrame "Hlc Hs". rewrite /state_interp /=. iFrame "Hh Ht".
+    iApply Hwp. iApply "Hf". }
+  iApply "H".
 Qed.
 
 Lemma pexec_safety_relate (e:expr) σ n:
diff --git a/theories/eris/ectx_lifting.v b/theories/eris/ectx_lifting.v
index fe27a1657..a2931b4de 100644
--- a/theories/eris/ectx_lifting.v
+++ b/theories/eris/ectx_lifting.v
@@ -17,28 +17,30 @@ Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd_couple {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1 ε1,
-    state_interp σ1 ∗ err_interp ε1
+  (∀ n σ1 ε1,
+    state_interp n σ1 ∗ err_interp ε1
     ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-      ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
+      £ (S (num_laters_per_step n))
+      ={∅}▷=∗^(S (num_laters_per_step n)) |={∅,E}=>
+      state_interp (S n) σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "Hσε".
+  iIntros (n σ1 ε) "Hσε".
   iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto.
 Qed.
 
 Lemma wp_lift_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ n σ1, state_interp n σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }})
+      state_interp (S n) σ2 ∗ WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by eapply head_prim_reducible. }
@@ -47,15 +49,15 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {E1 E2 Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ n σ1, state_interp n σ1 ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E1}[E2]▷=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (n σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iIntros (e2 σ2 Hstep).
@@ -64,15 +66,15 @@ Qed.
 
 Lemma wp_lift_atomic_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ n σ1, state_interp n σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (n σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iNext. iIntros (e2 σ2 Hstep).
diff --git a/theories/eris/error_rules.v b/theories/eris/error_rules.v
index de4bc9085..cc26b2111 100644
--- a/theories/eris/error_rules.v
+++ b/theories/eris/error_rules.v
@@ -179,7 +179,7 @@ Proof.
     intros; apply Hleq.
   }
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε_now) "[Hσ Hε]".
+  iIntros (k σ1 ε_now) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iApply glm_adv_comp; simpl.
@@ -430,7 +430,7 @@ Proof.
   iIntros (-> Hleq Hε1 Ψ) "Herr HΨ".
   destruct (fin_function_bounded _ ε2) as [r Hε2].
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε_now) "[Hσ Hε]".
+  iIntros (k σ1 ε_now) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iApply glm_adv_comp; simpl.
@@ -739,7 +739,7 @@ Lemma twp_rand_err_fin (N : nat) (z : Z) (m : fin (S N)) E Φ s :
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(?&?& -> & He).
@@ -815,7 +815,7 @@ Proof.
   iIntros (Heq) "[Herr Hwp]".
   rewrite Heq.
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr ") as %(?&?&->&He).
@@ -886,7 +886,7 @@ Lemma twp_err_incr e ε s E Φ :
   Proof.
     iIntros (?) "[Herr Hwp]".
     iApply twp_lift_step_fupd_glm; [done|].
-    iIntros (σ1 ε2) "[Hσ1 Hε2]".
+    iIntros (k σ1 ε2) "[Hσ1 Hε2]".
     iApply fupd_mask_intro; [set_solver|].
     iIntros "Hclose'".
     iApply glm_err_incr_step.
@@ -915,7 +915,7 @@ Lemma twp_err_incr e ε s E Φ :
     rewrite !tgl_wp_unfold /tgl_wp_pre /=.
     rewrite H.
     iMod ("Hclose'").
-    iMod ("Hwp" with "[$]").
+    iMod ("Hwp" $! k with "[$]").
     by iApply exec_stutter_free.
   Qed.
 
@@ -928,7 +928,7 @@ Lemma twp_err_incr e ε s E Φ :
   Proof.
     iIntros (?) "[Herr Hwp]".
     iApply wp_lift_step_fupd_glm; [done|].
-    iIntros (σ1 ε2) "[Hσ1 Hε2]".
+    iIntros (k σ1 ε2) "[Hσ1 Hε2]".
     iApply fupd_mask_intro; [set_solver|].
     iIntros "Hclose'".
     iApply glm_err_incr_step.
@@ -957,7 +957,7 @@ Lemma twp_err_incr e ε s E Φ :
     rewrite !pgl_wp_unfold /pgl_wp_pre /=.
     rewrite H.
     iMod ("Hclose'").
-    iMod ("Hwp" with "[$]").
+    iMod ("Hwp" $! k with "[$]").
     by iApply exec_stutter_free.
 Qed.
 
@@ -996,7 +996,7 @@ Proof.
   iIntros (H) "[Herr Hwp]".
   rewrite H.
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr ") as %(?&?&->&He).
@@ -1061,7 +1061,7 @@ Lemma twp_rand_err_list_int_fin (N : nat) (z : Z) (zs : list Z) E Φ :
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr ") as %(?&?&->&He).
@@ -1116,7 +1116,7 @@ Proof.
   iIntros (Heq) "[Herr Hwp]".
   rewrite Heq.
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(?&?&->&He).
@@ -1179,7 +1179,7 @@ Lemma twp_rand_err_list_nat_fin (N : nat) (z : Z) (ns : list nat) E Φ :
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (k σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(?&?&->&He).
diff --git a/theories/eris/lifting.v b/theories/eris/lifting.v
index 7eb7b1add..daebcdfef 100644
--- a/theories/eris/lifting.v
+++ b/theories/eris/lifting.v
@@ -18,11 +18,13 @@ Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step_fupd_glm E Φ e1 s :
   to_val e1 = None →
-  (∀ σ1 ε1,
-    state_interp σ1 ∗ err_interp ε1
+  (∀ n σ1 ε1,
+    state_interp n σ1 ∗ err_interp ε1
     ={E,∅}=∗
     glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-      ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
+      £ (S (num_laters_per_step n))
+      ={∅}▷=∗^(S (num_laters_per_step n)) |={∅,E}=>
+      state_interp (S n) σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   by rewrite pgl_wp_unfold /pgl_wp_pre =>->.
@@ -32,49 +34,47 @@ Qed.
 
 Lemma wp_lift_step_fupd E Φ e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1
+  (∀ n σ1, state_interp n σ1
      ={E,∅}=∗
     ⌜reducible (e1, σ1)⌝ ∗
      ∀ e2 σ2,
       ⌜prim_step e1 σ1 (e2, σ2) > 0 ⌝ ={∅}=∗ ▷ |={∅,E}=>
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }})
+      state_interp (S n) σ2 ∗ WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H".
   iApply wp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (n σ1 ε) "[Hσ Hε]".
   iMod ("H" with "Hσ") as "[%Hs H]". iModIntro.
   iApply (glm_prim_step e1 σ1).
-  iExists _.
-  iExists nnreal_zero.
-  iExists ε.
-  iSplit.
-  { iPureIntro. simpl. done. }
-  iSplit.
-  { iPureIntro. simpl. lra. }
+  iExists _, nnreal_zero, ε.
+  iSplit; [done|].
+  iSplit; [iPureIntro; simpl; lra|].
   iSplit.
-  { iPureIntro.
-    eapply pgl_pos_R, pgl_trivial.
-    simpl; lra.
-  }
+  { iPureIntro. eapply pgl_pos_R, pgl_trivial. simpl; lra. }
   iIntros (e2 σ2 (?&?)).
-  iMod ("H" with "[//]")as "H".
-  iIntros "!> !>".
-  by iMod "H" as "[$ $]".
+  iMod ("H" with "[//]") as "H".
+  iModIntro. iIntros "_".
+  (* H : ▷ |={∅,E}=> state_interp (S n) σ2 ∗ wp E e2 Φ *)
+  (* Goal: |={∅}▷=>^(S (num_laters_per_step n))
+            (|={∅,E}=> state_interp (S n) σ2 ∗ err_interp ε ∗ wp E e2 Φ) *)
+  iApply (step_fupdN_le 1 (S (num_laters_per_step n))); [lia|done|].
+  iApply step_fupdN_intro; [done|]. simpl.
+  iNext. iMod "H" as "[Hσ' Hwp]". iModIntro. iFrame.
 Qed.
 
 (** Derived lifting lemmas. *)
 Lemma wp_lift_step E Φ e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ n σ1, state_interp n σ1 ={E,∅}=∗
     ⌜reducible (e1, σ1)⌝ ∗
     ▷ ∀ e2 σ2,
      ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (n ?) "Hσ".
   iMod ("H" with "Hσ") as "[$ H]". iIntros "!>" (???) "!>!>" . by iApply "H".
 Qed.
 
@@ -86,29 +86,32 @@ Lemma wp_lift_pure_step `{!Inhabited (state Λ)} E E' Φ e1 s :
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { by eapply (to_final_None_1 (e1, inhabitant)), reducible_not_final. }
-  iIntros (σ1) "Hσ". iMod "H".
+  iIntros (n σ1) "Hσ". iMod "H".
   iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
   iSplit; [done|].
   iNext. iIntros (e2 σ2 Hprim).
   destruct (Hstep _ _ _ Hprim).
   iMod "Hclose" as "_". iMod "H".
-  iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
+  iDestruct ("H" with "[//]") as "H".
+  iMod (fupd_mask_subseteq ∅) as "Hclo"; first by set_solver+.
+  iMod (state_interp_mono with "[$]") as "$".
+  simpl. by iFrame.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can *)
 (* use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {E1 E2 Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ n σ1, state_interp n σ1 ={E1}=∗
     ⌜reducible (e1, σ1)⌝ ∗
     ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E1}[E2]▷=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H".
-  iApply (wp_lift_step_fupd E1 _ e1)=>//; iIntros (σ1) "Hσ1".
-  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
+  iApply (wp_lift_step_fupd E1 _ e1)=>//; iIntros (n σ1) "Hσ1".
+  iMod ("H" $! n σ1 with "Hσ1") as "[$ H]".
   iApply fupd_mask_intro; first set_solver.
   iIntros "Hclose" (e2 σ2 Hs). iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 with "[#]") as "H"; [done|].
@@ -120,15 +123,15 @@ Qed.
 
 Lemma wp_lift_atomic_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ n σ1, state_interp n σ1 ={E}=∗
          ⌜reducible (e1, σ1)⌝ ∗
          ▷ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
-                    state_interp σ2 ∗
+                    state_interp (S n) σ2 ∗
                     from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]".
+  iIntros (n ?) "?". iMod ("H" with "[$]") as "[$ H]".
   iIntros "!> *". iIntros (Hstep) "!> !>".
   by iApply "H".
 Qed.
diff --git a/theories/eris/presample_rules.v b/theories/eris/presample_rules.v
index 186edd742..f56284300 100644
--- a/theories/eris/presample_rules.v
+++ b/theories/eris/presample_rules.v
@@ -54,7 +54,7 @@ Section rules.
   Proof.
     iIntros (He) "(H𝛼&Hwp)".
     iApply twp_lift_step_fupd_glm; [done|].
-    iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
+    iIntros (k 𝜎 ε) "((Hheap&Htapes)&Hε)".
     iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
     replace ε with (nnreal_zero + ε)%NNR by (apply nnreal_ext; simpl; lra).
@@ -70,7 +70,7 @@ Section rules.
     iMod "Hclose'" as "_".
     iSpecialize ("Hwp" $! n with "H𝛼").
     rewrite !tgl_wp_unfold /tgl_wp_pre /= He.
-    iSpecialize ("Hwp" $! 𝜎' ε).
+    iSpecialize ("Hwp" $! k 𝜎' ε).
     iMod ("Hwp" with "[Hheap Htapes Hε]") as "Hwp".
     { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
       rewrite H𝜎'.
@@ -87,7 +87,7 @@ Section rules.
   Proof.
     iIntros (He) "(>H𝛼&Hwp)".
     iApply wp_lift_step_fupd_glm; [done|].
-    iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
+    iIntros (k 𝜎 ε) "((Hheap&Htapes)&Hε)".
     iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
     replace ε with (nnreal_zero + ε)%NNR by (apply nnreal_ext; simpl; lra).
@@ -103,7 +103,7 @@ Section rules.
     iMod "Hclose'" as "_".
     iSpecialize ("Hwp" $! n with "H𝛼").
     rewrite !pgl_wp_unfold /pgl_wp_pre /= He.
-    iSpecialize ("Hwp" $! 𝜎' ε).
+    iSpecialize ("Hwp" $! k 𝜎' ε).
     iMod ("Hwp" with "[Hheap Htapes Hε]") as "Hwp".
     { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
       rewrite H𝜎'.
@@ -129,7 +129,7 @@ Section rules.
       transitivity (ε2 0%fin); auto.
     }
     iApply twp_lift_step_fupd_glm; [done|].
-    iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
+    iIntros (k σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
     iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
     iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub.
 
@@ -285,7 +285,7 @@ Section rules.
     remember {| heap := heap2; tapes := tapes2 |} as σ2.
     rewrite Hσ_red.
     iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
-    iSpecialize ("Hwp" $! σ2 _).
+    iSpecialize ("Hwp" $! k σ2 _).
     iSpecialize ("Hwp" with "[Hheap Htapes Hε_supply]").
     { iSplitL "Hheap Htapes".
       - rewrite /tapes_auth.
@@ -315,7 +315,7 @@ Section rules.
       transitivity (ε2 0%fin); auto.
     }
     iApply wp_lift_step_fupd_glm; [done|].
-    iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
+    iIntros (k σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
     iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
     iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub.
     iMod (ec_supply_decrease with "Hε_supply Hε") as (ε1' ε_rem -> Hε1') "Hε_supply".
@@ -460,7 +460,7 @@ Section rules.
     remember {| heap := heap2; tapes := tapes2 |} as σ2.
     rewrite /= Hσ_red /=.
     iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
-    iSpecialize ("Hwp" $! σ2 _).
+    iSpecialize ("Hwp" $! k σ2 _).
     iSpecialize ("Hwp" with "[Hheap Htapes Hε_supply]").
     { iSplitL "Hheap Htapes".
       - rewrite /tapes_auth.
@@ -585,7 +585,7 @@ Section rules.
   Proof.
     iIntros (H1 H2) "He".
     iApply wp_lift_step_fupd_glm; first done.
-    iIntros (σ1 ε) "[Hσ Hε]".
+    iIntros (k σ1 ε) "[Hσ Hε]".
     iApply fupd_mask_intro; [set_solver|].
     iIntros "Hclose'".
     iDestruct (ec_supply_bound with "Hε He ") as %Hle.
diff --git a/theories/eris/primitive_laws.v b/theories/eris/primitive_laws.v
index b67cf0960..be2c34a88 100644
--- a/theories/eris/primitive_laws.v
+++ b/theories/eris/primitive_laws.v
@@ -10,7 +10,7 @@ From clutch.prob_lang Require Import tactics lang notation.
 From iris.prelude Require Import options.
 
 Class erisGS Σ := HeapG {
-  erisGS_invG : invGS_gen HasNoLc Σ;
+  erisGS_invG : invGS_gen HasLc Σ;
   (* CMRA for the state *)
   erisGS_heap : ghost_mapG Σ loc val;
   erisGS_tapes : ghost_mapG Σ loc tape;
@@ -32,11 +32,13 @@ Definition tapes_auth `{erisGS Σ} :=
   @ghost_map_auth _ _ _ _ _ erisGS_tapes erisGS_tapes_name.
 
 
-Global Instance erisGS_erisWpGS `{!erisGS Σ} : erisWpGS prob_lang Σ := {
+Program Global Instance erisGS_erisWpGS `{!erisGS Σ} : erisWpGS prob_lang Σ := {
   erisWpGS_invGS := erisGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp _ σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
   err_interp ε := (ec_supply ε);
+  num_laters_per_step _ := 0;
 }.
+Next Obligation. auto. Qed.
 
 (** Heap *)
 Notation "l ↦{ dq } v" := (@ghost_map_elem _ _ _ _ _ erisGS_heap erisGS_heap_name l dq v)
@@ -89,7 +91,7 @@ Lemma wp_alloc E v s :
 Proof.
   iIntros (Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   solve_red.
   iIntros "!> /=" (e2 σ2 Hs); inv_head_step.
   iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]".
@@ -109,7 +111,7 @@ Lemma wp_allocN_seq (N : nat) (z : Z) E v s:
 Proof.
   iIntros (-> Hn Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iSplit.
   { iPureIntro.
     rewrite /head_reducible.
@@ -161,7 +163,7 @@ Lemma wp_load E l dq v s :
 Proof.
   iIntros (Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iDestruct (ghost_map_lookup with "Hh Hl") as %?.
   solve_red.
   iIntros "!> /=" (e2 σ2 Hs); inv_head_step.
@@ -174,7 +176,7 @@ Lemma wp_store E l v' v s :
 Proof.
   iIntros (Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iDestruct (ghost_map_lookup with "Hh Hl") as %?.
   solve_red.
   iIntros "!> /=" (e2 σ2 Hs); inv_head_step.
@@ -188,7 +190,7 @@ Lemma wp_rand (N : nat) (z : Z) E s :
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "Hσ !#".
+  iIntros (n σ1) "Hσ !#".
   solve_red.
   iIntros "!>" (e2 σ2 Hs).
   inv_head_step.
@@ -218,7 +220,7 @@ Lemma wp_alloc_tape N z E s :
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !# /=".
+  iIntros (n σ1) "(Hh & Ht) !# /=".
   solve_red.
   iIntros "!>" (e2 σ2 Hs); inv_head_step.
   iMod (ghost_map_insert (fresh_loc σ1.(tapes)) with "Ht") as "[$ Hl]".
@@ -233,7 +235,7 @@ Lemma wp_rand_tape N α n ns z E s :
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n' σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros "!>" (e2 σ2 Hs).
@@ -249,7 +251,7 @@ Lemma wp_rand_tape_empty N z α E s :
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros "!>" (e2 σ2 Hs).
@@ -265,7 +267,7 @@ Lemma wp_rand_tape_wrong_bound N M z α E ns s :
 Proof.
   iIntros (-> ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros "!>" (e2 σ2 Hs).
diff --git a/theories/eris/total_adequacy.v b/theories/eris/total_adequacy.v
index 6ebffce30..5eafe24a2 100644
--- a/theories/eris/total_adequacy.v
+++ b/theories/eris/total_adequacy.v
@@ -249,40 +249,48 @@ Qed.
 Section adequacy.
   Context `{!erisGS Σ}.
 
+  (** Helper: lift a pure-monotone implication through [◇ ⌜·⌝]. *)
+  Local Lemma except_0_pure_mono_iprop (P Q : Prop) :
+    (P → Q) → ((◇ ⌜P⌝ : iProp Σ) ⊢ ◇ ⌜Q⌝).
+  Proof. intros HPQ. apply bi.except_0_mono, bi.pure_mono, HPQ. Qed.
+
   Lemma tgl_dbind' `{Countable A, Countable A'}
     (f : A → distr A') (μ : distr A) (R : A → Prop) (T : A' → Prop) ε ε':
     ⌜ 0 <= ε ⌝ -∗
     ⌜ 0 <= ε'⌝ -∗
     ⌜tgl μ R ε⌝ -∗
-    (∀ a , ⌜R a⌝ -∗ |={∅}=> ⌜tgl (f a) T ε'⌝) -∗
-    |={∅}=> ⌜tgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
+    (∀ a , ⌜R a⌝ -∗ |={∅|}=> ◇ ⌜tgl (f a) T ε'⌝) -∗
+    |={∅|}=> ◇ ⌜tgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
   Proof.
-    iIntros (???) "H".
-    iApply (fupd_mono _ _ (⌜(∀ a b, R a → tgl (f a) T ε')⌝)).
-    { iIntros (?). iPureIntro. eapply tgl_dbind; eauto. }
-    iIntros (???) "/=".
-    iMod ("H" with "[//]"); auto.
+    iIntros (Hε Hε' HR) "H".
+    iApply (fupd_finally_mono _ (◇ ⌜∀ a, R a → tgl (f a) T ε'⌝)%I).
+    { apply except_0_pure_mono_iprop. intros Hall.
+      eapply tgl_dbind; eauto. }
+    iIntros (a HRa). iApply ("H" with "[//]").
   Qed.
 
-
-  Theorem twp_step_fupd_tgl (e : expr) (σ : state) (ε : nonnegreal) φ  :
-    state_interp σ ∗ err_interp (ε) ∗ WP e [{ v, ⌜φ v⌝ }] ⊢
-    |={⊤,∅}=> ⌜tgl (lim_exec (e, σ)) φ ε⌝.
+  Theorem twp_step_fupd_tgl k (e : expr) (σ : state) (ε : nonnegreal) φ  :
+    state_interp k σ ∗ err_interp (ε) ∗ WP e [{ v, ⌜φ v⌝ }] ⊢
+    |={⊤|}=> ◇ ⌜tgl (lim_exec (e, σ)) φ ε⌝.
   Proof.
     iIntros "(Hstate & Herr & Htwp)".
-    iRevert (σ ε) "Hstate Herr".
-    pose proof (tgl_wp_ind_simple ⊤ () (λ e, ∀ (a : state) (a0 : nonnegreal),
-                                  state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜tgl (lim_exec (e, a)) φ a0⌝)%I) as H. iApply H.
+    iRevert (k σ ε) "Hstate Herr".
+    pose proof (tgl_wp_ind_simple ⊤ () (λ e, ∀ (k : nat) (a : state) (a0 : nonnegreal),
+                                  state_interp k a -∗ err_interp a0 -∗
+                                  |={⊤|}=> ◇ ⌜tgl (lim_exec (e, a)) φ a0⌝)%I) as H.
+    iApply H.
     2: { destruct twp_default. done. }
     clear H e.
     iModIntro.
     iIntros (e) "H".
-    iIntros (σ ε) "Hs Hec".
+    iIntros (k σ ε) "Hs Hec".
     rewrite /tgl_wp_pre.
     case_match.
-    - iMod "H" as "%".
-      iApply fupd_mask_intro; first done. iIntros "_".
-      iPureIntro.
+    - iApply (elim_fupd_hfupd_plain 0 0 ⊤ ⊤ ⌜φ v⌝
+        ⌜tgl (lim_exec (e, σ)) φ ε⌝); [lia|].
+      iSplitL "H"; [iApply "H"|].
+      iIntros (l Hl) "%Hφ". assert (l = 0%nat) as -> by lia.
+      iApply hfupd_intro. rewrite /bi_except_0. iRight. iPureIntro.
       rewrite /tgl/prob.
       etrans.
       2:{ eapply SeriesC_ge_elem; last apply ex_seriesC_filter_bool_pos; try done.
@@ -291,76 +299,115 @@ Section adequacy.
       { simpl. rewrite H. rewrite dret_1_1; last done. destruct ε. simpl.
         case_bool_decide; try lra. done. }
       simpl. rewrite H. by rewrite dret_mass.
-    - iSpecialize ("H" $! σ ε with "[$]").
-      iMod "H".
+    - iSpecialize ("H" $! k σ ε with "[$]").
+      iApply (elim_fupd_hfupd_plain 0 0 ⊤ ∅ _
+        ⌜tgl (lim_exec (e, σ)) φ ε⌝ with "[$H]"); first lia.
+      iIntros (l Hl) "Hglm". assert (l = 0%nat) as -> by lia.
       iRevert (H).
-      iApply (glm_strong_ind (λ e σ ε, ⌜language.to_val e = None⌝ ={∅}=∗  ⌜tgl (lim_exec (e, σ)) φ ε⌝)%I with "[][$H]").
+      iApply (glm_strong_ind
+        (λ e σ ε, ⌜language.to_val e = None⌝ -∗
+                  |={∅|}=> ◇ ⌜tgl (lim_exec (e, σ)) φ ε⌝)%I
+        with "[][$Hglm]").
       iModIntro. clear e σ ε. iIntros (e σ ε) "H %Hval".
       iDestruct "H" as "[H|[H | H]]".
-      + iAssert (|={∅}=>  ⌜∀ ε' : nonnegreal,
-                             (ε < ε') -> tgl (lim_exec (e, σ)) φ ε'⌝)%I with "[H]" as "H".
-        {
-          iIntros (ε') "%Hε'".
-          iMod ("H" $! ε' (Hε')) as "H".
-          iDestruct "H" as "(%R' & %ε1' & %ε2' & %Hineq' & %Hub' & H)".
-          iApply fupd_mono.
-          { iApply pure_mono. intros. eapply tgl_mon_grading; [eapply Hineq'|eauto]. }
-          rewrite -{2}(dret_id_left' (fun _ : () => (lim_exec (e, σ))) tt).
-          iApply tgl_dbind'.
-          - iPureIntro; apply cond_nonneg.
-          - iPureIntro; apply cond_nonneg.
-          - iPureIntro; eapply Hub'.
-          - iIntros. destruct a.
-            iSpecialize ("H" with "[//]").
-            iDestruct "H" as "[H _]".
-            iApply ("H" with "[//]").
-        }
-        iApply fupd_mono; [|done].
-        apply pure_mono.
-        intro H.
-        apply tgl_epsilon_limit; [apply Rle_ge, cond_nonneg|].
-        intros ε' Hε'.
-        eapply (H (mknonnegreal ε' _)); eauto.
-        Unshelve.
-        apply Rgt_lt in Hε'.
-        etrans; [|left;eauto].
-        apply cond_nonneg.
+      + iApply (fupd_finally_mono _ (◇ ⌜∀ ε' : nonnegreal,
+            (ε < ε') → tgl (lim_exec (e, σ)) φ ε'⌝)%I).
+        { iIntros "Hgoal". iStopProof.
+          apply except_0_pure_mono_iprop.
+          intros Hall.
+          apply tgl_epsilon_limit; [apply Rle_ge, cond_nonneg|].
+          intros ε' Hε'.
+          assert (0 <= ε')%R as Hε'nn.
+          { apply Rgt_lt in Hε'. etrans; [|left; eauto]. apply cond_nonneg. }
+          eapply (Hall (mknonnegreal ε' Hε'nn)). simpl. lra. }
+        rewrite bi.pure_forall except_0_forall.
+        iApply fupd_finally_forall. iIntros (ε').
+        destruct (decide (ε < ε')%R) as [Hε'|Hε']; last first.
+        { iApply hfupd_intro. rewrite /bi_except_0. iRight.
+          iPureIntro. intros. done. }
+        iSpecialize ("H" $! ε' with "[//]").
+        iApply (elim_fupd_hfupd_plain 0 0 ∅ ∅
+          (exec_stutter
+             (λ ε'' : nonnegreal,
+                ((⌜language.to_val e = None⌝ ={∅|}=∗
+                  ◇ ⌜tgl (lim_exec (e, σ)) φ ε''⌝) ∧
+                 glm e σ ε''
+                   (λ '(e2, σ2) (ε2 : nonnegreal),
+                      |={∅,⊤}=> state_interp (S k) σ2 ∗ err_interp ε2 ∗
+                        ∀ (k0 : nat) (a : state) (a0 : nonnegreal),
+                          state_interp k0 a -∗ err_interp a0 ={⊤|}=∗
+                          ◇ ⌜tgl (lim_exec (e2, a)) φ a0⌝))%I)
+             ε')
+          ⌜ε < ε' → tgl (lim_exec (e, σ)) φ ε'⌝); [lia|].
+        iSplitL "H"; [iApply "H"|].
+        iIntros (l' Hl') "Hst". assert (l' = 0%nat) as -> by lia.
+        iDestruct (exec_stutter_compat_1 _ _ with "[] Hst") as "[%H'|H2]".
+        { iIntros (εa εb Hle) "H". iSplit.
+          - iDestruct "H" as "[H _]". iIntros "%Hto". iSpecialize ("H" with "[//]").
+            iApply (fupd_finally_mono _ _ with "H").
+            apply except_0_pure_mono_iprop.
+            intros Hge. eapply tgl_mon_grading; eauto.
+          - iDestruct "H" as "[_ H]".
+            iApply (glm_mono_grading with "[%] H"). exact Hle. }
+        2: { iDestruct "H2" as "[H2 _]". iSpecialize ("H2" with "[//]").
+          iApply (fupd_finally_mono _ _ with "H2").
+          apply except_0_pure_mono_iprop. intros; auto. }
+        iApply hfupd_intro. iApply laterN_intro.
+        rewrite /bi_except_0. iRight. iPureIntro.
+        intros _. rewrite /tgl. intros.
+        eapply Rle_trans; [|apply prob_ge_0]. lra.
       + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)".
         rewrite lim_exec_step step_or_final_no_final.
         2: { by apply reducible_not_final. }
         iAssert (∀ ρ2 : language.expr prob_lang * language.state prob_lang,
-          ⌜R ρ2⌝ ={∅}=∗
-          let
-          '(e2, σ2) := ρ2 in
-          |={∅}=>  ⌜tgl (lim_exec (e2, σ2)) φ (ε2 ρ2)⌝)%I with "[H]" as "H".
-        { iIntros (ρ2) "%Hρ2". destruct (ρ2) as (e2&σ2). iMod ("H" $! e2 σ2 Hρ2) as "H".
-          rewrite /exec_stutter.
-          iDestruct "H" as (R2 ε1' ε2' Hineq' Htotal_ub) "H".
-          iModIntro.
-          iApply (fupd_mono _ _ (⌜tgl (lim_exec (e2, σ2)) φ (ε1' + ε2')⌝)%I).
-          { iPureIntro. apply tgl_mon_grading, Hineq'. }
-          rewrite -(dret_id_left' (fun _ : () => (lim_exec (e2, σ2))) tt).
-          iApply tgl_dbind'.
-          (* Fix the weakening for the first two goals *)
-          * iPureIntro. apply cond_nonneg.
-          * iPureIntro. apply cond_nonneg.
-          * iPureIntro. eapply Htotal_ub.
-          * iIntros ([] ?).
-            iMod ("H" with "[]") as "(Hσ&Herr&Hwand)". { iPureIntro; auto. }
-            iMod ("Hwand" with "[$] [$]"); eauto.
-        }
+          ⌜R ρ2⌝ -∗
+          |={∅|}=> ◇ ⌜tgl (lim_exec ρ2) φ (ε2 ρ2)⌝)%I with "[H]" as "H".
+        { iIntros (ρ2) "%Hρ2". destruct (ρ2) as (e2&σ2).
+          iApply (elim_fupd_hfupd_plain 0 0 ∅ ∅
+            (exec_stutter
+               (λ ε' : nonnegreal,
+                  (|={∅,⊤}=> state_interp (S k) σ2 ∗ err_interp ε' ∗
+                    ∀ (k0 : nat) (a : state) (a0 : nonnegreal),
+                      state_interp k0 a -∗ err_interp a0 ={⊤|}=∗
+                      ◇ ⌜tgl (lim_exec (e2, a)) φ a0⌝)%I)
+               (ε2 (e2, σ2)))
+            ⌜tgl (lim_exec (e2, σ2)) φ (ε2 (e2, σ2))⌝); [lia|].
+          iSplitL "H"; [iApply ("H" $! e2 σ2 Hρ2)|].
+          iIntros (l1 Hl1) "Hst". assert (l1 = 0%nat) as -> by lia.
+          iDestruct "Hst" as "(%R' & %ε1' & %ε2' & %Hineq' & %Hlift' & H)".
+          rewrite -(dret_id_left' (λ _ : (), lim_exec (e2, σ2)) tt).
+          iApply (fupd_finally_mono _ (◇ ⌜tgl (dret tt ≫= λ _ : (), lim_exec (e2, σ2)) φ (ε1' + ε2')⌝)%I).
+          { apply except_0_pure_mono_iprop.
+            intros Htgl. eapply tgl_mon_grading; eauto. }
+          iApply (tgl_dbind' (λ _ : (), lim_exec (e2, σ2)) (dret tt) R' (λ x, φ x) ε1' ε2').
+          { iPureIntro. apply cond_nonneg. }
+          { iPureIntro. apply cond_nonneg. }
+          { iPureIntro. exact Hlift'. }
+          iIntros (a HRa). destruct a.
+          iSpecialize ("H" with "[//]").
+          iApply (elim_fupd_hfupd_plain 0 0 ∅ ⊤
+            (state_interp (S k) σ2 ∗ err_interp ε2' ∗
+              (∀ (k0 : nat) (a : state) (a0 : nonnegreal),
+                state_interp k0 a -∗ err_interp a0 ={⊤|}=∗
+                ◇ ⌜tgl (lim_exec (e2, a)) φ a0⌝))%I
+            ⌜tgl (lim_exec (e2, σ2)) φ ε2'⌝); [lia|].
+          iSplitL "H"; [iApply "H"|].
+          iIntros (l' Hl') "(Hσ' & Hε' & Hwp')".
+          assert (l' = 0%nat) as -> by lia.
+          iSpecialize ("Hwp'" $! (S k) σ2 ε2' with "Hσ' Hε'").
+          iApply (fupd_finally_mono _ _ with "Hwp'").
+          apply except_0_pure_mono_iprop. intros Htgl. exact Htgl. }
         rewrite {2}/tgl.
         setoid_rewrite prob_dbind.
-        iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - (ε2 e) <= prob (lim_exec e) (λ x, bool_decide(φ x))⌝)%I).
-        {
-          iIntros (HR). iPureIntro.
-          by eapply twp_step_fupd_tgl_prim_step.
-        }
-        iIntros (a HR). iMod ("H" $! a (HR)) as "H".
-        destruct a.
-        iMod "H" as "%".
-        iPureIntro.
-        by apply H.
+        iApply (fupd_finally_mono _ (◇ ⌜∀ e0, R e0 → 1 - (ε2 e0) <=
+                          prob (lim_exec e0) (λ x, bool_decide (φ x))⌝)%I).
+        { iIntros "Hgoal". iStopProof.
+          apply except_0_pure_mono_iprop. intros HR.
+          by eapply twp_step_fupd_tgl_prim_step. }
+        iIntros (a HRa).
+        iApply (fupd_finally_mono _ _ with "(H [//])").
+        apply except_0_pure_mono_iprop.
+        intros. by destruct a.
       + remember (language.get_active σ) as l.
         assert (l ⊆ language.get_active σ) as Hsubseteq by set_solver.
         clear Heql.
@@ -371,36 +418,57 @@ Section adequacy.
         2:{ iApply "IH"; try done. iPureIntro. set_solver. }
         iDestruct "H" as "(%R & %ε1 & %ε2 & %Hbound & %Hineq & %Hub & H)".
         iAssert (∀ σ2 : language.state prob_lang,
-                   ⌜R σ2⌝ ={∅}=∗ ⌜tgl (lim_exec (e, σ2)) φ (ε2 (e, σ2))⌝)%I with "[H]" as "H".
+                   ⌜R σ2⌝ -∗
+                   |={∅|}=> ◇ ⌜tgl (lim_exec (e, σ2)) φ (ε2 (e, σ2))⌝)%I
+          with "[H]" as "H".
         { iClear "IH".
-          iIntros. iMod ("H" $! σ2 (H)) as "H".
-          iDestruct "H" as "(%R' & %ε1' & %ε2' & %Hineq' & %Hub' & H)".
-          iApply fupd_mono.
-          { iApply pure_mono. intros. eapply tgl_mon_grading; [eapply Hineq'|eauto]. }
-          rewrite -{2}(dret_id_left' (fun _ : () => (lim_exec (e, σ2))) tt).
-          iApply tgl_dbind'.
-          - iPureIntro; apply cond_nonneg.
-          - iPureIntro; apply cond_nonneg.
-          - iPureIntro; eapply Hub'.
-          - iIntros. destruct a.
-            iSpecialize ("H" with "[//]").
-            iDestruct "H" as "[H _]".
-            iApply ("H" with "[//]").
-        }
+          iIntros (σ2) "%HRs2".
+          iApply (elim_fupd_hfupd_plain 0 0 ∅ ∅
+            (exec_stutter
+               (λ ε2' : nonnegreal,
+                  ((⌜language.to_val e = None⌝ ={∅|}=∗
+                    ◇ ⌜tgl (lim_exec (e, σ2)) φ ε2'⌝) ∧
+                   glm e σ2 ε2'
+                     (λ '(e2, σ2') (ε2'' : nonnegreal),
+                        |={∅,⊤}=> state_interp (S k) σ2' ∗ err_interp ε2'' ∗
+                          ∀ (k0 : nat) (a : state) (a0 : nonnegreal),
+                            state_interp k0 a -∗ err_interp a0 ={⊤|}=∗
+                            ◇ ⌜tgl (lim_exec (e2, a)) φ a0⌝))%I)
+               (ε2 (e, σ2)))
+            ⌜tgl (lim_exec (e, σ2)) φ (ε2 (e, σ2))⌝); [lia|].
+          iSplitL "H"; [iApply ("H" $! σ2 HRs2)|].
+          iIntros (l' Hl') "Hst". assert (l' = 0%nat) as -> by lia.
+          iDestruct (exec_stutter_compat_1 _ _ with "[] Hst") as "[%H'|H2]".
+          { iIntros (εa εb Hle) "H". iSplit.
+            - iDestruct "H" as "[H _]". iIntros "%Hto". iSpecialize ("H" with "[//]").
+              iApply (fupd_finally_mono _ _ with "H").
+              apply except_0_pure_mono_iprop.
+              intros Hge. eapply tgl_mon_grading; eauto.
+            - iDestruct "H" as "[_ H]".
+              iApply (glm_mono_grading with "[%] H"). exact Hle. }
+          2: { iDestruct "H2" as "[H2 _]". iSpecialize ("H2" with "[//]").
+            iApply (fupd_finally_mono _ _ with "H2").
+            apply except_0_pure_mono_iprop. intros; auto. }
+          iApply hfupd_intro. iApply laterN_intro.
+          rewrite /bi_except_0. iRight. iPureIntro.
+          rewrite /tgl. intros.
+          eapply Rle_trans; [|apply prob_ge_0].
+          destruct (ε2 (e, σ2)) as [? ?]. simpl in *. lra. }
         rewrite {2}/tgl.
-        iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 (e, s) <= prob (lim_exec (e, s)) (λ x, bool_decide (φ x))⌝)%I).
-        {
-          iIntros. iPureIntro.
+        iApply (fupd_finally_mono _ (◇ ⌜∀ s, R s → 1 - ε2 (e, s) <=
+              prob (lim_exec (e, s)) (λ x, bool_decide (φ x))⌝)%I).
+        { iIntros "Hgoal". iStopProof.
+          apply except_0_pure_mono_iprop. intros HR.
           rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver.
           simpl.
           rewrite /tgl prob_dbind.
           erewrite SeriesC_ext; last by rewrite dret_id_right.
           eapply twp_step_fupd_tgl_state_step; try done.
-          set_solver.
-        }
-        iIntros (a HR). iMod ("H" $! a (HR)) as "%H".
-        iPureIntro. by apply H.
-    Qed.
+          set_solver. }
+        iIntros (s HRs).
+        iApply (fupd_finally_mono _ _ with "(H [//])").
+        apply except_0_pure_mono_iprop. intros; done.
+  Qed.
 End adequacy.
 
 
@@ -410,28 +478,27 @@ Theorem twp_tgl Σ `{erisGpreS Σ} (e : expr) (σ : state) (ε : R) φ :
   tgl (lim_exec (e, σ)) φ ε.
 Proof.
   intros Hε Hwp.
-  eapply pure_soundness, (step_fupdN_soundness_no_lc _ 0 0) => Hinv.
-  iIntros "_".
-  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
-  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
+  apply (pure_soundness (PROP:=iPropI Σ)).
+  apply (laterN_soundness _ 1).
+  rewrite laterN_later -except_0_into_later.
   destruct (decide (ε < 1)) as [Hcr|Hcr]; last first.
-  { iClear "Hh Ht".
-    iApply (fupd_mask_intro); [eauto|].
-    iIntros "_".
-    simpl.
-    iPureIntro.
+  { iApply laterN_intro. iApply except_0_intro. iPureIntro.
     apply not_Rlt, Rge_le in Hcr.
-    rewrite /tgl; intros.
+    rewrite /tgl. intros.
     eapply Rle_trans; last eapply prob_ge_0.
     lra. }
+  apply (fupd_finally_soundness HasLc 0 ⊤).
+  iIntros (Hinv) "_".
+  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
+  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
   set ε' := mknonnegreal _ Hε.
-  iMod (ec_alloc ε') as (?) "[? ?]"; [by simpl|].
+  iMod (ec_alloc ε') as (Hec) "[Hs Hf]"; [done|].
   set (HclutchGS := HeapG Σ _ _ _ γH γT _).
-  epose proof (twp_step_fupd_tgl e σ ε' φ).
-  iApply fupd_wand_r. iSplitL.
-  - iApply H1. iFrame. by iApply Hwp.
-  - iIntros "%". done.
-    Unshelve. apply _.
+  change ε with (nonneg ε').
+  iPoseProof (twp_step_fupd_tgl O e σ ε' φ) as "H".
+  iApply "H".
+  iFrame "Hs". rewrite /state_interp /=. iFrame "Hh Ht".
+  iApply Hwp. iApply "Hf".
 Qed.
 
 Theorem twp_mass_lim_exec Σ `{erisGpreS Σ} (e : expr) (σ : state) (ε : R) φ :
diff --git a/theories/eris/total_ectx_lifting.v b/theories/eris/total_ectx_lifting.v
index eb6dc5ec4..a9a213c70 100644
--- a/theories/eris/total_ectx_lifting.v
+++ b/theories/eris/total_ectx_lifting.v
@@ -15,28 +15,28 @@ Local Hint Resolve head_stuck_stuck : core.
 
 Lemma twp_lift_head_step_glm {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1 ε1,
-    state_interp σ1 ∗ err_interp ε1
+  (∀ n σ1 ε1,
+    state_interp n σ1 ∗ err_interp ε1
     ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-      |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]))
+      |={∅,E}=> state_interp (S n) σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε1) "Hσε".
+  iIntros (n σ1 ε1) "Hσε".
   iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto.
 Qed.
 
 Lemma twp_lift_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ n σ1, state_interp n σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
      ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }])
+      state_interp (S n) σ2 ∗ WP e2 @ s; E [{ Φ }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+  iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
@@ -45,15 +45,15 @@ Qed.
 
 Lemma twp_lift_atomic_head_step_fupd {E1 Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ n σ1, state_interp n σ1 ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E1}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (? σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iIntros (e2 σ2 Hstep).
@@ -62,15 +62,15 @@ Qed.
 
 Lemma twp_lift_atomic_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ n σ1, state_interp n σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
      ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (? σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iIntros (e2 σ2 Hstep).
diff --git a/theories/eris/total_lifting.v b/theories/eris/total_lifting.v
index 4608bc45b..af6e26e8f 100644
--- a/theories/eris/total_lifting.v
+++ b/theories/eris/total_lifting.v
@@ -14,11 +14,11 @@ Section total_lifting.
 
   Lemma twp_lift_step_fupd_glm E Φ e1 s :
   to_val e1 = None →
-  (∀ σ1 ε1,
-    state_interp σ1 ∗ err_interp ε1
+  (∀ n σ1 ε1,
+    state_interp n σ1 ∗ err_interp ε1
     ={E,∅}=∗
     glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-                      |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]))
+                      |={∅,E}=> state_interp (S n) σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]))
   ⊢ WP e1 @ s; E [{ Φ }].
   Proof.
     by rewrite tgl_wp_unfold /tgl_wp_pre =>->.
@@ -26,18 +26,18 @@ Section total_lifting.
 
   Lemma twp_lift_step_fupd E Φ e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1
+  (∀ n σ1, state_interp n σ1
      ={E,∅}=∗
     ⌜reducible (e1, σ1)⌝ ∗
      ∀ e2 σ2,
       ⌜prim_step e1 σ1 (e2, σ2) > 0 ⌝ ={∅}=∗ |={∅,E}=>
-      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }])
+      state_interp (S n) σ2 ∗ WP e2 @ s; E [{ Φ }])
   ⊢ WP e1 @ s; E  [{ Φ }].
   Proof.
     intros Hval.
     iIntros "H".
     iApply twp_lift_step_fupd_glm; [done|].
-    iIntros (σ1 ε1) "[Hσ Hε]".
+    iIntros (n1 σ1 ε1) "[Hσ Hε]".
     iMod ("H" with "Hσ") as "[%Hs H]". iModIntro.
     iApply (glm_prim_step e1 σ1).
     iExists _.
@@ -60,15 +60,15 @@ Section total_lifting.
   (** Derived lifting lemmas. *)
   Lemma twp_lift_step E Φ e1 s :
     to_val e1 = None →
-    (∀ σ1, state_interp σ1 ={E,∅}=∗
+    (∀ n σ1, state_interp n σ1 ={E,∅}=∗
            ⌜reducible (e1, σ1)⌝ ∗
            ∀ e2 σ2,
        ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
-       state_interp σ2 ∗
+       state_interp (S n) σ2 ∗
        WP e2 @ s; E [{ Φ }])
     ⊢ WP e1 @ s; E [{ Φ }].
   Proof.
-    iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+    iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
     iMod ("H" with "Hσ") as "[$ H]". iIntros "!>" (???) "!>" . iMod ("H" with "[]"); first done.
     iModIntro; done.
   Qed.
@@ -81,27 +81,30 @@ Section total_lifting.
   Proof.
     iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
     { by eapply (to_final_None_1 (e1, inhabitant)), reducible_not_final. }
-    iIntros (σ1) "Hσ". iMod "H".
+    iIntros (n σ1) "Hσ". iMod "H".
     iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
     iSplit; [done|].
     iIntros (e2 σ2 Hprim).
     destruct (Hstep _ _ _ Hprim).
-    iMod "Hclose" as "_". iModIntro.
-    iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
+    iMod "Hclose" as "_".
+    iDestruct ("H" with "[//]") as "H".
+    iMod (fupd_mask_subseteq ∅) as "Hclo"; first by set_solver+.
+    iMod (state_interp_mono with "[$]") as "$".
+    iMod "Hclo". by iFrame.
   Qed.
 
   Lemma twp_lift_atomic_step_fupd {E1 Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ n σ1, state_interp n σ1 ={E1}=∗
     ⌜reducible (e1, σ1)⌝ ∗
     ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E1}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 [{ Φ }].
   Proof.
     iIntros (?) "H".
-    iApply (twp_lift_step_fupd E1 _ e1)=>//; iIntros (σ1) "Hσ1".
-    iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
+    iApply (twp_lift_step_fupd E1 _ e1)=>//; iIntros (n σ1) "Hσ1".
+    iMod ("H" $! n σ1 with "Hσ1") as "[$ H]".
     iApply fupd_mask_intro; first set_solver.
     iIntros "Hclose" (e2 σ2 Hs). iMod "Hclose" as "_".
     iMod ("H" $! e2 σ2 with "[#]") as "[Hs ?]"; [done|].
@@ -114,15 +117,15 @@ Section total_lifting.
 
   Lemma twp_lift_atomic_step {E Φ} e1 s :
     to_val e1 = None →
-    (∀ σ1, state_interp σ1 ={E}=∗
+    (∀ n σ1, state_interp n σ1 ={E}=∗
            ⌜reducible (e1, σ1)⌝ ∗
           ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
-                    state_interp σ2 ∗
+                    state_interp (S n) σ2 ∗
                     from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
   Proof.
     iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|].
-    iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]".
+    iIntros (n ?) "?". iMod ("H" with "[$]") as "[$ H]".
     iIntros "!> *". iIntros (Hstep).
     by iApply "H".
   Qed.
diff --git a/theories/eris/total_primitive_laws.v b/theories/eris/total_primitive_laws.v
index 9c7f3ebca..a5cf6fa9c 100644
--- a/theories/eris/total_primitive_laws.v
+++ b/theories/eris/total_primitive_laws.v
@@ -20,7 +20,7 @@ Lemma twp_alloc E v s :
 Proof.
   iIntros (Φ) "_ HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   solve_red.
   iIntros "/=" (e2 σ2 Hs); inv_head_step.
   iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]".
@@ -40,7 +40,7 @@ Lemma twp_allocN_seq (N : nat) (z : Z) E v s:
 Proof.
   iIntros (-> Hn Φ) "_ HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iSplit.
   { iPureIntro.
     rewrite /head_reducible.
@@ -92,7 +92,7 @@ Lemma twp_load E l dq v s :
 Proof.
   iIntros (Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iDestruct (ghost_map_lookup with "Hh Hl") as %?.
   solve_red.
   iIntros "/=" (e2 σ2 Hs); inv_head_step.
@@ -105,7 +105,7 @@ Lemma twp_store E l v' v s :
 Proof.
   iIntros (Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "[Hh Ht] !#".
+  iIntros (n σ1) "[Hh Ht] !#".
   iDestruct (ghost_map_lookup with "Hh Hl") as %?.
   solve_red.
   iIntros "/=" (e2 σ2 Hs); inv_head_step.
@@ -119,7 +119,7 @@ Lemma twp_rand (N : nat) (z : Z) E s :
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "Hσ !#".
+  iIntros (n σ1) "Hσ !#".
   solve_red.
   iIntros (e2 σ2 Hs).
   inv_head_step.
@@ -148,7 +148,7 @@ Lemma twp_alloc_tape N z E s :
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !# /=".
+  iIntros (n σ1) "(Hh & Ht) !# /=".
   solve_red.
   iIntros (e2 σ2 Hs); inv_head_step.
   iMod (ghost_map_insert (fresh_loc σ1.(tapes)) with "Ht") as "[$ Hl]".
@@ -163,7 +163,7 @@ Lemma twp_rand_tape N α n ns z E s :
 Proof.
   iIntros (-> Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n' σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros (e2 σ2 Hs).
@@ -179,7 +179,7 @@ Lemma twp_rand_tape_empty N z α E s :
 Proof.
   iIntros (-> Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros (e2 σ2 Hs).
@@ -195,7 +195,7 @@ Lemma twp_rand_tape_wrong_bound N M z α E ns s :
 Proof.
   iIntros (-> ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1) "(Hh & Ht) !#".
+  iIntros (n σ1) "(Hh & Ht) !#".
   iDestruct (ghost_map_lookup with "Ht Hl") as %?.
   solve_red.
   iIntros (e2 σ2 Hs).
diff --git a/theories/eris/total_weakestpre.v b/theories/eris/total_weakestpre.v
index 7fbf34793..96553c6a7 100644
--- a/theories/eris/total_weakestpre.v
+++ b/theories/eris/total_weakestpre.v
@@ -9,10 +9,10 @@ Definition tgl_wp_pre `{!erisWpGS Λ Σ}
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 ε1,
-      state_interp σ1 ∗ err_interp ε1 ={E,∅}=∗
+  | None => ∀ n σ1 ε1,
+      state_interp n σ1 ∗ err_interp ε1 ={E,∅}=∗
       glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-        |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ wp E e2 Φ)
+        |={∅,E}=> state_interp (S n) σ2 ∗ err_interp ε2 ∗ wp E e2 Φ)
 end%I.
 
 Local Lemma tgl_wp_pre_mono `{!erisWpGS Λ Σ}
@@ -23,7 +23,7 @@ Proof.
   iIntros "#H".
   iIntros (E e Φ) "Hwp". rewrite /tgl_wp_pre.
   case_match; first done.
-  iIntros (σ ε) "He". iMod ("Hwp" with "He") as "Hwp".
+  iIntros (n σ ε) "He". iMod ("Hwp" with "He") as "Hwp".
   iModIntro. iApply (glm_mono_pred with "[][$Hwp]").
   iIntros ([e' s] ε') "He".
   iApply (fupd_wand_l with "[H He]").
@@ -44,7 +44,7 @@ Proof.
     iApply tgl_wp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /curry3 /tgl_wp_pre. do 7 (f_equiv).
+    rewrite /curry3 /tgl_wp_pre. do 9 (f_equiv).
     rewrite /glm /glm'.
     f_equiv.
     intros Φ e. unfold glm_pre.
@@ -114,7 +114,7 @@ Section tgl_wp.
       clear. iIntros (e E Φ) "H #IH".
       iApply "IH".
       rewrite {2 4}/tgl_wp_pre. case_match; first done.
-      iIntros (σ ε) "[Hs He]".
+      iIntros (n σ ε) "[Hs He]".
       iMod ("H" with "[$]") as "H".
       iModIntro.
       iApply (glm_mono_pred with "[]H").
@@ -141,7 +141,7 @@ Section tgl_wp.
     iIntros (e E Φ) "H #IH".
     iApply "IH".
     rewrite {2 4}/tgl_wp_pre. case_match; first done.
-    iIntros (σ ε) "[Hs He]".
+    iIntros (n σ ε) "[Hs He]".
     iMod ("H" with "[$]") as "H".
     iModIntro.
     iApply (glm_mono_pred with "[]H").
@@ -161,8 +161,8 @@ Section tgl_wp.
     iApply tgl_wp_ind; first solve_proper.
     iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
     rewrite !tgl_wp_unfold /tgl_wp_pre. destruct (to_val e) as [v|] eqn:?.
-    { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }    
-    iIntros (σ1 ε1) "[Hs He]".
+    { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
+    iIntros (n σ1 ε1) "[Hs He]".
     iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
     iMod ("IH" with "[$Hs $He]") as "IH".
     iModIntro.
@@ -178,7 +178,7 @@ Section tgl_wp.
   Proof.
     rewrite tgl_wp_unfold /tgl_wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
     { by iMod "H". }
-    iIntros (s' ε) "[Hs He]".
+    iIntros (n s' ε) "[Hs He]".
     iMod "H". iApply "H". iFrame.
   Qed.
   Lemma tgl_wp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] ⊢ WP e @ s; E [{ Φ }].
@@ -190,7 +190,7 @@ Section tgl_wp.
     iIntros "H". rewrite !tgl_wp_unfold /tgl_wp_pre /=.
     destruct (to_val e) as [v|] eqn:He.
     { by iDestruct "H" as ">>> $". }
-    iIntros (σ1 ε) "[Hs He]". iMod "H". iMod ("H" $! σ1 ε with "[$Hs $He]") as "H".
+    iIntros (n σ1 ε) "[Hs He]". iMod "H". iMod ("H" $! n σ1 ε with "[$Hs $He]") as "H".
   iModIntro. iApply (glm_strong_mono with "[][]H"); [done|].
   iIntros (e2 σ2 ε2) "([%σ' %Hstep]&H)".
   iMod "H" as "(Hσ&Hε&Hwp)".
@@ -214,7 +214,7 @@ Section tgl_wp.
     rewrite /tgl_wp_pre. destruct (to_val e) as [v|] eqn:He.
     { apply of_to_val in He as <-. iApply fupd_tgl_wp. by iApply "HΦ". }
     rewrite tgl_wp_unfold /tgl_wp_pre fill_not_val //.
-    iIntros (σ1 ε1) "[Hσ Hε]". iMod ("IH" with "[$]") as "IH".
+    iIntros (n σ1 ε1) "[Hσ Hε]". iMod ("IH" with "[$]") as "IH".
     iModIntro.
     iApply glm_bind; [done|].
     iApply (glm_mono with "[][HΦ][$]"); first done.
@@ -226,13 +226,20 @@ Section tgl_wp.
   Lemma tgl_wp_pgl_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
   Proof.
     iIntros "H". iLöb as "IH" forall (E e Φ).
-    rewrite pgl_wp_unfold tgl_wp_unfold /pgl_wp_pre /tgl_wp_pre. destruct (to_val e) as [v|]=>//=.
-    iIntros (σ1 ε) "[Hσ Hε]". iMod ("H" with "[$Hσ $Hε]") as "H".
+    rewrite pgl_wp_unfold tgl_wp_unfold /pgl_wp_pre /tgl_wp_pre.
+    destruct (to_val e) as [v|]=>//=.
+    iIntros (n σ1 ε) "[Hσ Hε]". iMod ("H" with "[$Hσ $Hε]") as "H".
     iIntros "!>".
     iApply glm_mono_pred; last iFrame.
-    iIntros ([e' s'] ε').
-    iIntros "H". iNext. iMod "H" as "[?[?H]]".
-    iModIntro. iFrame. iApply "IH". done.
+    iIntros ([e' s'] ε') "H _".
+    (* Goal: step_fupdN (S _) (|={∅,E}=> state_interp ∗ err_interp ∗ pgl_wp).
+       H : |={∅,E}=> state_interp ∗ err_interp ∗ tgl_wp.
+       Use [step_fupdN_le 0 _] (since 0 ≤ S _) to weaken the trivial
+       [step_fupdN 0 P = P] to [step_fupdN (S _) P]. *)
+    iApply (step_fupdN_le 1 (S (num_laters_per_step n))); [lia|done|].
+    iApply step_fupdN_intro; [done|]. simpl.
+    iNext.
+    iMod "H" as "(? & ? & H)". iModIntro. iFrame. by iApply "IH".
   Qed.
 
   Lemma tgl_wp_pgl_wp' E e Φ : WP e @ E [{ Φ }] -∗ WP e @ E {{ Φ }}.
diff --git a/theories/eris/weakestpre.v b/theories/eris/weakestpre.v
index 880ca4e5a..56898c731 100644
--- a/theories/eris/weakestpre.v
+++ b/theories/eris/weakestpre.v
@@ -1,6 +1,6 @@
 From Stdlib Require Export Reals Psatz.
 From iris.proofmode Require Import base proofmode.
-From iris.base_logic.lib Require Export fancy_updates.
+From iris.base_logic.lib Require Export fancy_updates later_credits.
 From iris.bi Require Export lib.fixpoint_mono big_op.
 From iris.prelude Require Import options.
 
@@ -21,9 +21,12 @@ Local Open Scope NNR_scope.
     error (i.e. terminating in a state that does not satisfy the postcondition)
  *)
 Class erisWpGS (Λ : language) (Σ : gFunctors) := ErisWpGS {
-  erisWpGS_invGS :: invGS_gen HasNoLc Σ;
-  state_interp : state Λ → iProp Σ;
+  erisWpGS_invGS :: invGS_gen HasLc Σ;
+  state_interp : nat → state Λ → iProp Σ;
   err_interp : nonnegreal → iProp Σ;
+  num_laters_per_step : nat → nat;
+  state_interp_mono ns σ :
+    state_interp ns σ ⊢ |={∅}=> state_interp (S ns) σ;
 }.
 Global Opaque erisWpGS_invGS.
 Global Arguments ErisWpGS {Λ Σ}.
@@ -682,20 +685,25 @@ Definition pgl_wp_pre `{!erisWpGS Λ Σ}
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 ε1,
-      state_interp σ1 ∗ err_interp ε1 ={E,∅}=∗
+  | None => ∀ n σ1 ε1,
+      state_interp n σ1 ∗ err_interp ε1 ={E,∅}=∗
       glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-        ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ wp E e2 Φ)
+        £ (S (num_laters_per_step n))
+        ={∅}▷=∗^(S (num_laters_per_step n)) |={∅,E}=>
+        state_interp (S n) σ2 ∗ err_interp ε2 ∗ wp E e2 Φ)
 end%I.
 
 Local Instance wp_pre_contractive `{!erisWpGS Λ Σ} : Contractive (pgl_wp_pre).
 Proof.
   rewrite /pgl_wp_pre /= => n wp wp' Hwp E e1 Φ /=.
-  do 7 (f_equiv).
+  do 9 (f_equiv).
   apply least_fixpoint_ne_outer; [|done].
   intros Ψ [[e' σ'] ε']. rewrite /glm_pre.
   do 17 f_equiv.
-  { rewrite /exec_stutter. do 10 f_equiv. f_contractive. do 3 f_equiv. apply Hwp. }
+  rewrite /exec_stutter. do 14 (f_contractive || f_equiv).
+  (* Strip [£ _ -∗] and step through the [step_fupdN] iteration. *)
+  induction num_laters_per_step as [|k IHk]; simpl; last by rewrite -IHk.
+  repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
 
@@ -729,14 +737,16 @@ Global Instance pgl_wp_ne s E e n :
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !pgl_wp_unfold /pgl_wp_pre /=.
-  do 7 f_equiv.
+  do 9 f_equiv.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /glm_pre.
   do 16 f_equiv.
   rewrite /exec_stutter.
-  do 11 f_equiv. f_contractive_fin.
+  do 11 f_equiv. do 1 f_equiv.
+  induction num_laters_per_step as [|k IHk]; simpl; last by rewrite IHk.
+  f_equiv. f_contractive_fin. do 4 f_equiv.
   rewrite IH; [done|lia|].
-  intros ?. eapply dist_S, HΦ. 
+  intros ?. eapply dist_S, HΦ.
 Qed.
 
 Global Instance pgl_wp_proper s E e :
@@ -749,11 +759,13 @@ Global Instance pgl_wp_contractive s E e n :
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   intros He Φ Ψ HΦ. rewrite !pgl_wp_unfold /pgl_wp_pre He /=.
-  do 6 f_equiv.
+  do 8 f_equiv.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /glm_pre.
   do 16 f_equiv.
-  rewrite /exec_stutter. do 11 f_equiv. f_contractive. do 6 f_equiv.
+  rewrite /exec_stutter. do 14 (f_contractive || f_equiv).
+  induction num_laters_per_step as [|k IHk]; simpl; last by rewrite IHk.
+  by do 6 (f_contractive || f_equiv).
 Qed.
 
 Lemma pgl_wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
@@ -767,12 +779,14 @@ Proof.
   rewrite !pgl_wp_unfold /pgl_wp_pre /=.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (n σ1 ε) "[Hσ Hε]".
   iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "H".
   iApply (glm_mono_pred with "[Hclose HΦ] H").
-  iIntros ([e2 σ2]?) "H".
-  iModIntro.
+  iIntros ([e2 σ2]?) "H Hcred".
+  iSpecialize ("H" with "Hcred").
+  iApply (step_fupdN_wand with "H").
+  iIntros "!> H".
   iMod "H" as "(?&?& Hwp)". iFrame.
   iMod "Hclose" as "_". iModIntro.
   iApply ("IH" with "[] Hwp"); auto.
@@ -782,7 +796,7 @@ Lemma fupd_pgl_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ 
 Proof.
   rewrite pgl_wp_unfold /pgl_wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-   iIntros (σ1 ε) "Hi". iMod "H". by iApply "H".
+   iIntros (n σ1 ε) "Hi". iMod "H". by iApply "H".
 Qed.
 Lemma pgl_wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (pgl_wp_strong_mono E with "H"); auto. Qed.
@@ -793,38 +807,55 @@ Proof.
   iIntros "H".
   rewrite !pgl_wp_unfold /pgl_wp_pre.
   destruct (to_val e) as [v|] eqn:He; [by do 2 iMod "H"|].
-  iIntros (σ1 ε1) "(Hσ&Hε)".
-  iSpecialize ("H" $! σ1 ε1).
+  iIntros (n σ1 ε1) "(Hσ&Hε)".
+  iSpecialize ("H" $! n σ1 ε1).
   iMod ("H" with "[Hσ Hε]") as "H"; [iFrame|].
   iMod "H"; iModIntro.
   iApply (glm_strong_mono with "[] [] H"); [done|].
-  iIntros (e2 σ2 ε2) "([%σ' %Hstep]&H)".
-  iNext.
+  iIntros (e2 σ2 ε2) "([%σ' %Hstep]&H) Hcred".
+  iSpecialize ("H" with "Hcred").
+  iApply (step_fupdN_wand with "H").
+  iIntros "H".
   iMod "H" as "(Hσ&Hε&Hwp)".
   rewrite !pgl_wp_unfold /pgl_wp_pre.
   destruct (to_val e2) as [?|] eqn:He2.
   + iFrame. do 2 (iMod "Hwp"). by do 2 iModIntro.
-  + iMod ("Hwp" $! _ _ with "[Hσ Hε]") as "Hwp"; [iFrame|].
+  + iMod ("Hwp" $! _ _ _ with "[Hσ Hε]") as "Hwp"; [iFrame|].
     specialize (atomic _ _ _ Hstep) as Hatomic. (* key step *)
     destruct Hatomic.
     congruence. (* how do we do this "by hand"? Not obvious to me *)
 Qed.
 
+(** Helper: a ▷ on R can be absorbed by an [S n]-step [step_fupdN], with
+    R appearing un-laterised inside. *)
+Lemma step_fupdN_later_frame_l `{!erisWpGS Λ Σ} Eo Ei n (R Q : iProp Σ) :
+  ▷ R ∗ (|={Eo}[Ei]▷=>^(S n) Q) ⊢ |={Eo}[Ei]▷=>^(S n) (R ∗ Q).
+Proof.
+  iIntros "[HR HQ]".
+  simpl. iMod "HQ". iModIntro. iNext.
+  iMod "HQ". iModIntro.
+  iApply step_fupdN_frame_l. iFrame.
+Qed.
+
 Lemma pgl_wp_step_fupd s E1 E2 e P Φ :
   TCEq (to_val e) None → E2 ⊆ E1 →
   (|={E1}[E2]▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !pgl_wp_unfold /pgl_wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1 ε) "[Hσ Hε]". iMod "HR".
+  iIntros (n σ1 ε) "[Hσ Hε]". iMod "HR".
   iMod ("H" with "[$Hσ $Hε]") as "H".
   iModIntro.
   iApply (glm_mono_pred with "[HR] H").
-  iIntros ([e2 σ2] ?) "H".
-  iModIntro.
-  iMod "H" as "(Hσ & Hρ & H)".
+  iIntros ([e2 σ2] ?) "H Hcred".
+  iSpecialize ("H" with "Hcred").
+  iCombine "HR H" as "H".
+  rewrite step_fupdN_later_frame_l.
+  iApply (step_fupdN_wand with "H").
+  iIntros "[HR H]".
+  iMod "H" as "(Hσ & Hρ & Hwp)".
   iMod "HR".
   iFrame "Hσ Hρ".
-  iApply (pgl_wp_strong_mono E2 with "H"); [done..|].
+  iApply (pgl_wp_strong_mono E2 with "Hwp"); [done..|].
   iIntros "!>" (v) "H". by iApply "H".
 Qed.
 
@@ -835,15 +866,16 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_pgl_wp. }
   rewrite pgl_wp_unfold /pgl_wp_pre fill_not_val /=; [|done].
-  iIntros (σ1 ε) "[Hσ Hε]".
+  iIntros (n σ1 ε) "[Hσ Hε]".
   iMod ("H" with "[$Hσ $Hε]") as "H".
   iModIntro.
   iApply glm_bind; [done |].
   iApply (glm_mono with "[] [] H").
   - iPureIntro; lra.
-  - iIntros ([e2 σ2] ?) "H".
-    iModIntro.
-    iMod "H" as "(Hσ & Hρ & H)".
+  - iIntros ([e2 σ2] ?) "H Hcred".
+    iSpecialize ("H" with "Hcred").
+    iApply (step_fupdN_wand with "H").
+    iIntros "!> H". iMod "H" as "(Hσ & Hρ & H)".
     iModIntro.
     iFrame "Hσ Hρ". by iApply "IH".
 Qed.
diff --git a/theories/foxtrot/examples/encryption.v b/theories/foxtrot/examples/encryption.v
index 977f4f43a..7ceb5ba57 100644
--- a/theories/foxtrot/examples/encryption.v
+++ b/theories/foxtrot/examples/encryption.v
@@ -167,8 +167,8 @@ Section encr.
       rewrite /coupling_f. rewrite bool_decide_eq_true_2; last done.
       iMod (ghost_var_alloc false) as "(%γ1 & [Hγ1 Hγ1'])".
       iMod (ghost_var_alloc false) as "(%γ2 & [Hγ2 Hγ2'])".
-      iMod (inv_alloc nroot _ (∃ (b1 b2:bool), ghost_var γ1 (1/2) b1 ∗ ghost_var γ2 (1/2) b2 ∗ l ↦ # ((if b1 then n else 0)+(if b2 then n' else 0)))%I with "[$]") as "#Hinv".
-      wp_apply (wp_par (λ _, ghost_var γ1 (1/2) true)(λ _, ghost_var γ2 (1/2) true) with "[Hα Hγ1][Hα' Hγ2]").
+      iMod (inv_alloc nroot _ (∃ (b1 b2:bool), ghost_var γ1 (DfracOwn (1/2)) b1 ∗ ghost_var γ2 (DfracOwn (1/2)) b2 ∗ l ↦ # ((if b1 then n else 0)+(if b2 then n' else 0)))%I with "[$]") as "#Hinv".
+      wp_apply (wp_par (λ _, ghost_var γ1 (DfracOwn (1/2)) true)(λ _, ghost_var γ2 (DfracOwn (1/2)) true) with "[Hα Hγ1][Hα' Hγ2]").
       - wp_apply (wp_rand_tape with "[$]").
         iIntros "(_&%)".
         wp_pures.
diff --git a/theories/foxtrot/examples/encryption_unknown.v b/theories/foxtrot/examples/encryption_unknown.v
index 9a7de641b..e81df842e 100644
--- a/theories/foxtrot/examples/encryption_unknown.v
+++ b/theories/foxtrot/examples/encryption_unknown.v
@@ -177,8 +177,8 @@ Section encr.
       rewrite /coupling_f. rewrite bool_decide_eq_true_2; last done.
       iMod (ghost_var_alloc false) as "(%γ1 & [Hγ1 Hγ1'])".
       iMod (ghost_var_alloc false) as "(%γ2 & [Hγ2 Hγ2'])".
-      iMod (inv_alloc nroot _ (∃ (b1 b2:bool), ghost_var γ1 (1/2) b1 ∗ ghost_var γ2 (1/2) b2 ∗ l ↦ # ((if b1 then n else 0)+(if b2 then n' else 0)))%I with "[$]") as "#Hinv".
-      wp_apply (wp_par (λ _, ghost_var γ1 (1/2) true)(λ _, ghost_var γ2 (1/2) true) with "[Hα Hγ1][Hα' Hγ2]").
+      iMod (inv_alloc nroot _ (∃ (b1 b2:bool), ghost_var γ1 (DfracOwn (1/2)) b1 ∗ ghost_var γ2 (DfracOwn (1/2)) b2 ∗ l ↦ # ((if b1 then n else 0)+(if b2 then n' else 0)))%I with "[$]") as "#Hinv".
+      wp_apply (wp_par (λ _, ghost_var γ1 (DfracOwn (1/2)) true)(λ _, ghost_var γ2 (DfracOwn (1/2)) true) with "[Hα Hγ1][Hα' Hγ2]").
       - wp_apply (sample_tape_spec_some with "[$]") as "_".
         wp_pures.
         iInv "Hinv" as ">(%&%&?&?&Hl)" "Hclose".
diff --git a/theories/foxtrot/primitive_laws.v b/theories/foxtrot/primitive_laws.v
index f56d36fee..a354ca204 100644
--- a/theories/foxtrot/primitive_laws.v
+++ b/theories/foxtrot/primitive_laws.v
@@ -49,7 +49,7 @@ Definition tapes_auth `{foxtrotGS Σ} :=
 
 Global Instance foxtrotGS_irisGS `{!foxtrotGS Σ} : foxtrotWpGS con_prob_lang Σ := {
   foxtrotWpGS_invGS := foxtrotGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
   spec_interp ρ := spec_auth ρ;
   fork_post v :=  True%I;
   err_interp := ec_supply;
diff --git a/theories/prelude/iris_ext.v b/theories/prelude/iris_ext.v
index 84a9a5449..f522fcf35 100644
--- a/theories/prelude/iris_ext.v
+++ b/theories/prelude/iris_ext.v
@@ -26,6 +26,15 @@ Section fupd.
       /fancy_updates.uPred_fupd_def -assoc /=.
     by iApply ("HP" with "HwE").
   Qed.
+
+  Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+    (∀ `{Hinv : !invGS_gen HasNoLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) → ⊢ P.
+  Proof. intros HP. by apply (step_fupdN_soundness HasNoLc n m P). Qed.
+
+  Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+    (∀ `{Hinv : !invGS_gen HasLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) → ⊢ P.
+  Proof. intros HP. by apply (step_fupdN_soundness HasLc n m P). Qed.
+
 End fupd.
 
 (* TODO: upstream? *)
diff --git a/theories/prob_lang/spec/spec_ra.v b/theories/prob_lang/spec/spec_ra.v
index 606296c88..61ac82f81 100644
--- a/theories/prob_lang/spec/spec_ra.v
+++ b/theories/prob_lang/spec/spec_ra.v
@@ -45,11 +45,11 @@ Section resources.
   Definition spec_prog_auth e :=
     own specG_prob_lang_prog_name (● (Excl' e : progUR)).
   Definition spec_heap_auth `{specG_prob_lang Σ} :=
-    @ghost_map_auth _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name (DfracOwn 1).
   Definition spec_tapes_auth `{specG_prob_lang Σ} :=
-    @ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name (DfracOwn 1).
   Definition spec_tapes_laplace_auth `{specG_prob_lang Σ} :=
-    @ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes_laplace specG_prob_lang_tapes_laplace_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes_laplace specG_prob_lang_tapes_laplace_name (DfracOwn 1).
 
   Definition spec_auth (ρ : cfg) : iProp Σ :=
     spec_prog_auth (ρ.1) ∗
diff --git a/theories/pure_complete/eris_ast.v b/theories/pure_complete/eris_ast.v
index 6c71a1e44..489447185 100644
--- a/theories/pure_complete/eris_ast.v
+++ b/theories/pure_complete/eris_ast.v
@@ -71,7 +71,7 @@ Section Complete.
       { iIntros. apply of_to_val in He as <-. by wp_pures. }
       iIntros "Herr".
       iApply twp_lift_step_fupd_glm; auto.
-      iIntros "%% [Hs Herra]". 
+      iIntros (k σ1 ε_now) "[Hs Herra]".
       iDestruct (ec_supply_ec_inv with "Herra Herr") as %(ε1' & ε3 & Hε_now & Hε1').
       iApply fupd_mask_intro.
       { set_solver. }
@@ -204,7 +204,7 @@ Section Complete.
            iPoseProof (ec_contradict with "Herr") as "H"; auto; lra. }
       iIntros "Herr".
       iApply twp_lift_step_fupd_glm; auto.
-      iIntros "%% [Hs Herra]". 
+      iIntros (k σ1 ε_now) "[Hs Herra]".
       iDestruct (ec_supply_ec_inv with "Herra Herr") as %(ε1' & ε3 & Hε_now & Hε1').
       iApply fupd_mask_intro.
       { set_solver. }
@@ -350,7 +350,7 @@ Section Complete.
       iPoseProof (ec_contradict with "Herr") as "H"; auto; lra.
     }
     iApply twp_lift_step_fupd_glm; auto.
-    iIntros "%% [Hs Herra]". 
+    iIntros (k σ1 ε_now) "[Hs Herra]". 
     iApply fupd_mask_intro.
     { set_solver. }
     iIntros "hclose".
@@ -383,7 +383,7 @@ Section Complete.
     eapply tgl_gt_lim in H0 as [n H0]; [|exact H4].
     iPoseProof (AST_complete_pure_pre' with "Herr") as "hwp"; eauto.
     rewrite tgl_wp_unfold /tgl_wp_pre //= He.
-    iPoseProof ("hwp" with "[Hs Herra]") as "hwp"; try iFrame.
+    iPoseProof ("hwp" $! k with "[Hs Herra]") as "hwp"; try iFrame.
     iMod "hwp". 
     iApply fupd_mask_intro. 
     { set_solver. }
diff --git a/theories/tachis/problang_wp.v b/theories/tachis/problang_wp.v
index f61b50453..60a7b6d3b 100644
--- a/theories/tachis/problang_wp.v
+++ b/theories/tachis/problang_wp.v
@@ -33,7 +33,7 @@ Global Instance tachisGS_tachisWpGSS `{!tachisGS Σ F} : tachisWpGS prob_lang Σ
   tachisWpGS_invGS := tachisGS_invG;
   tachisWpGS_etcGS := tachisGS_etc;
 
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
   costfun := F
 }.