diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8bd5fbc5ea1129673b71bc3fa245eaec8fd1b6e6..b41986950ae4170783b2b4a08fe71370077bd727 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,36 @@ lemma.
 
 * Make the `inG` instances for `libG` fields local, so they are only used inside
   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.
+  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`
+  and `HasNoLc`, that allow opting for either later credits or `BiFUpdPlainly`.
+  The soundness lemmas for the fancy update modality are available in two versions,
+  with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
+  The lemma `step_fupdN_soundness_gen` is generic over this choice.
+
+**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 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.
+  + The adequacy lemmas for the partial WP, in particular `wp_adequacy`,
+    `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors,
+    one providing `HasLc` to enable the use of later credits in the future (suffix `_lc`),
+    and one without support for later credits, providing `HasNoLc` (suffix `_no_lc`).
+    Clients of the adequacy proof will need to opt for either of these and introduce
+    the additional assumptions.
+  + The parameter for the stuckness bit `s` in `wp_strong_adequacy{_lc, _no_lc}` has
+    moved up and is now universally quantified in the lemma instead of being existentially
+    quantified at the Iris-level. For clients that already previously quantified over `s`
+    at the Coq level, the only required change should be to remove the instantiation
+    of the existential quantifier.
 
 **Changes in `iris_heap_lang`:**
 
@@ -61,6 +91,14 @@ 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:
+  + `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`.
 
 ## Iris 3.6.0 (2022-01-22)
 
diff --git a/_CoqProject b/_CoqProject
index 0847d523af66f6299728c480015bed726756345c..a159af6bdc69cb0aeab3ab058b03c0bd3f3ecf93 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -106,6 +106,7 @@ iris/base_logic/lib/ghost_var.v
 iris/base_logic/lib/mono_nat.v
 iris/base_logic/lib/gset_bij.v
 iris/base_logic/lib/ghost_map.v
+iris/base_logic/lib/later_credits.v
 iris/program_logic/adequacy.v
 iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index bedddcc6806d3675a754b290dc455ba31e2cf71e..b9ba2d8a4434f4d7dd70005e90b9891d3a19e106 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -3,12 +3,59 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
+From iris.base_logic Require Export later_credits.
 From iris.prelude Require Import options.
-Export invGS.
+Export wsatGS.
 Import uPred.
+Import le_upd_if.
+
+(** The definition of fancy updates (and in turn the logic built on top of it) is parameterized
+    by whether it supports elimination of laters via later credits or not.
+    This choice is necessary as the fancy update *with* later credits does *not* support
+    the interaction laws with the plainly modality in [BiFUpdPlainly]. While these laws are
+    seldomly used, support for them is required for backwards compatibility.
+
+    Thus, we define two typeclasses [HasLc] and [HasNoLc].
+    The availability of the rules for later credits or the plainly interaction depends
+    on having an instance of the right one of these classes in the context. See below.
+ *)
+
+Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
+  invGpreS_wsat : wsatGpreS Σ;
+  invGpreS_lc : lcGpreS Σ;
+}.
+
+Class invGS (Σ : gFunctors) : Set := InvG {
+  invGS_wsat : wsatGS Σ;
+  invGS_lc : lcGS Σ;
+  (* flag determining whether the fancy update allows later credit elimination *)
+  invGS_use_credits : bool;
+}.
+Global Hint Mode invGS - : typeclass_instances.
+Global Hint Mode invGpreS - : typeclass_instances.
+Local Existing Instances invGpreS_wsat invGpreS_lc.
+(* [invGS_lc] needs to be global in order to enable the use of lemmas like [lc_split]
+   that require [lcGS], and not [invGS].
+   [invGS_wsat] also needs to be global as the lemmas in [invariants.v] require it. *)
+Global Existing Instances invGS_lc invGS_wsat.
+
+Definition invΣ : gFunctors :=
+  #[wsatΣ; lcΣ].
+Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
+Proof. solve_inG. Qed.
+
+(** [HasLc] asserts that the fancy update is defined with support for later credits. *)
+Class HasLc (Σ : gFunctors) `{!invGS Σ} :=
+  { has_credits : invGS_use_credits = true }.
+Global Hint Mode HasLc - - : typeclass_instances.
+(** [HasNoLc] asserts that the fancy update is defined without support for later credits,
+    but in turn supports the plainly interaction laws [BiFUpdPlainly]. *)
+Class HasNoLc (Σ : gFunctors) `{!invGS Σ} :=
+  { has_no_credits : invGS_use_credits = false }.
+Global Hint Mode HasNoLc - - : typeclass_instances.
 
 Local Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
-  wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
+  wsat ∗ ownE E1 -∗ le_upd_if invGS_use_credits (◇ (wsat ∗ ownE E2 ∗ P)).
 Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
 Global Arguments uPred_fupd {Σ _}.
@@ -41,44 +88,49 @@ Global Instance uPred_bi_fupd `{!invGS Σ} : BiFUpd (uPredI (iResUR Σ)) :=
 Global Instance uPred_bi_bupd_fupd `{!invGS Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
 Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
 
-Global Instance uPred_bi_fupd_plainly `{!invGS Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
+(** The interaction laws with the plainly modality are only supported when
+  we opt out of the support for later credits. *)
+Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS Σ, !HasNoLc Σ} :
+  BiFUpdPlainly (uPredI (iResUR Σ)).
 Proof.
-  split.
-  - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+  split; rewrite uPred_fupd_unseal /uPred_fupd_def has_no_credits.
+  - iIntros (E P) "H [Hw HE]".
     iAssert (â—‡ â–  P)%I as "#>HP".
     { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     by iFrame.
-  - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
+  - iIntros (E P Q) "[H HQ] [Hw HE]".
     iAssert (â—‡ â–  P)%I as "#>HP".
     { by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
     by iFrame.
-  - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+  - iIntros (E P) "H [Hw HE]".
     iAssert (â–· â—‡ â–  P)%I as "#HP".
     { iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     iFrame. iIntros "!> !> !>". by iMod "HP".
-  - rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
+  - iIntros (E A Φ) "HΦ [Hw HE]".
     iAssert (◇ ■ ∀ x : A, Φ x)%I as "#>HP".
     { iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
-  (∀ `{Hinv: !invGS Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
+Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
-  iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
+  iMod (lc_alloc 0) as (Hc) "[_ _]".
+  set (Hi := InvG _ Hw Hc false).
   iAssert (|={⊤,E2}=> P)%I as "H".
-  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. }
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. by constructor. }
   rewrite uPred_fupd_unseal /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma step_fupdN_soundness `{!invGpreS Σ} φ n :
-  (∀ `{Hinv: !invGS Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} φ n :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
-  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _)=> Hinv hc.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   iApply fupd_plainly_mask_empty. iMod "H".
   iMod (step_fupdN_plain with "H") as "H". iModIntro.
@@ -86,13 +138,99 @@ Proof.
   iNext. iMod "H" as %Hφ. auto.
 Qed.
 
-Lemma step_fupdN_soundness' `{!invGpreS Σ} φ n :
-  (∀ `{Hinv: !invGS Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} φ n :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness _ n)=>Hinv. destruct n as [|n].
+  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n)=>Hinv Hc. destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
    simpl in Hiter |- *. iMod Hiter as "H". iIntros "!>!>!>".
   iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
   simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.
+
+(** Later credits: the laws are only available when we opt into later credit support.*)
+
+(** [lc_fupd_elim_later] allows to eliminate a later from a hypothesis at an update.
+  This is typically used as [iMod (lc_fupd_elim_later with "Hcredit HP") as "HP".],
+  where ["Hcredit"] is a credit available in the context and ["HP"] is the
+  assumption from which a later should be stripped. *)
+Lemma lc_fupd_elim_later `{!invGS Σ} `{!HasLc Σ} E P :
+   £1 -∗ (▷ P) -∗ |={E}=> P.
+Proof.
+  iIntros "Hf Hupd".
+  rewrite uPred_fupd_unseal /uPred_fupd_def has_credits.
+  iIntros "[$ $]". iApply (le_upd_later with "Hf").
+  iNext. by iModIntro.
+Qed.
+
+(** If the goal is a fancy update, this lemma can be used to make a later appear
+  in front of it in exchange for a later credit.
+  This is typically used as [iApply (lc_fupd_add_later with "Hcredit")],
+  where ["Hcredit"] is a credit available in the context. *)
+Lemma lc_fupd_add_later `{!invGS Σ} `{!HasLc Σ} E1 E2 P :
+  £1 -∗ (▷ |={E1, E2}=> P) -∗ |={E1, E2}=> P.
+Proof.
+  iIntros "Hf Hupd". iApply (fupd_trans E1 E1).
+  iApply (lc_fupd_elim_later with "Hf Hupd").
+Qed.
+
+Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 φ :
+  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> ⌜φ⌝) → φ.
+Proof.
+  iIntros (Hfupd). eapply (lc_soundness (S n)). intros Hc.
+  rewrite lc_succ.
+  iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
+  iMod wsat_alloc as (Hw) "[Hw HE]".
+  set (Hi := InvG _ Hw Hc true).
+  iAssert (|={⊤,E2}=> ⌜φ⌝)%I with "[Hn]" as "H".
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. by iApply (Hfupd Hi). }
+  rewrite uPred_fupd_unseal /uPred_fupd_def.
+  iModIntro. iMod ("H" with "[$Hw $HE]") as "H".
+  iPoseProof (except_0_into_later with "H") as "H".
+  iApply (le_upd_later with "Hone"). iNext.
+  iDestruct "H" as "(_ & _ & $)".
+Qed.
+
+Lemma step_fupdN_soundness_lc `{!invGpreS Σ} φ n m :
+  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+  φ.
+Proof.
+  intros Hiter. eapply (fupd_soundness_lc (m + n)); [apply _..|].
+  iIntros (Hinv Hc) "Hlc". rewrite lc_split.
+  iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
+  clear Hiter.
+  iInduction n as [|n] "IH"; simpl.
+  - by iModIntro.
+  - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
+    iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
+    by iApply ("IH" with "Hn Hupd").
+Qed.
+
+Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} φ n m :
+  (∀ `{Hinv: !invGS Σ} `{!HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+  φ.
+Proof.
+  intros Hiter. eapply (fupd_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
+  iIntros (Hinv Hc) "Hlc". rewrite lc_split.
+  iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
+  clear Hiter.
+  iInduction n as [|n] "IH"; simpl.
+  - by iModIntro.
+  - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
+    iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
+    by iApply ("IH" with "Hn Hupd").
+Qed.
+
+(** Generic soundness lemma for the fancy update, parameterized by [use_credits]
+  on whether to use credits or not. *)
+Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (φ : Prop)
+    (use_credits : bool) (n m : nat) :
+  (∀ `{Hinv : invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+    (if use_credits then £ m else True) ={⊤,∅}=∗ |={∅}▷=>^n ⌜φ⌝) →
+  φ.
+Proof.
+  destruct use_credits.
+  - apply step_fupdN_soundness_lc.
+  - apply step_fupdN_soundness_no_lc.
+Qed.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index d13814d4085c6803ae8e08025e5523141349bd0d..3da0873656a13693ddd6209de1fae51079e7c660 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
 From iris.prelude Require Import options.
 Import uPred.
+Import le_upd_if.
 
 (** Semantic Invariants *)
 Local Definition inv_def `{!invGS Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
new file mode 100644
index 0000000000000000000000000000000000000000..329c938c76be1baca8d301ad78259d8003e71857
--- /dev/null
+++ b/iris/base_logic/lib/later_credits.v
@@ -0,0 +1,423 @@
+(** This file implements later credits, in particular the later-elimination update.
+That update is used internally to define the Iris [fupd]; it should not
+usually be directly used unless you are defining your own [fupd]. *)
+From iris.prelude Require Import options.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Export auth numbers.
+From iris.base_logic.lib Require Import iprop own.
+Import uPred.
+
+
+(** The ghost state for later credits *)
+Class lcGpreS (Σ : gFunctors) := LcGpreS {
+  lcGpreS_inG : inG Σ (authR natUR)
+}.
+
+Class lcGS (Σ : gFunctors) := LcGS {
+  lcGS_inG : inG Σ (authR natUR);
+  lcGS_name : gname;
+}.
+Global Hint Mode lcGS - : typeclass_instances.
+Local Existing Instances lcGS_inG lcGpreS_inG.
+
+Definition lcΣ := #[GFunctor (authR (natUR))].
+Global Instance subG_lcΣ {Σ} : subG lcΣ Σ → lcGpreS Σ.
+Proof. solve_inG. Qed.
+
+
+(** The user-facing credit resource, denoting ownership of [n] credits. *)
+Local Definition lc_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (◯ n).
+Local Definition lc_aux : seal (@lc_def). Proof. by eexists. Qed.
+Definition lc := lc_aux.(unseal).
+Local Definition lc_unseal :
+  @lc = @lc_def := lc_aux.(seal_eq).
+Global Arguments lc {Σ _} n.
+
+Notation "'£'  n" := (lc n) (at level 1).
+
+(** The internal authoritative part of the credit ghost state,
+  tracking how many credits are available in total.
+  Users should not directly interface with this. *)
+Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (● n).
+Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
+Definition lc_supply := lc_supply_aux.(unseal).
+Local Definition lc_supply_unseal :
+  @lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
+Global Arguments lc_supply {Σ _} n.
+
+
+Section later_credit_theory.
+  Context `{!lcGS Σ}.
+  Implicit Types (P Q : iProp Σ).
+
+  (** Later credit rules *)
+  Lemma lc_split n m :
+    £ (n + m) ⊣⊢ £ n ∗ £ m.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite -own_op auth_frag_op //=.
+  Qed.
+
+  Lemma lc_zero : ⊢ |==> £ 0.
+  Proof.
+    rewrite lc_unseal /lc_def. iApply own_unit.
+  Qed.
+
+  Lemma lc_supply_bound n m :
+    lc_supply m -∗ £ n -∗ ⌜n ≤ m⌝.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite lc_supply_unseal /lc_supply_def.
+    iIntros "H1 H2".
+    iDestruct (own_valid_2 with "H1 H2") as "%Hop".
+    iPureIntro. eapply auth_both_valid_discrete in Hop as [Hlt _].
+    by eapply nat_included.
+  Qed.
+
+  Lemma lc_decrease_supply n m :
+    lc_supply (n + m) -∗ £ n -∗ |==> lc_supply m.
+  Proof.
+    rewrite lc_unseal /lc_def.
+    rewrite lc_supply_unseal /lc_supply_def.
+    iIntros "H1 H2".
+    iMod (own_update_2 with "H1 H2") as "Hown".
+    { eapply auth_update. eapply (nat_local_update _ _ m 0). lia. }
+    by iDestruct "Hown" as "[Hm _]".
+  Qed.
+
+  Lemma lc_succ n :
+    £ (S n) ⊣⊢ £ 1 ∗ £ n.
+  Proof. rewrite -lc_split //=. Qed.
+
+  Lemma lc_weaken n m :
+    m ≤ n → (£ n -∗ £ m).
+  Proof.
+    intros [k ->]%nat_le_sum. rewrite lc_split. iIntros "[$ _]".
+  Qed.
+
+  Global Instance lc_timeless n : Timeless (£ n).
+  Proof.
+    rewrite lc_unseal /lc_def. apply _.
+  Qed.
+
+  Global Instance lc_0_persistent : Persistent (£ 0).
+  Proof.
+    rewrite lc_unseal /lc_def. apply _.
+  Qed.
+
+  Global Instance from_sep_lc_add n m :
+    FromSep (£ (n + m)) (£ n) (£ m).
+  Proof.
+    by rewrite /FromSep lc_split.
+  Qed.
+  Global Instance from_sep_lc_S n :
+    FromSep (£ (S n)) (£ 1) (£ n).
+  Proof.
+    by rewrite /FromSep (lc_succ n).
+  Qed.
+
+  Global Instance into_sep_lc_add n m :
+    IntoSep (£ (n + m)) (£ n) (£ m).
+  Proof.
+    by rewrite /IntoSep lc_split.
+  Qed.
+  Global Instance into_sep_lc_S n :
+    IntoSep (£ (S n)) (£ 1) (£ n).
+  Proof.
+    by rewrite /IntoSep (lc_succ n).
+  Qed.
+End later_credit_theory.
+
+(** Let users import the above without also getting the below laws.
+  This should only be imported by the internal development of fancy updates. *)
+Module le_upd.
+  (** Definition of the later-elimination update *)
+  Definition le_upd_pre `{!lcGS Σ}
+      (le_upd : iProp Σ -d> iPropO Σ) : iProp Σ -d> iPropO Σ := λ P,
+    (∀ n, lc_supply n ==∗
+          (lc_supply n ∗ P) ∨ (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ le_upd P))%I.
+
+  Local Instance le_upd_pre_contractive `{!lcGS Σ} : Contractive le_upd_pre.
+  Proof. solve_contractive. Qed.
+  Local Definition le_upd_def `{!lcGS Σ} :
+    iProp Σ -d> iPropO Σ := fixpoint le_upd_pre.
+  Local Definition le_upd_aux : seal (@le_upd_def). Proof. by eexists. Qed.
+  Definition le_upd := le_upd_aux.(unseal).
+  Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq).
+  Global Arguments le_upd {_ _} _.
+  Notation "'|==£>' P" := (le_upd P) (at level 99, P at level 200, format "|==£>  P").
+
+  Local Lemma le_upd_unfold `{!lcGS Σ} P:
+    (|==£> P) ⊣⊢
+    ∀ n, lc_supply n ==∗
+         (lc_supply n ∗ P) ∨ (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ le_upd P).
+  Proof.
+    by rewrite le_upd_unseal
+      /le_upd_def {1}(fixpoint_unfold le_upd_pre P) {1}/le_upd_pre.
+  Qed.
+
+  Section le_upd.
+    Context `{!lcGS Σ}.
+    Implicit Types (P Q : iProp Σ).
+
+    (** Rules for the later elimination update *)
+    Global Instance le_upd_ne : NonExpansive le_upd.
+    Proof.
+      intros n; induction (lt_wf n) as [n _ IH].
+      intros P1 P2 HP. rewrite (le_upd_unfold P1) (le_upd_unfold P2).
+      do 9 (done || f_equiv). f_contractive. eapply IH, dist_S; [lia|done].
+    Qed.
+
+    Lemma bupd_le_upd P : (|==> P) -∗ (|==£> P).
+    Proof.
+      rewrite le_upd_unfold; iIntros "Hupd" (x) "Hpr".
+      iMod "Hupd" as "P". iModIntro. iLeft. by iFrame.
+    Qed.
+
+    Lemma le_upd_intro P : P -∗ |==£> P.
+    Proof.
+      iIntros "H"; by iApply bupd_le_upd.
+    Qed.
+
+    Lemma le_upd_bind P Q :
+      (P -∗ |==£> Q) -∗ (|==£> P) -∗ (|==£> Q).
+    Proof.
+      iLöb as "IH". iIntros "PQ".
+      iEval (rewrite (le_upd_unfold P) (le_upd_unfold Q)).
+      iIntros "Hupd" (x) "Hpr". iMod ("Hupd" with "Hpr") as "[Hupd|Hupd]".
+      - iDestruct "Hupd" as "[Hpr Hupd]".
+        iSpecialize ("PQ" with "Hupd").
+        iEval (rewrite le_upd_unfold) in "PQ".
+        iMod ("PQ" with "Hpr") as "[Hupd|Hupd]".
+        + iModIntro. by iLeft.
+        + iModIntro. iRight. iDestruct "Hupd" as  (x'' Hstep'') "[Hpr Hupd]".
+          iExists _; iFrame. by iPureIntro.
+      - iModIntro. iRight. iDestruct "Hupd" as (x') "(Hstep & Hpr & Hupd)".
+        iExists _; iFrame. iNext. by iApply ("IH" with "PQ Hupd").
+    Qed.
+
+    Lemma le_upd_later_elim P :
+      £ 1 -∗ (▷ |==£> P) -∗ |==£> P.
+    Proof.
+      iIntros "Hc Hl".
+      iEval (rewrite le_upd_unfold). iIntros (n) "Hs".
+      iDestruct (lc_supply_bound with "Hs Hc") as "%".
+      destruct n as [ | n]; first by lia.
+      replace (S n) with (1 + n) by lia.
+      iMod (lc_decrease_supply with "Hs Hc") as "Hs". eauto 10 with iFrame lia.
+    Qed.
+
+    (** Derived lemmas *)
+    Lemma le_upd_mono P Q : (P ⊢ Q) → (|==£> P) -∗ (|==£> Q).
+    Proof.
+      intros Hent. iApply le_upd_bind.
+      iIntros "P"; iApply le_upd_intro; by iApply Hent.
+    Qed.
+    Lemma le_upd_trans P :  (|==£> |==£> P) -∗ |==£> P.
+    Proof.
+      iIntros "HP". iApply le_upd_bind; eauto.
+    Qed.
+    Lemma le_upd_frame_r P R : (|==£> P) ∗ R -∗ |==£> P ∗ R.
+    Proof.
+      iIntros "[Hupd R]". iApply (le_upd_bind with "[R]"); last done.
+      iIntros "P". iApply le_upd_intro. by iFrame.
+    Qed.
+
+    Lemma le_upd_later P :
+      £ 1 -∗ ▷ P -∗ |==£> P.
+    Proof.
+      iIntros "H1 H2". iApply (le_upd_later_elim with "H1").
+      iNext. by iApply le_upd_intro.
+    Qed.
+
+    Global Instance le_upd_mono' : Proper ((⊢) ==> (⊢)) le_upd.
+    Proof. intros P Q PQ; by apply le_upd_mono. Qed.
+    Global Instance le_upd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) le_upd.
+    Proof. intros P Q PQ; by apply le_upd_mono. Qed.
+    Global Instance le_upd_equiv_proper : Proper ((≡) ==> (≡)) le_upd.
+    Proof. apply ne_proper. apply _. Qed.
+
+    (** A safety check that later-elimination updates can replace basic updates *)
+    (** We do not use this to build an instance, because it would conflict
+       with the basic updates. *)
+    Local Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
+    Proof.
+      split.
+      - apply _.
+      - apply le_upd_intro.
+      - apply le_upd_mono.
+      - apply le_upd_trans.
+      - apply le_upd_frame_r.
+    Qed.
+
+    (** unfolding the later elimination update *)
+    Lemma le_upd_elim n P :
+      lc_supply n -∗
+      (|==£> P) -∗
+      Nat.iter n (λ P, |==> ▷ P) (|==> ◇ (∃ m, ⌜m ≤ n⌝ ∗ lc_supply m ∗ P)).
+    Proof.
+      induction (Nat.lt_wf_0 n) as [n _ IH].
+      iIntros "Ha". rewrite (le_upd_unfold P) //=.
+      iIntros "Hupd". iSpecialize ("Hupd" with "Ha").
+      destruct n as [|n]; simpl.
+      - iMod "Hupd" as "[[H● ?]| Hf]".
+        { do 2 iModIntro. iExists 0. iFrame. done. }
+        iDestruct "Hf" as (x' Hlt) "_". lia.
+      - iMod "Hupd" as "[[Hc P]|Hupd]".
+        + iModIntro. iNext. iApply iter_modal_intro; last first.
+          { do 2 iModIntro. iExists (S n); iFrame; done. }
+          iIntros (Q) "Q"; iModIntro; by iNext.
+        + iModIntro. iDestruct "Hupd" as (m Hstep) "[Hown Hupd]". iNext.
+          iPoseProof (IH with "Hown Hupd") as "Hit"; first done.
+          clear IH.
+          assert (m ≤ n) as [k ->]%nat_le_sum by lia.
+          rewrite Nat.add_comm Nat_iter_add.
+          iApply iter_modal_intro.
+          { by iIntros (Q) "$". }
+          iApply (iter_modal_mono with "[] Hit").
+          { iIntros (R S) "Hent H". by iApply "Hent". }
+          iIntros "H". iMod "H". iModIntro. iMod "H" as (m' Hle) "H".
+          iModIntro. iExists m'. iFrame. iPureIntro. lia.
+    Qed.
+
+    Lemma le_upd_elim_complete n P :
+      lc_supply n -∗
+      (|==£> P) -∗
+      Nat.iter (S n) (λ Q, |==> ▷ Q) P.
+    Proof.
+      iIntros "Hlc Hupd". iPoseProof (le_upd_elim with "Hlc Hupd") as "Hit".
+      rewrite Nat_iter_S_r. iApply (iter_modal_mono with "[] Hit").
+      { clear. iIntros (P Q) "Hent HP". by iApply "Hent". }
+      iIntros "Hupd". iMod "Hupd". iModIntro. iMod "Hupd".
+      iNext. iDestruct "Hupd" as "[%m (_ & _ & $)]".
+    Qed.
+  End le_upd.
+
+  Lemma lc_alloc `{!lcGpreS Σ} n :
+    ⊢ |==> ∃ _ : lcGS Σ, lc_supply n ∗ £ n.
+  Proof.
+    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
+    iMod (own_alloc (● n ⋅ ◯ n)) as (γLC) "[H● H◯]";
+      first (apply auth_both_valid; split; done).
+    pose (C := LcGS _ _ γLC).
+    iModIntro. iExists C. iFrame.
+  Qed.
+
+  Lemma lc_soundness `{!lcGpreS Σ} m φ :
+    (∀ {Hc: lcGS Σ}, £ m -∗ |==£> ⌜φ⌝) → φ.
+  Proof.
+    intros H. apply (@soundness (iResUR Σ) _ (S m)).
+    eapply bupd_plain_soundness; first apply _.
+    iStartProof.
+    iMod (lc_alloc m) as (C) "[H● H◯]".
+    iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "Hâ—¯").
+    iPoseProof (le_upd_elim_complete m with "H● Hc") as "H".
+    simpl. iMod "H". iModIntro. iNext.
+    clear H. iInduction m as [|m] "IH"; simpl; [done|].
+    iMod "H". iNext. by iApply "IH".
+  Qed.
+End le_upd.
+
+(** This should only be imported by the internal development of fancy updates. *)
+Module le_upd_if.
+  Export le_upd.
+
+  Section le_upd_if.
+    Context `{!lcGS Σ}.
+
+    Definition le_upd_if (b : bool) : iProp Σ → iProp Σ :=
+      if b then le_upd else bupd.
+
+    Global Instance le_upd_if_mono' b : Proper ((⊢) ==> (⊢)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_flip_mono' b :
+      Proper (flip (⊢) ==> flip (⊢)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_proper b : Proper ((≡) ==> (≡)) (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+    Global Instance le_upd_if_ne b : NonExpansive (le_upd_if b).
+    Proof. destruct b; apply _. Qed.
+
+    Lemma le_upd_if_intro b P : P -∗ le_upd_if b P.
+    Proof.
+      destruct b; [apply le_upd_intro | apply bupd_intro].
+    Qed.
+
+    Lemma le_upd_if_bind b P Q :
+      (P -∗ le_upd_if b Q) -∗ (le_upd_if b P) -∗ (le_upd_if b Q).
+    Proof.
+      destruct b; first apply le_upd_bind. simpl.
+      iIntros "HPQ >HP". by iApply "HPQ".
+    Qed.
+
+    Lemma le_upd_if_mono b P Q : (P ⊢ Q) → (le_upd_if b P) -∗ (le_upd_if b Q).
+    Proof.
+      destruct b; [apply le_upd_mono | apply bupd_mono].
+    Qed.
+    Lemma le_upd_if_trans b P : (le_upd_if b (le_upd_if b P)) -∗ le_upd_if b P.
+    Proof.
+      destruct b; [apply le_upd_trans | apply bupd_trans].
+    Qed.
+    Lemma le_upd_if_frame_r b P R : (le_upd_if b P) ∗ R -∗ le_upd_if b (P ∗ R).
+    Proof.
+      destruct b; [apply le_upd_frame_r | apply bupd_frame_r].
+    Qed.
+
+    Lemma bupd_le_upd_if b P : (|==> P) -∗ (le_upd_if b P).
+    Proof.
+      destruct b; [apply bupd_le_upd | done].
+    Qed.
+
+    Lemma le_upd_if_frame_l b R Q : (R ∗ le_upd_if b Q) -∗ le_upd_if b (R ∗ Q).
+    Proof.
+      rewrite comm le_upd_if_frame_r comm //.
+    Qed.
+
+    Lemma except_0_le_upd_if b P : ◇ (le_upd_if b P) ⊢ le_upd_if b (◇ P).
+    Proof.
+      rewrite /bi_except_0. apply or_elim; eauto using le_upd_if_mono, or_intro_r.
+      by rewrite -le_upd_if_intro -or_intro_l.
+    Qed.
+
+    (** Proof mode class instances that we need for the internal development,
+    i.e. for the definition of fancy updates. *)
+    Global Instance elim_bupd_le_upd_if b p P Q :
+      ElimModal True p false (bupd P) P (le_upd_if b Q) (le_upd_if b Q)%I.
+    Proof.
+      rewrite /ElimModal bi.intuitionistically_if_elim //=.
+      rewrite bupd_le_upd_if. iIntros "_ [HP HPQ]".
+      iApply (le_upd_if_bind with "HPQ HP").
+    Qed.
+
+    Global Instance from_assumption_le_upd_if b p P Q :
+      FromAssumption p P Q → KnownRFromAssumption p P (le_upd_if b Q).
+    Proof.
+      rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_if_intro.
+    Qed.
+
+    Global Instance from_pure_le_upd_if b a P φ :
+      FromPure a P φ → FromPure a (le_upd_if b P) φ.
+    Proof. rewrite /FromPure=> <-. apply le_upd_if_intro. Qed.
+
+    Global Instance is_except_0_le_upd_if b P : IsExcept0 P → IsExcept0 (le_upd_if b P).
+    Proof.
+      rewrite /IsExcept0=> HP.
+      by rewrite -{2}HP -(except_0_idemp P) -except_0_le_upd_if -(except_0_intro P).
+    Qed.
+
+    Global Instance from_modal_le_upd_if b P :
+      FromModal True modality_id (le_upd_if b P) (le_upd_if b P) P.
+    Proof. by rewrite /FromModal /= -le_upd_if_intro. Qed.
+
+    Global Instance elim_modal_le_upd_if b p P Q :
+      ElimModal True p false (le_upd_if b P) P (le_upd_if b Q) (le_upd_if b Q).
+    Proof.
+      by rewrite /ElimModal
+        intuitionistically_if_elim le_upd_if_frame_r wand_elim_r le_upd_if_trans.
+    Qed.
+
+    Global Instance frame_le_upd_if b p R P Q :
+      Frame p R P Q → Frame p R (le_upd_if b P) (le_upd_if b Q).
+    Proof. rewrite /Frame=><-. by rewrite le_upd_if_frame_l. Qed.
+  End le_upd_if.
+End le_upd_if.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 9c821c1b3ea4c7583f59eb489d935624d3de8cef..c39b636b62dd49bd098f01297e31934aac5a190e 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -5,58 +5,58 @@ From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
 (** All definitions in this file are internal to [fancy_updates] with the
-exception of what's in the [invGS] module. The module [invGS] is thus exported in
+exception of what's in the [wsatGS] module. The module [wsatGS] is thus exported in
 [fancy_updates], where [wsat] is only imported. *)
-Module invGS.
-  Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
-    invGpreS_inv : inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    invGpreS_enabled : inG Σ coPset_disjR;
-    invGpreS_disabled : inG Σ (gset_disjR positive);
+Module wsatGS.
+  Class wsatGpreS (Σ : gFunctors) : Set := WsatGpreS {
+    wsatGpreS_inv : inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    wsatGpreS_enabled : inG Σ coPset_disjR;
+    wsatGpreS_disabled : inG Σ (gset_disjR positive);
   }.
 
-  Class invGS (Σ : gFunctors) : Set := InvG {
-    inv_inG : invGpreS Σ;
+  Class wsatGS (Σ : gFunctors) : Set := WsatG {
+    wsat_inG : wsatGpreS Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
   }.
 
-  Definition invΣ : gFunctors :=
+  Definition wsatΣ : gFunctors :=
     #[GFunctor (gmap_viewRF positive (laterOF idOF));
       GFunctor coPset_disjR;
       GFunctor (gset_disjR positive)].
 
-  Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
+  Global Instance subG_wsatΣ {Σ} : subG wsatΣ Σ → wsatGpreS Σ.
   Proof. solve_inG. Qed.
-End invGS.
-Import invGS.
-Local Existing Instances inv_inG invGpreS_inv invGpreS_enabled invGpreS_disabled.
+End wsatGS.
+Import wsatGS.
+Local Existing Instances wsat_inG wsatGpreS_inv wsatGpreS_enabled wsatGpreS_disabled.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
-Definition ownI `{!invGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{!wsatGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
 Typeclasses Opaque ownI.
 Global Instance: Params (@invariant_unfold) 1 := {}.
 Global Instance: Params (@ownI) 3 := {}.
 
-Definition ownE `{!invGS Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{!wsatGS Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
 Global Instance: Params (@ownE) 3 := {}.
 
-Definition ownD `{!invGS Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{!wsatGS Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
 Global Instance: Params (@ownD) 3 := {}.
 
-Definition wsat `{!invGS Σ} : iProp Σ :=
+Definition wsat `{!wsatGS Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
     own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
-Context `{!invGS Σ}.
+Context `{!wsatGS Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
@@ -183,14 +183,14 @@ Qed.
 End wsat.
 
 (* Allocation of an initial world *)
-Lemma wsat_alloc `{!invGpreS Σ} : ⊢ |==> ∃ _ : invGS Σ, wsat ∗ ownE ⊤.
+Lemma wsat_alloc `{!wsatGpreS Σ} : ⊢ |==> ∃ _ : wsatGS Σ, wsat ∗ ownE ⊤.
 Proof.
   iIntros.
   iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γI) "HI";
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (InvG _ _ γI γE γD).
+  iModIntro; iExists (WsatG _ _ γI γE γD).
   rewrite /wsat /ownE -lock; iFrame.
   iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index aed7dc1e27a1632eba1936c9ff31332c725b8b43..ba106a831c04c221c006780e17be5e5c5222a311 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1640,6 +1640,24 @@ Qed.
 Global Instance limit_preserving_Persistent {A:ofe} `{Cofe A} (Φ : A → PROP) :
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+
+(* iterated modalities *)
+Lemma iter_modal_intro (M : PROP → PROP) P (n : nat) :
+  (∀ Q, Q ⊢ M Q) →
+  P -∗ Nat.iter n M P.
+Proof.
+  intros Hintro; induction n as [|n IHn]; simpl; first done.
+  etransitivity; first apply IHn. apply Hintro.
+Qed.
+
+Lemma iter_modal_mono (M : PROP → PROP) P Q (n : nat) :
+  (∀ P Q, (P -∗ Q) -∗ M P -∗ M Q)  →
+  (P -∗ Q) -∗
+  Nat.iter n M P -∗ Nat.iter n M Q.
+Proof.
+  intros Hmono; induction n as [|n IHn]; simpl; first done.
+  rewrite -Hmono //.
+Qed.
 End derived.
 
 End bi.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 23fbdff87fc734fc52ff46a5587d8c13d4dc0e8d..1429e59f9f23c202309970eb6ab325b9b3c8f476 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -78,50 +78,95 @@ Proof.
 Qed.
 
 Lemma wp_not_stuck κs nt e σ ns Φ :
-  state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
+  state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤, ∅}=∗ ⌜not_stuck e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
-  destruct (to_val e) as [v|] eqn:?; first by eauto.
+  destruct (to_val e) as [v|] eqn:?.
+  { iMod (fupd_mask_subseteq ∅); first set_solver. iModIntro. eauto. }
   iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
-  iMod (fupd_plain_mask with "H") as %?; eauto.
+  iMod "H" as "%". iModIntro. eauto.
 Qed.
 
-Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 ns σ2 nt:
+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
   ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
-    ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝ ∗
     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.
   iModIntro. iApply (step_fupdN_wand with "Hwp").
   iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
-  iMod (fupd_plain_keep_l ⊤
-    ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
-    (state_interp σ2 (n + ns) κs' (nt + nt') ∗
-     wptp s es2 (Φs ++ replicate nt' fork_post))%I
-    with "[$Hσ $Ht]") as "(%&Hσ&Hwp)".
-  { iIntros "(Hσ & Ht)" (e' -> He').
-    move: He' => /(elem_of_list_split _ _)[?[?->]].
-    iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ?) "[? Hwp]".
-    iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
-    iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
-  iExists _. iSplitR; first done. iFrame "Hσ".
+  iExists _. iFrame "Hσ".
   iApply big_sepL2_fupd.
-  iApply (big_sepL2_impl with "Hwp").
+  iApply (big_sepL2_impl with "Ht").
   iIntros "!#" (? e Φ ??) "Hwp".
   destruct (to_val e) as [v2|] eqn:He2'; last done.
   apply of_to_val in He2' as <-. simpl. iApply wp_value_fupd'. done.
 Qed.
+
+
+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 -∗
+  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.
+  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].
+  destruct ((Φs ++ replicate nt' fork_post) !! i) as [Φ|] eqn: Hlook2; last first.
+  { rewrite big_sepL2_alt. iDestruct "Ht" as "[%Hlen _]". exfalso.
+    eapply lookup_lt_Some in Hlook. rewrite Hlen in Hlook.
+    eapply lookup_lt_is_Some_2 in Hlook. rewrite Hlook2 in Hlook.
+    destruct Hlook as [? ?]. naive_solver. }
+  iDestruct (big_sepL2_lookup with "Ht") as "Ht"; [done..|].
+  by iApply (wp_not_stuck with "Hσ").
+Qed.
 End adequacy.
 
+Local Lemma wp_progress_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 e2
+        (num_laters_per_step : nat → nat)  :
+    (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+    ⊢ |={⊤}=> ∃
+         (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
+         (Φs : list (val Λ → iProp Σ))
+         (fork_post : val Λ → iProp Σ)
+         state_interp_mono,
+       let _ : irisGS Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+                                  state_interp_mono
+       in
+       stateI σ1 0 κs 0 ∗
+       ([∗ list] e;Φ ∈ es;Φs, WP e @ ⊤ {{ Φ }})) →
+  nsteps n (es, σ1) κs (t2, σ2) →
+  e2 ∈ t2 →
+  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) "_".
+  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|].
+  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. }
+  iApply (step_fupdN_wand with "H"). iIntros "$".
+Qed.
+
+
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 φ
+(** The lemma is parameterized by [use_credits] over whether to make later credits available or not.
+  Below, two specific instances are provided. *)
+Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1 n κs t2 σ2 φ
         (num_laters_per_step : nat → nat) :
-  (∀ `{Hinv : !invGS Σ},
-    ⊢ |={⊤}=> ∃
-         (s: stuckness)
+  (* WP *)
+  (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+      ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
          (fork_post : val Λ → iProp Σ)
@@ -156,9 +201,10 @@ Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 φ
   (* Then we can conclude [φ] at the meta-level. *)
   φ.
 Proof.
-  intros Hwp ?.
-  apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n))=> Hinv.
-  iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
+  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 *)
+  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) _ []
@@ -167,16 +213,31 @@ Proof.
     with "[-]" as "H"; last first.
   { destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
   iApply (step_fupdN_wand with "H").
-  iMod 1 as (nt' ?) "(Hσ & Hval) /=".
+  iMod 1 as (nt') "(Hσ & Hval) /=".
   iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
   iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
   rewrite replicate_length in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
-  iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
-  by rewrite big_sepL2_replicate_r // big_sepL_omap.
+  iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'"); [congruence| |]; last first.
+  { by rewrite big_sepL2_replicate_r // big_sepL_omap. }
+  (* we run the adequacy proof again to get this assumption *)
+  iPureIntro. intros e2 -> Hel.
+  eapply (wp_progress_gen use_credits);
+    [ done | clear stateI Φ fork_post state_interp_mono Hlen1 Hlen3 | done|done].
+  iIntros (??).
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
+  iModIntro. iExists _, _, _, _. iFrame.
 Qed.
 
+(** Adequacy when using later credits *)
+Definition wp_strong_adequacy_lc := wp_strong_adequacy_gen true.
+Global Arguments wp_strong_adequacy_lc _ _ {_}.
+(** Adequacy when using no later credits *)
+Definition wp_strong_adequacy_no_lc := wp_strong_adequacy_gen false.
+Global Arguments wp_strong_adequacy_no_lc _ _ {_}.
+
+
 (** Since the full adequacy statement is quite a mouthful, we prove some more
 intuitive and simpler corollaries. These lemmas are morover stated in terms of
 [rtc erased_step] so one does not have to provide the trace. *)
@@ -229,8 +290,9 @@ In other words, the state interpretation must ignore [ns] and [nt], the number
 of laters per step must be 0, and the proof of [state_interp_mono] must have
 this specific proof term.
 *)
-Corollary wp_adequacy Σ Λ `{!invGpreS Σ} s e σ φ :
-  (∀ `{Hinv : !invGS Σ} κs,
+(** Again, we first prove a lemma generic over the usage of credits. *)
+Lemma wp_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e σ φ :
+  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -242,9 +304,9 @@ Corollary wp_adequacy Σ Λ `{!invGpreS Σ} s e σ φ :
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy Σ _); [|done]=> ?.
-  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
-  iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
+  eapply (wp_strong_adequacy_gen use_credits Σ _); [ | done]=> ??.
+  iMod Hwp as (stateI fork_post) "[Hσ Hwp]"; first done.
+  iExists (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
   iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
@@ -252,8 +314,16 @@ Proof.
   iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
 Qed.
 
-Corollary wp_invariance Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
-  (∀ `{Hinv : !invGS Σ} κs,
+(** Instance for using credits *)
+Definition wp_adequacy_lc := wp_adequacy_gen true.
+Global Arguments wp_adequacy_lc _ _ {_}.
+(** Instance for no credits  *)
+Definition wp_adequacy_no_lc := wp_adequacy_gen false.
+Global Arguments wp_adequacy_no_lc _ _ {_}.
+
+
+Lemma wp_invariance_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
+  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -265,12 +335,17 @@ Corollary wp_invariance Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy Σ _); [|done]=> ?.
-  iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
-  iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
+  eapply (wp_strong_adequacy_gen use_credits Σ); [done| |done]=> ? Hc.
+  iMod (Hwp _ Hc κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
+  iExists (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
   iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
   iDestruct (big_sepL2_nil_inv_r with "H") as %->.
   iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
   by iApply fupd_mask_intro_discard; first set_solver.
 Qed.
+
+Definition wp_invariance_lc := wp_invariance_gen true.
+Global Arguments wp_invariance_lc _ _ {_}.
+Definition wp_invariance_no_lc := wp_invariance_gen false.
+Global Arguments wp_invariance_no_lc _ _ {_}.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 34eb93c7969a638489d56be44f474a99bf020f28..d467e21f5d564c77fc34db7291216b41c7f33b04 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -51,11 +51,11 @@ Global Instance: Params (@ownP) 3 := {}.
 
 (* Adequacy *)
 Theorem ownP_adequacy Σ `{!ownPGpreS Λ Σ} s e σ φ :
-  (∀ `{!ownPGS Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{!ownPGS Λ Σ, !HasLc Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
-  intros Hwp. apply (wp_adequacy Σ _).
-  iIntros (? κs).
+  intros Hwp. apply (wp_adequacy_lc Σ _).
+  iIntros (? ? κs).
   iMod (own_alloc (●E σ ⋅ ◯E σ)) as (γσ) "[Hσ Hσf]";
     first by apply excl_auth_valid.
   iModIntro. iExists (λ σ κs, own γσ (●E σ))%I, (λ _, True%I).
@@ -64,14 +64,14 @@ Proof.
 Qed.
 
 Theorem ownP_invariance Σ `{!ownPGpreS Λ Σ} s e σ1 t2 σ2 φ :
-  (∀ `{!ownPGS Λ Σ},
+  (∀ `{!ownPGS Λ Σ, !HasLc Σ},
       ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
       |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
-  iIntros (? κs).
+  intros Hwp Hsteps. eapply (wp_invariance_lc Σ Λ s e σ1 t2 σ2 _)=> //.
+  iIntros (? ? κs).
   iMod (own_alloc (●E σ1 ⋅ ◯E σ1)) as (γσ) "[Hσ Hσf]";
     first by apply auth_both_valid_discrete.
   iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 0e6dd10e749d30247a128ab429b7bb9c442ff6a8..74fb6223c846c246d2e65fb3e17cbab1a68d7f9e 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -104,7 +104,7 @@ Proof.
   iApply (twptp_app [_] with "(IH' [//])"). by iApply "IH".
 Qed.
 
-Lemma twptp_total σ ns nt t :
+Lemma twptp_total `{!HasNoLc Σ} σ ns nt t :
   state_interp σ ns [] nt -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
   iIntros "Hσ Ht". iRevert (σ ns nt) "Hσ". iRevert (t) "Ht".
@@ -117,7 +117,7 @@ Qed.
 End adequacy.
 
 Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
-  (∀ `{Hinv : !invGS Σ},
+  (∀ `{Hinv : !invGS Σ} `{!HasNoLc Σ},
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (** We abstract over any instance of [irisG], and thus any value of
@@ -134,9 +134,9 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
-  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _)=> Hinv HNC.
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
   set (iG := IrisG _ _ Hinv stateI fork_post num_laters_per_step stateI_mono).
-  iApply (@twptp_total _ _ iG _ n with "Hσ").
+  iApply (@twptp_total _ _ iG _ _ n with "Hσ").
   by iApply (@twp_twptp _ _ (IrisG _ _ Hinv _ fork_post _ _)).
 Qed.
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index 9d4ad1e7ff8b381d819fcff35361d453167d142e..f14ffa9f95ee1caa17ea36974c803f8bd3fb698f 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -25,19 +25,19 @@ with a non-constant step index function. We thus use the more general
 [wp_adequacy], and it hence would make sense to see if we can prove a version
 of [wp_adequacy] for a non-constant step version. *)
 Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
-  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{!heapGS Σ, !HasLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp.
   apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
-  eapply (wp_strong_adequacy Σ _); [|done].
-  iIntros (Hinv).
+  eapply (wp_strong_adequacy_lc Σ _); [|done].
+  iIntros (Hinv HC).
   iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iMod (mono_nat_own_alloc) as (γ) "[Hsteps _]".
   iDestruct (Hwp (HeapGS _ _ _ _ _ _ _) with "Hi") as "Hwp".
-  iModIntro. iExists s.
+  iModIntro.
   iExists (λ σ ns κs nt, (gen_heap_interp σ.(heap) ∗
                           proph_map_interp κs σ.(used_proph_id) ∗
                           mono_nat_auth_own γ 1 ns))%I.
diff --git a/iris_heap_lang/total_adequacy.v b/iris_heap_lang/total_adequacy.v
index f947da923faec7dc30a5c7e9bc61e88cada29131..a6287612f45aea9f7e6c5315e5ca91dfade07b1c 100644
--- a/iris_heap_lang/total_adequacy.v
+++ b/iris_heap_lang/total_adequacy.v
@@ -6,10 +6,10 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 Definition heap_total Σ `{!heapGpreS Σ} s e σ φ :
-  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
+  (∀ `{!heapGS Σ, !HasNoLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
   sn erased_step ([e], σ).
 Proof.
-  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
+  intros Hwp; eapply (twp_total _ _); iIntros (??) "".
   iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index c20fdf92b1a3259b1093f8788d014782ee288130..420b6229bcb7a6a19809d94d81eb0d61362e1a62 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -452,4 +452,4 @@ End error_tests.
 
 (* Test a closed proof *)
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
-Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
+Proof. eapply (heap_adequacy heapΣ)=> ??. iIntros "_". by iApply heap_e_spec. Qed.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 378177ec1cac857a5ec8462674ea08494500dc5e..f6aa093dc229f640bad8b4a38b2dc905e50fc7d6 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -135,7 +135,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ??. iIntros "_". iApply client_safe. Qed.
 
 (* Since we check the output of the test files, this means
 our test suite will fail if we ever accidentally add an axiom
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 506ac4cc71f5ec82f54c09325872fd89242f8e7b..b9ca8654bbe231657246b32f491d3d19b96dc61c 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -153,4 +153,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ??. iIntros "_". iApply client_safe. Qed.
diff --git a/tex/extended-logic.tex b/tex/extended-logic.tex
index f52d3a4dc9e52844491fb4ecdeeed5c67cfc2794..8260c71df1ba99fc18b556885497ed8707ecb00e 100644
--- a/tex/extended-logic.tex
+++ b/tex/extended-logic.tex
@@ -196,6 +196,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
 
 
 \subsection{Timeless Propositions and Except-0}
+\label{sec:timeless-props}
 
 One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
 It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
diff --git a/tex/iris.sty b/tex/iris.sty
index 2eae486b47c8b4496ed08ba80824de14bd994dbe..5c2379219c788bfab2702c654459e315bad066c4 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -309,7 +309,7 @@
       {#2}_{#1}%
     }{%
       % Two masks
-      \tensor*[^{#1}]{#2}{^{#3}}
+      \tensor*[_{#1}]{#2}{_{#3}}
     }%
   }}%
 \NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
@@ -330,6 +330,19 @@
 
 \NewDocumentCommand\Acc{O{} O{} m m}{#3 \mathrel{~\vsGen[#1]{\propto}[#2]~} #4}
 
+%% Later credits
+\newcommand{\laterCredit}[1]{\text{\textsterling}\hskip 0.1em \ensuremath{#1}}
+\newcommand{\laterCreditSupply}[1]{\text{\textsterling}_{\!\bullet}\hskip 0.1em \ensuremath{#1}}
+% macro for oversetting a character with custom spacing
+% \makeatletter
+% \newcommand{\osetCharacter}[3][0ex]{%
+%   \mathrel{\mathop{#3}\limits^{
+%     \vbox to#1{\kern-2\ex@
+%     \hbox{$\scriptstyle#2$}\vss}}}}
+% \makeatother
+\newcommand{\creditUpd}{\mathop{\pvs^{\!\!\textsterling}}}
+\newcommand{\LaterCreditsFlag}{\textsf{UseLaterCredits}}
+
 
 %% Hoare Triples
 
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index ca3f25f938712421285eb083a5f0927cad668299..2334d994e0fedb40d861c1a3269246aca19c2bed 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -6,6 +6,95 @@ This section describes how to build a program logic for an arbitrary language (\
 So in the following, we assume that some language $\Lang$ was fixed.
 Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composable-resources}.
 
+\subsection{Later Credits}
+Introducing a later modality is easy (see~\ruleref{later-intro}), but eliminating them can be tricky.
+Laters often appear in the middle of our proofs after unfolding a circular construction (\eg by opening an invariant, see~\secref{sec:invariants}).
+In these cases, we get to assume $\later \prop$, but we really want $\prop$ to continue in the proof.
+Iris offers us four options to do so.
+We have seen two of them already: timeless propositions (see~\secref{sec:timeless-props}) and the commuting rules for later.
+Together, they can be used to turn $\later \prop$ into $\prop$, or to delay when we have to deal with the later modality by commuting it inward (\eg{} over an existential quantifer and a separating conjunction).
+Another option, which we will encounter in~\secref{sec:weakest-pre}, is taking program steps: every program step allows us to eliminate (at least) one later (see~\ruleref{wp-lift-step}).
+We now introduce the fourth option: \emph{later credits}.
+Later credits turn the right to eliminate a later into an ownable separation-logic resource $\laterCredit{n}$, where $n$ is the number of laters that we can eliminate.
+
+\paragraph{Resources}
+We assume that the camera
+\[ \textdom{LaterCredits} \eqdef{} \authm{(\nat^{+})} \]
+is available (\ie{} part of $\Sigma$), where $\nat^{+}$ is the RA derived from the monoid $\nat$ with operation $+$, and that an instance of it has been created and made globally available at the beginning of verification under the name $\gname_{\textdom{Credits}}$.
+We define the following notations for the fragments and authoritative part:
+\begin{mathpar}
+  \laterCredit{n} \eqdef{} \ownGhost{\gname_{\textdom{Credits}}}{\authfrag{n}}
+
+  \laterCreditSupply{n} \eqdef{} \ownGhost{\gname_{\textdom{Credits}}}{\authfull{n}}
+\end{mathpar}
+
+This definition satisfies the following laws:
+\begin{mathpar}
+  \inferH{Credit-Split}{}{\laterCredit{(n + m)} \Leftrightarrow \laterCredit{n} * \laterCredit{m}}
+
+  \inferH{Credit-Timeless}{}{\timeless{\laterCredit{n}}}\\
+
+  \inferH{Credit-SupplyBound}{}{\laterCreditSupply{m} * \laterCredit{n} \proves m \geq n}
+
+  \inferH{Credit-SupplyDecr}{}{\laterCreditSupply{(n + m)} * \laterCredit{n} \proves \pvs \laterCreditSupply{m}}
+
+  \inferH{Credit-SupplyExcl}{}{\laterCreditSupply{m_1} * \laterCreditSupply{m_2} \proves \FALSE}
+\end{mathpar}
+
+\paragraph{Later Elimination Update}%
+\label{sec:later-credits}
+To eliminate laters by \emph{spending} later credits $\laterCredit{n}$, we define a \emph{later-elimination update} $\creditUpd{}\prop$ on top of the basic update modality.
+It satisfies all the properties of basic updates, except for \ruleref{upd-plainly}, but with the additional rule
+\begin{mathpar}
+  \inferH{credit-upd-use}
+  {}
+  {\later \prop * \laterCredit{1} \proves \creditUpd{} \prop}
+\end{mathpar}
+\ruleref{credit-upd-use} allows to \emph{spend} one credit in exchange for stripping one later off of $\prop$.
+
+The later-elimination update is defined by guarded recursion:
+\begin{align*}
+  \creditUpd{}&\eqdef \MU~\mathit{upd}. \Lam \prop. \All n. \laterCreditSupply{n} \wand \upd{} (\laterCreditSupply{n} * \prop) \lor (\Exists m < n. \laterCreditSupply{m} * \later \mathit{upd}(\prop))
+\end{align*}
+It threads through the authoritative resource $\laterCreditSupply{n}$, the credit supply, to control how many credits can be spent in total.
+The basic update ensures that the later elimination update inherits the ability to update resources.
+In the first disjunct (the \enquote{base case}), no credits are spent.
+In the second disjunct (the \enquote{recursive case}), a later can be eliminated before going into recursion.
+To take the second disjunct, the credit supply $\laterCreditSupply{n}$ has to be decreased, which means giving up at least $\laterCredit{1}$.
+
+The later-elimination update satisfies the following laws:
+\begin{mathpar}
+  \inferH{credit-upd-mono}
+  {\prop \proves \propB}
+  {\creditUpd\prop \proves \creditUpd\propB}
+
+  \inferH{credit-upd-intro}
+  {}{\prop \proves \creditUpd \prop}
+
+  \inferH{credit-upd-trans}
+  {}
+  {\creditUpd \creditUpd \prop \proves \creditUpd \prop}
+
+  \inferH{credit-upd-frame}
+  {}{\propB * \creditUpd\prop \proves \creditUpd (\propB * \prop)}
+
+  \inferH{credit-upd-update}
+  %{}
+  %{\upd\creditUpd{} \prop \proves \creditUpd{} \prop}
+  {\melt \mupd \meltsB}
+  {\ownM\melt \proves \creditUpd \Exists\meltB\in\meltsB. \ownM\meltB}
+
+  \inferH{credit-upd-later}
+  {}
+  {\laterCredit{1} * \later \creditUpd{} \prop \proves \creditUpd{} \prop}
+  %\inferH{credit-upd-use}
+  %{}
+  %{\later \prop * \laterCredit{1} \proves \creditUpd{} \prop}
+\end{mathpar}
+The rule \ruleref{credit-upd-use} shown above can be derived from \ruleref{credit-upd-later} and \ruleref{credit-upd-intro}.
+
+Note the absence of a rule corresponding to \ruleref{upd-plainly}, which is not validated by the model.
+As some existing Iris developments rely on \ruleref{upd-plainly}, we parameterize the logic by a boolean constant $\LaterCreditsFlag$ that determines whether the later-elimination update is used instead of the basic update, in particular in the definition of fancy updates below.
 
 \subsection{World Satisfaction, Invariants, Fancy Updates}
 \label{sec:invariants}
@@ -44,8 +133,17 @@ The following proposition states that an invariant with name $\iname$ exists and
   {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
 
 \paragraph{Fancy Updates and View Shifts.}
-Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
-\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) \]
+Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$) or later-elimination updates (\Sref{sec:later-credits}), except that they also have access to world satisfaction and can enable and disable invariants.
+
+Depending on how the logic is parameterized with the $\LaterCreditsFlag$, fancy updates are defined on top the basic update or the later-elimination update.
+This influences which rules fancy updates satisfy: either fancy updates can be used to eliminate later credits, or they satisfy certain interaction laws with the plainly modality.
+
+\[ \pvs[\mask_1][\mask_2] \prop \eqdef
+  \begin{cases}
+    W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \creditUpd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) & \text{if } \LaterCreditsFlag = \textsf{true}\\
+    W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) & \text{if } \LaterCreditsFlag = \textsf{false}\\
+  \end{cases}
+  \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
 Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
 \footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
@@ -80,6 +178,10 @@ Fancy updates satisfy the following basic proof rules:
 \infer[fup-timeless]
 {\timeless\prop}
 {\later\prop \proves \pvs[\mask] \prop}
+
+\infer[fup-credit-use]
+{\LaterCreditsFlag = \textsf{true}}
+{\laterCredit{1} * \later \pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \prop}
 \end{mathparpagebreakable}
 (There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)
 
@@ -134,6 +236,7 @@ Still, just to give an idea of what view shifts ``are'', here are some proof rul
 \end{mathparpagebreakable}
 
 \subsection{Weakest Precondition}
+\label{sec:weakest-pre}
 
 Finally, we can define the core piece of the program logic, the proposition that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
 
@@ -204,7 +307,7 @@ We will also want a rule that connect weakest preconditions to the operational s
 This basically just copies the second branch (the non-value case) of the definition of weakest preconditions.
 
 \begin{mathpar}
-  \infer[wp-lift-step]
+  \inferH{wp-lift-step}
   {\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)) * {}\\
@@ -223,10 +326,11 @@ The purpose of the adequacy statement is to show that our notion of weakest prec
 The most general form of the adequacy statement is about proving properties of an arbitrary program execution.
 
 \begin{thm}[Adequacy]
-  Assume we are given some $\vec\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $(\vec\expr_1, \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
+  Assume we are given some $\vec\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $(\vec\expr_1, \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$.
+  Moreover, assume we are given a stuckness parameter $\stuckness$ and \emph{meta-level} property $\metaprop$ that we want to show.
   To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
 \begin{align*}
- &\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \vec\pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \left(\Sep_{\expr,\pred \in \vec\expr_1,\vec\pred} \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\top]{x.\; \pred(x)}\right) * \left(\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
+ &\TRUE \proves \pvs[\top] \Exists \stateinterp, \vec\pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \left(\Sep_{\expr,\pred \in \vec\expr_1,\vec\pred} \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\top]{x.\; \pred(x)}\right) * \left(\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
 \end{align*}
 where $\consstate$ describes states that are consistent with the state interpretation and postconditions:
 \begin{align*}
@@ -255,7 +359,7 @@ In other words, to show that $\metaprop$ holds, we have to prove an entailment i
   \item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_2, \state_2)$.
 \end{itemize}
 Notice that the state interpretation and the postconditions are chosen \emph{after} doing a fancy update, which allows them to depend on the names of ghost variables that are picked in that initial fancy update.
-This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to.
+This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to (\eg the name $\gname_{\textdom{Credits}}$).
 
 $\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
 \begin{itemize}
@@ -290,7 +394,7 @@ Similarly we could show that the postcondition makes adequate statements about t
 \begin{cor}[Adequate postcondition]
   Assume we are given some $\expr_1$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
 \[
-\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; x \in V}
+\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; x \in V}
 \]
   Then it is the case that:
 \[
@@ -307,7 +411,7 @@ As a final example, we could use adequacy to show that the state $\state$ of the
 \begin{cor}[Adequate state interpretation]
   Assume we are given some $\expr_1$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
 \[
-\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{\pred} * (\All \state_2, n_s, n_t. \stateinterp(\state_2,n_s(),n_t) \!\vs[\top][\emptyset] \state_2 \in \Sigma)
+\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{\pred} * (\All \state_2, n_s, n_t. \stateinterp(\state_2,n_s,(),n_t) \!\vs[\top][\emptyset] \state_2 \in \Sigma)
 \]
   Then it is the case that:
 \[