问题描述
我的问题摘要
我将 libsparkcrypto library 用于我的 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
解决方法
虽然这不是问题的答案,但对较小示例的一些调查表明该问题并非特定于 libsparkcrypto 库中的 LSC.SHA2.Hash_SHA256
函数。似乎证明具有数组类型参数的函数的“纯度”存在普遍困难。另一方面,带有标量类型参数的函数被证明是符合预期的。
所以问题可能是数组上缺少一些条件,求解器超时太短,或者只是 SPARK 目前无法证明这样的事情(例如,参见 SPARK UG 中的 7.8.3 部分) .关于缺失的条件:我不确定(还)这些缺失的条件是什么,我已经添加了很多,但似乎没有任何帮助。
如果您是证明专家,那么您可以通过检查在手动证明环境中失败的“目标”来进一步调查问题(有关详细信息,另请参阅 SPARK UG 中的 7.1.8 部分)。不幸的是,我在这里缺少合适的博士来理解 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
更新
仔细想想,还有更多。虽然仍然无法解决问题,但我意识到 Is_Equal
函数的先决条件在数组类型的情况下是强制性的。这是因为数组的相等运算符在 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,4); -- Bounds on index differ.
现在将简单函数 First_Index
定义为:
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,4);
A2 : constant Arr (1 .. 4) := (1,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
,
可能的解释(是的,我知道,爸爸的笑话)。您没有为 X 和 Y 设置任何前提条件检查,因此 SPARK 无法验证它们。即使它们是同一种类型。尝试设置任何检查,看看会发生什么。一般来说,SPARK 喜欢一切都在合同中,越多越好。