Scalable SPARK Proofs

Introduction

In a recent Ada SPARK project, I needed a function to count characters in a buffer. To be more specific, I needed a function that, given an input buffer, returns an array (indexed by characters) that counts the number of occurrences of each character in the input buffer.

For people not familiar with SPARK, it is a subset of Ada that includes support for deductive formal verification. In other words, it allows software developers to write code that can be formally proven to be absent of runtime errors (SPARK Silver) and even to be functionally correct (SPARK Gold).

This function is part of a larger project, and I needed a strong proof of correctness for this function. Simply proving the absence of runtime errors is not sufficient in this case. I needed SPARK Gold to satisfy my proof in the wider project. The formal methods engine behind SPARK builds proofs from the ground up, and this function is in one of the lower layers of my project. My plan is to provide more information about the larger project in a later blog post.

The following blog post goes into a lot of detail to first prove the absence of runtime errors and then prove a stronger post-condition for the function so that we can build the rest of the program on top of it. Building this proof is additional work for the developer; however, the payback in the later parts of the software development cycle is significant. A mathematically proven implementation reduces the amount of defects found during testing, and maintenance of this software will be a breeze. Typically, the only defects are due to problems in the requirements, not the actual implementation.

I tried to provide lots of detail with the intent that this blog post serves as a guideline to help you write better proofs yourself.

Declarations

The declarations for my function Char_Counts in SPARK is straight forward:

package Counts
 with SPARK_Mode
is

  Max_Size : constant := 1024;

  type Int32 is range 0 .. 2**31 - 1;
  subtype Length is Int32 range 0 .. Max_Size;

  subtype Index is Length range 1 .. Max_Size;

  type Buffer is array (Index range <>) of Character;

  type Counts_Array is array (Character) of Length;

  function Char_Counts (Input : Buffer) return Counts_Array;

end Counts;

The implementation of Char_Counts is equally straightforward:

package body Counts with SPARK_Mode is

  function Char_Counts (Input : Buffer) return Counts_Array is
     Counts : Counts_Array := [others => 0];
  begin
     for I in Input'Range loop
        Counts (Input (I)) := Counts (Input (I)) + 1;
     end loop;
     return Counts;
  end Char_Counts;

end Counts;

You can find the entire code of this project here: https://github.com/kanigsson/counts

Proving the Absence of Runtime Errors

Proving the absence of run-time errors is simple. We have to show that the increment Counts (Input (I)) + 1 does not overflow. To achieve that,  it is enough to show that we cannot exceed the length of the array for each character. We can introduce a loop invariant for this:

  function Char_Counts (Input : Buffer) return Counts_Array is
     Counts : Counts_Array := [others => 0];
  begin
     for I in Input'Range loop
        pragma Loop_Invariant (for all C in Character =>
                              Counts (C) <= I - Input'First);
        Counts (Input (I)) := Counts (Input (I)) + 1;
     end loop;
     return Counts;
  end Char_Counts;

(All SPARK proofs in this blog post are done at level 2 with this command: gnatprove --level=2)

This is a great first step, but for the larger program, we need a stronger proof.

Introducing a Post Condition

My larger project needs more information about the array of counts. With the loop invariant so far, we will only be able to prove that the array doesn’t contain entries larger than the length of the input buffer, Input’Length. But based on this invariant, each cell of the result array might contain this maximum value.

In reality, this can’t happen, and the sum of all values of the array of character counts can’t exceed Input’Length. This property is what I need to prove the next step in my larger project. We can introduce this property as a post condition to Char_Counts and then start our work to prove that the post condition always holds.

To prove this in SPARK, we first need a Sum function. A common approach to prove properties is to use induction, so we will implement the core logic in a recursive helper function that sums up to a certain character. We can introduce this Sum function as a Ghost function, a function that is only present to assist the proof engines:

  function Sum (Arr : Counts_Array; Up_To : Character) return Int32
  is (if Up_To = Character'First
      then Arr (Up_To)
      else Arr (Up_To) + Sum (Arr, Character'Pred (Up_To)))
  with
    Ghost,
    Subprogram_Variant => (Decreases => Up_To),
    Post               =>
      Sum'Result <= Length'Last * (Character'Pos (Up_To) + 1);

  function Sum (Arr : Counts_Array) return Int32
  is (Sum (Arr, Character'Last))
  with Ghost;

  function Char_Counts (Input : Buffer) return Counts_Array
  with Post => Sum (Char_Counts'Result) = Input'Length;

A quick note on preventing overflow in Sum: we use Int32 as the return type to safely hold the result even in the worst case. The postcondition is essential for bounding the size of the recursive call's result, which in turn allows SPARK to prove the absence of overflow.

First Step In Proving The Post Condition

Now we need to prove that the sum of the counts array in our loop progresses as intended. A logical invariant to introduce is that the sum of all the counts of the characters is equal to the length of the array that we have processed

     for I in Input'Range loop
        pragma
          Loop_Invariant
            (for all C in Character => Counts (C) <= I - Input'First);
        pragma Loop_Invariant (Sum (Counts) = I - Input'First);
        Counts (Input (I)) := Counts (Input (I)) + 1;
     end loop;

Unfortunately, SPARK needs more assistance and reports two issues for the new loop invariant:

counts.adb:11:33: medium: loop invariant might not be preserved by an arbitrary iteration
counts.adb:11:33: medium: loop invariant might fail in first iteration

In other words, SPARK can’t figure out that the sum of the counts is zero at the start, and that adding 1 to some cell increases the sum by one. We need to help it with each of these. Both these are typical starting points in a SPARK proof for a loop over an array.

In both cases, we must use lemmas to help the provers. For those unfamiliar, lemmas are not a built-in feature of SPARK but a powerful convention: they are typically Ghost procedures with no global outputs, often named with "Lem" or "Lemma." They act as more powerful assertions, breaking the main proof into smaller, verifiable parts.

Lemma 1: The Initial Iteration

To prove the sum is zero at the start, we define a lemma that shows an array initialized to all zeros has a zero sum:

  procedure Lem_Sum_Zero (Arr : Counts_Array; Up_To : Character)
  with
    Ghost,
    Global             => null,
    Subprogram_Variant => (Decreases => Up_To),
    Pre                =>
      (for all C in Character'First .. Up_To => Arr (C) = 0),
    Post               => Sum (Arr, Up_To) = 0;

To break things down, we can see that, as I said, this is a ghost procedure with no global outputs. The precondition states that the input array is all zeros. The post states that the sum (up to Up_To) is also zero. The Up_To argument helps us with the induction, as we will explain shortly.

The next step is to prove the lemma. In some cases, just writing a null procedure works (always try this first):

  procedure Lem_Sum_Zero (Arr : Counts_Array; Up_To : Character) is
  begin
     null;
  end Lem_Sum_Zero;

But in this case it is not as simple. We need to help gnatprove to do the proof by induction. Looking at the definition of Sum, the proof is simple if Up_To is the first character. When Up_To is any other character, we can use the proof for a smaller Up_To to prove the property for our own Up_To:

 procedure Lem_Sum_Zero (Arr : Counts_Array; Up_To : Character) is
  begin
     if Up_To = Character'First then
        return;
     else
        Lem_Sum_Zero (Arr, Character'Pred (Up_To));
     end if;
  end Lem_Sum_Zero;

Simply writing return in the if case is a way of saying “I trust SPARK can figure this case out on its own”. Similarly, in the else case we just provide the induction hypothesis, and let SPARK figure out itself how to connect the pieces. The lemma code provides the “skeleton” of the proof in a way.

This is why we have this Up_To argument in the lemma (and the Sum function in the first place): it is a way to write inductive lemmas like the above. The Subprogram_Variant annotation shows that the induction eventually reaches the “bottom”.

Writing lemmas like this requires some experience and practice. The above “scheme” works in many cases, and we will use it later for our second lemma.

The last step is actually using the lemma at the place where we need it:

  function Char_Counts (Input : Buffer) return Counts_Array is
     Counts : Counts_Array := [others => 0];
  begin
     Lem_Sum_Zero (Counts, Character'Last);
     for I in Input'Range loop
	 ...

Invoking a lemma is as simple as calling the ghost procedure with the arguments that make sense in our context. The proof of the first iteration of the loop invariant is now proved, and the other one still remains:

counts.adb:30:33: medium: loop invariant might not be preserved by an arbitrary iteration

Lemma 2: Preserving the Invariant

To prove the case where we add 1 to a cell in the array, in principle, it works the same way. However, when I attempted this, I ran into an issue, and I worked with my colleagues in the SPARK team to fix it.

My First Attempt

Here is my first version of the lemma:

  function Incr (Arr : Counts_Array; Pos : Character) return Counts_Array
  is (Arr with delta Pos => Arr (Pos) + 1)
  with
    Ghost,
    Pre  => Arr (Pos) < Length'Last;

  procedure Lem_Incr_Neq (Arr : Counts_Array; Up_To, Pos : Character)
  with
    Ghost,
    Global             => null,
    Subprogram_Variant => (Decreases => Up_To),
    Pre                => Pos <= Up_To and then Arr (Pos) < Length'Last,
    Post               => Sum (Incr (Arr, Pos), Up_To) = Sum (Arr, Up_To) + 1;

We first define a helper function Incr to increment a position in an array. It’s a common pattern to write functional (side-effect free) variants of imperative code for proof, to be able to more easily talk about the “before” and “after” of a state mutation. Then we define the lemma.

To prove this lemma, it turns out there are in fact two cases: when the count includes the modified cell, and when it doesn’t (remember that we have this Up_To argument which restricts the sum to a prefix of the full array). While the precondition of the lemma restricts us to the former case, while doing the inductive proof, we may fall out of this case. So we need another lemma that helps us when the count excludes the modified cell:

  procedure Lem_Incr_Eq (Arr : Counts_Array; Up_To, Pos : Character)
  with
    Ghost,
    Global             => null,
    Subprogram_Variant => (Decreases => Up_To),
    Pre                => Pos > Up_To and then Arr (Pos) < Length'Last,
    Post               => Sum (Incr (Arr, Pos), Up_To) = Sum (Arr, Up_To);

Proving these lemmas is quite simple and uses the previously introduced style of providing the proof skeleton:

  procedure Lem_Incr_Eq (Arr : Counts_Array; Up_To, Pos : Character) is
  begin
     if Up_To = Character'First then
        return;
     else
        Lem_Incr_Eq (Arr, Character'Pred (Up_To), Pos);
     end if;
  end Lem_Incr_Eq;

  procedure Lem_Incr_Neq (Arr : Counts_Array; Up_To, Pos : Character) is
     Tmp : Counts_Array := Incr (Arr, Pos);
  begin
     if Up_To = Pos then
        if Up_To = Character'First then
           return;
        else
           Lem_Incr_Eq (Arr, Character'Pred (Up_To), Pos);
        end if;
     else
        Lem_Incr_Neq (Arr, Character'Pred (Up_To), Pos);
     end if;
  end Lem_Incr_Neq;

The only tricky part is that in the Neq case, when recursing to the previous character, we might fall into the case where the sum isn’t modified anymore, and we need to use the Eq lemma in that case.

Now we can use the lemma in our loop:

     for I in Input'Range loop
 	 ...
        pragma Loop_Invariant (Sum (Counts) = I - Input'First);
        Lem_Incr_Neq (Counts, Character'Last, Input (I));
        Counts (Input (I)) := Counts (Input (I)) + 1;
     end loop;

And … the above doesn’t work, the loop invariant is still unproved.

The reason is that SPARK needs to prove that `Incr (Counts)` (the functional variant) and Counts after the imperative increment are not only equal in the Ada sense (same length and same elements), but indistinguishable. Basically, the problem is that we have these two different arrays, and it’s hard for SPARK to prove they are equal.

The corrected version using a relational style

To fix this issue, I discussed with my colleagues and the solution is to avoid having this extra array that is created by the Incr function. Instead of creating a new array, it is better to relate the existing arrays, transforming the functional style into a relational style:

  function Is_Incr (Arr1, Arr2 : Counts_Array; Pos : Character) return Boolean
  is (for all C in Character =>
        (if C = Pos then Arr1 (C) + 1 = Arr2 (C) else Arr1 (C) = Arr2 (C)));

  procedure Lem_Incr_Eq (Arr1, Arr2 : Counts_Array; Up_To, Pos : Character)
  with
    Ghost,
    Global             => null,
    Subprogram_Variant => (Decreases => Up_To),
    Pre                =>
      Pos > Up_To
      and then Arr1 (Pos) < Length'Last
      and then Is_Incr (Arr1, Arr2, Pos),
    Post               => Sum (Arr2, Up_To) = Sum (Arr1, Up_To);

  procedure Lem_Incr_Neq (Arr1, Arr2 : Counts_Array; Up_To, Pos : Character)
  with
    Ghost,
    Global             => null,
    Subprogram_Variant => (Decreases => Up_To),
    Pre                =>
      Pos <= Up_To
      and then Arr1 (Pos) < Length'Last
      and then Is_Incr (Arr1, Arr2, Pos),
    Post               => Sum (Arr2, Up_To) = Sum (Arr1, Up_To) + 1;

The proofs (implementations) of the lemmas (lemma procedures) have minimal changes, just to account for the change in signature.

The full implementation of the function with the loop now looks like this.

  function Char_Counts (Input : Buffer) return Counts_Array is
     Counts : Counts_Array := [others => 0];
     Tmp    : Counts_Array := Counts with Ghost;
  begin
     Lem_Sum_Zero (Counts, Character'Last);
     for I in Input'Range loop
        pragma
          Loop_Invariant
            (for all C in Character => Counts (C) <= I - Input'First);
        pragma Loop_Invariant (Sum (Counts) = I - Input'First);
        Tmp := Counts;
        Counts (Input (I)) := Counts (Input (I)) + 1;
        Lem_Incr_Neq (Tmp, Counts, Character'Last, Input (I));
     end loop;
     return Counts;
  end Char_Counts;

We need to introduce another ghost variable to capture the state of the counts array before incrementing it, then call the Lem_Incr_Neq procedure with the appropriate arguments.

And we can now add the desired postcondition:

  function Char_Counts (Input : Buffer) return Counts_Array
  with Post =>
    (Sum (Char_Counts'Result) = Input'Length);

And the proof is complete.

Another variant using logical equality

As I said before, the problem with my failed attempt was that SPARK couldn’t prove that the functional and imperative way of “incrementing” the array both yield arrays that are indistinguishable. But there is a way to tell SPARK that they are. First one needs to create a logical equality for the array type:

  function Logic_Eq (X, Y : Counts_Array) return Boolean
  is (X'First = Y'First and X'Last = Y'Last and X = Y)
  with Annotate => (GNATprove, Logical_Equal);

The special annotation tells SPARK to use this function as a logical equality function for the type Counts_Array. Then we can simply state that the two ways to increment the array are equal, in our loop (see the assertion at the end of the loop):

     for I in Input'Range loop
        pragma
          Loop_Invariant
            (for all C in Character => Counts (C) <= I - Input'First);
        pragma Loop_Invariant (Sum (Counts) = I - Input'First);
        Lem_Incr_Neq (Counts, Character'Last, Input (I));
        Tmp := Counts;
        Counts (Input (I)) := Counts (Input (I)) + 1;
        pragma Assert (Logic_Eq (Incr (Tmp, Input (I)), Counts));
     end loop;

This technique of using ghost code to prove “real” code is called “auto-active verification”, which is a portmanteau word expressing the fact that this style is a mix of “automated verification” (using the automated provers coming with SPARK) and “interactive verification” (in the style of proof assistants such as Lean or Rocq). It is a powerful technique that often helps with more complex proof cases and is a good technique to master to truly become an expert in SPARK.

Conclusion

Some effort is required to help the formal methods engine mathematically prove a) the absence of runtime errors and b) functional correctness.

The first step, the absence of runtime errors, is the easiest. In this case, it required making sure there were no array overruns and helping the engine understand that.

The second step typically requires more thought and requires that the developer help the proof engine to construct the steps that logically connect the implementation to the post-condition. Lemmas and Ghost code are a convenient tool to help the developer guide the proof engine. Still, as this post demonstrates, how you write the Lemmas matters.

If you are looking for assistance, there are many ways to ask other experts for help. If you are an AdaCore customer, then AdaCore support is available for an engineer-to-engineer discussion on how to get to the proof you need. If not, there are several open-source communities available for assistance as well.