How can I avoid long solver times?

[benreynwar]

I'd like to use dafny to write programs that generate circuits and be able to prove properties about the circuits that are generated.

At the moment I'm just starting out and am learning my way around dafny. I worked through the "Program Proofs" book, which I really enjoyed, and have received helpful feedback on stack exchange for specific questions.

I'm having the problem though, that as soon as I move from simple examples to a real problem that I'd like to solve, that I'm constantly hitting prohibitively long solver times. Presumably either:

1. I'm attempt to solver problems in dafny that aren't appropriate for dafny.
2. The way I'm formulating the problem in dafny is not appropriate.
3. There are additional tricks or techniques for using dafny that I need to learn.

Below I'm attaching a link to a github commit where I'm creating a structure to represent a circuit, and then adding a function that will combine two of the circuits into a single circuit. As soon as I try to write a lemma to prove properties about this function, I quickly hit long solve times. The lemma is at the bottom of the file, and the final expression in a 'calc' statement is just the unrolling of a function, yet this unrolling causes the solver to timeout. What am I missing?

benreynwar/dafny_experiments@2ab30fd

Also, any additional suggestions on how whether this problem is appropriate for dafny or whether I'm going about it in the wrong manner would be very much appreciated! My normal languages are python and verilog, so this is quite a different approach from what I'm used to.

[benreynwar]

I did manage to get the property I was stuck on solved in the end (benreynwar/dafny_experiments@73d66c4).
Using 'reveal' statements seemed to help.
But any advice on my approach would still be much appreciated.

[atomb]

There are a few things I could suggest here.

First (and perhaps this is what you're saying has already helped) it might be helpful to add the opaque keyword to some of your functions and predicates and then explicitly use reveal when you need to use their definitions (as opposed to their postconditions or lemmas about them).

Doing this is probably especially important for predicates that use forall in their bodies. Even though Dafny can often prove quite sophisticated properties about quantified statements, the more of them that are present in the context of the code you're verifying the more unpredictable (and, generally, slower) the verification process will get. So making sure that only the ones you need at the moment are visible at any particular program point can help a lot. One thing that can help is to make at least some of your lemmas take extra parameters to bind the variables that you want to quantify over instead of having forall in their postconditions. You can then use these lemmas to prove something universal, by calling them in the body of a forall statement, but they can also be instantiated where they're used.

Once you've made more functions and predicates opaque, writing some additional lemmas about them that use opaque predicates in their requires and ensures clauses can be useful. Those predicates can encapsulate core abstractions, and will sometimes need to be revealed, but can sometimes be propagated in their abstract form from, say, the postcondition of one lemma to the precondition of another.

Besides that, there are some changes upcoming in Dafny that I think may make this program verify at least a little more quickly. Stay tuned!

[benreynwar]

Thanks for taking the time to look at my attempts. This is really helpful advice.

[atomb]

One other suggestion if you haven't already looked at it is that we have a guide on optimizing proofs that goes into a little more detail on some of the things I mentioned above: https://dafny.org/latest/VerificationOptimization/VerificationOptimization

[benreynwar]

This is exactly the document I need to read. Thanks so much!