Merge branch 'step_indexing_controlled_by_ghosts' into 'master'

Flexible number of logical steps per physical step

See merge request iris/iris!595

CHANGELOG.md

@@ -31,6 +31,28 @@ s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
 EOF
 ```
 
+**Changes in `base_logic`:**
+
+* Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
+  It applies even if invariants stay open accross an arbitrary number of laters.
+
+**Changes in `program_logic`:**
+
+* Change definition of weakest precondition to use a variable number of laters
+  (i.e., logical steps) for each physical step of the operational semantics,
+  depending on the number of physical steps executed since the begining of the
+  execution of the program. See merge request [!595](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595).
+
+  This implies several API-breaking changes, which can be easily fixed in client
+  formalizations in a backward compatible manner as follows:
+   - Ignore the new parameter `ns` in the state interpretation, which
+     corresponds to a step counter.
+   - Use the constant function "0" for the new field `num_laters_per_step` of
+     `irisG`.
+   - Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
+   - Some proofs using lifting lemmas and adequacy theorems need to be adapted
+     to ignore the new step counter.
+
 ## Iris 3.4.0
 
 The highlights and most notable changes of this release are as follows:

iris/base_logic/lib/fancy_updates.v

@@ -71,28 +71,26 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
-  destruct n as [|n].
-  - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
-  - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
-    { by iApply fupd_plain_mask_empty. }
-    rewrite -step_fupdN_S_fupd.
-    iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
-    rewrite -later_laterN laterN_later.
-    iNext. by iMod "Hφ".
+  iApply fupd_plainly_mask_empty. iMod "H".
+  iMod (step_fupdN_plain with "H") as "H". iModIntro.
+  rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
+  iNext. iMod "H" as %Hφ. auto.
 Qed.
 
 Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
   (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness _ n).
-  iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_intro_discard.
+  iIntros (Hiter). eapply (step_fupdN_soundness _ n)=>Hinv. destruct n as [|n].
+  { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
+   simpl in Hiter |- *. iMod Hiter as "H". iIntros "!>!>!>".
+  iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
+  simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.

iris/bi/updates.v

@@ -370,6 +370,16 @@ Section fupd_derived.
     rewrite {4}(union_difference_L _ _ HE). done.
   Qed.
 
+  Lemma fupd_mask_subseteq_emptyset_difference E1 E2 :
+    E2 ⊆ E1 →
+    ⊢@{PROP} |={E1, E2}=> |={∅, E1∖E2}=> emp.
+  Proof.
+    intros ?. rewrite [in fupd E1](union_difference_L E2 E1); [|done].
+    rewrite (comm_L (∪))
+      -[X in fupd _ X](left_id_L ∅ (∪) E2) -fupd_mask_frame_r; [|set_solver+].
+    apply fupd_mask_intro_subseteq; set_solver.
+  Qed.
+
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
 
@@ -460,6 +470,12 @@ Section fupd_derived.
     by apply sep_mono; first apply later_intro.
   Qed.
 
+  Lemma step_fupdN_intro Ei Eo n P : Ei ⊆ Eo → ▷^n P -∗ |={Eo}[Ei]▷=>^n P.
+  Proof.
+    induction n as [|n IH]=> ?; [done|].
+    rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
+  Qed.
+
   Lemma step_fupdN_S_fupd n E P :
     (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.

iris/program_logic/adequacy.v

@@ -7,6 +7,7 @@ Import uPred.
 
 (** This file contains the adequacy statements of the Iris program logic. First
 we prove a number of auxilary results. *)
+
 Section adequacy.
 Context `{!irisG Λ Σ}.
 Implicit Types e : expr Λ.
@@ -16,84 +17,96 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 
 Notation wptp s t Φs := ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
 
-Lemma wp_step s e1 σ1 κ κs e2 σ2 efs nt Φ :
+Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
-    state_interp σ2 κs (nt + length efs) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗
+  state_interp σ1 ns (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }}
+    ={⊤,∅}=∗ |={∅}▷=>^(S $ num_laters_per_step ns) |={∅,⊤}=>
+    state_interp σ2 (S ns) κs (nt + length efs) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗
     wptp s efs (replicate (length efs) fork_post).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
-  iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
-  iMod ("H" $! e2 σ2 efs with "[//]") as "H".
+  iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
+  iApply (step_fupdN_wand with "[H]"); first by iApply "H". iIntros ">H".
   by rewrite Nat.add_comm big_sepL2_replicate_r.
 Qed.
 
-Lemma wptp_step s es1 es2 κ κs σ1 σ2 Φs nt :
+Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
   step (es1,σ1) κ (es2, σ2) →
-  state_interp σ1 (κ ++ κs) nt -∗ wptp s es1 Φs -∗
-  ∃ nt', |={⊤}[∅]▷=> state_interp σ2 κs (nt + nt') ∗
+  state_interp σ1 ns (κ ++ κs) nt -∗ wptp s es1 Φs -∗
+  ∃ nt', |={⊤,∅}=> |={∅}▷=>^(S $ num_laters_per_step$ ns) |={∅,⊤}=>
+         state_interp σ2 (S ns) κs (nt + nt') ∗
          wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
   iIntros (Hstep) "Hσ Ht".
   destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
   iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
   iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
-  iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done.
-  iIntros "!> !>". iMod "H" as "($ & He2 & Hefs)". iIntros "!>".
+  iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done. iModIntro.
+  iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
   rewrite -(assoc_L app) -app_comm_cons. iFrame.
 Qed.
 
-Lemma wptp_steps s n es1 es2 κs κs' σ1 σ2 Φs nt :
+(* The total number of laters used between the physical steps number
+   [start] (included) to [start+ns] (excluded). *)
+Local Fixpoint steps_sum (num_laters_per_step : nat → nat) (start ns : nat) : nat :=
+  match ns with
+  | O => 0
+  | S ns =>
+    S $ num_laters_per_step start + steps_sum num_laters_per_step (S start) ns
+  end.
+
+Lemma wptp_steps s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
   nsteps n (es1, σ1) κs (es2, σ2) →
-  state_interp σ1 (κs ++ κs') nt -∗ wptp s es1 Φs
-  ={⊤}[∅]▷=∗^n ∃ nt',
-    state_interp σ2 κs' (nt + nt') ∗ wptp s es2 (Φs ++ replicate nt' fork_post).
+  state_interp σ1 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
+    state_interp σ2 (n + ns) κs' (nt + nt') ∗
+    wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
-  revert nt es1 es2 κs κs' σ1 σ2 Φs.
-  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 σ2 Φs /=.
+  revert nt es1 es2 κs κs' σ1 ns σ2 Φs.
+  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
   { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
-    rewrite Nat.add_0_r right_id_L. by iFrame. }
+    rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
   iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite -(assoc_L (++)).
+  rewrite -(assoc_L (++)) Nat_iter_add plus_n_Sm.
   iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
-  iIntros "!> !>". iMod "H" as "(Hσ & He)". iModIntro.
-  iApply (step_fupdN_wand with "[Hσ He]"); first by iApply (IH with "Hσ He").
-  iDestruct 1 as (nt'') "[??]". rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus.
-  by eauto with iFrame.
+  iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
+  iIntros ">(Hσ & He)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
+  iApply (step_fupdN_wand with "IH"). iIntros ">IH".
+  iDestruct "IH" as (nt'') "[??]".
+  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
 Qed.
 
-Lemma wp_not_stuck κs nt e σ Φ :
-  state_interp σ κs nt -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
+Lemma wp_not_stuck κs nt e σ ns Φ :
+  state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?; first by eauto.
-  iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
+  iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
   iMod (fupd_plain_mask with "H") as %?; eauto.
 Qed.
 
-Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 σ2 nt:
+Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 ns σ2 nt:
   nsteps n (es1, σ1) κs (es2, σ2) →
-  state_interp σ1 (κs ++ κs') nt -∗
-  wptp s es1 Φs ={⊤}[∅]▷=∗^(S n) ∃ nt',
+  state_interp σ1 ns (κs ++ κs') nt -∗ wptp s es1 Φs
+  ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝ ∗
-    state_interp σ2 κs' (nt + nt') ∗
+    state_interp σ2 (n + ns) κs' (nt + nt') ∗
     [∗ list] e;Φ ∈ es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
 Proof.
-  iIntros (Hstep) "Hσ He". rewrite Nat_iter_S_r.
-  iDestruct (wptp_steps with "Hσ He") as "Hwp"; first done.
-  iApply (step_fupdN_wand with "Hwp").
-  iDestruct 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
+  iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
+  iModIntro. iApply (step_fupdN_wand with "Hwp").
+  iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
   iMod (fupd_plain_keep_l ⊤
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
-    (state_interp σ2 κs' (nt + nt') ∗ wptp s es2 (Φs ++ replicate nt' fork_post))%I
+    (state_interp σ2 (n + ns) κs' (nt + nt') ∗
+     wptp s es2 (Φs ++ replicate nt' fork_post))%I
     with "[$Hσ $Ht]") as "(%&Hσ&Hwp)".
   { iIntros "(Hσ & Ht)" (e' -> He').
     move: He' => /(elem_of_list_split _ _)[?[?->]].
     iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ?) "[? Hwp]".
     iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
     iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
-  iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
   iExists _. iSplitR; first done. iFrame "Hσ".
   iApply big_sepL2_fupd.
   iApply (big_sepL2_impl with "Hwp").
@@ -104,15 +117,19 @@ Qed.
 End adequacy.
 
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
+        (num_laters_per_step : nat → nat) :
   (∀ `{Hinv : !invG Σ},
     ⊢ |={⊤}=> ∃
          (s: stuckness)
-         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
+         (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
-         (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
-       stateI σ1 κs 0 ∗
+         (fork_post : val Λ → iProp Σ)
+         state_interp_mono,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
+                                  state_interp_mono
+       in
+       stateI σ1 0 κs 0 ∗
        ([∗ list] e;Φ ∈ es;Φs, WP e @ s; ⊤ {{ Φ }}) ∗
        (∀ es' t2',
          (* es' is the final state of the initial threads, t2' the rest *)
@@ -123,7 +140,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
          threads in [t2] are not stuck *)
          ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2 ⌝ -∗
          (* The state interpretation holds for [σ2] *)
-         stateI σ2 [] (length t2') -∗
+         stateI σ2 n [] (length t2') -∗
          (* If the initial threads are done, their post-condition [Φ] holds *)
          ([∗ list] e;Φ ∈ es';Φs, from_option Φ True (to_val e)) -∗
          (* For all forked-off threads that are done, their postcondition
@@ -138,19 +155,22 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
   φ.
 Proof.
   intros Hwp ?.
-  eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
-  iMod Hwp as (s stateI Φ fork_post) "(Hσ & Hwp & Hφ)".
+  apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n))=> Hinv.
+  iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
-  iApply step_fupd_intro; [done|]; iModIntro.
-  iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "[-Hφ]").
-  { iApply (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI fork_post) _ []
-    with "[Hσ] Hwp"); eauto; by rewrite right_id_L. }
-  iDestruct 1 as (nt' ?) "(Hσ & Hval) /=".
+  iMod (@wptp_strong_adequacy _ _
+       (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
+    with "[Hσ] Hwp") as "H"; [done|by rewrite right_id_L|].
+  iAssert (|={∅}▷=>^(steps_sum num_laters_per_step 0 n) |={∅}=> ⌜φ⌝)%I
+    with "[-]" as "H"; last first.
+  { destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
+  iApply (step_fupdN_wand with "H").
+  iMod 1 as (nt' ?) "(Hσ & Hval) /=".
   iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
   iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
   rewrite replicate_length in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
-  iApply fupd_plain_mask_empty.
+  rewrite -plus_n_O.
   iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
   by rewrite big_sepL2_replicate_r // big_sepL_omap.
 Qed.
@@ -199,14 +219,17 @@ Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) fork_post in
+       let _ : irisG Λ Σ :=
+           IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
+                 (λ _ _ _ _, fupd_intro _ _)
+       in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
   eapply (wp_strong_adequacy Σ _); [|done]=> ?.
   iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
-  iExists s, (λ σ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post => /=.
+  iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
   iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
@@ -219,7 +242,8 @@ Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
+       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
+              (λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
        stateI σ1 κs 0 ∗ WP e1 @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝)) →
   rtc erased_step ([e1], σ1) (t2, σ2) →
@@ -228,7 +252,7 @@ Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
   eapply (wp_strong_adequacy Σ _); [|done]=> ?.
   iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
-  iExists s, stateI, [(λ _, True)%I], fork_post => /=.
+  iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
   iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
   iDestruct (big_sepL2_nil_inv_r with "H") as %->.

iris/program_logic/ectx_lifting.v

@@ -17,15 +17,15 @@ Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 ns κ κs nt) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
   iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
   iApply "H"; eauto.
@@ -33,26 +33,26 @@ Qed.
 
 Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
+  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?????) "?".
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
   to_val e = None →
   sub_redexes_are_values e →
-  (∀ σ κs n, state_interp σ κs n ={E,∅}=∗ ⌜head_stuck e σ⌝)
+  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜head_stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros (??) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
+  iIntros (σ ns κs nt) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
 Qed.
 
 Lemma wp_lift_pure_head_stuck E Φ e :
@@ -62,51 +62,51 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   ⊢ WP e @ E ?{{ Φ }}.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ κs n) "_". iApply fupd_mask_intro; by auto with set_solver.
+  iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; by auto with set_solver.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iIntros (v2 σ2 efs Hstep).
   iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
   iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
@@ -114,14 +114,14 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
+      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
-  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs Hstep).
   iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
 Qed.

iris/program_logic/lifting.v

@@ -16,23 +16,38 @@ Implicit Types Φ : val Λ → iProp Σ.
 
 Local Hint Resolve reducible_no_obs_reducible : core.
 
+Lemma wp_lift_step_fupdN s E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝
+      ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
+      WP e2 @ s; E {{ Φ }} ∗
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
+
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
-      state_interp σ2 κs (length efs + n) ∗
+      state_interp σ2 (S ns) κs (length efs + nt) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
-Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
+Proof.
+  intros ?. rewrite -wp_lift_step_fupdN; [|done]. simpl. do 22 f_equiv.
+  rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro. auto.
+Qed.