From ebf06f918f428b435cb2589240ad610dc8dd543d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jun 2018 01:33:18 +0200
Subject: [PATCH] Fine-grained post-conditions for forked-off threads.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This commit extends the state interpretation with an additional parameter to
talk about the number of forked-off threads, and a fixed postcondition for each
forked-off thread:

    state_interp : Λstate → list Λobservation → nat → iProp Σ;
    fork_post : iProp Σ;

This way, instead of having `True` as the post-condition of `Fork`, one can
have any post-condition, which is then recorded in the state interpretation.
The point of keeping track of the postconditions of forked-off threads, is that
we get an (additional) stronger adequacy theorem:

    Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
       (∀ `{Hinv : invG Σ} κs,
         (|={⊤}=> ∃
             (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
             (fork_post : iProp Σ),
           let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
           stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
             let m := length vs in
             stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
      rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
      φ v.

The difference with the ordinary adequacy theorem is that this one only applies
once all threads terminated. In this case, one gets back the post-conditions
`[∗] replicate m fork_post` of all forked-off threads.

In Iron we showed that we can use this mechanism to make sure that all
resources are disposed of properly in the presence of fork-based concurrency.
---
 theories/heap_lang/lifting.v                |  40 ++--
 theories/heap_lang/total_adequacy.v         |   4 +-
 theories/program_logic/adequacy.v           | 228 +++++++++++++-------
 theories/program_logic/ectx_lifting.v       |  74 ++++---
 theories/program_logic/lifting.v            |  99 ++++++---
 theories/program_logic/ownp.v               |  30 ++-
 theories/program_logic/total_adequacy.v     |  65 +++---
 theories/program_logic/total_ectx_lifting.v |  56 +++--
 theories/program_logic/total_lifting.v      |  71 ++++--
 theories/program_logic/total_weakestpre.v   |  65 +++---
 theories/program_logic/weakestpre.v         |  58 +++--
 11 files changed, 491 insertions(+), 299 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 143dc1424..505b93895 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -16,8 +16,9 @@ Class heapG Σ := HeapG {
 
 Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
-  state_interp σ κs :=
-    (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I
+  state_interp σ κs _ :=
+    (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
+  fork_post := True%I;
 }.
 
 (** Override the notations so that scopes and coercions work out *)
@@ -162,7 +163,7 @@ Lemma wp_fork s E e Φ :
   ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "He HΦ".
-  iApply wp_lift_pure_det_head_step; [by eauto|intros; inv_head_step; by eauto|].
+  iApply wp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
   iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
 Qed.
 
@@ -170,7 +171,7 @@ Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
   iIntros "He HΦ".
-  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
+  iApply twp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
   iIntros "!> /= {$He}". by iApply twp_value.
 Qed.
 
@@ -179,7 +180,7 @@ Lemma wp_alloc s E v :
   {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by auto.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -188,7 +189,7 @@ Lemma twp_alloc s E v :
   [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
   iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
@@ -198,7 +199,7 @@ Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -206,7 +207,7 @@ Lemma twp_load s E l q v :
   [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -217,7 +218,7 @@ Lemma wp_store s E l v' v :
 Proof.
   iIntros (Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
@@ -228,7 +229,7 @@ Lemma twp_store s E l v' v :
 Proof.
   iIntros (Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
@@ -240,7 +241,7 @@ Lemma wp_cas_fail s E l q v' v1 v2 :
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -250,7 +251,7 @@ Lemma twp_cas_fail s E l q v' v1 v2 :
   [[{ RET LitV (LitBool false); l ↦{q} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -261,7 +262,7 @@ Lemma wp_cas_suc s E l v1 v2 :
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
   iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
@@ -272,7 +273,7 @@ Lemma twp_cas_suc s E l v1 v2 :
   [[{ RET LitV (LitBool true); l ↦ v2 }]].
 Proof.
   iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
@@ -283,7 +284,7 @@ Lemma wp_faa s E l i1 i2 :
   {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
@@ -293,7 +294,7 @@ Lemma twp_faa s E l i1 i2 :
   [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
@@ -304,7 +305,7 @@ Lemma wp_new_proph :
   {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
   iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
   iMod (@proph_map_alloc with "HR") as "[HR Hp]".
@@ -323,7 +324,7 @@ Lemma wp_resolve_proph p v w:
   {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
 Proof.
   iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
   iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
   iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
@@ -331,8 +332,7 @@ Proof.
   iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
   iSplitR "HΦ".
   - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
-    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
+    rewrite dom_delete. set_solver.
   - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
 Qed.
-
 End lifting.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 9006687fa..4294e9940 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -12,6 +12,8 @@ Proof.
   iMod (gen_heap_init σ.(heap)) as (?) "Hh".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.
-  iExists (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
+  iExists
+    (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
+    True%I; iFrame.
   iApply (Hwp (HeapG _ _ _ _)).
 Qed.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index ab9e3e583..b8743f29f 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -39,14 +39,14 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, fork_post }})%I.
 
-Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
+Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
-  ={E,∅}▷=∗ (state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
+  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤,∅}▷=∗
+  state_interp σ2 κs (length efs + m) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s efs.
 Proof.
-  rewrite {1}wp_unfold /wp_pre. iIntros (?) "[Hσ H]".
+  rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
   iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
   iMod ("H" $! e2 σ2 efs with "[//]") as "H".
@@ -55,43 +55,52 @@ Qed.
 
 Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
-  state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
-  ==∗ ∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ |={⊤,∅}▷=> (state_interp σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+  state_interp σ1 (κ ++ κs) (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1 ==∗
+  ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗
+  |={⊤,∅}▷=> state_interp σ2 κs (pred (length t2)) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
 Proof.
-  iIntros (Hstep) "(HW & He & Ht)".
+  iIntros (Hstep) "Hσ He Ht".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
-  - iExists e2', (t2' ++ efs). iSplitR; first by eauto.
-    iFrame "Ht". iApply wp_step; eauto with iFrame.
+  - iExists e2', (t2' ++ efs). iModIntro. iSplitR; first by eauto.
+    iMod (wp_step with "Hσ He") as "H"; first done.
+    iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)".
+    iIntros "!>". rewrite Nat.add_comm app_length. iFrame.
   - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
-    iDestruct "Ht" as "($ & He' & $)". iFrame "He".
-    iApply wp_step; eauto with iFrame.
+    iFrame "He". iDestruct "Ht" as "(Ht1 & He1 & Ht2)".
+    iModIntro. iMod (wp_step with "Hσ He1") as "H"; first done.
+    iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
+    rewrite !app_length /= !app_length.
+    replace (length t1' + S (length t2' + length efs))
+      with (length efs + (length t1' + S (length t2'))) by omega. iFrame.
 Qed.
 
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
-  |={⊤,∅}▷=>^n (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ state_interp σ2 κs' ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+  state_interp σ1 (κs ++ κs') (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1
+  ={⊤,∅}▷=∗^n ∃ e2 t2',
+    ⌜t2 = e2 :: t2'⌝ ∗
+    state_interp σ2 κs' (pred (length t2)) ∗
+    WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
 Proof.
-  revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
-  { inversion_clear 1; iIntros "(?&?&?)"; iExists e1, t1; iFrame; eauto 10. }
-  iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite <- app_assoc.
-  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
-  iMod "H". iModIntro; iNext. iMod "H". iModIntro.
-  by iApply IH.
+  revert e1 t1 κs κs' t2 σ1 σ2; simpl.
+  induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
+  { inversion_clear 1; iIntros "???"; iExists e1, t1; iFrame; eauto 10. }
+  iIntros (Hsteps) "Hσ He Ht". inversion_clear Hsteps as [|?? [t1' σ1']].
+  rewrite -(assoc_L (++)).
+  iMod (wptp_step with "Hσ He Ht") as (e1' t1'' ?) ">H"; first eauto; simplify_eq.
+  iIntros "!> !>". iMod "H" as "(Hσ & He & Ht)". iModIntro.
+  by iApply (IH with "Hσ He Ht").
 Qed.
 
-Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
+Lemma wptp_result φ κs' s n e1 t1 κs v2 t2 σ1 σ2  :
   nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2) →
-  state_interp σ1 (κs ++ κs') ∗
-  WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ κs' ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗
-  wptp s t1 ⊢
-  |={⊤,∅}▷=>^(S n) ⌜φ v2 σ2⌝.
+  state_interp σ1 (κs ++ κs') (length t1) -∗
+  WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ κs' (length t2) ={⊤,∅}=∗ ⌜φ v σ⌝ }} -∗
+  wptp s t1 ={⊤,∅}▷=∗^(S n) ⌜φ v2 σ2⌝.
 Proof.
-  intros. rewrite Nat_iter_S_r wptp_steps //.
-  apply step_fupdN_mono.
+  iIntros (?) "Hσ He Ht". rewrite Nat_iter_S_r.
+  iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
+  iApply (step_fupdN_wand with "H").
   iDestruct 1 as (e2 t2' ?) "(Hσ & H & _)"; simplify_eq.
   iMod (wp_value_inv' with "H") as "H".
   iMod (fupd_plain_mask_empty _ ⌜φ v2 σ2⌝%I with "[H Hσ]") as %?.
@@ -99,109 +108,166 @@ Proof.
   by iApply step_fupd_intro.
 Qed.
 
-Lemma wp_safe E e σ κs Φ :
-  state_interp σ κs -∗ WP e @ E {{ Φ }} ={E, ∅}▷=∗ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+Lemma wptp_all_result φ κs' s n e1 t1 κs v2 vs2 σ1 σ2 :
+  nsteps n (e1 :: t1, σ1) κs (of_val <$> v2 :: vs2, σ2) →
+  state_interp σ1 (κs ++ κs') (length t1) -∗
+  WP e1 @ s; ⊤ {{ v,
+    let m' := length vs2 in
+    state_interp σ2 κs' m' -∗ [∗] replicate m' fork_post ={⊤,∅}=∗ ⌜φ v ⌝ }} -∗
+  wptp s t1
+  ={⊤,∅}▷=∗^(S n) ⌜φ v2 ⌝.
+Proof.
+  iIntros (Hstep) "Hσ He Ht". rewrite Nat_iter_S_r.
+  iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
+  iApply (step_fupdN_wand with "H").
+  iDestruct 1 as (e2 t2' ?) "(Hσ & H & Hvs)"; simplify_eq/=.
+  rewrite fmap_length. iMod (wp_value_inv' with "H") as "H".
+  iAssert ([∗] replicate (length vs2) fork_post)%I with "[> Hvs]" as "Hm".
+  { clear Hstep. iInduction vs2 as [|v vs] "IH"; csimpl; first by iFrame.
+    iDestruct "Hvs" as "[Hv Hvs]".
+    iMod (wp_value_inv' with "Hv") as "$". by iApply "IH". }
+  iMod (fupd_plain_mask_empty _ ⌜φ v2⌝%I with "[H Hm Hσ]") as %?.
+  { iApply ("H" with "Hσ Hm"). }
+  by iApply step_fupd_intro.
+Qed.
+
+Lemma wp_safe κs m e σ Φ :
+  state_interp σ κs m -∗
+  WP e {{ Φ }} ={⊤,∅}▷=∗ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?.
-  { iApply (step_fupd_mask_mono ∅ _ _ ∅); eauto. set_solver. }
+  { iApply step_fupd_intro. set_solver. eauto. }
   iMod (fupd_plain_mask_empty _ ⌜reducible e σ⌝%I with "[H Hσ]") as %?.
-  { by iMod ("H" $! σ [] κs with "Hσ") as "($&H)". }
+  { by iMod ("H" $! σ [] κs with "Hσ") as "[$ H]". }
   iApply step_fupd_intro; first by set_solver+. 
   iIntros "!> !%". by right.
 Qed.
 
-Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
+Lemma wptp_safe κs' n e1 κs e2 t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) → e2 ∈ t2 →
-  state_interp σ1 (κs ++ κs') ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
-  ⊢ |={⊤,∅}▷=>^(S n) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  state_interp σ1 (κs ++ κs') (length t1) -∗ WP e1 {{ Φ }} -∗ wptp NotStuck t1
+  ={⊤,∅}▷=∗^(S n) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
-  intros ? He2. rewrite Nat_iter_S_r wptp_steps //.
-  apply step_fupdN_mono.
-  iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
-  apply elem_of_cons in He2 as [<-|?].
-  - iMod (wp_safe with "Hw H") as "$"; auto.
-  - iMod (wp_safe with "Hw [Htp]") as "$"; auto. by iApply (big_sepL_elem_of with "Htp").
+  iIntros (? He2) "Hσ He Ht". rewrite Nat_iter_S_r.
+  iDestruct (wptp_steps  with "Hσ He Ht") as "H"; first done.
+  iApply (step_fupdN_wand with "H").
+  iDestruct 1 as (e2' t2' ?) "(Hσ & H & Ht)"; simplify_eq.
+  apply elem_of_cons in He2 as [<-|(t1''&t2''&->)%elem_of_list_split].
+  - iMod (wp_safe with "Hσ H") as "$"; auto.
+  - iDestruct "Ht" as "(_ & He2 & _)". by iMod (wp_safe with "Hσ He2").
 Qed.
 
-Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
+Lemma wptp_invariance φ s n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗
-  state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
-  ⊢ |={⊤,∅}▷=>^(S n) |={⊤,∅}=> ⌜φ⌝.
+  (state_interp σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝) -∗
+  state_interp σ1 (κs ++ κs') (length t1) -∗
+  WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1
+  ={⊤,∅}▷=∗^(S n) ⌜φ⌝.
 Proof.
-  intros ?. rewrite Nat_iter_S_r wptp_steps // step_fupdN_frame_l.
-  apply step_fupdN_mono.
-  iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[Hσ _]".
-  iSpecialize ("Hback" with "Hσ"). by iApply step_fupd_intro.
+  iIntros (?) "Hφ Hσ He Ht". rewrite Nat_iter_S_r.
+  iDestruct (wptp_steps _ n with "Hσ He Ht") as "H"; first done.
+  iApply (step_fupdN_wand with "H"). iDestruct 1 as (e2' t2' ->) "[Hσ _]".
+  iSpecialize ("Hφ" with "Hσ").
+  iMod (fupd_plain_mask_empty _ ⌜φ⌝%I with "Hφ") as %?.
+  by iApply step_fupd_intro.
 Qed.
 End adequacy.
 
 Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
-     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
-       stateI σ κs ∗ WP e @ s; ⊤ {{ v, ∀ σ, stateI σ [] ={⊤,∅}=∗ ⌜φ v σ⌝ }})%I) →
+     (|={⊤}=> ∃
+         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (fork_post : iProp Σ),
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
+       (* This could be strengthened so that φ also talks about the number 
+       of forked-off threads *)
+       stateI σ κs 0 ∗ WP e @ s; ⊤ {{ v, ∀ σ m, stateI σ [] m ={⊤,∅}=∗ ⌜φ v σ⌝ }})%I) →
   adequate s e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
-    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
-    rewrite Nat_iter_S.
-    iMod Hwp as (Istate) "[HI Hwp]".
-    iApply (step_fupd_mask_mono ∅ _ _ ∅); auto. iModIntro. iNext; iModIntro.
-    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); eauto with iFrame.
+    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
+    iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
+    iApply step_fupd_intro; first done. iModIntro.
+    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto.
+    iApply (wp_wand with "Hwp"). iIntros (v) "H"; iIntros (σ'). iApply "H".
   - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
-    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
-    rewrite Nat_iter_S.
-    iMod Hwp as (Istate) "[HI Hwp]".
-    iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
-    iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); [by eauto..|].
-    rewrite app_nil_r. eauto with iFrame.
+    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
+    iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
+    iApply step_fupd_intro; first done. iModIntro.
+    iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
 Qed.
 
 Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv (λ σ κs _, stateI σ κs) True%I in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
-  iMod Hwp as (stateI) "[Hσ H]". iExists stateI. iIntros "{$Hσ} !>".
+  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), True%I.
+  iIntros "{$Hσ} !>".
   iApply (wp_wand with "H"). iIntros (v ? σ') "_".
-  iMod (fupd_intro_mask' ⊤ ∅) as "_"; auto.
+  iIntros "_". by iApply fupd_mask_weaken.
+Qed.
+
+Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
+  (∀ `{Hinv : invG Σ} κs,
+     (|={⊤}=> ∃
+         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (fork_post : iProp Σ),
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
+       stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
+         let m := length vs in
+         stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
+  rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
+  φ v.
+Proof.
+  intros Hwp [n [κs ?]]%erased_steps_nsteps.
+  eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
+  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
+  iApply step_fupd_intro; first done. iModIntro.
+  iApply (@wptp_all_result _ _ (IrisG _ _ _ Hinv stateI fork_post)
+    with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
 Qed.
 
 Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
-     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
-       stateI σ1 (κs ++ κs') ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' ={⊤,∅}=∗ ⌜φ⌝))%I) →
+     (|={⊤}=> ∃
+         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (fork_post : iProp Σ),
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
+       stateI σ1 (κs ++ κs') 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
+       (stateI σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
-  eapply (step_fupdN_soundness _ (S (S n)))=> Hinv.
-  rewrite Nat_iter_S.
-  iMod (Hwp Hinv κs []) as (Istate) "(HIstate & Hwp & Hclose)".
+  apply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
+  iMod (Hwp Hinv κs []) as (Istate fork_post) "(Hσ & Hwp & Hclose)".
   iApply step_fupd_intro; first done.
-  iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
+  iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate fork_post)
+    with "Hclose [Hσ] [Hwp]"); eauto.
 Qed.
 
 (* An equivalent version that does not require finding [fupd_intro_mask'], but
 can be confusing to use. *)
 Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
-     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
-       stateI σ1 κs ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
+     (|={⊤}=> ∃
+         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (fork_post : iProp Σ),
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
+       stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
+       (stateI σ2 κs' (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
   intros Hwp. eapply wp_invariance; first done.
-  intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
-  iModIntro. iExists stateI. iFrame. iIntros "Hσ".
+  intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI fork_post) "(? & ? & Hφ)".
+  iModIntro. iExists stateI, fork_post. iFrame. iIntros "Hσ".
   iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
-  iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
+  by iApply fupd_mask_weaken; first set_solver.
 Qed.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 080d39947..d878c0a8e 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,48 +16,53 @@ Hint Resolve head_stuck_stuck.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      WP e2 @ s; E {{ Φ }} ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs Hstep).
+  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      WP e2 @ s; E {{ Φ }} ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (???) "?".
+  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
   to_val e = None →
   sub_redexes_are_values e →
-  (∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜head_stuck e σ⌝)
+  (∀ σ κs n, state_interp σ κs n ={E,∅}=∗ ⌜head_stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros (??) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ κs) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
+  iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
 Qed.
 
 Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
+  state_interp_fork_indep →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
   (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
-  iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
+  iIntros (???) "H". iApply wp_lift_pure_step; [done| |by eauto|].
   { by destruct s; auto. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   iIntros (?????). iApply "H"; eauto.
@@ -70,74 +75,77 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   WP e @ E ?{{ Φ }}%I.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ κs) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
   by auto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
-  iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_atomic__head_step_no_fork_fupd {s E1 E2 Φ} e1 :
+Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
-  iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iIntros (v2 σ2 efs Hstep).
   iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
-  iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
+  iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
-  iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs Hstep).
-  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
+  iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
+  state_interp_fork_indep →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
@@ -148,10 +156,10 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+  intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
   destruct s; by auto.
 Qed.
 
@@ -159,7 +167,7 @@ Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧  σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧  σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
   ▷ 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 //.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 5533cb1d8..2c885e962 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,23 +15,25 @@ Hint Resolve reducible_no_obs_reducible.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      WP e2 @ s; E {{ Φ }} ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs) "Hσ".
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
   iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
   iIntros (????). iApply "H". eauto.
 Qed.
 
 Lemma wp_lift_stuck E Φ e :
   to_val e = None →
-  (∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜stuck e σ⌝)
+  (∀ σ κs n, state_interp σ κs n ={E,∅}=∗ ⌜stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs) "Hσ".
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
   iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
   iIntros (e2 σ2 efs ?). by case: (Hirr κ e2 σ2 efs).
 Qed.
@@ -39,32 +41,53 @@ Qed.
 (** Derived lifting lemmas. *)
 Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      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".
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (????) "Hσ".
+  iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
+  state_interp_fork_indep →
   (∀ σ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 → κ = [] ∧ σ1 = σ2) →
   (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
+  iIntros (Hfork Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-  iIntros (σ1 κ κs) "Hσ". iMod "H".
+  iIntros (σ1 κ κs n) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
   { iPureIntro. destruct s; done. }
   iNext. iIntros (e2 σ2 efs Hstep').
   destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
-  iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
+  iMod "Hclose" as "_". iMod "H". iModIntro.
+  rewrite (Hfork _ _ _ n). iFrame "Hσ". iApply "H"; auto.
+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 → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
+  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
+  { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
+  iIntros (σ1 κ κs n) "Hσ". iMod "H".
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  { iPureIntro. destruct s; done. }
+  iNext. iIntros (e2 σ2 efs ?).
+  destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
+  iMod "Hclose" as "_". iMod "H". iModIntro.
+  iDestruct ("H" with "[//]") as "H". simpl. iFrame.
 Qed.
 
 Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
@@ -74,59 +97,75 @@ Proof.
   iIntros (Hstuck) "_". iApply wp_lift_stuck.
   - destruct(to_val e) as [v|] eqn:He; last done.
     rewrite -He. by case: (Hstuck inhabitant).
-  - iIntros (σ κs) "_". iMod (fupd_intro_mask' E ∅) as "_".
-    by set_solver. by auto.
+  - iIntros (σ κs n) "_". by iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs) "Hσ1".
+  iIntros (?) "H".
+  iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
   iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
-  iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
+  iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply wp_value; last done. by apply of_to_val.
 Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
+  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (???) "?". iMod ("H" with "[$]") as "[$ H]".
+  iIntros (????) "?". iMod ("H" with "[$]") as "[$ H]".
   iIntros "!> *". iIntros (Hstep) "!> !>".
   by iApply "H".
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
+  state_interp_fork_indep →
   (∀ σ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' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
+    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
+  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
   { by naive_solver. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
+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' →
+    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
+  (|={E,E'}▷=> 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. }
+  iApply (step_fupd_wand with "H"); iIntros "H".
+  iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
+Qed.
+
 Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
@@ -134,10 +173,10 @@ Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
-  iApply wp_lift_pure_det_step.
+  iApply wp_lift_pure_det_step_no_fork.
   - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
-  - destruct s; naive_solver.
-  - rewrite /= right_id. by iApply (step_fupd_wand with "Hwp").
+  - done.
+  - by iApply (step_fupd_wand with "Hwp").
 Qed.
 
 Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 4eacbbb5c..4f12f1e48 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -14,7 +14,8 @@ Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ).
 
 Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := {
   iris_invG := ownP_invG;
-  state_interp σ κs := (own ownP_name (● (Excl' (σ:leibnizC Λstate))))%I
+  state_interp σ κs _ := (own ownP_name (● (Excl' (σ:leibnizC Λstate))))%I;
+  fork_post := True%I;
 }.
 Global Opaque iris_invG.
 
@@ -64,14 +65,13 @@ Proof.
   iIntros (? κs κs').
   iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
     as (γσ) "[Hσ Hσf]"; first done.
-  iExists (λ σ κs',
-           own γσ (● (Excl' (σ:leibnizC _))))%I.
+  iExists (λ σ κs' _, own γσ (● (Excl' (σ:leibnizC _))))%I, True%I.
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
-  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
-  iDestruct (own_valid_2 with "Hσ Hσf") as %[Hp _]%auth_valid_discrete_2.
-  pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
+  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
+  iDestruct (own_valid_2 with "Hσ Hσf")
+    as %[Hp%Excl_included _]%auth_valid_discrete_2; simplify_eq; auto.
 Qed.
 
 
@@ -82,13 +82,11 @@ Section lifting.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Lemma ownP_eq σ1 σ2 κs : state_interp σ1 κs -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
+  Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯")
-      as %[Hps _]%auth_valid_discrete_2.
-    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
-    done.
+    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_valid_discrete_2.
+    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
@@ -108,7 +106,7 @@ Section lifting.
       iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
       destruct s; last done. apply reducible_not_val in Hred.
       move: Hred; by rewrite to_of_val.
-    - iApply wp_lift_step; [done|]; iIntros (σ1 κ κs) "Hσκs".
+    - iApply wp_lift_step; [done|]; iIntros (σ1 κ κs n) "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).
@@ -127,7 +125,7 @@ Section lifting.
     - apply of_to_val in EQe as <-. iApply fupd_wp.
       iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
       by rewrite to_of_val in Hnv.
-    - iApply wp_lift_stuck; [done|]. iIntros (σ1 κs) "Hσ".
+    - iApply wp_lift_stuck; [done|]. iIntros (σ1 κs n) "Hσ".
       iMod "H" as (σ1') "(% & >Hσf)".
       by iDestruct (ownP_eq with "Hσ Hσf") as %->.
   Qed.
@@ -142,7 +140,7 @@ Section lifting.
     iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-    iIntros (σ1 κ κs) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+    iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
     iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
@@ -206,7 +204,7 @@ Section lifting.
     (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) // ?big_sepL_nil ?right_id; eauto.
   Qed.
 End lifting.
 
@@ -297,7 +295,7 @@ Section ectx_lifting.
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
-    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
+    iIntros (??) "H"; iApply wp_lift_pure_det_step; try by eauto.
     by destruct s; eauto using reducible_not_val.
   Qed.
 
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 130f2983a..c62a5dfaa 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -11,16 +11,17 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 κ κs σ2, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
-    state_interp σ1 κs ={⊤}=∗ ⌜κ = []⌝ ∗ state_interp σ2 κs ∗ twptp t2)%I.
+  (∀ t2 σ1 κ κs σ2 n, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
+    state_interp σ1 κs n ={⊤}=∗ ∃ n', ⌜κ = []⌝ ∗ state_interp σ2 κs n' ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
   ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
-  iIntros (t2 σ1 κ κs σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ [$ ?]]".
-  by iApply "H".
+  iIntros (t2 σ1 κ κs σ2 n1) "Hstep Hσ".
+  iMod ("Hwp" with "[$] [$]") as (n2) "($ & Hσ & ?)".
+  iModIntro. iExists n2. iFrame "Hσ". by iApply "H".
 Qed.
 
 Local Instance twptp_pre_mono' : BiMonoPred twptp_pre.
@@ -49,9 +50,10 @@ Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
 Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
-  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 Hstep) "Hσ".
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
   destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
-  iMod ("IH" $! t2' with "[% //] Hσ") as "($ & $ & IH & _)". by iApply "IH".
+  iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
+  iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
 Qed.
 
 Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
@@ -60,22 +62,23 @@ Proof.
   iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
   iRevert (t1) "IH1"; iRevert (t2) "H2".
   iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
-  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 Hstep) "Hσ1".
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1".
   destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]; simplify_eq/=.
   apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
-    + iMod ("IH2" with "[%] Hσ1") as "($ & $ & IH2 & _)".
+    + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
       { by eapply step_atomic with (t1:=[]). }
-      iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
+      iModIntro. iExists n2. iFrame "Hσ".
+      rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
-    + iMod ("IH1" with "[%] Hσ1") as "($ & $ & IH1 & _)"; first by econstructor.
+    + iMod ("IH1" with "[%] Hσ1") as (n2) "($ & Hσ & IH1 & _)"; first by econstructor.
       iAssert (twptp t2) with "[IH2]" as "Ht2".
       { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
         iIntros "!# * [_ ?] //". }
-      iModIntro. rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L.
-      by iApply "IH1".
-  - iMod ("IH2" with "[%] Hσ1") as "($ & $ & IH2 & _)"; first by econstructor.
-    iModIntro. rewrite -assoc. by iApply "IH2".
+      iModIntro. iExists n2. iFrame "Hσ".
+      rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L. by iApply "IH1".
+  - iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)"; first by econstructor.
+    iModIntro. iExists n2. iFrame "Hσ". rewrite -assoc_L. by iApply "IH2".
 Qed.
 
 Lemma twp_twptp s Φ e : WP e @ s; ⊤ [{ Φ }] -∗ twptp [e].
@@ -83,42 +86,46 @@ Proof.
   iIntros "He". remember (⊤ : coPset) as E eqn:HE.
   iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
   iIntros "!#" (e E Φ); iIntros "IH" (->).
-  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ2' Hstep) "Hσ1".
+  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ2' n Hstep) "Hσ1".
   destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
     simplify_eq/=; try discriminate_list.
   destruct (to_val e1) as [v|] eqn:He1.
   { apply val_stuck in Hstep; naive_solver. }
   iMod ("IH" with "Hσ1") as "[_ IH]".
-  iMod ("IH" with "[% //]") as "($ & $ & [IH _] & IHfork)"; iModIntro.
+  iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
+  iModIntro. iExists (length efs + n). iFrame "Hσ".
   iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
   clear. iInduction efs as [|e efs] "IH"; simpl.
-  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 Hstep).
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n1 Hstep).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
-  iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
+  iApply (twptp_app [_] with "[IH']"). by iApply "IH'". by iApply "IH".
 Qed.
 
-Lemma twptp_total σ t :
-  state_interp σ [] -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
+Lemma twptp_total n σ t :
+  state_interp σ [] n -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
-  iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "Hσ".
+  iIntros "Hσ Ht". iRevert (σ n) "Hσ". iRevert (t) "Ht".
+  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ n) "Hσ".
   iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
-  iMod ("IH" with "[% //] Hσ") as (->) "[Hσ [H _]]".
+  rewrite /twptp_pre.
+  iMod ("IH" with "[% //] Hσ") as (n' ->) "[Hσ [H _]]".
   by iApply "H".
 Qed.
 End adequacy.
 
 Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
   (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) -> iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
-       stateI σ [] ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+     (|={⊤}=> ∃
+         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (fork_post : iProp Σ),
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
+       stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
   apply (fupd_plain_soundness ⊤ _)=> Hinv.
-  iMod (Hwp) as (stateI) "[Hσ H]".
-  iApply (@twptp_total _ _ (IrisG _ _ _ Hinv stateI) with "Hσ").
-  by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv stateI)).
+  iMod (Hwp) as (stateI fork_post) "[Hσ H]".
+  iApply (@twptp_total _ _ (IrisG _ _ _ Hinv stateI fork_post) with "Hσ").
+  by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv stateI fork_post)).
 Qed.
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 5e7748848..c26cc5acf 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -10,77 +10,95 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step head_reducible_no_obs_reducible.
+Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
+  head_reducible_no_obs_reducible.
 
 Lemma twp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κs n, state_interp σ1 κs n ={E,∅}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
-      WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+      ⌜κ = []⌝ ∗
+      state_interp σ2 κs (length efs + n) ∗
+      WP e2 @ s; E [{ Φ }] ∗
+      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1 κs) "Hσ".
+  iIntros (?) "H".
+  iApply (twp_lift_step _ E)=>//. iIntros (σ1 κs n) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
   iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
   iApply "H". by eauto.
 Qed.
 
 Lemma twp_lift_pure_head_step {s E Φ} e1 :
+  state_interp_fork_indep →
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
   (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh.
-  iIntros (??) ">H". iApply twp_lift_pure_step; eauto.
+  iIntros (???) ">H". iApply twp_lift_pure_step; eauto.
+  iIntros "!>" (?????). iApply "H"; eauto.
+Qed.
+
+Lemma twp_lift_pure_head_step_no_fork {s E Φ} e1 :
+  (∀ σ1, head_reducible_no_obs e1 σ1) →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
+  (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }] )
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof using Hinh.
+  iIntros (??) ">H". iApply twp_lift_pure_step_no_fork; eauto.
   iIntros "!>" (?????). iApply "H"; eauto.
 Qed.
 
 Lemma twp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+      ⌜κ = []⌝ ∗
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
-  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 κs n) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
 Qed.
 
 Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
+      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
-  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 κs n) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iIntros (κ v2 σ2 efs Hstep).
-  iMod ("H" with "[# //]") as "($ & % & $ & $)"; subst; auto.
+  iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
 Qed.
 
 Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
+  state_interp_fork_indep →
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
-Proof using Hinh. eauto 10 using twp_lift_pure_det_step. Qed.
+Proof using Hinh. eauto 20 using twp_lift_pure_det_step. Qed.
 
 Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh.
-  intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+  intros. rewrite -(twp_lift_pure_det_step_no_fork e1 e2); eauto.
 Qed.
 End wp.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index 4b1335d93..12ec53f16 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -11,46 +11,71 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
+Hint Resolve reducible_no_obs_reducible.
+
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κs n, state_interp σ1 κs n ={E,∅}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+      ⌜κ = []⌝ ∗
+      state_interp σ2 κs (length efs + n) ∗
+      WP e2 @ s; E [{ Φ }] ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
-(** Derived lifting lemmas. *)
 
+(** Derived lifting lemmas. *)
 Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
+  state_interp_fork_indep →
   (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
   (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
+  iIntros (Hfork Hsafe Hstep) "H". iApply twp_lift_step.
   { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
-  iIntros (σ1 κs) "Hσ". iMod "H".
+  iIntros (σ1 κs n) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
   iSplit; [by destruct s|]. iIntros (κ e2 σ2 efs Hstep').
   destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
-  iMod "Hclose" as "_". iModIntro. iSplit; first done.
+  iMod "Hclose" as "_". iModIntro. iSplit; first done. rewrite (Hfork _ _ _ n).
   iFrame "Hσ". iApply "H"; auto.
 Qed.
 
+Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
+  (∀ σ1, reducible_no_obs e1 σ1) →
+  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
+  (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
+  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
+  iIntros (σ1 κs n) "Hσ".
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  { iPureIntro. destruct s; auto. }
+  iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
+  iMod "Hclose" as "_". iModIntro.
+  iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
+Qed.
+
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
 Lemma twp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κs n, state_interp σ1 κs n ={E}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
-      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+      ⌜κ = []⌝ ∗
+      state_interp σ2 κs (length efs + n) ∗
+      from_option Φ False (to_val e2) ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs) "Hσ1".
+  iIntros (?) "H".
+  iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
@@ -60,16 +85,29 @@ Proof.
 Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
+  state_interp_fork_indep →
   (∀ σ1, reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
+    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
+  iIntros (?? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
   { by naive_solver. }
   by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
+Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+  (∀ σ1, reducible_no_obs e1 σ1) →
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
+    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
+  (|={E}=> WP e2 @ s; E [{ Φ }]) ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step_no_fork s E); try done.
+  { naive_solver. }
+  iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
+Qed.
+
 Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
@@ -77,8 +115,7 @@ Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
-  iApply twp_lift_pure_det_step; [done|naive_solver|].
-  iModIntro. rewrite /= right_id. by iApply "IH".
+  iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
+  iModIntro. by iApply "IH".
 Qed.
-
 End lifting.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index aa53b6716..6892cc1fc 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -9,11 +9,14 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 κs,
-     state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
-     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-       ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
-       wp E e2 Φ ∗ [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+  | None => ∀ σ1 κs n,
+     state_interp σ1 κs n ={E,∅}=∗
+       ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
+       ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
+         ⌜κ = []⌝ ∗
+         state_interp σ2 κs (length efs + n) ∗
+         wp E e2 Φ ∗
+         [∗ list] ef ∈ efs, wp ⊤ ef (λ _, fork_post)
   end%I.
 
 Lemma twp_pre_mono `{irisG Λ Σ} s
@@ -23,12 +26,12 @@ Lemma twp_pre_mono `{irisG Λ Σ} s
 Proof.
   iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
   destruct (to_val e1) as [v|]; first done.
-  iIntros (σ1 κs) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
+  iIntros (σ1 κs n) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
   iIntros (κ e2 σ2 efs) "Hstep".
-  iMod ("Hwp" with "Hstep") as "($ & $ & Hwp & Hfork)"; iModIntro.
-  iSplitL "Hwp".
+  iMod ("Hwp" with "Hstep") as (?) "(Hσ & Hwp & Hfork)".
+  iModIntro. iFrame "Hσ". iSplit; first done. iSplitL "Hwp".
   - by iApply "H".
-  - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
+  - iApply (@big_sepL_impl with "Hfork"); iIntros "!#" (k e _) "Hwp".
     by iApply "H".
 Qed.
 
@@ -45,7 +48,7 @@ Proof.
     iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply pair_ne.
+    rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
 Qed.
 
 Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
@@ -106,21 +109,22 @@ Proof.
   iIntros "!#" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+  iIntros (σ1 κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("IH" with "[$]") as "[% IH]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
-  iMod ("IH" with "[//]") as "($ & $ & IH & IHefs)"; auto.
-  iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
+  iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
+  iMod "Hclose" as "_"; iModIntro.
+  iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
-  - iApply (big_sepL_impl with "[$IHefs]"); iIntros "!#" (k ef _) "[IH _]".
-    by iApply "IH".
+  - iApply (big_sepL_impl with "IHefs"); iIntros "!#" (k ef _) "[IH _]".
+    iApply "IH"; auto.
 Qed.
 
 Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) -∗ WP e @ s; E [{ Φ }].
 Proof.
   rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κs) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 κs n) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] -∗ WP e @ s; E [{ Φ }].
 Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
@@ -131,16 +135,16 @@ Proof.
   iIntros "H". rewrite !twp_unfold /twp_pre /=.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iIntros (σ1 κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iIntros (κ e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "(% & Hphy & H & $)". destruct s.
+  iMod ("H" with "[//]") as (?) "(Hσ & H & Hefs)". destruct s.
   - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (twp_value_inv' with "H") as ">H". iModIntro. iSplit; first done.
-    iFrame "Hphy". by iApply twp_value'.
+    iMod (twp_value_inv' with "H") as ">H".
+    iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
 Qed.
 
 Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
@@ -154,13 +158,13 @@ Proof.
   rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
   rewrite twp_unfold /twp_pre fill_not_val //.
-  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { iPureIntro. unfold reducible_no_obs in *.
     destruct s; naive_solver eauto using fill_step. }
   iIntros (κ e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("IH" $! κ e2' σ2 efs with "[//]") as "($ & $ & IH & IHfork)".
-  iModIntro; iSplitR "IHfork".
+  iMod ("IH" $! κ e2' σ2 efs with "[//]") as (?) "(Hσ & IH & IHefs)".
+  iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
 Qed.
@@ -175,11 +179,11 @@ Proof.
   { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
     iApply (twp_pre_mono with "[] IH"). by iIntros "!#" (E e Φ') "[_ ?]". }
   rewrite /twp_pre fill_not_val //.
-  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { destruct s; eauto using reducible_no_obs_fill. }
   iIntros (κ e2 σ2 efs Hstep).
-  iMod ("IH" $! κ (K e2) σ2 efs with "[]") as "($ & $ & IH & IHfork)"; eauto using fill_step.
-  iModIntro; iSplitR "IHfork".
+  iMod ("IH" $! κ (K e2) σ2 efs with "[]") as (?) "(Hσ & IH & IHefs)"; eauto using fill_step.
+  iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
 Qed.
@@ -188,12 +192,13 @@ Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ).
   rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
-  iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
+  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
   { destruct s; last done. eauto using reducible_no_obs_reducible. }
-  iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(-> & $ & H & Hfork)".
+  iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
-  iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
-  iIntros "!#" (k e' _) "H". by iApply "IH".
+  iFrame "Hσ". iSplitL "H". by iApply "IH".
+  iApply (@big_sepL_impl with "Hfork").
+  iIntros "!#" (k ef _) "H". by iApply "IH".
 Qed.
 
 (** * Derived rules *)
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index bcaa16f44..c2437fb8a 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -7,21 +7,27 @@ Import uPred.
 
 Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
-  state_interp : Λstate → list Λobservation → iProp Σ;
+  state_interp : Λstate → list Λobservation → nat → iProp Σ;
+  fork_post : iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ).
 Global Opaque iris_invG.
 
+Definition state_interp_fork_indep `{irisG Λ Σ} :=
+  ∀ σ κs n n', state_interp σ κs n = state_interp σ κs n'.
+
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 κ κs,
-      state_interp σ1 (κ ++ κs) ={E,∅}=∗
-        ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-        ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-          state_interp σ2 κs ∗ wp E e2 Φ ∗ [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+  | None => ∀ σ1 κ κs n,
+     state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+       ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+         state_interp σ2 κs (length efs + n) ∗
+         wp E e2 Φ ∗
+         [∗ list] i ↦ ef ∈ efs, wp ⊤ ef (λ _, fork_post)
   end%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
@@ -57,7 +63,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 22 (f_contractive || f_equiv). apply IH; first lia.
+  do 24 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with lia.
 Qed.
 Global Instance wp_proper s E e :
@@ -79,21 +85,22 @@ Proof.
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κ κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+  iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
-  iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
+  iMod ("H" with "[//]") as "H". iIntros "!> !>".
+  iMod "H" as "(Hσ & H & Hefs)".
+  iMod "Hclose" as "_". iModIntro. iFrame "Hσ". iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
-  - iApply (big_sepL_impl with "[$Hefs]"); iIntros "!#" (k ef _) "H".
-    by iApply ("IH" with "[] H").
+  - iApply (big_sepL_impl with "Hefs"); iIntros "!#" (k ef _).
+    iIntros "H". iApply ("IH" with "[] H"); auto.
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κ κs) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 κ κs n) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
@@ -104,15 +111,17 @@ Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κ κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iIntros (σ1 κ κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "H". iIntros "!>!>". iMod "H" as "(Hphy & H & $)". destruct s.
+  iMod ("H" with "[//]") as "H". iIntros "!>!>".
+  iMod "H" as "(Hσ & H & Hefs)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
     + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
+    iMod (wp_value_inv' with "H") as ">H".
+    iModIntro. iFrame "Hσ Hefs". by iApply wp_value'.
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
@@ -120,10 +129,11 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
   (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1 κ κs) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
+  iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
-  iIntros "!>!>". iMod "H" as "($ & H & $)".
-  iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
+  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
+  iMod "HR". iModIntro. iFrame "Hσ Hefs".
+  iApply (wp_strong_mono s s E2 with "H"); [done..|].
   iIntros (v) "H". by iApply "H".
 Qed.
 
@@ -134,13 +144,14 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1 κ κs) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { iPureIntro. destruct s; last done.
     unfold reducible in *. naive_solver eauto using fill_step. }
   iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
-  iMod "H" as "($ & H & $)". by iApply "IH".
+  iMod "H" as "(Hσ & H & Hefs)".
+  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
 Qed.
 
 Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
@@ -150,11 +161,12 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
-  iIntros (σ1 κ κs) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
   iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
-  iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
+  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
+  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
 Qed.
 
 (** * Derived rules *)
-- 
GitLab