Verifying while loops (with mvcgen)

Stream: Program verification

[Alexander Bentkamp]

Hello!

Is there any ongoing work for verification of while loops? The current implementation is marked as partial, preventing us from proving anything about it: https://github.com/leanprover/lean4/blob/master/src/Init/While.lean#L25
The only way I see around this is to add a second definition that uses partial_fixpoint, whenever the employed monad allows it. Then it should be fairly easy to add a spec for mvcgen as well.

Would the lean4 maintainers be interested in a PR in this direction?

[Henrik Böving]

I think this intersects with plans that @Paul Reichert has regarding extrinsic termination

[Paul Reichert]

I believe @Sebastian Graf is thinking about having a while...decreasing syntax that lets you provide a termination proof in place, an then this loop will not rely on partial such that you can prove things about it.

Henrik is right that I'm planning to provide a mechanism to defer such termination proofs. This makes the definition much simpler, but you will still need to prove termination before you can prove things. Rught now, we are still making sure that the machanism is actually compatible with the compiler's behavior, so it's not 100% certain that it will happen.

[Sebastian Graf]

I think in order to have while ... decreasing syntax (or even just while with extrinsic termination proofs) we first need to touch WF preprocessing to add support for monadic attach. Without that, it would be very inconvenient to write while loops in such a way that termination proofs are feasible.

So yes, it's on our radar, but it won't happen in this Q. If we as the FRO decide to work on it, then Q2 next year seems realistic.

[Alexander Bentkamp]

Okay, thanks for the quick replies!