Aptos 中的 Leaner Move从 Lean 4 合约到官方 Move 字节码的编译器管道设计【免费下载链接】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 Move 项目的 living design documentdesign-plan.md为主线系统讲解 Aptos 核心仓库中用 Lean 4 语言编写 Move 智能合约再编译为官方 Move 字节码的完整编译器管道包括术语与目标架构、已落地的四层 IR 边界LIR → IR → XIR → compiler-v2 → 字节码、泛型表示策略、JSON 交换格式、Rust 侧 XIR 模型加载器、受支持的子集边界、双层验证门槛以及端到端差分测试策略。读完本文你将掌握 Leaner Move 的架构骨架、MoveModel.IR/XIR 的数据结构与约束、.lean源文件如何一步步变成可被 Move VM 执行的.mv文件以及该项目当前已实现与尚未实现的能力边界。一、项目背景与文档定位Leaner Move 是嵌入在 Lean 4 宿主语言中的 Move 方言一个 Leaner 模块本身就是普通的 Lean 源码其中每个构造都是被 Lean 展开、并被 Leaner 编译器降低到 Move IR 与字节码的语法片段见 leaner-move.md 开篇定义。宿主语言中不属于该子集的构造闭包、Nat、递归数据、IO、依赖类型运行时值等不会在编译边界被重新解释而是连同源位置信息一起被诊断拒绝。本设计文档的状态是living design document持续演化的设计文档即已决定的决策与待定的开放问题分开记录实现里程碑随原型进展持续更新。它同时是一份术语澄清文档Move.Compiler.LIR是当前编译器面向的具名可执行 CFG独立的 unified LIR design 为 Move、Leaner Move、Leaner Rust 与 Rust MIR 前端/后端保留了一个新的 profile-aware 表示LIR在迁移完成之前本文描述的表示被称为named stackless IRNSIR。即本文描述的是当前已实现的字节码路径而非新 LIR 的设计。二、目标与能力边界2.1 六个核心目标让 Lean 编写的 Move 源码足够简洁从而能评估其开发者体验developer experience以MoveModel.IR作为规范语义编译器 IR以MoveModel.Frontend.XIR作为有限、可序列化的交换表示通过生产级的 Move 二进制格式、序列化器与验证器 crate 产出官方 Move 字节码让同一程序既能被 Lean 解释器执行也能被 Move VM 执行从而在测试中对比两种结果显式拒绝不支持或非法的程序绝不静默改变其语义。2.2 后端保持真泛型后端保留真正的 Move 泛型类型参数、ability 约束、phantom 标记、实例化的用户类型以及操作类型实参从MoveModel.IR经 XIR 一直到字节码都是显式的泛型声明不做单态化monomorphization。Lean 作者模块之间的跨模块依赖已实现而导入 Move 编写的模块、native 函数声明与源码映射source map仍是后续工作。三、泛型表示在面向证明的 IR 中单态构造器仍然作为兼容性简写存在泛型代码则使用显式的实例化形式Ty.typeParam i、Ty.structInst r args、Ty.enumInst r args声明局部的TypeParamDecl值携带名称、ability 约束以及仅 struct 可用的 phantom 标记实例化的 pack/unpack、变体、字段、全局资源与函数调用操作均携带具体类型实参。解释器执行时会把类型实参从值中抹去但在全局资源键中保留它们。在实例化函数调用时解释器先把调用者的类型代入被调用方的 CFG 再执行因此嵌套调用与资源操作都能观察到具体实例化。compiler-v2 则重建move_model::ty::Type::TypeParameter与Type::Struct(..., args)安装模型的TypeParameterKind约束并把操作实例化送入常规的 stackless 与 file-format 管道。导出器为每个声明发出一个参数化声明而不是在每个使用点做特化。3.1 Lean IVL 证明器的有限验证视图Lean 侧的 IVL 证明器使用一个单独的有限验证视图而可执行编译保持真泛型。MoveModel.IR.Mono.Transform会为每个泛型函数创建一个无 binder 的给定实例统一资源标签表达式找出运行时标签冲突的情形在所有同步组合下闭合兼容的冲突传递性地跟踪实例化调用。计划验证器在验证前拒绝缺失的冲突/调用情形MoveModel.Prover.Translate.MonoVerification.specializedSound再把每个生成的代表实例送入既有的单态充分性定理。剩余的证明义务是泛型元定理从统一推导MonoPlan.Certificate.tagCoverage并证明资源键重命名能把每个闭合源实例的执行迁移到其代表实例上泛型 ability 与内存类型化也尚待完成。四、已定架构Settled Architecture四层管道可执行编译器必须经过MoveModel.IR不存在直接的 LIR-to-XIR 降低直接源码验证是 Lean 侧的独立分支既不生成也不消费 XIRLean declarations | | elaboration and kernel checking --------------------------- generated source semantics contract | | | verify f | v | kernel theorem f.verified | | attributes and base LCNF normalization v Move.Compiler.LIR.Module | | name resolution and semantic lowering v MoveModel.IR.Module | \ | -------------------------- interpreter, prover, ref elimination | | explicit export only: finite materialization v MoveModel.Frontend.XIR.MModule | | stable, versioned JSON encoding v XIR model loader | | GlobalEnv declarations baseline stackless FunctionData v compiler-v2 stackless checks and optimizations | v compiler-v2 file-format generator v move_binary_format::CompiledModule | ---- official bytecode verifier | ---- canonical .mv serialization关键结论XIR 只是传输层不是证明表示。源码验证、IR/IVL 验证与生产字节码验证器建立的是三种不同的主张要把直接源码定理连接到产出的字节码需要一条独立的编译器正确性证明。层所有权严格分离Move.Compiler.LIR知道 Lean 声明名与局部名MoveModel.IR拥有可执行语义与变换MoveModel.Frontend.XIR拥有有限交换数据与 JSON 序列化Move model 拥有二进制加载器与 XIR 加载器共享的运行时声明构造compiler-v2 拥有源码发现与编排XIR 以 baseline stackless 字节码的身份加入其目标持有者target holder后续检查、优化、file-format 构造与最终验证都在现有 compiler-v2 管道中完成。依赖方向由 import 强制执行特别是Move.Compiler.LIR只 importMoveModel.IR绝不 importMoveModel.Frontend.XIR从而避免形成 import 环。五、已实现的 IR 边界原型目前使用两个显式转换Move.Compiler.LIR.Module.toIR : Move.Compiler.LIR.Module → Except String MoveModel.IR.Module MoveModel.Frontend.XIR.MModule.ofIR : MoveModel.IR.Module → Except String MoveModel.Frontend.XIR.MModule第二个转换位于MoveModel/Frontend/XIR/FromIR.lean。把它放在MoveModel.IR之外是为了避免反转依赖、形成 import 环。六、Move.Compiler.LIR 扩展Move.Compiler.LIR保持为具名、面向编译器的表示已包含下一阶段需要的大部分元数据模块地址与名称Lean 与 Move 声明名函数可见性entry 函数直接调用信息传递闭包的acquires具名局部变量与块struct 字段名与类型它还携带完整的 Move ability 集合structure AbilitySet where copy : Bool : false drop : Bool : false store : Bool : false key : Bool : falseMove struct 与 enum 通过 Lean 的 deriving 表面声明精确 abilitieshas Copy, Drop, Store, Key。struct本身不授予任何 ability资源用struct ... has Key表示。降低过程把这些 abilities 记录进 LIR、Move IR 与 XIR生产 Move 编译器负责验证字段类型确实支持这些 abilities。当前 Leaner 子集无需任何指令级改动——现有函数调用、引用操作、分支与资源操作都有对应的MoveModel.IR操作。七、MoveModel.IR 扩展既有的MoveModel.IR.Program是语义化的刻意用偏函数表示structure Program where funs : FunId → Option FunDecl structs : StructDecls它既没有有限声明边界也没有部署元数据因此无法靠自身转换回有限的 XIR 值。解决方案是保持Program专注语义外加一层包装namespace MoveModel.IR inductive Visibility where | private_ | public_ | friend inductive Dialect where | stackless | referenceEliminated structure StructMeta where name : String abilities : AbilitySet structure FunMeta where name : String visibility : Visibility isEntry : Bool acquires : List ResourceId structure Module where address : Address name : String program : Program numStructs : Nat numFuns : Nat structMeta : ResourceId → Option StructMeta funMeta : FunId → Option FunMeta dialect : Dialect : .stackless end MoveModel.IR要点模型中的Address是NatLIR-to-IR 降低解析源地址字符串、检查 256 位边界、保留数值地址XIR JSON 用规范十六进制编码。声明计数numStructs/numFuns允许 IR-to-XIR 枚举所有 ID一个良构的有限模块必须为范围内每个 ID 都有声明与元数据且范围外不存在语义相关声明。Dialect 防止仅用于验证器的 IR 意外进入字节码后端Move 源码降低产生.stackless引用消除产生.referenceEliminated。官方后端只接受.stackless因为引用消除引入的 mutation-algebra 操作不是 Move 字节码。Module.mapProgram在程序变换时保留模块元数据模块感知的引用消除包装器必须把 dialect 更新为.referenceEliminated。八、LIR 到 IR 的降低Move.Compiler.LIR.Module.toIR执行唯一的名称解析过程共九步校验 Move struct 与函数名唯一为资源与函数分配确定性的位置 ID解析 struct 类型、被调用函数与被获取资源分配局部 ID参数在前包括用于并行尾调用参数赋值的临时局部按布局顺序分配块 ID 并保留真实 entry ID直接构造MoveModel.IR.StructDecl、FunDecl、Cfg、Block、Instr、Term值把 LIR 的.entry可见性转换为 IR 的.public_加isEntry : true把.friend_转换为 IR 的.friend把 abilities、名称、地址与acquires挂到MoveModel.IR.Module上把结果标记为.stackless。递归函数含互递归是允许的。直接自调用若写作continue f args...且结果立即返回则降低为并行参数赋值加回边到 entry 块若continue指向其他函数或不在尾位置则被拒绝。普通递归调用包括同时含continue的函数里的调用保持调用语义。结构化while/loop体降低为同一FunDecl内部的 CFG 头与回边不生成辅助函数见 loop-design.md。递归 struct 类型在原型中仍被拒绝。九、MoveModel.Frontend.XIR 扩展保留MProgram作为前端导入、证明与解释器测试使用的既有基于列表的 body新增一个可部署包装器而不是强迫遗留 exchange-version-7 输入提供新元数据namespace MoveModel.Frontend.XIR structure MStructMeta where name : String abilities : MoveModel.IR.AbilitySet structure MFunMeta where name : String visibility : MoveModel.IR.Visibility isEntry : Bool acquires : List ResourceId structure MModule where address : Address name : String dialect : MoveModel.IR.Dialect program : MProgram structMeta : List MStructMeta funMeta : List MFunMeta end MoveModel.Frontend.XIR同时提供便捷操作使使用更丰富的包装器不至于让测试变得嘈杂MModule.toProgram、MModule.funId、MModule.resourceId。既有的MProgram.toProgram仍然受支持在 upstream exchange schema 提供模块元数据之前既有 Move/Masm 交换解码可以继续只产出MProgram。9.1 IR 到 XIR 的转换MModule.ofIR物化每个有限偏映射struct 声明与元数据覆盖0 .. numStructs函数声明与元数据覆盖0 .. numFuns局部变量覆盖0 .. numLocals块覆盖0 .. body.size循环成员与目标覆盖各自对应的有限域。范围内缺失值即视为 malformed IR 并返回错误。合约即使原始子句分组不可恢复语义仍然精确把语义表达式编码为单例子句——requires : [contract.requires] abortsIf : contract.aborts.toList ensures : [contract.ensures] modifies : contract.modifies循环不变式同理用包含 IR 合取式的单个 XIR invariant 表示。预期的正确性性质为theorem MModule.ofIR_toProgram (h : module.FiniteWellFormed) : (MModule.ofIR module).toOption.map MModule.toProgram some module.program初始实现可以在证明之前先通过可执行 round-trip 测试建立该性质。十、XIR JSON 格式不重载遗留 exchange 格式当前版本 7而是定义独立的、带版本标识的 schema{ schema: move-xir-module, version: 2, module: { address: 0x0, name: Account, dialect: stackless }, structs: [], functions: [] }线上格式应该把每个声明体与对应元数据合并即使 Lean 表示里两者分开这样 JSON 自包含、便于 Rust 校验。编码规则使用显式编码器而非泛型Repr输出使用 snake-case 外部标签的 enum 变体整型常量编码为十进制字符串模块地址编码为规范十六进制字符串资源、函数、字段、局部与块引用保持位置式positional声明与块顺序确定性地保留拒绝未知 schema 版本Rust 侧还拒绝未知字段。MoveModel/Frontend/XIR/Json.lean编码/解码可部署 schema 版本 2MoveModel/Frontend/Decode.lean保持为遗留 exchange-version-7 解码器。10.1 显式导出命令导出是显式构建动作不是偶发的 elaboration 期写入。基线文件使用#export_leaner_xir compiled to Account.xir.json编译器输入使用#export_leaner Module它在一个面向源码的指令里组合了自动属性发现、语义IR.Module构造与编译器交接请求在其出现处注册、在输入末尾处理因此可以紧跟在 import 之后、namespace 或 open 之前。可选的structs [...] functions [...]后缀显式选择声明。低层#emit_leaner_xir compiled形式只在请求交换文件时物化既有IR.Module。两者都只在 compiler-v2 提供其私有LEANER_XIR_OUTPUT时才写入普通 Lean 构建只做模块校验。推荐的编写形式是module Module where ...宏它一次创建同名 Lean namespace、打开 Move API 与语法并注册导出。struct/enum/fun/entry fun/friend fun项展开为持久元数据属性而普通def仍是仅供规格与证明使用的 Lean 辅助项。仓库中存在对应基线文件可作印证例如 Account.xir.json其中schema为move-xir-module、模块名为Account、dialect 为stackless、地址为0x0struct 声明携带type_parameters、fields含ty: u64与abilities: [copy, drop, store]等完整元数据。十一、Rust XIR 模型加载器后端是move-compiler-v2中的一个输入前端。源码发现把.lean目标与.move分开并启动固定的 Lean 工程。Move AST 变换结束后读取器把 XIR 模块、struct 与函数声明加入既有GlobalEnv构造 baseline stacklessFunctionData插入既有目标持有者。运行时声明构造函数与move-model/src/builder/binary_module_loader.rs共享因此 abilities、签名、字段、可见性、位置与调用图初始化遵循同样的模型不变量。仓库中的 xir_loader.rs 实现了声明到模型的边界XirModuleData/XirStructData/XirFunctionData承载名称、位置、abilities、类型参数、字段、变体与可见性GlobalEnv::load_xir_module负责把解析后的 XIR 声明加入环境并做重复模块/重复字段等一致性校验。概念级 APIpub fn import_xir( env: mut GlobalEnv, targets: mut FunctionTargetsHolder, module: XirModule, ) - Result();编译器九个阶段用serde反序列化 JSON拒绝未知字段校验 schema、边界、ID、CFG 形状、签名与操作类型校验名称并用共享运行时声明构造函数构造模型声明把 XIR 的局部、块、指令与终止符直接翻译为 stackless 字节码把每个函数作为 baseline 变体插入FunctionTargetsHolder运行生产 stackless safety-check 管道运行生产 stackless 优化管道含赋值种类推断与最终活跃变量分析运行 compiler-v2 常规 file-format 生成器运行官方字节码验证器并正常序列化。XIR 导入刻意发生在 AST 级变换之后stackless XIR 没有 Move 模型 AST因此 lambda 提升等 AST 变换无法作用于它。若未来 Leaner 导出 lambdaXIR 必须保留模型 AST 级形式并在 lambda 提升之前导入当前一阶 XIR 在 stackless 边界进入。十二、受支持的子集与拒绝边界12.1 已实现的标量/资源后端支持bool、全部整型宽度u8…u256、address、signer、struct、native enum、vector 与引用常量与局部赋值MoveModel.IR中已有的算术、比较与布尔操作struct pack/unpack 与基于引用的字段访问通过普通构造器与match的 enum 变体 pack/unpack/testvector 字面量、empty、push、insert、remove、length、get、set 与元素借用全局 exists、borrow、move-from 与 move-to不可变与可变字段借用引用读、写与 freezejump、branch、return 与 abort真泛型函数、struct、enum、资源、操作与调用Lean 作者模块之间的同模块与受支持跨模块调用private、public、public(friend)与 entry 函数public fun/friend fun/entry fun用户提供的源码属性如[resource_group (scope global)]记录为 struct/函数元数据并经 XIR 交换携带acquires递归与互递归函数显式continue标记的直接自调用降低为栈安全 CFG 循环结构化while/loop/带标签break/continue降低为函数内 CFG 循环任意块的return见 loop-design.md。12.2 当前边界拒绝以 Move 编写的模块作为源码级 Lean 依赖以及 native 函数声明XIR 具备合格外部类型引用之前跨模块签名中导入的用户定义 struct/enum索引化、递归或空 enum以及 enum 变体字段借用值级getField与updateField递归 struct 类型引用消除引入的 mutation-algebra 操作闭包与一般高阶值仅规范specification用途、无字节码语义的构造后端未显式映射的任何MoveModel.IR操作。不支持的构造必须在诊断中指明函数、块、指令与操作。十三、验证边界13.1 Lean 侧验证源码构造属于受支持的 Leaner 子集名称唯一解析每个 LIR 类型与操作都能降低到MoveModel.IR模块地址在 256 位以内每个范围内局部与块都已声明函数与资源引用在范围内entry 函数满足受支持边界限制递归 struct 声明被拒绝。13.2 Rust 侧验证JSON schema 与版本受支持元数据与声明数组长度匹配每个表与代码索引适合官方 file-format 宽度每个块目标都存在所有 CFG 路径上局部先定义后使用操作元数与局部类型一致调用实参与结果匹配签名return 与 abort 操作数类型正确只接受 stackless、可字节码表示的操作。13.3 部署门槛官方 Move 字节码验证器是强制的——通过 Lean 建模的检查器不能替代通过生产验证器。十四、测试策略14.1 Lean 测试直接执行语义 IR 的源码级spec/verify测试LIR-to-IR 期望形状测试面向 Arithmetic、Account、Read、Calls 的 IR 解释器执行在显式导出/导入边界的 IR-to-XIR 物化与 XIR JSON 测试代表模块的基线 JSON 文件针对未解析名称、非法地址、malformed 有限 IR、不支持操作与递归结构的负向测试。14.2 Rust 测试反序列化并校验每个 Lean 生成的基线 JSON 文件每个 opcode 族的 XIR-to-CompiledModule单元测试字节码序列化/反序列化 round-trip官方验证器接受测试负向验证器与 malformed-XIR 测试确定性逐字节输出测试。14.3 端到端差分测试对每个代表性 Lean 作者 Move 程序把 Lean 源码经 LIR、IR、XIR、JSON 编译为.mv用MoveModel.IR.interpFun执行原始 IR在 Move VM 中执行生成的模块对比返回值、abort 码与相关全局存储。在可行处用 compiler-v2 编译等价的 Move 源码模块反汇编两个模块并比较归一化后的指令行为——精确的表索引与字节偏移不必一致。十五、实现里程碑里程碑状态内容1. 确立 IR 边界已实现为Move.Compiler.LIR增加 abilities新增MoveModel.IR.Module及元数据类型实现toIR移除直接 LIR-to-XIR 降低让既有解释器测试走新 IR 路径新增 LIR-to-IR 形状与失败测试2. 物化 XIR已实现新增MModule与元数据记录实现带检查的MModule.ofIR增加语义Program便捷投影用直接 LIR-to-IR 引号实现lowerToIR增加 round-trip 与 malformed 有限 IR 测试3. JSON 契约已实现冻结move-xir-moduleschema 版本 2实现显式 Lean 编码器/解码器增加显式基线文件与编译器交接导出命令增加基线文件与确定性编码测试4. XIR 模型与 stackless 加载器已实现新增 Rust DTO 与结构校验构造共享模型声明与 baseline stackless targets支持常量、局部、算术、分支、abort、return 与调用运行 compiler-v2 检查、优化、file-format 生成与验证器5. struct、资源、引用、vector 与 enum已实现增加 abilities、struct、字段、globals 与acquires表支持 struct/全局借用、引用、move-from、move-to支持 native vector 操作与元素借用支持泛型 native enum、构造器与穷举嵌套 match经 XIR 保留真泛型声明与实例化操作用 compiler-v2 赋值种类推断与活跃变量分析编译并验证 Account 示例6. 执行置信度与开发者体验进行中Move VM 与 Lean 解释器差分测试改进跨边界源定位诊断事务性.lean测试在 Move VM 中发布并执行算术、调用、引用、vector、enum、泛型、递归与有序映射示例跨模块 Lean 依赖按依赖序编译为普通 Move 函数句柄文档化一键 author/compile/test 工作流扩展语言子集前重新评估语法与生成字节码7. 源码到字节码的证明连接未实现陈述规范化与 LIR-to-IR 降低的语义保持关联生成源码Spec与对应 IR 函数语义把该结果与既有 IR 变换及充分性定理组合把 XIR 序列化/解码当作带检查的表示保持边界而非额外程序语义十六、原型完成定义Definition of Done已检入的 Account 与 Arithmetic 程序编译为确定性.mv文件生成的模块通过官方 Move 字节码验证器生成的模块在 Move VM 中成功执行对全部正向与 aborting 测试用例Move VM 结果与 Lean IR 解释器一致同模块与受支持的 Lean 作者跨模块调用可用一般递归函数与带检查的栈安全直接continue循环可用不支持的类型、操作、导入签名与依赖以清晰错误失败没有任何编译路径绕过MoveModel.IR直接 LIR-to-XIR 降低。十七、开放问题模块标识符应使用建模的Address : Nat还是MoveModel.IR应增加专门的受检查 256 位模块地址类型如何表示源码映射而不污染语义 IR仅用于分析的编译器 API 是否也应导入 XIR哪些消费者需要重建模型 AST 而非 stackless targets连接生成源码语义与MoveModel.IR的最小编译器正确性命题是什么才能在 LCNF 变化下保持稳健Move 编写的依赖模块应如何向 Lean 暴露证明摘要十八、演进记录Change Log 摘要2026-08-15记录初始计划确立强制的Move.Compiler.LIR → MoveModel.IR → MoveModel.Frontend.XIR → JSON管道与初始字节码后端里程碑把.lean目标与包源码发现集成进 Move compiler-v2用 XIR-to-model 加载器替换临时 MASM 桥XIR 以 baseline stackless 字节码身份进入 compiler-v2 生产检查、优化、file-format 生成器与验证器。2026-08-17计划更新到 XIR schema 版本 2、真泛型、vector、enum、abilities、递归、事务性 MoveVM 执行与 Lean 作者跨模块调用把直接源码验证记为独立于 XIR 生成的分支并把源码到 IR 的语义保持记录为剩余端到端证明边界。2026-08-20记录已实现的结构化while/loopCFG 降低、public fun/friend fun可见性关键字与public(friend)导出以及语言定义拆分到 leaner-move.md。延伸阅读Leaner Move 语言定义struct/enum/fun/spec/verify等语言构造的完整定义循环与结构化控制流设计while/loop/continue的 CFG 降低统一 LIR 设计未来与 Leaner Rust、Rust MIR 共享的 profile-aware 表示XIR 模型加载器实现Rust 侧声明到模型的边界代码基线 XIR 示例move-xir-moduleschema 的真实序列化产物Leaner 测试目录资源、entry 函数、合约与证明的一体化示例。【免费下载链接】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），仅供参考