AdaCore Blog

VerifyThis Challenge in SPARK

by Yannick Moy –

This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure.

I am going to use this challenge to show how one can reach different levels of software assurance with SPARK. I'm referring here to the five levels of software assurance that we have used in our guidance document with Thales:

  • Stone level - valid SPARK
  • Bronze level - initialization and correct data flow
  • Silver level - absence of run-time errors (AoRTE)
  • Gold level - proof of key integrity properties
  • Platinum level - full functional proof of requirements

Stone level - valid SPARK

We start with a simple translation in Ada of the simplified variant of pair insertion sort given in page 2 of the challenge sheet:

package Pair_Insertion_Sort with
  SPARK_Mode
is
   subtype Index is Integer range 0 .. Integer'Last-1;
   type Arr is array (Index range <>) of Integer
     with Predicate => Arr'First = 0;

   procedure Sort (A : in out Arr);

end Pair_Insertion_Sort;

package body Pair_Insertion_Sort with
  SPARK_Mode
is
   procedure Sort (A : in out Arr) is
      I, J, X, Y, Z : Integer;
   begin
      I := 0;
      while I < A'Length-1 loop
         X := A(I);
         Y := A(I+1);
         if X < Y then
            Z := X;
            X := Y;
            Y := Z;
         end if;

         J := I - 1;
         while J >= 0 and then A(J) > X loop
            A(J+2) := A(J);
            J := J - 1;
         end loop;
         A(J+2) := X;

         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            J := J - 1;
         end loop;
         A(J+1) := Y;
         I := I+2;
      end loop;

      if I = A'Length-1 then
         Y := A(I);
         J := I - 1;
         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            J := J - 1;
         end loop;
         A(J+1) := Y;
      end if;
   end Sort;

end Pair_Insertion_Sort;

Stone level is reached immediately on this code, as it is in the SPARK subset of Ada.

Bronze level - initialization and correct data flow

Bronze level is also reached immediately, although the flow analysis in SPARK detected a problem the first time I ran it:

pair_insertion_sort.adb:35:39: medium: "Y" might not be initialized
pair_insertion_sort.adb:39:20: medium: "Y" might not be initialized

The problem was that the line initializing Y to A(I) near the end of the program was missing from my initial version. As I copied the algorithm in pseudo-code from the PDF and removed the comments in the badly formatted result, I also removed that line of code! After restoring that line, flow analysis did not complain anymore, I had reached Bronze level.

Silver level - absence of run-time errors (AoRTE)

Then comes Silver level, which was suggested as an initial goal in the challenge: proving absence of runtime errors. As the main reason for run-time errors in this code is the possibility of indexing outside of array bounds, we need to provide bounds for the values of variables I and J used to index A. As these accesses are performed inside loops, we need to do so in loop invariants. Exactly 5 loop invariants are needed here, and with these GNATprove can prove the absence of run-time errors in the code in 7 seconds on my machine:

package body Pair_Insertion_Sort with
  SPARK_Mode
is
   procedure Sort (A : in out Arr) is
      I, J, X, Y, Z : Integer;
   begin
      I := 0;
      while I < A'Length-1 loop
         X := A(I);
         Y := A(I+1);
         if X < Y then
            Z := X;
            X := Y;
            Y := Z;
         end if;

         J := I - 1;
         while J >= 0 and then A(J) > X loop
            A(J+2) := A(J);
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            J := J - 1;
         end loop;
         A(J+2) := X;

         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            J := J - 1;
         end loop;
         A(J+1) := Y;

         pragma Loop_Invariant (I in 0 .. A'Length-2);
         pragma Loop_Invariant (J in -1 .. A'Length-3);
         I := I+2;
      end loop;

      if I = A'Length-1 then
         Y := A(I);
         J := I - 1;
         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            pragma Loop_Invariant (J in 0 .. A'Length-2);
            J := J - 1;
         end loop;
         A(J+1) := Y;
      end if;
   end Sort;

end Pair_Insertion_Sort;

Gold level - proof of key integrity properties

Then comes Gold level, which is the first task of the verification challenge: proving that A is sorted on return. This can be expressed easily with a ghost function Sorted:

function Sorted (A : Arr; I, J : Integer) return Boolean is
      (for all K in I .. J-1 => A(K) <= A(K+1))
   with Ghost,
        Pre => J > Integer'First
          and then (if I <= J then I in A'Range and J in A'Range);

   procedure Sort (A : in out Arr) with
     Post => Sorted (A, 0, A'Length-1);

Then, we need to augment the previous loop invariants with enough information to prove this sorting property. Let's look at the first (inner) loop. The invariant of this loop is that it maintains the array sorted up to the current high bound I+1, except for a hole of one index at J+1. That's easily expressed with the ghost function Sorted:

pragma Loop_Invariant (Sorted (A, 0, J));
            pragma Loop_Invariant (Sorted (A, J+2, I+1));

For these loop invariants to be proved, we need to know that the next value possibly passed across the hole at the next iteration (from index J-1 to J+1) is lower than the value currently at J+2. Well, we know that the value at index J-1 is lower than the value at index J thanks to the property Sorted(A,0,J). All we need to add is that A(J+2)=A(J):

pragma Loop_Invariant (A(J+2) = A(J));

This proves the loop invariant. Next, after the loop, value X is inserted at index J+2 in the array. For the sorting property to hold from J+2 upwards after the loop, X needs to be less than the value at J+2 in the loop invariant. As A(J+2) and A(J) are equal, we can write:

pragma Loop_Invariant (A(J) > X);

All the other loops are similar. With these additional loop invariants, GNATprove can prove the sorting property in the code in 12 seconds on my machine:

package body Pair_Insertion_Sort with
  SPARK_Mode
is
   procedure Sort (A : in out Arr) is
      I, J, X, Y, Z : Integer;
   begin
      I := 0;
      while I < A'Length-1 loop
         X := A(I);
         Y := A(I+1);
         if X < Y then
            Z := X;
            X := Y;
            Y := Z;
         end if;

         J := I - 1;
         while J >= 0 and then A(J) > X loop
            A(J+2) := A(J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J));
            pragma Loop_Invariant (Sorted (A, J+2, I+1));
            pragma Loop_Invariant (A(J+2) = A(J));
            pragma Loop_Invariant (A(J) > X);
            J := J - 1;
         end loop;
         A(J+2) := X;

         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J));
            pragma Loop_Invariant (Sorted (A, J+1, I+1));
            pragma Loop_Invariant (A(J+1) = A(J));
            pragma Loop_Invariant (A(J) > Y);
            J := J - 1;
         end loop;
         A(J+1) := Y;

         --  loop invariant for absence of run-time errors
         pragma Loop_Invariant (I in 0 .. A'Length-2);
         --  loop invariant for sorting
         pragma Loop_Invariant (J in -1 .. A'Length-3);
         pragma Loop_Invariant (Sorted (A, 0, I+1));
         I := I+2;
      end loop;

      if I = A'Length-1 then
         Y := A(I);
         J := I - 1;
         while J >= 0 and then A(J) > Y loop
            A(J+1) := A(J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-2);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J));
            pragma Loop_Invariant (Sorted (A, J+1, A'Length-1));
            pragma Loop_Invariant (A(J+1) = A(J));
            pragma Loop_Invariant (A(J) > Y);
            J := J - 1;
         end loop;
         A(J+1) := Y;
      end if;
   end Sort;

end Pair_Insertion_Sort;

Platinum level - full functional proof of requirements

Then comes Platinum level, which is the second task of the verification challenge: proving that A on return is a permutation of its value on entry. For that, we are going to use the ghost function Is_Perm that my colleague Claire Dross presented in this blog post, that expresses that the number of occurrences of any integer in arrays A and B coincide (that is, they represent the same multisets, which is a way to express that they are permutations of one another):

function Is_Perm (A, B : Arr) return Boolean is
     (for all E in Integer => Occ (A, E) = Occ (B, E));

and the procedure Swap that she presented in the same blog post, for which I simply give the contract here:

procedure Swap (Values : in out Arr;
                   X      : in     Index;
                   Y      : in     Index)
   with
     Pre  => X in Values'Range
       and then Y in Values'Range
       and then X /= Y,
     Post => Is_Perm (Values'Old, Values)
       and then Values (X) = Values'Old (Y)
       and then Values (Y) = Values'Old (X)
       and then (for all Z in Values'Range =>
                   (if Z /= X and Z /= Y then Values (Z) = Values'Old (Z)))

The only changes I made with respect to her initial version were to change in various places Natural for Integer, as arrays in our challenge store integers instead of natural numbers. In order to use the same strategy that she showed for selection sort on our pair insertion sort, we need to rewrite a bit the algorithm to swap array cells (as suggested in the challenge specification). For example, instead of the assignment in the first (inner) loop:

A(J+2) := A(J);

we now have:

Swap (A, J+2, J);

This has an effect on the loop invariants seen so far, which must be slightly modified. Then, we need to express that every loop maintains in A a permutation of the entry value for A. For that, we create a ghost constant B that stores the entry value of A:

B : constant Arr(A'Range) := A with Ghost;

and use this constant in loop invariants of the form:

pragma Loop_Invariant (Is_Perm (B, A));

We also need to express that the values X and Y that are pushed down the array are indeed the ones found around index J in all loops. For example in the first (inner) loop:

pragma Loop_Invariant ((A(J) = X and A(J+1) = Y) or (A(J) = Y and A(J+1) = X));

With these changes, GNATprove can prove the permutation property in the code in 27 seconds on my machine (including all the ghost code copied from Claire's blog post):

procedure Sort (A : in out Arr) is
      I, J, X, Y, Z : Integer;
      B : constant Arr(A'Range) := A with Ghost;
   begin
      I := 0;
      while I < A'Length-1 loop
         X := A(I);
         Y := A(I+1);
         if X < Y then
            Z := X;
            X := Y;
            Y := Z;
         end if;

         J := I - 1;
         while J >= 0 and then A(J) > X loop
            Swap (A, J+2, J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J-1));
            pragma Loop_Invariant (Sorted (A, J+2, I+1));
            pragma Loop_Invariant (if J > 0 then A(J+2) >= A(J-1));
            pragma Loop_Invariant (A(J+2) > X);
            --  loop invariant for permutation
            pragma Loop_Invariant (Is_Perm (B, A));
            pragma Loop_Invariant ((A(J) = X and A(J+1) = Y) or (A(J) = Y and A(J+1) = X));
            J := J - 1;
         end loop;
         if A(J+2) /= X then
            Swap (A, J+2, J+1);
         end if;

         while J >= 0 and then A(J) > Y loop
            Swap (A, J+1, J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-3);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J-1));
            pragma Loop_Invariant (Sorted (A, J+1, I+1));
            pragma Loop_Invariant (if J > 0 then A(J+1) >= A(J-1));
            pragma Loop_Invariant (A(J+1) > Y);
            --  loop invariant for permutation
            pragma Loop_Invariant (Is_Perm (B, A));
            pragma Loop_Invariant (A(J) = Y);
            J := J - 1;
         end loop;

         --  loop invariant for absence of run-time errors
         pragma Loop_Invariant (I in 0 .. A'Length-2);
         --  loop invariant for sorting
         pragma Loop_Invariant (J in -1 .. A'Length-3);
         pragma Loop_Invariant (Sorted (A, 0, I+1));
         --  loop invariant for permutation
         pragma Loop_Invariant (Is_Perm (B, A));
         I := I+2;
      end loop;

      if I = A'Length-1 then
         Y := A(I);
         J := I - 1;
         while J >= 0 and then A(J) > Y loop
            Swap (A, J+1, J);
            --  loop invariant for absence of run-time errors
            pragma Loop_Invariant (J in 0 .. A'Length-2);
            --  loop invariant for sorting
            pragma Loop_Invariant (Sorted (A, 0, J-1));
            pragma Loop_Invariant (Sorted (A, J+1, A'Length-1));
            pragma Loop_Invariant (if J > 0 then A(J+1) >= A(J-1));
            pragma Loop_Invariant (A(J+1) > Y);
            --  loop invariant for permutation
            pragma Loop_Invariant (Is_Perm (B, A));
            pragma Loop_Invariant (A(J) = Y);
            J := J - 1;
         end loop;
      end if;
   end Sort;

The complete code for this challenge can be found on GitHub.

Conclusions

Two features of SPARK were particularly useful to help debug unprovable properties. Counterexamples was the first, issuing messages such as the following:

pair_insertion_sort.adb:20:16: medium: array index check might fail (e.g. when A = (others => 1) and A'Last = 3 and J = 2)

Here it allowed me to realize that the upper bound I set for J was too high, so that J+2 was outside of A's bounds.

The second very useful feature was the ability to execute assertions and contracts, issuing messages such as the following:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Loop_Invariant failed at pair_insertion_sort.adb:51

Here it allowed me to realize that a loop invariant which I was trying to prove was in fact incorrect!

As this challenge shows, the five levels of software assurance in SPARK do not require the same level of effort at all. Stone and Bronze levels are rather easy to achieve on small codebases (although they might require refactoring on large codebases), Silver level requires some modest effort, Gold level requires more expertise to drive automatic provers, and finally Platinum level requires a much larger effort than all the previous levels (including possibly some rewriting of the algorithm to make automatic proof possible like here).

Thanks to the organisers of this year's VerifyThis competition, and congrats to the winning teams, two of which used Why3!

Posted in #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.