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-L170move_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#L316pragma 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_overwrittenMVP_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.svgsrc/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 等非确定值做红actionredact处理保证基线跨机器稳定sanitize_output将临时目录路径归一为TEMPDIR、将框架 crate 路径归一为FRAMEWORK_DIRmove_prover_tests.rs#L144-L156设置环境变量UB1或UPBL1/UPDATE_BASELINE1可从当前输出重新生成基线。对于预期会失败但错误信息需要被锁定的场景例如故意构造的坏规约用例这套机制比直接 panic 的断言更精细。规约编写参考与排查清单编写 spec 的完整语法与最佳实践原指南指向 aptos.dev 上的 Move Prover Bookprover-guides 章节本仓库不再重复该文档内容。结合上述源码证据日常排查可以按如下清单执行超时先用only/filter缩小目标函数必要时开split_vcs_by_assert定位到具体断言能证则加pragma verify_duration_estimate难证则pragma verify false TODOboogie 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。以上所有规则最终都落到两个事实prover 测试是framework目录改动不可绕过的合入门槛而超时与内部错误的豁免手段verify false TODO 注释是仓库中已大规模沿用的既定约定遵循它们可以既保住 PR 的可合并性又为后续修复保留完整线索。【免费下载链接】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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考