Dafny高阶恒等函数验证失败：f.reads前置条件无法证明

你遇到的问题是Dafny对堆读取偏函数（A ~> B类型）的高阶函数验证约束问题，直接定义恒等函数时，Dafny无法确认lambda表达式的reads子句是否符合内存安全规则。

问题复现 #

你的MCVE代码：

function Id<A, B>(f: A ~> B): A ~> B
{
    x reads f.reads(x) requires f.requires(x) => f(x)
}

在Dafny 4.11中报错：

Error: function precondition could not be proved
|
|     x reads f.reads(x) requires f.requires(x) => f(x)
|                    ^

解决方法 #

需要给Id函数本身添加reads声明和全域前置条件，来约束函数的读取范围，确保内部lambda的reads子句合法。修正后的代码如下：

function Id<A, B>(f: A ~> B): A ~> B
  reads f.reads
  requires forall x: A :: f.requires(x) ==> f.reads(x) <= this.reads
{
  x reads f.reads(x) requires f.requires(x) => f(x)
}

关键解释 #

1. reads f.reads：声明Id函数读取f自身的reads集合——因为f是堆函数，其reads信息存储在堆中，函数必须明确声明读取这部分内容。
2. 全域前置条件：forall x: A :: f.requires(x) ==> f.reads(x) <= this.reads，确保对于任何满足f前置条件的输入x，f.reads(x)是Id函数读取范围的子集。这一步让Dafny能验证lambda表达式中的reads f.reads(x)没有超出允许的内存读取范围。
3. 内部lambda的结构保持不变，因为它本身就是正确的恒等逻辑，只是缺少外层函数的约束来通过验证。

补充说明 #

即使替换为具体类型（如int ~> bool），同样需要添加这些约束。如果你的场景中f的reads集合不依赖输入x（即固定reads范围），可以简化前置条件，但对于通用的依赖x的偏函数，上述约束是必要的。

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