(* iris/program_logic/adequacy.v *)
(* Iris's generic adequacy result *)
Lemma wp_strong_adequacy_gen hlc Σ Λ `{!invGpreS Σ} s es σ1 n κs t2 σ2 φ
        (num_laters_per_step : nat → nat) :
  (* WP *)
  (∀ `{Hinv : !invGS_gen hlc Σ},
      ⊢ |={⊤}=> ∃
         (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
         (Φs : list (val Λ → iProp Σ))
         (fork_post : val Λ → iProp Σ)
         (* Note: existentially quantifying over Iris goal! [iExists _] should
         usually work. *)
         state_interp_mono,
       let _ : irisGS_gen hlc Λ Σ := 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 *)
         ⌜ 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 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
            [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_mask_subseteq] to introduce the fancy update. *)
         |={⊤,∅}=> ⌜ φ ⌝)) →
  nsteps n (es, σ1) κs (t2, σ2) →
  (* Then we can conclude [φ] at the meta-level. *)
  φ.
Proof.
  intros Hwp ?. apply (pure_soundness (PROP:=iPropI Σ)).
  apply (laterN_soundness _ (steps_sum num_laters_per_step 0 n + 1)).
  rewrite laterN_add /= -except_0_into_later.
  apply (fupd_finally_soundness hlc (steps_sum num_laters_per_step 0 n) ⊤).
  iIntros (?) "H£".
  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)". clear Hwp.
  iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
  pose (iG := IrisG _ stateI fork_post num_laters_per_step state_interp_mono).
  rewrite -(right_id_L [] (++) κs).
  iMod (@wptp_preservation _ _ _ iG with "Hσ H£ Hwp") as "H /="; first done.
  rewrite Nat.add_0_r. iApply step_fupdN_fupd_finally.
  iApply (step_fupdN_wand with "H"); iIntros ">(%nt' & Hσ & Ht)".
  iApply (fupd_finally_keep
    ⌜∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2⌝); iSplit.
  { iIntros (e -> [i He]%list_elem_of_lookup).
    iDestruct (big_sepL2_lookup_l with "Ht") as (Φ' _) "He"; first done.
    iMod (@wp_not_stuck _ _ _ iG with "Hσ He") as %?. done. }
  iIntros (?). iMod (wptp_postconditions with "Ht") as "Ht".
  iDestruct (big_sepL2_app_inv_r with "Ht") as (es' t2' ->) "[Hes' Ht2']".
  iDestruct (big_sepL2_length with "Hes'") as %?.
  iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
  rewrite length_replicate in Hlen2; subst.
  rewrite big_sepL2_replicate_r // -big_sepL_omap.
  iMod ("Hφ" with "[//] [] [//] Hσ Hes' Ht2'") as %?; first by rewrite Hlen1.
  done.
Qed.