Slightly weaker WP (i.e., easier to prove), so that we have an fupd where we did not
In iGPS/Lambdarust-weak, we need to use something like the wp_step_fupd
rule at some places, but the decision on whether we use it or not depends on the step which is taken (in a non-deterministic context).
However, in the current definition of WP, this is impossible, since there is no fupd available between the quantification over the next state and the later. This MR fixes this issue and hence gives a more powerful WP. Of course, this is compatible with the previous definition, in the sense that the old one implies the new one.
This gives rise to new lifting lemmas, that are more expressive. However, even though they imply the previous ones, they are syntactically incompatible, and therefore, in order to avoid incompatibilities, I wrote new lifting lemmas (suffixed with _fupd
) and kept the statement of the old one as is. I am not sure this is the right way to go, given the number of lifting lemmas we have. Perhaps we should just keep the new ones, and let the various developments adapt the proof of their lifting lemmas. That should not be complicated.
-
Update CHANGELOG
Cc @haidang