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 forkedoff 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 calledwp_invariance'
.  I made
wp_adequacy
more consistent w.r.t. the other lemmas so one can also specificpost_fork
.