Leaner 语义管线重构以 Validated LIR 驱动 Elaboration、验证与执行的设计与实践【免费下载链接】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 仓库内 Leaner 形式化验证工具链的一份核心设计文档解读原始文档位于 designs/elaboration-design.md。Leaner 是仓库中基于 Lean 定理证明器构建的 Move/Rust 智能合约验证栈本文档定义了它的一次关键架构迁移将源码级 elaboration 验证的双路径模式收敛为以经过校验的 Leaner IRLIR为唯一语义输入的单一路径。读完本文你将理解 Leaner 如何用RawUnit → validate → ValidatedUnit管道统一 Move、Leaner 源码与 Rust MIR 三个前端如何用结构化 big-step 语义 有燃料解释器 语义最弱前置条件WP构建可证明正确的执行与验证体系以及 M0–M7 的渐进式迁移策略与完整正确性义务清单。一、背景与动机为什么要消灭第二条语义路径1.1 术语澄清Elaboration 的两层含义Leaner 原先的 Elaboration 一词同时混淆了两个本应分离的操作而新架构将它们严格分开前端 elaborationFrontend elaboration解析并解析resolve一种源语言产出一个带源码位置和对齐证据的RawUnitLIR 语义 elaborationLIR semantic elaboration消费一个ValidatedUnit为它的运行时含义、契约、证明接口和可选的执行门面executable façade注册 Lean 声明。其中只有第二种操作是所有前端共享的。Lean 仍然负责 elaborate 一份 Leaner 源码文件的语法但源码语法在 LIR 构建完成之后不再定义该函数的语义或验证路径。1.2 当前架构的重复问题原文档给出了当前迁移前Leaner Move 路径的依赖图Leaner source | -- Lean elaboration -- Lean definitions / Move.Action façade | | | -- retained raw Lean Syntax | | | -- Move.Verify.Source | -- sourceSpec / contract / proof | -- Lean environment / LCNF -- Move.Compiler.LIR (NSIR) -- MoveModel.IR -- interpreter / bytecode | -- transitional Leaner-to-LIR importer具体表现为四个各自独立推导语义的组件move/Move/Verify/Syntax.lean保存一份私有的原始Declaration内含原始Syntax重新解析源码、重建签名、分析借用作用域、生成关系型规约move/Move/Compiler/LIR.lean独立地从 elaborated Lean 声明中恢复可执行结构move/Move/Compiler/Elab.lean把降级后的MoveModel.IR反引quote回 Lean当时的 LIR 路径虽能打印规范化的 Leaner 源码却不能为该 LIR 提供 elaboration、执行或证明语义。这种重复正是要移除的问题它允许编译器与验证器各说各话disagree、让导入的 MIR 成为特例并导致源码语法 Lean 环境侧表在 validated LIR body 已经存在之后仍然长期充当语义输入。1.3 2026-08-27 的关键重构Reframing原文档特别标注了一次重要的设计再定位2026-08-27move、move-model、transpiler三个包被整体弃用为仅作参考reference-only没有任何现存代码再链接它们Move 交换前端现在位于LeanerMove.Frontend。这意味着不再存在活的直接 elaboration 路径需要被影子化M3、迁移M6或增量退役M7旧路径被冻结为oracle参照标准其语料库通过拷贝测试来挖掘而不是通过切换默认实现主线剩余交付物是 M2 尾部语料库可执行覆盖 应还的无理论确定性、至燃料完备性、保持性/无卡死与 M4–M5契约、计算出的 WP、借用/状态/循环/模块化验证目标是 LeanerLang 表面与端到端语料库。同时验证管线单次运行的 validate、权威的 resolve 与 unification 类型检查、在 validate 阶段一次性运行的分析、ValidatedUnit上携带证书也已在同一天落地validate 现在拥有类型检查与初始化/借用分析preparation 只做能力过滤capability filtering。验证半部M4–M5 的验证部分自 2026-09-01 起由 historical/certifying-execution.md 承接无 frame 的 row 路线本文档保持对运行时模型、big-step 语义、解释器与正确性义务的权威地位。二、目标架构一条由 ValidatedUnit 出发的单一语义管线原文档给出的目标架构如下Leaner source -------- Move source ------------ RawUnit -- LeanerIR.Validation.validate -- ValidatedUnit Rust MIR ------------- | | --------------------------------------------------- | | | v v v LIR interpreter LIR big-step LIR contracts (computable) semantics and WP | | | ---------- soundness -------------------- verify f | ----------------------------------- | | v v executable backend Lean declaration UI (Move IR/bytecode) and source backend架构的最终端点是Validated LIR 是 Leaner 执行、验证、可执行降级executable lowering与生成的 Lean 声明的唯一语义输入。两个硬性约束值得强调能力显式检查从ValidatedUnit出去的每一条箭头都可以通过显式的能力检查capability check拒绝某个特性但它们不得回看源码 AST也不得静默地把一个不支持的节点重新解释为别的含义。来源只影响诊断函数Origin只影响诊断与对齐不影响语义。来源信息provenance必须穿透每条离开 LIR 的路径——验证错误、解释器错误、语言 throw、验证义务、后端诊断都必须指向来源LocId并借此指向作者编写的源码区间。一个 pass 可以细化或追加相关位置related locations但不能把可用的作者位置替换成只含生成位置的信息。2.1 包归属语义核心与前端客户分离新架构把语义核心集中到leaner-ir/LeanerIR它拥有Move/Rust 已知语义并集known semantic union的运行时值与状态模型结构化表达式、place、调用、控制与 throw 语义可执行解释器权威的关系型 big-step 语义契约、语义最弱前置条件、计算出的 WP 规则及其正确性定理面向 LIR 函数的通用verify证明接口语义能力检查与带源码位置的语义诊断包括运行时终止点与证明义务来源。包依赖约束leaner-ir只依赖 Lean 基础库绝不允许依赖move、move-model或transpiler。这在仓库中可直接验证——lakefile.toml 中该包是独立构建的。模块与命名空间的归属镜像了整条管线模块职责LeanerIR.Import原始前端信封与检查过的 CFG 结构化structurizationLeanerIR.Validation诊断、已验证信封、结构检查、语义能力准备LeanerIR.Semantics运行时域与 big-step 关系LeanerIR.Interpreter可执行求值LeanerIR.Proofs正确性与未来验证定理测试模块位于LeanerIR.Tests之下按它们所覆盖的边界命名不存在笼统的LeanerIR.Tests源模块仓库中实际可见 LeanerIR/Tests 下按Abilities、Closures、Control、Data、Finalization、Generics等主题划分的测试文件。其余包全部降级为客户move拥有 Leaner 表面语法、Leaner→LIR 前端、兼容命令与 Move 可执行降级leaner-move提供 Move 策略并校验残余的仅前端属性元数据如 LeanerMove/Frontendmove-model成为更低层的可执行/prover IR不再定义 LIR 的含义transpiler只拥有交换适配器与源码打印不拥有语义。profile语义画像库只为实现真正的扩展节点与策略如事务中止回滚、panic 清理提供实现。已知的 Move 与 Rust 构造属于核心并集Move profile 不再接受任何残余的类型或操作标签其剩余的属性标签只是等待结构声明的仅前端元数据——词汇表检查通过本身并不构成可执行语义。三、语义准备边界Semantic Preparation BoundaryValidatedUnit目前保证的是结构性质ID 边界、arena 无环、profile 词汇表、结构化控制流。要让解释器或验证器公开可用验证还必须额外确立以下内容已解析的声明与调用目标resolved declaration and call targets表达式、模式、place 与操作的类型检查泛型实参与能力ability满足性局部作用域、初始化、move 与 drop 的合法性调用与返回的元数arity合法的break_/continue_嵌套构造器、析构器与枚举变体一致性选定 profile 所要求的生命周期与借用约束契约与规约表达式的类型检查每个可达扩展节点的语义实现。后端的特性选择与语义准备分离。原文档给出的两个私有构造器包装wrapper使意外的不完整执行在类型层面不可能发生prepareExecution : SemanticsRegistry - ValidatedUnit - Except (Array Diagnostic) ExecutableUnit prepareVerification : SemanticsRegistry - ValidatedUnit - Except (Array Diagnostic) VerifiableUnit这两个包装器包含索引与已检查的 handler它们不复制、不翻译函数体。仓库中的实际实现位于 LeanerIR/Validation/Capability.leanprepareExecution/prepareVerification第 4566 / 4579 行附近。长期规划是把公共检查移入LeanerIR.Validation.validate让 preparation 只检查消费者的能力。3.1 结构化控制的类型检查structured control preparation 会跟踪循环结果类型break_与continue_必须选中一个外层循环break 值必须与该循环的结果类型匹配可能落穿fall through且无结果的块必须具有 Unit 类型无else的if表达式与模式赋值必须具有 Unit 类型可落穿的循环体同样必须具有 Unit 类型非落穿表达式在 abrupt control 下保持多态polymorphic可落穿的函数体必须具有其声明的 packed 结果类型。这些检查直接消除了 prepared unit 中的解释器卡死或保持性preservation失败。3.2 初始化分析与能力检查可执行准备还对结构化 body 执行路径敏感的确定性初始化分析path-sensitive definite-initialization参数初始化前导局部变量模式绑定与直接局部写入初始化直接局部 move 与 drop 消费分支汇合只保留所有落穿路径共有的初始化循环回边迭代到有限不动点未初始化读取在其作者的LocId处被拒绝之后解释器收到的ExecutableUnit才不会再遇到未初始化局部。声明的ValueHasType判定对运行时整数使用同样的可表示范围谓词——越界的定宽值不能仅仅因为类型表项是整数就被当作保持性证人。泛型与能力方面核心Copy、Drop、Store、Key约束在具体泛型实参上检查Move 能力结构化传播名义类型使用其声明Rust 拥有隐式Drop、标量/共享引用的Copy、显式名义/函数Copy。缺少必需能力时place/value 拷贝与显式 drop 被拒绝。结构验证还要求canonical 命名空间路径唯一、每个顶层声明的 interned 限定名属于其所在命名空间、名义声明必须严格是 struct 或 enum 形态、拒绝重复字段与变体、拒绝每个 resolver 查询族内的重复项而不是让解析取第一个歧义目标。完整的结构类型图含逻辑类型/资源域实参在语义准备之前完成边界检查与无环检查。四、运行时模型4.1 值Values初始解释器使用一阶RuntimeValue加上独立的类型判定而不是用 arenaTypeId索引的依赖值——后者在 schema 仍在演进时会无谓地增加执行与解码的难度。运行时值联合需要一等情形unit、布尔、整数、字符串与字节元组与向量含定长向量校验名义结构体与枚举变体带捕获值的闭包指向运行时位置的引用由语义 handler 拥有其表示的已检查扩展值。ValueHasType unit namespace value typeId表述运行时良类型性后续的 preservation 证明语义检查过的函数求值不可能产生其声明结果类型之外的值。仓库中的类型化层见 LeanerIR/Semantics/Typing.lean。4.2 状态与 placeState and Places运行时状态包含带已初始化/未初始化局部的调用栈全局/资源存储死亡帧导出的未决 loan 写回集pending write-back set任意 profile 自有的事务状态。关键设计没有堆、没有引用目标。在先知式所有权模型prophetic ownership model见 prophetic-references.md下借用borrow是一个拥有所借内容的值的值可变 loan 在原处留下一个洞hole解析出的 place 是根 投影路径其中 dereference 步投影进 borrow 的当前值。该模型是 RustHorn 编码Matsushita/Tsukada/Kobayashi也是 V0 栈在完整 Move 验证中成功用过的模型——它覆盖嵌套引用、reborrow 与返回引用的函数并让别名在验证之后结构上不可表示exclusivity 是结构性的验证器中任何地方都不需要分离逻辑或逐点不相交推理。Keyed global storage 使用核心GlobalKind操作contains、borrow、take、publish可变全局 borrow 在全局槽中留下洞take/publish只通过认证的互斥性certified exclusivity与洞交互。Move 的existsAt/borrowGlobal/moveFrom/moveTo直接映射到这些节点而不是 profile 操作标签。生命周期不是运行时值而是被借用分析消费的已检查证据其证书许可先知模型。解释器与 big-step 关系运行同一套确定性规则loan 死亡标记写回 borrow死亡帧通过 pending 集导出因此不存在需要关联的独立 prophecy 判定——prophecy 只是 pending 导出的契约层读法。4.3 Throwabort 与 panic 必须区分Move abort 与 Rust panic 必须是不同的ThrowKind。求值首先产生一个带参数列表的 thrown outcome然后由 profile 特定的调用边界决定状态可见性Move abort 暴露事务前的全局状态Rust panic 按所选 panic 策略保留突变或运行清理解释器燃料耗尽与畸形状态是工具错误tool errors永远不是语言 throw。语义 outcome 与来源无关但可执行结果会把它与一个ExecutionOrigin配对——至少记录返回或抛出表达式的LocId运行时错误记录变得卡死或耗尽本地燃料预算的操作位置调用保留调用点位置与被调用者位置作为紧凑栈使 abort/panic 能在其起源处被报告并带相关调用者区间。位置是可观测的元数据改变它们不能改变程序是否返回、抛出或改变状态。五、结构化 big-step 语义权威语义是对结构化 body的归纳关系而不是翻译成 CFG 或MoveModel.IR。原文档给出了核心定义inductive Control where | value (values : Array RuntimeValue) | break_ (nest : Nat) (value : Option RuntimeValue) | continue_ (nest : Nat) | return_ (values : Array RuntimeValue) | throw_ (kind : ThrowKind) (arguments : Array RuntimeValue) EvalExpr : SemanticContext - FrameState - ExprId - FrameState - Control - Prop该Control归纳类型在仓库中的实际定义位于 LeanerIR/Semantics/Runtime.lean第 478 行附近。签名可能继续演化但以下性质是硬性要求块传播非局部控制且不继续求值其后缀loop消费匹配的深度为零的 break/continue并在传播时递减外层嵌套深度调用按 LIR 定义的顺序求值参数、进入新帧、把被调用者的返回转换为调用者的值throw_保留所有参数值模式要么原子绑定要么不匹配place 赋值在改写目标之前先求值其右端闭包打包按声明顺序捕获值invoke调用捕获的函数值规约块specification blocks无运行时效应缺失的 body 只能通过已注册的外部摘要summary或实现来执行。非终止用不存在有限 big-step 派生来表示——语义中不含燃料也没有outOfFueloutcome。函数含义是这个关系的小包装structure FunctionMeaning where relates : Invocation - RuntimeState - RuntimeState - Outcome - Prop仓库实现见 LeanerIR/Semantics/BigStep.lean 第 836 行附近。它按profile 与函数身份选择绝不由 body 来自 Leaner、Move、MIR 还是生成源码决定。5.1 开规则与闭语义2026-09-03 更新规则在被调用者 oracle之上陈述EvalExprWith unit callee以及EvalValuesWith、EvalStatementsWith、EvalArmsWith用callee : CalleeRelation回答每一次直接调用与闭包调用闭语义EvalFunction unit是打结tie the knot的嵌套归纳——它的唯一规则在EvalFunction unit自身之下求值 body。EvalExpr unit及其余闭关系是那个 oracle 上的实例因此每个消费者都保持原有拼写。这个结的无理论位于 LeanerIR/Proofs/Oracle.lean开规则在 oracle 上是单调的EvalExprWith.mono且EvalFunction.induction断言闭语义低于每一个对函数边界的一次展开封闭的 oracle——这正是递归函数原生指称native denotation所依据的最小不动点归纳详见 historical/certifying-execution.md 的Recursion一节。该文件的模块注释明确写道Both are proved by mirroring every constructor, which is what a change to the rules must keep in step.二者都通过镜像每个构造子证明规则的任何改动都必须与之保持同步。六、解释器解释器镜像 big-step 规则但在循环、递归与调用上显式带燃料fuelledinterpret : ExecutableUnit - Fuel - FunctionRef - RuntimeState - Array RuntimeValue - Except LocatedInterpError (RuntimeState × LocatedOutcome)LocatedInterpError包含一个InterpError、一个主LocId与相关调用位置InterpError至少区分不支持的外部实现、卡死/畸形运行时输入、outOfFuel。LocatedOutcome包含语义Outcome加上它的ExecutionOrigin。因此语言的throw_是一个成功的、带源码位置的解释器结果。实现约束初始实现可以拷贝MoveModel.IR.Interp中有用的有限存储与证明模式但必须直接执行结构化 LIR。如果把 LIR 执行定义为降级到MoveModel.IR就会让该降级因定义而正确、丢失为 Lean 与 Rust 想要的结构化语义并且使该降级无法被独立测试。要求的无理论按实现顺序有限运行时存储的 lookup/update 引理操作级解释器正确性表达式与控制流解释器正确性函数/调用解释器正确性可执行 profile 下 big-step 语义的确定性至燃料完备性每个有限派生都能用足够燃料重现类型保持性与 prepared invocation 的no-stuck 定理。基础定理是interpret executable fuel f state args ok (state, outcome) - f.semantics.Relates state args state outcomeoutOfFuel不做任何语义声明也永远不会被转换为 abort 或 panic。仓库中run_sound每次成功的解释器调用都有 big-step 派生实现在 LeanerIR/Proofs/Interpreter.lean第 2001 行附近run_complete有限确定性执行在足够燃料下可重现在 LeanerIR/Proofs/Completeness.lean第 1121 行附近两者在 LeanerIR/Proofs/Meaning.lean 中组合出functionSpec读取 big-step 判定的关系含义。七、契约与验证7.1 一个含义两种有用的表示验证瞄准的是FunctionMeaning而不是解释器实现。最简单的语义 WP 最初从 big-step 关系定义SemanticWP f normalPost throwPost initialState : every outcome related by f.semantics satisfies the matching postcondition然后计算出的wpExpr通过对 LIR 的结构递归实现使证明不必对派生树做量化它的正确性定理把它与SemanticWP连接起来。这个次序防止 tactic 变成正确性的定义。仓库中的wpExpr实现在 LeanerIR/Proofs/WP.lean第 31 行附近另有一个按命名空间/unit 展开的wpExpr第 1936 行附近与wpExprStep步进 tactic。原文档 2026-08-27 的附注明确了一条已被取代的旧安排运行时与证明两种引用表示现在完全相同——validated LIR 采用基于 prophecy 的所有权模型解释器运行 ghost-erased 规则因此旧的concrete→relational 精化义务被该设计的 agreement 定理取代见 prophetic-references.md。7.2 规约表达式与契约契约已经以FunctionContract、Condition、Frame与表达式根的形式存在于 LIR 中验证器直接解释这些节点requires约束初始逻辑环境ensures观察结果、最终引用与最终状态异常子句匹配ThrowKind与全部 throw 参数old选择初始状态锚点frame 子句约束未被提及的状态循环不变式附着在结构化的循环点上而不是重建的源码循环上。逻辑量词与未解释的规约函数即使不可执行也拥有关系指称因此验证准备可以接受比执行准备更大的子集但必须诊断任何没有逻辑指称的构造。7.3 生成的证明接口对每个可执行声明fLIR 语义 elaboration 暴露等价于以下内容的接口f.lirDecl -- stable handle into the validated unit f.semantics -- FunctionMeaning f.spec -- denotation of the LIR FunctionContract f.contract -- Contract.Satisfies f.semantics f.spec f.verified -- theorem produced by verify f迁移期间f.sourceSpec可以作为f.semantics的兼容别名保留但绝不能通过遍历保留的源码来生成。调用使用绑定到 LIR 函数身份的已证明或受信任摘要因此只要 profile 兼容调用者与被调用者可以来自不同前端。verify f变成一个小型命令 elaborator解析f.lirDecl、构造标准Contract.Satisfies定理并调用 LIR 证明自动化不检索原始源码语法。原文档 M4 的状态记录2026-08-29还补充了实现细节生成的契约读取完整的 Move abort 纪律aborts_if … with code钉住失败 outcomeaborts_if_is_partial/aborts_if_is_strict选择参考栈的abortComponents读法命名常量与spec.bitVectorToInt在子句中翻译每个生成的义务通过Obligation标记携带作者子句的字节区间残余目标由leaner_report在该子句处报为错误。首个从参考栈拷贝的验证测试LeanerLang/Tests/VerificationAborts.lean源自AbortDirections从 LIR 证明相同的公共契约且在#guard_msgs下故意写错的 body 会在预期的ensures区间失败。prepared unit 每个命名空间只 quote 一次ns.semantics带内核检查的等式因此命名空间内每次 verify 共享一次准备。7.4 M5 的全局状态验证2026-08-29 修订全局状态通过类型化的 spec 级状态验证取代了无类型访问器读法与早期状态类型假设。每个 struct 声明前端生成一个类型化孪生certifiedSpecInt整数、普通 Lean 标量、嵌套孪生及erase/decode?对与证明过的往返LeanerLang/SpecTypes.lean契约的requires对每个可存储族量化一个类型化映射StorageKey → Option Twin通过FamilyRepresentation绑定到运行时内存——映射律在 keyedGlobalMap上证明跨族不相交是 key 不等式的定理而非假设。可变全局借用的写回由状态的 loan 注册表RuntimeState.globalLoans键控——认证互斥性使记录的 key 就是洞的位置因此不需要搜索全局内存signer 通过其地址在RuntimeValue.storageKey?中键控存储。已知边界穿过可变全局借用的字段投影mut Coin[addr].value会降级为对 borrow 值的 dataselect而核心求值器不定义它——该模式从来不可执行与验证无关。在降级层发出局部变量所用的基于 place 的模式或核心定义聚焦引用投影之前支持的表面形式是整资源借用。八、Lean 声明 elaboration 与诊断映射LIR 语义 elaboration 应把每个 validated unit只 quote/注册一次。生成的声明引用一个 unit 常量与稳定的声明 ID而不是把每个表达式节点展开成新的 Lean 语法树——避免同一个 arena 为执行、验证与编译各重复一次。elaborator 有两类输出语义声明如f.semantics、f.spec与稳定的 LIR handle——每个受支持函数都必须有人体工学门面façades如类型化的 Lean 函数或Move.Action包装——只有当函数的 profile 与类型能被该表面 API 表示时才生成。名义 LIR 声明同样生成 Lean structure/enum 及在类型化门面与RuntimeValue之间跨越所需的类型具体化reification证据。泛型 body 保持对 type/const/lifetime/trait-ability 证据的泛型语义 elaborator 不得仅为产出 Lean 声明而单态化它们。为控制 elaboration 规模一个ValidatedUnit只 quote 一次之后用声明索引计算 WP 项时保留 arena 共享让常用语义组合子成为普通定义与引理为每个消费者生成小包装而不是一个完全展开的项在能实质性减少重复遍历时对逐表达式验证结果做 memoize把源码/来源表排除在定义相等性与证明项之外。诊断与源码映射每个生成的声明与义务都在持久环境扩展中记录其来源NamespaceId、声明 ID 与LocId。语义准备的错误直接用 LIR 位置elaborate 生成的 Lean 声明时抛出的错误通过反向映射翻译后再呈现。生成子项继承最具体的 LIR 节点位置诊断可以为调用点、被调用者声明、宏来源或导入的 MIR 位置追加相关源码区间。canonical Leaner 打印器是这个映射的另一个消费者——生成的文本不是权威错误位置。位置传播在每一条语义边界都是强制的验证报告非法表达式/place/声明/条件/frame 的位置而非仅命名空间解释器在抛出表达式处报告throw_、在操作表达式处报告卡死操作调用者位置作为相关区间计算的 WP 节点与生成的 Lean 目标保留创建它们的 LIR 代码或契约子句的LocId畸形规约指向其Condition/Frame/规约表达式位置未证明的验证目标在相关代码或规约位置展示即使生成的定理带合成 Lean 语法可执行与源码降级维护显式的目标节点→LIR 位置映射以便后续后端错误能翻译回 LIR。九、迁移计划 M0–M7每个里程碑都应可独立评审并在其 gate 达成前保持两条路径都能工作。下表汇总了原文档的完整里程碑设计里程碑主题状态按原文档记录M0语义能力清单与门控核心节点与 MoveProfileValue标签的 inventorySemanticsRegistry/ExecutableUnit/VerifiableUnit边界CI 清单检查已实现M1值、状态、big-step 核心与解释器常量/局部/块/let/模式/赋值/ifElse/match_/return/throw/直接调用结构化loop/break_/continue_位置传播操作与解释器正确性已实现M2数据、操作、引用与闭包名义构造/析构、字段更新/选择、枚举变体测试、向量、checked 算术/移位/转换、定宽位运算、闭包、具体引用、keyed globals、throw 终结化preservation 与 no-stuck 证明进行中见下M3为 Leaner 源码影子化语义 elaboration已重构2026-08-27直接路径已弃用影子差分安排不再是目标差分执行角色移交 MonoVM harnessM4契约与计算 WP解释 LIR 规约函数/条件/frame/不变式计算 WP 的证明生成f.spec/f.contractverify f切到 LIR 查找Gate 已达成2026-08-29M5借用、状态、循环与模块化验证进展中2026-08-29 第二修订类型化 spec 级状态落地读取、move_from、整资源mut更新自动验证M6语料库迁移与默认路径切换已重构无默认路径切换旧语料库是待拷贝的 oracleM7退役直接路径已重构整包弃用为冻结参考9.1 M2 当前细节M2 已经落地的部分原文档 Implementation status运行时值现在包含向量、名义值、闭包与引用具体堆/全局引用共享嵌套 place 机制类型化核心纯操作、闭包调用、返回引用、keyed 全局存储与 profile 选择的 throw 终结化在解释器与 big-step 语义中都执行。Move 前端现在发出核心全局与原语操作而非 profile 标签。定宽算术区分模运算与携带溢出ThrowKind的显式checked*操作Move 用abort发出 checked 算术。语义准备检查闭原语词汇表的操作数与结果类型元组形状、向量元素/定长义务、带源码位置的整数/布尔/比较/索引/切片错误。Raw validation 在任何语义消费者观察到类型表之前就拒绝零宽整数与负数或非整数的定长向量长度。break_/continue_循环控制检查、常量声明检查、关联项默认值检查、构造器模式与调用共享同一名义声明/变体解析。可执行准备还执行路径敏感的确定性初始化分析见 §3.2。剩余工作不支持的 primitive/引用子集、trait/predicate 满足性、非名义的整单元类型良构性、剩余声明族以及 preservation/no-stuck 证明。9.2 M0/M1 的仓库落地证据M0 的中性包拥有穷举式核心语义清单、版本化 profile 语义注册表、私有构造器ExecutableUnit/VerifiableUnit准备门、可达节点能力检查、首个可执行字面量类型检查、稳定带位置诊断以及 M1 的一阶运行时值、帧与保留存储、纯叶操作、无燃料结构化 big-step 关系、面向完整 M1 控制子集的带源码感知燃料解释器均有对应源码。run_soundProofs/Interpreter.lean证明每次成功的解释器调用都有 big-step 派生fixtures 覆盖值、元组与区间模式、赋值、分支、结构化循环、常量、直接调用、正常返回、多参数 throw、卡死诊断、调用栈与作者字节区间见 LeanerIR/Tests 下的Control.lean、Data.lean、Closures.lean、Finalization.lean等。十、测试迁移策略测试采用增量拷贝而非整体搬迁旧测试在功能波收敛前保持 oracle 地位。每个拷贝的用例在适用处记录四个观测返回值、throw kind 与参数、可见最终状态、生成的契约结果。throw 与失败用例还断言其主区间与相关源码区间。燃料是测试 harness 参数永远不是期望语言行为的一部分。建议的八个功能波①字面量/整数算术/元组/块/条件/普通返回②循环与结构化控制退出③结构体/枚举/向量/泛型/直接调用/闭包④不可变与可变局部引用、嵌套 place、返回引用⑤全局资源、回滚、帧、跨模块调用⑥基础契约与 abort 方向⑦借用/循环/递归/不变式/模块化摘要证明⑧负面表面/类型/借用/降级/验证诊断。三种互补测试形式语义单元测试构造小型 raw LIR fixtures验证后运行解释器前端集成测试把 Leaner 源码 elaborate 到 LIR 并运行该 validated 工件差分测试对公共子集把 LIR 执行与现有MoveModel.IR解释器或事务性 VM 比较。big-step 测试不应只是重算解释器成功的解释器求值用正确性定理产生语义事实精选示例还直接构造或反转关系型派生。负面测试在执行前断言诊断码与源码区间。聚合测试根按关注点拆分例如LeanerIR/Tests/Validation.lean LeanerIR/Tests/Interpreter.lean LeanerIR/Tests/Semantics/* LeanerIR/Tests/Verification/* LeanerIR/Tests/Elaboration/*跨包前端一致性测试与 VM 差分测试放在专门的leaner-e2e-tests包中仓库中见 leaner-e2e-tests/LeanerE2ETests/Check含Language/、Negative/、Verification/三组以及MonoDifferential/差分目录以免给leaner-ir或语义 profile 包引入前端依赖。十一、正确性义务与保持性分解迁移只有在以下主张全部显式化时才完成解释器结果被 LIR big-step 语义接纳run_sound已实现有限确定性 LIR 执行在足够燃料下被重现evalFunction_complete/run_complete基于燃料单调性已实现EvalFunction与FunctionMeaning的 big-step 确定性因解释器是函数而随之成立语义准备 良类型输入蕴含保持性与 no-stuck 执行解释器 outcome、错误与生成的证明义务保留其来源 LIR 位置计算的 WP 蕴含语义 WPf.verified证明Contract.Satisfies f.semantics f.spec具体引用执行精化先知验证模型Move abort 终结化精确回滚所需状态每个可执行降级保持 LIR outcome每个前端的对齐证据证明其源码工件与 LIR 语义的关系canonical 源码重新 elaboration 保持规范化 LIR 语义。前六项由leaner-ir拥有。11.1 Preservation 与 no-stuck 的五阶段分解剩余 M2 无理论以 M1 的ValueHasType为结构层分五阶段推进存储类型化Store typingStateTyping为每个堆槽赋予可选TypeId全局槽已携带资源TypeId。类型化值判定在引用处强化ValueHasType目标槽的赋根类型经引用投影后就是引用类型的 referent。名义字段与闭包捕获类型化需要拥有ExecutableUnit在相应引理落地时加入判定。帧与状态判定TypedFrame把声明的局部表关联到运行时帧——已初始化局部按其声明类型类型化未初始化局部为noneTypedState要求每个存活堆/全局槽按其赋型类型化。叶引理验证的字面量/类型检查器firstSliceConstMatchesType与具体化器constValue?与ValueHasType一致initialFrame?从类型化实参产出类型化帧。两个函数必须全函数total这些引理才存在因此嵌套ConstValue递归是结构的而非partial。操作引理每个语义操作求值器保持类型化且——对 no-stuck——定义在语义准备接纳的操作数形状上validation 中每条LIR-SEMANTIC-TYPE规则命名其操作引理可假设的形状。求值器归纳Preservation 让增长的StateTyping穿过互递归求值器no-stuck 额外消费ValidatedUnit携带的初始化证书并得出结论prepared 的、类型化的调用要么返回结果要么outOfFuel——绝不返回卡死诊断。原文档状态记录2026-08-27阶段 1–4 已在 LeanerIR/Semantics/Typing.lean 中对纯 primitive 词汇表证明——WfPrimitive.eval_typed覆盖标量、布尔、字符转换与溢出组位运算在整数结果节点下需要操作数标量前提逐操作引理覆盖聚合组与 copy/move 转发。延后项pointer-width 整数节点.integer .pointer须在ValueHasType能陈述该节点之前对目标解析、深名义字段与闭包捕获类型化、阶段 5 归纳本身。Profile 终结化定律针对那里声明的接口证明降级与前端对齐定理由各自适配器拥有再与 LIR 验证组合。仅构造一个ValidatedUnit并不证明源码或 MIR 对齐。十二、兼容性政策与已定决策兼容性政策要点在可行处保留用户可见的源码名与spec f/verify f的形状内部生成名与定理陈述可为诚实陈述 LIR 结果而改变兼容别名仅在从旧 API 指向新 LIR 拥有的声明时允许新 LIR 语义绝不能回调旧源码翻译器临时差分模式可同时运行两条路径并报告分歧但任一结果都不得静默取代另一个不支持的构造在验证或语义准备期间以位置 稳定诊断码失败一旦函数 opt-in 进入 LIR 路径回退到源码 elaboration 就被禁止否则会掩盖覆盖缺口。原文档已定决策Settled decisions清单完整如下Validated 结构化 LIR而非保留源码语法或更低层 CFG IR是语义的真相来源解释器直接执行结构化 LIR燃料只是终止装置关系型 big-step 语义是权威的且不含燃料验证基于 big-step 函数含义陈述自动化用证明过正确的计算 WP具体运行时引用与先知证明引用可以不同但需要精化定理LIR 语义声明独立于前端来源源码位置贯穿执行、验证与降级它们是诊断元数据永不改变语义 outcome泛型 LIR body 对证据保持泛型而非为 elaboration 单态化生成的 Lean 声明是在一个注册 unit 上的小型索引门面而非 LIR body 的重复展开现有 elaboration 与证明代码可拷入leaner-ir后做结构适配保持旧实现 DRY 不是目标直接源码语义路径只在语料库覆盖与比较 gate 使 LIR 路径成为默认之后删除。十三、开放实现选择以下选择应在 M0 期间敲定且不改变架构可执行全局与堆存储使用的具体有限映射表示为纯函数与有效函数生成的确切类型化门面语义准备包装是独立类型还是ValidatedUnit索引内的私有能力记录已注册语义 handler 的稳定身份与版本化方案计算的 WP 有多少被急切物化、多少按需 memoizef.sourceSpec在成为f.semantics之前的临时兼容名。结语这条管线在仓库中的位置这份设计文档不是纸上谈兵——它的 M0/M1 已实现、M2 进行中、M4 gate 已达成源码全部位于 third_party/move/lean/leaner-ir 下可独立构建的leaner-ir包配套设计可继续阅读 lir-design.mdLIR 本身的定义与边界不变式、prophetic-references.md先知引用语义的完整里程碑登记其 P1–P7 已实现并取代本文 M5 的引用条款与 historical/certifying-execution.md验证半部的 frame-free 路线。端到端验证覆盖可参见 leaner-e2e-tests 下的Increment.lean、Loops.lean、GlobalBorrows.lean、Calls.lean等测试。理解这条管线就理解了 Leaner 如何让 Move 与 Rust 的验证共用一个语义、一个验证器、一个真相来源。【免费下载链接】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），仅供参考
