Не удалось подтвердить, что результаты libsparkcrypto SHA256 равны

Question

Резюме моей проблемы

Я использую библиотеку libsparkcrypto для своей функции SHA256. Я обнаружил, что не могу Assert который x = y подразумевает Sha256(x) = Sha256(y). Любая помощь будет принята с благодарностью.

Код

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;

Выход

Я получаю следующую ошибку:

testpackage.adb: 8: 25: medium: утверждение может завершиться ошибкой, не может подтвердить LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y) [возможное объяснение: подпрограмма на testpackage.ads:8 должна упоминать X и Y в предварительное условие] [# 0]

Мой 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

Хотя это не ответ на вопрос, некоторые исследования на небольшом примере показывают, что проблема не связана с LSC.SHA2.Hash_SHA256функция в библиотеке libsparkcrypto. Похоже, что в целом сложно доказать «чистоту» функций с параметром типа массива. С другой стороны, функции с параметром скалярного типа доказаны, как и ожидалось.

Таким образом, проблема может заключаться в некоторых пропущенных условиях в массиве, слишком коротком таймауте решателя или просто в некоторой текущей неспособности SPARK подтвердить что-то подобное (см., Например, раздел 7.8.3 в SPARK UG). Что касается отсутствующих условий: я (пока) не уверен, что это за недостающие условия, я добавил довольно много, но, похоже, ни одно из них не помогает.

Если вы являетесь экспертом по доказательству, то вы можете исследовать проблему дальше, проверив «цель», которая не удалась в среде ручного доказательства (подробности см. В разделе 7.1.8 в SPARK UG). К сожалению, мне здесь не хватает соответствующей докторской степени, чтобы понять эту часть инструментария SPARK и быть в этом полезной ;-).

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;

вывод (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

---

ОБНОВИТЬ

Если подумать, это еще не все. Хотя все еще не в состоянии решить проблему, я понимаю, что предварительные условия для функций являются обязательными в случае типов массивов. Это связано с тем, как в Ada ведет себя оператор равенства для массивов. Оператор равенства для массивов не принимает во внимание границы индекса ( RM 4.5.2 (18)), он проверяет только длину массива и значения его компонентов. Следовательно, следующие массивы, A1 и A2, считаются равными:

      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.

Теперь определите простую функцию как:

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

Эта функция возвращает нижнюю границу индекса массива. к несчастью gnatprove не сможет доказать Is_Equal функция для этого First_Index функция только с постусловием по очевидным причинам.

      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));

Следовательно, предусловие является обязательным, поскольку результат «чистой» функции может зависеть от границ массива. С этим предварительным условием функция может быть доказана (см. Ниже). Для случаев из предыдущего примера это не работает.

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;

вывод (основной)

      Equal

вывод (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

Возможное объяснение (да, я знаю, папа шутит). Вы не установили никаких предварительных условий для X и Y, поэтому SPARK не может их проверить. Даже если они одного типа. Попробуйте поставить какие-нибудь проверки и посмотрите, что получится. Вообще СПАРК любит, когда все в контрактах, чем больше, тем лучше.