AdaCore Blog

Using Coq to Verify SPARK 2014 Code

by Yannick Moy

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo.

Automatic provers are very handy when it comes to perform a big numberof simple proof. But they can fail to prove valid formulas when the proof involves some advanced reasoning. As mentioned in a previous post, one check left unproved might invalidate assumptions on which are based the proofs of multiple other checks. This is a case where manual proof may be useful for SPARK 2014 users.

The development version of GNATprove now supports Coq to perform manual proof. Coq is an interactive proof assistant. Coq allows users to perform mathematical proof guaranteed to be rigorous and free from human mistakes.

To prove a formula with Coq, the user writes a "proof scripts". A proof script is composed of different Coq instructions named tactics. Each tactic represents the operation being the transition between one state of the proof and the next one. A Coq proof starts with one subgoal, i.e. the formula we want to prove.  Each tactic applies to one subgoal an can produce an arbitrary number of subgoals (including 0). The initial formula is proved once there are no subgoals remaining.

Let's see how to use Coq on some simple SPARK 2014 code from the GPS environment:

package Vectors with SPARK_Mode is

   subtype Element is Positive range 1 .. 100;
   subtype Index is Positive range 1 .. 100;

   type Vector is array (Positive range 1 .. 100) of Element;

   function Scalar_Product (V1 : Vector; V2 : Vector) return Natural;

end Vectors;

package body Vectors with SPARK_Mode is

   function Scalar_Product (V1 : Vector ; V2 : Vector) return Natural
   is
      Result : Natural := 0;

   begin
      for I in Vector'Range loop
         Result := V1 (I) * V2 (I) + Result;
         pragma Loop_Invariant
           (Result <= (I - Vector'First + 1) * (Element'Last * Element'Last));
      end loop;

      return Result;
   end Scalar_Product;

end Vectors;

First, we analyse the code with the SPARK/Prove All menu to get the results of flow and automated proof:

Here, the loop invariant is needed to prove that there will be no overflow errors, but Alt-Ergo is not capable of proving the preservation of the invariant. To prove it with Coq we first select the failing check and choose the menu SPARK/Prove Check and indicate Coq as alternate prover:

Gps Prove Check
Gps Alter Prover

If it is the first time we try to prove this check with Coq, GNATprove will generate a new file containing the corresponding VC in Coq syntax. If the analysis fails (i.e. there was no proof with Coq for this check or the proof is invalid), GPS will suggest to edit the Coq file:

Editing the file will open a new editor adapted for the chosen interactive prover (this will require some preliminary configuration for Why3). The file presented to us contains many axioms corresponding to the formal definitions of SPARK 2014 types and subprograms. These will be needed to have some properties about the values manipulated during the proof. At the end of the file, we find the VC formula we have to prove to be certain of our loop invariant preservation:

The proof is to be completed between the introductions of variable and hypothesis in the proof context and the "Qed." proof terminator.

The reason for launching a new editor from GPS instead of writing the proof in GPS is that editors for manual proof offer an interactive display of the state of the proof (i.e. what is in the context? how many subgoals are there and what are these subgoals). This is really essential when writing a proof since proof scripts can become easily confusing when they are long or when one doesn't know exactly how each tactic he uses in the proof works.

The editor buffer on the right displays the state of the proof, on the left we can see highlighted in blue what has been already processed by Coq. In this state, we have two subgoals to the proof. Only one subgoal is "focused" at a given moment.

Once the proof is finished, we can close the editor and GPS will offer to re-run the "Prove Check" operation in order to validate our proof. Now our loop invariant preservation is proved:

Now we can re-run "Prove All" and see that our function is now fully verified by GNATprove:

To know more about this new capability of GNATprove, see the following sections of the SPARK User's Guide:

Posted in #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents 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.