Incremental solving

[pchaigno]

At the LinuxPlumbers'24 talk, @viktormalik suggested we may want to try incremental solving [1] to improve performance. In modular mode, Agni performs the verification of reg_bounds_sync and per-operation logic separately. AFAIU, the idea here would be to let the solver use what it learned during the verification of the per-operation logic for the verification of reg_bounds_sync. It looks like, if possible, it should be fairly simple and may help improve performance, so it's probably worth taking a look. Opening this so we don't forget about it.

@viktormalik Feel free to add more explanations/references if you have any.

cc @shunghsiyu

1 - https://stackoverflow.com/questions/18269016/incremental-solving-in-z3-using-push-command

[viktormalik]

Let me clarify things a bit as there may be slight misunderstanding :-)

Incremental solving is especially effective when you repeatedly solve multiple formulae which are to large extent the same. I don't think that it would help in this particular case as I expect the formulae for verifying the individual operations logic and the reg_bounds_sync function to be fairly different.

I'm not sure how you could use incremental solving in this work but it's certainly something to keep in mind as it can be very effective when used correctly.

Also, @pchaigno mentioned that you plan to split verification of reg_bounds_sync to multiple independent pieces. If these cannot be verified separately (b/c they are not sound piece-wise but only as a whole), my other idea is to try to deduce some "summary" from the earlier stages (albeit they are not sound) which can help prove soundness of the later stages of the function. That could help proving soundness of the entire function while keeping high scalability thanks to verifying things in pieces.

[harishankarv]

That helps Viktor, thanks for the clarification!

Indeed, verifying individual pieces seems to be the way forward for scaling our verification.

As it stands, the individual pieces of reg_bounds_sync are sound, but this might not be the case in the future.

my other idea is to try to deduce some "summary" from the earlier stages (albeit they are not sound) which can help prove soundness of the later stages of the function.

Any pointers on what these summaries would look like in general, and how does one go about deducing them?

[viktormalik]

my other idea is to try to deduce some "summary" from the earlier stages (albeit they are not sound) which can help prove soundness of the later stages of the function.

Any pointers on what these summaries would look like in general, and how does one go about deducing them?

It very much depends on your verification approach. In general, you want the summary to describe constraints (probably some SMT formulae in your case) over variables and memory locations shared between the stages.

If you wish, I'll happy to chat about this off this issue.

[harishankarv]

Thanks for the heads up Viktor, that makes sense.

I will contact you here once we decide on an approach for the next steps. We can decide how (meet/zoom/etc.).