Weakest preconditions for total program correctness

This MR implements weakest preconditions for total program correctness using a least fixpoint (as suggested by @abizjak). These weakest preconditions are defined without the later modality, so one can only open invariants whose contents is timeless.

Note that for the case of concurrency, these total weakest preconditions are probably not so useful: one typically wants to prove something like totality assuming fair scheduling. To do that, we probably need something TotalTaDa-ish, but that is beyond the scope of this MR. The weakest preconditions in this MR are intended mainly to be used for sequential code.

TODO

• Prove generic weakest precondition lemmas
• Prove adequacy
• Prove the lifting lemmas
• Implement proofmode support, this depends on !64 (merged)
• Wait for !71 (merged) to be merged.

changed the description

added 2 commits

• fd6dc62e - Start working on weakest preconditions for total program correctness.
• ae1cc418 - Prove adequacy of total weakest preconditions.

Compare with previous version

added 2 commits

• d2bf32c9 - Start working on weakest preconditions for total program correctness.
• ea6ba2ed - Prove adequacy of total weakest preconditions.

Compare with previous version

added 1 commit

• fd97a7a4 - Prove adequacy of total weakest preconditions.

Compare with previous version

Neat! One thing I am wondering about: One could use least fixpoint and still have a later, right? What is the problem with that approach?

@jung You could keep the old definition with the later and take the least fixed point of that. However, the WP defined that way can be shown to be equal to the one defined using guarded recursion, and, also, to the one defined as the greatest fixed point.

That is because fixed points of contractive functions are unique.

To add to that, if you try adding the later, you cannot prove the adequacy theorem.

That is because fixed points of contractive functions are unique.

Ah, of course. And then of course we can't get total correctness. Now I wonder how removing the later makes it so that total correctness works.

Now I wonder how removing the later makes it so that total correctness works.

The way I understand it, if you have a formulation with later and with a non-terminating program, then you can "cheat" by doing Loeb induction, unfolding the fixed point once and getting rid of the guard in the induction hypothesis.

The way I understand it, if you have a formulation with later and with a non-terminating program, then you can "cheat" by doing Loeb induction, unfolding the fixed point once and getting rid of the guard in the induction hypothesis.

That makes sense.

For me, the main remaining question is whether it is better to have this in Iris proper, or to experiment in a dependency.

For me, the main remaining question is whether it is better to have this in Iris proper, or to experiment in a dependency.

I don't see any reason not to have it in Iris proper, it is rather small, and it is generic (i.e. it applies to any language).

Related to that, I think the generic parts of iris-atomic (like logically atomic triples and some theory about them) should also become part of Iris proper at some point.

Fair enough. Sounds reasonable.

To add to that: if we add total weakest preconditions and logically atomic triples, then we have some code that exercises both least and greatest fixpoints, and thus avoids regressions there.

Atomic triples will probably not end up using fixpoints due to the problem described in FP/iris-atomic!5 (comment 19660).

added 1 commit

• dae46024 - Lifting lemmas for total weakest preconditions.

Compare with previous version

added 32 commits

• dae46024...fda80965 - 29 commits from branch master
• fa7ca6b4 - Start working on weakest preconditions for total program correctness.
• 97904170 - Prove adequacy of total weakest preconditions.
• d2e429f8 - Lifting lemmas for total weakest preconditions.

Compare with previous version