On https://​github.​com/​Microsoft/​dafny/​issues/​231, a Dafny user asked:

Is there a way in Dafny to mark a lemma as “automatic” and add it to the knowledge base of z3 ?

For student homeworks, we often stumble on specifications that are just a bit too complex for Dafny to prove, and require some hand-crafted asserts or lemmas.

It would be nice if we could define those lemmas to augment boogie/z3 search space with domain-specific knowledge, avoiding the need to explain to our students how lemmas work, and the tedious and difficult task to find and use the required lemmas.

Is something like an {:auto} annotation feasible ? Can we augment the .bpl axiomatization ?

Here is an example that shows the issue. Suppose you declare a function and prove a property about it:

function FibFib(n: nat): nat {
  if n == 0 then 0
  else if n == 1 then 2
  else FibFib(n-2) + FibFib(n-1)
}

lemma FibFibIsEven(n: nat)
  ensures FibFib(n) % 2 == 0
{
  // automatically proved by induction
}

For your application, it may be crucial that FibFib always returns an even number. Using the declarations above, you would then have to call the lemma FibFibIsEven every time you use the function. This is tedious. Is there some way to instruct Dafny to automatically apply FibFibIsEven whenever it's needed?

No, there's no such feature in Dafny. (VCC had such a feature, for example.) In some situations, such automation may work well. In other situations, it may cause the lemma to be invoked too many times (say, an infinite number of times), which is problematic.

If you have an interest in trying out some kind of {:autoLemma} feature, please feel free to play around with the open Dafny sources. In the present state, I have four suggestions that you may try, and which may alleviate some of the tedium you're experiencing.

Uber Lemmas

One suggestion is to create an “uber lemma” that collects the statements of several other lemmas. For example, if you already have:

lemma Lemma0(x: X) ensures P0(x) { ... }
lemma Lemma1(x: X) ensures P1(x) { ... }
lemma Lemma2(x: X) ensures P2(x) { ... }

then you can combine them into one:

lemma Everything(x: X)
  ensures P0(x) && P1(x) && P2(x)
{
  Lemma0(x: X);
  Lemma1(x: X);
  Lemma2(x: X);
}

This lets you get all 3 properties by calling a single lemma.

Aggregate Lemma Invocations

Another suggestion is to invoke a lemma on many values at the same time. Given:

lemma LemmaForOneX(x: X) ensures P(x) { ... }

you can invoke this lemma for all values of X simultaneously:

forall x {
  LemmaForOneX(x);
}

By placing this forall statement at the beginning of some code you're trying to prove, you have in effect called it for every imaginable value of X. You can of course also tuck this statement into a lemma of its own and then call this one lemma:

lemma LemmaForEveryX()
  ensures forall x :: P(x)
{
  forall x {
    LemmaForOneX(x);
  }
}

In many cases, this will work fine. In other cases, the verifier may not realize that you have called the lemma on the value that needs the individual lemma, so you may still need to invoke LemmaForOneX manually. Also, Dafny takes measure to avoid “matching loops” in the quantifiers generated for the lemma calls above (“matching loops” are what can cause an infinite number of uses of the lemmas). However, the mechanism is not perfect, so this added automation may in some cases cause degraded performance.

Function Postconditions

A third suggestion is to declare some of the most useful properties of a function in the postcondition of the function, rather than in a separate lemma. For example, instead of:

function F(x: X): int { ... }
lemma AboutF(x: X)
  ensures F(x) % 2 == 0
{ ... }

you can declare:

function F(x: X): int
  ensures F(x) % 2 == 0
{ ... }

To obtain the property stated by the lemma, you must call the lemma. In contrast, any property stated in the postcondition of a function is automatically applied every time you call the function.

As I've mentioned, more information can help the verifier do more things automatically, but too much information can also overwhelm and confuse the verifier. Therefore, my suggestion is to use function postconditions only for those properties that you think every user of the function will need. Properties needed more rarely are better off declared in lemmas that have to be manually invoked.

Also, there are limits to what you can write in a function postcondition. In particular, what you write must “terminate”. In practice, this means you may have problems mentioning the function applied to other arguments in the postcondition. For example,

predicate R(x: X, y: X)
  // commutativity:
  ensures R(x, y) <==> R(y, x)
  // transitivity:
  ensures forall z :: R(x, z) && R(z, y) ==> R(x, y)

is not admitted, because there are self-referential non-terminating (that is, infinitely recursive) calls in the postcondition. Thus, properties like commutativity and transitivity always need to be stated as separate lemmas.

Basic/premium function pairs

A function postcondition conveniently provides all users of a function with the property that it states, alleviating the need to call the lemma explicitly. If the property is not interesting for all users, a fourth suggestion is to declare two functions. The basic function gives the actual definition of the function and an accompanying lemma states the property about it. The premium function calls the basic function and states the property as its postcondition, which is proved by a call to the lemma.

function F(x: X): int { ... }
lemma AboutF(x: X)
  ensures F(x) % 2 == 0
{ ... }

function F_premium(x: X): int
  ensures F_premium(x) % 2 == 0
{ AboutF(x); F(x) }

Users can now choose: a call to F_premium obtains both the value of the function and the proved property, whereas a call to F obtains only the value. If you expect the premium version to be more popular than the basic version, you can of course rename F and F_premium to F_basic and F, respectively.

Other than the postcondition, the two functions are synonyms. Semantically. A note of caution is that the mechanism the verifier uses as a guide to its use of quantifiers is syntactic. Therefore, which of the two functions you use in the body of a quantifier can make a difference in when the verifier decides to instantiate the quantifier. For this reason, I suggest you use the basic version of the function inside any quantifier you write.

Acknowledgments

Bryan Parno provided the fourth suggestion of wrapping a basic version of a function and its lemma into a premium version of the function.