尧图网站建设 
Verification v2在原生数据之上构建浅层指称验证——Aptos Leaner 验证栈的设计、测量与落地【免费下载链接】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本文基于 third_party/move/lean/designs/historical/verification-v2.md 展开讲述 Aptos 仓库内 Lean 形式化验证栈Leaner中一次关键的验证架构演进保留深度语义big-step 关系与燃料解释器作为唯一权威同时为验证引入一层由定理证明连接、而非假设连接的浅层指称shallow denotation把验证自动化从逐条目的符号执行重担中解放出来。读完本文你将理解该设计的动机、两条正交轴控制流指称与原生数据表示、泛型参数的分类处理、以 bareverify为门槛的自动化测量方法以及 V1–V7 里程碑的完整落地过程与遗留开放项。背景深度嵌入税与 v0 之间的自动化差距Leaner 栈的验证最初采用**符号执行symbolic execution**方式在 quoted unit 之上运行一个解释器函数体是 arena 中的数据要得到 proof obligation就必须在 tactic 内部反复做 arena 查找、名字解析与求值器应用。文档将这一成本称为deep embedding tax深度嵌入税——它按 obligation 支付永远无法摊销。截至 2026-08-29 的实测后果是明显的差距leaner 栈仅验证了5 个存储合约读、move_from、一次整资源可变更新每个都要数秒的 tactic 工作为了达到这一结果消耗了几乎整个会话去诊断归约行为——whnf 不深入投影、良基定义对归约不透明、递归深度异常直接中止 tactic 扫描、simp无法重写 matcher 判别式等。被冻结的 v0 栈v0/move在 330 个verify条目中225 个函数可完全自动验证——即裸写verify f、不带任何证明体。其全局存储套件全部自动Account.lean2/2、GlobalBorrows.lean6/6、GlobalInv.lean5/5、GenericStorage.lean7/7含泛型资源。手工证明只集中在真正需要数学推导的地方OrderedMap.lean、Quicksort.lean、ReturnedMutRefs.lean。v0 的这些测试仍然保留在树中——被弃用的包只是从 CI 中移除并未删除。v0/move/Move/Tests/Verification 是本文档提案的验收语料acceptance corpus。文档强调这个差距不是逐个 fixture 修补 tactic就能弥合的上述每个陷阱都是嵌入方式embedding的产物而非 Move 语义本身的问题。v0 并没有更好的 tactic它的成功是因为目标本身不需要那些 tactic。为什么 v0 能做到浅层以及为此付出了什么代价v0 中浅层形式本身就是语义一个 Move 函数直接被 elaboration 成Specmonad 上的 Lean 函数因此不存在第二个模型需要与之达成一致也不需要 agreement 定理。这正是其自动化优势的全部来源。v0 的关系单子实现位于 v0/move/Move/Semantics/Spec.lean其Spec结构包含三条关系ok正常结果、aborts中止条件只提及初始状态因为交易效果会回滚、undefined默认恒为False用于把需要证明的数据不变量变成正向义务而非空真义务。但这种浅层换来了两个缺陷而 Leaner 栈存在的目的正是修复它们没有元理论no metatheory。任何量化所有程序的陈述——把验证当作信任边界、no-stuck、preservation、determinism——在浅层编码里都没有安身之处因为每个程序都是不同的 Lean 项。通向执行存在未证间隙。v0 自己的树中见 CLAUDE.md 的 Keep these claims separate写明了verify f证明的是关于生成源码语义的定理编译器将其降级为字节码而连接二者的编译器正确性定理是未来工作。此外 v0 的 store 是公理化的——ResourceStoretypeclass 的四条定律只是字段没有任何实例且每个有序资源类型对都附带一个IndependentResourceStores假设。因此最天真的路线直接让浅层形式成为语义会通过重新引入这两个缺陷来恢复自动化——而这恰恰发生在为消除它们而构建的栈上。更糟的是它在信任上还不如 v0v0 的浅层项是人工撰写、可读为程序的而我们的浅层项是从数据中由一个大型元程序派生出来的没人会去审查它。文档给出了精确的批评定位成本不在浅层本身而在把浅层当作权威shallowness as the authority。v2 同样把合约表述在原生形式上——但通过denote_agrees每个这样的定理都是关于 big-step 关系的定理而该关系解释器是可证明地实现的。在 v0 中verify f的定理只关于浅层项本身浅层 elaboration 中的错误在系统内部是无法证伪的。两个栈共同遗留的间隙——深度语义到生产字节码——不变且在下文明确列为非目标。提案保留深度语义添加一条由证明连接的浅层指称核心方案是保留深度语义作为参考保留解释器作为可执行形式新增一个验证所面向的浅层指称shallow denotation它通过证明而非假设与参考语义相连。命名上使用denotation指称语义意义上的从数据到意义而不是reification后者惯例上方向相反。Axis 1——控制函数体的指称一个 Lean 函数denote把 validated unit 和函数句柄映射为规范 monad 中的一个 Lean 函数denote : ValidatedUnit → FunctionHandle → Array RuntimeValue → Spec RuntimeState Failure (Array RuntimeValue)它由组合子combinators构建顺序、条件、带不变量的循环、检查算术、keyed 存储操作、作用域化的可变借用以及每个注册 intrinsic 一个由 profile 拥有的组合子、携带其注册语义。这里的Spec是关系式的与 v0 相同它赋予意义并不执行——执行仍属于解释器。连接关系只证明一次通过对 LIR 的归纳、在关系本身的层面上theorem denote_agrees : ∀ args, denote unit f args ≃ functionSpec unit f args其中≃是 normal、abort、obligation 三条关系的分量等价。它必须是双向的aborts_if子句陈述的是精确的中止条件单向细化无法承载它们。此后每个合约的Satisfies双条件式就是推论写在denote unit f之上的合约成为关于 big-step 语义的陈述而最弱前置条件规则按组合子逐个触发而非逐个从 arena 挖掘 LIR 节点——这正是 v0 的wp_norm但不再携带 v0 的间隙。对denote本身有两条设计约束定义透明性definitional transparency每函数成本模型依赖denote unit f通过 kernel defeq 归约到其组合子项。这排除了denote定义中任何位置的良基递归well-founded bodies 对 whnf 和 defeq 不透明本树已多次实测denote必须对 validated body 结构递归其余都通过展开是定义性的显式不动点组合子路由。互递归mutual recursion调用图同一强连通分量SCC内的调用不能展开为被调方的指称。SCC 通过作用于该分量函数族的互不动点组合子来指称v0 的fixFamily见 Spec.lean是参考形状。跨 SCC 调用则直接展开为被调方的指称模块化验证落地后也可展开为其合约。Axis 2——数据原生表示Move 的struct变成 Lean 结构体其字段携带经过认证的表示——整数为范围认证子类型嵌套结构为其自身的孪生twin——而不是RuntimeValue。这条轴在 2026-08-29 已经建成LeanerLang/SpecTypes.lean、LeanerIR/Proofs/Representation.lean孪生类型按 struct 从 validated unit 生成带一对erase/decode?并证明 roundtrip全局存储是按资源族划分的类型化映射通过FamilyRepresentation与运行时内存绑定。它的 store 定律在 keyed map 上证明跨族不相交性是键不相等key disequality的定理——这两点都优于 v0v0 是直接假设的。组合类型化包装器两条轴汇合在类型化的每函数包装器中deposit : Address → SpecInt 64 false → Spec TypedState Failure Unit它通过孪生的erase/decode?roundtrip应用于实参与结果与denote unit f关联——与FamilyRepresentation同思路只是高了一级从存储到函数边界。这一步是每函数的但很便宜因为 codec、roundtrip 与类型化 store 都已存在。文档特别强调两条轴缺一不可任何一条都不能取代另一条。没有 Axis 2浅层指称只在控制流上浅、值仍是未类型化的——它解决了 arena 归约问题却没解决RuntimeValue反演问题没有 Axis 1类型化值仍要靠符号执行挖出来——这正是现状也是五个合约消耗一个会话的原因。泛型类型参数parametric 与 storage-key-dependent 的分野权威 LIR 保持泛型RawUnit和ValidatedUnit保留一份带 type/const/lifetime/evidence binder 的 body。任何实例化形状的工作只发生在派生证明面向的指称时且特化指称永远是泛型 body 加 agreement 证明的一个视图绝不是克隆出第二个语义权威的 body。这引用了 Dill et al., TACAS 2022 中的特化边界。第一迭代已做storage-parametric 参数。Move 类型参数出现在实参、结果、局部、聚合载荷、操作或泛型调用中时保持 parametric只有当它参与全局存储键的资源族分量contains、borrow、take、publish包括经直接调用传递依赖时才需要特化。这不是phantomnesscarryT(value : T) : T全程使用T却仍是 parametric。storage-parametric 参数被视为给定的抽象、有居类型inhabited type生成的定理量化于该载体因此可传递到每个具体实例——这也是为什么在没有此类定理时用便利的具体类型代入会不健全。Preparation 遇到 storage-key 相关使用时会给出显式诊断拒绝而不是静默地为所有实例共用一个符号资源族。推迟V4storage-key-dependent 参数。此类实例化得到按资源键相关类型实参元组键控的特化指称。Rust trait 实现证据日后会再加一个语义特化轴trait 选择默认是实例相关的即使不涉及全局资源键。Preparation 从入口计算可达实例图、在调用下闭包、一起证明有限族它特化可达元组而非笛卡尔积。实例闭包不有限多态递归、开放入口的配置必须保留 parametric 定理或显式有限覆盖证书——绝不能从恰好看到的实例静默推广。合并证据组合是更晚的优化且只由经过检查的语义等价授权。单一语义仍然成立prophetic-references.md 已裁定解释器、big-step 关系与验证器运行在同一个模型上。本提案不添加第二个模型指称是带证明连接的派生视图正如类型化 store 是全局内存的派生视图。改变的是哪条视图承担自动化。解释器含 MonoVM 差分链路与 big-step 关系分别保持执行与参考语义的角色。迁移期间的共存与 V7 退休直到 V72026-09-02两条路线并存指称尚未承载的结构仍走旧的符号执行路线。退休之后只存在 native 路线指称不承载的结构变成 negative check其期望文本指名该结构详见 certifying-execution.md 的 Retirement performed。成本模型三条获得连接的路由文档给出三种获得连接的方式按成本落点划分RouteOne-timePer function / instance classFragilityStatus quo (symbolic execution)—perobligationtactic searchhigh, unpredictable — 10-minute hangs observedEmitted proof termscertifying generatorlinear proof checklow; no searchVerified denotationinduction proofonerfllowest第三条是终点每函数或 V4 下每实例类的成本塌缩为单次 kernel defeq 检查——本树在 quoted prepared unit 上为semantics_eq已经成功使用的模式——且任何 tactic 都不再做任何搜索。该检查之所以可用完全依赖上文的denote定义透明性约束放弃它第三行就会悄悄退化成第一行。一次性成本是归纳证明文档诚实定价数周而非数天。第一行现状不摊销每个合约、每个循环不变量、每个算术边条件都要重付。V2 测量十个函数、裸verify的自动化基准2026-08-31 完成的 V2 里程碑是这份提案的证伪实验从 v0 验收语料移植十个函数合约不改写每个都以裸verify尝试。这些 fixture 现在退休于 Check/Verification/Corpus.lean原VerificationV2.leanT3 时并入。文档记录的测量如下v0 sourceFunctionBareverifyCallees.leanbumpautomatic(~3s)Callees.leanbump_twiceautomatic(~30s)Callees.leantake_and_bumpautomatic(~15s)Callees.leanset_pairautomaticCallees.leanforward_set_pairautomaticGlobalBorrows.leanreplaceautomaticGlobalBorrows.leanread_wholeautomaticGlobalInv.leanremoveautomatic函数合约模块不变量尚无 leaner 表面Account.leandepositautomaticwith V6s field-focused borrows见下Account.leanwithdrawautomaticwith V6s field-focused borrows and the branch the denotation subset gained with them十对十全部满足门槛阈值八个。首次测量时只有八个达标Account的两个函数随 V6 的 field-focused borrows 与分支支持加入。验证时间是每函数秒级但仍高于 v0亚秒残余成本是调用边界写回对账call-boundary write-back reconciliation且是可测量的、非结构性的见 V3 注释。仓库中 Corpus.lean 的源码与测量表一一对应三个模块分别移植Callees.leanbump、bump_twice、take_and_bump、set_pair、forward_set_pair、GlobalBorrows.lean/GlobalInv.leanreplace、read_whole、remove、Account.leandeposit、withdraw每个函数都带完整的spec块ensures/aborts_if/modifies/requires与裸verify命令。例如deposit验证的是mut Balance[addr].balance.value字段级全局借用加经引用的检查加法而withdraw额外覆盖带守卫中止if current amount then abort(1)的分支形状。文件头部注释明确说明该文件测量的是 native denotation 交付的自动化而非提供 fixture 专属证明脚本。空虚性发现vacuity findingselect链的健全性教训V6 的调查把一个健全性危险提纯为值得记录的结果LeanerLang 前端曾把mut X[a].f.g降级为值级引用类型select链——这种形状没有运行时意义evaluateDataOperation?拒绝引用操作数只有 exchange 路径的borrow(select(local))树会被 validation 归一化为 place。由于Satisfies是部分正确性——其undefined关系对 M1 子集为空——卡在这种形状上的函数会空真地vacuously满足任何合约一个故意写假的ensures竟然验证通过了。两条结论被记录下来裸verify成功只有在 LIR 每个节点都具有可执行语义时才有意义preparation 必须拒绝无意义形状而不是无条件地把data.select视为可执行——后者正是它现在的做法。实现交接V1–V3 的落地与一值一拼写V1–V3 已完整落地实现分布如下V1 组合子语义与 agreement 库在 LeanerIR/Proofs/Denotation.leancertifying lowering 在 LeanerLang/Denotation.lean直接 WP 驱动器在 LeanerIR/Proofs/DenotationWP.lean。静态参数、局部、全局、字段、构造器、调用与借用位置都由 lowering 选定动态贷款路由使用 native frame/state 索引与封闭的初始 frame/写回方程而不是在 VC 内部靠查找重新发现位置。V3 的 codec 与类型化合约传输实现在 LeanerIR/Proofs/Typed.lean每函数的 nativeArguments/结果类型、codec 与类型化指称由 LeanerLang/Typed.lean 生成。SpecInt、生成的标称孪生、可变实参与抽象泛型载体跨过这一边界而不会在撰写的类型化定理中暴露RuntimeValue公开运行时定理通过 codec roundtrip 与指称 agreement 从类型化定理搬运。全参数化泛型函数量化于一个抽象载体与一个认证 codec。storage-key 相关特化仍是 V4 工作没有实现有限实例化闭包或 trait-evidence monomorphization。V3 稳定化2026-08-31反复应用了一条教训每个值必须恰好有一种拼写every value must have exactly one spelling。收敛与正确性失败全部归结为同一项的两个拼写并存——裸 kernel 投影与命名字段访问、set!与setIfInBounds、Array.mk与字面量、push 形式贷款注册表与其归一化字面量、未展开解码器与其 roundtrip——这会静默击败形状键控重写与omega的句法原子同一性。修复手段归约折叠把卡住的 kernel 投影折回命名形式reconcile 集在形状引理运行前规范化数组拼写封闭 frame 引理陈述于规范字面量拼写量化注册表中的 profile 查找被密封、其方程成为路由事实未路由即达上下文的类型化存储读经FamilyRepresentation重写marker 剥离规范化只在全有或全无的 closing 尝试内运行因此失败子句仍在其撰写的 range 上报。这些测试中没有任何手工 fixture 证明——门槛就是裸verify。里程碑 V1–V7状态全景文档的里程碑表完整记录截至 2026-09-01 状态StatusMilestoneWhat remains before it is doneDONEV1组合子指称、certifying lowering、agreement 生成、native 位置、storage/generic 门控以及最初的裸verifyfixture 门控均在 V3 工作前实现并通过DONEV2十个 v0 corpus 函数以裸verify全部验证通过对比记录如上DONEV3重复嵌套可变调用验证收敛bump_twice与完整五函数VerificationV2fixture验证套件全绿包括此前红色的VerificationAborts与VerificationStorageNOT STARTEDV4Storage-key-dependent 实例化闭包与 monomorphized viewsNOT STARTEDV5取代所生成 agreement 证明的泛型归纳证明IN PROGRESSV6Projected borrows、.return_/.throw_、动态/多重/投影/全局返回引用带分析撰写的死亡、不变量驱动结构化循环全部 native 化并有防回退门控带值 break 与模式赋值仍待办IN PROGRESSRust support三个 Rust-profile 函数经共享 native 路线验证通过引用字段解码仍开放trait/evidence 指称推迟DONE (2026-09-02)V7退休frame 路线移除每个未覆盖目标都是 negative check见 certifying-execution.mdV6 明细引用、分支、循环的 native 化V6 是超越整资源与循环的引用里程碑文档逐一记录了已完成项全部为 DONE其后列明剩余Canonical loweringmut X[a].f.g降级为运行时 place 机制执行的那一形状——整资源全局借用绑定到合成 holder 局部pushTemporaryLocalbody 临时量索引越过所有声明局部并由函数驱动器追加焦点是通过 holder 的deref/field…投影的 place 借用。可变情形不再发出值级引用类型 select 链共享情形保留它们——这是健全的因为 preparation 会把共享引用擦除为其所指。Exit reconciliation无记录死亡的贷款在函数出口对账。exportFrameLoans在导出前结算帧内空洞settleFrameLoans每轮把一个 resting current 移入其帧内空洞使穿过外层贷款逃逸的 holder 携带焦点化突变。此前逃逸 holder 会把陈旧的空洞导出到全局内存。Focused mutation certificateupdateBorrowValue?_focusedBorrowPair为 holder/focus 帧形状闭合 mutate 步骤并注册到驱动器。Focused export certificateexportFrameLoans_focusedGlobalNominal为已结算的 holder/focus 形状闭合 finalization*_focusedBorrowPairSaved与*_focusedGlobalNominalSaved是body 在突变前把读保存到局部的变体。量词与存在义务的闭合两个生成脚本缺口随焦点形状暴露并已为每个函数修复——frame 子句对未修改的键全称量化而 closing 此前无法打开量词故从未触及 keyed-map 定律义务叶子读取位于合约实参行的存在量词之下归一化 pass 在 witness 实例化之前运行无法进入因此 closing 现在在实例化后再归一化一次。raw 脚本也获得了类型化脚本已携带的模块解码器。depositmut Balance[addr].balance.value加经引用的检查加法从裸verify配合requires/ensures/aborts_if/modifies验证通过故意写假的ensures孪生正确失败。Execution gatepreparation 拒绝操作数类型为可变引用的data.select/data.selectVariants求值器读取的是标称值而可变引用是活贷款、其被指物可能持有焦点化空洞。想要字段的前端必须经 place 重新借用。Typing 仍接受该形状因为规范会读它。Loan reconciliation order多个贷款可在同一程序点结束证书按铸造顺序列出。按该顺序对账会在 reborrow 的持有者仍携带其洞时写回使洞逃逸进全局内存、焦点写入落在pending而非资源。endLoans?现在按递减实例序对账reborrow 在它投影的贷款之后铸造故该顺序在持有该值的贷款被写回前结算洞。是执行测试发现此问题证明没有——因为它们都不会在焦点写入后触达move_from。Branches in the shallow denotationnativeBranch运行条件一次让产生的布尔选择分支无 else 时结果为 unitwpExpr_nativeBranch变换条件由其自身的后条件选择分支于是驱动器不再有求值器方程需要重建。语句位置的 branch 现在走浅层路线Verification.raise。Native function controlnativeReturn与nativeThrow求值其 native 值行并抛出相应控制其 WP 与 agreement 定理让返回或中止的分支留在浅层路线。withdraw现在经守卫中止 native 验证不再保留泛型符号执行覆盖。Generated decoders are simp-owned曾展开孪生decode?的符号执行会分裂其触达的每个认证整数的范围测试且假设测试失败的分支之后无法被反驳——孪生内嵌套的SpecInt永远成不了范围假设。解码器在 roundtrip 证明后密封保持折叠直到 closing 针对合约携带的范围事实执行它们。基准无成本。Corpusdeposit与withdraw进入 V2 fixture测量表读作十对十withdraw同时是基准目标焦点借用上的分支成本类别。全部十个 V2 函数携带#leaner_require_native门控泛型验证无法静默满足 fixture。Projected borrows and frame materializationnative reborrow 描述符现在携带任意标称字段步行agreement 使用证明专用的DerefLocalFieldPath可执行描述符只保留局部与已解析字段行。稳定initialLocals加封闭的四/五局部 frame 方程进入 account body 而不暴露依赖数组索引。deposit与withdraw因此端到端使用 native 描述符。Scalar returned reborrow across calls引用类型结果有 native codec被调方 finalization 导出(outerLoan, loanHole returnedLoan)调用方对账从该洞取得转移身份。合约把源参数的可见调用边界值与返回 current 绑定负向回归证明无关的存在退出值不能建立假子句。VerificationReferences.lean 覆盖返回被调方、经第二个函数边界转发引用、经直接返回与转发引用两种突变以及返回贷款死亡后恢复原参数。每个函数都由#leaner_require_native门控。Path-free prophecy and explicit death运行时可变引用保持恰为borrow loan current——没有 owner root 或投影路径。导出值中的loanHole跨调用传递动态身份。借用分析在正常 fallthrough、显式 return 与 throw 处记录LoanDeath值语义 preparation 把它们物化为显式endLoan操作。正常结果携带的贷款被刻意排除在被调方死亡之外以便调用边界转移它们。native WP 有封闭死亡证书而非展开泛型贷款 fold。RuntimeFrame.loanLocations是带语义扫描回退的 validated 局部执行缓存RuntimeState.globalLoans是 keyed 全局写回注册表——两者都不是引用值的一部分。局部返回贷款转移的身份只源自预言洞返回的全局 reborrow 另在globalLoans中把存储键从完成的外层贷款转移到返回贷款。没有引用存储 owner root 或投影路径。Native-only performance gate性能套件测量reborrow、forward_reborrow、set_then_read、set_through_forward含跨两个调用边界的返回引用转移。返回引用方程只对匹配形状派发而非加入每个泛型对账 pass普通重复调用保持在前基线 1% 内。显式生命周期模型刻意重置存储基线replace为 161.7M typed heartbeats一次全局死亡deposit503.0M成对投影死亡withdraw915.6M跨 normal 与 abort 路径——分别为前死亡基线的 35%、38%、24% 增幅。驱动器在封闭 native 死亡证书不匹配时拒绝展开泛型贷款 fold故这些实测成本不可能隐藏符号回退。未来变更以此正确性基线为门控。Returned-reference breadthnative 引用 fixture 现在覆盖两个可变输入加动态选择结果、一对可变结果并经两者突变、投影字段结果及其调用方、从全局存储返回的字段引用及其调用方。连同标量转发共十二个正函数全部#leaner_require_native门控加负向预言测试。转移继续使用预言洞与分析撰写死亡全局所有权元数据在独立注册表中重键而非编码为引用中的路径。Invariant-driven structured loopsnativeLoop是 repeat、continue、break、return、throw 的最小有限归纳关系。其 agreement 定理与 big-step 循环双向WP 定理证明生成不变量初始成立且经一个 native body 步后保持再对有限关系归纳。它不符号展开表达式 id也不携带验证燃料表达式 id 只是选择生成谓词的静态证明标签运行时求值是 elaboratedNativeLoop body关系不做 arena 查找。合约生成把每个撰写的循环不变量翻译为 entry/current frame 与 state 上的 native 谓词记录完整局部行把不可变局部锚定到 entry 槽并在编码局部形状中保留引用贷款身份。VerificationLoops.lean 证明count_to的正常重复与显式continue版本含result limitnative-only 门控。NOT STARTED — 剩余循环形式带值 break 与模式赋值仍在 native 循环子集之外。Rust 支持共享路线的三函数验证Rust-profile 验证与 Move 共用同一 LIR 与 native 证明路线DONE — Native verification fixtureVerificationRust.lean以裸verify证明replace、sum、increment可变引用与标量函数共享普通 native 验证器。DONE — Target pointer width生成的宽度事实比较封闭的支持拼写而非让 kernel 归约String.toNat?Rust unit 无需 profile 专属证明逃生舱即可 elaborate。DONE — Profile-correct arithmeticRustu32加法以模运算合约、无 abort 验证通过同一 Rust 操作对 Move 形状的检查算术 abort 合约正确地不可证。NOT STARTED — Reference-field decoding从引用传入的 struct 读取整数字段仍会搁置解码器范围决策驱动器必须保持认证孪生解码器密封而非分裂Decidable.rec——把嵌套范围作为高优先级 simp fact 加入不能闭合目标还让deposit搜索增加 36%。DEFERRED — Traits and evidencetrait 调用指称、实现证据及其特化轴未启动刻意留在当前 Rust native 验证子集之外。什么被冗余、什么被保留成功后冗余Proofs/WP.lean符号执行机制的大部分——deepWhnf及其 seal 清单、leaner_drive、leaner_storage的 stepping 集成、leaner_flatten。保留燃料解释器及其健全性证明保持可执行形式与 MonoVM 差分测试锚点validation 及其证书不变且借用证书变得更加承重——它为作用域借用恢复授权big-step 关系作为参考语义全部 LIR 元理论2026-08-29 的类型化数据表示全量buildContract其 spec 侧翻译已经浅层、已经类型化。非目标替换 LIR、validation 或前端交换格式。移除 big-step 关系或解释器——删除任一者都会重新引入 v0 的缺陷而那正是不能走天真路线的原因。字节码正确性定理仍超出范围、仍未证明、绝不能被描述为已交付。开放问题Profile 参数化组合子库必须服务 Rust profile 而不只是 Moveintrinsic 组合子是 profile 拥有的部分。哪些组合子属于 core、哪些属于 profile镜像 lir-design.md 中现有的 core/profile 划分。特化等价类V4 从每个语义不同的实参/证据元组一个键的保守起步。哪些元组能按表示相等、实现合约相等或关系参数性定理合并而不使证明搜索更困难V5 是否可达对 LIR 的归纳证明是这里最大单项尚未划定范围。即使 V5 被证明不可行V1–V4 依然有用——所生成证明项是可接受的第二归宿。测试要求每个里程碑门控都是以裸verify f验证的函数数量与 v0 在同函数上的比率对比。自动化率是本提案存在的度量仅 tactic 时间改进不能满足门控。v0/move/Move/Tests/Verification 是验收语料。移植不要重写移植测试需要 v0 不需要的手工证明是要记录的结果而不是要削弱的测试。泛型测试记录哪些参数是 storage-parametric以及从 V4 起计算的资源键 monomorphization 键与生成的 agreement 证明数。基线必须区分一个共享 parametric 证明、storage-key-dependent 组合的精确有限集、未覆盖配置的显式拒绝意外的笛卡尔爆炸即使每个生成的证明都成功也是回归。四套件矩阵leaner-ir、leaner-move、leaner-rust、leaner-e2e-tests全程保持绿色任何里程碑不得以红色落地。历史位置与后续演进本文档于 2026-09-03 移入historical/标记为已执行V1–V3 与 V7 完成而 V6 描述的 native elaborated-Lean 路线已于 2026-09-02 被废弃改用 frame-free row 路线由 certifying-execution.md 设计与跟踪该路线随后又被 denotation.md2026-09-08 决定取代——后者执行 V5 里程碑实现一个指称、一个 agreement 证明LeanerIR/Proofs/Denote/下的compileFunction、compileFunction_agrees与lir_denote归一化关闭器当前verify由 LeanerLang/Verify.lean 实现。遗留的 V4、V5 与被推迟的 Rust shapes 在 certifying-execution.md 的登记簿中继续跟踪。本文档保留的价值在于其设计动机为什么不能把浅层当作权威、V2 测量与空虚性发现它不再更新。跨设计的工作优先级可参考 roadmap.md。无论路线如何更迭这篇设计确立的骨架一直延续至今深度语义是唯一权威验证面向的是带证明连接的派生视图自动化以裸verify的可证明函数数为度量而每个值恰好一种拼写的纪律仍然是 Leaner 验证实现中一切收敛与正确性修复的底层原因。【免费下载链接】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），仅供参考 Verification v2：在原生数据之上构建浅层指称验证——Aptos Leaner 验证栈的设计、测量与落地
Verification v2在原生数据之上构建浅层指称验证——Aptos Leaner 验证栈的设计、测量与落地【免费下载链接】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本文基于 third_party/move/lean/designs/historical/verification-v2.md 展开讲述 Aptos 仓库内 Lean 形式化验证栈Leaner中一次关键的验证架构演进保留深度语义big-step 关系与燃料解释器作为唯一权威同时为验证引入一层由定理证明连接、而非假设连接的浅层指称shallow denotation把验证自动化从逐条目的符号执行重担中解放出来。读完本文你将理解该设计的动机、两条正交轴控制流指称与原生数据表示、泛型参数的分类处理、以 bareverify为门槛的自动化测量方法以及 V1–V7 里程碑的完整落地过程与遗留开放项。背景深度嵌入税与 v0 之间的自动化差距Leaner 栈的验证最初采用**符号执行symbolic execution**方式在 quoted unit 之上运行一个解释器函数体是 arena 中的数据要得到 proof obligation就必须在 tactic 内部反复做 arena 查找、名字解析与求值器应用。文档将这一成本称为deep embedding tax深度嵌入税——它按 obligation 支付永远无法摊销。截至 2026-08-29 的实测后果是明显的差距leaner 栈仅验证了5 个存储合约读、move_from、一次整资源可变更新每个都要数秒的 tactic 工作为了达到这一结果消耗了几乎整个会话去诊断归约行为——whnf 不深入投影、良基定义对归约不透明、递归深度异常直接中止 tactic 扫描、simp无法重写 matcher 判别式等。被冻结的 v0 栈v0/move在 330 个verify条目中225 个函数可完全自动验证——即裸写verify f、不带任何证明体。其全局存储套件全部自动Account.lean2/2、GlobalBorrows.lean6/6、GlobalInv.lean5/5、GenericStorage.lean7/7含泛型资源。手工证明只集中在真正需要数学推导的地方OrderedMap.lean、Quicksort.lean、ReturnedMutRefs.lean。v0 的这些测试仍然保留在树中——被弃用的包只是从 CI 中移除并未删除。v0/move/Move/Tests/Verification 是本文档提案的验收语料acceptance corpus。文档强调这个差距不是逐个 fixture 修补 tactic就能弥合的上述每个陷阱都是嵌入方式embedding的产物而非 Move 语义本身的问题。v0 并没有更好的 tactic它的成功是因为目标本身不需要那些 tactic。为什么 v0 能做到浅层以及为此付出了什么代价v0 中浅层形式本身就是语义一个 Move 函数直接被 elaboration 成Specmonad 上的 Lean 函数因此不存在第二个模型需要与之达成一致也不需要 agreement 定理。这正是其自动化优势的全部来源。v0 的关系单子实现位于 v0/move/Move/Semantics/Spec.lean其Spec结构包含三条关系ok正常结果、aborts中止条件只提及初始状态因为交易效果会回滚、undefined默认恒为False用于把需要证明的数据不变量变成正向义务而非空真义务。但这种浅层换来了两个缺陷而 Leaner 栈存在的目的正是修复它们没有元理论no metatheory。任何量化所有程序的陈述——把验证当作信任边界、no-stuck、preservation、determinism——在浅层编码里都没有安身之处因为每个程序都是不同的 Lean 项。通向执行存在未证间隙。v0 自己的树中见 CLAUDE.md 的 Keep these claims separate写明了verify f证明的是关于生成源码语义的定理编译器将其降级为字节码而连接二者的编译器正确性定理是未来工作。此外 v0 的 store 是公理化的——ResourceStoretypeclass 的四条定律只是字段没有任何实例且每个有序资源类型对都附带一个IndependentResourceStores假设。因此最天真的路线直接让浅层形式成为语义会通过重新引入这两个缺陷来恢复自动化——而这恰恰发生在为消除它们而构建的栈上。更糟的是它在信任上还不如 v0v0 的浅层项是人工撰写、可读为程序的而我们的浅层项是从数据中由一个大型元程序派生出来的没人会去审查它。文档给出了精确的批评定位成本不在浅层本身而在把浅层当作权威shallowness as the authority。v2 同样把合约表述在原生形式上——但通过denote_agrees每个这样的定理都是关于 big-step 关系的定理而该关系解释器是可证明地实现的。在 v0 中verify f的定理只关于浅层项本身浅层 elaboration 中的错误在系统内部是无法证伪的。两个栈共同遗留的间隙——深度语义到生产字节码——不变且在下文明确列为非目标。提案保留深度语义添加一条由证明连接的浅层指称核心方案是保留深度语义作为参考保留解释器作为可执行形式新增一个验证所面向的浅层指称shallow denotation它通过证明而非假设与参考语义相连。命名上使用denotation指称语义意义上的从数据到意义而不是reification后者惯例上方向相反。Axis 1——控制函数体的指称一个 Lean 函数denote把 validated unit 和函数句柄映射为规范 monad 中的一个 Lean 函数denote : ValidatedUnit → FunctionHandle → Array RuntimeValue → Spec RuntimeState Failure (Array RuntimeValue)它由组合子combinators构建顺序、条件、带不变量的循环、检查算术、keyed 存储操作、作用域化的可变借用以及每个注册 intrinsic 一个由 profile 拥有的组合子、携带其注册语义。这里的Spec是关系式的与 v0 相同它赋予意义并不执行——执行仍属于解释器。连接关系只证明一次通过对 LIR 的归纳、在关系本身的层面上theorem denote_agrees : ∀ args, denote unit f args ≃ functionSpec unit f args其中≃是 normal、abort、obligation 三条关系的分量等价。它必须是双向的aborts_if子句陈述的是精确的中止条件单向细化无法承载它们。此后每个合约的Satisfies双条件式就是推论写在denote unit f之上的合约成为关于 big-step 语义的陈述而最弱前置条件规则按组合子逐个触发而非逐个从 arena 挖掘 LIR 节点——这正是 v0 的wp_norm但不再携带 v0 的间隙。对denote本身有两条设计约束定义透明性definitional transparency每函数成本模型依赖denote unit f通过 kernel defeq 归约到其组合子项。这排除了denote定义中任何位置的良基递归well-founded bodies 对 whnf 和 defeq 不透明本树已多次实测denote必须对 validated body 结构递归其余都通过展开是定义性的显式不动点组合子路由。互递归mutual recursion调用图同一强连通分量SCC内的调用不能展开为被调方的指称。SCC 通过作用于该分量函数族的互不动点组合子来指称v0 的fixFamily见 Spec.lean是参考形状。跨 SCC 调用则直接展开为被调方的指称模块化验证落地后也可展开为其合约。Axis 2——数据原生表示Move 的struct变成 Lean 结构体其字段携带经过认证的表示——整数为范围认证子类型嵌套结构为其自身的孪生twin——而不是RuntimeValue。这条轴在 2026-08-29 已经建成LeanerLang/SpecTypes.lean、LeanerIR/Proofs/Representation.lean孪生类型按 struct 从 validated unit 生成带一对erase/decode?并证明 roundtrip全局存储是按资源族划分的类型化映射通过FamilyRepresentation与运行时内存绑定。它的 store 定律在 keyed map 上证明跨族不相交性是键不相等key disequality的定理——这两点都优于 v0v0 是直接假设的。组合类型化包装器两条轴汇合在类型化的每函数包装器中deposit : Address → SpecInt 64 false → Spec TypedState Failure Unit它通过孪生的erase/decode?roundtrip应用于实参与结果与denote unit f关联——与FamilyRepresentation同思路只是高了一级从存储到函数边界。这一步是每函数的但很便宜因为 codec、roundtrip 与类型化 store 都已存在。文档特别强调两条轴缺一不可任何一条都不能取代另一条。没有 Axis 2浅层指称只在控制流上浅、值仍是未类型化的——它解决了 arena 归约问题却没解决RuntimeValue反演问题没有 Axis 1类型化值仍要靠符号执行挖出来——这正是现状也是五个合约消耗一个会话的原因。泛型类型参数parametric 与 storage-key-dependent 的分野权威 LIR 保持泛型RawUnit和ValidatedUnit保留一份带 type/const/lifetime/evidence binder 的 body。任何实例化形状的工作只发生在派生证明面向的指称时且特化指称永远是泛型 body 加 agreement 证明的一个视图绝不是克隆出第二个语义权威的 body。这引用了 Dill et al., TACAS 2022 中的特化边界。第一迭代已做storage-parametric 参数。Move 类型参数出现在实参、结果、局部、聚合载荷、操作或泛型调用中时保持 parametric只有当它参与全局存储键的资源族分量contains、borrow、take、publish包括经直接调用传递依赖时才需要特化。这不是phantomnesscarryT(value : T) : T全程使用T却仍是 parametric。storage-parametric 参数被视为给定的抽象、有居类型inhabited type生成的定理量化于该载体因此可传递到每个具体实例——这也是为什么在没有此类定理时用便利的具体类型代入会不健全。Preparation 遇到 storage-key 相关使用时会给出显式诊断拒绝而不是静默地为所有实例共用一个符号资源族。推迟V4storage-key-dependent 参数。此类实例化得到按资源键相关类型实参元组键控的特化指称。Rust trait 实现证据日后会再加一个语义特化轴trait 选择默认是实例相关的即使不涉及全局资源键。Preparation 从入口计算可达实例图、在调用下闭包、一起证明有限族它特化可达元组而非笛卡尔积。实例闭包不有限多态递归、开放入口的配置必须保留 parametric 定理或显式有限覆盖证书——绝不能从恰好看到的实例静默推广。合并证据组合是更晚的优化且只由经过检查的语义等价授权。单一语义仍然成立prophetic-references.md 已裁定解释器、big-step 关系与验证器运行在同一个模型上。本提案不添加第二个模型指称是带证明连接的派生视图正如类型化 store 是全局内存的派生视图。改变的是哪条视图承担自动化。解释器含 MonoVM 差分链路与 big-step 关系分别保持执行与参考语义的角色。迁移期间的共存与 V7 退休直到 V72026-09-02两条路线并存指称尚未承载的结构仍走旧的符号执行路线。退休之后只存在 native 路线指称不承载的结构变成 negative check其期望文本指名该结构详见 certifying-execution.md 的 Retirement performed。成本模型三条获得连接的路由文档给出三种获得连接的方式按成本落点划分RouteOne-timePer function / instance classFragilityStatus quo (symbolic execution)—perobligationtactic searchhigh, unpredictable — 10-minute hangs observedEmitted proof termscertifying generatorlinear proof checklow; no searchVerified denotationinduction proofonerfllowest第三条是终点每函数或 V4 下每实例类的成本塌缩为单次 kernel defeq 检查——本树在 quoted prepared unit 上为semantics_eq已经成功使用的模式——且任何 tactic 都不再做任何搜索。该检查之所以可用完全依赖上文的denote定义透明性约束放弃它第三行就会悄悄退化成第一行。一次性成本是归纳证明文档诚实定价数周而非数天。第一行现状不摊销每个合约、每个循环不变量、每个算术边条件都要重付。V2 测量十个函数、裸verify的自动化基准2026-08-31 完成的 V2 里程碑是这份提案的证伪实验从 v0 验收语料移植十个函数合约不改写每个都以裸verify尝试。这些 fixture 现在退休于 Check/Verification/Corpus.lean原VerificationV2.leanT3 时并入。文档记录的测量如下v0 sourceFunctionBareverifyCallees.leanbumpautomatic(~3s)Callees.leanbump_twiceautomatic(~30s)Callees.leantake_and_bumpautomatic(~15s)Callees.leanset_pairautomaticCallees.leanforward_set_pairautomaticGlobalBorrows.leanreplaceautomaticGlobalBorrows.leanread_wholeautomaticGlobalInv.leanremoveautomatic函数合约模块不变量尚无 leaner 表面Account.leandepositautomaticwith V6s field-focused borrows见下Account.leanwithdrawautomaticwith V6s field-focused borrows and the branch the denotation subset gained with them十对十全部满足门槛阈值八个。首次测量时只有八个达标Account的两个函数随 V6 的 field-focused borrows 与分支支持加入。验证时间是每函数秒级但仍高于 v0亚秒残余成本是调用边界写回对账call-boundary write-back reconciliation且是可测量的、非结构性的见 V3 注释。仓库中 Corpus.lean 的源码与测量表一一对应三个模块分别移植Callees.leanbump、bump_twice、take_and_bump、set_pair、forward_set_pair、GlobalBorrows.lean/GlobalInv.leanreplace、read_whole、remove、Account.leandeposit、withdraw每个函数都带完整的spec块ensures/aborts_if/modifies/requires与裸verify命令。例如deposit验证的是mut Balance[addr].balance.value字段级全局借用加经引用的检查加法而withdraw额外覆盖带守卫中止if current amount then abort(1)的分支形状。文件头部注释明确说明该文件测量的是 native denotation 交付的自动化而非提供 fixture 专属证明脚本。空虚性发现vacuity findingselect链的健全性教训V6 的调查把一个健全性危险提纯为值得记录的结果LeanerLang 前端曾把mut X[a].f.g降级为值级引用类型select链——这种形状没有运行时意义evaluateDataOperation?拒绝引用操作数只有 exchange 路径的borrow(select(local))树会被 validation 归一化为 place。由于Satisfies是部分正确性——其undefined关系对 M1 子集为空——卡在这种形状上的函数会空真地vacuously满足任何合约一个故意写假的ensures竟然验证通过了。两条结论被记录下来裸verify成功只有在 LIR 每个节点都具有可执行语义时才有意义preparation 必须拒绝无意义形状而不是无条件地把data.select视为可执行——后者正是它现在的做法。实现交接V1–V3 的落地与一值一拼写V1–V3 已完整落地实现分布如下V1 组合子语义与 agreement 库在 LeanerIR/Proofs/Denotation.leancertifying lowering 在 LeanerLang/Denotation.lean直接 WP 驱动器在 LeanerIR/Proofs/DenotationWP.lean。静态参数、局部、全局、字段、构造器、调用与借用位置都由 lowering 选定动态贷款路由使用 native frame/state 索引与封闭的初始 frame/写回方程而不是在 VC 内部靠查找重新发现位置。V3 的 codec 与类型化合约传输实现在 LeanerIR/Proofs/Typed.lean每函数的 nativeArguments/结果类型、codec 与类型化指称由 LeanerLang/Typed.lean 生成。SpecInt、生成的标称孪生、可变实参与抽象泛型载体跨过这一边界而不会在撰写的类型化定理中暴露RuntimeValue公开运行时定理通过 codec roundtrip 与指称 agreement 从类型化定理搬运。全参数化泛型函数量化于一个抽象载体与一个认证 codec。storage-key 相关特化仍是 V4 工作没有实现有限实例化闭包或 trait-evidence monomorphization。V3 稳定化2026-08-31反复应用了一条教训每个值必须恰好有一种拼写every value must have exactly one spelling。收敛与正确性失败全部归结为同一项的两个拼写并存——裸 kernel 投影与命名字段访问、set!与setIfInBounds、Array.mk与字面量、push 形式贷款注册表与其归一化字面量、未展开解码器与其 roundtrip——这会静默击败形状键控重写与omega的句法原子同一性。修复手段归约折叠把卡住的 kernel 投影折回命名形式reconcile 集在形状引理运行前规范化数组拼写封闭 frame 引理陈述于规范字面量拼写量化注册表中的 profile 查找被密封、其方程成为路由事实未路由即达上下文的类型化存储读经FamilyRepresentation重写marker 剥离规范化只在全有或全无的 closing 尝试内运行因此失败子句仍在其撰写的 range 上报。这些测试中没有任何手工 fixture 证明——门槛就是裸verify。里程碑 V1–V7状态全景文档的里程碑表完整记录截至 2026-09-01 状态StatusMilestoneWhat remains before it is doneDONEV1组合子指称、certifying lowering、agreement 生成、native 位置、storage/generic 门控以及最初的裸verifyfixture 门控均在 V3 工作前实现并通过DONEV2十个 v0 corpus 函数以裸verify全部验证通过对比记录如上DONEV3重复嵌套可变调用验证收敛bump_twice与完整五函数VerificationV2fixture验证套件全绿包括此前红色的VerificationAborts与VerificationStorageNOT STARTEDV4Storage-key-dependent 实例化闭包与 monomorphized viewsNOT STARTEDV5取代所生成 agreement 证明的泛型归纳证明IN PROGRESSV6Projected borrows、.return_/.throw_、动态/多重/投影/全局返回引用带分析撰写的死亡、不变量驱动结构化循环全部 native 化并有防回退门控带值 break 与模式赋值仍待办IN PROGRESSRust support三个 Rust-profile 函数经共享 native 路线验证通过引用字段解码仍开放trait/evidence 指称推迟DONE (2026-09-02)V7退休frame 路线移除每个未覆盖目标都是 negative check见 certifying-execution.mdV6 明细引用、分支、循环的 native 化V6 是超越整资源与循环的引用里程碑文档逐一记录了已完成项全部为 DONE其后列明剩余Canonical loweringmut X[a].f.g降级为运行时 place 机制执行的那一形状——整资源全局借用绑定到合成 holder 局部pushTemporaryLocalbody 临时量索引越过所有声明局部并由函数驱动器追加焦点是通过 holder 的deref/field…投影的 place 借用。可变情形不再发出值级引用类型 select 链共享情形保留它们——这是健全的因为 preparation 会把共享引用擦除为其所指。Exit reconciliation无记录死亡的贷款在函数出口对账。exportFrameLoans在导出前结算帧内空洞settleFrameLoans每轮把一个 resting current 移入其帧内空洞使穿过外层贷款逃逸的 holder 携带焦点化突变。此前逃逸 holder 会把陈旧的空洞导出到全局内存。Focused mutation certificateupdateBorrowValue?_focusedBorrowPair为 holder/focus 帧形状闭合 mutate 步骤并注册到驱动器。Focused export certificateexportFrameLoans_focusedGlobalNominal为已结算的 holder/focus 形状闭合 finalization*_focusedBorrowPairSaved与*_focusedGlobalNominalSaved是body 在突变前把读保存到局部的变体。量词与存在义务的闭合两个生成脚本缺口随焦点形状暴露并已为每个函数修复——frame 子句对未修改的键全称量化而 closing 此前无法打开量词故从未触及 keyed-map 定律义务叶子读取位于合约实参行的存在量词之下归一化 pass 在 witness 实例化之前运行无法进入因此 closing 现在在实例化后再归一化一次。raw 脚本也获得了类型化脚本已携带的模块解码器。depositmut Balance[addr].balance.value加经引用的检查加法从裸verify配合requires/ensures/aborts_if/modifies验证通过故意写假的ensures孪生正确失败。Execution gatepreparation 拒绝操作数类型为可变引用的data.select/data.selectVariants求值器读取的是标称值而可变引用是活贷款、其被指物可能持有焦点化空洞。想要字段的前端必须经 place 重新借用。Typing 仍接受该形状因为规范会读它。Loan reconciliation order多个贷款可在同一程序点结束证书按铸造顺序列出。按该顺序对账会在 reborrow 的持有者仍携带其洞时写回使洞逃逸进全局内存、焦点写入落在pending而非资源。endLoans?现在按递减实例序对账reborrow 在它投影的贷款之后铸造故该顺序在持有该值的贷款被写回前结算洞。是执行测试发现此问题证明没有——因为它们都不会在焦点写入后触达move_from。Branches in the shallow denotationnativeBranch运行条件一次让产生的布尔选择分支无 else 时结果为 unitwpExpr_nativeBranch变换条件由其自身的后条件选择分支于是驱动器不再有求值器方程需要重建。语句位置的 branch 现在走浅层路线Verification.raise。Native function controlnativeReturn与nativeThrow求值其 native 值行并抛出相应控制其 WP 与 agreement 定理让返回或中止的分支留在浅层路线。withdraw现在经守卫中止 native 验证不再保留泛型符号执行覆盖。Generated decoders are simp-owned曾展开孪生decode?的符号执行会分裂其触达的每个认证整数的范围测试且假设测试失败的分支之后无法被反驳——孪生内嵌套的SpecInt永远成不了范围假设。解码器在 roundtrip 证明后密封保持折叠直到 closing 针对合约携带的范围事实执行它们。基准无成本。Corpusdeposit与withdraw进入 V2 fixture测量表读作十对十withdraw同时是基准目标焦点借用上的分支成本类别。全部十个 V2 函数携带#leaner_require_native门控泛型验证无法静默满足 fixture。Projected borrows and frame materializationnative reborrow 描述符现在携带任意标称字段步行agreement 使用证明专用的DerefLocalFieldPath可执行描述符只保留局部与已解析字段行。稳定initialLocals加封闭的四/五局部 frame 方程进入 account body 而不暴露依赖数组索引。deposit与withdraw因此端到端使用 native 描述符。Scalar returned reborrow across calls引用类型结果有 native codec被调方 finalization 导出(outerLoan, loanHole returnedLoan)调用方对账从该洞取得转移身份。合约把源参数的可见调用边界值与返回 current 绑定负向回归证明无关的存在退出值不能建立假子句。VerificationReferences.lean 覆盖返回被调方、经第二个函数边界转发引用、经直接返回与转发引用两种突变以及返回贷款死亡后恢复原参数。每个函数都由#leaner_require_native门控。Path-free prophecy and explicit death运行时可变引用保持恰为borrow loan current——没有 owner root 或投影路径。导出值中的loanHole跨调用传递动态身份。借用分析在正常 fallthrough、显式 return 与 throw 处记录LoanDeath值语义 preparation 把它们物化为显式endLoan操作。正常结果携带的贷款被刻意排除在被调方死亡之外以便调用边界转移它们。native WP 有封闭死亡证书而非展开泛型贷款 fold。RuntimeFrame.loanLocations是带语义扫描回退的 validated 局部执行缓存RuntimeState.globalLoans是 keyed 全局写回注册表——两者都不是引用值的一部分。局部返回贷款转移的身份只源自预言洞返回的全局 reborrow 另在globalLoans中把存储键从完成的外层贷款转移到返回贷款。没有引用存储 owner root 或投影路径。Native-only performance gate性能套件测量reborrow、forward_reborrow、set_then_read、set_through_forward含跨两个调用边界的返回引用转移。返回引用方程只对匹配形状派发而非加入每个泛型对账 pass普通重复调用保持在前基线 1% 内。显式生命周期模型刻意重置存储基线replace为 161.7M typed heartbeats一次全局死亡deposit503.0M成对投影死亡withdraw915.6M跨 normal 与 abort 路径——分别为前死亡基线的 35%、38%、24% 增幅。驱动器在封闭 native 死亡证书不匹配时拒绝展开泛型贷款 fold故这些实测成本不可能隐藏符号回退。未来变更以此正确性基线为门控。Returned-reference breadthnative 引用 fixture 现在覆盖两个可变输入加动态选择结果、一对可变结果并经两者突变、投影字段结果及其调用方、从全局存储返回的字段引用及其调用方。连同标量转发共十二个正函数全部#leaner_require_native门控加负向预言测试。转移继续使用预言洞与分析撰写死亡全局所有权元数据在独立注册表中重键而非编码为引用中的路径。Invariant-driven structured loopsnativeLoop是 repeat、continue、break、return、throw 的最小有限归纳关系。其 agreement 定理与 big-step 循环双向WP 定理证明生成不变量初始成立且经一个 native body 步后保持再对有限关系归纳。它不符号展开表达式 id也不携带验证燃料表达式 id 只是选择生成谓词的静态证明标签运行时求值是 elaboratedNativeLoop body关系不做 arena 查找。合约生成把每个撰写的循环不变量翻译为 entry/current frame 与 state 上的 native 谓词记录完整局部行把不可变局部锚定到 entry 槽并在编码局部形状中保留引用贷款身份。VerificationLoops.lean 证明count_to的正常重复与显式continue版本含result limitnative-only 门控。NOT STARTED — 剩余循环形式带值 break 与模式赋值仍在 native 循环子集之外。Rust 支持共享路线的三函数验证Rust-profile 验证与 Move 共用同一 LIR 与 native 证明路线DONE — Native verification fixtureVerificationRust.lean以裸verify证明replace、sum、increment可变引用与标量函数共享普通 native 验证器。DONE — Target pointer width生成的宽度事实比较封闭的支持拼写而非让 kernel 归约String.toNat?Rust unit 无需 profile 专属证明逃生舱即可 elaborate。DONE — Profile-correct arithmeticRustu32加法以模运算合约、无 abort 验证通过同一 Rust 操作对 Move 形状的检查算术 abort 合约正确地不可证。NOT STARTED — Reference-field decoding从引用传入的 struct 读取整数字段仍会搁置解码器范围决策驱动器必须保持认证孪生解码器密封而非分裂Decidable.rec——把嵌套范围作为高优先级 simp fact 加入不能闭合目标还让deposit搜索增加 36%。DEFERRED — Traits and evidencetrait 调用指称、实现证据及其特化轴未启动刻意留在当前 Rust native 验证子集之外。什么被冗余、什么被保留成功后冗余Proofs/WP.lean符号执行机制的大部分——deepWhnf及其 seal 清单、leaner_drive、leaner_storage的 stepping 集成、leaner_flatten。保留燃料解释器及其健全性证明保持可执行形式与 MonoVM 差分测试锚点validation 及其证书不变且借用证书变得更加承重——它为作用域借用恢复授权big-step 关系作为参考语义全部 LIR 元理论2026-08-29 的类型化数据表示全量buildContract其 spec 侧翻译已经浅层、已经类型化。非目标替换 LIR、validation 或前端交换格式。移除 big-step 关系或解释器——删除任一者都会重新引入 v0 的缺陷而那正是不能走天真路线的原因。字节码正确性定理仍超出范围、仍未证明、绝不能被描述为已交付。开放问题Profile 参数化组合子库必须服务 Rust profile 而不只是 Moveintrinsic 组合子是 profile 拥有的部分。哪些组合子属于 core、哪些属于 profile镜像 lir-design.md 中现有的 core/profile 划分。特化等价类V4 从每个语义不同的实参/证据元组一个键的保守起步。哪些元组能按表示相等、实现合约相等或关系参数性定理合并而不使证明搜索更困难V5 是否可达对 LIR 的归纳证明是这里最大单项尚未划定范围。即使 V5 被证明不可行V1–V4 依然有用——所生成证明项是可接受的第二归宿。测试要求每个里程碑门控都是以裸verify f验证的函数数量与 v0 在同函数上的比率对比。自动化率是本提案存在的度量仅 tactic 时间改进不能满足门控。v0/move/Move/Tests/Verification 是验收语料。移植不要重写移植测试需要 v0 不需要的手工证明是要记录的结果而不是要削弱的测试。泛型测试记录哪些参数是 storage-parametric以及从 V4 起计算的资源键 monomorphization 键与生成的 agreement 证明数。基线必须区分一个共享 parametric 证明、storage-key-dependent 组合的精确有限集、未覆盖配置的显式拒绝意外的笛卡尔爆炸即使每个生成的证明都成功也是回归。四套件矩阵leaner-ir、leaner-move、leaner-rust、leaner-e2e-tests全程保持绿色任何里程碑不得以红色落地。历史位置与后续演进本文档于 2026-09-03 移入historical/标记为已执行V1–V3 与 V7 完成而 V6 描述的 native elaborated-Lean 路线已于 2026-09-02 被废弃改用 frame-free row 路线由 certifying-execution.md 设计与跟踪该路线随后又被 denotation.md2026-09-08 决定取代——后者执行 V5 里程碑实现一个指称、一个 agreement 证明LeanerIR/Proofs/Denote/下的compileFunction、compileFunction_agrees与lir_denote归一化关闭器当前verify由 LeanerLang/Verify.lean 实现。遗留的 V4、V5 与被推迟的 Rust shapes 在 certifying-execution.md 的登记簿中继续跟踪。本文档保留的价值在于其设计动机为什么不能把浅层当作权威、V2 测量与空虚性发现它不再更新。跨设计的工作优先级可参考 roadmap.md。无论路线如何更迭这篇设计确立的骨架一直延续至今深度语义是唯一权威验证面向的是带证明连接的派生视图自动化以裸verify的可证明函数数为度量而每个值恰好一种拼写的纪律仍然是 Leaner 验证实现中一切收敛与正确性修复的底层原因。【免费下载链接】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），仅供参考