Aptos Framework Move Prover 实战指南：验证超时、Boogie 内部错误与 Prover 测试控制策略-开发者社区

Aptos Framework Move Prover 实战指南：验证超时、Boogie 内部错误与 Prover 测试控制策略

【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core

本篇技术指南基于仓库内的 FRAMEWORK-PROVER-GUIDE.md 展开，面向需要为aptos-move/framework目录下的 Move 代码编写或维护形式化规约（spec）的开发者。指南覆盖 Move Prover 的超时处理、Boogie 内部错误的规避手法，以及本地跳过 prover 测试的完整命令，并结合 tests/move_prover_tests.rs 与 src/prover.rs 的源码实现，说明这些规则背后的实际执行机制，帮助你在修改框架代码时快速定位并绕开验证瓶颈。

Prover 测试在框架仓库中的角色

在aptos-move/framework仓库中，Prover 测试是合入门槛（land-blockers）：任何修改了framework目录下 Move 代码或规约的 PR，都必须通过move prover的验证。测试入口位于 tests/move_prover_tests.rs，其中定义了四个核心测试函数，分别对四个框架包执行完整验证：

move_framework_prover_tests：验证aptos-framework主包（move_prover_tests.rs#L167-L170）
move_token_prover_tests：验证aptos-token包
move_aptos_stdlib_prover_tests：验证aptos-stdlib包
move_stdlib_prover_tests：验证move-stdlib包

每个测试通过run_prover_for_pkg调用ProverOptions::prove（实现见 src/prover.rs#L139-L164），以默认的编译与语言版本（CompilerVersion::latest_stable()与LanguageVersion::latest_stable()）构建模型并运行验证。验证失败时测试直接 panic，因此 Prover 测试在 CI 中表现为硬门槛。

本地跳过 Prover 测试

完整跑一遍 prover 非常耗时。为了日常开发效率，原指南给出的本地跳过命令是：

cargo test --release -p aptos-framework -- --skip prover

该命令依赖cargo test的--skip过滤参数：测试函数名中包含prover的（如上述四个测试）会被整体跳过。这一建议同样被测试源码印证——move_prover_tests.rs#L56-L68 中的assert_prover_tools_available在未配置外部工具时给出的 panic 信息里，也明确提示了use "-- --skip prover" to filter out the prover tests。

注意区分两种场景：

本地开发、未安装 Boogie/Z3：直接跳过 prover 测试是推荐做法；
PR 合并前：prover 测试仍必须完整通过，不能长期以 skip 代替验证。

外部工具依赖

原指南的 Installation 一节指向 aptos.dev 上的 Move Prover 安装文档（build/cli/setup-cli/install-move-prover）。从测试源码可以确认安装完成的可验证标志：测试在运行前会检查环境变量BOOGIE_EXE、Z3_EXE（未启用 cvc5 时）或CVC5_EXE（启用 cvc5 时），三者任一缺失即 panic 并指回本指南（move_prover_tests.rs#L56-L68）。也就是说，安装成功的判据是：move prover可用，且 Boogie 与 SMT 求解器（Z3 或 CVC5）的二进制路径已通过对应环境变量暴露给进程。

验证超时：识别原因与 pragma 豁免

超时行为与默认时限

当 prover 无法在指定时间内完成某个验证任务时（默认 40 秒），它会直接退出并产生错误信息。这里的"时间"作用于单个验证条件（VC）级别，对应ProverOptions中的vc_timeout字段，其定义为“A (soft) timeout for the solver, per verification condition, in seconds”（src/prover.rs#L60-L62）。

标准处理手法：pragma verify = false 加 TODO

原指南给出的标准处理方式是：在导致超时的 spec 中加入pragma verify = false，并附上TODO注释，说明留给 prover 开发者调试的原因：

spec foo { pragma verify = false; // TODO: set to false because of timeout }

这不是仓库中的空谈——框架规约里有大量真实用例。例如 aptos_governance.spec.move 中多处出现：

pragma verify = false; // TODO: set because of timeout (property proved).

此外还存在一种变体：当属性本身可以证明、只是默认时限不够时，仓库中会改用verify_duration_estimate提高时限而非整体豁免，例如 account.spec.move#L316：

pragma verify_duration_estimate = 120; // TODO: set because of timeout (property proved)

两者的取舍可以概括为：属性可证但慢 → 提高 duration estimate；属性难证或证明方向有争议 →verify = false豁免，无论哪种都保留 TODO 以便后续跟进。

超时参数在测试链路中的调节方式

从源码结构看，测试链路还暴露了一组环境变量（move_prover_tests.rs#L15-L19），在构建测试选项时读取（move_prover_tests.rs#L40-L52）：

环境变量	作用
`MVP_TEST_VC_TIMEOUT`	覆盖`vc_timeout`，即单 VC 的软超时秒数
`MVP_TEST_DISALLOW_TIMEOUT_OVERWRITE`	置 1 后禁用全局超时的自动改写（对应`disallow_global_timeout_to_be_overwritten`）
`MVP_TEST_INCONSISTENCY`	置 1 启用`check_inconsistency`，通过注入不可满足断言检查规约的一致性
`MVP_TEST_UNCONDITIONAL_ABORT_AS_INCONSISTENCY`	置 1 后将 abort 也视为不一致，需与上一项配合使用

排查超时时，可以临时调大MVP_TEST_VC_TIMEOUT观察目标 VC 是"慢"还是"卡死"，再决定采用 duration estimate 还是豁免。

Boogie 内部错误的定位与规避

prover 自身的 bug 经常以boogie internal errors的形式出现，这与"规约写错了"导致的普通验证失败有本质区别。原指南的处理流程是：

定位：先确定是哪份 spec 触发了该问题；
规避：注释掉相关 spec；如果根因在 Move 代码侧（例如foo.move），则在对应的foo.spec.move（不存在则新建）中添加模块级豁免：

spec module { pragma verify = false; // TODO: see issue <url> }

与超时豁免相比，这里有两点差异值得注意：

豁免粒度是模块级（spec module），因为内部错误往往无法精确归因到单个 spec 块；
TODO 注释中应包含对应 GitHub issue 的 URL，并随即向 prover 团队提交 issue 跟踪修复。这保证了豁免不是静默吞掉问题，而是有明确的修复闭环。

用 Prover.toml 持久化验证选项

命令行参数之外，ProverOptions支持从包目录下的Prover.toml加载基线配置：convert_options会检查package_path.join("Prover.toml")，存在则通过Options::create_from_toml_file读取，再与命令行/代码中传入的选项合并（src/prover.rs#L241-L313）。

仓库中现存的真实示例是 aptos-framework/Prover.toml：

[prover] borrow_natives = ["storage_slot::borrow_storage_slot_resource_mut"]

它把storage_slot::borrow_storage_slot_resource_mut声明为借用型 native，影响 prover 对该 native 的验证建模。合并逻辑是"显式传入值优先、未传则回落 toml 值"（如proc_cores、vc_timeout、error_limit均如此），因此Prover.toml适合作为包的长期稳定配置，而临时调参仍建议走ProverOptions的字段或测试环境变量。

值得了解的常用 ProverOptions 字段

以下选项定义于 src/prover.rs#L24-L135，与超时/错误排查直接相关：

filter：只把文件名匹配的模块作为验证目标，类似cargo test的过滤语义；
only：把验证范围缩小到mod::func或func，用于逐函数排查；
proc_cores：并发 Boogie 进程上限，也可用环境变量MVP_PROC_CORES设置；
cvc5：切换为 cvc5 求解器后端（需设置CVC5_EXE），换用不同求解器有时能绕开 Z3 侧的内部错误；
split_vcs_by_assert：为函数内每条断言生成独立 VC，便于诊断"函数里哪一条 assert 导致超时"；
check_inconsistency/unconditional_abort_as_inconsistency：规约一致性检查，前者通过注入不可满足断言实现；
loop_unroll/keep_loops：控制循环展开与是否原样交给求解器，影响含循环函数的可证性。

另外，benchmark模式会把每个验证目标独立计时，写出prover_benchmark.fun_data与对比用的prover_benchmark.svg（src/prover.rs#L323-L393），是定位性能回退的现成工具。

Aptos 专属 native 的 Boogie 支持

一个容易忽视但必要的细节：对任何依赖move-stdlib的包运行 prover 前，必须调用configure_aptos_custom_natives，把 src/aptos-natives.bpl 作为自定义 native 模板注入 Boogie 后端。源码注释说明，缺失该步骤会导致$1_cmp_Ordering类型声明与cmp_vector_instances公理缺失，进而引发 Boogie 编译错误（src/prover.rs#L403-L416）。ProverOptions::prove_to在调用run_move_prover_with_model_v2前会自动完成这一步（src/prover.rs#L231），因此走框架内测试链路时无需手动处理；但如果你在框架外自行拼装 prover 调用链，需要留意此依赖。

基线式 prover 测试：错误输出也可被"冻结"

除 panic-on-error 的run_prover_for_pkg外，tests/move_prover_tests.rs 还提供了run_prover_for_pkg_with_baseline：它把 prover 的诊断输出（含错误信息）与.exp基线文件比对，prover 报错本身不会失败测试，只有输出相对基线变化才失败（move_prover_tests.rs#L97-L130）。其机制要点：

开启stable_test_output，对签名地址、临时 ID 等非确定值做红action（redact）处理，保证基线跨机器稳定；
sanitize_output将临时目录路径归一为<TEMPDIR>、将框架 crate 路径归一为<FRAMEWORK_DIR>（move_prover_tests.rs#L144-L156）；
设置环境变量UB=1（或UPBL=1/UPDATE_BASELINE=1）可从当前输出重新生成基线。

对于"预期会失败但错误信息需要被锁定"的场景（例如故意构造的坏规约用例），这套机制比直接 panic 的断言更精细。

规约编写参考与排查清单

编写 spec 的完整语法与最佳实践，原指南指向 aptos.dev 上的 Move Prover Book（prover-guides 章节），本仓库不再重复该文档内容。结合上述源码证据，日常排查可以按如下清单执行：

超时：先用only/filter缩小目标函数，必要时开split_vcs_by_assert定位到具体断言；能证则加pragma verify_duration_estimate，难证则pragma verify = false+ TODO；
boogie internal error：注释掉嫌疑 spec 二分定位，确认模块级根因后加spec module { pragma verify = false; }+ 带 issue URL 的 TODO，并向 prover 团队提 issue；
换求解器：尝试cvc5后端（设置CVC5_EXE），排除 Z3 侧 bug；
性能回退：跑benchmark模式对比prover_benchmark.fun_data；
本地提效：未装外部工具或临时不需要验证时，cargo test --release -p aptos-framework -- --skip prover。