Document how to debug slowness of the proof

[Kixunil]

The documentation says:

Model checking allows you to prove non-trivial properties about programs, and check those proofs in roughly the same amount of time as a traditional test suite would take to run. The downside is many types of properties can quickly become "too large" to practically model-check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does. This process basically boils down to "debugging" the proof.

However I was not able to find any documentation on how to do such debugging. I've encountered some slow tests and would love to learn how to make them faster.

[adpaco-aws]

Hi @Kixunil , thanks for opening the issue!

However I was not able to find any documentation on how to do such debugging.

Unfortunately, we don't have at the moment any documentation or resources to help debugging slow harnesses. What follows is what we recommend doing in most cases:

• Remove sources of nondeterminism from the program. For example, replace values initialized with kani::any() by concrete values and check if performance improves. See Kani unwinds forever on semver-pubgrub #2982 for an example.
• Reduce collections to one or two elements at most. If your test involves any collection like Vec or BTreeSet, avoid working with more than two elements at first. Then try to split the test into multiple ones instead of having one test with multiple values. See Memory blows up on a deterministic BTreeSet harness #2517 for an example.
• Reduce loops to one or two iterations at most. Same as before: Start with just one or two iterations. If that works, there's a good chance you can decompose the test into multiple tests where a fixed amount of iterations is done each time.
• Beware of multiplication/modulo/division operations. These operations can often become too difficult for SAT solvers, especially if they involve multiple iterations or large-sized operands. See Division with concrete and constant operands causes long verification times #2801 for an example.

I hope this helps you to figure out the source of the performances issues you're seeing. Also, if the code you're working on is or can be made public, feel free to open a bug report pointing to the specific branch/example so we can further advise.

[Kixunil]

Thanks! I will look into it. I suspect loops are what made my private experiment slow. There's another public code we have that implements u256 which obviously has to contain multiplication/modulo/division. I guess we'll just accept the slowness for now.

Remove sources of nondeterminism from the program

Is there any way to do this that doesn't decrease the power of the proof? The linked issue suggests that it's better to just exhaustively test some values (bools?).

[adpaco-aws]

Thanks! I will look into it. I suspect loops are what made my private experiment slow. There's another public code we have that implements u256 which obviously has to contain multiplication/modulo/division. I guess we'll just accept the slowness for now.

Thanks for sharing your code! Please feel free to participate in issues related to slow operations or open new ones if they don't match your experience.

Is there any way to do this that doesn't decrease the power of the proof?

I can't think of any, assuming that "power" refers to the "generality" of the proof. But it's OK to decompose one proof into multiple harnesses (where one input gets fixed to a different value each time) to make the individual harnesses more efficient. Of course, the more general proof would be preferred in most cases, but that might not be feasible in some of them.