Verus项目中via_fn证明函数中assert by {}的行为分析

Verus是一种用于Rust的形式化验证工具，它允许开发者编写可验证的正确性证明。最近在Verus项目中发现了一个关于#[via_fn]证明函数中assert(...) by {}行为的有趣现象，这涉及到验证系统的健全性(soundness)问题。

问题现象

在Verus的#[via_fn]证明函数中，当使用assert(false) by {}这样的断言时，验证过程会意外地通过，而不会报告任何错误。这与常规情况下的行为不符，因为false显然是一个不可满足的条件。

示例代码如下：

#[via_fn]
proof fn test_decr(i: nat) {
    assert(false) by {};
}

正常情况下，这样的断言应该导致验证失败，但实际上验证器会报告"2 verified, 0 errors"，这意味着验证过程被意外地接受了。

技术背景

Verus中的#[via_fn]属性用于指定一个证明函数作为另一个规格函数的终止性证明。assert(...) by {}语法通常用于提供一个空证明块，表示该断言不需要额外证明。

在Verus的实现中，函数体在转换为中间表示时会创建一个函数上下文(fun_ctx)，其中包含一个checking_spec_preconditions标志。当前实现中，对于via_fn函数，这个标志被硬编码设置为true。

问题根源

问题的核心在于checking_spec_preconditions标志的设置。当这个标志为true时，验证器会跳过某些验证步骤，导致assert(...) by {}实际上等同于调用了admit()（即无条件接受断言）。

在AST到SST（结构化语法树）的转换过程中，via_fn证明函数的上下文被创建时强制设置了checking_spec_preconditions=true。这种设置原本可能是为了处理规格函数的前置条件检查，但意外影响了证明函数内部的断言验证行为。

影响分析

这种行为的直接影响是可能导致验证系统的不健全(unsound)，因为开发者可能无意中使用了看似无害的assert(...) by {}语法，但实际上却跳过了重要的验证步骤。在终止性证明等关键验证场景中，这可能导致错误的验证结果。

解决方案

修复此问题需要仔细考虑checking_spec_preconditions标志在via_fn上下文中的正确设置。可能的解决方案包括：

1. 对于via_fn证明函数，将checking_spec_preconditions设置为false
2. 修改验证逻辑，确保即使checking_spec_preconditions为true，assert(...) by {}也不会被无条件接受
3. 引入专门的上下文标志来处理via_fn函数的特殊情况

最佳实践建议

在问题修复前，开发者在使用#[via_fn]时应当：

1. 避免在证明函数中使用assert(...) by {}语法
2. 对于关键断言，总是提供完整的证明块
3. 特别注意终止性证明中的断言验证结果

Verus团队正在积极解决此问题，未来的版本将会提供更健全的行为。开发者应关注更新日志，了解此问题的修复情况。

结论

形式化验证工具的正确性至关重要。Verus项目中发现的这个边缘案例提醒我们，即使是精心设计的验证系统也可能存在微妙的健全性问题。开发者应当理解工具的行为特性，并在关键证明中采用防御性的验证策略。Verus团队对此问题的响应展示了他们对验证系统健全性的高度重视。