From 996ec29782cafb88fb98d81742b8379e7bbeb9af Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 29 Jul 2020 10:44:59 +0200
Subject: [PATCH] make adequacy apply to multiple initial threads

---
 CHANGELOG.md                      |   6 ++
 tex/program-logic.tex             |  27 ++---
 theories/program_logic/adequacy.v | 173 +++++++++++++++---------------
 3 files changed, 109 insertions(+), 97 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b8c78888..ae60bff11 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,12 @@ With this release, we dropped support for Coq 8.9.
   `auth_alloc`.
 * Change `uPred_mono` to only require inclusion at the smaller step-index.
 
+**Changes in `program_logic`:**
+
+* `wp_strong_adequacy` now applies to an initial state with multiple
+  threads instead of only a single thread. The derived adequacy lemmas
+  are unchanged.
+
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index f6ddeebd3..2983ceb39 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -214,17 +214,18 @@ The purpose of the adequacy statement is to show that our notion of weakest prec
 The most general form of the adequacy statement is about proving properties of an arbitrary program execution.
 
 \begin{thm}[Adequacy]
-  Assume we are given some $\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
+  Assume we are given some $\vec\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $(\vec\expr_1, \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
   To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
 \begin{align*}
- &\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; \pred(x)} * \left(\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
+ &\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \vec\pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \left(\Sep_{\expr,\pred \in \vec\expr_1,\vec\pred} \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\top]{x.\; \pred(x)}\right) * \left(\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
 \end{align*}
 where $\consstate$ describes states that are consistent with the state interpretation and postconditions:
 \begin{align*}
- \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \eqdef{}&\Exists \expr_2, \tpool_2'. \tpool_2 = [\expr_2] \dplus \tpool_2' * {}\\
+ \consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \eqdef{}&\Exists \vec\expr_2, \tpool_2'. \tpool_2 = \vec\expr_2 \dplus \tpool_2' * {}\\
+ &\quad |\vec\expr_1| = |\vec\expr_2| *{}\\
  &\quad (s = \NotStuck \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2) ) *{}\\
  &\quad \stateinterp(\state_2, (), |\tpool_2'|) *{}\\
- &\quad (\toval(\expr_2) \ne \bot \wand \pred(\toval(\expr_2))) *{}\\
+ &\quad \left(\Sep_{\expr,\pred \in \vec\expr_2,\vec\pred} \toval(\expr) \ne \bot \wand \pred(\toval(\expr))\right) *{}\\
  &\quad \left(\Sep_{\expr \in \tpool_2'} \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
 \end{align*}
 The $\hat\metaprop$ here arises because we need a way to talk about $\metaprop$ inside Iris.
@@ -238,7 +239,7 @@ Furthermore, we assume that the \emph{interpretation} $\Sem{\hat{\metaprop}}$ of
 The signature can of course state arbitrary additional properties of $\hat{\metaprop}$, as long as they are proven sound.
 \end{thm}
 
-In other words, to show that $\metaprop$ holds, we have to prove an entailment in Iris that, starting from the empty context, chooses some state interpretation, postcondition, forked-thread postcondition and stuckness and then proves:
+In other words, to show that $\metaprop$ holds, we have to prove an entailment in Iris that, starting from the empty context, chooses some state interpretation, postconditions for the initial threads, forked-thread postcondition and stuckness and then proves:
 \begin{itemize}
   \item the initial state interpretation,
   \item a weakest-precondition,
@@ -247,12 +248,12 @@ In other words, to show that $\metaprop$ holds, we have to prove an entailment i
 Notice that the state interpretation and the postconditions are chosen \emph{after} doing a fancy update, which allows them to depend on the names of ghost variables that are picked in that initial fancy update.
 This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to.
 
-$\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
+$\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
 \begin{itemize}
-\item The final thread-pool $\tpool_2$ contains the final state of the main thread $\expr_2$, and any number of additional forked threads in $\tpool_2'$.
+\item The final thread-pool $\tpool_2$ contains the final state of the initial threads $\vec\expr_2$, and any number of additional forked threads in $\tpool_2'$.
 \item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_2$.
 \item The state interpretation $\stateinterp$ holds for the final state.
-\item If the main thread reduced to a value, the post-condition $\pred$ of the weakest precondition holds for that value.
+\item If one of the initial threads reduced to a value, the corresponding post-condition $\pred \in \vec\pred$ holds for that value.
 \item If any other thread reduced to a value, the forked-thread post-condition $\pred_F$ holds for that value.
 \end{itemize}
 
@@ -271,7 +272,7 @@ As an example for how to use this adequacy theorem, let us say we wanted to prov
 \end{cor}
 To prove the conclusion of this corollary, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ and $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)$.
 We can then show the premise of adequacy using the Iris entailment that we assumed in the corollary and:
-\[ \TRUE \proves \consstate^{\stateinterp;\pred;\pred_F}_{\NotStuck}(\tpool_2, \state_2) \vs[\top][\emptyset] \metaprop \]
+\[ \TRUE \proves \consstate^{\stateinterp;[\pred];\pred_F}_{\NotStuck}(\tpool_2, \state_2) \vs[\top][\emptyset] \metaprop \]
 This proof, just like the following, also exploits that we can freely swap between meta-level universal quantification ($\All x. \TRUE \proves \prop$) and quantification in Iris ($\TRUE \proves \All x. \prop$).
 
 ~\par
@@ -289,7 +290,7 @@ Similarly we could show that the postcondition makes adequate statements about t
 \end{cor}
 To show this, we assume some $\state_1, \vec\obs, \val_2, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_2 \in \Val$.
 Then we only have to show:
-$$\TRUE \proves \consstate^{\stateinterp;(\Lam \val. \val \in \Val);\pred_F}_{\stuckness}([\ofval(\val_2)] \dplus \tpool_2, \state_2) \vs[\top][\emptyset] \val_2 \in \Val $$
+$$\TRUE \proves \consstate^{\stateinterp;[(\Lam \val. \val \in \Val)];\pred_F}_{\stuckness}([\ofval(\val_2)] \dplus \tpool_2, \state_2) \vs[\top][\emptyset] \val_2 \in \Val $$
 
 ~\par
 
@@ -307,7 +308,7 @@ As a final example, we could use adequacy to show that the state $\state$ of the
 To show this, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_2 \in \Sigma$.
 Then we have to show:
 \[
-(\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma) \proves \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \state_2 \in \Sigma
+(\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma) \proves \consstate^{\stateinterp;[\pred];\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \state_2 \in \Sigma
 \]
 
 \paragraph{Hoare triples.}
@@ -331,7 +332,7 @@ We only give some of the proof rules for Hoare triples here, since we usually do
 \and
 \inferH{Ht-csq}
   {\prop \vs \prop' \\
-    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
+    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
    \All \val. \propB' \vs \propB}
   {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
 \and
@@ -349,7 +350,7 @@ We only give some of the proof rules for Hoare triples here, since we usually do
 % \and
 \inferH{Ht-atomic}
   {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
-    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
+    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
    \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\
    \atomic(\expr)
   }
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 599c09a10..fc3abc68c 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -14,61 +14,57 @@ 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; ⊤ {{ fork_post }})%I.
+Notation wptp s t Φs := ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
 
-Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
+Lemma wp_step s e1 σ1 κ κs e2 σ2 efs nt Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
-  state_interp σ2 κs (length efs + m) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s efs.
+  state_interp σ1 (κ ++ κs) nt -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
+    state_interp σ2 κ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".
-  by iIntros "!> !>".
+  by rewrite Nat.add_comm big_sepL2_replicate_r.
 Qed.
 
-Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
-  step (e1 :: t1,σ1) κ (t2, σ2) →
-  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'.
+Lemma wptp_step s es1 es2 κ κs σ1 σ2 Φs nt :
+  step (es1,σ1) κ (es2, σ2) →
+  state_interp σ1 (κ ++ κs) nt -∗ wptp s es1 Φs -∗
+  ∃ nt', |={⊤}[∅]▷=> state_interp σ2 κs (nt + nt') ∗
+         wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
-  iIntros (Hstep) "Hσ He Ht".
-  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
-  - 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.
-    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 lia. iFrame.
+  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 "!>".
+  rewrite -(assoc_L app) -app_comm_cons. 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') (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'.
+Lemma wptp_steps s n es1 es2 κs κs' σ1 σ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).
 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σ He Ht". inversion_clear Hsteps as [|?? [t1' σ1']].
+  revert nt es1 es2 κs κs' σ1 σ2 Φs.
+  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 σ2 Φs /=.
+  { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
+    rewrite Nat.add_0_r right_id_L. by iFrame. }
+  iIntros (Hsteps) "Hσ He". 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").
+  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.
 Qed.
 
-Lemma wp_not_stuck κs m e σ Φ :
-  state_interp σ κs m -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
+Lemma wp_not_stuck κs nt e σ Φ :
+  state_interp σ κ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.
@@ -76,83 +72,88 @@ Proof.
   iMod (fupd_plain_mask with "H") as %?; eauto.
 Qed.
 
-Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs t2 σ1 σ2 :
-  nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  state_interp σ1 (κs ++ κs') (length t1) -∗
-  WP e1 @ s; ⊤ {{ Φ }} -∗
-  wptp s t1 ={⊤}[∅]▷=∗^(S n) ∃ e2 t2',
-    ⌜ t2 = e2 :: t2' ⌝ ∗
-    ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2 ⌝ ∗
-    state_interp σ2 κs' (length t2') ∗
-    from_option Φ True (to_val e2) ∗
-    ([∗ list] v ∈ omap to_val t2', fork_post v).
+Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 σ2 nt:
+  nsteps n (es1, σ1) κs (es2, σ2) →
+  state_interp σ1 (κs ++ κs') nt -∗
+  wptp s es1 Φs ={⊤}[∅]▷=∗^(S n) ∃ nt',
+    ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝ ∗
+    state_interp σ2 κs' (nt + nt') ∗
+    [∗ list] e;Φ ∈ es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
 Proof.
-  iIntros (Hstep) "Hσ He Ht". rewrite Nat_iter_S_r.
-  iDestruct (wptp_steps with "Hσ He Ht") as "Hwp"; first done.
+  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 (e2' t2' ?) "(Hσ & Hwp & Ht)"; simplify_eq/=.
+  iDestruct 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
   iMod (fupd_plain_keep_l ⊤
-    ⌜ ∀ e2, s = NotStuck → e2 ∈ (e2' :: t2') → not_stuck e2 σ2 ⌝%I
-    (state_interp σ2 κs' (length t2') ∗ WP e2' @ s; ⊤ {{ v, Φ v }} ∗ wptp s t2')%I
-    with "[$Hσ $Hwp $Ht]") as "(Hsafe&Hσ&Hwp&Hvs)".
-  { iIntros "(Hσ & Hwp & Ht)" (e' -> He').
-    apply elem_of_cons in He' as [<-|(t1''&t2''&->)%elem_of_list_split].
-    - iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto.
-    - iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_not_stuck with "Hσ He'"). }
+    ⌜ ∀ 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
+    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 _, _. iSplitL ""; first done. iFrame "Hsafe Hσ".
-  iSplitL "Hwp".
-  - destruct (to_val e2') as [v2|] eqn:He2'; last done.
-    apply of_to_val in He2' as <-. iApply (wp_value_inv' with "Hwp").
-  - clear Hstep. iInduction t2' as [|e t2'] "IH"; csimpl; first by iFrame.
-    iDestruct "Hvs" as "[Hv Hvs]". destruct (to_val e) as [v|] eqn:He.
-    + apply of_to_val in He as <-. iMod (wp_value_inv' with "Hv") as "$".
-      by iApply "IH".
-    + by iApply "IH".
+  iExists _. iSplitR; first done. iFrame "Hσ".
+  iApply big_sepL2_fupd.
+  iApply (big_sepL2_impl with "Hwp").
+  iIntros "!#" (? e Φ ??) "Hwp".
+  destruct (to_val e) as [v2|] eqn:He2'; last done.
+  apply of_to_val in He2' as <-. iApply (wp_value_inv' with "Hwp").
 Qed.
 End adequacy.
 
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
   (∀ `{Hinv : !invG Σ},
     ⊢ |={⊤}=> ∃
          (s: stuckness)
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (Φ fork_post : val Λ → iProp Σ),
+         (Φs : list (val Λ → iProp Σ))
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗
-       WP e1 @ s; ⊤ {{ Φ }} ∗
-       (∀ e2 t2',
-         (* e2 is the final state of the main thread, t2' the rest *)
-         ⌜ t2 = e2 :: t2' ⌝ -∗
+       ([∗ list] e;Φ ∈ es;Φs, WP e @ s; ⊤ {{ Φ }}) ∗
+       (∀ es' t2',
+         (* es' is the final state of the initial threads, t2' the rest *)
+         ⌜ t2 = es' ++ t2' ⌝ -∗
+         (* es' corresponds to the initial threads *)
+         ⌜ length es' = length es ⌝ -∗
          (* If this is a stuck-free triple (i.e. [s = NotStuck]), then all
          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') -∗
-         (* If the main thread is done, its post-condition [Φ] holds *)
-         from_option Φ True (to_val e2) -∗
-         (* For all threads that are done, their postcondition [fork_post] holds. *)
+         (* 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
+            [fork_post] holds. *)
          ([∗ list] v ∈ omap to_val t2', fork_post v) -∗
          (* Under all these assumptions, and while opening all invariants, we
          can conclude [φ] in the logic. After opening all required invariants,
          one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
          fancy update. *)
          |={⊤,∅}=> ⌜ φ ⌝)) →
-  nsteps n ([e1], σ1) κs (t2, σ2) →
+  nsteps n (es, σ1) κs (t2, σ2) →
   (* Then we can conclude [φ] at the meta-level. *)
   φ.
 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φ)".
+  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. }
-  iIntros "Hpost". iDestruct "Hpost" as (e2 t2' ->) "(? & ? & ? & ?)".
+  iDestruct 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.
-  iMod ("Hφ" with "[% //] [$] [$] [$] [$]"). done.
+  iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
+  by rewrite big_sepL2_replicate_r // big_sepL_omap.
 Qed.
 
 (** Since the full adequacy statement is quite a mouthful, we prove some more
@@ -202,9 +203,11 @@ 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.
-  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ?) "_ H _".
+  iExists s, (λ σ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post => /=.
+  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_weaken; [done|]. iSplit; [|done].
+  iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
+  iDestruct (big_sepL2_nil_inv_r with "H") as %->.
   iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
 Qed.
 
@@ -222,8 +225,10 @@ 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.
-  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _) "Hσ _ _ /=".
+  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 %->.
   iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
   by iApply fupd_mask_weaken; first set_solver.
 Qed.
-- 
GitLab