Aptos 中的 Leaner Move：从 Lean 4 合约到官方 Move 字节码的编译器管道设计-创锋一号

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 document（design-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 IR（NSIR）。

即：本文描述的是当前已实现的字节码路径，而非新 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 侧的独立分支，既不生成也不消费 XIR：

Lean 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 := false

Move struct 与 enum 通过 Lean 的 deriving 表面声明精确 abilities：has 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是Nat；LIR-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 版本 2；MoveModel/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、地址为0x0，struct 声明携带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 声明加入环境并做重复模块/重复字段等一致性校验。

概念级 API：

pub 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 导出 lambda，XIR 必须保留模型 AST 级形式并在 lambda 提升之前导入；当前一阶 XIR 在 stackless 边界进入。

十二、受支持的子集与拒绝边界

12.1 已实现的标量/资源后端支持

bool、全部整型宽度（u8…u256）、address、signer、struct、native enum、vector 与引用；
常量与局部赋值；
MoveModel.IR中已有的算术、比较与布尔操作；
struct pack/unpack 与基于引用的字段访问；
通过普通构造器与match的 enum 变体 pack/unpack/test；
vector 字面量、empty、push、insert、remove、length、get、set 与元素借用；
全局 exists、borrow、move-from 与 move-to；
不可变与可变字段借用；
引用读、写与 freeze；
jump、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-module`schema 版本 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。

企业官网建设流程全解析