Failed assert that libsparkcrypto SHA256 results are equal

Question

Summary of my issue

I am using the libsparkcrypto library for my SHA256 function. I am finding that I cannot Assert that x = y implies Sha256(x) = Sha256(y). Any help would be greatly appreciated.

Code

testpackage.adb

package body TestPackage with
 SPARK_Mode
is
   
   function Is_Equal (X, Y : LSC.Types.Bytes) return Boolean is
   begin
      if X = Y then
         pragma Assert (LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y));
         return True;
      end if;
      return (LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y));
   end Is_Equal;

end TestPackage;

testpackage.ads

with LSC.Types; use LSC.Types;
with LSC.SHA2;

package TestPackage with
 SPARK_Mode
is
   
   function Is_Equal (X, Y : LSC.Types.Bytes) return Boolean with
     Post => Is_Equal'Result = (LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y));
   
end TestPackage;

Output

The error i receive is:

testpackage.adb:8:25: medium: assertion might fail, cannot prove LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y) [possible explanation: subprogram at testpackage.ads:8 should mention X and Y in a precondition][#0]

My gnatprove.out:

Summary of SPARK analysis
=========================

-------------------------------------------------------------------------------------------
SPARK Analysis results        Total      Flow   CodePeer     Provers   Justified   Unproved
-------------------------------------------------------------------------------------------
Data Dependencies                 .         .          .           .           .          .
Flow Dependencies                 .         .          .           .           .          .
Initialization                    .         .          .           .           .          .
Non-Aliasing                      .         .          .           .           .          .
Run-time Checks                   6         .          .    6 (CVC4)           .          .
Assertions                        1         .          .           .           .          1
Functional Contracts              1         .          .    1 (CVC4)           .          .
LSP Verification                  .         .          .           .           .          .
Termination                       .         .          .           .           .          .
Concurrency                       .         .          .           .           .          .
-------------------------------------------------------------------------------------------
Total                             8         .          .     7 (88%)           .    1 (13%)


max steps used for successful proof: 1

Analyzed 2 units
in unit main, 0 subprograms and packages out of 1 analyzed
  Main at main.adb:8 skipped
in unit testpackage, 2 subprograms and packages out of 2 analyzed
  TestPackage at testpackage.ads:4 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  TestPackage.Is_Equal at testpackage.ads:8 flow analyzed (0 errors, 0 checks and 0 warnings) and not proved, 7 checks out of 8 proved

Answer 1

While this is not an answer to the question, some investigation on a smaller example shows that the issue is not specific to the LSC.SHA2.Hash_SHA256 function in the libsparkcrypto library. It looks like that there is a general difficulty in proving "purity" of functions with an array type parameter. Functions with a scalar type parameter on the other hand are proven as expected.

So the problem could be some missing conditions on the array, the solver timeout being too short or just some current inability of SPARK to proof something like this (see, for example, section 7.8.3 in the SPARK UG). Regarding the missing conditions: I'm not sure (yet) what these missing conditions could be, I've added quite a bunch, but none seem to help.

If you are a proof expert, then you could investigate the problem further by inspecting the "goal" that failed in the manual proof environment (see also section 7.1.8 in the SPARK UG for details). Unfortunately, I'm missing the appropriate PhD here to understand this part of the SPARK tooling and be of any help on this ;-).

pkg.ads

package Pkg with SPARK_Mode, Pure is 
   
   --------------------------------------------
   -- Functions with a scalar type parameter --
   --------------------------------------------
   
   function Fcn_Scalar_1 (X : Integer) return Integer;
   
   function Fcn_Scalar_2 (X : Integer) return Integer
     with Pure_Function;

   function Fcn_Scalar_3 (X : Integer) return Integer
     with 
       Global  => null, 
       Depends => (Fcn_Scalar_3'Result => X);

   function Fcn_Scalar_4 (X : Integer) return Integer
     with Post => Fcn_Scalar_4'Result = X; 
   
   --------------------------------------------
   -- Functions with an array type parameter --
   --------------------------------------------
   
   type Arr is array (Natural range <>) of Integer;
   
   function Fcn_Array_1 (X : Arr) return Integer;
   
   function Fcn_Array_2 (X : Arr) return Integer
     with Pure_Function;

   function Fcn_Array_3 (X : Arr) return Integer
     with       
       Global  => null, 
       Depends => (Fcn_Array_3'Result => X);

   function Fcn_Array_4 (X : Arr) return Arr
     with Post => Fcn_Array_4'Result = X; 

end Pkg;

test.ads

with Pkg; use Pkg;

package Test with SPARK_Mode is
   
   --  Is_Equal_Scalar_1 : Postcondition proved.
   --  Is_Equal_Scalar_2 : Postcondition proved.
   --  Is_Equal_Scalar_3 : Postcondition proved. 
   --  Is_Equal_Scalar_4 : Postcondition proved.  
   
   function Is_Equal_Scalar_1 (X, Y : Integer) return Boolean is
     (if X = Y then True else Fcn_Scalar_1 (X) = Fcn_Scalar_1 (Y))
       with Post => Is_Equal_Scalar_1'Result = (Fcn_Scalar_1 (X) = Fcn_Scalar_1 (Y));
   
   function Is_Equal_Scalar_2 (X, Y : Integer) return Boolean is
     (if X = Y then True else Fcn_Scalar_2 (X) = Fcn_Scalar_2 (Y))
       with Post => Is_Equal_Scalar_2'Result = (Fcn_Scalar_2 (X) = Fcn_Scalar_2 (Y));
   
   function Is_Equal_Scalar_3 (X, Y : Integer) return Boolean is
     (if X = Y then True else Fcn_Scalar_3 (X) = Fcn_Scalar_3(Y))
       with Post => Is_Equal_Scalar_3'Result = (Fcn_Scalar_3 (X) = Fcn_Scalar_3 (Y));
   
   function Is_Equal_Scalar_4 (X, Y : Integer) return Boolean is
     (if X = Y then True else Fcn_Scalar_4 (X) = Fcn_Scalar_4(Y))
       with Post => Is_Equal_Scalar_4'Result = (Fcn_Scalar_4 (X) = Fcn_Scalar_4 (Y));
  
   --  Is_Equal_Array_1 : Postcondition NOT proved.
   --  Is_Equal_Array_2 : Postcondition NOT proved.
   --  Is_Equal_Array_3 : Postcondition NOT proved.
   --  Is_Equal_Array_4 : Postcondition proved, but only because of the postcondition on Fcn_Array_4.
   
   function Is_Equal_Array_1 (X, Y : Arr) return Boolean is
     (if X = Y then True else Fcn_Array_1 (X) = Fcn_Array_1 (Y))
         Pre  => X'First = 0 and Y'First = 0 and X'Length = Y'Length and X'Length > 0 and Y'Length > 0,
         Post => Is_Equal_Array_1'Result = (Fcn_Array_1 (X) = Fcn_Array_1 (Y));
   
   function Is_Equal_Array_2 (X, Y : Arr) return Boolean is
     (if X = Y then True else Fcn_Array_2 (X) = Fcn_Array_2 (Y))
       with 
         Pre  => X'First = 0 and Y'First = 0 and X'Length = Y'Length and X'Length > 0 and Y'Length > 0,
         Post => Is_Equal_Array_2'Result = (Fcn_Array_2 (X) = Fcn_Array_2 (Y));
   
   function Is_Equal_Array_3 (X, Y : Arr) return Boolean is
     (if X = Y then True else Fcn_Array_3 (X) = Fcn_Array_3 (Y))
       with 
         Pre  => X'First = 0 and Y'First = 0 and X'Length = Y'Length and X'Length > 0 and Y'Length > 0,
         Post => Is_Equal_Array_3'Result = (Fcn_Array_3 (X) = Fcn_Array_3 (Y));
   
   function Is_Equal_Array_4 (X, Y : Arr) return Boolean is
     (if X = Y then True else Fcn_Array_4 (X) = Fcn_Array_4 (Y))
       with Post => Is_Equal_Array_4'Result = (Fcn_Array_4 (X) = Fcn_Array_4 (Y));

end Test;

output (gnatprove)

$ gnatprove -Pdefault.gpr --level=2 -j0 -u test.ads --report=statistics
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
test.ads:12:21: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
test.ads:16:21: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
test.ads:20:21: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
test.ads:24:21: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
test.ads:35:18: medium: postcondition might fail, cannot prove Is_Equal_Array_1'Result = (Fcn_Array_1 (X) = Fcn_Array_1 (Y)) (e.g. when X = (others => 0) and X'First = 0 and X'Last = 0 and Y = (others => 0) and Y'First = 0 and Y'Last = 0)
test.ads:41:18: medium: postcondition might fail, cannot prove Is_Equal_Array_2'Result = (Fcn_Array_2 (X) = Fcn_Array_2 (Y)) (e.g. when X = (others => 0) and X'First = 0 and X'Last = 0 and Y = (others => 0) and Y'First = 0 and Y'Last = 0)
test.ads:47:18: medium: postcondition might fail, cannot prove Is_Equal_Array_3'Result = (Fcn_Array_3 (X) = Fcn_Array_3 (Y)) (e.g. when X = (others => 0) and X'First = 0 and X'Last = 0 and Y = (others => 0) and Y'First = 0 and Y'Last = 0)
test.ads:51:21: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
Summary logged in /obj/gnatprove/gnatprove.out

---

UPDATE

On second thought, there is more. While still not able to solve the problem, I realize that preconditions on the Is_Equal functions are mandatory in the case of array types. This is because of how the equality operator for arrays behave in Ada. The equality operator on arrays does not take into account the index bounds (RM 4.5.2 (18)), it only checks the array lengths and its component values. Hence, the following arrays, A1 and A2, are considered equal:

type Arr is array (Natural range <>) of Integer;

A1 : constant Arr (0 .. 3) := (1, 2, 3, 4);
A2 : constant Arr (1 .. 4) := (1, 2, 3, 4);   --  Bounds on index differ.

Now define the simple function First_Index as being:

function First_Index (A : Arr) return Integer is (A'First);

This function returns the array's index lower bound. Unfortunately gnatprove will not be able to prove an Is_Equal function for this First_Index function with only a postcondition for obvious reasons.

function Is_Equal (X, Y : Arr) return Boolean is
     (if X = Y then True else First_Index (X) = First_Index (Y))
       with Post => Is_Equal'Result = (First_Index (X) = First_Index (Y));

Hence, a precondition is mandatory as the result of the "pure" function may depend on the bounds of the array. With this precondition, the function can be proven (see below). For the cases in the earlier example, this does not work.

main.adb

with Ada.Text_IO; use Ada.Text_IO;

procedure Main with SPARK_Mode is
   
   type Arr is array (Natural range <>) of Integer;   
   
   function First_Index (A : Arr) return Integer is (A'First);
   
   function Is_Equal (X, Y : Arr) return Boolean is
     (if X = Y then True else First_Index (X) = First_Index (Y))
       with  
         Pre  => X'First = 0 and Y'First = 0,
         Post => Is_Equal'Result = (First_Index (X) = First_Index (Y));   
   
   A1 : constant Arr (0 .. 3) := (1, 2, 3, 4);
   A2 : constant Arr (1 .. 4) := (1, 2, 3, 4);   --  Bounds on index differ.
   
begin
   if (A1 = A2) then
      Put_Line ("Equal");
   else
      Put_Line ("Not Equal");
   end if;
end Main;

output (main)

Equal

output (gnatprove)

$ gnatprove -Pdefault.gpr --level=1 -j0 -u main.adb --report=statistics
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:16:18: info: postcondition proved (CVC4: 2 VC in max 0.0 seconds and 1 step)
Summary logged in obj/gnatprove/gnatprove.out

Answer 2

Possible explanation (yes, I know, dad joke). You didn't set any precondition checks for X and Y, thus SPARK can't verify them. Even if they are that same type. Try to set any checks and see what happen. Generally, SPARK likes when everything is in contracts, more is better.