使用libsparkcrypto库时无法证明SHA256函数相等性断言的技术求助

这个问题的核心原因是：SPARK证明器默认不知道LSC.SHA2.Hash_SHA256是一个纯函数（即输出仅由输入决定，无副作用，相同输入必然返回相同输出）。你需要明确告诉证明器这个函数的行为特性，它才能推导出当X=Y时，哈希结果必然相等。

解决方案步骤 #

1. 为Hash_SHA256添加纯函数契约 #

在你的包规范（testpackage.ads）中，我们可以通过重命名函数并添加Pure_Function编译指示，或者直接声明公理来约束Hash_SHA256的纯特性。

修改后的testpackage.ads如下：

with LSC.Types; use LSC.Types;
with LSC.SHA2; use LSC.SHA2;
package TestPackage with SPARK_Mode is

   -- 重命名哈希函数并标记为纯函数，告诉SPARK它的输出仅依赖输入
   function Hash_SHA256 (Data : Bytes) return SHA256_Hash_Type
     renames LSC.SHA2.Hash_SHA256;
   pragma Pure_Function (Hash_SHA256);

   -- 可选：如果Pure_Function不够，用更明确的公理约束输入输出关系
   -- axiom Hash_SHA256_Equality :
   --   for all X, Y : Bytes =>
   --     X = Y => Hash_SHA256(X) = Hash_SHA256(Y);

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

2. 验证断言逻辑 #

有了纯函数的契约后，证明器已经能理解X=Y时哈希结果必然相等，你的原断言可以正常被验证。如果需要，也可以简化函数逻辑：

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 (Hash_SHA256 (X) = Hash_SHA256 (Y)); -- 现在证明器能验证这个断言
      return True;
   end if;
   return Hash_SHA256 (X) = Hash_SHA256 (Y);
end Is_Equal;
end TestPackage;

为什么这能解决问题？ #

SPARK的证明器不会假设第三方库函数的行为——哪怕SHA256算法本身是纯的，证明器需要明确的契约来确认这一点。Pure_Function编译指示告诉证明器：

• 函数没有副作用
• 相同输入一定会返回相同输出

如果Pure_Function不足以让证明器推导（比如某些复杂场景），你可以用注释里的公理Hash_SHA256_Equality，直接声明"若X等于Y，则它们的哈希结果必相等"的逻辑，让证明器直接使用这个规则。

验证修改 #

重新运行gnatprove：

gnatprove -Pyour_project.gpr -j0 --proof=all

此时那个未证明的断言应该会被标记为已验证。

内容的提问来源于stack exchange，提问作者WhaleDancer