Trying out Ada SPARK

Lately me and Benjamin Nauck have been investigating languages with proving functionality, such as the variant of Ada known as SPARK. The basic idea of such languages is that the programmer can supply a set of contracts on the inputs and outputs of each function, and then a prover (gnatprove) is run on the program which checks that the contracts are indeed fulfilled for every possible combination of inputs. This is great for catching lots of bugs, for example issues due to overflow or when math functions are given atypical floating points numbers like ∞ or NaN (not-a-number). By comparison languages such as C or C++ are not able to provide guarantees like these, not even current popular "safe" languages like Rust or Go.

I decided to make a Saturday project out of writing a primality tester and integer square root function in Ada, then throwing some SPARK contracts on top of them. Both the primality testing (IsPrime) and integer square root functions (Isqrt and Isqrt2) are limited by the maximum range of Integer in Ada: 2147483647. This also happens to be a Mersenne prime. IsPrime does typical trial division up to the square root of the input value. Integer square roots are done because Sqrt in Ada.Numerics.Elementary_Functions gives no guarantees on the returned values beyond them being >= 0. gnatprove also has trouble proving that if some integer x is >= 5 then Float(x) >= 5.0. For these reasons I decided to implement my own square root function.

I decided to write two integer square root implementations. The first implementation (Isqrt) iterates i from 2 .. 46340 (floor(sqrt(2147483647))) and checks at every step if i² >= num and returns either i or i-1 if that is the case. This is of course very slow, but fairly easy to prove correct. The key to proving this was the Loop_Invariant pragma. Isqrt is listed below:

   -- Returns floor(sqrt(num)) for 0 <= num <= 2147483647 (Natural'Last)
   function Isqrt (num : Natural) return Natural with
     SPARK_Mode => On,
     Post =>
       (if num < 46340*46340 then
          num in Isqrt'Result**2 .. (Isqrt'Result + 1)**2 - 1)
       and then (if num >= 46340*46340 then Isqrt'Result = 46340)
   is
   begin
      -- 0 -> 0, 1 -> 1
      if num < 2 then
         return num;
      end if;

      for i in 2 .. 46340 loop
         if i*i = num then
            return i;
         end if;

         if i*i > num then
            return i-1;
         end if;

         pragma Loop_Invariant(i*i < num);
      end loop;
      return 46340;
   end Isqrt;

The second integer square root (Isqrt2) computes the value by recursion. A range is kept and halved at every step until it is known that the solution lies between two consecutive integers. Then the lowest of those two integers is returned. This variant turned out to be easier to write. Isqrt2 and the recursive Isqrt2_inner are given below:

   function Isqrt2_inner (num, lo, hi : Natural) return Natural with
     SPARK_Mode => On,
     Pre => 
       lo in 1 .. 46340 and then
       hi in 1 .. 46340 and then
       lo < hi and then
       num in lo**2 .. hi**2-1,
       Post =>
         num in Isqrt2_inner'Result**2 .. (Isqrt2_inner'Result + 1)**2 - 1
   is
      mid : Natural;
   begin
      if lo = hi-1 then
         return lo;
      end if;
      mid := (lo + hi) / 2;
      pragma Assert (mid in lo+1 .. hi-1);
      if mid**2 > num then
         return Isqrt2_inner(num, lo, mid);
      else
         return Isqrt2_inner(num, mid, hi);
      end if;
   end Isqrt2_inner;

   -- Faster, recursive version of Isqrt
   function Isqrt2 (num : Natural) return Natural with
     SPARK_Mode => On,
     Post =>
       (if num < 46340*46340 then
          Isqrt2'Result < 46340 and then
          num in Isqrt2'Result**2 .. (Isqrt2'Result + 1)**2 - 1)
       and then (if num >= 46340*46340 then Isqrt2'Result = 46340)
   is
   begin
      -- 0 -> 0, 1 -> 1
      if num < 2 then
         return num;
      end if;

      if num >= 46340*46340 then
         return 46340;
      end if;

      return Isqrt2_inner(num, 1, 46340);
   end Isqrt2;

IsPrime itself is not very interesting. I don't prove that the function actually behaves correctly, such a proof would be very involved. All we can know is that it will terminate and that its assertions are correct.

The complete code listing will be given below. There are three files: isprime.adb which has the bulk of the code, isprime.ads is like a header, and main.adb which does user interaction:

-- isprime.adb
package body IsPrime is
   -- Returns floor(sqrt(num)) for 0 <= num <= 2147483647 (Natural'Last)
   function Isqrt (num : Natural) return Natural with
     SPARK_Mode => On,
     Post =>
       (if num < 46340*46340 then
          num in Isqrt'Result**2 .. (Isqrt'Result + 1)**2 - 1)
       and then (if num >= 46340*46340 then Isqrt'Result = 46340)
   is
   begin
      -- 0 -> 0, 1 -> 1
      if num < 2 then
         return num;
      end if;

      for i in 2 .. 46340 loop
         if i*i = num then
            return i;
         end if;

         if i*i > num then
            return i-1;
         end if;

         pragma Loop_Invariant(i*i < num);
      end loop;
      return 46340;
   end Isqrt;

   function Isqrt2_inner (num, lo, hi : Natural) return Natural with
     SPARK_Mode => On,
     Pre => 
       lo in 1 .. 46340 and then
       hi in 1 .. 46340 and then
       lo < hi and then
       num in lo**2 .. hi**2-1,
       Post =>
         num in Isqrt2_inner'Result**2 .. (Isqrt2_inner'Result + 1)**2 - 1
   is
      mid : Natural;
   begin
      if lo = hi-1 then
         return lo;
      end if;
      mid := (lo + hi) / 2;
      pragma Assert (mid in lo+1 .. hi-1);
      if mid**2 > num then
         return Isqrt2_inner(num, lo, mid);
      else
         return Isqrt2_inner(num, mid, hi);
      end if;
   end Isqrt2_inner;

   -- Faster, recursive version of Isqrt
   function Isqrt2 (num : Natural) return Natural with
     SPARK_Mode => On,
     Post =>
       (if num < 46340*46340 then
          Isqrt2'Result < 46340 and then
          num in Isqrt2'Result**2 .. (Isqrt2'Result + 1)**2 - 1)
       and then (if num >= 46340*46340 then Isqrt2'Result = 46340)
   is
   begin
      -- 0 -> 0, 1 -> 1
      if num < 2 then
         return num;
      end if;

      if num >= 46340*46340 then
         return 46340;
      end if;

      return Isqrt2_inner(num, 1, 46340);
   end Isqrt2;

   -- Tests whether a Positive is prime
   function IsPrime (num : Positive) return Boolean with
     SPARK_Mode => On
   is
      top : Positive;
   begin
      if num = 2 or num = 3 then
         return True;
      end if;

      if num mod 2 = 0 then
         return False;
      end if;

      top := Isqrt2(num);
      pragma Assert (top < num);

      for i in Integer range 3 .. top loop
         pragma Assert (i < num);
         if num mod i = 0 then
            return False;
         end if;
      end loop;
      return True;
   end IsPrime; 
end IsPrime;
-- isprime.ads
package IsPrime is

  function IsPrime (num : Positive) return Boolean with
     SPARK_Mode => On,
     Pre => num >= 2;

end IsPrime;
-- main.adb
with Ada.Text_IO;
with Ada.Integer_Text_IO;
with IsPrime;

procedure Main
is
   num : Integer;
begin
   Ada.Text_IO.Put_Line("Enter an integer to test");
   Ada.Integer_Text_IO.Get(num);

   --num := 2147483647; -- largest Positive, also a prime
   if num < 2 then
      Ada.Text_IO.Put_Line("Number must be >= 2");
      return;
   end if;

   Ada.Text_IO.Put_Line(Boolean'Image(IsPrime.IsPrime(num)));
end Main;

Example gnatprove output on the entire project:

gnatprove -P/home/thardin/projects/ada/exempel/default.gpr --level=0 --ide-progress-bar -U
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Summary logged in /home/thardin/projects/ada/exempel/obj/gnatprove/gnatprove.out
[2018-01-20 21:24:42] process terminated successfully, elapsed time: 05.20s

Report:

Summary of SPARK analysis
=========================

--------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total       Flow   Interval   CodePeer      Provers   Justified   Unproved
--------------------------------------------------------------------------------------------------------
Data Dependencies                 .          .          .          .            .           .          .
Flow Dependencies                 .          .          .          .            .           .          .
Initialization                    6          6          .          .            .           .          .
Non-Aliasing                      .          .          .          .            .           .          .
Run-time Checks                  26          .          .          .    26 (CVC4)           .          .
Assertions                        5          .          .          .     5 (CVC4)           .          .
Functional Contracts              6          .          .          .     6 (CVC4)           .          .
LSP Verification                  .          .          .          .            .           .          .
--------------------------------------------------------------------------------------------------------
Total                            43    6 (14%)          .          .     37 (86%)           .          .


Analyzed 2 units
in unit isprime, 4 subprograms and packages out of 4 analyzed
  IsPrime.IsPrime at isprime.ads:3 flow analyzed (0 errors and 0 warnings) and proved (6 checks)
  IsPrime.Isqrt at isprime.adb:3 flow analyzed (0 errors and 0 warnings) and proved (10 checks)
  IsPrime.Isqrt2 at isprime.adb:55 flow analyzed (0 errors and 0 warnings) and proved (6 checks)
  IsPrime.Isqrt2_inner at isprime.adb:30 flow analyzed (0 errors and 0 warnings) and proved (15 checks)
in unit main, 0 subprograms and packages out of 1 analyzed
  Main at main.adb:5 skipped

I tried to prove that Main behaves correctly, but unfortunaly the Text_IO functions do not provide any suitable contracts:

gnatprove -P/home/thardin/projects/ada/exempel/default.gpr --ide-progress-bar --level=0 -u main.adb
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:10:15: warning: no Global contract available for "Put_Line"
main.adb:10:15: warning: assuming "Put_Line" has no effect on global items
main.adb:11:23: warning: no Global contract available for "Get"
main.adb:11:23: warning: assuming "Get" has no effect on global items
main.adb:15:18: warning: no Global contract available for "Put_Line"
main.adb:15:18: warning: assuming "Put_Line" has no effect on global items
main.adb:19:15: warning: no Global contract available for "Put_Line"
main.adb:19:15: warning: assuming "Put_Line" has no effect on global items
Summary logged in /home/thardin/projects/ada/exempel/obj/gnatprove/gnatprove.out
[2018-01-20 21:26:37] process terminated successfully, elapsed time: 02.20s

This Stackoverflow question seems to indicate that a SPARK.Ada.Text_IO module exists. Unfortunately I don't have that package in my setup. It was previously known as SPARK_IO, which also does not exist on my machine.

There are however some major limitations with SPARK. The biggest one is that dynamic memory allocation is not allowed. All SPARK functions must also terminate. So SPARK is not suitable for every case at least. There is however a separation kernel called Muen which is written in SPARK, so clearly a lot can be done with it.

Finally, I'll mention that there are other tools and languages with similar functionality, such as Coq and Idris. I haven't looked at those yet, but Coq seems especially popular among mathematicians.