From c5ebd34d646c572e56fdf95f33a2866f730891fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 27 Jul 2022 06:42:54 +0000
Subject: [PATCH] Add later credits to the WP

---
 CHANGELOG.md                          | 21 ++++--
 iris/base_logic/lib/later_credits.v   |  4 +-
 iris/bi/updates.v                     | 20 +++++-
 iris/program_logic/adequacy.v         | 54 +++++++++------
 iris/program_logic/ectx_lifting.v     | 26 ++++----
 iris/program_logic/lifting.v          | 50 ++++++++------
 iris/program_logic/ownp.v             |  8 ++-
 iris/program_logic/total_weakestpre.v |  2 +-
 iris/program_logic/weakestpre.v       | 95 +++++++++++++++++++++------
 iris_heap_lang/derived_laws.v         |  4 +-
 iris_heap_lang/primitive_laws.v       | 14 ++--
 iris_heap_lang/proofmode.v            |  1 +
 tex/program-logic.tex                 |  9 +--
 13 files changed, 210 insertions(+), 98 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68d579c4d..89bc4ab23 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 d63748060..de2dec96f 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 99b613eaa..fdd9aa030 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 1429e59f9..64226cef5 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 74532a115..a6ecf16ad 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 2e7845f67..85a7d3662 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 c7ec1a2dd..22d9b2791 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 76e9177d3..d71dfb12a 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 551087338..3119a20cf 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 f9553c03e..93725bafb 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 e51974e02..799b58df3 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 a4e1dc21f..a77de67b6 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 2334d994e..d810bb022 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}} }
-- 
GitLab