Verus语言中call_requires/call_ensures对普通函数调用的行为分析

Verus是一种用于Rust的形式化验证工具，它允许开发者为函数指定前置条件和后置条件。在Verus中，call_requires和call_ensures是两个重要的验证原语，分别用于检查函数调用的前置条件是否满足和验证函数调用的后置条件是否成立。

问题现象

在Verus中，当直接调用普通函数时，call_requires和call_ensures的行为与预期不符。具体表现为：

1. 对于call_ensures，即使函数调用成功返回，验证器也无法自动证明后置条件成立
2. 对于call_requires，即使显式假设前置条件成立，验证器仍然会拒绝函数调用

技术分析

这种现象的根本原因在于Verus对普通函数调用和函数指针调用的处理方式不同。Verus内部有两种编码机制：

1. 对于直接函数调用，Verus采用更严格的验证方式
2. 对于通过函数指针/函数变量的调用，Verus会启用更灵活的函数特质（trait）编码机制

解决方案

通过将函数赋值给变量再调用，可以强制Verus使用更灵活的函数特质编码机制，从而解决上述问题。这种间接调用方式能够正确识别call_requires和call_ensures的语义。

实际应用

在实际验证代码中，建议采用以下模式：

// 将函数赋值给变量
let f = target_function;
// 通过变量调用函数
let result = f(args);
// 此时call_ensures能够正确验证
assert(call_ensures(target_function, (args,), result));

对于需要验证前置条件的情况：

// 假设前置条件成立
assume(call_requires(target_function, (args,)));
// 将函数赋值给变量
let f = target_function;
// 通过变量调用函数
f(args);

结论

Verus对直接函数调用和间接函数调用的不同处理机制导致了call_requires和call_ensures行为上的差异。理解这一机制对于编写可验证的Verus代码非常重要。在实际开发中，当遇到相关验证问题时，可以考虑通过函数变量间接调用的方式来规避限制。