diff --git a/CHANGELOG.md b/CHANGELOG.md
index e99eb4a39663e16e923ee8869ec0a32bbbc5470b..8adfc4fcfa4eaa89a9ed05a4e140ef290276fa16 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,28 @@ s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
 EOF
 ```
 
+**Changes in `base_logic`:**
+
+* The soundness lemma of the base logic `step_fupdN_soundness`, has been
+generalized. It now states the soundness of the logic even if invariants stay
+open accross an arbitrary number of laters.
+
+**Changes in `program_logic`:**
+
+* The definition of weakest precondition has been changed in order to use
+a variable number of laters (i.e., logical steps) for each physical step of
+the operational semantics, depending on the number of physical steps executed
+since the begining of the execution of the program. See merge request !595.
+This implies several API-breaking changes, which can be easily fixed in client
+formalizations in a backward compatible manner as follows:
+   - Ignore the new parameter `ns` in the state interpretation, which
+     corresponds to a step counter.
+   - Use the constant function "0" for the new field `num_laters_per_step` of
+     `irisG`.
+   - Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
+   - Some proofs using lifting lemmas and adequacy theorems need to be adapted
+     to ignore the new step counter.
+
 ## Iris 3.4.0
 
 The highlights and most notable changes of this release are as follows:
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 5471682dbba9a32b6a991b771be7ec65fe2d8943..c7d7a40503bc53986c448e1c2a71e6b4bbe37134 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -71,28 +71,26 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
-  destruct n as [|n].
-  - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
-  - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
-    { by iApply fupd_plain_mask_empty. }
-    rewrite -step_fupdN_S_fupd.
-    iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
-    rewrite -later_laterN laterN_later.
-    iNext. by iMod "Hφ".
+  iApply fupd_plainly_mask_empty. iMod "H".
+  iMod (step_fupdN_plain with "H") as "H". iModIntro.
+  rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
+  iNext. iMod "H" as %Hφ. auto.
 Qed.
 
 Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
   (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness _ n).
-  iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_intro_discard.
+  iIntros (Hiter). eapply (step_fupdN_soundness _ n)=>Hinv. destruct n as [|n].
+  { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
+   simpl in Hiter |- *. iMod Hiter as "H". iIntros "!>!>!>".
+  iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
+  simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 60c88f31cb2f930a13e13916dd156fbf1ef6f8b4..435c788c7b41aa6a986a361f78ddf93ab11d67f0 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -370,6 +370,16 @@ Section fupd_derived.
     rewrite {4}(union_difference_L _ _ HE). done.
   Qed.
 
+  Lemma fupd_mask_subseteq_emptyset_difference E1 E2 :
+    E2 ⊆ E1 →
+    ⊢@{PROP} |={E1, E2}=> |={∅, E1∖E2}=> emp.
+  Proof.
+    intros ?. rewrite [in fupd E1](union_difference_L E2 E1); [|done].
+    rewrite (comm_L (∪))
+      -[X in fupd _ X](left_id_L ∅ (∪) E2) -fupd_mask_frame_r; [|set_solver+].
+    apply fupd_mask_intro_subseteq; set_solver.
+  Qed.
+
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
 
@@ -460,6 +470,12 @@ Section fupd_derived.
     by apply sep_mono; first apply later_intro.
   Qed.
 
+  Lemma step_fupdN_intro Ei Eo n P : Ei ⊆ Eo → ▷^n P -∗ |={Eo}[Ei]▷=>^n P.
+  Proof.
+    induction n as [|n IH]=> ?; [done|].
+    rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
+  Qed.
+
   Lemma step_fupdN_S_fupd n E P :
     (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 356b7ff7556b9da5d56b9aaab8e1c6139ea25792..32c05e909f07d697840d2bf961ab0e4e3c5405ab 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -7,6 +7,7 @@ Import uPred.
 
 (** This file contains the adequacy statements of the Iris program logic. First
 we prove a number of auxilary results. *)
+
 Section adequacy.
 Context `{!irisG Λ Σ}.
 Implicit Types e : expr Λ.
@@ -16,84 +17,96 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 
 Notation wptp s t Φs := ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
 
-Lemma wp_step s e1 σ1 κ κs e2 σ2 efs nt Φ :
+Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
-    state_interp σ2 κs (nt + length efs) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗
+  state_interp σ1 ns (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }}
+    ={⊤,∅}=∗ |={∅}▷=>^(S $ num_laters_per_step ns) |={∅,⊤}=>
+    state_interp σ2 (S ns) κs (nt + length efs) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗
     wptp s efs (replicate (length efs) fork_post).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
-  iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
-  iMod ("H" $! e2 σ2 efs with "[//]") as "H".
+  iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
+  iApply (step_fupdN_wand with "[H]"); first by iApply "H". iIntros ">H".
   by rewrite Nat.add_comm big_sepL2_replicate_r.
 Qed.
 
-Lemma wptp_step s es1 es2 κ κs σ1 σ2 Φs nt :
+Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
   step (es1,σ1) κ (es2, σ2) →
-  state_interp σ1 (κ ++ κs) nt -∗ wptp s es1 Φs -∗
-  ∃ nt', |={⊤}[∅]▷=> state_interp σ2 κs (nt + nt') ∗
+  state_interp σ1 ns (κ ++ κs) nt -∗ wptp s es1 Φs -∗
+  ∃ nt', |={⊤,∅}=> |={∅}▷=>^(S $ num_laters_per_step$ ns) |={∅,⊤}=>
+         state_interp σ2 (S ns) κs (nt + nt') ∗
          wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
   iIntros (Hstep) "Hσ Ht".
   destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
   iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
   iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
-  iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done.
-  iIntros "!> !>". iMod "H" as "($ & He2 & Hefs)". iIntros "!>".
+  iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done. iModIntro.
+  iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
   rewrite -(assoc_L app) -app_comm_cons. iFrame.
 Qed.
 
-Lemma wptp_steps s n es1 es2 κs κs' σ1 σ2 Φs nt :
+(* The total number of laters used between the physical steps number
+   [start] (included) to [start+ns] (excluded). *)
+Local Fixpoint steps_sum (num_laters_per_step : nat → nat) (start ns : nat) : nat :=
+  match ns with
+  | O => 0
+  | S ns =>
+    S $ num_laters_per_step start + steps_sum num_laters_per_step (S start) ns
+  end.
+
+Lemma wptp_steps s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
   nsteps n (es1, σ1) κs (es2, σ2) →
-  state_interp σ1 (κs ++ κs') nt -∗ wptp s es1 Φs
-  ={⊤}[∅]▷=∗^n ∃ nt',
-    state_interp σ2 κs' (nt + nt') ∗ wptp s es2 (Φs ++ replicate nt' fork_post).
+  state_interp σ1 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
+    state_interp σ2 (n + ns) κs' (nt + nt') ∗
+    wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
-  revert nt es1 es2 κs κs' σ1 σ2 Φs.
-  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 σ2 Φs /=.
+  revert nt es1 es2 κs κs' σ1 ns σ2 Φs.
+  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
   { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
-    rewrite Nat.add_0_r right_id_L. by iFrame. }
+    rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
   iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite -(assoc_L (++)).
+  rewrite -(assoc_L (++)) Nat_iter_add plus_n_Sm.
   iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
-  iIntros "!> !>". iMod "H" as "(Hσ & He)". iModIntro.
-  iApply (step_fupdN_wand with "[Hσ He]"); first by iApply (IH with "Hσ He").
-  iDestruct 1 as (nt'') "[??]". rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus.
-  by eauto with iFrame.
+  iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
+  iIntros ">(Hσ & He)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
+  iApply (step_fupdN_wand with "IH"). iIntros ">IH".
+  iDestruct "IH" as (nt'') "[??]".
+  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
 Qed.
 
-Lemma wp_not_stuck κs nt e σ Φ :
-  state_interp σ κs nt -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
+Lemma wp_not_stuck κs nt e σ ns Φ :
+  state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?; first by eauto.
-  iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
+  iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
   iMod (fupd_plain_mask with "H") as %?; eauto.
 Qed.
 
-Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 σ2 nt:
+Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 ns σ2 nt:
   nsteps n (es1, σ1) κs (es2, σ2) →
-  state_interp σ1 (κs ++ κs') nt -∗
-  wptp s es1 Φs ={⊤}[∅]▷=∗^(S n) ∃ nt',
+  state_interp σ1 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝ ∗
-    state_interp σ2 κs' (nt + nt') ∗
+    state_interp σ2 (n + ns) κs' (nt + nt') ∗
     [∗ list] e;Φ ∈ es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
 Proof.
-  iIntros (Hstep) "Hσ He". rewrite Nat_iter_S_r.
-  iDestruct (wptp_steps with "Hσ He") as "Hwp"; first done.
-  iApply (step_fupdN_wand with "Hwp").
-  iDestruct 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
+  iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
+  iModIntro. iApply (step_fupdN_wand with "Hwp").
+  iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
   iMod (fupd_plain_keep_l ⊤
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
-    (state_interp σ2 κs' (nt + nt') ∗ wptp s es2 (Φs ++ replicate nt' fork_post))%I
+    (state_interp σ2 (n + ns) κs' (nt + nt') ∗
+     wptp s es2 (Φs ++ replicate nt' fork_post))%I
     with "[$Hσ $Ht]") as "(%&Hσ&Hwp)".
   { iIntros "(Hσ & Ht)" (e' -> He').
     move: He' => /(elem_of_list_split _ _)[?[?->]].
     iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ?) "[? Hwp]".
     iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
     iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
-  iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
   iExists _. iSplitR; first done. iFrame "Hσ".
   iApply big_sepL2_fupd.
   iApply (big_sepL2_impl with "Hwp").
@@ -104,15 +117,19 @@ Qed.
 End adequacy.
 
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
+        (num_laters_per_step : nat → nat) :
   (∀ `{Hinv : !invG Σ},
     ⊢ |={⊤}=> ∃
          (s: stuckness)
-         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
-         (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
-       stateI σ1 κs 0 ∗
+         (fork_post : val Λ → iProp Σ)
+         state_interp_mono,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+                                  state_interp_mono
+       in
+       stateI σ1 0 κs 0 ∗
        ([∗ list] e;Φ ∈ es;Φs, WP e @ s; ⊤ {{ Φ }}) ∗
        (∀ es' t2',
          (* es' is the final state of the initial threads, t2' the rest *)
@@ -123,7 +140,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
          threads in [t2] are not stuck *)
          ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2 ⌝ -∗
          (* The state interpretation holds for [σ2] *)
-         stateI σ2 [] (length t2') -∗
+         stateI σ2 n [] (length t2') -∗
          (* If the initial threads are done, their post-condition [Φ] holds *)
          ([∗ list] e;Φ ∈ es';Φs, from_option Φ True (to_val e)) -∗
          (* For all forked-off threads that are done, their postcondition
@@ -138,19 +155,22 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
   φ.
 Proof.
   intros Hwp ?.
-  eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
-  iMod Hwp as (s stateI Φ fork_post) "(Hσ & Hwp & Hφ)".
+  apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n))=> Hinv.
+  iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
-  iApply step_fupd_intro; [done|]; iModIntro.
-  iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "[-Hφ]").
-  { iApply (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI fork_post) _ []
-    with "[Hσ] Hwp"); eauto; by rewrite right_id_L. }
-  iDestruct 1 as (nt' ?) "(Hσ & Hval) /=".
+  iMod (@wptp_strong_adequacy _ _
+       (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
+    with "[Hσ] Hwp") as "H"; [done|by rewrite right_id_L|].
+  iAssert (|={∅}▷=>^(steps_sum num_laters_per_step 0 n) |={∅}=> ⌜φ⌝)%I
+    with "[-]" as "H"; last first.
+  { destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
+  iApply (step_fupdN_wand with "H").
+  iMod 1 as (nt' ?) "(Hσ & Hval) /=".
   iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
   iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
   rewrite replicate_length in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
-  iApply fupd_plain_mask_empty.
+  rewrite -plus_n_O.
   iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
   by rewrite big_sepL2_replicate_r // big_sepL_omap.
 Qed.
@@ -199,14 +219,17 @@ Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) fork_post in
+       let _ : irisG Λ Σ :=
+           IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
+                 (λ _ _ _ _, fupd_intro _ _)
+       in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
   eapply (wp_strong_adequacy Σ _); [|done]=> ?.
   iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
-  iExists s, (λ σ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post => /=.
+  iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
   iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
@@ -219,7 +242,8 @@ Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
+       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
+              (λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
        stateI σ1 κs 0 ∗ WP e1 @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝)) →
   rtc erased_step ([e1], σ1) (t2, σ2) →
@@ -228,7 +252,7 @@ Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
   eapply (wp_strong_adequacy Σ _); [|done]=> ?.
   iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
-  iExists s, stateI, [(λ _, True)%I], fork_post => /=.
+  iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
   iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
   iDestruct (big_sepL2_nil_inv_r with "H") as %->.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 189a1a216f8f216c771d69e023e41a779d1ee8c1..468b0bfa6b6c5bf684ff6f91d1c1abda6a8fb594 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -17,15 +17,15 @@ Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 ns κ κs nt) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
   iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
   iApply "H"; eauto.
@@ -33,26 +33,26 @@ Qed.
 
 Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
+  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?????) "?".
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
   to_val e = None →
   sub_redexes_are_values e →
-  (∀ σ κs n, state_interp σ κs n ={E,∅}=∗ ⌜head_stuck e σ⌝)
+  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜head_stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros (??) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
+  iIntros (σ ns κs nt) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
 Qed.
 
 Lemma wp_lift_pure_head_stuck E Φ e :
@@ -62,51 +62,51 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   ⊢ WP e @ E ?{{ Φ }}.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ κs n) "_". iApply fupd_mask_intro; by auto with set_solver.
+  iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; by auto with set_solver.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iIntros (v2 σ2 efs Hstep).
   iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
   iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
@@ -114,14 +114,14 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs Hstep).
   iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
 Qed.
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index ac6e173053892bc6321cb9b5af74a08115e3541b..1a5aaca96a2652cb503d9b8e65a4cc6dfe685a18 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -16,23 +16,38 @@ Implicit Types Φ : val Λ → iProp Σ.
 
 Local Hint Resolve reducible_no_obs_reducible : core.
 
+Lemma wp_lift_step_fupdN s E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝
+      ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
+      WP e2 @ s; E {{ Φ }} ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
+
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
-Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
+Proof.
+  intros ?. rewrite -wp_lift_step_fupdN; [|done]. simpl. do 22 f_equiv.
+  rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro. auto.
+Qed.
 
 Lemma wp_lift_stuck E Φ e :
   to_val e = None →
-  (∀ σ κs n, state_interp σ κs n ={E,∅}=∗ ⌜stuck e σ⌝)
+  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 ns κ κs nt) "Hσ".
   iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
   iIntros (e2 σ2 efs ?). by case: (Hirr κ e2 σ2 efs).
 Qed.
@@ -40,15 +55,15 @@ Qed.
 (** Derived lifting lemmas. *)
 Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ 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]". iIntros "!> * % !> !>". by iApply "H".
 Qed.
 
@@ -60,13 +75,14 @@ Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
-  iIntros (σ1 κ κs n) "Hσ". iMod "H".
+  iIntros (σ1 ns κ κs nt) "Hσ". iMod "H".
   iApply fupd_mask_intro; first set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; done. }
   iNext. iIntros (e2 σ2 efs ?).
   destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
+  iMod (state_interp_mono with "Hσ") as "$".
   iMod "Hclose" as "_". iMod "H". iModIntro.
-  iDestruct ("H" with "[//]") as "H". simpl. iFrame.
+  by iDestruct ("H" with "[//]") as "$".
 Qed.
 
 Lemma wp_lift_pure_stuck `{!Inhabited (state Λ)} E Φ e :
@@ -76,23 +92,23 @@ Proof.
   iIntros (Hstuck) "_". iApply wp_lift_stuck.
   - destruct(to_val e) as [v|] eqn:He; last done.
     rewrite -He. by case: (Hstuck inhabitant).
-  - iIntros (σ κs n) "_". iApply fupd_mask_intro; auto with set_solver.
+  - iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; auto with set_solver.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H".
-  iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs n) "Hσ1".
+  iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 ns κ κs nt) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iApply fupd_mask_intro; first set_solver.
   iIntros "Hclose" (e2 σ2 efs ?). iMod "Hclose" as "_".
@@ -105,16 +121,16 @@ Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (????) "?". iMod ("H" with "[$]") as "[$ H]".
+  iIntros (?????) "?". iMod ("H" with "[$]") as "[$ H]".
   iIntros "!> *". iIntros (Hstep) "!> !>".
   by iApply "H".
 Qed.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index bbd50bc3ba84d2df311b69051aed17e9e6f97f6d..b160c1b62ee6662e4b888d574a314be56fd41746 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -22,8 +22,10 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
 
 Global Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
   iris_invG := ownP_invG;
-  state_interp σ κs _ := own ownP_name (●E σ)%I;
+  state_interp σ _ κs _ := own ownP_name (●E σ)%I;
   fork_post _ := True%I;
+  num_laters_per_step _ := 0;
+  state_interp_mono _ _ _ _ := fupd_intro _ _
 }.
 Global Opaque iris_invG.
 
@@ -87,7 +89,8 @@ Section lifting.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
+  Lemma ownP_eq σ1 ns σ2 κs nt :
+    state_interp σ1 ns κs nt -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
     by iDestruct (own_valid_2 with "Hσ● Hσ◯")
@@ -113,7 +116,7 @@ Section lifting.
       iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
       destruct s; last done. apply reducible_not_val in Hred.
       move: Hred; by rewrite to_of_val.
-    - iApply wp_lift_step; [done|]; iIntros (σ1 κ κs n) "Hσκs".
+    - iApply wp_lift_step; [done|]; iIntros (σ1 ns κ κs nt) "Hσκs".
       iMod "H" as (σ1' ?) "[>Hσf H]".
       iDestruct (ownP_eq with "Hσκs Hσf") as %<-.
       iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
@@ -131,7 +134,7 @@ Section lifting.
     - apply of_to_val in EQe as <-. iApply fupd_wp.
       iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
       by rewrite to_of_val in Hnv.
-    - iApply wp_lift_stuck; [done|]. iIntros (σ1 κs n) "Hσ".
+    - iApply wp_lift_stuck; [done|]. iIntros (σ1 ns κs nt) "Hσ".
       iMod "H" as (σ1') "(% & >Hσf)".
       by iDestruct (ownP_eq with "Hσ Hσf") as %->.
   Qed.
@@ -146,7 +149,7 @@ Section lifting.
     iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-    iIntros (σ1 κ κs n) "Hσ". iApply fupd_mask_intro; first set_solver.
+    iIntros (σ1 ns κ κs nt) "Hσ". iApply fupd_mask_intro; first set_solver.
     iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index a717aa5700454100ffc787dd68558dad946e2062..2695ce19cb064b66a4386e8a2745b0e81fb929fe 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -11,15 +11,16 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 κ κs σ2 n, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
-    state_interp σ1 κs n ={⊤}=∗ ∃ n', ⌜κ = []⌝ ∗ state_interp σ2 κs n' ∗ twptp t2)%I.
+  (∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
+    state_interp σ1 ns κs nt ={⊤}=∗
+              ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
     ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
-  iIntros (t2 σ1 κ κs σ2 n1) "Hstep Hσ".
+  iIntros (t2 σ1 ns κ κs σ2 nt1) "Hstep Hσ".
   iMod ("Hwp" with "[$] [$]") as (n2) "($ & Hσ & ?)".
   iModIntro. iExists n2. iFrame "Hσ". by iApply "H".
 Qed.
@@ -50,7 +51,7 @@ Local Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
 Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
-  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt Hstep) "Hσ".
   destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); [done..|].
   iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
   iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
@@ -62,7 +63,7 @@ Proof.
   iApply twptp_ind; iIntros "!>" (t1) "IH1". iIntros (t2) "H2".
   iRevert (t1) "IH1"; iRevert (t2) "H2".
   iApply twptp_ind; iIntros "!>" (t2) "IH2". iIntros (t1) "IH1".
-  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1".
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 ns κ κs σ2 nt Hstep) "Hσ1".
   destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=.
   apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
@@ -86,27 +87,28 @@ Proof.
   iIntros "He". remember (⊤ : coPset) as E eqn:HE.
   iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
   iIntros "!>" (e E Φ); iIntros "IH" (->).
-  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ2' n Hstep) "Hσ1".
+  rewrite twptp_unfold /twptp_pre /twp_pre.
+  iIntros (t1' σ1' ns κ κs σ2' nt Hstep) "Hσ1".
   destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
     simplify_eq/=; try discriminate_list.
   destruct (to_val e1) as [v|] eqn:He1.
   { apply val_stuck in Hstep; naive_solver. }
   iMod ("IH" with "Hσ1") as "[_ IH]".
   iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
-  iModIntro. iExists (length efs + n). iFrame "Hσ".
+  iModIntro. iExists (length efs + nt). iFrame "Hσ".
   iApply (twptp_app [_] with "(IH [//])").
   clear. iInduction efs as [|e efs] "IH"; simpl.
-  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n1 Hstep).
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt1 Hstep).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
   iApply (twptp_app [_] with "(IH' [//])"). by iApply "IH".
 Qed.
 
-Lemma twptp_total n σ t :
-  state_interp σ [] n -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
+Lemma twptp_total σ ns nt t :
+  state_interp σ ns [] nt -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
-  iIntros "Hσ Ht". iRevert (σ n) "Hσ". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!>" (t) "IH"; iIntros (σ n) "Hσ".
+  iIntros "Hσ Ht". iRevert (σ ns nt) "Hσ". iRevert (t) "Ht".
+  iApply twptp_ind; iIntros "!>" (t) "IH"; iIntros (σ ns nt) "Hσ".
   iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
   rewrite /twptp_pre.
   iMod ("IH" with "[% //] Hσ") as (n' ->) "[Hσ [H _]]".
@@ -119,13 +121,17 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
+       let _ : irisG Λ Σ :=
+           IrisG _ _ Hinv (λ σ _, stateI σ) fork_post (λ _, 0)
+                 (λ _ _ _ _, fupd_intro _ _)
+       in
        stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }]) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iMod (Hwp) as (stateI fork_post) "[Hσ H]".
-  iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
-  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)).
+  iApply (@twptp_total _ _ (IrisG _ _ Hinv (λ σ _, stateI σ) fork_post _ _)
+                       _ 0 with "Hσ").
+  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv _ fork_post _ _)).
 Qed.
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 0f7147c5a8bb7994519d549c5c65ee51e9d2d73d..35d776409cc259cc1617f48f157ef21c1868ee0e 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -14,17 +14,17 @@ Local Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
 
 Lemma twp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs n, state_interp σ1 κs n ={E,∅}=∗
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E,∅}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       ⌜κ = []⌝ ∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E [{ Φ }] ∗
       [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".
-  iApply (twp_lift_step _ E)=>//. iIntros (σ1 κs n) "Hσ".
+  iApply (twp_lift_step _ E)=>//. iIntros (σ1 ns κs nt) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
   iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
   iApply "H". by eauto.
@@ -42,30 +42,31 @@ Qed.
 
 Lemma twp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       ⌜κ = []⌝ ∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
-  iIntros (σ1 κs n) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
 Qed.
 
 Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
+      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt
+                            ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
-  iIntros (σ1 κs n) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iIntros (κ v2 σ2 efs Hstep).
   iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
 Qed.
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index c24d7127e12a2c75fdafd799cc467c50ae7c6236..101bf4d62f83e8fed0369015956ef499e1f99ee7 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -15,11 +15,11 @@ Local Hint Resolve reducible_no_obs_reducible : core.
 
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κs n, state_interp σ1 κs n ={E,∅}=∗
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E,∅}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       ⌜κ = []⌝ ∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E [{ Φ }] ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
@@ -34,11 +34,11 @@ Lemma twp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E Φ e1 :
 Proof.
   iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
   { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
-  iIntros (σ1 κs n) "Hσ".
+  iIntros (σ1 ns κs n) "Hσ".
   iApply fupd_mask_intro; first by set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; auto. }
   iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
-  iMod "Hclose" as "_". iModIntro.
+  iMod (state_interp_mono with "Hσ"). iMod "Hclose" as "_".
   iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
 Qed.
 
@@ -46,17 +46,17 @@ Qed.
    use the generic lemmas here. *)
 Lemma twp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       ⌜κ = []⌝ ∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".
-  iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs n) "Hσ1".
+  iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 ns κs nt) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iApply fupd_mask_intro; first set_solver.
   iIntros "Hclose" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index f3458227f1be8a07e684f883c0ad289cbc2e296b..6278dc971dbcbdf978cf2e3ac32a194514af81c8 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -13,12 +13,12 @@ Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 κs n,
-     state_interp σ1 κs n ={E,∅}=∗
+  | None => ∀ σ1 ns κs nt,
+     state_interp σ1 ns κs nt ={E,∅}=∗
        ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
        ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
          ⌜κ = []⌝ ∗
-         state_interp σ2 κs (length efs + n) ∗
+         state_interp σ2 (S ns) κs (length efs + nt) ∗
          wp E e2 Φ ∗
          [∗ list] ef ∈ efs, wp ⊤ ef fork_post
   end%I.
@@ -32,7 +32,7 @@ Lemma twp_pre_mono `{!irisG Λ Σ} s
 Proof.
   iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
   destruct (to_val e1) as [v|]; first done.
-  iIntros (σ1 κs n) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
+  iIntros (σ1 ns κs nt) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
   iIntros (κ e2 σ2 efs) "Hstep".
   iMod ("Hwp" with "Hstep") as (?) "(Hσ & Hwp & Hfork)".
   iModIntro. iFrame "Hσ". iSplit; first done. iSplitL "Hwp".
@@ -54,7 +54,7 @@ Proof.
     iApply twp_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 /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
+    rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
 Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
@@ -115,7 +115,7 @@ Proof.
   iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κs n) "Hσ".
+  iIntros (σ1 ns κs nt) "Hσ".
   iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("IH" with "[$]") as "[% IH]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
@@ -131,7 +131,7 @@ Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) -∗ WP e @ s; E [{ Φ
 Proof.
   rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κs n) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 ns κs nt) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] -∗ WP e @ s; E [{ Φ }].
 Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
@@ -142,7 +142,7 @@ Proof.
   iIntros "H". rewrite !twp_unfold /twp_pre /=.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iIntros (σ1 ns κs nt) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iIntros (κ e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as (?) "(Hσ & H & Hefs)". destruct s.
   - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
@@ -165,7 +165,8 @@ Proof.
   rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
   rewrite twp_unfold /twp_pre fill_not_val //.
-  iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 ns κs nt) "Hσ". iMod ("IH" with "[$]") as "[% IH]".
+  iModIntro; iSplit.
   { iPureIntro. unfold reducible_no_obs in *.
     destruct s; naive_solver eauto using fill_step. }
   iIntros (κ e2 σ2 efs Hstep).
@@ -186,7 +187,8 @@ Proof.
   { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
     iApply (twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". }
   rewrite /twp_pre fill_not_val //.
-  iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 ns κs nt) "Hσ". iMod ("IH" with "[$]") as "[% IH]".
+  iModIntro; iSplit.
   { destruct s; eauto using reducible_no_obs_fill_inv. }
   iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" $! κ (K e2) σ2 efs with "[]") as (?) "(Hσ & IH & IHefs)"; eauto using fill_step.
@@ -198,12 +200,14 @@ Qed.
 Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ).
-  rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
-  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
+  rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//=.
+  iIntros (σ1 ns κ κs nt) "Hσ". iMod ("H" with "Hσ") as "[% H]".
+  iIntros "!>". iSplitR.
   { destruct s; eauto using reducible_no_obs_reducible. }
   iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
-  iApply step_fupd_intro; [set_solver+|]. iNext.
-  iFrame "Hσ". iSplitL "H".
+  iApply fupd_mask_intro; [set_solver+|]. iIntros "Hclose".
+  iIntros "!>!>". iApply step_fupdN_intro=>//. iModIntro. iMod "Hclose" as "_".
+  iModIntro. iFrame "Hσ". iSplitL "H".
   { by iApply "IH". }
   iApply (@big_sepL_impl with "Hfork").
   iIntros "!>" (k ef _) "H". by iApply "IH".
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index b0880ff8fdcfe07a6d576cb564a865493ae4216e..3f97d83d401890011fe063f0bb0f7f336e3f209d 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -10,17 +10,40 @@ Import uPred.
 Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
 
-  (** The state interpretation is an invariant that should hold in between each
-  step of reduction. Here [Λstate] is the global state, [list Λobservation] are
-  the remaining observations, and [nat] is the number of forked-off threads
-  (not the total number of threads, which is one higher because there is always
-  a main thread). *)
-  state_interp : state Λ → list (observation Λ) → nat → iProp Σ;
+  (** The state interpretation is an invariant that should hold in
+  between each step of reduction. Here [Λstate] is the global state,
+  the first [nat] is the number of steps already performed by the
+  program, [list Λobservation] are the remaining observations, and the
+  last [nat] is the number of forked-off threads (not the total number
+  of threads, which is one higher because there is always a main
+  thread). *)
+  state_interp : state Λ → nat → list (observation Λ) → nat → iProp Σ;
 
   (** A fixed postcondition for any forked-off thread. For most languages, e.g.
   heap_lang, this will simply be [True]. However, it is useful if one wants to
   keep track of resources precisely, as in e.g. Iron. *)
   fork_post : val Λ → iProp Σ;
+
+  (** Number of additional logical steps (i.e., later modality in the
+  definition of WP) per physical step, depending on the physical steps
+  counter. In addition to these steps, the definition of WP adds one
+  extra later per physical step to make sure that there is at least
+  one later for each physical step. *)
+  num_laters_per_step : nat → nat;
+
+  (** When performing pure steps, the state interpretation needs to be
+  adapted for the change in the [ns] parameter.
+
+  Note that we use an empty-mask fancy update here. We could also use
+  a basic update or a bare magic wand, the expressiveness of the
+  framework would be the same. If we removed the modality here, then
+  the client would have to include the modality it needs as part of
+  the definition of [state_interp]. Since adding the modality as part
+  of the definition [state_interp_mono] does not significantly
+  complicate the formalization in Iris, we prefer simplifying the
+  client. *)
+  state_interp_mono σ ns κs nt:
+    state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
 }.
 Global Opaque iris_invG.
 
@@ -29,19 +52,25 @@ Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 κ κs n,
-     state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  | None => ∀ σ1 ns κ κs nt,
+     state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
        ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
-         state_interp σ2 κs (length efs + n) ∗
+       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝
+         ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
+         state_interp σ2 (S ns) κs (length efs + nt) ∗
          wp E e2 Φ ∗
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
 Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
 Proof.
-  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
-  repeat (f_contractive || f_equiv); apply Hwp.
+  rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
+  do 24 (f_contractive || f_equiv).
+  (* FIXME : simplify this proof once we have a good definition and a
+     proper instance for step_fupdN. *)
+  induction num_laters_per_step as [|k IH]; simpl.
+  - repeat (f_contractive || f_equiv); apply Hwp.
+  - by rewrite -IH.
 Qed.
 
 Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
@@ -70,12 +99,15 @@ Global Instance wp_ne s E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
-  rewrite !wp_unfold /wp_pre.
+  rewrite !wp_unfold /wp_pre /=.
   (* FIXME: figure out a way to properly automate this proof *)
   (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
   is very slow here *)
-  do 24 (f_contractive || f_equiv). apply IH; first lia.
-  intros v. eapply dist_le; eauto with lia.
+  do 24 (f_contractive || f_equiv).
+  (* FIXME : simplify this proof once we have a good definition and a
+     proper instance for step_fupdN. *)
+  induction num_laters_per_step as [|k IHk]; simpl; last by rewrite IHk.
+  rewrite IH; [done|lia|]. intros v. eapply dist_S, HΦ.
 Qed.
 Global Instance wp_proper s E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
@@ -86,8 +118,12 @@ Global Instance wp_contractive s E e n :
   TCEq (to_val e) None →
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
-  intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He.
-  by repeat (f_contractive || f_equiv).
+  intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He /=.
+  do 23 (f_contractive || f_equiv).
+  (* FIXME : simplify this proof once we have a good definition and a
+     proper instance for step_fupdN. *)
+  induction num_laters_per_step as [|k IHk]; simpl; last by rewrite IHk.
+  by do 4 f_equiv.
 Qed.
 
 Lemma wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
@@ -98,16 +134,16 @@ Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
   WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
 Proof.
   iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
-  rewrite !wp_unfold /wp_pre.
+  rewrite !wp_unfold /wp_pre /=.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κ κs n) "Hσ".
+  iIntros (σ1 ns κ κs nt) "Hσ".
   iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "H". iIntros "!> !>".
-  iMod "H" as "(Hσ & H & Hefs)".
-  iMod "Hclose" as "_". iModIntro. iFrame "Hσ". iSplitR "Hefs".
+  iMod ("H" with "[//]") as "H". iIntros "!> !>".  iMod "H". iModIntro.
+  iApply (step_fupdN_wand with "[H]"); first by iApply "H".
+  iIntros ">($ & H & Hefs)". iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
   - iApply (big_sepL_impl with "Hefs"); iIntros "!>" (k ef _).
     iIntros "H". iApply ("IH" with "[] H"); auto.
@@ -117,7 +153,7 @@ Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κ κs n) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
@@ -128,30 +164,54 @@ Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κ κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iIntros (σ1 ns κ κs nt) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "H". iIntros "!>!>".
-  iMod "H" as "(Hσ & H & Hefs)". destruct s.
+  iApply (step_fupdN_wand with "[H]"); first by iApply "H".
+  iIntros ">(Hσ & H & Hefs)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
-    + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+    + iMod ("H" $! _ _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
     rewrite wp_value_fupd'. iMod "H" as ">H".
     iModIntro. iFrame "Hσ Hefs". by iApply wp_value_fupd'.
 Qed.
 
-Lemma wp_step_fupd s E1 E2 e P Φ :
+(** In this stronger version of [wp_step_fupdN], the masks in the
+   step-taking fancy update are a bit weird and somewhat difficult to
+   use in practice. Hence, we prove it for the sake of completeness,
+   but [wp_step_fupdN] is just a little bit weaker, suffices in
+   practice and is easier to use.
+
+   See the statement of [wp_step_fupdN] below to understand the use of
+   ordinary conjunction here. *)
+Lemma wp_step_fupdN_strong n 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 {{ Φ }}.
+  (∀ σ ns κs nt, state_interp σ ns κs nt
+       ={E1,∅}=∗ ⌜n ≤ S (num_laters_per_step ns)⌝) ∧
+  ((|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P) ∗
+    WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }}) -∗
+  WP e @ s; E1 {{ Φ }}.
 Proof.
-  rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
+  destruct n as [|n].
+  { iIntros (_ ?) "/= [_ [HP Hwp]]".
+    iApply (wp_strong_mono with "Hwp"); [done..|].
+    iIntros (v) "H". iApply ("H" with "[>HP]"). by do 2 iMod "HP". }
+  rewrite !wp_unfold /wp_pre /=. iIntros (-> ?) "H".
+  iIntros (σ1 ns κ κs nt) "Hσ".
+  destruct (decide (n ≤ num_laters_per_step ns)) as [Hn|Hn]; first last.
+  { iDestruct "H" as "[Hn _]". iMod ("Hn" with "Hσ") as %?. lia. }
+  iDestruct "H" as "[_ [>HP Hwp]]". iMod ("Hwp" with "[$]") as "[$ H]". iMod "HP".
   iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
-  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
-  iMod "HR". iModIntro. iFrame "Hσ Hefs".
-  iApply (wp_strong_mono s s E2 with "H"); [done..|].
-  iIntros (v) "H". by iApply "H".
+  iIntros "!>!>". iMod "H". iMod "HP". iModIntro.
+  revert n Hn. generalize (num_laters_per_step ns)=>n0 n Hn.
+  iInduction n as [|n] "IH" forall (n0 Hn).
+  - iApply (step_fupdN_wand with "H"). iIntros ">($ & Hwp & $)". iMod "HP".
+    iModIntro. iApply (wp_strong_mono with "Hwp"); [done|set_solver|].
+    iIntros (v) "HΦ". iApply ("HΦ" with "HP").
+  - destruct n0 as [|n0]; [lia|]=>/=. iMod "HP". iMod "H". iIntros "!> !>".
+    iMod "HP". iMod "H". iModIntro. iApply ("IH" with "[] HP H").
+    auto with lia.
 Qed.
 
 Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
@@ -160,29 +220,31 @@ Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
-  rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  rewrite wp_unfold /wp_pre fill_not_val /=; [|done].
+  iIntros (σ1 step κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]".
+  iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
   iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
-  iMod "H" as "(Hσ & H & Hefs)".
-  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
+  iMod "H". iModIntro. iApply (step_fupdN_wand with "H"). iIntros "H".
+  iMod "H" as "($ & H & $)". iModIntro. by iApply "IH".
 Qed.
 
 Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
   WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
 Proof.
-  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
+  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre /=.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
-  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1 ns κ κs nt) "Hσ". iMod ("H" with "[$]") as "[% H]".
+  iModIntro; iSplit.
   { destruct s; eauto using reducible_fill_inv. }
   iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
-  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
-  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
+  iMod ("H" $! _ _ _ with "[]") as "H"; first eauto using fill_step.
+  iIntros "!> !>". iMod "H". iModIntro. iApply (step_fupdN_wand with "H").
+  iIntros "H". iMod "H" as "($ & H & $)". iModIntro. by iApply "IH".
 Qed.
 
 (** * Derived rules *)
@@ -218,6 +280,41 @@ Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
 Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
+(** This lemma states that if we can prove that [n] laters are used in
+   the current physical step, then one can perform an n-steps fancy
+   update during that physical step. The resources needed to prove the
+   bound on [n] are not used up: they can be reused in the proof of
+   the WP or in the proof of the n-steps fancy update. In order to
+   describe this unusual resource flow, we use ordinary conjunction as
+   a premise. *)
+Lemma wp_step_fupdN n s E1 E2 e P Φ :
+  TCEq (to_val e) None → E2 ⊆ E1 →
+  (∀ σ ns κs nt, state_interp σ ns κs nt
+       ={E1,∅}=∗ ⌜n ≤ S (num_laters_per_step ns)⌝) ∧
+  ((|={E1∖E2,∅}=> |={∅}▷=>^n |={∅,E1∖E2}=> P) ∗
+    WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }}) -∗
+  WP e @ s; E1 {{ Φ }}.
+Proof.
+  iIntros (??) "H". iApply (wp_step_fupdN_strong with "[H]"); [done|].
+  iApply (and_mono_r with "H"). apply sep_mono_l. iIntros "HP".
+  iMod fupd_mask_subseteq_emptyset_difference as "H"; [|iMod "HP"]; [set_solver|].
+  iMod "H" as "_". replace (E1 ∖ (E1 ∖ E2)) with E2; last first.
+  { set_unfold=>x. destruct (decide (x ∈ E2)); naive_solver. }
+  iModIntro. iApply (step_fupdN_wand with "HP"). iIntros "H".
+  iApply fupd_mask_frame; [|iMod "H"; iModIntro]; [set_solver|].
+  by rewrite difference_empty_L (comm_L (∪)) -union_difference_L.
+Qed.
+Lemma 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.
+  iIntros (??) "HR H".
+  iApply (wp_step_fupdN_strong 1 _ E1 E2 with "[-]"); [done|..]. iSplit.
+  - iIntros (????) "_". iMod (fupd_mask_subseteq ∅) as "_"; [set_solver+|].
+    auto with lia.
+  - iFrame "H". iMod "HR" as "$". auto.
+Qed.
+
 Lemma wp_frame_step_l s E1 E2 e Φ R :
   TCEq (to_val e) None → E2 ⊆ E1 →
   (|={E1}[E2]▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
@@ -257,7 +354,6 @@ Proof.
   iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
 Qed.
-
 End wp.
 
 (** Proofmode class instances *)
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 236c1d0227109411df8953c982d072ab43e7270a..32a2d6f2579f431adfc876c92789571890a30d69 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -19,9 +19,11 @@ Class heapG Σ := HeapG {
 
 Global Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
-  state_interp σ κs _ :=
+  state_interp σ _ κs _ :=
     (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
   fork_post _ := True%I;
+  num_laters_per_step _ := 0;
+  state_interp_mono _ _ _ _ := fupd_intro _ _
 }.
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
@@ -85,7 +87,7 @@ Lemma wp_fork s E e Φ :
   ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto with head_step.
+  iIntros (σ1 ns κ κs nt) "Hσ !>"; iSplit; first by eauto with head_step.
   iIntros "!>" (v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
@@ -93,7 +95,7 @@ Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
   iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto with head_step.
+  iIntros (σ1 ns κs nt) "Hσ !>"; iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
@@ -222,7 +224,7 @@ Lemma twp_allocN_seq s E v n :
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
@@ -261,7 +263,7 @@ Lemma twp_free s E l v :
   [[{ RET LitV LitUnit; True }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
@@ -279,7 +281,7 @@ Lemma twp_load s E l dq v :
   [[{ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{dq} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
@@ -296,7 +298,7 @@ Lemma twp_store s E l v' v :
   [[{ RET LitV LitUnit; l ↦ v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
@@ -316,7 +318,7 @@ Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
   [[{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   rewrite bool_decide_false //.
@@ -337,7 +339,7 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' :
   [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   rewrite bool_decide_true //.
@@ -358,7 +360,7 @@ Lemma twp_faa s E l i1 i2 :
   [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ e2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
@@ -378,7 +380,7 @@ Lemma wp_new_proph s E :
   {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto with head_step.
+  iIntros (σ1 ns κ κs nt) "[Hσ HR] !>". iSplit; first by eauto with head_step.
   iIntros "!>" (v2 σ2 efs Hstep). inv_head_step.
   rename select proph_id into p.
   iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
@@ -437,19 +439,20 @@ Proof.
   (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
      here, since this breaks the WP abstraction. *)
   iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
-  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
-  - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
+  iIntros (σ1 ns κ κs nt) "[Hσ Hκ]".
+  destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
+  - iMod ("WPe" $! σ1 ns [] κs nt with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
     { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
     iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
     inv_head_step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
   - rewrite -assoc.
-    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
+    iMod ("WPe" $! σ1 0 _ _ nt with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
     { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
     iIntros (e2 σ2 efs step). apply step_resolve in step; last done.
     inv_head_step; simplify_list_eq.
     iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
     { by eexists [] _ _. }
-    iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
+    iModIntro. iNext. iModIntro. iMod "WPe" as ">[[$ Hκ] WPe]".
     iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ HPost]".
     iModIntro. rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[HΦ $]".
     iMod "HΦ". iModIntro. by iApply "HΦ".