# Prusti interactively (28.1.2024)

How to make a Prusti verification workflow more interactive, or "real time", i.e. be able to gradually develop a proof and get feedback on the changes quickly (even if the verification time overall is high)?

## Per-method caching

When developing a proof, it is likely that the file/package under verification is not changing a lot from one failed verification run to another. It is likely that the changes occur within a single method, in fact. (Workflow being: Prusti indicated a number of verification errors, so the user will work through them one at a time.)

Consider a simple model of the verification pipeline: Prusti takes a Rust crate consisting of types, functions, etc. For every `fn` in the crate that should be verified, it produces a Viper method. The Viper verifier is a black box that can tell, for each Viper method, whether there is an error or not.

An additional assumption is the stability of proofs: if Viper verified/rejected a method, attempting to verify that exact same method again should give the same result.

In this pipeline, we can introduce caching on a per method level. Given a Rust crate, compute the hash of every Viper method (and dependencies) that we send to the verifier. If Prusti is invoked after a verification run, only re-verify methods whose hashes have not already been run through the verifier. For any hash that was already seen, immediately output the same result as before (success or stored errors).

## Per-method caching with re-verification

What if we want to be able to confirm the verification results we have in the cache? We could simply run the original Viper method through the verifier again, and confirm that the result is the same. Can we increase the performance of this re-verification step?

Consider a small refinement to the model of the verification pipeline: the Viper verifier is now a tool that internally invokes an SMT solver (Z3) as it verifies methods.

In addition to the result of verification, we can also ask Z3 to produce a proof log. When re-verifying, we can ask Z3 to use the proof log to "replay" the proof rather than attempting to prove the method from scratch.

Documentation/tutorial on Proof Logs in Z3: https://microsoft.github.io/z3guide/programming/Proof%20Logs/

## Branch prediction

While developing a proof and modifying one method at a time, it is likely that the method itself is also being updated gradually. For example, verification is attempted for one branch of the method control flow at a time.

Consider another refinement to the model of the verification pipeline: the Viper verifier uses symbolic execution to verify methods. It interacts with the SMT solver by pushing/popping contexts as it enters/exits nodes of the control-flow graph.

If the verifier finds a verification error within a particular CFG branch, the user may be updating the method to fix the error. When symbolically executing the method, the verifier has the freedom to choose the order in which the branches are explored, since any errors identified are aggregated. However, to give the user more rapid feedback within the IDE (where errors can be streamed), the verifier can treat branches with (more) errors with a higher precedence.

## Branch progress reporting

Similarly to its streaming reports on quantifier instantiations, the Viper verifier could report which nodes of the CFG it is currently entering. Prusti can then use this information to let the user know which parts of the method are currently being verified, e.g. by mapping the Viper CFG nodes back to spans in the original source code and colouring the lines in the IDE.

## Per-branch caching

Given a CFG-based view of a method, and a verifier which can clone Z3's state at any point in the symbolic execution, it may be possible to perform fine-grained caching of verification results.

* To check: can we check that a Z3 state matches another?

Assuming the (hash of the) Z3 state matches one seen before, the verifier can immediately return the same verification result as before.

* To check: what about join points?

## Work area

Let the user designate the part of the method under development as a "work area", with a pair of magic functions/macros `wa_begin!()`, `wa_end!()`. When looking at the control flow of the method, any verification error which occurs between the entrypoint and `wa_begin` is not relevant to the user. Analogously for any verification error which occurs after `wa_end`.

A soft contract should exist between the user and the verifier when a work area is utilised: *if* the changes to the method only affect parts of the method within the work area (which can be seen as a subgraph of the method's CFG), *then* the verifier will be able to produce relevant verification errors in a shorter amount of time. It is important to note that this contract may be broken inadvertently, by the compiler rather than the user: even if changes to a method syntactically occur within the work area, the compiler may introduce additional local variables, CFG nodes, etc, which do not strictly fall within the work area subgraph. Hence a "soft" contract.

The `wa_end` part of the work area can be encoded simply as `assume false`: any execution reaching this point no longer matters, ignore verification errors that would occur there.

The `wa_begin` part of the work area requires more care. Verification errors that occur before `wa_begin` can be hidden from the user, but the verifier still spends time here.

* To check: can we use Z3 proof logs to replay proofs partially? I.e. can we produce a proof log at some point (within a number of pushed contexts), then replay the proof to get to that same point?

While the verifier is still running, we can clone Z3's state at the point `wa_begin` is reached. We can then try to continue the Z3 interaction with the parts of the CFG that are part of the work area. This is an optimistic approach: for example, the interaction may not be well-formed because it assumes that certain variables are declared within the context when they are not (or vice versa), because the state was cloned prior to the variable existing in the program. Additionally, even if the interaction itself works, there may be changes to the context that would lead to different verification results when using the context obtained from proper execution.

As a middle ground, we can display verification errors obtained from the cloned state *tentatively*: first run the verifier against the work area using the cloned state, then run the verifier against the entry point until the work area is reached. If we can show that the cloned state matches the one reached in the second pass, then the tentative verification results are confirmed (and we can stop the verification pass), otherwise we continue verification as normal. Although the user might be presented with non-sensical verification results, they are presented much more quickly than if the entire method up to `wa_begin` was verified as well.

Another aspect of `wa_begin`: the CFG node representing the start of the work area may be in one branch of the method. Even when the verifier is (re-)verifying the part of the method before `wa_begin`, it should not waste any time exploring branches which cannot reach the `wa_begin` node at all. This should be a simple reachability check in the CFG.

## Inferring the work area

To avoid the (small) overhead of setting up/moving the work area, Prusti might attempt to infer the work area. This could be an analysis that first identifies which methods changed at all (overall hash of the input or output), then for the changed ones, tries to find CFG similarities (try to zip CFG nodes, compare hashes). This is an imperfect approach since there is no guarantee that the method has only changed within a work area, nor that the verification results of the nodes after the changes should be the same (it might suffice to treat the exit point of the method as `wa_end`). Nevertheless, if enabled, tentative verification results could be displayed to the user more rapidly.