Aptos Leaner 验证器测试组织与 Check 账本：61 个验收夹具的通过率、失败分类与驱动约定

Aptos Leaner 验证器测试组织与 Check 账本：61 个验收夹具的通过率、失败分类与驱动约定

【免费下载链接】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-core 仓库中third_party/move/lean子项目的验收测试组织文档展开，系统解读 Leaner（Move 智能合约的 Lean 形式化验证器）当前 denotation 路线的 Check 验收套件账本：61 个夹具中哪些精确通过、哪些失败、为何失败，以及 Check 驱动的运行方式、基线与更新约定。读完本文，你将掌握LEANER_E2E_SUITE=check lake test的完整使用流程、UB=1基线再生成机制、#leaner_require_native等注解的语义，并能通过逐文件状态表定位验证器尚未覆盖的语言构造。

一、背景：denotation 路线与 Check 账本的角色

test-organization.md 是denotation 路线（denotation route）的验收账本（ledger），记录 leaner-e2e-tests/LeanerE2ETests/Check/ 下全部接受性夹具的状态：哪些精确通过（pass exactly）、哪些未通过、未通过的具体原因是什么。

• 文档更新于2026-09-08，是 denotation 路线的检查点快照，路线设计见 denotation.md（V5：一个 denotation、一个一致性证明）。
• 原始 v0 用例的时间线与映射关系归档在 test-organization-history.md，不在本账本内重复。

denotation 路线的核心思想是：为 LeanerIR 定义一套语义模型（denotation），并证明编译（compileFunction）与求值的一致性（compileFunction_agrees），最终把每个verify目标发布为 Lean 内核可检查的定理。该路线当前"已实现但挂起"——一致性定理按用户决策被assumed（作为公理），直到其归纳证明完成。这一背景决定了账本中大量失败的根因：凡是 denotation 尚未承载的构造，验证器就报"不承载"而非给出错误的诊断差异。

二、总体结果：35 of 61 精确通过，26 失败

账本给出的总账是：61 个 Check 文件中，35 个精确通过（pass exactly），26 个失败。

每一次失败都是 denotation 尚未承载的构造，或者仍断言已退役路线名称的夹具；没有任何一次是诊断（diagnostics）不匹配。

判定标准非常严格：

• 一个文件只有在其全部输出与相邻的.exp基线完全一致（在驱动的上限内，即每个目标180k 验证心跳 verification heartbeats）时才算通过；
• 一个文件只要有一个目标失败就整体失败，无论它证明了其他多少目标；
• 没有.exp文件即意味着预期输出为空（一个干净的验证文件就是没有基线文件的）。

三、五道 Gate 的当前状态

账本把 CI/本地构建与测试门禁分为以下五道，并逐项记录状态：

值得注意的两点：

1. DenotePerformance门禁是性能回归保护：denotation.md 中记录该测试会输出每个目标的心跳数与证明对象规模（直线代码约 1.7–6M 心跳、循环约 20M、带匹配契约的三变体match约 35M），而 e2e Check 驱动把每个验证目标限制在180k 心跳——两套上限的用途不同：门禁衡量证明规模，Check 驱动保证验收可在合理时间窗内完成。
2. leaner-e2e-tests的构建失败与验证器本身无关（是mono-move-lean-link适配器 crate 的 E0061 编译错误），因此账本改用单文件方式采集，不阻塞验收记录。

四、按规模排序的失败类别

26 个失败按缺失能力归为七类：

这七类与 denotation.md 的 "Not carried" 清单完全对应：|、^、有符号按位运算、向量（"类型未被承载"行的来源）、泛型调用/构造函数/字段、递归（被调函数先于调用者验证，drain、recursive_choose即此例）等。换言之，账本的每一行失败都可以直接映射到 denotation 路线的下一步实现清单，这正是该账本作为路线图驱动的价值所在。

五、逐文件状态：完整验收账本

每个名字对应Check/下的一个.lean文件。PASS 意味着整个夹具与其基线匹配；无verify目标的 PASS 仅覆盖执行或诊断，文档中已注明。以下三个表格完整继承原文档，是 Check 套件的"权威体检表"。

5.1 Language（19 个文件：13 通过，6 失败）

5.2 Verification（30 个文件：13 通过，17 失败）

5.3 Negative 与支撑（12 个文件：9 通过，3 失败）

关键规则：正确的拒绝（correct rejection）并不能让一个文件通过——如果它的正向对照（positive control）失败的话。即负向夹具必须同时证明"该拒的拒、该过的过"。

5.4 缺失的 v0 夹具（尚未移植）

账本同时登记了尚未从 v0 移植的夹具与剩余工作量：

六、Check 套件工作原理：驱动、基线与运行方式

6.1 驱动模型

根据 leaner-e2e-tests/README.md 与账本约定，Check 套件的工作方式为：

• 一个 Check 文件就是LeanerLang 源码：模块 + 契约 +verify命令 + 真正的数学所在的证明脚本；
• 驱动自动发现Check/**/*.lean下的每一个.lean文件（任意深度），在各自的 Lean 进程中、在驱动上限（每目标 180k 心跳）下elaborate；
• 驱动把lean打印的全部输出逐字与相邻的<name>.exp基线比较；无.exp文件即表示预期输出为空；
• 约定与 compiler-v2 的基线惯例一致：干净检查无期望文件，打印任何内容的检查恰好以该输出为期望，UB=1会写入或删除文件；
• 正负测试是同一类文件，全部位于Check/下；前端路径（Move/Rust 翻译）保留在自己的目录。

6.2 运行与更新命令

从leaner-e2e-tests目录运行：

LEANER_E2E_SUITE=check lake test # 以 check 套件运行验收 UB=1 lake test # 重新生成基线（UB=1 等价于 UPBL / UPDATE_BASELINE）

LEANER_E2E_SUITE环境变量选择套件：move、rust、check、monovm或monodiff。UB=1重新生成基线后，每个重新生成的 diff 都必须人工审查——基线是"意图行为"的记录，不能被当作自动批准的通行证。

6.3 基线与晋升规则（原文档的硬性约定）

账本末尾的 Conventions 是 Check 套件的"宪法"，必须逐条遵守：

1. 基线记录的是预期行为：负向用例的期望诊断必须点名所测构造或子句；一个不支持的"正向证明"永远不会被记录为预期失败（防止把能力缺失伪装成验收通过）。
2. 文件只能由驱动在未变更的上限下晋升：通过中的 pilot 不晋升任何文件；不得为了把一个移植计为完成而抬高上限。
3. 成功验证的verify会自动通过native audit：部分移植用#leaner_require_native，完成移植的夹具用#leaner_require_native_all。
4. 断言风格的 IR、Move、Rust 测试留在各自所属的包中；已废弃的包仅作参考材料，不再运行。
5. 源码验证不是"所生成字节码的编译器正确性定理"——账本不承诺编译后字节码的等价性。
6. 每批工作结束后，就地更新日期、计数、受影响的行与 Gate 表；提交（commit）单独记录，一次 commit 不改变任何状态。

七、Check 夹具解剖：以真实文件为样本

以下从仓库中选取四个代表性夹具，说明"通过/失败"在源码层面到底是什么形态。

7.1 最简干净用例：Increment.lean

Verification/Increment.lean 是"契约被实现证明"的最简形态，整个文件即为账本中Verification/Increment | PASS的源码：

leaner module 0x42::increment where public fun increment(value : u64) -> u64 := value + 1 spec increment where ensures result == value + 1 aborts_if value + 1 > 18446744073709551615 verify increment

注意其头注释："the check is clean and has no expectation file"——目录清单中Increment.lean确实没有对应的.exp，这正是"干净检查无期望文件"约定的直接体现。

7.2 综合夹具：ControlForms.lean 的完整解剖

Language/ControlForms.lean 是账本中标记FAIL（index_arithmetic有向量局部变量）的文件，但它展示了 Check 夹具的完整构成：

• 路由选择：set_option leaner.route "native"指定 native 路线；
• LeanerLang 模块：leaner module 0x42::control_forms where ...，内含struct、fun、spec ... where、verify声明；
• 顶层验证指令：#leaner_verify 0x42::control_forms::branch_effect与#leaner_require_native ...组合出现——前者把目标发布为验证任务，后者要求 native audit 通过（require语义即"此目标必须真正被原生证明，不许用sorry带过"）；
• 证明卫生检查：文件末尾用run_cmd遍历所有函数名，确认verified定理存在于环境中，并调用collectAxioms断言其中不含sorryAx（不允许 admission）；
• 规范不动点检查：LeanerLang.Print.render输出再formatSource后必须与自身相等，保证源码是规范形式的不动点（canonical fixed point），防止打印器漂移；
• 执行断言：assertRuns携带大量输入/输出对，例如branch_effect在u64::MAX上执行应得到.threw .abort #[.integer 18446744073709551616]——算术失败保留 VM 计算出的真实载荷（这是与 v0 固定零载荷行为的关键差异）；checked_assert_eq/checked_assert_ne验证断言码 19/20 的中止行为。

该文件正是账本中index_arithmetic失败的出处：其fun index_arithmetic(base : u64) -> u64 := do let values := vector<u64>[10, 20, 30] ...含向量局部变量与&values[base + 1]元素借用，而向量未被 denotation 承载，因此它只能以#leaner_require_native做部分覆盖。

7.3 负向夹具：拒绝必须点名来源子句

Negative/Verification.lean 与其基线 Negative/Verification.exp 展示了"正确拒绝"的形态。夹具中的wrong_increment与wrong_action契约刻意写错，其.exp基线精确记录了诊断：

LeanerE2ETests/Check/Negative/Verification.lean:12:4: error: the specification clause `ensures result == value` is not established LeanerE2ETests/Check/Negative/Verification.lean:19:9: error: leaner verification failed

关键点：诊断发生在源契约子句处（12:4 是ensures子句本身），并且文件末尾的run_cmd显式断言环境中不存在wrong_increment.verified这样的定理——错误契约绝不能导出证明定理。同理可参考 Negative/LoopInvariants.exp，它在入口与迭代处分别给出a loop invariant at entry is not established与a loop invariant at an iteration is not established——这正是账本中该文件 PASS 并注明"基线命名了入口处与迭代处未建立的不变量"的依据。

7.4 资源不变量：GlobalInv.lean

Verification/GlobalInv.lean 是账本中FAIL（"准备阶段在whnf处超时"）的文件，但它完整演示了 LeanerLang 的资源验证面：

• spec module where声明模块级全局不变量，包括[update]标记的不变量（old ≤ new 的单调性）；
• 存储内建：move_to<Counter>、move_from<Counter>、exists<Counter>、&mut Counter[addr].value全局可变借用；
• 头部使用set_option leaner.verifyHeartbeats 50000——注意这是单文件提高上限的做法，而账本约定"不得为计数移植而抬高驱动上限"，两者界限分明：驱动上限 180k 是验收基准，文件内选项只影响单个夹具的 elaborate 预算，而该文件恰恰是在准备阶段（whnf归一化不变量）耗尽了预算。

7.5 执行断言的支撑层：CheckSupport.lean

CheckSupport.lean 是执行断言的公共支撑：RunCase/StateRunCase结构体定义输入输出对（后者还固定最终全局/借用状态），assertRuns/assertRunsState通过LeanerIR.Interpreter.Interpreter.run以256 燃料解释执行并把结果与期望值比对。头注释强调：这些是执行检查，与单独生成的契约证明相互独立——这正是账本中"无验证目标但 PASS"（纯执行覆盖）类夹具的运行底座。

八、从账本看 denotation 路线的下一步

账本的 26 个失败与 7 个缺失 v0 夹具，本质上是一张按优先级排序的实现路线图：

1. **向量（11 个文件）**是最大缺口：向量类型、元素借用、length/get/set原语、循环内向量变更（LoopInvariants/clear、Loops/drain）全部依赖它；
2. 泛型（4 个文件）：泛型局部变量、调用、构造函数与字段（GenericStorage的泛型字段）紧随其后；
3. **资源不变量与顺序资源效应（5 个文件）**涉及 denotation 的 wp（weakest precondition）规则对全局状态的表达能力，GlobalInv的whnf超时说明不变量归一化的性能也需优化；
4. **递归与未指定被调函数（2 个文件）**要求把"被调函数先于调用者验证"的策略扩展为支持递归与纯函数摘要；
5. 引用边界（2 个文件）：绑定/调用参数之外的裸借用与返回引用的承载；
6. 清理项（3 个文件）：Verification/Typed、Verification/EnumRefs中已退役路线的断言产物（其移除属 D4），以及 Rust profile 原语的 denotation。

对照 denotation.md 的 "Carried" 清单（标量与受检算术、比较、布尔运算、无符号&、受检移位与转换、常量、if/let/块、abort/assert、提前return、赋值、break/continue、带invariant的循环、单态直接调用、元组、结构体、枚举、局部变量共享借用、NTy.ref可变引用、基于运行时键控全局图的存储原语），可以清晰看到：账本每一行失败都落在 "Not carried" 与 "Carried" 的交界线上。因此，本文所述的账本不仅是一份测试报告，更是 Leaner 验证器后续开发的验收门与进度条——任何新承载的构造，都以"Check 账本中的 FAIL 行翻转为 PASS"作为唯一可信的完成证据。

对读者而言，若要复现或扩展这套验收：在leaner-e2e-tests目录执行LEANER_E2E_SUITE=check lake test即可逐文件验证本账本，新增一个.lean夹具无需注册（驱动自动发现），用UB=1可再生成基线但必须人工审查 diff——这套"自动发现 + 逐字基线 + 人工审查晋升"的组织方式，本身就是一个值得借鉴的验证器验收工程范式。

【免费下载链接】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