In SPARK, as in most programming languages, there are a bunch of bounded integer types. Theoretically, there are infinitely many (or at least really a lot) of those, as the user can declare her own, like in:

These integer types have the following semantics with respect to their bounds:

• They have a base type, usually the smallest possible machine integer type in which they fit. Computations are done on this base type.
• The type and its base type can be either modular or signed. On modular types, computation wraps around when the modulo is exceeded. For signed types, an error is propagated.
• Checks for specific type's bounds are only done at assignment or subprogram call. If they fail, an error is propagated.

On the other hand, Why3 only has mathematical integers and a library for bitvectors. Since bitwise operations can only be done on modular types in Ada, we currently translate arithmetic operations on signed integer types as operations on mathematical integers and arithmetic operations on modular types as operation on bitvectors (see a previous post on this subject).

The only remaining question now is, how do we encode specific bounds of the Ada types into our Why3 translation? In this post, I will present three different ways we tried to do this and explain which one we currently use and why.

1. Use an abstract type with a range axiom and conversion functions (that is what we did in GNATprove until recently):
   • Integer types whose bounds are statically known are encoded as abstract Why3 types with to_rep and of_rep conversion functions to the representation type (int or bitvector) and a range axiom stating that the conversion of objects of the abstract type are always in the appropriate range.

     type Int_10 is new Integer range 1 .. 10;

     is translated as

     (* An abstract type *)
     type int_10
     
     (* Conversion functions toward mathematical integers *)
     function to_rep int_10 : int
     function of_rep int : int_10
     
     axiom inversion_axiom :
       forall x : t. of_rep (to_rep (x)) = x
     axiom coerce_axiom :
       forall x : int. 1 <= x <= 10 -> to_rep (of_rep x) = x
     
     (* Range axiom *)
     axiom range_axiom :
       forall x : int_10. 1 <= to_rep x <= 10

   • Other integer types (those with dynamic bounds) are encoded as a renaming of their base type's Why3 encoding. As the bounds of these types are not static, they may have different values between different runs of the code. As a consequence, we cannot assume that elements of these types are in any other bounds than those of its base type.

     type Int_A_B is new Integer range A .. B;

     is translated as

     (* A renaming of Integer *)
     type int_a_b = integer

   • The Why3 translation of Ada expressions of an integer type are always of the corresponding abstract Why3 type. Additionally, every time an object of a dynamic integer type is used, an assumption is generated that the object is in its dynamic type.

     X : Int_A_B := ...;

     is translated into

     let x : ref int_a_b = ... in
     assume { a <= !x <= b };

   The major drawbacks of this approach are:

   • to determine the bounds of a static integer expression, the solver has to do quantifier reasoning,  which is known to be incomplete and unpredictable.
   • call to the conversion functions appear all over the place as expressions have to be converted back and forth between storage in variables and arithmetic operations. Dealing with these conversion functions require usage of the inversion and coerce axioms, which means more quantifier reasoning.
2. Translate types directly to their representation and assume the bounds when needed:
   • No new Why3 type are created for Ada integer types.
   • Static and dynamic integer expressions are encoded as their representation type (int or bitvector). Additionally, every time an object of a discrete type is used, an assumption is generated that the object is in its type.

     X : Int_10 := ...;

     is translated into

     let x : ref int = ... in
     assume { 1 <= !x <= 10 };

   With this translation, the conversion functions to_rep and of_rep and the range, inversion, and coerce axioms disappear completely. On the other hand, we have heavy quantified formulas whenever objects of integer types are stored in an array. Here is an example of this:

   type Int_10_Array is array (1 .. 3) of Int_10;
   A : Int_10_Array := ...;

   is translated as

   let a : ref (map int int) = ... in
   assume { forall i : int. 1 <= i <= 3 -> 1 <= get !a i <= 10 }

   To alleviate this, we tried assuming bounds only at array accesses. As such accesses can appear in logic expressions, we used epsilon formulas for this:

   pragma Assert (for all X in 1 .. 3 => A (X) = 0);

   is then translated as

   assert { forall x : int. 1 <= x <= 3 ->  (epsilon y : int. y = get !a 1 /\ 1 <= y <= 10) = 0 }

   which roughly means, x is any mathematical integer type such that x is the value stored at index 1 in a and x is between 1 and 10. Unfortunately, this does not remove the quantifier as, for each such epsilon construct, Why3 generates something like:

   function f (a : map int int) (x : int)
   axiom f_definition:
     forall a : map int int, x : int. f a x = get a x /\ 1 <= f a x <= 10
   
   assert { forall x : int. 1 <= x <= 3 ->  f !a x = 0 }

3. Translate expressions of an integer type to its representation except when they are included in composite types:

   • Ada integer types are translated as in 1, using an abstract Why3 type along with conversion functions to the representative type and a range axiom.
   • Like in 2, Ada integer expressions are translated directly into mathematical integers or bitvectors  and assumptions are generated for their ranges when needed.
   • Components of composite types of an Ada integer type are translated using the Why3 abstract type generated for the Ada type. In this way, no quantified formulas are introduced for arrays of static integer types.

   In this framework,

   A : Int_10_Array := ...;
   X : Int_10 := ...;
   A (2) := A (1) + X;

   is translated as

   let a : ref (map int int_10) = ... in
   let x : ref int = ... in
   assume { 1 <= !x <= 10 };
   a := set !a 2 (of_rep (to_rep (get !a 1) + !x)) ;

As you may have guessed from this presentation, this third model was the one which gave the best results in our experiments. Indeed, the amount of required quantified formulas seemed to be minimized: on the one hand, most of the time, bounds are directly available for integer expressions and arithmetic operations can be applied to variables without requiring a conversion. On the other hand, we avoid generating numerous quantified expressions for arrays containing integer types with static bounds.

Also note that, a bit against our expectations, we did not experiment that many differences in solver efficiency using our different models for Ada integer types. This tends to make me think that, finally, solvers are not so bad with dealing with these quantified axioms...