Aptos Move Prover 循环不变量证据Loop-Invariant Evidence为规范推断提供有界的循环头事实诊断【免费下载链接】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导读当 Move 函数中的循环缺少循环不变量时Move Prover 的规范推断Specification Inference会把该循环修改的状态进行 havoc随机化导致函数契约被标记为[inferred sathard]从而无法可靠使用。本文讲解 Aptos 仓库内 Move Prover 引入的一项可选、仅诊断diagnostic-only的输出能力——循环不变量证据Loop-Invariant Evidence它通过有界深度展开与割点cut-point最弱前置条件分析报告循环入口状态、入口事实、单次回边back-edge遍历的符号效果以及前几个循环头的路径条件化状态帮助人工或 Agent 推导出不变量。读完本文你将掌握该功能的命令行用法、诊断输出语义、三类证据状态exact / partial / unavailable、三条声学边界soundness boundary以及它在当前仓库中的实现落点。本文的规划与设计文档为 third_party/move/move-prover/doc/dev/loop_invariant_evidence.md实现证据可对照 bytecode-pipeline/src/loop_analysis.rs、bytecode-pipeline/src/spec_inference.rs、src/inference.rs 与 bytecode-pipeline/src/options.rs 阅读。背景无不变量循环如何产生sathard契约Move Prover 的循环分析处理器LoopAnalysisProcessor会把没有用户不变量的循环改写为有向无环图DAG在循环头插入assert L基础情形检查、havoc Thavoc 循环修改的目标、assume L重新假定不变量并将每个回边重定向到不变量检查块。当循环没有不变量L时等价于对循环修改的状态直接 havoc规范推断只能把相关条件量化为“任意值”于是函数契约被标记为[inferred sathard]——条件虽然成立但依赖求解器难以证明调用方无法依赖该契约。推断器会针对该循环发出如下告警WP inferredsathardconditions after this loop without an invariant. Add ordinary loop invariants, or, when the iteration is naturally a fold, consider an inline higher-order iterator with afolds_ofloop invariant.见 spec_inference.rs其中对 inline 展开产生的循环还会额外提示folds_of修复建议。问题在于告警只告诉调用者“这里缺不变量”却没有给出任何可用于推导不变量的线索。循环不变量证据正是为此而生——它描述循环携带的源可见状态、入口事实、一次回边遍历的符号效果、前几个循环头处的路径条件化状态让调用者从事实出发构造候选不变量。需要强调的是该输出不合成、不插入、也不验证不变量它只是推导不变量过程中的诊断辅助。用户契约--loop-invariant-evidence[N]选项该功能归属于推断命令默认关闭不改变普通验证行为也不修改推断出的 Move 源码。命令行形式为move-prover --inference --loop-invariant-evidence[N] ...其约束语义如下用法行为省略选项不执行任何额外分析不产生任何新输出提供选项但不带N使用默认深度 3N的含义统计完成的回边遍历次数因此报告包含head[0..N]取值限制拒绝 0初始实现上限为 8模式限制未启用 inference 模式时拒绝该选项这些约束在 src/inference.rs 中有源码级落实parse_loop_invariant_evidence_depth只接受 1..8 的整数clap 参数声明了requires inference、require_equals true、num_args 0..1default_value与default_missing_value均为3。CLI 字段解析后拷贝到内部 prover 选项loop_invariant_evidence_depth: Optionusize见 bytecode-pipeline/src/options.rs处理器可廉价地测试证据是否被请求。输出通道推断源码输出已有三种形式stdout、每模块文件、统一文件这些输出必须保持合法的 Move 源码因此证据通过推断错误写入器error writer以诊断diagnostics形式呈现而非混入生成的源码。结构化记录以LoopInvariantEvidence注解形式保存在FunctionData上直到SpecInferenceProcessor渲染它们——该处理器仅在函数确实产生了sathard条件时才渲染注解。此外该标志只是“请求”不是“必有可用证据”的承诺对不支持或不精确的循环报告给出简短原因而不是编造事实。诊断输出示例与语义设计文档给出了一个典型示例循环同时递减两个参数x、y当前诊断形状为warning: WP inferred sathard conditions after this loop without an invariant loop-invariant evidence (bounded to 3 back-edges; diagnostic only) source-visible loop-carried state: x, y bounded loop-head facts (for paths reaching each head): head[0]: head[0].x x head[0].y y head[1]: x 0 y 0 head[1].x x - 1 x 0 y 0 head[1].y y - 1 head[2]: x 1 y 1 head[2].x x - 2 x 1 y 1 head[2].y y - 2 head[3]: x 2 y 2 head[3].x x - 3 x 2 y 2 head[3].y y - 3 seek a predicate which includes the entry facts and is preserved by one back-edge; bounded observations are not an invariant or a proof关键点head[k]是诊断记号不是 Move 语法。参数与保留局部变量的名字来自FunctionTarget/FunctionEnv无法映射到源码的内部临时变量被省略并在完整性说明completeness note中报告。若循环体存在分支则保留路径条件而不是合并互不兼容的状态例如head[2], when choose_left: x a 2, y b head[2], when !choose_left: x a, y b 2路径与变量按确定性顺序排序若数量超过显示上限报告有多少被省略。在源码实现中渲染逻辑位于 spec_inference.rs首条 note 固定为常量LOOP_INVARIANT_EVIDENCE_NOTE loop-invariant evidence供消费者以文本选取避免与渲染文本漂移随后依次输出“carried state”行、状态行exact within the displayed bound或partial、按头组织的 facts、partial 说明与结尾的“seek a predicate ...”提示。证据的含义三条不变量义务与有界性设H为源可见的循环携带值向量候选不变量P(H)必须满足经典的三条义务entry(H) P(H) establishment建立 P(H) guard(H) body P(H) preservation保持 P(H) !guard(H) Q(H) sufficiency对期望延续 Q 的充分性在候选P存在之前谈不上建立或保持失败而在推断期间可能还没有固定的后置条件Q推断是在构造函数摘要而非证明用户给定的摘要。因此诊断只为前两条义务报告证据不会声称三条义务中的某一条失败。调用者写出不变量后普通验证会分别报告基础base与归纳induction失败充分性则交由循环之后未证明的断言或后置条件表达。有界性每个head[k]事实只关于“恰好经过k次回边到达该头”的路径不涉及head[k1]或任意满足候选公式的状态。报告始终包含边界说明与文末的警告“bounded observations are not an invariant or a proof”。设计文档同时指出循环局部的单步关系one-step relation比有界头列表更有通用价值因为它展示保持义务需要覆盖什么该关系是计划中的扩展。当前已实现的有界头仍然有价值因为它们在不声称归纳的前提下暴露了累积模式与分支依赖状态。三种证据状态每份报告具有三种状态之一exact within the bound边界内精确有界 DAG 中每条到达路径都被分析且每个展示的携带值都有符号表达式partial部分展示的事实有效但某条路径、值或内存效果因无法紧凑表示而被省略unavailable不可用没有保留下有用的源码级关系。部分输出可以省略事实但不得弱化路径条件并把结果表述为无条件。未知值渲染为 unknown 或被省略绝不渲染成不受约束的等式。声学边界三条红线设计文档明确划定了三条 soundness 边界实现严格规避不从不可解释谓词uninterpreted predicate的模型中读出不变量。在一阶有效性查询中Z3 可以自由地为缺失不变量I赋予任何与断言公式兼容的解释它求解的并不是“寻找归纳不变量”的二阶问题显示的函数表可能是任意甚至退化的。因此实现不断言!I、不解析模型表、也不把模型条目描述为循环状态。CHC 求解或基于 Spacer 的不变量合成属于另一个独立项目。不把有界观测当作循环不变量发出。一个事实在深度N内每条被观测路径上都成立仍可能在任意满足它的状态上归纳失败即使是有守卫的行如i 2 r old(r) 2通常也不保持——转换可能从未被观测的状态进入该守卫值。第一版只发诊断不添加Condition值不写入循环spec块也不使用[inferred unrolled]标记。未来的源码编辑功能只有在每个子句被独立检查并明确区别于已接受的推断输出时才可能发出注释或候选子句。不把普通 WP 注解重新解释为前向状态。WPAnnotation当前把代码偏移映射到“足以让该偏移处的后缀到达函数出口”的条件它是向后义务不是该偏移处可达的符号状态。在复制的循环头上读这个注解会颠倒其含义。循环头证据需要下面描述的显式割点分析。分析设计四步流水线证据 pass 复用推断引擎的表达式与字节码语义但运行在隔离的FunctionData上从不更新函数的Spec。第 1 步筛选合格循环先运行普通推断。一个函数合格当且仅当至少有一条发出的条件为[inferred sathard]LoopsWithoutInvariants识别出至少一个源码循环该函数位于请求的推断作用域内。这是相关性correlation不是因果证明。存在多个缺失循环时把每个都报告为可能的精度损失来源。仅由不可信result_of载体造成的sathard条件不产生循环证据。实现上loop_analysis.rs 中的LoopWithoutInvariant除Loc与is_inlined外还扩展了稳定的循环标识符loop_id、原始头header以及FatLoopSpecInfo::{val_targets, mut_targets, mem_targets}的源可见子集carried并在LoopAnalysisProcessor::transform用 havoc 替换循环之前保留诊断 pass 所需的变换前数据。第 2 步构建隔离的有界 DAG对每个合格循环一次处理一个克隆规范化后的循环前FunctionData对没有作者不变量的循环强制展开到深度N当前实现仅在恰好存在一个此类循环时继续其他缺失循环按普通方式抽象havoc 摘要从展开中返回确定的k - copied_header映射在克隆的 shadow 数据上运行诊断 WP 查询。LoopAnalysisProcessor::unroll被重构为返回头映射而非丢弃局部映射普通流水线忽略该映射证据流水线消费它。shadow 数据的任何展开标记、复制的指令、推断条件或注解都不得进入主 target 持有者或生成的源码。第 3 步计算割点关系已实现的入口到头entry-to-head查询对每个复制的头在其 label 之后立即插入合成的Stop并用head[k].v current(v)种入该精确指令。在该诊断分析器模式下普通 return、abort 及其他 stop 都是中性出口neutral exits现有的分支感知向后连接backward join因此保留到达被选 stop 的路径上的守卫离开循环或在别处终止的路径不贡献伪造的等式。报告把每一行显式限定在到达该头的路径上。普通规范化与简化路径被复用但禁用模型变更查询不调用update_spec、公共子表达式提取、frame 发射或坏临时变量诊断。表达式通过 Move sourcifier 渲染任何仍暴露$临时变量的条件都被省略。这产生建立事实head[0]与累积的有界入口到head[k]关系但暂不产生对任意循环头状态全称量化的转换。计划中的循环局部查询把内部 WP 分析器推广出诊断入口接受起点割点、一个或多个终点割点以及命名快照值上的种子关系。对每个携带值v在复制头k处种入snapshot[k].v current(v)并计算reaches[k]在复制头k处种入true、在每个其他割点出口种入false再传播到复制头 0——这一区分至关重要在普通部分正确性 WP 下提前退出割点的路径可能空泛地满足快照等式。随后从复制头k向后运行既有转移函数到复制头 0把 head 0 的状态重命名为head.v并用reaches[k]守卫每个快照关系得到“实际到达割点的执行”的路径条件化关系。k 1时就是单回边转换更大的k是有界累积证据。再从函数入口到 head 0 跑第二次割点得到以参数与函数入口内存表达的建立事实并与循环局部转换关系分开存放。割点运行必须保留普通分析器的分支敏感连接、abort 语义、变更处理与状态标签且不得调用update_spec、cse_inferred_conditions或emit_modifies。设计文档给出的小结果类型如下struct LoopInvariantEvidence { function: QualifiedIdFunId, loop_id: usize, loc: Loc, depth: usize, carried: VecLoopValue, entry: VecPathRelation, step: VecPathRelation, heads: VecHeadEvidence, completeness: EvidenceCompleteness, omissions: VecString, }当前记录存于主函数数据上的LoopInvariantEvidence注解中只有字符串与循环元数据被从隔离分析拷贝进注解shadow 字节码不进入。第 4 步为显示简化对每条关系使用推断简化器但只应用保持蕴含方向的变换保留路径谓词移除重言式与重复等式不求解递推或猜测闭式不使用求解器导出的具体值优先使用源码名与源码级操作对表达式大小、路径数与行数设置上限并给出显式省略说明。若关系仍含内部临时变量先尝试既有的替换与源码名机制若仍为内部变量则省略该值并把报告标记为 partial而不是打印$t17。当前代码中的落点选项与驱动src/inference.rs定义仅推断模式的 CLI 字段loop_invariant_evidence并把深度拷贝到内部 prover 选项诊断继续走既有 model diagnostic / error-writer 路径stdout / file / unified 源码输出不变。bytecode-pipeline/src/options.rs携带内部Optionusize深度供处理器廉价测试证据是否被请求公开选项仍归组在InferenceOptions下。循环发现与展开bytecode-pipeline/src/loop_analysis.rs丰富LoopsWithoutInvariants、保留被选循环的变换前输入并暴露强制展开的复制头映射。其中的MAX_BOUNDED_EVIDENCE_WORK 512与MAX_BOUNDED_EVIDENCE_PATHS 512是两个预算常量当loop_count² × (depth 1)超出工作预算或(depth 1)^unrolled_loops超出路径预算时报告直接标记为 unavailable 并附原因。move-model/bytecode/src/fat_loop.rs抽出LoopUnrollingMark的构造使诊断请求可以强制缺失循环展开而无需添加源码 pragma。推断分析bytecode-pipeline/src/spec_inference.rs把分析与模型变更分离。普通路径继续用update_spec应用入口摘要诊断路径调用割点分析器并只返回证据记录。当前切片不需要额外流水线处理器——循环分析记录隔离结果既有推断处理器负责渲染。避免第二个GlobalEnv位置、符号、类型与源码映射已属于主环境隔离停留在拥有的FunctionData与结果记录层。作用域与刻意降级Scope and Degradation第一版支持可归约、非嵌套的源码循环其携带状态可命名为局部变量、参数或可变引用值对不支持的情况刻意降级情形v1 行为多个缺失循环当前报告证据不可用后续循环局部查询可分别分析而不产生错误归因嵌套循环先分析最内层循环若界定嵌套循环会使路径倍增则 v1 把外层循环报告为 unavailableinline 展开的循环保留 inline 源码链优先使用既有folds_of修复指导仅当携带值有可用源码名时展示证据不透明调用或 native 效应有可用符号摘要时保留否则把受影响值标为 unknown、报告标为 partial全局内存当前切片省略并标记 partial后续版本可能仅在地址与类型可表示时报告globalT(address)被选体内的非确定性或 havoc按既有 WP 语义量化或标为 unknown不把全称不确定性变成具体样本提前 return 或 abort只保留到达被请求复制头的路径并说明排除了多少条终止路径成本与确定性普通推断运行不变。对合格的函数请求证据会构建一个有界 shadow DAG 并运行N 1次割点 WP 查询工作量随展开 DAG 与分支数增长因此深度上限为 8、每个头的显示事实上限为 8。不分析依赖项的证据。该设计不调用 Boogie 也不调用 Z3因此对固定源码与固定深度记录输出是确定性的stable_test_output可以规范化路径与名字但不得用脱敏占位符替换有用关系。若未来引入包级推断截止时间证据是尽力而为的先完成普通推断源码再以显式的不完整说明停止证据收集。测试策略声学性与隔离启用证据后推断条件、frame、pragma 与生成的源码逐字节不变shadow 展开与割点种子从不出现于主 target 数据或模型Spec每个无条件的显示等式都被“所有到达该头的有界路径”蕴含分支特定等式保留其路径谓词在复制头之前终止的路径在诊断模式下是中性出口分支感知连接保留到达合成割点的路径上的守卫不支持的状态成为省略或 unknown绝不成为具体值诊断中不出现原始临时变量、标签或 Boogie 名字。基线Baselines初始确定性基线覆盖两个携带参数、带守卫的有界头、面向源码的渲染、省略说明与深度。设计文档还要求补充以下推断诊断基线累加器sum_to_n几何增长double_n_times含两个保留路径谓词的条件体在请求深度之前退出的循环可变引用状态多个缺失循环inline 展开的 fold嵌套循环降级产生无循环证据的非循环sathard结果。基线 harness 不得运行求解器每个聚焦测试在正常预热测试环境下应低于 20 秒含编译。分析器检查head 0 是实际循环入口不是函数入口或循环出口headk对应恰好k次完成的回边单步证据在深度 1 直接请求与作为更深请求的第一步请求时完全一致排序在 map/set 迭代顺序变化下保持稳定表达式与路径上限产生显式省略计数。交付序列、评估与非目标交付序列✅ 已交付选项、结果类型与确定性诊断渲染器✅ 已交付保留循环身份/携带目标并返回复制头映射选项缺席时普通推断不变✅ 已交付从非变更割点路径中抽出模型变更并对head[0..N]发出入口到头关系⏭ 下一步通用循环局部单步关系、显式可达谓词与可分别归因的多循环分析评估累积头是否实质改善不变量提案除非证据支持经单独评审的设计否则不添加源码编辑。评估应在新颖循环上测量而非开发轮次中从公共推断 fixtures 复制的任务至少评估调用者是否提出同时通过基础与归纳的不变量从首个缺失循环诊断到验证通过不变量的轮次与墙钟时间请求报告中 exact / partial / unavailable 的比例不同深度下的证据大小与分析时间以及“误用假象”调用者把有界模式误当成已证明不变量的案例。有用结果的判定不是“看起来合理的公式”而是到达一个普通 prover 能独立验证的不变量所需努力的减少。非目标明确排除避免与主项目其他方向混淆不变量合成或 CHC 求解自动插入循环spec块改变[inferred sathard]的含义在验证或推断中默认启用该功能把 MoveFlow 或其求值分支作为核心实现的一部分修改把有界证据用作超出请求深度的证明。小结循环不变量证据为“缺不变量 →sathard”这一常见推断失败模式补上了缺失的中间事实通过--inference --loop-invariant-evidence[N]默认深度 3上限 8触发它在隔离的 shadow 数据上有界展开循环、插入合成割点、运行分支感知的向后 WP 查询最终以诊断形式输出入口事实与head[0..N]的路径条件化关系。它严格恪守三条声学边界——不从不可解释谓词模型读不变量、不把有界观测当证明、不颠倒 WP 注解的方向——因此“给出推导不变量的线索”与“声称证明”之间始终有清晰界限。对于正在使用 Move 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考