6.1.1. Example: Swapping🔗

Consider the following program, which swaps the values of two variables using addition and subtraction, instead of by assigning to a temporary variable.

X := X + Y;
Y := X - Y;
X := X - Y

We can give a proof, in the form of decorations, that this program is correct — i.e., it really swaps X and Y — as follows.

(1)    {{ X = m ∧ Y = n }} ->>
(2)    {{ (X + Y) - ((X + Y) - Y) = n ∧ (X + Y) - Y = m }}
         X := X + Y
(3)                     {{ X - (X - Y) = n ∧ X - Y = m }};
         Y := X - Y
(4)                     {{ X - Y = n ∧ Y = m }};
         X := X - Y
(5)    {{ X = n ∧ Y = m }}

The decorations can be constructed as follows:

• We begin with the undecorated program (the unnumbered lines).

• We add the specification — i.e., the outer precondition (1) and postcondition (5). In the precondition, we use parameters m and n to remember the initial values of variables X and Y so that we can refer to them in the postcondition (5).

• We work backwards, mechanically, starting from (5) and proceeding until we get to (2). At each step, we obtain the precondition of the assignment from its postcondition by substituting the assigned variable with the right-hand-side of the assignment. For instance, we obtain (4) by substituting X with X - Y in (5), and we obtain (3) by substituting Y with X - Y in (4).

• Finally, we verify that (1) logically implies (2) — i.e., that the step from (1) to (2) is a valid use of the law of consequence — by doing a bit of high-school algebra.

6.1.2. Example: Simple Conditionals🔗

Here is a simple decorated program using conditionals:

(1)   {{ True }}
        if X ≤ Y then
(2)                    {{ True ∧ X ≤ Y }} ->>
(3)                    {{ (Y - X) + X = Y ∨ (Y - X) + Y = X }}
          Z := Y - X
(4)                    {{ Z + X = Y ∨ Z + Y = X }}
        else
(5)                    {{ True ∧ ¬(X ≤ Y) }} ->>
(6)                    {{ (X - Y) + X = Y ∨ (X - Y) + Y = X }}
          Z := X - Y
(7)                    {{ Z + X = Y ∨ Z + Y = X }}
        end
(8)   {{ Z + X = Y ∨ Z + Y = X }}

These decorations can be constructed as follows:

• We start with the outer precondition (1) and postcondition (8).

• Following the format dictated by the hoare_if rule, we copy the postcondition (8) to (4) and (7). We conjoin the precondition (1) with the guard of the conditional to obtain (2). We conjoin (1) with the negated guard of the conditional to obtain (5).

• In order to use the assignment rule and obtain (3), we substitute Z by Y - X in (4). To obtain (6) we substitute Z by X - Y in (7).

• Finally, we verify that (2) implies (3) and (5) implies (6). Both of these implications crucially depend on the ordering of X and Y obtained from the guard. For instance, knowing that X ≤ Y ensures that subtracting X from Y and then adding back X produces Y, as required by the first disjunct of (3). Similarly, knowing that ¬ (X ≤ Y) ensures that subtracting Y from X and then adding back Y produces X, as needed by the second disjunct of (6). Note that n - m + m = n does not hold for arbitrary natural numbers n and m (for example, [3 - 5 + 5 = 5]).

{{ True }}
  if X ≤ Y then
            {{                         }} ->>
            {{                         }}
    Z := Y - X
            {{                         }}
  else
            {{                         }} ->>
            {{                         }}
    Y := X + Z
            {{                         }}
  end
{{ Y = X + Z }}

{{ True }}
  if X ≤ Y then
       {{ True ∧ X ≤ Y }} ->>
       {{ Y = X + (Y - X) }}
    Z := Y - X
       {{ Y = X + Z }}
  else
       {{ True ∧ ¬(X ≤ Y) }} ->>
       {{ X + Z = X + Z }}
    Y := X + Z
       {{ Y = X + Z }}
  end
{{ Y = X + Z }}

6.1.3. Example: Reduce to Zero🔗

Here is a while loop that is so simple that True suffices as a loop invariant.

(1)    {{ True }}
         while X ≠ 0 do
(2)                  {{ True ∧ X ≠ 0 }} ->>
(3)                  {{ True }}
           X := X - 1
(4)                  {{ True }}
         end
(5)    {{ True ∧ ¬(X ≠ 0) }} ->>
(6)    {{ X = 0 }}

The decorations can be constructed as follows:

• Start with the outer precondition (1) and postcondition (6).

• Following the format dictated by the hoare_while rule, we copy (1) to (4). We conjoin (1) with the guard to obtain (2). We also conjoin (1) with the negation of the guard to obtain (5).

• Because the final postcondition (6) does not syntactically match (5), we add an implication between them.

• Using the assignment rule with assertion (4), we trivially substitute and obtain assertion (3).

• We add the implication between (2) and (3).

Finally we check that the implications do hold; both are trivial.

6.1.4. Example: Division🔗

Let's do one more example of simple reasoning about a loop.

The following Imp program calculates the integer quotient and remainder of parameters m and n.

X := m;
Y := 0;
while n ≤ X do
  X := X - n;
  Y := Y + 1
end;

If we replace m and n by concrete numbers and execute the program, it will terminate with the variable X set to the remainder when m is divided by n and Y set to the quotient.

In order to give a specification to this program we need to remember that dividing m by n produces a remainder X and a quotient Y such that n * Y + X = m ∧ X < n.

It turns out that we get lucky with this program and don't have to think very hard about the loop invariant: the loop invariant is just the first conjunct, n * Y + X = m, and we can use this to decorate the program.

 (1)  {{ True }} ->>
 (2)  {{ n * 0 + m = m }}
        X := m;
 (3)                     {{ n * 0 + X = m }}
        Y := 0;
 (4)                     {{ n * Y + X = m }}
        while n ≤ X do
 (5)                     {{ n * Y + X = m ∧ n ≤ X }} ->>
 (6)                     {{ n * (Y + 1) + (X - n) = m }}
          X := X - n;
 (7)                     {{ n * (Y + 1) + X = m }}
          Y := Y + 1
 (8)                     {{ n * Y + X = m }}
        end
 (9)  {{ n * Y + X = m ∧ ¬ (n ≤ X) }} ->>
(10)  {{ n * Y + X = m ∧ X < n }}

Assertions (4), (5), (8), and (9) are derived mechanically from the loop invariant and the loop's guard. Assertions (8), (7), and (6) are derived using the assignment rule going backwards from (8) to (6). Assertions (4), (3), and (2) are again backwards applications of the assignment rule.

Now that we've decorated the program it only remains to check that the uses of the consequence rule are correct — i.e., that (1) implies (2), that (5) implies (6), and that (9) implies (10). This is indeed the case:

• (1) ->> (2): trivial, by algebra.

• (5) ->> (6): because n ≤ X, we are guaranteed that the subtraction in (6) does not get zero-truncated. We can therefore rewrite (6) as n * Y + n + X - n and cancel the ns, which results in the left conjunct of (5).

• (9) ->> (10): if ¬ (n ≤ X) then X < n. That's straightforward from high-school algebra. So, we have a valid decorated program.

6.1.5. From Decorated Programs to Formal Proofs🔗

From an informal proof in the form of a decorated program, it is "easy in principle" to read off a formal proof using the Lean theorems corresponding to the Hoare Logic rules, but these proofs can be a bit long and fiddly.

Note that we do not unfold the definition of ValidHoareTriple anywhere in this proof: the point of the game we're playing now is to use the Hoare rules as a self-contained logic for reasoning about programs.

For example...

In Hoare we introduced a series of tactics named assertion_auto to automate proofs involving assertions.

The following declaration introduces a more sophisticated tactic that will help with proving assertions throughout the rest of this chapter. You don't need to understand the details, but briefly: it introduces the available hypotheses, simplifies assertions, maps, and arithmetic expressions, and then asks lia to solve linear arithmetic goals. What's left after verify_assertion does its work should be just the "interesting parts" of the proof (which, if we're lucky, might be nothing at all!).

This makes it pretty easy to verify reduce_to_zero:

This example shows that it is conceptually straightforward to read off the main elements of a formal proof from a decorated program. Indeed, the process is so straightforward that it can be automated, as we will see next.

6.2.1. Syntax🔗

The first thing we need to do is to formalize a variant of the syntax of Imp commands that includes embedded assertions, which we'll call "decorations." We call the new commands decorated commands, or dcoms.

The choice of exactly where to put assertions in the definition of dcom is a bit subtle. The simplest thing to do would be to annotate every dcom with a precondition and postcondition — something like this...

But this would result in very verbose decorated programs with a lot of repeated annotations: a simple program like skip;skip would be decorated like this,

{{p}} ({{p}} skip {{p}}) ; ({{p}} skip {{p}}) {{p}}

with pre- and post-conditions around each skip, plus identical pre- and post-conditions on the semicolon!

In other words, we don't want both preconditions and postconditions on each command, because a sequence of two commands would contain redundant decorations — the postcondition of the first likely being the same as the precondition of the second.

Instead, our formal syntax of decorated commands will omit preconditions whenever possible and embed just postconditions.

• The skip command, for example, is decorated only with its postcondition

skip {{ q }}

on the assumption that the precondition will be provided by somebody else.

We carry the same assumption through the other syntactic forms: each decorated command is assumed to carry its own postcondition within itself but take its precondition from its context in which it is used.

• Sequences d₁ ; d₂ need no additional decorations.

Why?

Because inside d₂ there will be a postcondition, which also serves as the postcondition of d₁;d₂.

Similarly, inside d₁ there will also be a postcondition, which additionally serves as the precondition for d₂.

• An assignment X := a is decorated only with its postcondition:

X := a {{ q }}

• A conditional if b then d₁ else d₂ is decorated with a postcondition for the entire statement, as well as preconditions for each branch:

if b then {{ p₁ }} d₁ else {{ p₂ }} d₂ end {{ q }}

• A loop while (b) {d} is decorated with its final postcondition plus a precondition for the body:

while (b) {{ p }} { d } {{ q }}

The postcondition embedded in d serves as the loop invariant.

• Implications ->> can be added as decorations either for a precondition...

->> {{ p }} d

...or for a postcondition:

d ->> {{ q }}

The former is waiting for another precondition to be supplied by the context; the latter relies on the postcondition already embedded in d.

Putting this all together gives us the formal syntax of decorated commands:

Lean keeps decorated-command notation in its own syntax category, dcom, so it can coexist with the ordinary Imp command syntax.

To provide the initial precondition that goes at the very top of a decorated program, we introduce a new type decorated:

To inspect the fully elaborated term behind this notation, put set_option pp.all true in before a #check or #print command.

The formal definitions can use either constructors directly or the decorated-command notation introduced above.

An example decorated program that decrements X to 0:

It is easy to go from a dcom to a com by erasing all annotations.

It is also straightforward to extract the precondition and postcondition from a decorated program.

It would be nice to use <{ ... }> notations
in this definition and the ones below...
     | <{ skip {{p}} }>        => p
     | <{ _; d₂ }>             => post d₂
     | <{ _ := _ {{q}} }>      => q

We can then express what it means for a decorated program to be correct as follows:

For example:

The outer Hoare triple of a decorated program is just a Prop; thus, to show that it is valid, we need to produce a proof of this proposition.

We will do this by extracting "proof obligations" from the decorations sprinkled throughout the program.

These obligations are often called verification conditions, because they are the facts that must be verified to see that the decorations are locally consistent and thus constitute a proof of validity of the outer triple.

6.2.2. Extracting Verification Conditions🔗

The function DCom.VerificationConditions takes a decorated command d together with a precondition p and returns a proposition that, if it can be proved, implies that the triple

{{p}} d.erase {{d.postcondition}}

is valid.

It does this by walking over d and generating a big conjunction that includes

• local consistency checks for each form of command, plus

• uses of ->> to bridge the gap between the assertions found inside a decorated command and the assertions imposed by the external precondition; these uses correspond to applications of the consequence rule.

Local consistency is defined as follows...

• The decorated command

skip {{q}}

is locally consistent with respect to a precondition p if p ->> q.

• The sequential composition of d₁ and d₂ is locally consistent with respect to p if d₁ is locally consistent with respect to p and d₂ is locally consistent with respect to the postcondition of d₁.

• An assignment

X := a {{q}}

is locally consistent with respect to a precondition p if:

p ->> q [X ↦ a]

• A conditional

if b then {{p₁}} d₁ else {{p₂}} d₂ end {{q}}

is locally consistent with respect to precondition p if

(1) p ∧ b ->> p₁

(2) p ∧ b ->> p₂

(3) d₁ is locally consistent with respect to p₁

(4) d₂ is locally consistent with respect to p₂

(5) d₁.postcondition ->> q

(6) d₂.postcondition ->> q

• A loop

while (b) {{{q}} d} {{r}}

is locally consistent with respect to precondition p if:

(1) p ->> d.postcondition

(2) d.postcondition ∧ b ->> q

(3) d.postcondition ∧ b ->> r

(4) d is locally consistent with respect to q

• A command with an extra assertion at the beginning

->> {{q}} d

is locally consistent with respect to a precondition p if:

(1) p ->> q

(2) d is locally consistent with respect to q

• A command with an extra assertion at the end

d ->> {{q}}

is locally consistent with respect to a precondition p if:

(1) d is locally consistent with respect to p

(2) d.postcondition ->> q

With all this in mind, we can write a verification condition generator that takes a decorated command and reads off a proposition saying that all its decorations are locally consistent.

Formally, since a decorated command is "waiting for its precondition" the main VC generator takes a dcom plus a given precondition as arguments.

The following key theorem states that DCom.VerificationConditions does its job correctly. Not surprisingly, each of the Hoare Logic rules plays a critical role at some point in the proof.

Now that all the pieces are in place, we can define what it means to verify an entire program.

And this brings us to the main theorem of this section:

6.2.3. More Automation🔗

The propositions generated by DCom.VerificationConditions are fairly big and contain many conjuncts that are essentially trivial.

HIDE: MRC'20: The conditions here used to be just [Eval]ed instead
of being duplicated in a comment.  They were actually incorrect
because of changes to notation.  Putting them in as an [Example]
will force us to keep them up-to-date. APT20: Yes, but but stating
this an equality completely misses the point about verify_assertion! So I
changed things back.

Fortunately, our verify_assertion tactic can generally take care of most (or sometimes all) of them.

To automate the overall process of verification, we can use verification_correct to extract the verification conditions, use verify_assertion to verify them as much as it can, and finally tidy up any remaining bits by hand.

Here's the final, formal proof that decWhile is correct.

Similarly, here is the formal decorated program for the "swapping by adding and subtracting" example that we saw earlier.

And here is the formal decorated version of the "positive difference" program from earlier:

6.3.1. Example: Slow Subtraction🔗

The following program subtracts the value of X from the value of Y by repeatedly decrementing both X and Y. We want to verify its correctness with respect to the pre- and postconditions shown:

{{ X = m ∧ Y = n }}
  while X ≠ 0 do
    Y := Y - 1;
    X := X - 1
  end
{{ Y = n - m }}

To verify this program, we need to find an invariant Inv for the loop. As a first step we can leave Inv as an unknown and build a skeleton for the proof by applying the rules for local consistency, working from the end of the program to the beginning, as usual, and without doing any thinking at all yet.

This leads to the following skeleton:

(1)    {{ X = m ∧ Y = n }}  ->>                   (a)
(2)    {{ Inv }}
         while X ≠ 0 do
(3)              {{ Inv ∧ X ≠ 0 }}  ->>          (c)
(4)              {{ Inv [X ↦ X-1] [Y ↦ Y-1] }}
           Y := Y - 1;
(5)              {{ Inv [X ↦ X-1] }}
           X := X - 1
(6)              {{ Inv }}
         end
(7)    {{ Inv ∧ ¬ (X ≠ 0) }}  ->>                (b)
(8)    {{ Y = n - m }}

Examining this skeleton, we can see that any valid Inv will have to respect three conditions:

• (a) it must be weak enough to be implied by the loop's precondition, i.e., (1) must imply (2);

• (b) it must be strong enough to imply the program's postcondition, i.e., (7) must imply (8);

• (c) it must be preserved by a single iteration of the loop, assuming that the loop guard also evaluates to true, i.e., (3) must imply (4).

These conditions are actually independent of the particular program and specification we are considering: every loop invariant has to satisfy them.

One way to find a loop invariant that simultaneously satisfies these three conditions is by using an iterative process: start with a "candidate" invariant (e.g., a guess or a heuristic choice) and check the three conditions above; if any of the checks fails, try to use the information that we get from the failure to produce another — hopefully better — candidate invariant, and repeat.

For instance, in the reduce-to-zero example above, we saw that, for a very simple loop, choosing True as a loop invariant did the job. Maybe it will work here too. To find out, let's try instantiating Inv with True in the skeleton above and see what we get...

(1)    {{ X = m ∧ Y = n }} ->>                    (a - OK)
(2)    {{ True }}
         while X ≠ 0 do
(3)                   {{ True ∧ X ≠ 0 }} ->>     (c - OK)
(4)                   {{ True }}
           Y := Y - 1;
(5)                   {{ True }}
           X := X - 1
(6)                   {{ True }}
         end
(7)    {{ True ∧ ¬(X ≠ 0) }} ->>                 (b - WRONG!)
(8)    {{ Y = n - m }}

While conditions (a) and (c) are trivially satisfied, (b) is wrong: it is not the case that True ∧ X = 0 (7) implies Y = n - m (8). In fact, the two assertions are completely unrelated, so it is very easy to find a counterexample to the implication (say, Y = X = m = 0 and n = 1).

If we want (b) to hold, we need to strengthen the loop invariant so that it implies the postcondition (8). One simple way to do this is to let the loop invariant be the postcondition. So let's return to our skeleton, instantiate Inv with Y = n - m, and try checking conditions (a) to (c) again.

(1)    {{ X = m ∧ Y = n }} ->>                        (a - WRONG!)
(2)    {{ Y = n - m }}
         while X ≠ 0 do
(3)                     {{ Y = n - m ∧ X ≠ 0 }} ->>  (c - WRONG!)
(4)                     {{ Y - 1 = n - m }}
           Y := Y - 1;
(5)                     {{ Y = n - m }}
           X := X - 1
(6)                     {{ Y = n - m }}
         end
(7)    {{ Y = n - m ∧ ¬(X ≠ 0) }} ->>                (b - OK)
(8)    {{ Y = n - m }}

This time, condition (b) holds trivially, but (a) and (c) are broken. Condition (a) requires that (1) X = m ∧ Y = n implies (2) Y = n - m. If we substitute Y by n we have to show that n = n - m for arbitrary m and n, which is not the case (for instance, when m = n = 1). Condition (c) requires that n - m - 1 = n - m, which fails, for instance, for n = 1 and m = 0. So, although Y = n - m holds at the end of the loop, it does not hold from the start, and it doesn't hold on each iteration; it is not a correct loop invariant.

This failure is not very surprising: the variable Y changes during the loop, while m and n are constant, so the assertion we chose didn't have much chance of being a loop invariant!

To do better, we need to generalize (7) to some statement that is equivalent to (8) when X is 0, since this will be the case when the loop terminates, and that "fills the gap" in some appropriate way when X is nonzero. Looking at how the loop works, we can observe that X and Y are decremented together until X reaches 0. So, if X = 2 and Y = 5 initially, after one iteration of the loop we obtain X = 1 and Y = 4; after two iterations X = 0 and Y = 3; and then the loop stops. Notice that the difference between Y and X stays constant between iterations: initially, Y = n and X = m, and the difference is always n - m. So let's try instantiating Inv in the skeleton above with Y - X = n - m.

(1)    {{ X = m ∧ Y = n }} ->>                            (a - OK)
(2)    {{ Y - X = n - m }}
         while X ≠ 0 do
(3)                    {{ Y - X = n - m ∧ X ≠ 0 }} ->>   (c - OK)
(4)                    {{ (Y - 1) - (X - 1) = n - m }}
           Y := Y - 1;
(5)                    {{ Y - (X - 1) = n - m }}
           X := X - 1
(6)                    {{ Y - X = n - m }}
         end
(7)    {{ Y - X = n - m ∧ ¬(X ≠ 0) }} ->>                (b - OK)
(8)    {{ Y = n - m }}

Success! Conditions (a), (b) and (c) all hold now. (To verify (c), we need to check that, under the assumption that X ≠ 0, we have Y - X = (Y - 1) - (X - 1); this holds for all natural numbers X and Y.)

Here is the final version of the decorated program:

6.3.2. Exercise: Slow Assignment🔗

6.3.3. Example: Parity🔗

Here is a cute way of computing the parity of a value initially stored in X, due to Daniel Cristofani.

{{ X = m }}
  while 2 ≤ X do
    X := X - 2
  end
{{ X = parity m }}

The parity function used in the specification is defined in Lean as follows:

The postcondition does not hold at the beginning of the loop, since m = parity m does not hold for an arbitrary m, so we cannot hope to use that as a loop invariant. To find a loop invariant that works, let's think a bit about what this loop does. On each iteration it decrements X by 2, which preserves the parity of X. So the parity of X does not change, i.e., it is invariant. The initial value of X is m, so the parity of X is always equal to the parity of m. Using parity X = parity m as an invariant we obtain the following decorated program:

{{ X = m }} ->>                                         (a - OK)
{{ parity X = parity m }}
  while 2 ≤ X do
               {{ parity X = parity m ∧ 2 ≤ X }} ->>  (c - OK)
               {{ parity (X-2) = parity m }}
    X := X - 2
               {{ parity X = parity m }}
  end
{{ parity X = parity m ∧ ¬(2 ≤ X) }} ->>              (b - OK)
{{ X = parity m }}

With this loop invariant, conditions (a), (b), and (c) are all satisfied. For verifying (b), we observe that, when X < 2, we have parity X = X (we can easily see this in the definition of parity). For verifying (c), we observe that, when 2 ≤ X, we have parity X = parity (X-2).

HIDE: A more complexly phrased loop invariant for the same program
[[
        {{ X = m }}  ->>                        (a - OK)
        {{ ev X <-> ev m }}
      while 2 ≤ X do
          {{ ev X <-> ev m ∧ 2 ≤ X }}  ->>    (c - OK)
          {{ ev (X-2) <-> ev m }}
        X := X - 2
          {{ ev X <-> ev m }}
      end
        {{ (ev X <-> ev m) ∧ ~(2 ≤ X) }}  ->>     (b - OK)
        {{ X=0 <-> ev m }}
]]

HIDE: find_parity'_dec; more complicated phrasing of invariant
there is very little resemblance between the invariant and the
postcondition -- the implication is also non-obvious, and the
X ≤ m condition makes the invariant more complicated
[[
 {{ X = m }} ->>
 {{ X ≤ m ∧ ev (m - X) }}
while 2 ≤ X do
   {{ X ≤ m ∧ ev (m - X) ∧ 2 ≤ X }} ->>
   {{ X - 2 ≤ m ∧ ev (m - (X - 2)) }}
 X := X - 2
   {{ X ≤ m ∧ ev (m - X) }}
end
 {{ X ≤ m ∧ ev (m - X) ∧ ~(2 ≤ X) }} ->>
 {{ X=0 <-> ev m }}
]]