Interactive proof debugging

[sakehl]

One of the things that make verification time intensive and hard, is that it is hard to iterate consecutive proofs. Especially if verification takes a few minutes of even more. It slows down your progress if you have to wait 5 minutes to see if your annotations are correct. I had the idea, maybe we can save the internal proof state & when a proof fails we can query this internal state. In essence you are asking the SMT solver queries, which it tries to answer immediately. Additionally we can add breakpoints to inspect the internal state at certain program points.

This idea comes from the fact that I know you can manually already do something like this in Viper. As in, you can let viper verify your file and produce an smt2 file, which are all the queries Viper asks of the SMT solver. And if your verification hangs, you can stop verification, and if you remove all the 'check-sat' from the SMT file except for the last one. From there you could, potentially, ask any queries towards an SMT solver.

I think you could even use an SMT solver efficiently, since you can use 'push' and 'pop' which I think make the SMT solver reuse parts (although a bit unsure on this).

I think we could do these things:

• If your proof fails, we save the last state and this allows you to query things to be true at the last state and understand better why your proof might have failed.
• We can add proof break points, similar to normal break points when you are debugging. When the prover hits this break point, you can ask the prover queries to understand what the internal state is and what can and what cannot be proven. We could also display the internal path conditions, although they might be hard to read.

I think most of the work that should be done is in Viper, although this is especially interesting if you link it toward a front end such as VerCors to see if you can translate the internal proof state towards something a user can understand.

An point is that 'debugging' changes your internal state, because of triggers. Since due to your asserts quantifiers can get triggered which otherwise would not. I don't think this matters to much, and maybe you can use pop and push here as well to remove your debugging state.

A different tangent is that when you are saving a proof state, maybe we can link and reuse previous proof states when only minor program edits are made. For instance, your program only fails verification at a loop-invariant deep down your program. You decide to change only that loop invariant, so everything above stays the same. Thus the path condition in Viper up to that point should remain the same, so it would be great if the program only changes there.

Anyway, I think this proof debugging might be interesting as master project, but I'd love to hear your thoughts!

[sakehl]

Actually the last paragraph is maybe a bit similar towards what @ArmborstL suggested in #1216 with fine grained caching.

[superaxander]

Silicon actually has debugging support similar to what you describe which was added by a master student of theirs a few months ago. Basically whenever verification fails you can inspect the current path conditions, add and remove assumptions, retry with a different timeout, or even retry with a different SMT solver. I did have a design project proposal for bachelor students to work on bringing support for that into VerCors. Unfortunately no student group chose it but maybe in the next round there'll be group.

[sakehl]

That is really cool! Do you have a reference towards it? I could not find it at their homepage.

[superaxander]

No information about how to use it, but it was described here It's pretty simple to figure out how it works though, just add --enableDebugging and it'll just attempt to verify and then show you all the failed assertions that you can debug.