diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 3b12c56bc..3b9e7a464 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -39,10 +39,13 @@ jobs:
             startGroup "Install dependencies"
               opam install odoc -y
               apt-get install rsync -y
+              opam repo add --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git || true
               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..2759c1d29 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,10 @@ 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: Amin's branch declares a strict stdpp dev constraint in its
+  # own opam file, 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"}
@@ -32,6 +34,10 @@ depends: [
   "elpi" {= "3.4.2"}
   "odoc" {with-doc}
 ]
+pin-depends: [
+  [ "rocq-iris.dev"
+    "git+https://gitlab.mpi-sws.org/amintimany/iris-coq.git#improve-later-credits" ]
+]
 build: [
   ["dune" "subst"] {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..4a1ae48e4 100644
--- a/theories/eris/adequacy.v
+++ b/theories/eris/adequacy.v
@@ -15,22 +15,24 @@ 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 ◇ ⌜·⌝]. Used inside [hfupd_mono]
+      to mirror the original [apply pure_mono] step under [step_fupdN_mono]. *)
+  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.
 
   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⌝ -∗ |={0; ∅|}=> ▷^(S n) ◇ ⌜pgl (f a) T ε'⌝) -∗
+    |={0; ∅|}=> ▷^(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ε' HR) "H".
+    iApply (hfupd_mono _ _ (▷^(S n) ◇ ⌜∀ a, R a → pgl (f a) T ε'⌝)%I).
+    { apply (laterN_except_0_pure_mono (S n)). intros Hall. eapply pgl_dbind; eauto. }
+    iIntros (a HRa). iApply ("H" with "[//]").
   Qed.
 
   Lemma pgl_dbind_adv' `{Countable A, Countable A'}
@@ -38,278 +40,282 @@ 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⌝ -∗ |={0; ∅|}=> ▷^(S n) ◇ ⌜pgl (f a) T (ε' a)⌝) -∗
+    |={0; ∅|}=> ▷^(S n) ◇ ⌜pgl (dbind f μ) T (ε + SeriesC (λ a : A, (μ a * ε' a)%R))⌝.
   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.
+    iIntros (Hε [r Hr] HR) "H".
+    iApply (hfupd_mono _ _ (▷^(S n) ◇ ⌜∀ a, R a → pgl (f a) T (ε' a)⌝)%I).
+    { apply (laterN_except_0_pure_mono (S n)). intros Hall.
+      eapply pgl_dbind_adv; [done|exists r; done|done|done]. }
+    iIntros (a HRa). iApply ("H" with "[//]").
   Qed.
 
+  Local Definition cfgO := (prodO exprO stateO).
 
+  (** [glm_erasure] in hfupd 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, σ)) φ ε⌝.
+        |={0; ∅|}=> ▷^(S n) ◇ ⌜pgl (exec n (e2, σ2)) φ ε'⌝)
+      ⊢ |={0; ∅|}=> ▷^(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⌝ -∗
+                  |={0; ∅|}=> ▷^(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)).
+                   |={0; ∅|}=> ▷^(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.
+      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.
+      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 _ (λ _ _,
+                     |={0; ∅|}=> ▷^(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.
+        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".
   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 (ε : nonnegreal) (e : expr) (σ : state) n φ :
+    state_interp σ ∗ err_interp ε ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+    |={0; ⊤|}=> ▷^n ◇ ⌜pgl (exec n (e, σ)) φ ε⌝.
   Proof.
-    iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
+    iInduction n as [|n] "IH" forall (e σ ε); iIntros "(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" with "[$Hσ $Hε]").
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ∅ _
+          ⌜pgl (prim_step e σ ≫= exec n) φ ε⌝
+          with "[$Hwp]"); first lia.
+        iIntros (l Hl) "Hlift". assert (l = 0%nat) as -> by lia.
+        rewrite Nat.add_0_r. replace (S n - 0)%nat with (S n) by lia.
+        (* Convert the glm payload into the hfupd-form expected by glm_erasure *)
         iPoseProof
-          (glm_mono _ (λ '(e2, σ2) ε', |={∅}▷=>^(S n)
-             ⌜pgl (exec n (e2, σ2)) φ ε'⌝)%I
+          (glm_mono _ (λ '(e2, σ2) ε2, |={0; ∅|}=> ▷^(S n)
+             ◇ ⌜pgl (exec n (e2, σ2)) φ ε2⌝)%I
             with "[%] [] 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' σ'] ε2) "H".
+          iApply (laterN_hfupd 1). iNext.
+          iApply (elim_fupd_hfupd_plain n 0 ∅ ⊤
+            (state_interp σ' ∗ err_interp ε2 ∗ WP e' {{ v, ⌜φ v⌝ }})%I
+            ⌜pgl (exec n (e', σ')) φ ε2⌝); first lia.
+          iSplitL "H"; [iApply "H"|].
+          iIntros (l' Hl') "(Hσ' & Hε' & Hwp')".
+          assert (l' = 0%nat) as -> by lia.
+          rewrite Nat.add_0_r. replace (n - 0)%nat with n by lia.
+          iApply ("IH" with "[$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 - ε⌝.
+        |={0; ∅|}=> ▷^(S n) ◇ ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε'⌝)
+      ⊢ |={0; ∅|}=> ▷^(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⌝ -∗
+                 |={0; ∅|}=> ▷^(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)).
+                   |={0; ∅|}=> ▷^(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⌝ -∗
+          |={0; ∅|}=> ▷^(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.
+      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 +331,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 +352,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,
+          (|={0; ∅|}=> ▷^(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.
+      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)
+                     |={0; ∅|}=> ▷^(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 +397,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 +416,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 +431,97 @@ 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⌝ -∗
+             |={0; ∅|}=> ▷^(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.
+        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 (ε : nonnegreal) (e : expr) (σ : state) n φ :
+    state_interp σ ∗ err_interp ε ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+    |={0; ⊤|}=> ▷^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.
+    iInduction n as [|n] "IH" forall (e σ ε); iIntros "(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" with "[$Hσ $Hε]").
+        iApply (elim_fupd_hfupd_plain (S n) 0 ⊤ ∅ _
+          ⌜SeriesC (iterM (S n) prim_step_or_val (e, σ)) >= 1 - ε⌝); first lia.
+        iSplitL "Hwp"; [iApply "Hwp"|].
+        iIntros (l Hl) "Hlift". assert (l = 0%nat) as -> by lia.
+        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
+          (glm_mono _ (λ '(e2, σ2) ε2, |={0; ∅|}=> ▷^(S n) ◇
+             ⌜SeriesC (iterM n prim_step_or_val (e2, σ2)) >= 1 - ε2⌝)%I
             with "[%] [] Hlift") as "H".
         { apply Rle_refl. }
-        { iIntros ([] ?) "H !> !>".
-          iMod "H" as "(Hstate & Herr_auth & Hwp)".
-          iMod ("IH" with "[$]") as "H".
-          iModIntro. done. }
+        { iIntros ([e' σ'] ε2) "H".
+          iApply (laterN_hfupd 1). iNext.
+          iApply (elim_fupd_hfupd_plain n 0 ∅ ⊤
+            (state_interp σ' ∗ err_interp ε2 ∗ WP e' {{ v, ⌜φ v⌝ }})%I
+            ⌜SeriesC (iterM n prim_step_or_val (e', σ')) >= 1 - ε2⌝); first lia.
+          iSplitL "H"; [iApply "H"|].
+          iIntros (l' Hl') "(Hσ' & Hε' & Hwp')".
+          assert (l' = 0%nat) as -> by lia.
+          rewrite Nat.add_0_r. replace (n - 0)%nat with n by lia.
+          iApply ("IH" with "[$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 +542,25 @@ 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]. }
+  iMod (hfupd_soundness HasLc 0 ⊤) as (Hinv) "(_ & Hhfupd)".
+  iApply "Hhfupd".
+  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 ε' e σ n φ) as "H".
+  iApply "H".
+  iFrame "Hs". rewrite /state_interp /=. iFrame "Hh Ht".
+  iApply Hwp. iApply "Hf".
 Qed.
 
 Lemma pgl_closed_lim (e : expr) (σ : state) (ε : R) φ :
@@ -615,27 +604,27 @@ 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. }
+  iMod (hfupd_soundness HasLc 0 ⊤) as (Hinv) "(_ & Hhfupd)".
+  iApply "Hhfupd".
+  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 ε' e σ n φ) as "H".
+  iApply "H".
+  iFrame "Hs". rewrite /state_interp /=. iFrame "Hh Ht".
+  iApply Hwp. iApply "Hf".
 Qed.
 
 Lemma pexec_safety_relate (e:expr) σ n:
diff --git a/theories/eris/primitive_laws.v b/theories/eris/primitive_laws.v
index b67cf0960..26b6e454c 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;
@@ -34,7 +34,7 @@ Definition tapes_auth `{erisGS Σ} :=
 
 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 ε);
 }.
 
diff --git a/theories/eris/total_adequacy.v b/theories/eris/total_adequacy.v
index 6ebffce30..a599b913c 100644
--- a/theories/eris/total_adequacy.v
+++ b/theories/eris/total_adequacy.v
@@ -249,30 +249,36 @@ 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⌝ -∗ |={0; ∅|}=> ◇ ⌜tgl (f a) T ε'⌝) -∗
+    |={0; ∅|}=> ◇ ⌜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 (hfupd_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, σ)) φ ε⌝.
+    |={0; ⊤|}=> ◇ ⌜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.
+                                  state_interp a -∗ err_interp a0 -∗
+                                  |={0; ⊤|}=> ◇ ⌜tgl (lim_exec (e, a)) φ a0⌝)%I) as H.
+    iApply H.
     2: { destruct twp_default. done. }
     clear H e.
     iModIntro.
@@ -280,9 +286,11 @@ Section adequacy.
     iIntros (σ ε) "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.
@@ -292,75 +300,114 @@ Section adequacy.
         case_bool_decide; try lra. done. }
       simpl. rewrite H. by rewrite dret_mass.
     - iSpecialize ("H" $! σ ε with "[$]").
-      iMod "H".
+      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⌝ -∗
+                  |={0; ∅|}=> ◇ ⌜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 (hfupd_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 hfupd_forall_2. 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⌝ ={0; ∅|}=∗
+                  ◇ ⌜tgl (lim_exec (e, σ)) φ ε''⌝) ∧
+                 glm e σ ε''
+                   (λ '(e2, σ2) (ε2 : nonnegreal),
+                      |={∅,⊤}=> state_interp σ2 ∗ err_interp ε2 ∗
+                        ∀ (a : state) (a0 : nonnegreal),
+                          state_interp a -∗ err_interp a0 ={0; ⊤|}=∗
+                          ◇ ⌜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 (hfupd_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 (hfupd_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⌝ -∗
+          |={0; ∅|}=> ◇ ⌜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 σ2 ∗ err_interp ε' ∗
+                    ∀ (a : state) (a0 : nonnegreal),
+                      state_interp a -∗ err_interp a0 ={0; ⊤|}=∗
+                      ◇ ⌜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 (hfupd_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 σ2 ∗ err_interp ε2' ∗
+              (∀ (a : state) (a0 : nonnegreal),
+                state_interp a -∗ err_interp a0 ={0; ⊤|}=∗
+                ◇ ⌜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'" $! σ2 ε2' with "Hσ' Hε'").
+          iApply (hfupd_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 (hfupd_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 (hfupd_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⌝ -∗
+                   |={0; ∅|}=> ◇ ⌜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⌝ ={0; ∅|}=∗
+                    ◇ ⌜tgl (lim_exec (e, σ2)) φ ε2'⌝) ∧
+                   glm e σ2 ε2'
+                     (λ '(e2, σ2') (ε2'' : nonnegreal),
+                        |={∅,⊤}=> state_interp σ2' ∗ err_interp ε2'' ∗
+                          ∀ (a : state) (a0 : nonnegreal),
+                            state_interp a -∗ err_interp a0 ={0; ⊤|}=∗
+                            ◇ ⌜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 (hfupd_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 (hfupd_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 (hfupd_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 (hfupd_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. }
+  iMod (hfupd_soundness HasLc 0 ⊤) as (Hinv) "(_ & Hhfupd)".
+  iApply "Hhfupd".
+  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 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/weakestpre.v b/theories/eris/weakestpre.v
index 880ca4e5a..be69ba253 100644
--- a/theories/eris/weakestpre.v
+++ b/theories/eris/weakestpre.v
@@ -21,7 +21,7 @@ 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 Σ;
+  erisWpGS_invGS :: invGS_gen HasLc Σ;
   state_interp : state Λ → iProp Σ;
   err_interp : nonnegreal → iProp Σ;
 }.
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..eb2bff549 100644
--- a/theories/prelude/iris_ext.v
+++ b/theories/prelude/iris_ext.v
@@ -26,6 +26,22 @@ 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 Hiter.
+    apply (laterN_soundness _ (S (m + n))).
+    rewrite laterN_later -except_0_into_later.
+    iMod (hfupd_soundness HasNoLc m ⊤) as (Hinv) "(Hlc & Hhfupd)".
+    iPoseProof (Hiter Hinv with "Hlc") as "Hupd".
+    iApply "Hhfupd".
+    iHFupdElimFupd "Hupd" as "Hupd"; first lia.
+    iApply (elim_step_fupdN_hfupd_plain (m - _) (m + n - _) n ∅ P P); [lia|].
+    iSplitL "Hupd"; [iApply "Hupd"|].
+    iIntros (l Hl) "HP". iApply hfupd_intro. iApply laterN_intro.
+    by iApply except_0_intro.
+  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/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
 }.