从脚本驱动到归一化验证Aptos Move 的 Leaner 验证器generic route设计演进实录【免费下载链接】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本文基于仓库内 generic-route.md 设计文档撰写。它记录的是 Aptos Move 形式化验证栈中 Leaner 验证器的验证路线verification route演进史从按函数形状手写策略脚本frame/row route到归一化而非逐步推导的 generic route再到被原生native计算与执行协议agreement取代最终由 V5单一指称 单一协议证明设计接棒。阅读本文你将理解为什么按形状匹配脚本注定无法规模化、verify f normalize ; close这条归一化路线的原理与实测成本、原生迁移的 25 个检查点及其 19/61 的真实迁移进度以及这些设计在 Leaner 验证器源码 中的落点。背景为什么需要一条通用路线Leaner 是 Aptos Move 仓库third_party/move/lean下的一个 Lean 4 验证器栈用于对Move/Rust 前端经过 lower 产生的LIR 程序做源语义验证source-semantic verification。在设计 generic route 之前验证走的是所谓frame-free row route它把运行期帧表示移除换来 20–50 倍的性能收益但代价是验证本身被实现成针对函数体形状生成的策略脚本。文档给出的关键数字说明这条路不可持续generic-route.md 中的Why一节记录LeanerLang/RowScript.lean曾包含 22 个形状识别器recognizer和 20 个脚本发射器约 6.8k 行配合约 200 条手写 row 定律其中很多是每个槽位布局一条四个mutate_evaluate_rowFrame_*、七个exportFrameLoans_rowFrame_*甚至把四槽 row 逐槽写出的括号定律每个脚本只覆盖它被写出来服务的那个函数及其近邻——计划plan不可组合因此每移植一个 v0 文件就要新写一个计划而语料库是无界的对比之下v0 验证了 176 个目标99 个自动只用了 1.2k 行 WP 演算和 0.5k 行策略Leaner 栈当时已有 26k 行验证代码却只覆盖 50 个目标。除了形状匹配而非组合这一条回归还有第二条更深层的回归逐步推导stepping而非归约reduction。Leaner 的指称是关系式的ExprDenotation是关于帧、状态和控制流的Prop。验证它意味着让策略一步步推导——每个节点应用一条定律、把求值器的等式当作假设、用injection/subst反演、归约match、拆分、继续——这本质上是产出证明的符号执行每一步都要花钱每一步都依赖目标的语法还要依赖leaner_row_drive、leaner_row_head、反演链和脚本约定的假设命名。而 v0 没有这些它的wp (program) post是一个会归一化normalize的项组合性来自bind。V1 选择关系式指称是为了让与大步语义big-step relation的一致性agreement精确而直接——这对agreement是对的对verification却是错的。generic route 因此提出的核心主张是保留关系式指称用于 agreement另加一个计算式computational指称用于验证。核心原理verify f normalize ; close文档给出了整条路线的总纲verify f normalize ; close其含义展开为四条设计函数体除了关系式指称外还指称为一个计算computation一个作用在符号状态row、registries、runtime state上、返回控制流的Spec。Spec及其wp在Proofs/Spec.lean、Proofs/Contract.lean以及lir_wp_normsimp 集中已经存在类型化契约层已经在讲wp。每个组合子恰好一条wpiff 定律标记为[lir_wp_norm]把wp (C …) post改写成各部分的wp每个叶子操作有一条求值定律把闭合求值器在字面 row 上归约成值或带侧条件的 throw。验证就是simp only [lir_wp_norm, leaner_eval]后接leaner_certified_close!——没有驱动、没有计划、没有反演、没有命名约定。计算与关系之间的一致性每个组合子一条定律由生成器按 V1 组合关系式一致性同样的方式组合起来从verified到functionSpec的链条经由Spec.Equiv的 transport保持精确不变。因此生成器为每个函数发射三类东西关系式指称不变、计算式指称、计算与关系的一致性证明外加一个策略leaner_normalize。归一化范式无法完成的主体会在某个程序点留下残差residue由 closer 在它无法建立的子句处报告——可见性与原来一致只是粒度细到组合子一级。计算式指称RowSpec与组合子计算式指称的定义文档原样给出/-- The symbolic state a body runs over. -/ structure RowState where row : Row registries : Registries state : RuntimeState /-- A body as a computation: a control, or a throw. -/ abbrev RowSpec : Spec RowState Failure Control组合子镜像ExprDenotationpureValue v、readLocal i、operation ev operands在操作数值上求值闭合求值器throw 即abort、branch c t e、letIn i init body、assign i v、loop site body作为Spec.withInvariant即契约层循环定律已经在用的不动点、throw_ k args、return_ vs、call handle callee args、globalBorrow key path、endLoan loans。操作数行与语句行都是bind。没有任何东西携带RuntimeFramerow 是字面列表、state 是结构更新的记录——这正是 row route 表示廉价的原因设计予以保留。每个组合子的wp定律是与 v0 相同形式的 iff例如[lir_wp_norm] theorem wp_operation … wp (operation ev operands) post s ↔ wp operands (fun values s match evaluate ev values s with | .value v s post (.value v) s | .throw k a s post (.throw_ k a) s | none False) s求值定律leaner_eval既有的*_evaluate定律、readLocal?_rowFrame、set!归一化、家族表示事实把evaluate ev values s在字面数据上归约使match可归约。受检运算留下范围条件全局读留下 closer 通过Representation.lean解析的家族查找。若某运算的求值器今天定义在RuntimeFrame上row 形式就是rowFrame row registries处的求值器定律从帧定律证明一次。控制流是结果中的一个 sum因此wp_bind对语句行只分发一次非值控制直接传播、不求值后缀——这就是块规则。调用、存储与引用都是bind这条路线把三类最难的结构统一表达为bind序列调用call handle callee args是把参数行 bind 进被调方在参数值处的Specwp_call消费被调方的Satisfies事实wpFunction_of_satisfies使延续运行在ensures、frame、aborts子句作为假设之上。契约是数据Contract.runtime对typed再对 raw contract 的展开由 simp 归约为存在与合取命名方式与调用方前置条件的命名同一遍完成leaner_native_cases、leaner_name_facts。递归调用是同一条定律只是事实取自归纳假设——除此以外递归没有任何特殊之处。mut写回是状态中的预言对prophecy pair被调方摘要说pending push (loan, newValue)endLoan把它解析回借用槽位处的 row一条参数化为槽位的定律resolveReturnedBorrows取代了把槽位固定在 0 的 reborrow 调用定律。存储括号即globalBorrow 主体 endLoan。借用的求值定律产生借用值、在.global key登记 loan、在家族中标记孔hole、递增nextLoan参数化为 key 与 pathtake/publish/contains 各一条定律全局endLoan把借用的当前值写回家族。字段聚焦是 loan 位置中的路径与孔中的focusValue——与运行时表示一致。返回引用是 row 中的值加上摘要的 export 子句调用方的call登记返回的 loan被调方退出时导出它exportFrameLoans_rowFrame_holeFree其侧条件由 simp 在字面 row 上决定。试点withdraw的归一化验证在推广之前路线先在一个最难的标量存储目标withdrawperf_storage的Account移植上验证并对照脚本基准。withdraw的形状正是手写脚本定律最多的形状wpRowThrow_focusedFieldBracket及其变体也是最初 51× 发现的载体帧路线 379.9M heartbeats脚本路线 17.3M、48k 证明对象。试点搭建了withdraw恰好需要的组合子、它们的wp定律、求值定律、与关系式组合子的一致性、生成器对主体计算的发射以及leaner_normalize然后在禁用脚本的情况下运行verify withdraw。deposit、replace、balance_of共享其组合子免费一并测量。结果表2026-09-03 首次切版 vs 默认路线targetrouteheartbeatsobjectswallwithdrawscript17.3M48,197withdrawnormal form (first cut, 2026-09-03)44.7M55,556~1.1 s vs 0.55 swithdrawnormal form (default route)39.7M60,0181.28 sdepositscript13.1M28,918depositnormal form31.5M45,6821.02 sreplacescript8.5M24,912replacenormal form17.1M24,1960.55 sbalance_ofscript11.9M16,523balance_ofnormal form11.7M12,3520.35 s归一化后的残差正是 v0 的形状abort 蕴含、正常路径以被写资源的 keyed insert 作为终态、以及算术上不可能的溢出分支。无逐形状定律、无驱动。未优化的成本拆分heartbeats暴露出四个发现按处理顺序stepcostnoteprologueleaner_cases、表示、资源存在3.3M与脚本共享切换到计算、入口事实2.1M归一化第一遍wp定律、读3.2M归一化第二遍求值器、写回、导出16.0M其中 11.4M 花在四次 ground 求值器运行closing、abort 分支6.5M仅 closerclosing、正常路径2.7M1.1M 为 fits 证书与表示事实closing、溢出分支0.5Mexfalso; omegakernel check~6.5M55k 对象的项Ground 求值是成本中心——每次求值器运行都是带着整个环境规则集的内层simp修复方向是专用求值集或反射性证明目标是把四次运行压到 3M 以下不可达分支必须在归一化中剪枝——closer 比omega贵 25 倍closer 需要被写资源作为孪生twin——表示事实以目标focusValue拼写陈述、由孪生的insert_over_hole证明清空上下文无济于事——closer 的成本在目标而非假设。结论路线在最难的标量存储目标上正确首个切版成本是脚本的 2.6× heartbeats、约 2× 墙钟时间落在设计允许的试点范围内一般化建设继续进行。构建状态与模块落点2026-09-03 的构建状态中路线已进入代码库leaner.route默认值为normalizeverify对受支持的非递归、非泛型树使用它其余类别自动保留脚本路线。核心模块多数至今仍在 leaner-ir/LeanerIR/Proofs 下Tree.lean函数体作为字面树Tree/Operands/Statementsdenote关系式组合子、computeRowSpec组合子、supported以及通过互归纳一次证明的一致性agreement与全性totalitywp_nativeFunction_tree是单次改写切换。生成器LeanerLang/Denotation.lean单遍emitWith在函数体旁发射f.denotationTree与denotationTree_denotesrfl任何函数都不携带协议证明。Normalize.leanlir_eval集wp_evaluate、wp_ite_prop按原语键控的受检加减乘除模定律[lir_wp_norm high]必须压过通用wp_evaluate每求值器头一个 ground-evaluation simproc在字面 row 上展开求值器自身的定义闭包unfoldClosure抽象GlobalMap与globalLoanKeyIn?保持折叠evalInitialLocals构造入口 rowevalBind处理结构模式reduceBEq/reduceBne判定闭合的派生BEq比较decideLoanEquality用omega判定 loan id 上的Nat等式否定结果缓存良基遍历器collectPruned_*、findFirst_*、rewriteFirst_*的构造子等式leaner_normalize [facts]还读取上下文中每个关于initial的事实。外层 simp不再把omega当作兜底消解器。Decode.leanevaluateDecoding——孪生的decode?或编解码器在字面量上求值范围证书从上下文证明返回孪生与证明。Represent.leanleaner_expose_resources [tree]在树的每次 keyed 读处把类型化内容拆为 absent/presentrequires 侧的存在事实关闭 absent 情形leaner_certify!解构孪生leaner_split_bools枚举布尔字段、leaner_represent_writes目标中每个字面名义量的insert/insert-over-hole/erase获得其FamilyRepresentation事实以目标拼写陈述、leaner_decode_results实例化∃ result, decode literal some result ∧ …、leaner_close_normalized。Certify.lean共享 closer等式行前的decodeLiteralTwinsleaner_resolve_rows中的字面名义行resolveReturnedBorrows_singleBorrow、两种拼写的填充定律算术叶子接受其自身改写能闭合的目标; omega。verifyLeanerLang/Contract.lean对受支持的非递归非泛型树一个定理形状——prologue、编解码展开含孪生编解码、leaner_expose_resources [tree] ; (…)、切换、leaner_normalize、契约前缀、leaner_close_normalized、leaner_report。CI 覆盖leaner-e2e-tests/…/Check/Verification/Normalized.lean即该路线下的存储检查Normalized.lean 至今保留着set_option leaner.route native其leaner module 0x42::storage_normalized内是balance_of/is_published/deposit等带spec的存储函数。覆盖验证lake env lean -D leaner.routenormalize跑遍所有正向Check/Verification文件均通过Account、Callees、Calls、Corpus、Generics脚本回退、Increment、Loops脚本回退、Normalized、Prophecies、References、Rust、Storage、TypedAborts负向用例非零退出并逐字复现预期诊断。后续完成的工作宽泛的subst_vars闭合被只替换已判定的布尔变量取代ground 求值器不再继承完整lir_wp_norm清单外层归一化 simp 的兜底omega被移除exportFrameLoans有了泛型结构单借用等式simproc 只计算frameBorrows、局部孔谓词和全局查找。于是路线数字回到试点量级withdraw39.7M、deposit31.5M、replace17.1M、is_published9.9M、balance_of11.7M、reborrow9.7M heartbeats。已判定的布尔参数在归一化前替换使choose_reborrow回到 50M heartbeats 上限内。踩坑记录给后来者的陷阱清单文档专门留了一节Trap其中几条至今仍适用于LeanerIR命名空间下的开发在namespace LeanerIR…内写Lean.Expr/Lean.Name会被LeanerIR.Expr遮蔽目标中的值可能被mdata包裹匹配前先consumeMDatarootNamespace是_root_永远不要写env.contains (rootNamespace n)在(a; b)块内产生目标的策略需要all_goals或;收尾用And.intro拆分帧子句会把LoanDiscipline展开到 closer 语法之外——让 closer 处理合取closer 以RuntimeValue.storageKey键控帧假设用rfl改写globalKey永远不要展开storageKeyset_option … in不能写进leaner module块出现在同一 shell 命令里的pkill -f模式会杀死 shell 本身。性能语义objects 上涨说明目标承载了更多某个状态或 row 不再被消费——范式中的表示问题heartbeats 上涨而 objects 持平说明在搜索simp 集过宽——键控问题。两者都要先在范式中修复再扩展覆盖都不是保留脚本的理由。正确性门与性能门正确性门每个今天能验证的目标——15 个基准目标与leaner-e2e-tests/LeanerE2ETests/Check/下每个检查——在禁用脚本的情况下由归一化验证两个预期负向用例保留其诊断不得出现新的.exp。从此程序形状永远不是加代码的理由只有缺失的定律才是。性能门Perf.measure在Performance.lean中按生成定理报告 heartbeats 与证明对象驱动扩展为把每个verify的类型化定理 heartbeats/objects 写入检查旁的.perf文件用UB1重新生成、10% 容差比较使整个语料库都被门槛覆盖而非十五个精挑目标。迁移期间生成器由leaner.route : script | normalize选择路线驱动在两条路线下各跑一遍。回归不是阻塞项而是里程碑要报告并解释的数字真正拦门的只有Performance.exp及其容差。里程碑规划StepCorrectness gatePerf gateP0测量逐检查.perf记录、leaner.route、附录基线表套件不变基线记录P1试点withdraw归一化——组合子、wp/求值定律、协议、发射、leaner_normalize禁用脚本下withdraw/deposit/replace/balance_of试点表决策P2第二试点调用对、wp_call、契约即数据、槽位参数化endLoanbump_twice、take_and_bump、bump表G1标量子集全量其余组合子、循环即withInvariantIncrement、Corpus、Loops、Rust、Aborts表G2调用全量、递归、返回引用Calls、Callees、References、Prophecies、Typed、Generics表G3存储全量take/publish/contains、整体与聚焦括号Storage、Account表G4删除RowScript.lean、drive 与逐布局定律verify只发射leaner_normalize全语料、脚本消失最终表Performance.exp经评审移动一次每个里程碑只有门槛满足、表格进入附录才落地。G4 之后账本移植恢复且此后移植失败只会命名缺失的定律永远不会是缺失的计划。非目标与开放问题非目标在具体化语法树上做反射式检查器组合子即语法、范式即作用于目标的 simp 集改动大步语义、关系式指称及其与语义的协议、或 closer互递归与泛型递归函数。开放问题计算式指称应由生成器逐函数发射还是定义为关系式组合子的函数denoteRow : ExprDenotation → RowSpec不可定义——关系不是程序带调用的循环中withInvariant如何量化逐迭代变化的 registries两个预期负向用例的残差如何报告。转向原生路线为什么不再优化退休路线2026-09-05 起文档记录了一次优先级修正停止优化退休中的 frame/row-script VC 路线。RuntimeFrame仍属于执行与语义协议但不得再出现在取代该路线的计算或原生契约证明中旧的typedDenotation适配器不合格——它仍会解码一次运行时执行。Proofs/Computation.lean引入精确的Represents边界连接普通原生Spec与对编码参数的执行保留正常/失败/未定义三种关系成功运行时结果必须是规范编码对任意编解码器仅解码不够transport 只用编解码器的左逆。Proofs/ComputationAgreement.lean承载只属于运行时的协议定律读、任意局部槽位的 move、操作数排序、纯调用、函数进入/导出。可选的leaner.route native消费computation/computationVerified/computationRepresents工件缺工件时 row 回退禁用并拒绝复用其他路线已证明的定理。当前仓库源码与文档一致 Options.lean 中leaner.route的默认值已是native其描述明确写着native only; legacy script/normalize/compose routes are disabledVerify.lean 的verifyFunction直接拒绝route ! native并拒绝任何证明脚本然后经compileFunction编译、requireNativeArtifacts审计原生工件。原生迁移的 25 个检查点与 19/61 进度文档用大量篇幅记录了从显式工件试点到自动原生主体生成的渐进迁移。要点如下显式工件试点2026-09-05LeanerLang.Tests.NativeComputation中泛型carry与具体carry_u64具备原生计算与模块化原生证明、独立的精确协议与公开源语义 transport依赖审计拒绝原生证明中的执行帧依赖与原生主体中的运行时值编码。carry1.44M/2,168、carry_u643.40M/4,530原始天花板 1.96M/2,568、4.94M/8,126。自动转发LeanerLang/Computation.lean为单参数值转发生成原生主体、可复用原生摘要与精确执行证书carry/carry_u64改为leaner.route native。carry_u64全阶段比原基线少 40% heartbeats、48% 证明对象。受检算术NativeArithmetic生成受检加减乘返回带范围证书的SpecInt或精确失败载荷perf_calls::guarded从 7.62M/8,793 降到 3.40M/4,771-54% heartbeats、-45% 对象。此后逐检查点扩展abort 调用组合NativeCalls消费nativeSummary不展开被调方主体→ 类型化局部绑定NativeSequence2/4/8 个受检操作 3.79M→17.30M heartbeats倍增门控→ 调用初始化局部NativeLocalCalls→ 嵌套操作数NativeOperands两个/四个嵌套加法 4.53M/8.04M→ 整数端口Language/Integers12 个 verify 31 个解释器断言全过→ 枚举引用含可变模式载荷经可变引用表示的真实缺陷修复→ 变体感知操作FocusStep携带可选变体标签→ 返回引用组合Verification/References12 项全过→ 字面向量与有界向量v0 的 2^64长度证书进入原生向量表示→ 类型化循环Verification/LoopInvariants与Language/Loops不动点证明不因迭代次数展开→ 受检控制表达式Language/ControlForms→ 泛型语言Language/Generics同一泛型体按调用方实例化、不重新验证。随后是从第 14 到第 25 步的逐特性落地每步均为 worktree、回退禁用共享引用读NativeReferences、受检向量索引NativeIndex、直线局部赋值NativeAssignmentsswap 从超 50M 降到 3.24M、条件赋值分支合并NativeConditionalAssignments、Unit 结果/显式 abortNativeStatements、原生循环内核NativeLoop.run类型化状态/退出不动点、源循环接入该不动点NativeLoops、词法体局部NativeLoopLocals、嵌套/带标签循环控制NativeNestedLoopsControlRoute只在执行协议中编码控制、语句位置提前返回NativeEarlyReturns、原生变更前置NativeVectorMutation、NativeMutation、所有权输出边界NativeBoundary.finishNativeMutableBoundary试点对set_seven(mut u64)的显式工件全套通过以及自动标量 owner 变更NativeMutableGeneratedContract.buildNativeOwnerContract独立翻译带old的后置条件。迁移进度与门槛原生专用切割普查 17/61 个 Check 文件通过、44 个失败其中 42 个是原生实现/证明缺口2 个仅诊断差异最新的标量 owner 变更步2026-09-08把原生专用审计推进到19/61——Verification/Loops与Language/Integers完全通过39 个原生缺口文件与 3 个纯诊断失配。同一批六个 IR 测试目标失败Move71 jobs与 Rust165 jobs套件通过。文档明确警告更早的混合路线通过审计是历史记录不是原生专用套件变绿的证据。20M/30,000 聚合 heartbeats/对象门与每精确执行断言 1M 上限未抬高任何既有基线。移除退出标准与最终归宿文档列出五条尚未全部满足的移除标准每个受支持的验收验证目标必须选择native并通过#leaner_require_native含协议与 VC 依赖审计完成回退已禁用的其余消费者删除RowScript与归一化/组合源 VC 生成器并退役其证明定律模块保留执行语义与精确的 native-to-execution 协议定律其中的运行时帧不是回退 VC 表示类型化原生存储/效应迁移必须替换兼容状态与契约适配器在不抬高预算或刷新基线掩盖回归的前提下通过既有功能/负向/验收/性能门。#leaner_require_native与#leaner_require_native_all命令在 Verify.lean 中定义前者拒绝遗留类型化包装并审计计算/VC 依赖后者对整文件强制原生审计路由回归在缓存复用前拒绝退休路线并在逐函数审计与整文件审计中同时拒绝畸形缓存定理。而这条路线的终点在文档头部已写明generic-route 与原生路线都已被 denotation.mdV5对已验证 LIR 的单一指称 单一协议证明取代。V5 保留本文件为试点测量、检查点与原生切割普查而存在不再更新。这一演进序列——形状脚本 → 归一化 → 原生计算协议 → 单一指称单一协议——正是 Leaner 验证器在可组合、无逐形状定律、性能可测量三个维度上不断收敛的过程其每个阶段的成本数字与验收门槛都完整保存在 generic-route.md 与配套的 test-organization.md、test-organization-history.md 中是理解 Aptos Move 形式化验证栈当前设计V5不可跳过的一手史料。【免费下载链接】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），仅供参考