Due to the nature of the underlying SMT used by Dafny for proof checking, Dafny sometimes takes a very long time to verify things. I find it useful to ask Dafny to work on a single lemma at a time. This can be achieved using the {:verify false} annotation. I set every function and method in my proof to {:verify false}, then change only the one I am working on back to {:verify true}. Occasionally I use find and replace to change all the {:verify false} annotations to {:verify true} and then run the whole proof through the Dafny command line.

I am using Opaque functions in Dafny quite heavily, and for three main reasons:

Opaque functions can improve performance

I have a very large predicate which judges partial isomorphism between two program states. This predicate appears in the requires, ensures and bodies of a large number of lemmas and functions in my proof. The number of facts that are introduce by Dafny automatically revealing these function definitions seems to substantially slow down the proof step, sometimes to the point where it no longer goes through in an amount of time I am willing to wait.

For example take a predicate like this

prediate I(a:T,b:T)
{
   P(a,b) && Q(a,b) && R(a,b) && S(a,b)
}
predicate P(a:T,b:T) { ... }
predicate Q(a:T,b:T) { ... }
...
static lemma IThenSomethingThatReliesOnQ(a:T,b:T)
  requires I(a,b);
  ensures SomethingThatReliesOnQ(a,b);
{
   // Q automatically revealed, but so is P,R and S
}

Instead we can write

prediate I(a:T,b:T)
{
   P(a,b) && Q(a,b) && R(a,b) && S(a,b)
}
predicate {:opaque true} P(a:T,b:T) { ... }
predicate {:opaque true} Q(a:T,b:T) { ... }
...
static lemma IThenSomethingThatReliesOnQ(a:T,b:T)
  requires I(a,b);
  ensures SomethingThatReliesOnQ(a,b);
{
   reveal_Q(); // reveals Q only, not P,R and S
}

Opaque functions can improve readability

I initially really liked the automatic function definition revealing feature, but as my proof got larger I liked it less. Particularly in the presence of big predicates (like my isomorphism predicate), I found it can get quite hard to understand which parts of the proof rely on which facts. This made it harder for me to work out what I need to establish in other parts of the proof (in this case, that the isomorphism has certain properties and that those can be used to show it is preserved by some particular program execution steps).

The example above shows how using opaque and reveal makes the proof more self documenting, allows us to automatically check that documentation and provides (I think) more insight into the proof.

Opaque functions help you find places that need re-verifying

If you are using {:verify false} to restrict re-verification only to the elements you are working on, then having functions set to opaque helps you find all the places that depend on their definition. So, if you change the definition then you can easily find all the places that will need to be re-verified with the new definition.

It seems to help Dafny with instantiation of quantifiers during proofs if you give the quantified expression a name by encapsulating it in a predicate. If you don’t you can end up in a situation where you prove some quantified property, but are then unable to subsequently assert that quantified property, I think due to Dafny not understanding that the quantification is the same. Naming the property (or more likely, only writing it in one place rather than two places) fixes this.

For example rather than writing:

   ...
   ensures forall c :: P(a, c) == P(b, c);
   ...
   assert forall c :: P(a, c) == P(b, c);

Write this:

   predicate Q(a:S,b:S)
   { forall c :: P(a, c) == P(b, c) }
   ...
   ensures Q(a, b);
   ...
   assert Q(a, b);