Aptos Move 规范推断与循环不变量验证move-inf 混合 WP 推理工作流全解【免费下载链接】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 仓库中aptos-move/flow/cont/agents/move-inf.md及其引用的模板体系完整讲解 Aptos Move 智能合约的规范specification推断与循环不变量验证工作流如何在缺失规范的情况下借助最弱前置条件Weakest Precondition, WP推理自动推导函数契约、定位并补齐循环不变量最终通过 Prover 与候选检查candidate check验收。读完本文你将掌握hybrid-guided与hybrid-flexible两种混合推理策略的完整执行顺序、WP 工具move_package_wp的诊断解读方法、pragma opaque契约的评判标准以及超时、反例、abort 码等验证问题的系统化处置思路。一、文档定位move-inf 在 Agent 工作流中的角色在 aptos-move/flow/cont/agents/ 目录下仓库将智能合约的自动化分析拆分为四个相互配合的 Agent 提示文档move-inf.md本文主角负责推断并验证缺失的 Move 规范与循环不变量frontmatter 中descriptionInfer and verify missing Move specifications and loop invariantsmove-check.md、move-verify.md、move-test.md分别承担检查、验证、测试等相邻任务。move-inf.md本身是一个 Jekyll 模板聚合文件通过{% include %}按固定顺序组合出完整文档骨架spec_inf_tasks.md——任务定义与策略编排仅存放与特定策略相关的编排逻辑WP 语义统一收敛在wp_tool.mdspec_inf_ref.md——规范推断参考聚合规则、WP 概念、WP 工具、包检查工具与规范语言verification_ref.md——Move Prover 验证参考编辑参考、证明指导、工具链限制、反例与超时解读spec_inf_report.md——最终报告格式约定。理解这一模板结构有助于把下文各章节对应到仓库中的具体文件按需查阅。二、任务定义为函数或模块推断完整规范spec_inf_tasks.md 开宗明义为请求的函数或模块推断一份完整规范同时保留可执行行为executable behavior与用户手写的规范。规范推断是一个编译-证明闭环compile-and-prove loop而非测试循环。2.1 策略选择文档提供两种可选的混合策略默认策略由调用方指定invocation 可以显式选择/move-inf hybrid-guided或/move-inf hybrid-flexible后接作用域参数。执行时只能跟随被选中的策略。直接策略agent_only仅从实现与依赖契约中推导契约与循环不变量先检查一个连贯的候选再精炼被拒绝的部分。灵活混合策略hybrid-flexiblemove_package_wp作为一次推断通道inference pass可用Agent 自行决定是否以及何时将其与直接推理、不变量合成结合使用。它可运行于任何作用域包括循环结果按 WP 工具一节解读。默认情况下在可修复的警告解决后应在保持契约语义的前提下尽可能简化再检查候选若调用带有no_wp_simplification参数则直接检查生成的子句仅在处理诊断信息时才修改。引导混合策略hybrid-guided严格按以下顺序执行这是全文最核心的可操作步骤在请求的作用域上运行 WP包括循环指定要求的输出位置处理 WP 的诊断按 WP 工具一节一次修复一个函数的缺失循环不变量并重跑 WP。注意保留继承的 callee 部分性——重试 caller 无法消除它默认情况下简化 WP 推导出的条件同时保留每一个结果result、中止abort与帧frame义务检查候选candidate check。若带no_wp_simplification则直接检查生成的子句。修复超时使用证明指导若对未修改、无警告的 WP 输出仍出现反例则属于工具缺陷应上报失败条件。从源码结构看spec_inf_tasks.md 末尾通过{% include templates/candidate_check.md %}把候选检查固化为两种策略共同的收尾步骤说明任何策略产出的契约都必须经过候选检查验收。三、WP 推理原理从后向前刻画初始状态wp_concepts.md 给出了策略无关的 WP 背景知识最弱前置条件WP推理从返回、中止、调用与状态更新出发向后backward推导刻画每种行为对应的初始状态。循环由其不变量表示不变量未约束的值在循环之后实际上可视为任意值。这一条原则解释了后续所有操作WP 输出的是使每个行为得以发生的初始状态条件因此它天然覆盖了隐式算术中止、越界、资源访问与 callee 中止而循环之所以成为难点正因为其行为需要不变量来抽象不变量缺失或过弱会直接导致推导失败。四、WP 工具move_package_wp的参数与诊断处理wp_tool.md 是 WP 工具契约与诊断处理的唯一权威描述。4.1 调用参数package_path必传指向包含Move.toml的包目录filter: module或filter: module::function可选将处理范围限定到模块或单个函数不传则处理整个包spec_output: inline默认把契约写回源文件file生成伴生的.spec.move文件。循环不变量始终紧邻其可执行循环放置。move_package_wp负责推导条件并写回源码但不运行 Prover——验证由后续的候选检查/move_package_verify完成。4.2 按函数解读结果WP 工具对每个函数返回四种典型结果处置方式截然不同结果含义与处置无警告生成的规范按构造即完整正确含隐式算术、边界、资源与 callee 中止。但验证仍可能超时修复证明或改用等价的求解器友好表达式不得弱化契约。对未修改、无警告的输出出现编译错误或反例属于工具缺陷缺失/不充分的循环不变量添加一个入口成立、每次迭代保持的不变量。警告附带的**有界循环头事实bounded loop-head observations**只描述所显示执行前缀用于帮助发现不变量并非证明。修复后移除过期的生成函数子句保留不变量、helper 与用户子句再对该函数重跑 WP部分 opaque / 无 body 的 callee 规范这是唯一能使 caller 合法保持部分性的 callee 情形。保留pragma aborts_if_is_partial在契约中说明具名 callee不得重写 caller 或删除该 pragma 来宣称全量性透明 callee 无完整 opaque 契约WP 无法完成 caller。若该 callee 在可编辑作用域内如当前模块先推断并验证其 opaque 契约再重跑 WP若在可编辑作用域外将该依赖上报为 corpus/package 阻塞项绝不借此在 caller 上使用aborts_if_is_partial未建模的 prover intrinsic属于 WP 工具缺陷。Intrinsic 执行 prover 内建语义而非 Move body不应添加源码级规范或使其 opaque最后一条总原则条件意外丢失、输出畸形或其他推断失败都是工具缺陷而非弱化规范的借口。五、规范推断规则工具、范围、完成标准与输出纪律spec_inf_rules.md 沉淀了所有策略共享的推断决策与安全护栏。5.1 本任务需要的工具规范推断是编译-证明循环不是测试循环move_spec_check判定工作是否完成——它是唯一能做此裁决的工具move_package_verify在候选检查报告验证失败后定位失败位置move_package_status/move_package_manifest/move_package_query回答关于包的问题。规则特别强调运行包的单元测试对规范是否成立没有任何说明力——Prover 对所有输入推理通过的测试既不能支撑契约也不能定位缺失条件且测试运行还会在包中留下覆盖率映射。5.2 范围与证据只在请求的函数或模块内工作除非用户要求测试规范否则跳过#[test]与#[test_only]函数写条件前先读实现、既有规范与相关 callee 契约用function_usage查询可执行调用与闭包捕获不要从 import 推断依赖保留用户手写规范若与实现冲突报告冲突而非静默改变其含义。5.3 完成标准规范必须描述调用者可见的全部行为正常结果与被修改的引用值每个直接与传递性中止含算术、越界、资源访问全局状态变更及其modifies帧真正的 API 前置条件证明循环体所需的不变量。必须显式检查边界情况相似的控制流在空输入或单元素输入上可能行为不同算术也可能在没有源码assert!的情况下中止。5.4pragma opaque整个任务被评判的主张对目标函数作者给出的规范必须标注pragma opaque。理由极具说服力opaque 意味着 Prover 允许调用者仅凭契约被验证而无需阅读函数体。因此遗漏了某个结果、中止或帧的契约不只是不完整而是错误——调用者将基于一个实现并不兑现的承诺被验证。同时注意pragma opaque不会抑制函数自身 body 的验证——opaque 契约仍须针对实现被证明不要给检查范围外的 helper 加pragma opaque只有范围内的函数被证明范围外 helper 的 opaque 契约会在目标调用点被直接假设而永不验证候选检查会因此拒绝保持透明的 helper 则不需要任何契约Prover 读取其 body目标函数即针对 helper 的真实行为被证明。绝不弱化契约换取验证通过不得删除或收窄行为条件、不得发明限制性的requires、不得启用部分 abort 覆盖、不得省略帧、不得跳过验证替换条件只能用语义等价且完整的形式。5.5 继承的部分性Inherited Partiality部分 abort 覆盖有一个狭窄例外当 opaque callee 的契约本身是部分的时caller 没有精确的 abort 条件可陈述此时pragma aborts_if_is_partial是诚实的表达而非弱化。但该例外只对你发现的部分性生效由推断报告或起始代码树中已存在自己写出的部分性不算数——先标记 helper 部分再援引它会为任何契约开脱检查会拒绝。适用例外时必须在契约中说明它来自哪个 calleecallee 保持部分期间 caller 必须保持部分此警告不是caller 的修复义务也无需反复调用 WP。5.6 循环抽象Loop Abstractions不变量必须初始成立、存活一次迭代、约束每个相关的循环修改值。被报告需要不变量的循环会附带前几次迭代的有界循环头事实把它们泛化为入口成立且存活于一条回边的谓词。常见形状累积Accumulation把累加器关联到已处理前缀常用递归 helper 或已处理 剩余守恒关系搜索Search记录索引边界与已处理前缀的已知事实包括结果所需的首匹配/无匹配事实量词遍历Quantified traversal把最终量词限制在已访问前缀上有状态遍历Stateful traversal把被修改的引用或资源关联到循环前状态并陈述必要的帧事实。对内联高阶迭代器当捕获变换器capture transformer能表达精确累积效果时使用folds_of若 Prover 判定 fold 不适用改写为等价普通循环并给出显式不变量。推断出的vacuous或sathard子句是未解决义务而非可删除子句必须诊断其来源循环 havoc → 需要更强的循环抽象困难的量词或非线性表达式 → 需要等价的、求解器友好的表示未约束的result_of/ensures_of/aborts_of载体 → 需要更强的 callee 或函数值契约。5.7 依赖与抽象普通非内联 callee 需要足以支撑目标的契约opaque callee 的 body 按其契约验证一次caller 之后只消费其 result、abort 与 frame 行为。目标用到的规范函数即使不在可执行调用图内也要保留。不要为pragma intrinsic函数合成普通契约——Prover 提供其内建语义。5.8 输出纪律每个作者书写的条件与不变量标注[inferred]绝不标记既有的用户子句遵循包的 inline 或.spec.move放置约定循环不变量始终留在可执行循环旁避免等价重复与空 spec 块为非显然的 helper 和引理写文档收尾时文件需格式化、编译器干净作用域内无未解决的vacuous、sathard、非不变量循环或不适用 fold 诊断。六、候选检查move_spec_check验收闭环candidate_check.md 定义无论规范是推断还是手写的都用move_spec_check来检验。它编译包、验证目标、拒绝自我弱化禁用/跳过验证、空条件、无 callee 理由的部分 abort pragma并报告契约未覆盖的义务类别。参数为package_path可选filter聚焦单一模块或函数。三种结果Accepted请求范围完成停止并报告Rejected首行说明哪项检查失败后续诊断行格式为path:line: code: message。用聚焦的move_package_verify定位验证失败并修复再重跑候选检查。弱化代码指向引入它的子句不是你引入的弱化项目既有可信边界会被报告而非被删除UnavailableProver 无法运行——这不是对规范的裁决照实报告即可。候选检查在验收时会执行验证因此取代收尾时对move_package_verify的调用之前调用是重复即将进行的工作之后调用是重新证明已经证明过的东西。Prover 只用于初始诊断或按更窄filter定位已报告失败。此外通过临时突变条件并重新检查来试探自己的契约是合法的自证手段代价是每次多一轮验证。七、Move 规范语言速查spec_lang.md 是这份工作流的规范语言工作参考关键语法如下。7.1 函数契约用spec function_name { ... }附加条件函数名是软关键字时转义为spec function_name { ... }requires e调用者义务在前置状态求值aborts_if e前置状态下允许的中止。开启完整中止检查时所有aborts_if的析取刻画函数的完整中止行为无子句表示中止行为未指定全函数用aborts_if falseensures e正常返回保证在后置状态求值用old(e)取前置状态值modifies globalT(addr)可变更全局状态的帧声明。opaque 函数若可变全局资源需要覆盖每个资源/地址效应的帧只读不写的全局访问不应声明帧——发明modifies是声称实现没有的效果。7.2 Opaque 与 Intrinsicpragma opaque改变 caller 的验证方式用契约而非实现不禁用 opaque 函数自身 body 的验证修复契约时保留 opaque pragma并包含完整 result、abort 与全局帧行为。pragma intrinsic表示函数具备内建 prover 语义不应因其 Move 实现缺失/不适合普通验证而杜撰 opaque 契约或 body 证明。7.3 规范表达式resultensures中的返回值globalT(addr)/existsT(addr)检查全局资源模块的spec_exists_at包装应建模为同一存在性事实规范使用数学整数MAX_U64等数值边界指 Move 值而规范表达式中的算术无界规范表达式作用于值而非引用用v.field不用*v或v。old(e)指函数入口的值不要在requires或aborts_if中使用它们本就是前置状态表达式。在循环不变量中old(x)仅对函数参数合法其他前置循环值须在循环前存入局部变量并在不变量中直接引用该局部。7.4 循环不变量示例while (i n) { // body } spec { invariant i n; invariant acc prefix_sum(values, i); };Prover 检查不变量的初始化、保持性以及从循环出口到函数契约的蕴含。对内联高阶迭代器引入的循环用 fold 逻辑与folds_of不变量folds_off(values, i)概括一元回调在前缀上的效果folds_off(|j| (j, values[j]), i)提供显式参数元组。该谓词包含累积捕获效果与前缀不中止行为仅作为循环不变量有效fold 警告不适用时把迭代器改写为等价普通循环并给出不变量。7.5 引用 callee 行为对非内联具名函数或函数值f规范可用requires_off(args)、aborts_off(args)、ensures_off(args, result)、result_off(args)暴露 callee 契约可跨模块。目标规范也可调用依赖中声明的规范函数因此除可执行调用闭包外还要保留规范级依赖闭包。7.6 独立规范文件与推断标记.spec.move文件扩展对应模块helper、引理与模块不变量放spec module { ... }某 Move 函数的条件放spec function_name { ... }不存在spec module_name { ... }形式。推断标记每个推断出的条件/不变量标[inferred]WP 可能输出[inferred vacuous]状态未约束与[inferred sathard]SMT 难解两者都标记未解决的推断输出。八、Move Prover 验证参考反例、abort 码与超时verification_ref.md 聚合了 spec_editing_ref.md、spec_lang_proofs.md、toolchain_limits.md 之后给出 Prover 使用规范。8.1 调用与可选控制调用move_package_verify需传package_path与显式超时。可选控制filter: module/module::function/address::module::function聚焦证明数字或命名地址裸模块名须无歧义exclude: [...]诊断期间临时排除已知目标split_vcs_by_assert: true定位函数中哪个断言难解或为假error_limit限制反例输出规模。过滤与排除只是诊断便利最终证明必须覆盖用户请求的作用域未匹配或被排除的目标不算成功。8.2 阅读反例反例展示一次失败执行的各帧及求解器选定的值先读符号说明再下结论命名局部按其源码名出现result为返回值优先由此推理$tN是编译器/Prover 引入的临时变量无源码对应按该步骤的中间值理解不要在源码中寻找或在规范中命名(spec)帧位于函数 spec 块内求值的是条件而非执行代码generic是类型参数值因不影响结果而被隐藏函数值按其来源源码实体打印闭包显示其打包的函数与按参数名捕获的参数value of function field .../value of function parameter ...是求解器为字段/参数选择的值尾部#n区分同字段的不同值重复#n即同一值。函数值的行为仅由规范对载体的陈述决定因此要给载体精确的result_of与aborts_of条件some T是求解器挑选的、与源码实体无关的T型函数。8.3 解读 abort 码诊断 abort 码不匹配前先读依赖的error.move本仓库为 aptos-move/framework/move-stdlib/sources/error.move。std::error::canonical契约故意 opaque[abstract]后置条件只返回类别[concrete]后置条件描述运行时编码(category 16) reason。例如error::invalid_argument(40)运行时编码为0x10028但在抽象契约下 Prover 只见类别0x1error::INVALID_ARGUMENT。因此仅类别的反例本身不是工具缺陷也不证明运行时 reason 丢失。选择aborts_if ... with ...码前先追踪证明实际使用的 helper 与契约抽象契约生效时用其类别常量运行时单元测试仍用具体编码值。不要把类别解码套用到任意模块局部 abort 码、不要改 stdlib 契约、不要删除 abort 码检查或为掩盖不匹配而启用部分 abort 检查。8.4 编辑前的分类编译/规范语言错误先修语法、名称解析、放置或非法old()用法再推理证明后置条件反例追踪正常路径判断是实现违反契约、callee 契约过弱、还是循环不变量丢失所需事实abort 反例枚举直接与传递性 abort算术、索引、资源、opaque callee补全精确 abort 行为仅当 callee 契约本身部分时保留继承的部分覆盖帧失败对照modifies子句比较可执行全局写尤其跨 opaque callee不变量失败分别检查初始化、保持性与循环出口蕴含——更强的不变量只有在 body 能证明它时才有用超时/资源耗尽把契约视为未解决既非假也非已验证。总原则绝不让期望属性消失来换取绿色 Prover 结果。新前置条件只有在反映真实 API 时才有效而非因为它排除了反例。8.5 超时诊断与策略超时诊断携带重放证据Prover 在分析求解器下重跑捕获的查询因此计数描述同一义务但非精确表示下界量词活动按求解器实例化排序并给出源位置减少该入口需要的实例化而不是提高预算。definition of spec function条目指向该 helper让其递归与循环对齐一次义务展开一步并保持单一递归forall条目指向书写的量词给出有效触发器或用帧/有界关系替代非线性算术活动arith-nla-*计数器搜索处于非线性算术中优先加法递推而非闭式解不变量中不要放符号乘积混合活动两者皆有先处理命名的顶层量词再处理算术不完整证据仍可排序量词但分类未定缺失计数器不代表原因缺失证据不可用重放无法运行退回到split_vcs_by_assert 更窄 filter 隔离义务。命名的源位置就是该改的地方。超时无论如何都使契约未解决绝不以弱化应对。超时策略六步简化 WP 生成或手写表达式删除可证冗余、提取公因子、替换机械更新、修复 vacuous/sathard循环输出用split_vcs_by_assert与小assert证明提示暴露中间事实或分情况用等价帧、有界关系或递归 helper 替换敌意的无界量词无法避免量化时加有效触发器优先加法递推不把内建算术包进 helper 来掩盖它把可复用事实证明为引理并用apply显式实例化对分析点名的递归 helper 或forall ... apply加[weight N]让求解器停止自行展开/实例化必要时提高单条件超时——通常的重试建议值为max_verification_timeout秒这只是一个建议而非硬上限。数据不变量与全局更新不变量只有在表达每个构造器/修改器都保持的真实属性时才可能有用它们会在整个模块产生新的证明义务不要只作为局部求解提示而添加除非确认了该全局语义承诺。九、检查包结构move_package_status/manifest/querycore_tools.md 提供了了解包的三件工具move_package_status当前编译错误与警告编辑后重跑缓存使未变检查廉价move_package_manifest区分目标源码source_paths与依赖源码dep_pathsmove_package_query结构性查询替代通读整个包module_summary签名与声明facts详细声明、属性与源位置dep_graph模块依赖call_graph包级调用function_usagefunction: module::function某函数直接与传递调用及闭包捕获。所有工具均接受package_path必须指向包含Move.toml的目录。十、最终报告三行收束spec_inf_report.md 规定任何策略结束时以至多三条紧凑要点收尾Result陈述新增的契约或不变量及最终验证/验收状态未解决则点名阻塞义务Strategy点名采用的方法与关键工具以及该策略为何适配此问题Decision points总结工作中最多两个关键抉择各附促成它的证据或结果省略常规步骤与逐轮转录。结语一次调用到验收的完整闭环综合以上模板move-inf工作流的端到端闭环可以概括为用move_package_wp在目标作用域含循环上做 WP 推断 → 按诊断逐函数补齐循环不变量并简化 → 以pragma opaque契约覆盖全部 result/abort/frame 行为 → 用move_spec_check做编译验证防弱化的最终验收 → 按三要点格式汇报。整个过程贯穿三条底线不弱化契约、不删除未解决的vacuous/sathard义务、不把工具缺陷当作修改规范的借口。这套方法论不仅适用于本仓库中 aptos-move/framework 等大量 Move 模块的规范补全也为任何希望以形式化验证手段保障 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），仅供参考