MoveFlow `/move-inf` 技能实战：为 Aptos Move 合约推断并验证完整规范与循环不变量

MoveFlow/move-inf技能实战为 Aptos Move 合约推断并验证完整规范与循环不变量【免费下载链接】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-core 仓库中 MoveFlow 项目的/move-inf技能SKILL.md展开完整讲解如何在缺少合约specification时从实现代码出发推断出完整的 Move 函数规范与循环不变量并通过 Move Prover 完成验证。你将掌握/move-inf三种推理策略tactic的选用、move_package_wp/move_package_verify/move_spec_check等 MCP 工具的调用方式、pragma opaque等规范语言要点以及反例阅读、超时诊断、lemma 证明等一整套可落地的实战方法。技能定位何时使用/move-inf/move-inf是 MoveFlowaptos-core 仓库内的 AI 辅助 Move 开发工作流见 flow/README.md为 AI 编程助手提供的专用技能其 frontmatter 明确定义了适用边界Infer and verify complete Move specifications and loop invariants. Use when contracts are missing; not merely to check existing specs.即当目标函数或模块缺少规范时推断并验证完整的 Move 规范与循环不变量它不是一个检查既有规范是否正确的通用工具。若合约已存在应使用其他技能而不是/move-inf。该技能文件本体是一个 Tera 模板通过{% include %}组合了四个核心片段构成了完整的工作流骨架spec_inf_tasks.md——任务编排与策略选择spec_inf_ref.md——规范推断参考规则、WP 概念、WP 工具、包检查工具、规范语言verification_ref.md——验证参考规范编辑、证明指南、工具链限制、Move Prover 参考spec_inf_report.md——最终报告输出格式。调用方式与三种推理策略/move-inf支持通过调用参数选择推理策略tactic_selectable时为混合插件与作用范围/move-inf # 使用插件的默认混合策略hybrid-guided /move-inf hybrid-guided scope # 引导式混合策略 /move-inf hybrid-flexible scope # 灵活混合策略其中scope指定要推断的函数或模块范围。默认策略由插件生成参数决定move-flow plugin ... --inference-tactic tactic或环境变量MOVE_FLOW_INFERENCE_TACTIC。agent-only是独立插件仅含直接推理策略生成的技能清单与运行时路由中都不会出现 WP 工具。Guided hybrid tactichybrid-guided默认按固定顺序执行诊断驱动推断在请求的范围内运行 WPmove_package_wp覆盖循环输出到指定位置处理其诊断按 WP 工具说明逐函数修复缺失的循环不变量并重跑 WP保留继承自被调用方的部分性inherited partiality重试调用方无法消除它简化 WP 推导出的条件若未启用no_wp_simplification在保留所有 result/abort/frame 义务的前提下化简检查候选move_spec_check若超时按证明指南修复对未经修改、无警告的 WP 输出出现反例属于工具 bug应报告失败条件。Flexible hybrid tactichybrid-flexiblemove_package_wp作为可选的推断通道由 Agent 自行决定何时与直接推理、不变量合成结合使用可在任意范围含循环运行。解析完可修复的警告后按合约需要化简并检查候选。Direct tacticagent-only不使用 WP 工具直接从实现与依赖合约中推导合约与循环不变量一次检查一个自洽的候选再精修被拒绝的部分。任务工具清单这是一个编译-证明循环规范推断是编译并证明的循环而不是测试循环。技能规则spec_inf_rules.md明确规定了任务允许的工具集move_spec_check——判定工作是否完成且唯一有权判定move_package_verify——在候选检查报告验证失败后用更窄的 filter 定位失败move_package_status、move_package_manifest、move_package_query——回答关于包的问题。除此之外的工具都不属于本任务。特别地运行单元测试对规范是否成立没有任何证明力证明器对所有输入推理通过一个测试既不能支持合约也不能定位缺失条件。包检查工具core_tools.md的用法要点move_package_status查看当前编译错误与警告编辑后重跑缓存使未变化的检查开销很低move_package_manifest区分目标源码source_paths与依赖源码dep_pathsmove_package_query结构化查询代替通读支持module_summary、facts、dep_graph、call_graph、function_usage后者的function: module::function可查某函数的直接/传递调用与闭包捕获。所有工具均接受package_path参数指向包含Move.toml的目录。这些工具在 MoveFlow MCP 服务器中均有对应实现工具清单见 flow/README.md。规范推断规则范围与证据只处理请求的函数或模块除非用户要求测试规范否则跳过#[test]与#[test_only]函数写条件前先读实现、既有规范与相关被调用方合约用function_usage查可执行调用与闭包捕获而不是从 import 推断依赖保留用户手写的规范若与实现冲突报告冲突而不是悄悄改变其含义。完成标准一个面向调用方的完整规范必须描述所有对外可见行为正常结果与被修改的引用值每个直接与传递的 abort包括算术、边界、资源访问全局状态变更及其modifies帧真正的 API 前置条件证明函数体所需的循环不变量。要显式检查边界情况相似的控制流在空输入或单元素输入上可能表现不同算术可能在源码没有assert!的情况下 abort。pragma opaque整个任务的评判基准技能要求为编写的目标规范加上pragma opaque。该 pragma 告诉证明器调用方可以只依据合约验证而不读函数体。因此遗漏 result、abort 或 frame 的合约不仅是不完整而是错误——调用方将针对实现无法兑现的承诺被验证。正确的做法是写出能让该声明成立的合约而不是删除 pragma 来为部分合约辩护。注意pragma opaque不会跳过函数自身函数体的验证不透明合约仍需对照实现被证明。两点边界不要给检查范围之外的 helper 添加pragma opaque只有范围内的函数会被证明helper 上的不透明合约将在目标调用点被假定而从未被验证候选检查会因此拒绝helper 保持透明则完全不需要合约证明器读取其函数体目标针对 helper 的真实行为被证明。严禁削弱合约来让验证通过不得删除或收窄行为条件、编造限制性requires、启用部分 abort 覆盖、省略 frame 或跳过验证只能用语义等价且完整的形式替换条件。继承的部分性Inherited partiality部分 abort 覆盖只有一个狭窄例外调用方是针对其不透明被调用方的合约而非函数体被验证的当某个合约自身不完整时调用方无法陈述精确的 abort 条件此时pragma aborts_if_is_partial是诚实的形式而非削弱。但它只计入你发现的部分性由推断为被调用方报告或你开始时树上已存在的部分性。自己写出的部分性不算——把 helper 标为 partial 再引用它可以开脱任何合约检查会拒绝。当例外适用时要在合约中说明它来自哪个被调用方只要被调用方仍 partial调用方就必须保持 partial该警告不是调用方的修复义务也不要求重复 WP 调用。循环抽象常见不变量形状不变量必须从实现与循环退出所需事实推导初始成立、单次迭代保持、约束每个被循环修改的相关值。WP 报告需要不变量的循环会附带前几次迭代的有界循环头事实bounded loop-head facts将其泛化为入口成立且越过一条回边仍成立的谓词。常见形状累积Accumulation把累加器关联到已处理前缀常用递归 helper 或 processed-plus-remaining 守恒关系搜索Search记录索引边界与已处理前缀已知信息包括结果所需的首匹配/无匹配事实量化遍历Quantified traversal把最终量词限制到已访问前缀有状态遍历Stateful traversal把被修改的引用或资源关联到循环前状态并陈述必要的 frame 事实。对内联高阶迭代器当捕获变换器capture transformer能精确表达累积效果时使用folds_of若证明器报告 fold 不适用改写为带显式不变量的等价普通循环。vacuous/sathard未解决的义务推断出的[inferred vacuous]状态未受约束或[inferred sathard]SMT 难解子句是未解决义务不是可以删除的子句。诊断其来源循环 havoc 需要更强的循环抽象困难的量词或非线性表达式需要等价的、求解器友好的表示未约束的result_of/ensures_of/aborts_of载体需要更强的被调用方或函数值合约。输出纪律每条自行编写的条件与不变量标记[inferred]绝不标记既有用户子句遵循包的 inline 或.spec.move放置约定循环不变量始终留在可执行循环旁边避免等价重复与空 spec 块为非显然的 helper 与 lemma 写注释结束时文件已格式化、编译器无错误范围内无未解决的vacuous、sathard、uninvariant-loop 或不适用 fold 诊断。WP 工具最弱前置条件推断move_package_wp实现见 package_spec_infer.rs源码中标注Low-level WP inference tool. Use through /move-inf从返回、abort、调用与状态更新向后推理刻画每种行为的初始状态循环由其不变量表示不变量未约束的值在循环后近似任意见 wp_concepts.md。参数package_path必填filter: module或module::function可选也支持address::module::function数值或命名地址均可不带 filter 时处理整个包spec_output: inline默认合约写入源码或file写入配套的.spec.move文件原文件不动。该枚举在 package_spec_infer.rs 中定义。按函数解释 WP 输出wp_tool.md无警告生成的规范构造即正确包括隐式算术、边界、资源与被调用方 abort。注意 WP不运行证明器验证仍可能超时——修复证明或用等价的求解器友好表达式而不削弱合约。对未修改、无警告输出出现编译错误或反例是工具 bug缺失或不充分的循环不变量补充入口成立、每次迭代保持的不变量用警告附带的循环头观测辅助发现它们不是证明只描述显示的执行前缀。移除陈旧的生成函数子句后重跑该函数的 WP保留不变量、helper 与用户子句部分不透明或无函数体的被调用方规范唯一能让调用方合理 partial 的被调用方情形。调用方无法在该边界保持部分的情况下获得总 abort 覆盖保留pragma aborts_if_is_partial记录具名被调用方不要重写调用方或删除 pragma 来宣称 totality透明被调用方缺少完整不透明合约WP 无法补全调用方。若该被调用方在可编辑范围内先为其推断并验证不透明合约再对调用方重跑 WP若在范围外报告为 corpus/package blocker其所有者必须提供完整验证的不透明合约。绝不可用此情形为调用方开脱aborts_if_is_partial未建模的证明器 intrinsicWP 工具 bug。intrinsic 执行证明器内建逻辑而非 Move 函数体不要添加源码级规范或使其 opaqueWP 必须内部提供内建的值、abort 与变更语义。条件意外丢失、输出畸形或任何其他推断失败都是工具 bug而非削弱规范的借口。候选检查move_spec_checkmove_spec_check是规范被测试的方式无论是推断的还是手写的其实现见 spec_check.rs。它编译包、验证目标、拒绝自我削弱的合约禁用或跳过的验证、空条件、无被调用方支撑的部分 abort pragma并报告合约未覆盖的义务类别。参数package_path、可选filter限定模块或函数、可选timeout每条件求解器超时默认 10 秒见源码DEFAULT_CHECK_TIMEOUT_SECS以及可选baseline_path工作开始前的原始包副本用于比对运行时代码是否仍编译为相同字节码。三种结果Accepted请求的范围已完成停止并报告Rejected标题行指明失败项随后的诊断行为path:line: code: message。用聚焦的move_package_verify定位验证失败修复后重跑候选检查弱化码weakening code指向引入该子句的位置对项目已有的可信边界不是你引入的弱化予以报告而不删除Unavailable证明器无法运行这不是对规范的裁决如实报告即可。由于检查在验收时已完成验证它取代紧随其后的move_package_verify调用此前调用重复了即将进行的验证之后调用则重复已证明的内容。证明器仅用于初始诊断或在更窄 filter 下定位失败。时间预算参考候选通常先给初始超时值重试时给最大值模板中的initial_verification_timeout/max_verification_timeout参数证明确需更大预算时可覆盖timeout。Move 规范语言速查函数合约用spec function_name { ... }附加条件函数名是软关键字时转义为spec function_name { ... }requires e调用方义务在前状态求值aborts_if e前状态下允许的 abort。完整 abort 检查下所有aborts_if的析取刻画函数 abort 行为无子句表示 abort 行为未指定全函数用aborts_if falseensures e正常返回保证后状态求值old(e)表示前状态值modifies globalT(addr)函数可能改变的全局状态帧。不透明函数若能变更全局资源需要覆盖每个资源/地址效应的帧只读不写全局的函数无需声明帧编造modifies等于声称实现并不存在的效应。不透明与 intrinsicpragma opaque改变调用方的验证方式用合约而非实现不禁用函数自身函数体的验证。修复不透明合约时保留 pragma并包含完整的 result、abort 与全局状态帧行为。pragma intrinsic标识具有内建证明器语义的函数不要因其 Move 实现缺失或不适合普通验证就编造不透明合约或函数体证明。规范表达式result在ensures中表示返回值globalT(addr)/existsT(addr)检查全局资源模块的spec_exists_at包装应建模为同一存在性事实证明器不受 Move 源码可见性限制规范使用数学整数MAX_U64等数值边界指 Move 值而规范表达式中的算术无界规范表达式操作值而非引用用v.field不用*v或vold(e)表示函数入口处的值不要在requires或aborts_if中使用它们本就是前状态表达式。循环不变量中的old(x)仅对函数参数有效其他循环前值应在循环前存入局部变量并直接引用。循环不变量while (i n) { // body } spec { invariant i n; invariant acc prefix_sum(values, i); };证明器检查不变量初始化、保持性以及循环退出到函数合约的蕴含。对内联高阶迭代器在捕获变换器适用时使用folds_offolds_off(values, i)汇总一元回调在前缀上的效果folds_off(|j| (j, values[j]), i)提供显式参数元组。该谓词包含累积捕获效应与前缀无 abort 行为且只能作为循环不变量使用fold 不适用时改写为等价普通循环并提供不变量。引用被调用方行为对非内联具名函数或函数值f规范可使用requires_off(args)、aborts_off(args)、ensures_off(args, result)、result_off(args)。这些谓词暴露被调用方合约可跨模块。目标规范还可调用依赖中声明的规范函数因此要同时保留规范级依赖闭包与可执行调用闭包。独立规范文件与推断标记.spec.move文件扩展对应模块helper、lemma 与模块不变量放在spec module { ... }Move 函数的条件放在spec function_name { ... }没有spec module_name { ... }形式。仓库中大量实际用例可参考 aptos-framework/sources 下的.spec.move文件。每条推断的条件或不变量标记[inferred]WP 可能输出[inferred vacuous]与[inferred sathard]二者都标记未解决的推断输出。验证参考move_package_verify与反例阅读调用move_package_verify时传package_path与显式超时可选控制项见 verification_ref.mdfilter: module、module::function或address::module::function聚焦证明数值或命名地址裸模块名必须无歧义exclude: [...]诊断期间临时排除已知目标split_vcs_by_assert: true定位函数中哪个断言困难或为假error_limit限制反例输出。filter 与 exclude 只是诊断便利最终证明必须覆盖用户请求的范围未匹配或被排除的目标不算成功。阅读反例反例显示一次失败执行中各帧及求解器选定的值具名局部变量以源码名出现result是返回值先据此推理$tN是编译器/证明器引入的临时变量无源码对应物按该步的中间值理解不要在规范中引用标记(spec)的帧位于函数 spec 块内求值的是条件而非执行代码generic是类型参数值因不影响结果而被隐藏函数值以来源实体打印闭包显示其打包的函数与按参数名捕获的参数value of function field ...与value of function parameter ...是求解器为该字段/参数选的值尾部#n区分同一字段的不同值重复#n即同一值。其行为仅由规范对载体所述内容决定因此要为载体给出精确的result_of与aborts_of条件some T是求解器选取的、与任何源码实体无关的T类型函数。解释 abort 码诊断 abort 码不匹配前先读依赖的error.move本仓库为 move-stdlib/sources/error.move。std::error::canonical合约刻意不透明其[abstract]后条件只返回类别[concrete]后条件描述运行时编码(category 16) reason。例如error::invalid_argument(40)运行时编码为0x10028但在抽象合约下证明器只看到类别0x1error::INVALID_ARGUMENT。因此类别级反例本身不构成工具 bug也不代表运行时 reason 丢失。选择aborts_if ... with ...码前先追踪证明实际使用的 helper 与合约抽象合约适用时用其类别常量运行时单测仍用具体编码码。不要对任意模块内 abort 码做类别解码、不要改 stdlib 合约、不要删除 abort 码检查、不要为消除不匹配而启用部分 abort 检查。编辑前分类编译/规范语言错误先修语法、名称解析、放置或非法old()使用再谈证明后条件反例追踪正常路径判断是实现违反意图、被调用方合约太弱还是循环不变量丢失所需事实abort 反例枚举直接与传递 abort含算术、索引、资源、不透明被调用方补全精确 abort 行为仅在被调用方合约自身 partial 时保留继承的部分 abort 覆盖frame 失败对照modifies子句比较可执行全局写入尤其跨不透明被调用方不变量失败分别检查初始化、保持性与循环退出蕴含更强的不变量只有在函数体能证明它时才有用超时/资源耗尽把合约视为未解决而非为假或已验证。绝不为了让证明器变绿而让期望属性消失新增前置条件只有当它反映 API 意图时才有效而不是因为它排除了反例。超时分析与策略超时诊断携带回放证据证明器在 profiling 求解器下重跑捕获的查询而非报告原运行因此计数描述同一义务但不精确表示下界。量词活动quantifier activity为每个实例化命名源码位置应减少该条目所需的实例化而非提高预算。definition of spec function条目指向该 helper让它的递归与循环对齐一个义务展开一步并保持递归单一forall条目指向写下的量词给它有效触发器或用 frame 或有界关系替换非线性算术活动arith-nla-*计数器表示搜索进入非线性算术优先加法递推而非闭式不变量中不放符号乘积混合活动先处理顶部具名量词再处理算术两者会叠加不完整/部分证据仍能排序量词但分类未定缺失计数器不代表其原因不存在证据不可用回放无法运行退回到split_vcs_by_assert加更窄 filter 隔离义务。被点名的源码位置就是应修改的位置。超时无论如何都让合约未解决所以绝不要用削弱来应付。超时策略六步化简 WP 生成或手写表达式删除已证冗余、提取公共因子、替换机械更新、修复vacuous/sathard循环输出用split_vcs_by_assert与小assert证明提示暴露中间事实或拆分情形用等价 frame、有界关系或递归 helper 替换敌意无界量词不可避免时加有效触发器优先加法递推而非非线性闭式不要为隐藏而把内建算术包进 helper把可复用事实证明为 lemma 并用apply显式实例化对分析点名的递归 helper 或forall ... apply加[weight N]让求解器不再自行展开/实例化必要时提高每条件超时模板参考为max_verification_timeout秒并非硬上限。数据不变量与全局更新不变量仅在表达每个构造器/变更器都保持的真实属性时有帮助它们会在模块内制造新的证明义务不要未经全局语义承诺就当作局部求解器提示添加。证明指南lemma、归纳与实例化权重当正确合约超时或求解器找不到中间事实时使用证明结构spec_lang_proofs.mdassert e暴露子目标且自身必须被证明apply lemma(args)实例化已证 lemmaforall x: T {trigger(x)} apply lemma(x)带显式触发器全称应用calc记录相等/不等链条件与值拆分分离不同证明情形。优先选用绑定到失败义务的小断言与 lemma。lemma 是已证明的模块级命题不是公理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]; } }在函数规范或 lemma 后附加proof { ... }。归纳就是递归 lemmalemma 可以在更小实例上apply自身但每次应用必须减小其 measure默认是整数参数按声明顺序的元组或用decreases e;/decreases (e1, e2);声明字典序否则报 does not decrease the measure对自身递归组的 lemma 做forall ... apply会被拒绝。lemma 之外没有归纳关于n次重复的量化事实必须安排成求解器只需要一步。让递归 spec helper 与循环对齐当base * 2^n这类闭式不可证时定义一个递归恰好执行循环一次迭代的 helper并用它陈述不变量每个证明义务即可定义性展开在溢出边界饱和 helper可用同一定义表达精确 abort 行为。保持 helper 递归单一两个相互加强的递归 helper 会成倍增加量词实例化通常超时。[weight N]提高求解器为每次实例化收取的代价使其只在没有更便宜选择时才展开/实例化不改变任何证明语义20 是合理起点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); }仅当所需事实来自逐步骤应用的 lemma、且定义不应自行展开时使用它否则同一合约可能可证但每次反证错误实现对照正确合约都会耗尽预算而不是失败。只有未解释函数应用才是合法量词触发器能用无量词形式表达时优先。工具链能力与限制从参考建立而非用试探性声明探测编译器toolchain_limits.mdpragma 是上下文特定的非法pragma是编译错误其诊断会列出该位置合法的全部 pragma归纳是递归 lemma应用必须减小 measure默认按整数参数声明顺序的元组decreases e;/decreases (e1, e2);字典序显式声明否则报 does not decrease the measure对自身递归组的forall ... apply被拒绝递归 spec helper 与循环对齐见上节helper 递归保持单一。规范编辑与信任边界编辑合约而非可执行行为推断任务中仅当需要表达可靠不变量时才做保持行为的循环/内联 HOF 重写。修订规范时做定向编辑只改变化的条件重写整个模块以调整一个条件会干扰无关的用户代码。简化顺序spec_editing_ref.md先修复抽象先解决vacuous/sathard子句背后的循环或被调用方事实再化简结果表达式替换无界量词编码frame 用modifies、累积用有界或递归 helper 表达确需量词时给有效触发器规范化机械状态表达式所有字段已知时嵌套update_field项替换为直接结构构造合理时把展开的情形合并为等价的通用条件化简算术与布尔结构只删除被保留子句或语言保证蕴含的子句展平重复更新、提取重复子表达式而不改变溢出或 abort 行为检查替换结果推断的替换保留[inferred]每次有意义的化简后重跑候选检查。每一步化简都必须保留 result、abort、前置条件与 frame 语义。信任边界不要自动添加pragma verify false、verify_duration_estimate、公理或未证假设作为回退仅在用户或显式项目策略接受该可信边界时使用并在旁边注释信任原因与观察到的超时/证明证据。最终报告以最多三个紧凑要点结尾spec_inf_report.mdResult说明添加的合约或不变量及最终验证/验收状态未解决时点名阻塞义务Strategy说明所用方法与关键工具以及该策略为何适合此问题Decision points总结最多两个关键决策各配以动机证据或结果省略常规步骤与逐轮转录。源码实现佐证上述工作流在仓库中有完整实现与测试支撑SKILL.md 与 agents/move-inf.md 为技能模板入口任务与参考片段位于 cont/templatesmove_package_wp的低层实现位于 package_spec_infer.rs其SpecOutput枚举inline/file与 filter 语义与模板描述一致并接入循环不变量证据深度LOOP_INVARIANT_EVIDENCE_DEPTHmove_spec_check实现于 spec_check.rs默认每条件超时 10 秒支持baseline_path字节码比对测试覆盖见 flow/src/tests/move_package_spec_infer、flow/src/tests/move_package_verify 与 flow/src/tests/spec_check含 filter、exclude、超时、反例证据、接受/拒绝等场景规范语言的真实应用可参考 aptos-framework/sources 下各模块的.spec.move文件与 move-stdlib/sources/error.move 的 canonical abort 编码。核心结论/move-inf的本质是一条WP 推断 → 修复不变量 → 化简 → 候选检查的闭环流水线其质量底线由两条纪律保证——完整覆盖所有 result/abort/frame 义务的pragma opaque合约以及绝不为了验证通过而削弱规范。掌握这套流程即可为任意缺失规范的 Aptos Move 函数与循环产出可证明、可被调用方安全依赖的完整规范。【免费下载链接】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），仅供参考