Let's consider various styles of writing proofs. As a running example, I'll start by defining a function and some axioms about its behavior.

0. A sample problem

Consider an integer function f with two arguments:

function f(x: int, y: int): int

Since I didn't provide a body for this function, Dafny treats it as an uninterpreted function. That means we don't know anything about it. Well, we do know it's a function, which means that its result value is determined entirely by its inputs. For example, we don't know which integer f(7, 3) evaluates to, but we know that if you call f again with those same arguments, you'll keep on getting the same value back.

To prove something about f, we'd like to know a little more of f's properties. Here are declarations of three lemmas that express such properties:

lemma Associativity(x: int, y: int, z: int)
  ensures f(x, f(y, z)) == f(f(x, y), z)

lemma Monotonicity(y: int, z: int)
  requires y <= z
  ensures forall w :: f(w, y) <= f(w, z)

lemma DiagonalIdentity(x: int)
  ensures f(x, x) == x

Like the function itself, these lemmas don't have bodies. It's the body of a lemma to justifies the postcondition of the lemma. In other words, the body is what gives the proof of the lemma. Since these lemmas don't have proofs, they are effectively axioms (that is, a claim you have to accept without proof).

If you run this function and these lemmas through the Dafny compiler, you'll get complaints that they don't have bodies. But for the purpose of this note, we don't care about getting executing code from the compiler. Our focus is on proofs, and the Dafny verifier has no objections about body-less declarations. As far as the verifier is concerned, a body-less declaration just says there is nothing to check.

The property we'll set out to prove, in various styles, is:

For any a, b, c, and x, if c <= x == f(a, b), then f(a, f(b, c)) <= x.

The proof of this property uses the three axioms from above.

1. Proof calculation

Sometimes, one simple assert statement is enough of a hint for the Dafny verifier to complete a proof. Other times, what you need is a call to a lemma. When the situation isn't quite as simple as that, the most common way to write a proof in Dafny is a proof calculation [0, 3].

A proof calculation is a chain of proof steps. Each step justifies one equality (e.g., A == B), inequality (e.g., A <= B), or logical consequence (e.g., A ==> B).

A step is written vertically, to give some room to justify why the step holds. Here is a prototypical step:

  A;
==  // explain why A equals B
  B;

As this step illustrates, each formula in the chain is terminated with a semi-colon.

In the prototypical step above, I wrote the justification, also called the hint, as a comment. Such a comment is useful documentation. If the verifier cannot check your step without help, the hint needs to be more than a comment. Then, you write a block of code in curly braces, where the knowledge gained from that code is used by the verifier in proving the step. For example,

  A;
==  { LemmaThatJustifiesABEquality();  }
  B;

It's time to write our proof. Here it is:

lemma CalculationalStyleProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  calc {
    f(a, f(b, c));
  ==  { Associativity(a, b, c); }
    f(f(a, b), c);
  ==  { assert f(a, b) == x; }
    f(x, c);
  <=  { assert c <= x; Monotonicity(c, x); }
    f(x, x);
  ==  { DiagonalIdentity(x); }
    x;
  }
}

Let me read this proof calculation.

The first step says that, on account of associativity, the expression f(a, f(b, c)) equals f(f(a, b), c). Note that the hint calls the Associativity lemma with the particular parameters a, b, and c.

The second step says that f(f(a, b), c) is the same as f(x, c), because the antecedent (i.e., precondition) of the lemma we're proving says that x equals f(a, b). The verifier knows the equality x == f(a, b) from the precondition of the lemma we're proving, so the verifier does not need an explicit hint for this proof step. However, it can sometimes be nice to make such a statement in a machine-checked way, which you can do with an assert statement, like I showed here.

The third step proves f(x, c) <= f(x, x). The justification given for this step is that c <= x holds (it is given in the lemma precondition) and therefore it's okay to call the lemma Monotonicity (which requires c <= x as a precondition). The call to the Monotonicity(c, x) lemma gives us

forall w :: f(w, c) <= f(w, x)

The verifier figures out that instantiating this quantifier with x for w gives the inequality we're trying to prove in this step.

The fourth step proves f(x, x) to be equal to x. This property follows directly from axiom DiagonalIdentity, called with parameter x.

Our four proof steps have justified the following four respective properties:

f(a, f(b, c)) == f(f(a, b), c)
f(f(a, b), c) == f(x, c)
f(x, c) <= f(x, x)
f(x, x) == x

By transitivity of == and <=, these four properties give us

f(a, f(b, c)) <= x

which is what we set out to prove.

2. Direction and line-type of calculations

Generally speaking, I find proof calculations to be convincing and easy to read. You can check each step separately, and you can see how the formula is “transformed” from line to line.

Many times, but far from always, I also find proof calculations to be straightforward to author. In the example above, we start the calculation with the left-hand side of the formula

f(a, f(b, c)) <= x

we're trying to prove. Then, we look at the current line of the proof to figure out what properties we know about that expression, and what transformation we can apply next. To get more guidance in this process, it is generally best to start with the more complicated side of the formula we're trying to prove. Case in point, if you start with

calc {
  x;

it is far from obvious that a good next step is

==  { DiagonalIdentity(x); }
  f(x, x);

We could continue this proof, writing the steps from the previous section in reverse order and reversing the direction of the operator in each step (for example, changing <= to >=):

>=  { assert c <= x; Monotonicity(c, x); }
  f(x, c);

Regardless of which direction we go in, each line in the calculations I have shown so far have type int. It also also possible to write the proof with a boolean formula in each line. Here is one such example:

calc {
  f(a, f(b, c)) <= x;
==  { DiagonalIdentity(x); }
  f(a, f(b, c)) <= f(x, x);
==  { Associativity(a, b, c); }
  f(f(a, b), c) <= f(x, x);
==  { assert f(a, b) == x; }
  f(x, c) <= f(x, x);
==  { assert c <= x; Monotonicity(c, x); }
  true;
}

By transitivity of ==, this proof calculation shows that formula f(a, f(b, c)) <= x has the value true.

If you choose such boolean expressions for the lines of your proof calculation, the operator in each step often turns out to be logical implication (==>, that is, “logical weakening”) or logical “explication” (<==, “logical strengthening”, or “follows from”). Of course, you must choose one of those two directions, not use both, or else your proof calculation wouldn't make any sense. Of these directions, <== usually gives you a nicer starting point, because you'd start from the formula you're trying to prove and you'd end up with true. However, in my experience, I see that many beginners are confused by the <== direction and write calculations as if they were in in the ==> direction. Use whichever direction makes sense to you.

3. A minimal proof

A proof calculation is a way to structure proof steps. It often contains more information than the verifier needs, especially if you, for your own benefit, write the proof in small steps. If you think a proof has too much detail, you can delete some of what is not needed. Whether or not that's a good idea—or, when it is, how much to delete—is mostly a matter of taste. If you come back to the proof later, the additional detail may provide useful documentation for how the proof was constructed in the first place.

If you were to reduce the hints in the proof calculations above, the first thing you'd probably do is delete the two assert statements that are part of the proofs, or at least the assertion c <= x. But you can do more.

With the above calculation in front of us, we can easily see which lemmas are used and, importantly, which values those lemmas are instantiated with. Once you know that, then you can leave off the proof calculation altogether. The whole proof would then look like this:

lemma MinimalProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  Associativity(a, b, c);
  Monotonicity(c, x);
  DiagonalIdentity(x);
}

4. Structured assertions

For the purpose of this note, it is instructive to write the calculational proof without the calc statement. Here's what it would look like:

lemma AssertProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  Associativity(a, b, c);
  assert f(a, f(b, c)) == f(f(a, b), c);

  assert f(a, b) == x;
  assert f(f(a, b), c) == f(x, c);

  assert c <= x; Monotonicity(c, x);
  assert f(x, c) <= f(x, x);

  DiagonalIdentity(x);
  assert f(x, x) == x;
}

Each of these four groups of statements corresponds to one step in the calculation in Section 1. What was the hint in the calc statement precedes the assertion that concludes the equality or inequality that the step proves. The verifier then glues together the four conclusions to prove the postcondition of the lemma.

5. Scopes

There is a difference between the calc statement in Section 1 and the broken-out assert statements in Section 4. The difference is that each hint in the calculation is local to the proof step. That is, the scope of a hint is just the step itself. For example, suppose you moved all the hints of the calc statement in Section 1 to the first proof step. Then, two of the proof steps would no longer verify:

calc {
  f(a, f(b, c));
==  { Associativity(a, b, c);
      assert f(a, b) == x;
      assert c <= x; Monotonicity(c, x);
      DiagonalIdentity(x);
    }
  f(f(a, b), c);
==
  f(x, c);
<=  // error: step not verified
  f(x, x);
==  // error: step not verified
  x;
}

That is, the information gained from calling the three lemmas in the hint in the first step does not rub off on the other steps. In contrast, if you collected the hint at the start of the lemma body, the four equality and inequalities would verify fine:

// hints
Associativity(a, b, c);
assert f(a, b) == x;
assert c <= x; Monotonicity(c, x);
DiagonalIdentity(x);
// equalities and inequalities
assert f(a, f(b, c)) == f(f(a, b), c);
assert f(f(a, b), c) == f(x, c);
assert f(x, c) <= f(x, x);
assert f(x, x) == x;

You can think of each step of a calc statement as being a little lemma in its own right, where the proof of that lemma is placed in the hint for that step. This makes a difference in writing your proof, not just because it tells the human reader that a certain hint applies to a particular proof step, but also because it limits where the verifier is able to apply a hint. For complicated proofs, this can make a big difference in practice, because the verifier can get “confused” with too much information—this manifests itself in poor verifier performance or some “butterfly effect” [2].

In conclusion, it's good to compartmentalize hints in a proof. The calc statement is good at that, but you can also do it with a form of the assert statement. Let's look at that next.

6. Assert by

The statement assert E; says three things:

0. it declares that you expect condition E to hold
1. it asks the verifier to prove E
2. it lets what follows the assertion assume E

You may not have thought to separate these three aspects of an assertion, but it's useful to do that, because Dafny provides alternatives to (1) and (2).

The statement

assert E by { Hint }

changes aspect (1) to say that E is proved under the given hint, where Hint is a statement. The scope of the hint is just the assertion itself, so it is not available downstream of the assert. In this way, the assert by statement is equivalent to:

calc {
  E;
==  { Hint }
  true;
}

We can rewrite the proof from Section 4 using assert by:

assert f(a, f(b, c)) == f(f(a, b), c) by {
  Associativity(a, b, c);
}
assert f(f(a, b), c) == f(x, c) by {
  assert f(a, b) == x;
}
assert f(x, c) <= f(x, x) by {
  assert c <= x; Monotonicity(c, x);
}
assert f(x, x) == x by {
  DiagonalIdentity(x);
}

This provides better compartmentalization, and thus more directly expresses why each asserted condition holds.

7. Proof by explicit ancestors

The proof in the Section 6 contains two assertions that restate what's written in the precondition. The idea behind those assertions is to make explicit where those preconditions are used. However, this has two shortcomings.

One shortcoming is that you have to compare the expression in the assertion with other expressions in the proof to realize that the assertion is just restating a previously available assumption. It would be nice if we could label the condition instead and then refer to the label.

The other shortcoming is that the preconditions are available regardless of if we restate the condition in an assertion. If we forget to write the assertion (perhaps because we don't realize that we're depending on this condition) or if we accidentally write the wrong precondition, then the proof still goes through. That is, the verifier is already able to use the precondition, so it doesn't care if you restate the condition, state a different (true) condition, or state nothing more. It would be nice if we could be more explicit about the scope of these assumptions.

There is one more form of the assert by statement. It relaxes aspect (2) from Section 6. This form looks like this:

assert Label: E by { Hint }

This labeled assert statement says you expect condition E to hold and it offers statement Hint as a proof for E. The use of a label before the condition has the effect of suppressing the use of E as a downstream assumption.

For example, to prove f(12, 12) == 12 requires a use of axiom DiagonalIdentity. If you use a labeled assert by to prove this fact, then the proved fact is still not available after the labeled assert:

assert Label: f(12, 12) == 12 by {
  DiagonalIdentity(12);
}
assert f(12, 12) == 12;  // error: assertion not verified

Why would you use such a statement if you can't use the fact you proved? Well, I should rather have said that the fact isn't automatically available after the labeled assertion. But you can explicitly request it. You do that with a reveal statement, in which you mention the label.

Here is the example again, but with a reveal statement:

assert Label: f(12, 12) == 12 by {
  DiagonalIdentity(12);
}
reveal Label;  // this recalls the condition from the prior assertion
assert f(12, 12) == 12;

You can play the same trick on preconditions. That is, usually in a lemma (or method or function), a precondition

requires E

is available throughout the body of the lemma. But if you label it, you have to use a reveal statement to bring out this assumption:

requires Label: E

Before we see this in action, let me say something about labels. A label in Dafny can be any identifier, but it can also be something that, textually, looks like a numeric literal. Here are five example labels:

MyLabel    Label57    L57    57    000_057

These are five distinct labels—the fact that, as numerical literals, 57 and 000_057 represent the same number does not make them the same label. If they look different on the printed page, they are different labels. (This is also true for field names in classes, destructors of datatypes, and other type members, which also have the extended syntax of allowing literal-looking identifiers.)

Alright, now we're ready to use labeled assertions in our running example:

lemma DifferentStyleOfProof(a: int, b: int, c: int, x: int)
  requires A: c <= x
  requires B: x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  assert 0: f(a, f(b, c)) == f(f(a, b), c) by {
    Associativity(a, b, c);
  }

  assert 1: f(f(a, b), c) == f(x, c) by {
    reveal B;
  }

  assert 2: f(x, c) <= f(x, x) by {
    assert c <= x by { reveal A; }
    Monotonicity(c, x);
  }

  assert 3: f(x, x) == x by {
    DiagonalIdentity(x);
  }

  assert 4: f(a, f(b, c)) == f(x, c) by {
    reveal 0, 1;
  }

  assert 5: f(x, c) <= x by {
    reveal 2, 3;
  }

  assert f(a, f(b, c)) <= x by {
    reveal 4, 5;
  }
}

In this style of proof, which is common in some texts on logic, each assertion is explicitly justified by through its dependencies. If you think of the dependencies among assertions as forming a proof DAG, then this style of proof is being explicit about the ancestors in the DAG. You can use the hierarchical structuring of nested assert by statements and labeled assertions to approximate a Lamport-style proof [1].

8. Summary

There are different styles of writing proofs. The absolutely simplest proofs are the ones that are done automatically and don't have to be further justified. Other simple proofs require an assert statement or a call to a lemma. Proof steps can be organized using calc statements and assert by statements. By labeling an assert by statement or a precondition, the condtion is suppressed from the proof until you explicitly ask for it back using a reveal statement.

Structuring proofs is a good idea, for readability and clarity, as well as for improved mechanical-prover performance. You can think of a proof statement as having some number of input conditions. These are the conditions and labels that are available in the context of the proof statement. The output of a proof statement is the transitive connection of the first and last lines of a calc statement, the condition in an unlabeled assert or assert by statement, and the label of a labeled assertion.