Verus项目中时间统计功能对spinoff_prover查询的遗漏问题分析

Verus是一个用于Rust的形式化验证工具，它提供了--time-expanded参数来输出详细的验证时间统计信息。然而，当前版本中存在一个关于spinoff_prover查询的时间统计遗漏问题，这会影响开发者对验证性能的准确评估。

问题现象

在Verus项目中，当使用#[verifier(spinoff_prover)]属性标记证明函数时，这些函数的验证时间不会被包含在--time-expanded的输出统计中。具体表现为：

1. 普通证明函数（如示例中的bar1）的验证时间会被正确统计
2. 使用spinoff_prover属性的证明函数（如示例中的bar2）的验证时间完全缺失
3. 只有当模块中包含非spinoff_prover函数时，该模块的时间统计才会出现

技术背景

spinoff_prover是Verus中的一个重要特性，它允许将特定的证明任务分离到独立的验证过程中。这种机制常用于处理复杂的非线性算术证明，或者需要特殊处理的验证场景。

Verus的时间统计系统基于"桶"(bucket)的概念组织验证时间数据，每个桶对应一个统计单元（如模块或函数）。当前实现中，系统会过滤掉仅包含函数的桶，这导致了纯spinoff_prover函数模块的统计遗漏。

问题根源

深入分析代码实现，问题出在时间统计的过滤逻辑上：

1. 系统首先将所有验证任务按模块和函数分类到不同的桶中
2. 然后过滤掉那些只包含函数级别的桶
3. 由于spinoff_prover函数会被单独处理，它们往往只存在于函数级别的桶中
4. 因此这些函数的验证时间就被错误地过滤掉了

值得注意的是，使用by (nonlinear_arith)等内置策略的证明虽然也会触发spinoff_prover行为，但由于它们属于系统内置机制，仍然会被统计到时间数据中。

解决方案

针对这个问题，开发团队提出了两种可能的解决方案：

1. 临时方案：当模块中只有spinoff_prover证明函数时，仍然保留该模块的时间统计信息。这种方法实现简单但不够优雅。

2. 统一方案：重构时间统计系统，统一以模块为基本单位进行统计，不再区分函数级别的桶。这种方法更符合实际使用场景，因为开发者通常更关心模块级别的验证性能。

影响与建议

这个问题会影响开发者：

1. 对项目整体验证时间的准确评估
2. 对spinoff_prover函数性能的监控
3. 对验证热点模块的识别

建议开发者在使用spinoff_prover时注意这个问题，或者等待官方修复。同时，可以通过在模块中添加非spinoff_prover函数的临时方案来确保时间统计的完整性。

总结

Verus的时间统计功能对spinoff_prover查询的遗漏是一个需要注意的实现细节问题。理解这一问题的原因和影响，有助于开发者更准确地评估验证性能，并做出相应的优化决策。开发团队已经意识到这个问题，并计划在后续版本中提供更完善的解决方案。