Persistent caching of verification results

[emugnier]

During the verification of multiple files using the Dafny CLI, most of the time is spent on the VCs generation, the conversion of these VCs to SMTLib queries, and solving these queries.It would be convenient to cache some of the verification results as done is the Dafny’s VSCode extension to avoid all of this processing if a file has not been changed.

One option is to make the current cache persistent but serializing the implementation object and all the nested objects that it contains is tricky.
A simpler option is to hash the Boogie code of an implementation once everything is inlined and use it as a key to store the verification result. An optional argument could be added to Boogie like cache:<filename> where <filename> is the file containing the map of boogie implementation hashes to verification results.

This option would make developing using the Dafny CLI faster by reverifying only what has changed.

[keyboardDrummer]

It would be convenient to cache some of the verification results as done is the Dafny’s VSCode extension to avoid all of this processing if a file has not been changed.

Actually, translation to Boogie is never cached, also not by the IDE, although that's something we'd like to do. Also, caching of verification after translation to Boogie is an experimental feature that's off by default.

I'm not sure I understand the two options you describe for caching. Wouldn't any cache boil down to a Key-Value map, where persisting that cache requires serializing the Key and Value? The Key is likely a hash so simple to persist, and the value some complicated object.

[emugnier]

The first option I was describing is to make the VerificationResultCache from VerificationResultCache.cs persistent by storing the cache in a file instead of in memory. Both the keys and the values are difficult to serialize.

The second option corresponds to what you are describing. However, I was hoping that for the value of the cache we would not have to serialize a complicated object. It seems tricky to serialize an object such as VerificationResult. Wouldn't it be possible to store the outcome Verification.Outcome in the cache and create a new VerificationResult object? Or would it break later part of the code?

[keyboardDrummer]

I think what you're saying is you only want to cache verification of methods that successfully verified, since that would simplify what needs to be persisted. I think making the cache work in such a partial way might be more effort, and be more prone to error, than serializing the whole Value (which might be VerificationResult in this case) object.

I think the main effort in caching verification is in determining the keys of the cache.

[emugnier]

The cache keys can be the cryptographic hash (to avoid collisions) of the content of the boogie impl inlined.

One problem with this approach is that parameters passed to Boogie that can change the verification results and do not influence the IR are not taken into account. They need to be included somehow to the hashed string to avoid any unsoundness issue.