diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68d579c4d39b805956dc21340011a5c7ad836513..89bc4ab2323ce9d45f893b75db1ceee808c56dfc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,8 +70,7 @@ lemma.
   the library that defines the `libG`.
 * Prepare for supporting later credits, by adding a resource `£ n` describing
   ownership of `n` credits that can be eliminated at fancy updates.
-  Note that the definition of WP has not yet been updated with support for later
-  credits, so it is not yet possible to actually generate any credits.
+  Note that HeapLang has not yet been equipped with support for later credits.
   To retain backwards compatibility with the interaction laws of fancy updates
   with the plainly modality (`BiFUpdPlainly`), which are incompatible with
   later credits, the logic is parameterized by two typeclasses, `HasLc`
@@ -88,8 +87,17 @@ lemma.
 
 **Changes in `program_logic`:**
 
-* In line with the preliminary support for later credits (see `base_logic`), the
-  adequacy statements have been changed to account for `HasLc` and `HasNoLc`:
+* The definition of the weakest precondition has been changed to generate later credits
+  (see `base_logic`) for each step:
+  + The member `num_laters_per_step` of the `irisGS` class now also determines the number
+    of later credits that are generated: `S (num_laters_per_step ns)` if `ns` steps
+    have been taken.
+  + The weakest precondition offers credits after a `prim_step` has been proven.
+  + All lifting lemmas have been altered to provide credits.
+    `wp_lift_step_fupdN` provides `S (num_laters_per_step ns)` credits, while all other
+    lemmas always provide one credit.
+* In line with the support for later credits (see `base_logic`), the adequacy statements
+  have been changed to account for `HasLc` and `HasNoLc`:
   + The lemma `twp_total` (total adequacy) provides an additional assumption `HasNoLc`.
     Clients of the adequacy proof will need to introduce this additional assumption and
     keep it around in case `BiFUpdPlainly` is used.
@@ -112,14 +120,15 @@ lemma.
   number of steps taken so far. This number is tied to ghost state in the state
   interpretation, which is exposed, updated, and used with new lemmas
   `wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
-* In line with the preliminary support for later credits (see `base_logic`), the
-  adequacy statements for HeapLang have been changed:
+* In line with the support for later credits (see `base_logic`), the adequacy statements
+  for HeapLang have been changed:
   + `heap_adequacy` provides the additional assumption `HasLc`, which needs to be
     introduced by clients and will enable using new proof rules for later credits
     in the future.
     This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
   + `heap_total` provides the additional assumption `HasNoLc`, which needs to be
     introduced by clients and needs to be kept around to use the laws in `BiFUpdPlainly`.
+  Currently, the primitive laws for HeapLang do not yet provide later credits.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index d63748060b0640ae4e175280a3ea45bbb7afe9c3..de2dec96fa12a39b3472e477a1c178759920efa2 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -89,8 +89,8 @@ Section later_credit_theory.
     £ (S n) ⊣⊢ £ 1 ∗ £ n.
   Proof. rewrite -lc_split //=. Qed.
 
-  Lemma lc_weaken n m :
-    m ≤ n → (£ n -∗ £ m).
+  Lemma lc_weaken {n} m :
+    m ≤ n → £ n -∗ £ m.
   Proof.
     intros [k ->]%nat_le_sum. rewrite lc_split. iIntros "[$ _]".
   Qed.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 99b613eaab1709a7034508a906c7924c31fe7813..fdd9aa030ca8c39ce85194c5d49f174cd1acebcb 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -366,7 +366,7 @@ Section fupd_derived.
     by replace (E1 ∪ E ∖ E1) with E by (by apply union_difference_L).
   Qed.
   (* A variant of [fupd_mask_frame] that works well for accessors: Tailored to
-     elliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
+     eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
      transform the closing view shift instead of letting you prove the same
      side-conditions twice. *)
   Lemma fupd_mask_frame_acc E E' E1(*Eo*) E2(*Em*) P Q :
@@ -531,6 +531,24 @@ Section fupd_derived.
     rewrite step_fupd_frame_l IH //=.
   Qed.
 
+  Lemma step_fupdN_add n m Eo Ei P :
+    (|={Eo}[Ei]▷=>^(n+m) P) ⊣⊢ (|={Eo}[Ei]▷=>^n |={Eo}[Ei]▷=>^m P).
+  Proof.
+    induction n as [ | n IH]; simpl; [done | by rewrite IH].
+  Qed.
+
+  (** The sidecondition [Ei ⊆ Eo] is needed because for [n = 0],
+    this lemma introduces updates in the same way as [step_fupdN_intro]
+    (in fact, for [n = 0] it is essentially [step_fupdN_intro], modulo laters). *)
+  Lemma step_fupdN_le n m Eo Ei P :
+    n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^n P) -∗ (|={Eo}[Ei]▷=>^m P).
+  Proof.
+    intros ??. replace m with ((m - n) + n) by lia.
+    rewrite step_fupdN_add.
+    rewrite -(step_fupdN_intro _ _ (m - n)); last done.
+    by rewrite -laterN_intro.
+  Qed.
+
   Section fupd_plainly_derived.
     Context `{!BiPlainly PROP, !BiFUpdPlainly PROP}.
 
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 1429e59f9f23c202309970eb6ab325b9b3c8f476..64226cef5faaf4d86839335a5731f4d6ac4fb3d0 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -19,30 +19,34 @@ Notation wptp s t Φs := ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
 
 Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 ns (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }}
+  state_interp σ1 ns (κ ++ κs) nt -∗
+  £ (S (num_laters_per_step ns)) -∗
+  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 {1}wp_unfold /wp_pre. iIntros (?) "Hσ Hcred H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
   iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
-  iApply (step_fupdN_wand with "[H]"); first by iApply "H". iIntros ">H".
+  iApply (step_fupdN_wand with "(H [//] Hcred)"). iIntros ">H".
   by rewrite Nat.add_comm big_sepL2_replicate_r.
 Qed.
 
 Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
   step (es1,σ1) κ (es2, σ2) →
-  state_interp σ1 ns (κ ++ κs) nt -∗ wptp s es1 Φs -∗
+  state_interp σ1 ns (κ ++ κs) nt -∗
+  £ (S (num_laters_per_step ns)) -∗
+  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".
+  iIntros (Hstep) "Hσ Hcred 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. iModIntro.
+  iExists _. iMod (wp_step with "Hσ Hcred Ht") as "H"; first done. iModIntro.
   iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
   rewrite -(assoc_L app) -app_comm_cons. iFrame.
 Qed.
@@ -58,20 +62,23 @@ Local Fixpoint steps_sum (num_laters_per_step : nat → nat) (start ns : nat) :
 
 Lemma wptp_steps s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
   nsteps n (es1, σ1) κs (es2, σ2) →
-  state_interp σ1 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  state_interp σ1 ns (κs ++ κs') nt -∗
+  £ (steps_sum num_laters_per_step ns n) -∗
+  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 ns σ2 Φs.
   induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
-  { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
+  { inversion_clear 1; iIntros "? ? ?"; iExists 0=> /=.
     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 (++)) Nat_iter_add plus_n_Sm.
-  iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
+  iIntros (Hsteps) "Hσ Hcred He". inversion_clear Hsteps as [|?? [t1' σ1']].
+  rewrite -(assoc_L (++)) Nat_iter_add -{1}plus_Sn_m plus_n_Sm.
+  rewrite lc_split. iDestruct "Hcred" as "[Hc1 Hc2]".
+  iDestruct (wptp_step with "Hσ Hc1 He") as (nt') ">H"; first eauto; simplify_eq.
   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.
+  iIntros ">(Hσ & He)". iMod (IH with "Hσ Hc2 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.
@@ -89,12 +96,14 @@ Qed.
 
 Local 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 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  state_interp σ1 ns (κs ++ κs') nt -∗
+  £ (steps_sum num_laters_per_step ns n) -∗
+  wptp s es1 Φs
   ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ 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". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
+  iIntros (Hstep) "Hσ Hcred He". iMod (wptp_steps with "Hσ Hcred He") as "Hwp"; first done.
   iModIntro. iApply (step_fupdN_wand with "Hwp").
   iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
   iExists _. iFrame "Hσ".
@@ -110,10 +119,11 @@ Local Lemma wptp_progress Φs κs' n es1 es2 κs σ1 ns σ2 nt e2 :
   nsteps n (es1, σ1) κs (es2, σ2) →
   e2 ∈ es2 →
   state_interp σ1 ns (κs ++ κs') nt -∗
+  £ (steps_sum num_laters_per_step ns n) -∗
   wptp NotStuck es1 Φs
   ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅}=> ⌜not_stuck e2 σ2⌝.
 Proof.
-  iIntros (Hstep Hel) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
+  iIntros (Hstep Hel) "Hσ Hcred He". iMod (wptp_steps with "Hσ Hcred He") as "Hwp"; first done.
   iModIntro. iApply (step_fupdN_wand with "Hwp").
   iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
   eapply elem_of_list_lookup in Hel as [i Hlook].
@@ -145,13 +155,14 @@ Local Lemma wp_progress_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} es σ1 n
   not_stuck e2 σ2.
 Proof.
   iIntros (Hwp ??).
-  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n) 0).
-  iIntros (Hinv Hc) "_".
+  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n)
+    (steps_sum num_laters_per_step 0 n)).
+  iIntros (Hinv Hc) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)"; first done.
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
   iMod (@wptp_progress _ _
        (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
-    with "[Hσ] Hwp") as "H"; [done| done |by rewrite right_id_L|].
+    with "[Hσ] Hcred  Hwp") as "H"; [done| done |by rewrite right_id_L|].
   iAssert (|={∅}▷=>^(steps_sum num_laters_per_step 0 n) |={∅}=> ⌜not_stuck e2 σ2⌝)%I
     with "[-]" as "H"; last first.
   { destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
@@ -202,13 +213,14 @@ Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1
   φ.
 Proof.
   iIntros (Hwp ?).
-  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n) 0).
-  iIntros (Hinv Hc) "_". (* no credit generation for now *)
+  eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n)
+    (steps_sum num_laters_per_step 0 n)).
+  iIntros (Hinv Hc) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
   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|].
+    with "[Hσ] Hcred 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. }
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 74532a115b07a52305b5eff6e88c8eadbb6bf1ec..a6ecf16adf3246a26ec564ce22c3d063b0a9b27c 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -19,7 +19,7 @@ Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ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}=>
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={∅}=∗ ▷ |={∅,E}=>
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -35,14 +35,14 @@ Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ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}=∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={∅,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.
   iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?????) "?".
-  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
+  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "Hcred !> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
@@ -69,7 +69,7 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ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]▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E1}[E2]▷=∗
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -85,7 +85,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ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}=∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E}=∗
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -101,14 +101,14 @@ Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ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]▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E1}[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 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 (v2 σ2 efs Hstep) "Hcred".
+  iMod ("H" $! v2 σ2 efs with "[# //] Hcred") as "H".
   iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
 Qed.
 
@@ -116,14 +116,14 @@ Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ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}=∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E}=∗
       ⌜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 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.
+  iNext; iIntros (v2 σ2 efs Hstep) "Hcred".
+  iMod ("H" $! v2 σ2 efs with "[//] Hcred") as "(-> & ? & ?) /=". by iFrame.
 Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
@@ -131,7 +131,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> £1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
   destruct s; by auto.
@@ -142,7 +142,7 @@ Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
+  ▷ (£1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
   rewrite -step_fupd_intro //.
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 2e7845f6796cfc22d400bef358a4025d2f20d654..85a7d3662e0d8b0f7d374a97fead374de46ef955 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -20,7 +20,8 @@ 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⌝
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗
+      £ (S $ num_laters_per_step ns)
       ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
@@ -32,14 +33,19 @@ Lemma wp_lift_step_fupd 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⌝ ={∅}=∗ ▷ |={∅,E}=>
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={∅}=∗ ▷ |={∅,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.
-  intros ?. rewrite -wp_lift_step_fupdN; [|done]. simpl. do 22 f_equiv.
-  rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro. auto.
+  iIntros (?) "Hwp". rewrite -wp_lift_step_fupdN; [|done].
+  iIntros (?????) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)".
+  iIntros "!>" (??? ?) "Hcred".
+  iPoseProof (lc_weaken 1 with "Hcred") as "Hcred"; first lia.
+  simpl. rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro.
+  iMod ("Hwp" with "[//] Hcred") as "Hwp".
+  iApply step_fupd_intro; done.
 Qed.
 
 Lemma wp_lift_stuck E Φ e :
@@ -57,20 +63,20 @@ Lemma wp_lift_step 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⌝ ={∅,E}=∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={∅,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.
   iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?????) "Hσ".
-  iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
+  iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % Hcred !> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
-  (|={E}[E']▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
+  (|={E}[E']▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ -∗ £1 -∗ WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
@@ -78,11 +84,11 @@ Proof.
   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 ?).
+  iNext. iIntros (e2 σ2 efs ?) "Hcred".
   destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
   iMod (state_interp_mono with "Hσ") as "$".
   iMod "Hclose" as "_". iMod "H". iModIntro.
-  by iDestruct ("H" with "[//]") as "$".
+  by iDestruct ("H" with "[//] Hcred") as "$".
 Qed.
 
 Lemma wp_lift_pure_stuck `{!Inhabited (state Λ)} E Φ e :
@@ -101,7 +107,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ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]▷=∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E1}[E2]▷=∗
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -111,8 +117,8 @@ Proof.
   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 "_".
-  iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
+  iIntros "Hclose" (e2 σ2 efs ?) "Hcred". iMod "Hclose" as "_".
+  iMod ("H" $! e2 σ2 efs with "[#] Hcred") as "H"; [done|].
   iApply fupd_mask_intro; first set_solver. iIntros "Hclose !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
@@ -123,7 +129,7 @@ Lemma wp_lift_atomic_step {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⌝ ={E}=∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £1 ={E}=∗
       state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -131,7 +137,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
   iIntros (?????) "?". iMod ("H" with "[$]") as "[$ H]".
-  iIntros "!> *". iIntros (Hstep) "!> !>".
+  iIntros "!> *". iIntros (Hstep) "Hcred !> !>".
   by iApply "H".
 Qed.
 
@@ -139,7 +145,7 @@ Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
     κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> £1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
   { naive_solver. }
@@ -150,22 +156,28 @@ Qed.
 Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  (|={E}[E']▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=>^n £n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
-  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl.
+  { iMod lc_zero as "Hz". by iApply "Hwp". }
   iApply wp_lift_pure_det_step_no_fork.
   - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
   - done.
-  - by iApply (step_fupd_wand with "Hwp").
+  - iApply (step_fupd_wand with "Hwp").
+    iIntros "Hwp Hone". iApply "IH".
+    iApply (step_fupdN_wand with "Hwp").
+    iIntros "Hwp Hc". iApply ("Hwp" with "[Hone Hc]").
+    rewrite (lc_succ n). iFrame.
 Qed.
 
 Lemma wp_pure_step_later `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  ▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
+  ▷^n (£n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
+  enough (∀ P, ▷^n P -∗ |={E}▷=>^n P) as Hwp by apply Hwp. iIntros (?).
   induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
 End lifting.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index c7ec1a2dd42dc035cab04b6e9f67da0bdee5ed3d..22d9b2791518efb3c54b34a4ae85ce20d8b9d47b 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -85,6 +85,7 @@ Qed.
 
 
 (** Lifting *)
+(** All lifting lemmas defined here discard later credits.*)
 Section lifting.
   Context `{!ownPGS Λ Σ}.
   Implicit Types s : stuckness.
@@ -121,7 +122,7 @@ Section lifting.
     - 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).
+      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep) "Hcred".
       iDestruct "Hσκs" as "Hσ". rewrite /ownP.
       iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
       { apply excl_auth_update. }
@@ -152,7 +153,7 @@ Section lifting.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
     iIntros (σ1 ns κ κs nt) "Hσ". iApply fupd_mask_intro; first set_solver.
-    iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
+    iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?) "Hcred".
     destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
@@ -205,7 +206,8 @@ Section lifting.
     (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
+    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //.
+    iIntros "Hwp". iApply step_fupd_intro; first done. iNext. by iIntros "_".
   Qed.
 End lifting.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 76e9177d320201bffaf09100a05aa6508cf6ff4e..d71dfb12ae0e911c5d8e26d0ef893b1054345fed 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -204,7 +204,7 @@ Proof.
   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)".
+  iIntros (e2 σ2 efs) "Hstep _". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
   iApply fupd_mask_intro; [set_solver+|]. iIntros "Hclose".
   iIntros "!>!>". iApply step_fupdN_intro=>//. iModIntro. iMod "Hclose" as "_".
   iModIntro. iFrame "Hσ". iSplitL "H".
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 55108733874d86775c0dca1af3d95869e9e06376..3119a20cf7c488f780fe459efeeedaaa854ea428 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -13,7 +13,7 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
   (** 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
+  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). *)
@@ -24,11 +24,11 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
   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. *)
+  (** The number of additional logical steps (i.e., later modality in the
+  definition of WP) and later credits per physical step is
+  [S (num_laters_per_step ns)], where [ns] is the number of physical steps
+  executed so far. We add one to [num_laters_per_step] to ensure that there
+  is always at least one later and later credit for each physical step. *)
   num_laters_per_step : nat → nat;
 
   (** When performing pure steps, the state interpretation needs to be
@@ -47,6 +47,19 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
 }.
 Global Opaque iris_invGS.
 
+(** The predicate we take the fixpoint of in order to define the WP. *)
+(** In the step case, we both provide [S (num_laters_per_step ns)]
+  later credits, as well as an iterated update modality that allows
+  stripping as many laters, where [ns] is the number of steps already taken.
+  We have both as each of these provides distinct advantages:
+  - Later credits do not have to be used right away, but can be kept to
+    eliminate laters at a later point.
+  - The step-taking update composes well in parallel: we can independently
+    compose two clients who want to eliminate their laters for the same
+    physical step, which is not possible with later credits, as they
+    can only be used by exactly one client.
+  - The step-taking update can even be used by clients that opt out of
+    later credits, e.g. because they use [BiFUpdPlainly]. *)
 Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
@@ -55,7 +68,8 @@ Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
   | 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⌝
+       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗
+         £ (S (num_laters_per_step ns))
          ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
          state_interp σ2 (S ns) κs (length efs + nt) ∗
          wp E e2 Φ ∗
@@ -65,7 +79,7 @@ Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
 Local Instance wp_pre_contractive `{!irisGS Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
-  do 24 (f_contractive || f_equiv).
+  do 25 (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.
@@ -103,7 +117,7 @@ Proof.
   (* 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).
+  do 25 (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.
@@ -119,7 +133,7 @@ Global Instance wp_contractive s E e n :
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He /=.
-  do 23 (f_contractive || f_equiv).
+  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.
@@ -140,8 +154,8 @@ Proof.
   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". iModIntro.
+  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep) "Hcred".
+  iMod ("H" with "[//] Hcred") 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Φ").
@@ -165,8 +179,8 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1 ns κ κs nt) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (e2 σ2 efs Hstep).
-  iApply (step_fupdN_wand with "[H]"); first by iApply "H".
+  iModIntro. iIntros (e2 σ2 efs Hstep) "Hcred".
+  iApply (step_fupdN_wand with "(H [//] Hcred)").
   iIntros ">(Hσ & H & Hefs)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
@@ -177,6 +191,49 @@ Proof.
     iModIntro. iFrame "Hσ Hefs". by iApply wp_value_fupd'.
 Qed.
 
+(** This lemma gives us access to the later credits that are generated in each step,
+  assuming that we have instantiated [num_laters_per_step] with a non-trivial (e.g. linear)
+  function.
+  This lemma can be used to provide a "regeneration" mechanism for later credits.
+  [state_interp] will have to be defined in a way that involves the required regneration
+  tokens. TODO: point to an example of how this is used.
+
+  In detail, a client can use this lemma as follows:
+  * the client obtains the state interpretation [state_interp _ ns _ _],
+  * it uses some ghost state wired up to the interpretation to know that
+    [ns = k + m], and update the state interpretation to [state_interp _ m _ _],
+  * _after_ [e] has finally stepped, we get [num_laters_per_step k] later credits
+    that we can use to prove [P] in the postcondition, and we have to update
+    the state interpretation from [state_interp _ (S m) _ _] to
+    [state_interp _ (S ns) _ _] again. *)
+Lemma wp_credit_access s E e Φ P :
+  TCEq (to_val e) None →
+  (∀ m k, num_laters_per_step m + num_laters_per_step k ≤ num_laters_per_step (m + k)) →
+  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
+    ∃ k m, state_interp σ1 m κs nt ∗ ⌜ns = (m + k)%nat⌝ ∗
+    (∀ nt σ2 κs, £ (num_laters_per_step k) -∗ state_interp σ2 (S m) κs nt ={E}=∗
+      state_interp σ2 (S ns) κs nt ∗ P)) -∗
+  WP e @ s; E {{ v, P ={E}=∗ Φ v }} -∗
+  WP e @ s; E {{ Φ }}.
+Proof.
+  rewrite !wp_unfold /wp_pre /=. iIntros (-> Htri) "Hupd Hwp".
+  iIntros (σ1 ns κ κs nt) "Hσ1".
+  iMod ("Hupd" with "Hσ1") as (k m) "(Hσ1 & -> & Hpost)".
+  iMod ("Hwp" with "Hσ1") as "[$ Hwp]". iModIntro.
+  iIntros (e2 σ2 efs Hstep) "Hc".
+  iDestruct "Hc" as "[Hone Hc]".
+  iPoseProof (lc_weaken with "Hc") as "Hc"; first apply Htri.
+  iDestruct "Hc" as "[Hm Hk]".
+  iCombine "Hone Hm" as "Hm".
+  iApply (step_fupd_wand with "(Hwp [//] Hm)"). iIntros "Hwp".
+  iApply (step_fupdN_le (num_laters_per_step m)); [ | done | ].
+  { etrans; last apply Htri. lia. }
+  iApply (step_fupdN_wand with "Hwp"). iIntros ">(SI & Hwp & $)".
+  iMod ("Hpost" with "Hk SI") as "[$ HP]". iModIntro.
+  iApply (wp_strong_mono with "Hwp"); [by auto..|].
+  iIntros (v) "HΦ". iApply ("HΦ" with "HP").
+Qed.
+
 (** 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,
@@ -202,7 +259,7 @@ Proof.
   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 "!>" (e2 σ2 efs Hstep) "Hcred". iMod ("H" $! e2 σ2 efs with "[% //] Hcred") as "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).
@@ -224,9 +281,9 @@ Proof.
   iIntros (σ1 step κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]".
   iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
-  iIntros (e2 σ2 efs Hstep).
+  iIntros (e2 σ2 efs Hstep) "Hcred".
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
+  iMod ("H" $! e2' σ2 efs with "[//] Hcred") as "H". iIntros "!>!>".
   iMod "H". iModIntro. iApply (step_fupdN_wand with "H"). iIntros "H".
   iMod "H" as "($ & H & $)". iModIntro. by iApply "IH".
 Qed.
@@ -241,8 +298,8 @@ Proof.
   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" $! _ _ _ with "[]") as "H"; first eauto using fill_step.
+  iIntros (e2 σ2 efs Hstep) "Hcred".
+  iMod ("H" $! _ _ _ with "[] Hcred") 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.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index f9553c03e5afc3f31fbf65eb55dc20a10946be2f..93725bafb7a878c79051873318e1ce85cbd5ec69 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -384,8 +384,8 @@ Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
   {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
 Proof.
   iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
-  iApply lifting.wp_pure_step_later; first done. iApply wp_value.
-  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
+  iApply lifting.wp_pure_step_later; first done.
+  iIntros "!> _". iApply wp_value. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
 Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index e51974e0260253e43b896516f27d21a55571d937..799b58df38d7a2b8b666b7e72ffd9597d18f6472 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -140,8 +140,8 @@ Proof.
   iDestruct (steps_lb_valid with "Hsteps Hlb") as %?.
   iMod ("Hwp" $! σ1 ns κ κs m with "[$Hσ $Hκ $Hsteps]") as "[%Hs Hwp]".
   iModIntro. iSplit; [done|].
-  iIntros (e2 σ2 efs Hstep).
-  iMod ("Hwp" with "[//]") as "Hwp".
+  iIntros (e2 σ2 efs Hstep) "Hcred".
+  iMod ("Hwp" with "[//] Hcred") as "Hwp".
   iIntros "!> !>". iMod "Hwp" as "Hwp". iIntros "!>".
   iApply (step_fupdN_wand with "Hwp").
   iIntros "Hwp". iMod "Hwp" as "(($ & $ & Hsteps)& Hwp & $)".
@@ -178,7 +178,7 @@ Lemma wp_rec_löb s E f x e Φ Ψ :
 Proof.
   iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
   iApply lifting.wp_pure_step_later; first done.
-  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
+  iIntros "!> _". iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
   iApply ("IH" with "HΨ").
 Qed.
 
@@ -188,7 +188,7 @@ Lemma wp_fork s E e Φ :
 Proof.
   iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
   iIntros (σ1 ns κ κs nt) "(?&?&Hsteps) !>"; iSplit; first by eauto with head_step.
-  iIntros "!>" (v2 σ2 efs Hstep); inv_head_step.
+  iIntros "!>" (v2 σ2 efs Hstep) "_"; inv_head_step.
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
   by iFrame.
 Qed.
@@ -513,7 +513,7 @@ Lemma wp_new_proph s E :
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 ns κ κs nt) "(Hσ & HR & Hsteps) !>". iSplit; first by eauto with head_step.
-  iIntros "!>" (v2 σ2 efs Hstep). inv_head_step.
+  iIntros "!>" (v2 σ2 efs Hstep) "_". inv_head_step.
   rename select proph_id into p.
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
   iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
@@ -582,9 +582,9 @@ Proof.
   - rewrite -assoc.
     iMod ("WPe" $! σ1 ns _ _ nt with "[$Hσ $Hκ $Hsteps]") 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.
+    iIntros (e2 σ2 efs step) "Hcred". apply step_resolve in step; last done.
     inv_head_step; simplify_list_eq.
-    iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
+    iMod ("WPe" $! (Val w') σ2 efs with "[%] Hcred") as "WPe".
     { by eexists [] _ _. }
     iModIntro. iNext. iMod "WPe" as "WPe". iModIntro.
     iApply (step_fupdN_wand with "WPe"); iIntros "> [($ & Hκ & $) WPe]".
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index a4e1dc21fb1cfb558125e34d92138bdd970c4fad..a77de67b67511395d43e28b09986c8a91ab86fac 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -39,6 +39,7 @@ Proof.
   (* We want [pure_exec_fill] to be available to TC search locally. *)
   pose proof @pure_exec_fill.
   rewrite HΔ' -lifting.wp_pure_step_later //.
+  iIntros "Hwp !> _" => //.
 Qed.
 Lemma tac_twp_pure `{!heapGS Σ} Δ s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 2334d994e0fedb40d861c1a3269246aca19c2bed..d810bb02269d70afd9cbeb14d8ba5bedfdd87828 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -242,7 +242,7 @@ Finally, we can define the core piece of the program logic, the proposition that
 
 \paragraph{Defining weakest precondition.}
 We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
-We further assume (as a parameter) a predicate $\stateinterp : \State \times \mathbb N \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-off threads, and a function $n_\rhd: \mathbb N \to \mathbb N$ specifying the number of additional laters used for each physical step.
+We further assume (as a parameter) a predicate $\stateinterp : \State \times \mathbb N \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-off threads, and a function $n_\rhd: \mathbb N \to \mathbb N$ specifying the number of additional laters and later credits used for each physical step.
 The state interpretation can depend on the current physical state, the number of steps since the begining of the execution, the list of \emph{future} observations as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
 It should be monotone with respect to the step counter: $\stateinterp(\state, n_s, \vec\obs, n_t) \vs[\emptyset] \stateinterp(\state, n_s, \vec\obs, n_t + 1)$.
 This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.
@@ -252,8 +252,9 @@ Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck,
   \textdom{wp}(\stateinterp, \pred_F, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
         & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
         & \Bigl(\toval(\expr) = \bot \land \All \state, n_s, \vec\obs, \vec\obs', n_t. \stateinterp(\state, n_s, \vec\obs \dplus \vec\obs', n_t) \vsW[\mask][\emptyset] {}\\
-        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \wand (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)+1} {}\\
-        &\qquad\qquad \pvs[\emptyset][\mask]\stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
+        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \wand \laterCredit{(n_\rhd(n_s)+1)} \wand {}\\
+        &\qquad\qquad (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)+1} \pvs[\emptyset][\mask]\stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * {}\\
+        &\qquad\qquad\qquad \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
   \wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
 \end{align*}
 The $\stateinterp$ and $\pred_F$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$ and fork-postcondition $\pred_F$.
@@ -311,7 +312,7 @@ This basically just copies the second branch (the non-value case) of the definit
   {\toval(\expr_1) = \bot}
   { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
         ~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,n_s,\vec\obs \dplus \vec\obs', n_t) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
-        \qquad~ \All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr) \wand (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)}\pvs[\emptyset][\mask] {}\\
+        \qquad~ \All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr) \wand \laterCredit{(n_\rhd(n_s) + 1)} \wand (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)}\pvs[\emptyset][\mask] {}\\
         \qquad\qquad\left(\stateinterp(\state_2,n_s+1,\vec\obs',n_t+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\right)  {}\\
         \proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
       \end{inbox}} }