Skip to content

Slightly weaker WP (i.e., easier to prove), so that we have an fupd where we did not

Jacques-Henri Jourdan requested to merge fupd_step_wp into gen_proofmode

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

Edited by Ralf Jung

Merge request reports