Move Prover 框架的形式化验证从 Move IR 到 IVL 的最弱前置条件、循环切割与端到端可靠性证明【免费下载链接】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 仓库中third_party/move/lean/v0/move-model的 Lean 形式化模型为对象系统讲解 Move Prover 验证管线的核心骨架——状态多态的中间验证语言IVL、关系语义与最弱前置条件演算、循环不变式的切割与可靠性理论以及从 Move IR 到 IVL 的编译、前向模拟与端到端契约充分性证明。读完本文你将掌握该模型中源码函数 → 编译为 IVL 块图 → 在 Lean 内生成验证条件 → 用prover_sound建立契约语义的完整证据链并能沿模块索引深入源码继续研究。1. 背景在 Lean 中形式化验证器的验证器生产环境中的 Move Prover 是一个把 Move 智能合约翻译为 Boogie 中间语言、再由 SMT 求解器完成验证的庞大工具链。third_party/move/lean/v0/move-model/MoveModel/Prover/README.md所描述的不是这一完整生产工具而是在 Lean 证明助手中对验证关键阶段的选择性形式化它覆盖了被建模的 IR 片段而非完整的生产 Move Prover 或每一个 Move 语言特性。该包建立在 Move IR 框架 之上包含四部分核心内容一种小型、状态多态state-polymorphic的中间验证语言IVLIVL 的关系语义与最弱前置条件weakest-precondition演算循环切割loop cutting与循环不变式的可靠性理论从 Move IR 到 IVL 的编译器、其前向模拟forward simulation以及端到端契约充分性contract adequacy。关键设计原则是Move IR 保持为表示、执行、分析与变换代码的通用框架本包只消费它的语法与语义不向 IR 本身添加任何 prover 专属构造。设计依据来自两篇关于生产 Move Prover 的论文TACAS 2022Dill、Grieskamp、Park、Qadeer、Xu、Zhong《Fast and Reliable Formal Verification of Smart Contracts with the Move Prover》arXiv:2110.08362FMCAD 2026Grieskamp、Zhang、Kashyap、Silverman《Formal Verification of Imperative First-Class Functions in Move》。从源码结构看该模型与仓库中的 Move 形式化体系third_party/move/lean/v0/move-model/MoveModel/IR/、Frontend/、Tests/同处一个 Lean 工程中MoveModel.lean、lakefile.toml、lean-toolchain等文件表明它按标准 Lean 工程组织可直接构建验证。2. 模块层级谁构建在谁之上README 给出的模块层级图揭示了清晰的依赖关系——箭头指向构建于其上的模块跨包的节点标注的是 prover 用到的主要 IR 概念而非每一次直接的 Lean importMove IR framework State-polymorphic IVL Move IR to IVL ┌──────────────────────┐ ┌───────────────────────┐ ┌──────────────────────┐ │ IRSyntax (Program, │ │ IvlSyntax ──▶ IvlSem │ │ Compile ──▶ Sim │ │ FunDecl, CFG, │ │ │ │ │ │ │ │ │ │ Instr) │ │ ▼ ▼ │ │ ▼ ▼ │ │ IRSpec (SpecExp, │ │ Wp ────▶ WpSound │ │ Adequacy │ │ Contract) │ │ │ │ │ │ │ IRSem (RunFrom, │ │ ▼ │ │ │ │ FunExec) │ │ LoopCut │ │ │ │ IRTyping (WfProg, │ └───────────────────────┘ │ │ │ TypedLocals, │ ▲ │ │ │ TypedMemory) │ │ │ │ │ IRExec (RunFrom. │ └─────── WpSound ──▶ Sim / Adequacy │ │ inductGrouped) │ │ └──────────────────────┘ │ │ IRSyntax/IRSpec/IvlSyntax/Wp ──▶ Compile │ │ IRSem/IRTyping/IRExec ──▶ SimIRSem ──▶ Adequacy │ └──────────────────────────────────────────────────────────────────────────────────┘IR 层提供语法Program、FunDecl、CFG、Instr、规范SpecExp、Contract、语义RunFrom、FunExec、类型WfProg、TypedLocals、TypedMemory以及证明模板RunFrom.inductGroupedIVL 层自底向上为语法 → 语义 → WP → WP 可靠性 → 循环切割翻译层中Compile依赖 IR 语法/规范、IVL 语法与 WPSim与Adequacy依赖 IR 语义/类型/执行模板与WpSound。这个分层意味着IVL 理论完全独立于 Move IR而翻译层把两者粘合起来形成每个 IVL 定理只需在状态类型σ上做多态证明Move 具体状态作为实例注入的架构。3. 验证流程一条从源码函数到契约可靠性的流水线验证流程README 的 verification flow 图是一条清晰的单向流水线Move IR function (FunDecl Contract) │ compileFun ▼ IVL BProgram VState compAnns │ ▼ Verified∃ fuel, wpB at entry 在 Lean 内部生成的验证条件 │ ▼ sim_aux源执行在 IVL 中的表示 │ ▼ funExec_conforms │ ▼ prover_soundSatisfiesContractcompileFun用VState实例化泛型 IVL 状态。除当前的MoveState外VState还携带入口参数、返回值、保存的内存快照以及编码后的 abort 标志深层的SpecExp表达式被解释为该状态上的浅层 Lean 谓词验证条件是 Lean 内部直接定义的wpB见第 5 节以∃ fuel, wpB …的形式陈述而非转交给外部 Boogie/SMTsim_aux是主归纳把一次源执行表示为 IVL 执行funExec_conforms证明一次满足requires的良类型源执行符合声明的契约prover_sound把每个已编译函数都可验证提升为每个声明的源码函数都满足其语义契约。4. 设计对应关系源码如何映射到 IVLREADME 的 Design correspondence 一节总结了六个关键映射这些映射在源码中均可找到对应实现控制流与规范分离Move 代码保持三地址 CFG而契约与循环不变式使用深层SpecExp语言内存标签表示保存的状态如 pre-stateIVL 编译器将这些表达式表示为VState上的 Lean 谓词状态多态IVL 的块结构是深层语法而守卫、赋值、havoc 关系、断言与假设都是所选状态上的浅层函数或谓词循环不变式规则wpB实现了不变式规则loopCut给出等价的显式程序变换并证明它产生无环、最弱前置条件等价的图见第 6 节Abort 变为数据流Move 的 abort 在VState中变成数据流——编译后的指令更新 abort 标志终止符路由到不同的正常退出块与 abort 退出块契约检查被注入到这两类退出块中。VState中的aborted : Option Nat字段Translate/Compile.lean中的structure VState正是 Boogie$abort_flag/$abort_code的对应物调用采用不透明契约摘要源码调用执行具体被调方函数体编译后的调用则使用不透明契约摘要——先断言前置条件再 havoc 出一个满足被调方契约与 frame 的 aborting 或 normal 结果对应 TACAS 2022 Fig. 9 的 opaque schema;逐块对应源块b映射到 IVL 块b 1其余标签为入口桩label 0与两个退出块size 1与size 2这使模拟可以逐块进行。其中Move 引用消除reference elimination是 IR 到 IR 的预处理过程实现在IR/RefElim/Transform.lean直接翻译会把剩余的引用指令故意映射为失败的断言因此验证含引用的输入需先经过引用消除阶段。5. IVL 核心概念Boogie 风格的块图与 WP 演算IVL 独立于 Move IR由其状态类型σ参数化。源码Ivl/Syntax.lean给出了精确定义BCmd σ直线命令的深层归纳类型提供四种命令assign f—— 确定性更新s ↦ f s对应 Boogie 的x : ehavoc R—— 非确定性更新任意满足R s s的sassume p—— 假设仅从满足p的状态继续assert p—— 断言p不成立则失败BTerm σ带守卫的goto目标是List ((σ → Prop) × Label)或正常结束ret。守卫设为True即模拟 Boogie 的非确定性多目标goto互补守卫模拟条件分支——Boogie 用目标块的假设表达后者此 IVL 把条件直接放在边上BBlock σ命令列表加终止符BProgram σ标签到块的部分映射加入口标签LoopAnn σ提供不变式inv、循环目标关系targets与循环成员membersAnns σ是从头标签到LoopAnn的部分映射noAnns即无环程序的空注解映射。Ivl/Wp.lean将验证条件生成器用 Lean 直接定义为块图上的最弱前置条件演算而非转交 Boogie直线命令的 WP 是递归定义的wpCmdsassign向后代入f shavoc对s全称量化assume取蕴含assert取合取wpB G anns rank Q fuel l是从块l出发安全且每个正常结果满足Q的最弱前置条件沿前向边以fuel做结构递归fuel 0时是FalsewpB_fuel_mono保证wpB对 fuel 单调因此验证条件写成∃ fuel, wpB …边分类rank l rank l是前向边递归进入目标rank l ≤ rank l是回边必须指向带注解的头其前置条件即头不变式在带注解的头处wpB先检查不变式再从任意满足不变式的 target 相关状态继续——这建模了havoc targets; assume I副作用条件WfProgram承载不变式规则所需的全部假设是 fat-loop 识别与目标分析target analysis的语义对应物backMember、entryAtHeader、headerMember、nestedMember描述可归约 CFG 的自然循环结构targetsRefl、targetsClosed声明目标关系自反且覆盖循环块的所有改变。WfProgram与 Move IR 的类型检查无关——同名源属性是WfProgIR/CodeTyping.leanREADME 特别提醒避免混淆。注意一个工程细节wpCmds刻意不加[simp]因为对很长的直线块一次展开整个嵌套会让 kernel 检查成本随块长度超线性增长证明通过Translate.wpCmds_onOk_step一条命令一条命令地推进。6. 循环切割把不变式规则变成程序变换生产 Move Prover 在验证前重写循环LoopAnalysisProcessor而wpB在演算内部处理循环不变式。Ivl/LoopCut.lean为 IVL 实现了同样的变换在循环头插入assert I; havoc targets; assume I基础情形然后是一个任意的 target 相关迭代状态每个循环追加一个全新的块X assert I; stop归纳步其中stop即assume False; ret把所有回边重定向到X。loopCut为每个带注解的头h分配新标签base hCutOk要求base超过所有原始标签、maxR超过所有原始 rankcutRank把新块映射到maxR。主要结论把变换后的程序与注解演算连接起来loopCut_wp切割程序上无注解的 WP 等于原带注解程序上的wpBloopCut_acyclic切割程序每条边都严格增大扩展 rank结果是 DAGwpB_complete在无环无注解程序上每个执行的语义安全蕴含其最弱前置条件。这组定理使循环不变式规则获得了双重表述——演算内规则wpB与显式变换loopCut两者 WP 等价且变换保证无环。7. 编译与模拟从 Move IR 到 IVL 的正确性7.1 规范注入Translate/Compile.lean该模块形式化规范注入TACAS 2022 §3.2 与 Appendix A 的SpecInstrumentationProcessor把字节码函数与其契约编译为 IVL 程序IVL 断言的安全性蕴含契约。编译中深层规范表达式被解释为基于验证状态构建的SpecEnv上的浅层谓词。验证状态VState含当前字节码状态与四个仅验证用的组件——内存快照、入口参数、返回值、abort 标志。preLabel标识入口内存赋予old(..)意义块布局源块b变为 IVL 块b 1label 0 是入口桩size 1/size 2是返回与 abort 退出块。源码标识符按代码顺序排列因此恒等 rank 把回边识别为 rank 非增边非调用指令每个非调用指令变成一个由onOk守卫的确定性赋值$AddU64这类操作失败时置 abort 标志编译后的终止符每块检查一次该标志必要时路由到 abort 退出不透明调用模式TACAS 2022 Fig. 9在块内是两个命令assert requires; havoc { abort 分支flag : some code, aborts 成立 | normal 分支memory 在 modifies 内被 havoc, ensures ∧ frame }退出检查TACAS 2022 Fig. 8abort 退出断言aborts_if返回退出断言其否定加上ensures与modifiesframe。两个退出一起强制 abort 条件的双条件语义卡死处理源码语义中类型不当的情形会卡死编译代码将其视为 no-op或不可证的验证条件。由于卡死配置没有源结果这对模拟是可靠的对良类型程序也无影响。7.2 前向模拟Translate/Sim.lean该模块证明翻译正确性的前向方向每条字节码执行都被一条 IVL 执行表示。编译程序含有断言包括被调方前置条件可能在表示某次源运行时失败——但已验证程序排除了失败分支。它通过 abort 标志编码复现源结果OutRel正常返回 标志为none且内存与rets一致abort 标志携带代码。主归纳sim_aux沿大步执行推导进行直接处理互递归函数并同时确立三个性质模拟编译执行逐命令构建ContRun抬起的 abort 标志跳过块余下部分直达 abort 退出契约符合Conforms构造运行沿途记录的退出块断言翻译到外围边界类型保持TypedLocals、TypedMemory、OutTyped在调用点满足SatisfiesContract与callRel的类型前提。调用时归纳假设模拟被调方函数体再前缀入口桩调用点类型与已断言的前置条件确立其假设被调方的Verified证明给出wpB_safe排除失败并产生callRel所需的符合事实。由于源块与 IVL 块一一对应源b↦ 标签b 1公开的compile_simulates定理是逐块的。8. 端到端充分性prover_sound主定理Translate/Adequacy.lean给出分层架构的最终定理如果良类型程序的每个函数都可验证——即其编译程序在 Lean 侧的 WP 对所有边界状态成立——那么每个函数都满足其声明的契约。其陈述在源码中精确可见theorem prover_sound (P : Program) (hwfP : WfProg P) (hwf : ∀ f d, P.funs f some d → WfProgram (compileFun P d) (compAnns P d) (fun l l)) (hverified : ∀ f d, P.funs f some d → Verified P f) : ∀ f d, P.funs f some d → SatisfiesContract P f d证明组合Sim.lean的结果主归纳sim_aux跟随大步执行推导直接处理递归调用而非对调用图归纳模拟在编译执行中携带契约符合与类型保持。wpB_sound/wpB_safe排除断言失败分支剩余的退出断言建立SatisfiesContract包括aborts_if的双条件解释。定理有两个良构假设WfProg字节码验证保证的源类型与每个编译函数的WfProgram保证正确的循环结构与完整的循环目标。9. 主定理层级一览README 总结了完整定理层级可作为深入源码的索引定理含义Ivl.wpB_sound满足wpB的 IVL 状态无法到达断言失败且每个正常执行满足后置条件Ivl.wpB_safe、Ivl.wpB_postwpB_sound的安全-only 与正常后置条件投影Ivl.loopCut_wp注解循环规则与显式 loop-cut 程序具有相同的最弱前置条件Ivl.loopCut_acyclicloop-cut 程序的每条边严格增大其扩展 rankIvl.wpB_complete无环无注解 IVL 程序上语义安全蕴含wpBTranslate.sim_aux在 IVL 中表示源执行的主归纳同时携带类型与契约事实Translate.compile_simulates公开的逐块前向模拟定理Translate.contract_call_overapproximates编译的不透明调用模式覆盖满足契约的被调方的具体执行Translate.funExec_conforms一次满足requires的良类型源执行符合声明的契约Translate.prover_sound若每个编译函数可验证则每个声明的源码函数满足其语义契约MoveModel/Prover下的所有声明均无sorry地完成证明。引用消除也在明确的前端证书下于概念 IR 模型层面证明其范围与剩余证书细化工作在 IR 路线图 中跟踪。10. 语义范围这个模型证明什么、不证明什么SatisfiesContract给aborts_if以每次执行的逐执行双条件读法正常执行要求条件为假abort 执行要求条件成立。它同时确立两种生产上下文定义退出使用退出内存不透明调用使用入口内存。省略aborts_if不做任何 abort 声明写aborts_if false禁止 abort规范求值是关系式且部分的未定义操作读缺失资源、除零没有求值逻辑连接词短路因此带守卫的资源读取仍可用交换检查器exchange checker拒绝规范中的可变引用局部变量与结果、非字面量或零除数以及循环不变式中对局部变量的old(..)——在 Lean 规范模型表示隐式可变引用解引用、非零证明义务与循环入口局部快照之前这些是保守的前端限制Contract.modifies在此模型中是强制完整足迹空列表断言全局内存不变——与生产 prover 不同此处省略并不禁用 frame 检查IR 执行关系刻意无类型畸形状态可能卡死prover_sound假设WfProg与类型化边界值对应字节码验证器与生产编码的多排序有效性检查运行时 abort 当前只用一个固定代码契约不约束 abort 代码引用指令在 IR 中执行但编译为失败断言因此验证含引用的输入先走 IR 引用消除阶段。11. 证据状态与路线图就当前建模的 IR、IVL 与翻译定义而言已实现的证明链不含任何sorryIVL 执行与最弱前置条件、WP 可靠性、循环切割与无环完备性、规范注入、逐块前向模拟、不透明调用过近似、契约符合以及条件端到端定理prover_sound均已证明。该定理假设源类型、良构循环元数据与每个编译函数的验证——这并不确立未建模 Move 特性或完整生产 prover 管线的正确性。示例在MoveModel/Examples中演练算术契约、循环、全局内存、内嵌 masm 与 Move 源码、引用消除与跨调用契约推理。尤其MoveModel/Examples/Adequacy.lean构造良构源程序与编译 IVL 证书证明Verified并在每个假设都已实例化的情况下应用prover_sound——这使意外破坏定理可用性的改动对 Lean 构建可见。未来 prover 工作刻意记录在此处而非仓库 README数据与全局不变式包括不变式挂起与访问/修改分析TACAS 2022 §3.2高阶函数值闭包、参数与字段变体、行为谓词、动态调用FMCAD 2026 §III带标签的一状态与两状态谓词的状态标签、存在中间状态、标签 DAG 上的 abort 合成有限验证单态化基础given 类型根、基于类型统一的资源标签碰撞实例、组合效应与泛型调用点闭包、无 binder 函数物化MoveModel.IR.Mono.Transform把每个物化的 given/碰撞/调用闭包代表送入既有 IVL 充分性定理MonoVerification.specializedSound证明结构单态化层生成声明查找、binder 与 arity 保持、类型替换的运行时标签相等、认证生成调用目标、调用重写结构、原语语义同余、局部指令/路径传输MoveModel.IR.Mono.Correctness下各模块从发现算法消解MonoPlan.Certificate.tagCoverage并从覆盖的闭源实例证明到其代表的资源键重命名桥——证书显式陈述 TACAS 2022 §3.3 中留作非形式论证的有限实例覆盖论证Mono.Correct.Coverage现已提供该桥所需的函数式、单射观察键关系与观察内存关系剩余定理必须将其穿过 CFG 执行与泛型调用提升字节码 CFG 上基于 WP 的规范推断层。12. 包边界与阅读指南该 Lean 工程的包边界约定是通用 IVL 语法、语义与验证条件理论放在MoveModel/Prover/Ivl保持Ivl状态多态Move 专属状态与规范解释属于MoveModel/Prover/Translate编译与跨语言正确性放在MoveModel/Prover/Translate可复用的 Move IR 概念、分析、执行模板与 IR 到 IR 变换放在MoveModel/IR前端解码与源码细化放在MoveModel/Frontend。每个公开声明都应有简洁的文档注释说明其代表或证明什么、属于哪个抽象层。按此边界的推荐阅读路径先读Ivl/Syntax.lean与Ivl/Semantics.lean建立 IVL 语法与关系执行再读Ivl/Wp.lean与Ivl/WpSound.lean理解 WP 演算及其可靠性随后用Ivl/LoopCut.lean看循环到 DAG 的变换最后依次阅读Translate/Compile.lean、Translate/Sim.lean与Translate/Adequacy.lean抵达端到端prover_sound。测试用例集中在MoveModel/Tests/Prover/Account、CountDown、CrossCall、BorrowAccount、ElimSource、MasmSource、MoveSource、Adequacy 等可与理论模块对照阅读。【免费下载链接】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），仅供参考