Leaner 事务测试全解析：用 Lean 语言为 Aptos Move 编译器 v2 构建端到端覆盖

Leaner 事务测试全解析：用 Lean 语言为 Aptos Move 编译器 v2 构建端到端覆盖

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

Leaner 是 Aptos Move 编译器 v2（compiler-v2）中一个独特的测试前端：它让开发者直接用 Lean 4 语言编写 Move 程序，再经 XIR、Move 模型与编译器 v2 的完整流水线编译为生产 Move 字节码，并由真实 VM 执行。本文基于仓库中的 leaner 测试套件说明文档 及其配套源码，完整讲解该流水线的运行机制、leaner专属测试配置、--#事务命令语法、module … where声明方式，并逐项解析 40 余个覆盖文件所验证的语言特性。

Leaner 是什么：从 Lean 源文件到生产 VM 的完整流水线

Leaner 测试套件位于third_party/move/move-compiler-v2/transactional-tests/tests/leaner/目录。文档开篇即点明每个.lean文件经历的完整编译链：

1. XIR 编译：.lean源文件先被编译成 XIR（编译器 v2 的中间表示）；
2. 加载到 Move 模型：XIR 被载入 Move 模型，表示为stackless bytecode（无栈字节码）；
3. 编译器 v2 处理：由 Move 编译器 v2 对 stackless bytecode 进行类型检查、借用检查与代码生成；
4. 生成 Move 字节码：产出可供 MoveVM 执行的生产级字节码；
5. 生产 VM 执行：由事务测试框架的生产 VM harness 实际运行。

这五步缺一不可——Leaner 不是把 Lean 当作独立语言来测试，而是验证 Lean 前端产生的程序经过编译器 v2 全流程后，行为与手写 Move 完全一致。例如 references.lean 首行带有--# publish --print-bytecode指令，要求测试框架同时打印生成的字节码，因此它的基线文件references.exp除了记录执行结果外，还校验生成的resource（全局存储）与 reference（引用）指令是否符合预期。

专属测试配置：从优化矩阵中隔离 Leaner

leaner测试在事务测试框架中拥有专属配置，而不是复用通用配置。在 tests.rs 中可以找到两条关键证据：

• COMMON_EXCLUSIONS常量中包含"/leaner/"，即所有通用配置（baseline、optimize、no-optimize、opt-extra 等）都会把leaner/目录排除在外；
• 专门定义了名为leaner的TestConfig：

TestConfig { name: "leaner", runner: |p| run(p, get_config_by_name("leaner")), experiments: &[], language_version: LanguageVersion::latest(), include: &["/leaner/"], exclude: &[], cross_compile: false, },

这段配置的含义是：leaner配置只运行一次，采用编译器 v2 的默认实验开关（experiments: &[]），并且只包含leaner/目录下的测试、不做交叉编译。代码注释解释得很直白："Lean-authored programs have their own front end and only need one default compiler-v2 configuration. Keep them out of the generic optimization matrix above."（Lean 编写的程序有自己的前端，只需一种默认编译器 v2 配置，应将其排除在通用优化矩阵之外）。

其原因是优化开关组合会改变字节码生成路径，而 Leaner 作为独立前端，其语义正确性只需在默认配置下验证一次即可，无需像手写 Move 测试那样跑完整优化矩阵。

事务命令与 Lake 集成：--#前缀的两重身份

Leaner 测试文件是一种**"Lean 与事务测试指令的混合体"**，两者通过注释语法共存：

--# publish import Move module LeanerBasic where /-! ## Functions -/ @[entry] fun fail (code : U64) : Action Unit := do abort code /-! ## Tests -/ --# run 0x0::LeanerBasic::fail --args 7u64

以上是 basic.lean 的完整内容，它同时展示了两种语法：

• --# publish：声明本文件将被发布到链上（等价于 Move 事务测试中的//# publish）；
• --# run 0x0::LeanerBasic::fail --args 7u64：声明一条执行事务，调用已发布的fail函数并传入u64参数7。

关键设计在于：--#前缀以 Lean 的注释（--）开头，因此这些指令对 Lean 解析器完全透明。文档特别强调：

Transactional commands use the Lean-comment-compatible--#prefix. The local Lake wrapper depends on the main Lean project, so these files also elaborate in the Lean language server without any preprocessing.

即这些文件无需任何预处理，就能直接在Lean 语言服务器（language server）中正常 elaboration（类型检查与展开）。这是 Leaner 工作流的独特优势——测试文件本身就是合法的 Lean 程序，开发者可以享受 Lean 4 的 IDE 支持（语法高亮、跳转定义、类型提示、重构），同时这些文件又能被事务测试框架解析执行。

Lake 集成体现在 lakefile.toml：

name = "LeanerTransactionalTests" defaultTargets = ["LeanerTransactionalTests"] [[require]] name = "move" path = "../../../../lean/move" [[lean_lib]] name = "LeanerTransactionalTests" roots = ["arithmetic", "basic", "calls", "control_flow", "references"]

它声明对主 Lean 项目（../../../../lean/move，即 Move 的 Lean 模型）的依赖，并列出若干个作为 Lean 库根的文件。lean-toolchain 指定工具链版本leanprover/lean4:v4.32.2。正是这个 Lake 包装层让--#指令与 Lean 代码能在同一文件内无缝共存。

module Module where：命名空间、导出与延迟编译

Leaner 支持两种模块声明风格，分别对应文档表格中的不同覆盖文件：

风格一：module Module where（多数测试文件使用）

module LeanerArithmetic where fun calculate (left right : U64) : U64 := ((left + right) * 3 - right) / 2 % 100

如 arithmetic.lean 所示。文档解释：这种写法同时组合了命名空间（namespace）与导出（export），并且把普通def当作私有 Move 函数处理——即模块内部可见，但不会导出为可被外部调用的 Move 函数（除非显式标注@[entry]、@[move_public]等属性）。编译被延迟到整个输入结束时才执行，从而保证整个模块块被完整纳入编译，不会因中途出错而截断。

风格二：namespace … end+#export_leaner（references.lean 使用）

namespace LeanerTxnReferences @[move_struct] structure BalanceValue where value : U64 deriving Copy, Drop, Store @[move_fun] def read_balance (addr : Address) : Action U64 := do let value ← &Balance[addr].balance.value (*value) #export_leaner "LeanerReferences" structs [BalanceValue, Balance] functions [read_balance, add_to_balance, deposit] end LeanerTxnReferences

这种写法把结构体与函数组织在 Lean 命名空间内，再通过#export_leaner指令显式导出为 Move 模块LeanerReferences。注意@[move_fun]标注的def在导出后成为 Move 的公共函数，其测试调用路径为0x0::LeanerReferences::deposit。

覆盖矩阵：41 个文件逐项解读

文档给出了完整的覆盖表格，本节按语言特性分组逐项展开，并补充源码级示例佐证。

基础执行与能力推导

文件	覆盖内容
basic.lean	私有函数调用、显式abort、u64参数
abilities.lean	结构体/枚举/泛型的Copy、Drop、Store、Key精确推导

abilities.lean 展示了能力推导的四种形态：

@[move_struct] structure Plain where value : U64 -- 不声明任何能力 @[move_struct] structure CopyDrop where value : U64 deriving Copy, Drop @[move_struct] structure Stored (T : Type) where value : T deriving Store -- 泛型结构体 @[move_struct] structure Resource where value : U64 deriving Key -- 全局资源 @[move_enum] inductive Droppable where | empty | value (inner : U64) deriving Drop -- 枚举的能力推导

deriving从句由 Leaner 前端解析，在编译到 Move 时按字段类型精确推导出最终能力集合——这与 Move 中has子句的能力检查语义一一对应。

算术、地址与控制流

文件	覆盖内容
arithmetic.lean	返回u64值、局部变量、加减乘除模运算、算术失败（溢出/下溢/除零）
addresses.lean	地址别名注册、模块地址别名、字面地址值、地址相等、非零模块地址下的调用
control_flow.lean	分支返回值、<、<=、相等比较、嵌套分支、汇合点（join points）、尾递归

arithmetic.lean 用一个复合表达式覆盖全部五类算术运算：

fun calculate (left right : U64) : U64 := ((left + right) * 3 - right) / 2 % 100

同时用三个"失败"函数验证 MoveVM 的算术错误语义：value + 1（u64::MAX时上溢）、value - 1（0时下溢）、value / 0（除零）。测试命令如下：

--# run 0x0::LeanerArithmetic::calculate --args 8u64 2u64 --# run 0x0::LeanerArithmetic::calculate --args 81u64 21u64 --# run 0x0::LeanerArithmetic::add_overflow --args 18446744073709551615u64 --# run 0x0::LeanerArithmetic::subtract_underflow --args 0u64 --# run 0x0::LeanerArithmetic::divide_by_zero --args 9u64

addresses.lean 展示了地址系统在 Leaner 中的完整映射：

address_alias application = 0x42 module LeanerAddresses at application where @[move_public] fun own_address : Address := @application @[move_public] fun literal_address : Address := @0xCAFE @[move_public] fun is_application (address : Address) : Bool := address == @application

它验证了：address_alias注册命名地址别名；module … at application把模块部署到非零地址0x42；@application与@0xCAFE两种地址字面量写法；Address的相等比较；以及调用路径0x42::LeanerAddresses::…在非零模块地址下的解析。

control_flow.lean 覆盖分支表达式返回值和比较运算符：

fun classify (value : U64) : U64 := if value < 10 then 1 else if UInt.lessEq value 20 then 2 else 3 partial fun countdown (value accumulator : U64) : U64 := if value < 1 then accumulator else continue countdown (value - 1) (accumulator + 1)

注意两个细节：UInt.lessEq/UInt.equal是 Lean 侧的显式比较函数（对应 Move 的<=与==）；partial fun与continue组合实现尾递归，这是 Leaner 对 Move 递归语义的关键适配（见下文）。choose函数则验证了分支表达式的返回值（if flag then 4 else 5）。

调用、递归与尾递归

文件	覆盖内容
calls.lean	纯/带效果调用的返回值、绑定结果、嵌套调用、直接递归、互递归
tail_recursion.lean	栈安全的纯/带效果尾递归、并行循环参数更新、保留的非尾递归

calls.lean 展示了Action单子（monad）下的调用组合：

fun composed (value : U64) : Action U64 := do let doubled := twice value -- 纯调用的返回值绑定 increment doubled -- 带效果调用（Action） fun bound_call (value : U64) : Action U64 := do let incremented ← increment value -- 用 ← 解开 Action pure (twice incremented) mutual partial fun even_flag (value : U64) : U64 := if value < 1 then 1 else odd_flag (value - 1) partial fun odd_flag (value : U64) : U64 := if value < 1 then 0 else even_flag (value - 1) end

mutual … end块声明互递归函数对。注意sum_down与even_flag都标记partial——因为它们不是尾递归，Lean 无法证明其终止性（终止性证明是 Lean 的核心限制），而 Leaner 需要将这些函数映射为 Move 的普通递归。

tail_recursion.lean 则专门验证尾递归的正确编译：

partial fun countdown (remaining accumulator : U64) : U64 := if remaining < 1 then accumulator else continue countdown (remaining - 1) (accumulator + 1) partial fun alternate (remaining left right : U64) : U64 := if remaining < 1 then left else continue alternate (remaining - 1) right left -- 并行交换两个循环参数 partial fun effect_countdown (remaining accumulator : U64) : Action U64 := do if remaining < 1 then pure accumulator else continue effect_countdown (remaining - 1) (accumulator + 1) partial fun mixed_countdown (remaining accumulator : U64) : U64 := if remaining < 1 then accumulator else if remaining < 2 then mixed_countdown (remaining - 1) (accumulator + 1) -- 非尾调用 else continue mixed_countdown (remaining - 1) (accumulator + 1) -- 尾调用

测试命令直接验证栈安全性：countdown以2000次迭代运行，alternate以2001次迭代运行并验证并行参数交换——若被编译成真正的 Move 循环而非递归，则不会发生栈溢出。mixed_countdown验证同一函数中尾调用与非尾调用混合时仍能正确区分编译。sum_down（非尾递归）则确保普通递归语义被保留。

向量与枚举

文件	覆盖内容
vectors.lean	向量字面量、length/get/set、不可变与可变元素借用
vector_operations.lean	空向量/push、嵌套与布尔向量、native insert/remove 的稳定移位、边界更新、冻结（freeze）、写后借用、越界失败
enums.lean	零元、一元、多元变体与穷尽匹配
enum_patterns.lean	嵌套构造子模式、多重嵌套载荷、通配符、内部模式 fallthrough
enum_payloads.lean	重复与位置字段名、单变体、向量载荷、枚举向量、通配符、携带枚举的调用

vectors.lean 展示了向量在 Leaner 中的三层用法：

fun length : U64 := Move.Vector.length (vector![10, 20, 30] : Move.Vector U64) -- 字面量 fun borrowed : Action U64 := do let values : Move.Vector U64 := vector![10, 20, 30] let value ← &values[1] -- 不可变借用，返回 Action (&U64) (*value) fun borrowed_mut : Action U64 := do let values : Move.Vector U64 := vector![10, 20, 30] let value ← &mut values[1] -- 可变借用 value := 42 -- 通过引用写回 (*value)

vector![...]是 Lean 侧的字面量语法，Move.Vector.get/set映射到 Move 的 native 函数，&values[1]与&mut values[1]则是引用借用语法——这些写法都会被 XIR 翻译成对应的 Move 字节码指令。

enums.lean 演示了枚举在 Leaner 中的完整形态——用 Lean 的inductive声明（@[move_enum]标注），用match … with进行模式匹配：

@[move_enum] inductive Action where | idle -- 零元变体 | transfer (amount : U64) -- 一元变体 | split (left right : U64) -- 多元变体 deriving Copy, Drop, Store fun total (action : Action) : U64 := match action with | .idle => 0 | .transfer amount => amount | .split left right => left + right

match的穷尽性由 Lean 编译器保证（这是 Move 2.x 枚举模式匹配语义的 Lean 前端映射），三个变体的测试分别验证0、单参数、双参数路径。

泛型与存储身份

文件	覆盖内容
generics.lean	真正的泛型结构体、资源、枚举、函数、嵌套实例化调用、向量，以及同一地址上两个实例化保持独立存储身份（经编译器 v2 与 VM 双重验证）
ordered_map.lean	泛型排序向量映射、二分查找、隐式冻结、借用查找、native 向量插入/删除、布尔键、排序、MoveVM 上的重复/缺失键 abort

generics.lean 定义了泛型结构体Box T、Pair T U、泛型资源Vault T、泛型枚举Choice T，以及identity、box/unbox、swap、choose、singleton等泛型函数。其中最具价值的是存储身份测试——文档明确指出：

The generic test publishes, queries, and moves two instantiations of the same generic resource at one address, checking that production bytecode preserves their distinct storage identities.

对应测试命令：

-- The same generic resource at two instantiations must occupy distinct -- storage keys. Both publications at 0x42 therefore succeed. --# run --args 29u64 --signers 0x42 -- 0x0::LeanerGenerics::publish_u64 --# run --args true --signers 0x42 -- 0x0::LeanerGenerics::publish_bool

Vault U64与Vault Bool是同一泛型资源Vault T的两个实例化，但必须占用不同的存储键。测试先以签名者0x42发布Vault U64（值为 29），再发布Vault Bool（值为 true）——两次发布都成功，证明编译器 v2 生成的字节码为两个实例化保持了不同的存储身份。配套的take_u64/take_bool、has_u64/has_bool分别验证读取与存在性查询。

ordered_map.lean 是一个更大型的综合用例：以排序向量实现泛型有序映射，核心是二分查找lower_bound（带尾递归循环与借用参数），并基于它实现contains、borrow（缺失键abort 2）、add（重复键abort 1）、remove等操作。它同时验证了&Map K V参数上的隐式冻结、&entries[index].key嵌套字段借用、entries.insert/remove的 native 调用，以及布尔键（BoolStore）的排序语义。

引用与借用检查：三层验收边界

文件	覆盖内容
references.lean	私有资源函数、不可变/可变嵌套字段借用、读/写、传播的acquires、缺失全局失败
borrow_checker/	毒化感知（poison-aware）的源级接受/拒绝、精确的 Leaner 诊断、编译器 v2 对比失败、生产验证器对比失败、成功的 VM 执行

borrow_checker/README.md 将引用程序的验收边界细分为三层：

1. Leaner 的毒化感知源级检查器，由每个spec声明触发；
2. 编译器 v2 的 stackless-bytecode 引用安全分析（REFERENCE_SAFETY_V3/REFERENCE_SAFETY实验）；
3. 生产 Move 字节码验证器与 VM。

文件按预期边界分组：

• positive 文件（无reject_或leaner_permissive_前缀）：三层全部接受，记录成功的 VM 执行或有意的 VM abort 加状态检查。例如 accepted.lean 中的multiple_immutable（同一变量多个不可变借用）、disjoint_siblings（结构体两个字段的可变借用互不干扰）、child_then_parent（先借子字段再借父字段）等。loop_carried.lean还额外验证：不同的可变源绑定在 Lean 规范化后仍能保持为不同的 XIR 局部变量；
• leaner_permissive_*.lean：Leaner 源级检查器接受，但预期被更严格的下游检查器拒绝。这类文件同时存在.leaner.exp与.no-reference-safety.exp两份基线，分别记录"被编译器 v2 引用检查拒绝"与"抑制该检查后继续到生产验证器"两种结果。文档明确指出后一种配置不是正式验收模式，仅用于对比测试；
• reject_*.lean：在 Leaner 源级 elaboration 阶段即被拒绝，基线记录精确的带源码位置的借用错误。

当前的已知差异（deliberate differences）：

源文件	编译器 v2 引用检查器	抑制编译器检查后的生产验证器/VM
leaner_permissive_unused_handle.lean	在另一个可变借用存活期间拒绝转移	优化移除未使用的句柄后验证器接受，VM 返回5
leaner_permissive_read_only_call.lean	拒绝转移重叠的可变参数	验证器以CALL_BORROWED_MUTABLE_REFERENCE_ERROR拒绝

borrow_checker 的覆盖地图（policy surface）覆盖了可变激活与使用、重借用与谱系（lineage）、不可变引用、冻结、调用摘要与分离、返回引用派生、分支与循环、全局与 abort 回滚、向量别名抽象与结构变更、直接与互递归摘要等十大策略面，每个面都有对应的 positive 与 negative 测试对。

此外，references.lean 演示了 Leaner 对全局存储的引用访问：&Balance[addr].balance.value（不可变读取）与&mut Balance[addr].balance.value（可变写入），add_to_balance被deposit调用时自动传播acquires，未初始化的全局访问则触发 missing-global 失败。

reject_* 负向测试家族

文档表格中列出了 11 个reject_前缀文件，它们验证 Leaner 前端对非法程序的显式拒绝：

文件	拒绝原因
reject_non_tail_continue.lean	continue拒绝位于尾位置之外的自调用
reject_non_self_continue.lean	continue拒绝不指向当前函数的调用
reject_indexed_enum.lean	索引枚举声明被显式拒绝
reject_recursive_enum.lean	递归枚举声明被显式拒绝
reject_empty_enum.lean	空枚举声明在 XIR 发射前被拒绝
reject_unselected_call.lean	带有 Move 属性的辅助函数必须在同一模块请求中被选中
reject_ordinary_call.lean	对任意 Lean 函数的调用在源边界被拒绝
reject_recursive_type.lean	递归数据类型被拒绝，而递归函数仍受支持
reject_recursive_generic_type.lean	通过泛型实例化的间接递归被拒绝
reject_invalid_ability.lean	当字段缺少所需能力时，派生能力被拒绝
reject_unsupported_type.lean	保留但尚未启用的源类型被显式拒绝

以 reject_invalid_ability.lean 为例：若结构体声明deriving Copy，但其某个字段的类型（例如引用类型）本身不具备Copy能力，Leaner 在能力推导阶段就会报错——这与 Move 编译器的能力检查规则完全一致。reject_empty_enum.lean 则展示了错误发生的阶段：在 XIR 发射之前，即前端 elaboration 阶段就终止，避免空枚举流入编译器 v2。reject_non_tail_continue与reject_non_self_continue共同规定了continue的唯一合法用法：在尾位置调用当前函数自身（正是tail_recursion.lean中验证的正向用法）。

事务执行约定：返回值验证与 abort 的保留

文档末尾明确了 Leaner 事务测试的两条执行约定：

Successful computations are checked through ordinary function return values.abortis reserved for tests which intentionally exercise abort behavior.

• 成功计算通过普通函数返回值检查：测试命令不指定预期输出时，框架以函数的返回值作为断言依据（基线文件*.exp记录返回值与执行结果）；
• abort专用于故意测试 abort 行为的用例：basic.lean的fail、ordered_map.lean的重复/缺失键、arithmetic.lean的溢出/除零等，都是有意触发abort以验证错误路径的测试。

这两条约定保证了测试断言的确定性：不依赖日志输出或内部状态，而是以 VM 可观察的行为（返回值或 abort）为准。

如何运行 Leaner 测试

Leaner 测试是 Move 编译器 v2 事务测试套件（transactional-tests）的一部分，通过tests.rs中定义的leaner配置驱动。运行方式与仓库内其他事务测试一致——在third_party/move/move-compiler-v2/transactional-tests目录下以cargo test运行该 crate 的测试，测试框架会自动匹配tests/leaner/下的.lean文件并调用对应配置执行。仓库还通过positive_leaner_baselines_are_clean测试（见 tests.rs）检查所有 positive 用例的基线文件未被意外修改，确保覆盖矩阵始终有效。

需要注意的是：运行这些测试需要仓库中已就绪的完整工具链（Lean 4 工具链版本见 lean-toolchain，为leanprover/lean4:v4.32.2），且 Lake 依赖指向仓库内../../../../lean/move的 Move Lean 模型。

小结

Leaner 事务测试套件是 Move 编译器 v2 与 Lean 前端之间的一座桥梁：它以Lean 注释兼容的--#指令让同一份文件既能在 Lean 语言服务器中获得完整 IDE 支持，又能通过XIR → Move 模型 → 编译器 v2 → 生产字节码 → MoveVM的完整流水线得到端到端验证；以module Module where与namespace+#export_leaner两种声明方式映射 Move 的模块与可见性语义；以专属leaner测试配置将其隔离在通用优化矩阵之外。从基础算术到泛型存储身份、从尾递归到毒化感知的借用检查，这 40 余个文件构成的覆盖矩阵，为 Lean 前端引入的语言特性提供了可执行、可回归、可对比的语义保障。

如果想要深入某个特性，建议从三处入手：先读 README.md 掌握全局覆盖地图，再对照 tests.rs 理解测试配置的隔离设计，最后选择一个感兴趣的.lean文件连同其.exp基线一起阅读——返回值、abort 与生成的字节码都在基线中如实记录。

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