企业官网建设流程全解析

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 T（havoc 循环修改的目标）、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] ...

其约束语义如下：

这些约束在 src/inference.rs 中有源码级落实：parse_loop_invariant_evidence_depth只接受 1..=8 的整数，clap 参数声明了requires = "inference"、require_equals = true、num_args = 0..=1，default_value与default_missing_value均为"3"。CLI 字段解析后拷贝到内部 prover 选项loop_invariant_evidence_depth: Option<usize>（见 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[k+1]或任意满足候选公式的状态。报告始终包含边界说明与文末的警告（“bounded observations are not an invariant or a proof”）。

设计文档同时指出：循环局部的单步关系（one-step relation）比有界头列表更有通用价值，因为它展示保持义务需要覆盖什么；该关系是计划中的扩展。当前已实现的有界头仍然有价值，因为它们在不声称归纳的前提下暴露了累积模式与分支依赖状态。

三种证据状态

每份报告具有三种状态之一：

• exact within the bound（边界内精确）：有界 DAG 中每条到达路径都被分析，且每个展示的携带值都有符号表达式；
• partial（部分）：展示的事实有效，但某条路径、值或内存效果因无法紧凑表示而被省略；
• unavailable（不可用）：没有保留下有用的源码级关系。

部分输出可以省略事实，但不得弱化路径条件并把结果表述为无条件。未知值渲染为 unknown 或被省略，绝不渲染成不受约束的等式。

声学边界：三条红线

设计文档明确划定了三条 soundness 边界，实现严格规避：

1. 不从不可解释谓词（uninterpreted predicate）的模型中读出不变量。在一阶有效性查询中，Z3 可以自由地为缺失不变量I赋予任何与断言公式兼容的解释，它求解的并不是“寻找归纳不变量”的二阶问题，显示的函数表可能是任意甚至退化的。因此实现不断言!I、不解析模型表、也不把模型条目描述为循环状态。CHC 求解或基于 Spacer 的不变量合成属于另一个独立项目。
2. 不把有界观测当作循环不变量发出。一个事实在深度N内每条被观测路径上都成立，仍可能在任意满足它的状态上归纳失败；即使是有守卫的行（如i == 2 ==> r == old(r) + 2）通常也不保持——转换可能从未被观测的状态进入该守卫值。第一版只发诊断，不添加Condition值，不写入循环spec块，也不使用[inferred = unrolled]标记。未来的源码编辑功能只有在每个子句被独立检查并明确区别于已接受的推断输出时，才可能发出注释或候选子句。
3. 不把普通 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

对每个合格循环，一次处理一个：

1. 克隆规范化后的循环前FunctionData；
2. 对没有作者不变量的循环强制展开到深度N（当前实现仅在恰好存在一个此类循环时继续）；
3. 其他缺失循环按普通方式抽象（havoc 摘要）；
4. 从展开中返回确定的k -> copied_header映射；
5. 在克隆的 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: QualifiedId<FunId>, loop_id: usize, loc: Loc, depth: usize, carried: Vec<LoopValue>, entry: Vec<PathRelation>, step: Vec<PathRelation>, heads: Vec<HeadEvidence>, completeness: EvidenceCompleteness, omissions: Vec<String>, }

当前记录存于主函数数据上的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：携带内部Option<usize>深度，供处理器廉价测试证据是否被请求；公开选项仍归组在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）

第一版支持可归约、非嵌套的源码循环，其携带状态可命名为局部变量、参数或可变引用值；对不支持的情况刻意降级：

成本与确定性

普通推断运行不变。对合格的函数，请求证据会构建一个有界 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 迭代顺序变化下保持稳定；
• 表达式与路径上限产生显式省略计数。

交付序列、评估与非目标

交付序列：

1. ✅ 已交付：选项、结果类型与确定性诊断渲染器；
2. ✅ 已交付：保留循环身份/携带目标并返回复制头映射，选项缺席时普通推断不变；
3. ✅ 已交付：从非变更割点路径中抽出模型变更，并对head[0..=N]发出入口到头关系；
4. ⏭ 下一步：通用循环局部单步关系、显式可达谓词与可分别归因的多循环分析；
5. 评估累积头是否实质改善不变量提案；除非证据支持经单独评审的设计，否则不添加源码编辑。

评估：应在新颖循环上测量（而非开发轮次中从公共推断 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