Add progress bit to WP.
I indexed WP by a progress bit, making safety optional so that one can link against code that might get stuck. The meaning of WP e @ E {{ Φ }}
has not changed. The judgment WP e @ E ?{{ Φ }}
permits e
to get stuck. The judgment WP e @ p; E {{ Φ }}
where p : bool
is useful when either works. Similar notations exist for Texan and Hoare triples. There are lemmas for forgetting progress bits (e.g., converting a safe triple to a triple that might get stuck) and for lifting stuck expressions.
The heap_lang
tactics continue to assume safe WP.
I had to revert the recent weakening of atomic e
so that wp_atomic
goes through.