External Axiomatizations

What is it?

It is a feature of the SPARK toolset that allows to manually supply a WhyMl translation for the public specification of a library level package that is in SPARK. This feature is still experimental.

Why is it useful?

  • For features that cannot easily be described using contracts, like transitivity, counting, or summation
  • To link functions to the logic world, like trigonometry functions

How does it work?

  • To say that a library package has an external axiomatization, we annotate it using:

    pragma Annotate (GNATprove, External_Axiomatization);
    
  • These packages should have SPARK_Mode On on their public specification and SPARK_Mode Off on their private part.

  • The WhyMl translation for the package should be stored in a subdirectory named _theories of the proof directory specified for the project.

What should the translation look like?

  • For each publicly visible entity E in the package P, it should provide the same elements (types as well as logic and program functions) as the automatic translation, all grouped in one single module named P__e. For example, the module for a function F should provide both a logic function declaration named f__logic and a program function declaration named f.
  • For most types, a model module in defined in ada__model.mlw that can be cloned to get most of the required declarations.
  • The manual translation may use any type, constant and function that is visible from the Ada package declaration.
  • A good way to start an axiomatization file on a package is to launch the toolset on it and copy paste the modules created for each entity of the package. A WhyMl file created by the tool on a package P contains a module for every declaration visible from it, only declarations from P itself should be copied. The generated file usually contains two modules for each entity, one named P__e and one named P__e__axiom. Both should be put together in P__e for the manual translation. The toolset will replace statically known expressions with their value. Beware that they might be architecture dependent.

Example

For example, let us consider the following package, stored in a file sum.ads, providing a summation function for slices of arrays of integers:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
package Sums with SPARK_Mode is
   pragma Annotate (GNATprove, External_Axiomatization);

   subtype Extended_Index is Integer range 0 .. 2 ** 16;
   subtype Index is Integer range 1 .. Extended_Index'Last;

   subtype Vector_Element is
     Integer range Integer'First / Index'Last .. Integer'Last / Index'Last;

   type Vector is array (Index range <>) of Vector_Element;

   type Slice_Bounds is
      record
         Lo : Index;
         Hi : Extended_Index;
      end record;

   function Sum (X : Vector; Bounds : Slice_Bounds) return Integer with
     Pre => (Bounds.Lo > Bounds.Hi) or else
     (X'First <= Bounds.Lo and Bounds.Hi <= X'Last);

end Sums;

We can provide the following Why3 translation for it, that we should store in a file named sum.mlw:

module Sums__extended_index
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Integer
 use import "int".Int

 type extended_index

 function first : int = 0

 function last  : int = 65536

 predicate in_range (x : int) = first <= x /\ x <= last

 (* Clone of the model module for discrete types with static bounds *)
 clone export "ada__model".Static_Discrete with
 type t = extended_index,
 function first = first,
 function last = last,
 predicate in_range = in_range
 
 (* Type for mutable variables of type extended_index *)
 type extended_index__ref = { mutable extended_index__content : extended_index }
 val extended_index__havoc (x : extended_index__ref) : unit
   writes { x }

 (* All values of type extended_index are in range *)
 predicate dynamic_invariant (expr : int) bool bool bool  =
   dynamic_property first last expr
 
 (* We know nothing for default initialization of variables of type
    extended_index *)
 predicate default_initial_assumption int bool = true
end

module Sums__extended_index__rep
 use import Sums__extended_index
 use import "_gnatprove_standard".Main

 (* Projection functions from extended_index to int *)
 clone export "ada__model".Rep_Proj_Int with
   type t = extended_index,
   predicate in_range = in_range
end

module Sums__index
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Integer
 use import "int".Int

 type index

 function first : int = 1

 function last  : int = 65536

 predicate in_range (x : int) = first <= x /\ x <= last

 (* Clone of the model module for discrete types with static bounds *)
 clone export "ada__model".Static_Discrete with
 type t = index,
 function first = first,
 function last = last,
 predicate in_range = in_range

 (* Type for mutable variables of type index *)
 type index__ref = { mutable index__content : index }
 val index__havoc (x : index__ref) : unit
   writes { x }

 (* All values of type index are in range *)
 predicate dynamic_invariant (expr : int) bool bool bool  =
   dynamic_property first last expr
 
 (* We know nothing for default initialization of variables of type index *)
 predicate default_initial_assumption int bool = true

end

module Sums__index__rep
 use import Sums__index
 use import "_gnatprove_standard".Main

 (* Projection functions from index to int *)
 clone export "ada__model".Rep_Proj_Int with
   type t = index,
   predicate in_range = in_range
end

module Sums__vector_element
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Int_Division
 use import Standard__integer
 use import "int".Int

 type vector_element

 function first : int = Int_Division.div Standard__integer.first 65536

 function last  : int = Int_Division.div Standard__integer.last 65536

 predicate in_range (x : int)  = first <= x /\ x <= last

 (* Clone of the model module for discrete types with static bounds *)
 clone export "ada__model".Static_Discrete with
 type t = vector_element,
 function first = first,
 function last = last,
 predicate in_range = in_range

 (* Type for mutable variables of type vector_element *)
 type vector_element__ref = { mutable vector_element__content : vector_element }
 val vector_element__havoc (x : vector_element__ref) : unit
   writes { x }

end

module Sums__vector_element__rep
 use import Sums__vector_element
 use import "_gnatprove_standard".Main

 (* Projection functions from vector_element to int *)
 clone export "ada__model".Rep_Proj_Int with
   type t = vector_element,
   predicate in_range = in_range
end

(* Module for any array type ranging over signed integer types and
   containing vector_element *)
module Array__Int__Sums__vector_element
 use import "_gnatprove_standard".Main
 use import "int".Int
 use        Sums__vector_element
 use        Sums__vector_element__rep

 function one : int = 1

 type component_type = Sums__vector_element.vector_element

 (* Clone of the model module for logical arrays containing vector_element
    and indexed by mathematical integers *)
 clone export "_gnatprove_standard".Array__1 with
 type I1.t = int,
 predicate I1.le = Int.(<=),
 predicate I1.lt = Int.(<),
 predicate I1.gt = Int.(>),
 function I1.add = Int.(+),
 function I1.sub = Int.(-),
 function I1.one = one,
 type component_type = component_type

 (* Primitive equality between arrays *)
 function bool_eq (a:map) (af:int) (al:int) (b:map) (bf:int) (bl:int) : bool =
   (if af <= al
        then al - af = bl - bf
        else bf > bl) /\
         (forall idx : int. af <= idx <= al ->
             (get a idx) = (get b (bf - af + idx)))
 
 (* Clone of the model module for comparison of arrays *)
 clone export "ada__model".Array_Int_Rep_Comparison_Axiom with
 type component_type = component_type,
 function to_rep = Sums__vector_element__rep.to_rep,
 type map = map,
 type Index.t = int,
 predicate Index.le = Int.(<=),
 predicate Index.lt = Int.(<),
 predicate Index.gt = Int.(>),
 function Index.add = Int.(+),
 function Index.sub = Int.(-),
 function Index.one = one,
 function get = get,
 function bool_eq = bool_eq

end

module Sums__vector
 use import "int".Int
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Integer
 use import Standard__integer
 use import Sums__index
 use import Sums__vector_element
 use        Array__Int__Sums__vector_element
 use        Standard__integer__rep
 use        Sums__vector_element__rep

 predicate index_dynamic_property (first : int) (last : int) (x : int) =
      first <= x /\ x <= last

 (* Clone of the model module for unconstrained arrays *)
 type component_type  =
  Sums__vector_element.vector_element

 function id (x : int) : int = x

 (* Clone of the model module for unconstrained arrays *)
 clone export "ada__model".Unconstr_Array with
 type map = Array__Int__Sums__vector_element.map,
 function array_bool_eq = Array__Int__Sums__vector_element.bool_eq,
 type index_base_type = Standard__integer.integer,
 type index_rep_type = int,
 function to_rep = Standard__integer__rep.to_rep,
 function rep_to_int = id,
 predicate in_range_base = Standard__integer.in_range,
 predicate index_dynamic_property = index_dynamic_property,
 predicate index_rep_le = Int.(<=)

 type vector  = __t

 (* Type for mutable variables of type vector *)
 type vector__ref = { mutable vector__content : vector }
 val vector__havoc (x : vector__ref) : unit
   writes { x }

 (* Helper function *)
 function _get "inline" (v : vector) (i : int) : int =
   	  Sums__vector_element__rep.to_rep (Array__Int__Sums__vector_element.get (to_array v) i)

 (* If vectors are not empty, their bounds are between Index.first and
    Index.last *)
 predicate dynamic_invariant (expr : vector) bool (skip_bounds : bool) bool  =
  (if skip_bounds then true
   else dynamic_property Sums__index.first Sums__index.last
          (first expr) (last expr))
end

module Sums__slice_bounds
 use import "int".Int
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Integer
 use import Sums__index
 use        Sums__index__rep
 use import Sums__extended_index
 use        Sums__extended_index__rep

 (* Fields for record type *)
 type __split_fields  =
  { rec__sums__slice_bounds__lo : index; rec__sums__slice_bounds__hi : extended_index }

 type __split_fields__ref = { mutable __split_fields__content : __split_fields }
 val __split_fields__havoc (x : __split_fields__ref) : unit
   writes { x }

 (* Record type *)
 type slice_bounds  =
  { __split_fields : __split_fields }

 (* Type for mutable variables of type slice_bounds *)
 type slice_bounds__ref = { mutable slice_bounds__content : slice_bounds }
 val slice_bounds__havoc (x : slice_bounds__ref) : unit
   writes { x }

 (* Helper function *)
 function _rec__lo "inline" (b : slice_bounds) : int =
   	  Sums__index__rep.to_rep (rec__sums__slice_bounds__lo (__split_fields (b)))

 (* Helper function *)
 function _rec__hi "inline" (b : slice_bounds) : int =
   	  Sums__extended_index__rep.to_rep (rec__sums__slice_bounds__hi (__split_fields (b)))

 (* Condition to be allowed to access Lo *)
 predicate sums__slice_bounds__lo__pred  (a : slice_bounds) =
  true

 val rec__sums__slice_bounds__lo_
   (a : slice_bounds)  :Sums__index.index
  requires { sums__slice_bounds__lo__pred a }
  ensures  { result = a.__split_fields.rec__sums__slice_bounds__lo }


 (* Condition to be allowed to access Hi *)
 predicate sums__slice_bounds__hi__pred  (a : slice_bounds) =
  true

 val rec__sums__slice_bounds__hi_
   (a : slice_bounds)  :Sums__extended_index.extended_index
  requires { sums__slice_bounds__hi__pred a }
  ensures  { result = a.__split_fields.rec__sums__slice_bounds__hi }


 (* Equality function over slice_bounds *)
 function bool_eq  (a : slice_bounds) (b : slice_bounds) : bool =
  _rec__lo a = _rec__lo b /\ _rec__hi a = _rec__hi b

 function dummy : slice_bounds

 (* No particular property applies to all values of types slice_bounds *)
 predicate dynamic_invariant slice_bounds bool bool bool = true
 
 (* We know nothing for default initialization of variables of slice_bounds *)
 predicate default_initial_assumption slice_bounds bool = true
end

module Sums__sum
 use import "int".Int
 use import "_gnatprove_standard".Main
 use        "_gnatprove_standard".Integer
 use        "_gnatprove_standard".Array__1
 use import Sums__slice_bounds
 use import Sums__index
 use        Sums__index__rep
 use import Standard__integer
 use import Sums__extended_index
 use        Sums__extended_index__rep
 use import Sums__vector

 (* Logic complete function for sum *)
 function sum__logic
   (x : vector) (bounds : slice_bounds)  :int

 (* Helper function *)
 function _sum "inline" (x : vector) (bounds : slice_bounds)  :int =
   	  sum__logic x bounds

 (* Axiom for defining the sum function *)
 axiom sum_def:
    forall v : vector, b : slice_bounds
      [sum__logic v b].
      Standard__integer.in_range (sum__logic v b) /\
      (* Case of the empty slice *)
      (_rec__lo b > _rec__hi b -> _sum v b = 0) /\

      (* Case of a non-empty slice  *)
      (first v <= _rec__lo b <= _rec__hi b <= last v ->

         (* If the slice only contains one element *)
         (_rec__lo b = _rec__hi b -> _sum v b = _get v (_rec__lo b)) /\

         (* Link to smaller slices of the same vector *)
         (forall b1 : slice_bounds [sum__logic v b1].

             (* Ending at the same index *)
             ((_rec__hi b1 = _rec__hi b /\ _rec__lo b < _rec__lo b1 <= _rec__hi b) ->
              let b2 = {__split_fields =
	      	         {rec__sums__slice_bounds__lo = rec__sums__slice_bounds__lo (__split_fields b);
                          rec__sums__slice_bounds__hi = Sums__extended_index__rep.of_rep ((_rec__lo b1) - 1)}} in
                 _sum v b = _sum v b1 + _sum v b2) /\
             (* Sartind at the same index *)
             ((_rec__lo b1 = _rec__lo b /\ _rec__lo b <= _rec__hi b1 < _rec__hi b) ->
              let b2 = {__split_fields =
	      	         {rec__sums__slice_bounds__lo = Sums__index__rep.of_rep ((_rec__hi b1) + 1);
                          rec__sums__slice_bounds__hi = rec__sums__slice_bounds__hi (__split_fields b)}} in
                 _sum v b = _sum v b1 + _sum v b2)))

 (* Program partial function with a precondition for sum *)
 val sum (x : vector) (bounds : slice_bounds)  :int
  requires { _rec__lo bounds > _rec__hi bounds \/
             first x <= _rec__lo bounds /\ _rec__hi bounds <= last x }
  ensures  { result = sum__logic x bounds }

end