A strong adequacy statement to rule them all

The new adequacy statement unifies the jungle of old adequacy statement, namely wp_strong_adequacy, wp_strong_all_adequacy, and wp_invariance.

Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ1 n κs t2 σ2 φ :
  (∀ `{Hinv : !invG Σ},
     (|={⊤}=> ∃
         (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
         (Φ fork_post : val Λ → iProp Σ),
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
       stateI σ1 κs 0 ∗
       WP e @ s; ⊤ {{ Φ }} ∗
       (∀ e2 t2',
         ⌜ t2 = e2 :: t2' ⌝ -∗
         ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2) ⌝ -∗
         stateI σ2 [] (length t2') -∗
         from_option Φ True (to_val e2) -∗
         ([∗ list] v ∈ omap to_val t2', fork_post v) ={⊤,∅}=∗ ⌜ φ ⌝))%I) →
  nsteps n ([e], σ1) κs (t2, σ2) →
  φ.

This statement says that given given a proof of WP e @ s; ⊤ {{ Φ }} and a reduction from an initial state ([e], σ1) to some intermediate state (t2, σ2), then we can obtain a proof of a Coq proposition φ at the meta level, if we can prove |={⊤,∅}=> ⌜φ⌝ in the logic under the following conditions:

• t2 = e2 :: t2',
• All expressions in t2 are either reducible or in normal form (progress),
• The state interpretation holds for σ2,
• If the main thread t2 reduced to a value, the postcondition Φ holds,
• For any forked-off thread t2', if they are a value, fork_post holds.

Since we do not have any requirement on t2, the adequacy statement applies if just the main thread has terminated (formerly wp_strong_adequacy), all threads have terminated (formerly wp_strong_all_adequacy), or no threads have terminated (formerly wp_invariance). In fact, it works for any combination of threads that have terminated, and will give you exactly the postconditions of those threads.

Other changes

• I removed wp_invariance, and kept the more intuitive version, which was called wp_invariance'.
• I made wp_adequacy more consistent w.r.t. the other lemmas so one can also specific post_fork.