Published: lör 20 januari 2018
By tomas
In Blog .

tags: ada spark c c++ rust go coq idris

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