Aptos MoveFlow Move Prover 证明编写指南：断言、引理归纳、触发器与 [weight = N] 实例化权重

Aptos MoveFlow Move Prover 证明编写指南：断言、引理归纳、触发器与 [weight = N] 实例化权重

【免费下载链接】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

本文基于 Aptos 仓库中 MoveFlow 插件的证明编写指导模板spec_lang_proofs.md展开，讲解 Move Prover 证明结构中assert、apply、触发器、calc与条件分案的用法，递归引理的良基（measure）下降规则，以及[weight = N]实例化权重的工作原理，并结合 Move 编译器前端move-model的源码实现，说明每条证明技巧在求解器侧到底如何被展开和计费。

文档定位：MoveFlow 插件中的一个共享证明指导片段

spec_lang_proofs.md位于 aptos-move/flow/cont/templates/spec_lang_proofs.md，是 MoveFlow（aptos-move/flow，Aptos 面向 Move 合约开发的 Claude Code 插件）模板树cont/中的一个共享片段。MoveFlow 的架构见 aptos-move/flow/CLAUDE.md：move-flow plugin <dir>子命令使用 Tera 模板引擎把cont/下的agents/、skills/、hooks/与templates/渲染为插件文件，其中模板内的{% include %}用于组合共享片段。

本片段在渲染链中的位置是：

1. cont/skills/move-prove/SKILL.md —— “move-prove” 技能（用 Move Prover 验证并诊断已有 Move 规约），它 include 了 verification_tasks.md 与 verification_ref.md；
2. verification_ref.md的第 4 行{% include "templates/spec_lang_proofs.md" %}引入本片段，与spec_editing_ref.md、toolchain_limits.md以及 “Move Prover reference”“Reading a counterexample”“Timeout strategy” 等章节共同组成验证参考；
3. 片段首行的{% if once(name="spec_lang_proofs") %}是 Tera 去重守卫，保证同一插件生成过程中该片段最多渲染一次。

值得注意的一个模板变量是evaluation_mode。插件生成入口 src/plugin/mod.rs 会把evaluation.evaluation_mode写入 Tera 上下文（context.insert("evaluation_mode", &evaluation.evaluation_mode)），本片段第 42 行据此渲染出两种措辞分支；评测侧的 harness 也依赖该标志，例如 evaluation/spec-inference/harness/schedule.py 会校验manifest.get("evaluation_mode") is not True才拒绝运行。也就是说，同一份证明指导在“普通使用”与“评测模式”下会生成措辞不同的assume纪律条款，下节详解。

何时引入证明结构（proof structure）

文档开宗明义给出引入时机：当一份正确合约超时（timeout），或者求解器找不到某个中间事实（intermediate fact）时，才引入显式证明结构。证明结构是“给求解器递台阶”的手段，不是默认写法——默认应让 Prover 直接对合约求反例/证明。

文档列出的五类证明构件是：

• assert e：暴露一个有用的子目标，且该断言本身必须被证明（它不是假设，而是一条新的证明义务）；
• apply lemma(args)：实例化一个已证明的引理（把它的ensures引入当前上下文）；
• forall x: T {trigger(x)} apply lemma(x)：带显式触发器地对引理做全称实例化；
• calc：记录一条等式或不等式链；
• 条件判断与数值分案（conditionals and value splits）：把实质不同的证明情形拆开。

文档同时给出风格基线：优先选择与失败义务（failing obligation）直接绑定的小断言和小引理；引理是“已证明的模块级命题，而不是公理（a proved module-level proposition, not an axiom）”。

从源码结构看，这些构件在前端就被翻译成了明确的可执行动作。move-model的 spec_translator.rs 中，Proof::Calc的每一步（lhs op rhs）都被包装成一条带路径条件的断言动作，失败信息为 “calc step not satisfied”（spec_translator.rs#L868-L881）；而expand_lemma_apply的注释直接写明了apply lemma(args)的语义：先 assert 引理的每条requires，再 assume 它的每条ensures（spec_translator.rs#L927-L979）。这解释了文档为何强调“引理必须是已证明命题”——apply是在用你为引理付出过的证明，去换当前上下文里的一条 assume。

引理、归纳与 measure 下降规则

文档给出的示例把递归规约函数与配套引理放在spec module { ... }中：

spec module { fun sum(values: vector<u64>, n: num): num { if (n == 0) { 0 } else { sum(values, n - 1) + values[n - 1] } } lemma sum_step(values: vector<u64>, n: num) { requires 0 < n && n <= len(values); ensures sum(values, n) == sum(values, n - 1) + values[n - 1]; } }

proof { ... }块挂在函数规约或引理之后。上面这个例子里，sum的规约递归地定义前缀和，而sum_step是它的一步归纳规则：sum每展开一层恰好需要sum_step的一次实例化。

文档接着给出 Move Prover 的归纳纪律，这是整个片段最核心的规则集：

1. 在引理的证明里apply该引理自身就是归纳。但这种自应用必须让引理的“度量（measure）”下降；
2. 默认度量是该引理所有整型参数按声明顺序组成的元组；也可以用decreases e;显式声明——e可以是单个表达式，也可以是一个按字典序（lexicographically）排序的元组；
3. 文档举的具体例子：在if (e > 0)分支下apply pow_pos(b, e - 1)，度量元组(b, e)的第二分量减小，因此合法；
4. 若应用发生在同一实例或更大的实例上，或者度量可能降到零以下，证明会失败，报错 “does not decrease the measure”；
5. 在自己的递归组（recursion group）里用forall ... apply实例化一个引理，会被直接拒绝。

这几条规则在源码中有一一对应。expand_lemma_apply在检查到“被应用的引理与当前正在证明的引理同模块且同递归组”时，会分别翻译当前度量current与应用后的度量next，然后断言一个字典序下降条件；断言失败信息正是 “recursive lemma application does not decrease the measure”（spec_translator.rs#L944-L976）。而字典序下降的构造函数mk_lexicographic_decrease的文档注释给出了精确形式：

(n0 < c0 && 0 <= c0) || (n0 == c0 && (n1 < c1 && 0 <= c1)) || ...

即每一层要么严格变小、要么相等进入下一分量，并且每一级比较都附带0 <= c0的非负性检查——这正是文档所说“度量不能降到零以下就失败”的机器层面含义（spec_translator.rs#L1017）。

归纳写法的工程含义：把“大性质”拆成“一步性质”引理，主证明里按循环/递归结构逐步apply，让每次自引用都严格下降度量，是 Move Prover 处理递归合约性质的标准路径。

assume、公理与不可信辅助函数的纪律

文档对“用假设换证明”采取双分支措辞（由evaluation_mode模板变量切换渲染）：

• 评测模式：禁止添加assume、公理或未证明的 native 辅助函数——这类构造是“替换证明义务”而不是“解决证明义务”；
• 普通模式：除非用户或显式的项目策略确立了该“可信边界（trusted boundary）”，否则同样不得用assume/公理/未证明 native 辅助函数去让某个条件通过；若确属可信边界，必须清楚记录，因为它替换了一条证明义务。

这一纪律与 MoveFlow 的评测管线设计一致：评测 harness 只接受evaluation_mode为真的插件清单（见 schedule.py#L174），而评测模式下的技能文档渲染出“绝对禁止”的版本，保证评测结果不被手工假设污染。对使用者而言，这也意味着assume在 Move 规约语言里是“逃生舱”而非“工具箱”：它让 Prover 少证一条义务，验证结论的可信度就相应打折，必须显式登记。

量词触发器（trigger）的合法性

文档在引理一节末尾给出触发器规则：只有不可解释函数（uninterpreted function）的应用才是合法的量词触发器；当无量化（quantifier-free）的表述能表达同样的合约时，优先使用无量化形式。

这条规则约束的是forall x: T {trigger(x)} apply lemma(x)中花括号内的内容：触发器决定求解器在何时代入该量词，一个不含不可解释函数应用的“触发器”无法可靠地驱动实例化，会导致引理写了对却实例化不出来（或反之，过度实例化拖垮超时）。结合同模板树中 verification_ref.md 的超时分析章节（“Timeout strategy” 第 3 条）：替换敌意的无界量词、或在无法避免量化时“add valid triggers”，是超时治理的固定动作之一。

Instantiation weight：[weight = N] 如何压制求解器的自动展开

文档的最后一个专题 “Instantiation weight” 解释了两类会“吃掉”超时的构造，以及[weight = N]的对策：

• 递归规约函数被编码成一条“定义公理（defining axiom）”：求解器看到它的任一应用就展开（unroll）一层；
• forall ... apply是求解器在每个匹配点都会实例化（instantiate）的量词；
• 两者中任何一个都可能主导超时，超时分析（timeout analysis）会把它报告成一条definition of spec function或一条forall条目；
• [weight = N]提高求解器对每次实例化/展开收取的成本，使其“只有在没有更便宜的选项时才展开/实例化”；它不改变任何证明语义，只改变求解器的搜索优先级。

文档给出的完整示例（计数函数 + 带权重的全称实例化）：

spec module { fun count(v: vector<u64>, x: num, k: num): num [weight = 20] { if (k <= 0) { 0 } else { count(v, x, k - 1) + (if (v[k - 1] == x) { 1 } else { 0 }) } } } spec f { ... } proof { forall v: vector<u64>, i: num, j: num, x: num {count(update(update(v, i, v[j]), j, v[i]), x, len(v))} [weight = 20] apply count_swap(v, i, j, x); }

用法判据：当你需要的证明事实来自“引理逐步（one step at a time）应用”、且该定义不应被求解器自行展开时，就加上权重；文档建议20 作为合理的起始权重。它特别警告了一个不对称性：没有权重时，同一份合约可能仍然证明通过，但任何反例搜索（refutation——例如错误实现对照正确合约）都会耗尽预算而不是干脆失败。也就是说，权重不仅优化“证得”，还保住“可证伪性”。

源码侧可以印证这条机制的完整落点。[weight = N]在 AST 解析后被存入规约函数的属性中，注释写明是“留给 Boogie 后端”（// Stash [weight = N] in the spec fun's properties for the Boogie backend，module_builder.rs#L3755，并见 module_builder.rs#L2006 处def_ana_spec_fun接收weight参数）；而forall ... apply上的[weight = N]则走Proof::ForallApply的weight: Option<u32>字段，最终在翻译阶段调用env.set_quant_weight(quant_node_id, w)把权重挂到量词节点上（spec_translator.rs#L1058、spec_translator.rs#L1118-L1119）。两处入口对应文档中的两种挂法：挂在递归规约函数上（定义公理展开计费）与挂在forall ... apply量词上（实例化计费），语义上都只是提高求解器为每次展开/实例化“付费”的代价，不影响义务本身。

实操要点小结

把spec_lang_proofs.md的规则压缩为可执行清单：

1. 先别加证明结构：合约能直接证/直接给出反例时，保持裸合约；只在超时或中间事实缺失时介入；
2. 拆分义务：用小的assert暴露子目标，用if/数值分案分离实质不同的情形，用calc记录推导链（每步都会被独立断言）；
3. 引理即一步性质：为递归规约函数配套sum_step式引理；归纳时确保自apply严格下降 measure（默认整型参数元组，或decreases e;），同实例/更大实例/降破零都会以 “does not decrease the measure” 失败；同递归组内禁止forall ... apply自实例化；
4. 触发器只放不可解释函数应用；能无量化就无量化；
5. 超时分析点名definition of spec function或forall时，给对应对象加[weight = 20]起步，而非盲目加预算；并确认它保住反例搜索的预算；
6. assume/公理默认禁用：评测模式绝对禁止；普通模式下仅当用户或项目策略显式确立可信边界时可用，且必须记录在案；
7. 证明结构的更大上下文（move_package_verify的filter/exclude/split_vcs_by_assert控制、反例读法、超时策略六步法）在同目录的 verification_ref.md 中，与本文片段互为表里。

本文所有结论均以当前仓库内容为准：模板语义以aptos-move/flow/cont/下的 Tera 源文件为准；apply/calc/measure/weight 的机器行为以third_party/move/move-model/src/中spec_translator.rs与builder/module_builder.rs的实现与注释为准，且后者属于 Move 工具链前端，后续版本若调整 Boogie 后端策略，具体计费行为可能随之变化。

【免费下载链接】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