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是 MoveFlowaptos-move/flowAptos 面向 Move 合约开发的 Claude Code 插件模板树cont/中的一个共享片段。MoveFlow 的架构见 aptos-move/flow/CLAUDE.mdmove-flow plugin dir子命令使用 Tera 模板引擎把cont/下的agents/、skills/、hooks/与templates/渲染为插件文件其中模板内的{% include %}用于组合共享片段。本片段在渲染链中的位置是cont/skills/move-prove/SKILL.md —— “move-prove” 技能用 Move Prover 验证并诊断已有 Move 规约它 include 了 verification_tasks.md 与 verification_ref.mdverification_ref.md的第 4 行{% include templates/spec_lang_proofs.md %}引入本片段与spec_editing_ref.md、toolchain_limits.md以及 “Move Prover reference”“Reading a counterexample”“Timeout strategy” 等章节共同组成验证参考片段首行的{% if once(namespec_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 它的每条ensuresspec_translator.rs#L927-L979。这解释了文档为何强调“引理必须是已证明命题”——apply是在用你为引理付出过的证明去换当前上下文里的一条 assume。引理、归纳与 measure 下降规则文档给出的示例把递归规约函数与配套引理放在spec module { ... }中spec module { fun sum(values: vectoru64, n: num): num { if (n 0) { 0 } else { sum(values, n - 1) values[n - 1] } } lemma sum_step(values: vectoru64, 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 的归纳纪律这是整个片段最核心的规则集在引理的证明里apply该引理自身就是归纳。但这种自应用必须让引理的“度量measure”下降默认度量是该引理所有整型参数按声明顺序组成的元组也可以用decreases e;显式声明——e可以是单个表达式也可以是一个按字典序lexicographically排序的元组文档举的具体例子在if (e 0)分支下apply pow_pos(b, e - 1)度量元组(b, e)的第二分量减小因此合法若应用发生在同一实例或更大的实例上或者度量可能降到零以下证明会失败报错 “does not decrease the measure”在自己的递归组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: vectoru64, 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: vectoru64, 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 funs properties for the Boogie backendmodule_builder.rs#L3755并见 module_builder.rs#L2006 处def_ana_spec_fun接收weight参数而forall ... apply上的[weight N]则走Proof::ForallApply的weight: Optionu32字段最终在翻译阶段调用env.set_quant_weight(quant_node_id, w)把权重挂到量词节点上spec_translator.rs#L1058、spec_translator.rs#L1118-L1119。两处入口对应文档中的两种挂法挂在递归规约函数上定义公理展开计费与挂在forall ... apply量词上实例化计费语义上都只是提高求解器为每次展开/实例化“付费”的代价不影响义务本身。实操要点小结把spec_lang_proofs.md的规则压缩为可执行清单先别加证明结构合约能直接证/直接给出反例时保持裸合约只在超时或中间事实缺失时介入拆分义务用小的assert暴露子目标用if/数值分案分离实质不同的情形用calc记录推导链每步都会被独立断言引理即一步性质为递归规约函数配套sum_step式引理归纳时确保自apply严格下降 measure默认整型参数元组或decreases e;同实例/更大实例/降破零都会以 “does not decrease the measure” 失败同递归组内禁止forall ... apply自实例化触发器只放不可解释函数应用能无量化就无量化超时分析点名definition of spec function或forall时给对应对象加[weight 20]起步而非盲目加预算并确认它保住反例搜索的预算assume/公理默认禁用评测模式绝对禁止普通模式下仅当用户或项目策略显式确立可信边界时可用且必须记录在案证明结构的更大上下文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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考