Skip to content

A strong adequacy statement to rule them all

Robbert Krebbers 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

Merge request reports