# A strong adequacy statement to rule them all

requested to merge robbert/adequacy into master

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`.
Edited by Robbert Krebbers