SPARK prooving an array of Positives.

SPARK prooving an array of Positives.

[Shark8]

I have a bit of a problem getting the SPARK provers to accept that a postcondition cannot fail. Given the following in a spec file:

    Type Axis_Count is range 0..999   with Size => 10;
    Type Axis_Dimensions is Array (Axis_Count range <>) of Positive
      with Default_Component_Value => 1;
    Subtype Primary_Data_Array is Axis_Dimensions(1..999);
    Subtype Random_Groups_Data is Axis_Dimensions(1..998);

    Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64;

and the following in the implementation:

    Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64 is
        Max : Constant := Positive'Last;
        Function First return Interfaces.Unsigned_64 is
          ( Interfaces.Unsigned_64( Item( Item'First ) ) )
          with Inline, Pre => Item'Length > 0, Post => First'Result <= Max;
        Function Last return Interfaces.Unsigned_64 is
            ( Interfaces.Unsigned_64( Item( Item'Last ) ) )
          with Inline, Pre => Item'Length > 0, Post => Last'Result  <= Max;
        use all type Interfaces.Unsigned_64;
    Begin
	case Item'Length is
	   when 0      => return 1;
	   when 1      => return First;
	   when 2      => return First * Last;
	   when others =>
	    Declare
		Middle : Constant Axis_Count := Item'Length/2 + Item'First;
		Subtype Head is Axis_Count range Item'First..Middle;
		Subtype Tail is Axis_Count range Axis_Count'Succ(Middle)..Item'Last;
	    Begin
		Return EF(Item(Head)) * EF(Item(Tail));
	    End;
	end case;
    End EF;

the SPARK prover is issuing warnings that the postconditions might fail.
"medium: postcondition might fail, cannot prove First'Result <= Max (e.g. when First'Result = 0)"
But this is impossible given that the element-type is Positive and the precondition states there is at least one element. Does anyone know why this is happening? (And how to fix it?)

Re: SPARK prooving an array of Positives.

[Anh Vo]

On Tuesday, July 30, 2019 at 9:35:54 AM UTC-7, Shark8 wrote:
> I have a bit of a problem getting the SPARK provers to accept that a postcondition cannot fail. Given the following in a spec file:
> 
>     Type Axis_Count is range 0..999   with Size => 10;
>     Type Axis_Dimensions is Array (Axis_Count range <>) of Positive
>       with Default_Component_Value => 1;
>     Subtype Primary_Data_Array is Axis_Dimensions(1..999);
>     Subtype Random_Groups_Data is Axis_Dimensions(1..998);
> 
>     Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64;
> 
> and the following in the implementation:
> 
>     Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64 is
>         Max : Constant := Positive'Last;
>         Function First return Interfaces.Unsigned_64 is
>           ( Interfaces.Unsigned_64( Item( Item'First ) ) )
>           with Inline, Pre => Item'Length > 0, Post => First'Result <= Max;
>         Function Last return Interfaces.Unsigned_64 is
>             ( Interfaces.Unsigned_64( Item( Item'Last ) ) )
>           with Inline, Pre => Item'Length > 0, Post => Last'Result  <= Max;
>         use all type Interfaces.Unsigned_64;
>     Begin
> 	case Item'Length is
> 	   when 0      => return 1;
> 	   when 1      => return First;
> 	   when 2      => return First * Last;
> 	   when others =>
> 	    Declare
> 		Middle : Constant Axis_Count := Item'Length/2 + Item'First;
> 		Subtype Head is Axis_Count range Item'First..Middle;
> 		Subtype Tail is Axis_Count range Axis_Count'Succ(Middle)..Item'Last;
> 	    Begin
> 		Return EF(Item(Head)) * EF(Item(Tail));
> 	    End;
> 	end case;
>     End EF;
> 
> the SPARK prover is issuing warnings that the postconditions might fail.
> "medium: postcondition might fail, cannot prove First'Result <= Max (e.g. when First'Result = 0)"
> But this is impossible given that the element-type is Positive and the precondition states there is at least one element. Does anyone know why this is happening? (And how to fix it?)

Assuming you are using gnat-2019-community version, increase the level of proof by setting --level=n (n = 0 to 4) to see if it works.

Anh Vo

Re: SPARK prooving an array of Positives.

[Brad Moore]

I got this to prove in SPARK by making a couple of modifications.

The first thing I noticed is that post conditions of First and Last are trying to show that the result is not larger than the Positive type maximum value.

I find it is a good idea to simplify the code, as it usually helps the proofing effort. If the result type of First and Last is of subtype Positive, then there should be no need to prove anything, since Positive'Last = Max.

So I changed the result type to Positive. 
After doing that, the prover was happy about the First and Last functions, but was complaining about the case statement when Item'Length is 2, 

   i.e.  I had written, 
       when 2 =>  return Unsigned_64(First * Last);

SPARK wanted me to prove that this multiplication cannot cause a numeric overflow. This is a problem now because First and Last are of type Positive, and the result of multiplying the worst case positive values, Positive'Last*Positive'Last would overflow, so I needed to convert the results of First and Last to 64 bit unsigned values before doing the multiplication.
The SPARK prover is now happy because it can tell that the multiplying the two 31 bit values after converting to 64 bits will not overflow a 64 bit value.

I hope you don't mind, but I took the liberty of applying the GNAT style guidelines to the code, after turning on most style and warnings, and addressing those. I also made a couple other changes that I thought might have helped the prover, but I doubt was necessary, but something to keep in mind, and seemed to be improvements, but I don't think any of these changes likely helped the SPARK prover.

For example, rather than use subtype Positive, and Interfaces.Unsigned_64, I think it helped to define more specific types to fit the code problem.
That is, instead of Positive, I defined type Axis_Value. This is a type definition, rather than a subtype definition. This might be helpful for SPARK since the type definition is a compile-time definition, whereas subtypes typically involve dynamic checking at run time to ensure that the range constraints are being applied. I think generally SPARK would have an easier time analyzing code if it can rely on compile time constraints. 

I think also having the Axis_Value type declared makes it clearer in the code the number of bits associated with the type, rather than Positive, which can be more target-dependent.

Also, instead of using Interfaces.Unsigned_64, I defined the type Result_Value, which seems to help clarify to the reader, and eliminate the need for clients to with an extra package.

package FITS with SPARK_Mode is

   type Result_Value is mod 2 ** 64;
   for Result_Value'Size use 64;

   type Axis_Value is range 1 .. +(2 **31 - 1);
   for Axis_Value'Size use 32;
   
   type Axis_Count is range 0 .. 999   with Size => 10;

   type Axis_Dimensions is array (Axis_Count range <>) of Axis_Value
     with Default_Component_Value => 1;

   subtype Primary_Data_Array is Axis_Dimensions (1 .. 999);
   subtype Random_Groups_Data is Axis_Dimensions (1 .. 998);

   function EF (Item : FITS.Axis_Dimensions) return Result_Value;

end FITS;

package body FITS with SPARK_Mode is

   function EF (Item : FITS.Axis_Dimensions) return Result_Value
   is
      function First return Axis_Value is (Item (Item'First))
        with Inline,
             Pre => Item'Length > 0;

      function Last return Axis_Value is (Item (Item'Last))
        with Inline,
             Pre => Item'Length > 0;

   begin -- EF

      case Item'Length is
         when 0      => return 1;
         when 1      => return Result_Value (First);
         when 2      => return Result_Value (First) * Result_Value (Last);

         when others =>
            declare
               Middle : constant Axis_Count := Item'Length / 2 + Item'First;
               subtype Head is Axis_Count range Item'First .. Middle;
               subtype Tail is Axis_Count range
                 Axis_Count'Succ (Middle) .. Item'Last;
            begin
               return EF (Item (Head)) * EF (Item (Tail));
            end;
      end case;

   end EF;

end FITS;

Brad

Re: SPARK prooving an array of Positives.

[Shark8]

On Tuesday, July 30, 2019 at 10:20:51 PM UTC-6, Brad Moore wrote:
Thank you so much for your help; the explanation is by far the most valuable part.

PS -- I'm impressed about you knowing this was WRT a FITS library.

Re: SPARK prooving an array of Positives.

[Optikos]

On Tuesday, July 30, 2019 at 11:35:54 AM UTC-5, Shark8 wrote:
> I have a bit of a problem getting the SPARK provers to accept that a postcondition cannot fail. Given the following in a spec file:
> 
>     Type Axis_Count is range 0..999   with Size => 10;
>     Type Axis_Dimensions is Array (Axis_Count range <>) of Positive
>       with Default_Component_Value => 1;
>     Subtype Primary_Data_Array is Axis_Dimensions(1..999);
>     Subtype Random_Groups_Data is Axis_Dimensions(1..998);
> 
>     Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64;
> 
> and the following in the implementation:
> 
>     Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64 is
>         Max : Constant := Positive'Last;
>         Function First return Interfaces.Unsigned_64 is
>           ( Interfaces.Unsigned_64( Item( Item'First ) ) )
>           with Inline, Pre => Item'Length > 0, Post => First'Result <= Max;
>         Function Last return Interfaces.Unsigned_64 is
>             ( Interfaces.Unsigned_64( Item( Item'Last ) ) )
>           with Inline, Pre => Item'Length > 0, Post => Last'Result  <= Max;
>         use all type Interfaces.Unsigned_64;
>     Begin
> 	case Item'Length is
> 	   when 0      => return 1;
> 	   when 1      => return First;
> 	   when 2      => return First * Last;

As per the Axis_Value restriction to 32-bit modular-arithmetic integer portion of Brad Moore's more elaborate rewrite in his reply, the when-2 clause in Shark8's version could pessimistically be construed to be as much as a 128-bit integer when multiplying two Interfaces.Unsigned_64 modular-arithmetic integers together.  I suspect that that overt revelation to SPARK regarding 32-bit multiplicands is the main corrective act among Brad Moore's multiple edits.  I do admire how SPARK automatedly figured out (apparently via term replacement) in Brad Moore's variant that
> when 2      => return Result_Value (First) * Result_Value (Last);
could be rewritten equivalently as
when 2      => return Result_Value (First * Last);
in order to make obvious the logical deduction of lack-of-overflow-of-64-bit-unsigneds-due-to-multiplying-two-mere-32-bit-unsigneds possible in this proof.

> 	   when others =>
> 	    Declare
> 		Middle : Constant Axis_Count := Item'Length/2 + Item'First;
> 		Subtype Head is Axis_Count range Item'First..Middle;
> 		Subtype Tail is Axis_Count range Axis_Count'Succ(Middle)..Item'Last;
> 	    Begin
> 		Return EF(Item(Head)) * EF(Item(Tail));
> 	    End;
> 	end case;
>     End EF;
> 
> the SPARK prover is issuing warnings that the postconditions might fail.
> "medium: postcondition might fail, cannot prove First'Result <= Max (e.g. when First'Result = 0)"
> But this is impossible given that the element-type is Positive and the precondition states there is at least one element. Does anyone know why this is happening? (And how to fix it?)