Dafny Power User:

Different Styles of Proofs

Different Styles of Proofs

**Abstract.** Just like there are different sentence structures for expressing
various ideas in writing and speaking, there are different proof structures
to express proofs. This note shows some variations that are possible
in Dafny.

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.

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.

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.

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.

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);
}
```

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.

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.

The statement `assert E;`

says three things:

- it declares that you expect condition
`E`

to hold - it asks the verifier to prove
`E`

- 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.

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 { 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].

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.

[1]Leslie Lamport.
How to write a 21st century proof.
Technical report, Microsoft Research, 2011.
https://lamport.azurewebsites.net/pubs/proof.pdf. 🔎

[2]K. Rustan M. Leino and Clément Pit-Claudel.
Trigger selection strategies to stabilize program verifiers.
In Swarat Chaudhuri and Azadeh Farzan, editors, *Computer Aided
Verification - 28th International Conference, CAV 2016, Proceedings, Part
I*, volume 9779 of *Lecture Notes in Computer Science*, pages 361–381.
Springer, 2016. 🔎

[3]K. Rustan M. Leino and Nadia Polikarpova.
Verified calculations.
In Ernie Cohen and Andrey Rybalchenko, editors, *Verified
Software: Theories, Tools, Experiments — 5th International Conference,
VSTTE 2013, Revised Selected Papers*, volume 8164 of *Lecture Notes in
Computer Science*, pages 170–190. Springer, 2014. 🔎