企业官网建设流程全解析

Aptos Move 无栈 IR 的 Lean 形式化框架：语言定义、执行语义与引用消除证明

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

本文围绕 MoveModel/IR/README.md 展开，系统介绍 aptos-core 仓库中third_party/move/lean/v0/move-model这一 Lean 形式化开发：它以 Lean 语言完整刻画了 Move 无栈中间表示（stackless IR）的语法、值、状态、深层规格（specification）、函数契约、关系型大步执行语义、静态类型判定与引用消除（reference elimination）变换。读者阅读后可以掌握该 IR 框架的模块分层、检查证书体系、语义约定、参考实现的证明边界，以及如何用lake build构建与验证这套 Lean 模型。文中所引源码均为当前仓库真实文件，可沿相对路径继续深入阅读。

一、框架定位：为 Move Prover 服务的 Lean 中间表示

Aptos 的 Move Prover 在生产管线中会先把 Move 字节码编译成“无栈字节码”（stackless bytecode），再进行引用消除、规格注入、翻译到中间验证语言（IVL）等步骤。本仓库third_party/move/lean/v0/move-model中的 Lean 模型正是对这条管线的形式化重构：MoveModel/IR目录定义了语言本身，并提供了“执行、类型判定、检查、分析、变换、性质证明”这六类可复用工具，全部以 Lean 定理与归纳类型呈现。

该包刻意不包含 Prover 的中间验证语言 IVL——IVL 的语法、语义、循环分析与最弱前置条件理论位于MoveModel/Prover/Ivl；从 Move IR 到 IVL 的翻译位于MoveModel/Prover/Translate（见 Prover/README.md）。也就是说，MoveModel/IR是一套通用的“程序表示 + 语义 + 证明基础设施”框架，Prover 只是它的一个消费者。

二、模块分层：四层架构全景

原文档用一张 mermaid 依赖图描述模块层次，箭头表示“箭头端模块构建在尾端模块之上”，并刻意省略了可由传递依赖解释的冗余直接导入：

四个层次分别对应四类职责：

• 语言基础层（Language foundation）：Value、State、ValueTyping、Spec、Contract、Syntax，定义运行时值、执行状态、值的语义合法性、规格表达式语言、函数契约与程序语法；
• 执行与检查层（Execution and checking）：Semantics、Execution、CodeTyping、Checked，给出关系型大步语义、结构化执行归纳、静态 IR 类型判定与前端检查证书；
• 可复用分析与证明基础设施（Reusable analyses and proof infrastructure）：Util、Frame、Liveness，提供跨 pass 复用的框架安全谓词、栈索引关系与向后可能活性分析；
• IR 工具（IR tools built from the framework）：Interp（可执行解释器及其正确性）、RefElim（引用消除变换及其正确性定理），它们是直接消费框架的“客户端”。

三、语言基础层：从值到程序语法

3.1 Value：运行时值与引用目标

Value.lean定义运行期与规格期共用的值域、引用根（reference root）与引用目标（reference target），以及结构化的值操作。它是一切执行语义的“原子类型”，后续所有模块都构建在其上。

3.2 State：帧索引的局部变量与全局内存

State.lean给出了字节码状态的两个组成部分（见 State.lean）：

• 帧索引的局部存储：Locals := LocalIndex → Option Value，none表示未初始化；FrameStore := FrameId → Locals按调用深度索引各帧，已退出的帧被清空；
• 类型索引的全局内存：Memory := ResourceKey → Address → Option Value，由“资源类型（含结构类型实参标签）+ 账户地址”定位一个资源值。

该模块还提供了initLocals（参数占0..args.length-1）、memWrite/memRemove（写/删单个资源）、Location（(rsrc, addr)对）、Footprint（modifies子句的全局位置谓词）以及agreesOutside Δ m m'——它断言内存从m到m'的迁移没有触碰 footprint 之外的任何位置，即modifies子句的框架条件（frame condition）。完整状态MoveState携带current帧、frames、memory等组件，普通操作数寻址当前帧，而引用值携带显式帧身份，因此调用期间可以寻址祖先帧。

3.3 ValueTyping：运行时值的语义合法性

ValueTyping.lean刻画“运行期值在声明的 Move 类型下语义有效”的判定（对应IsValid、IsValidList等谓词）。它构成了类型化边界值、循环 havoc、调用与量词域的底层依据，被 Prover 翻译层的多个定理引用。

3.4 Spec 与 Contract：深层规格表达式与函数契约

Spec.lean定义深度规格表达式语言（SpecExp）及其求值关系（EvalSpec、Holds）。规格不是浅层 Lean 谓词，而是一种独立的语法；到了 Prover 翻译阶段才被解释为 IVL 守卫与断言。Contract.lean则定义函数契约（requires/ensures/aborts_if/modifies等）以及契约子句被解释的环境。

3.5 Syntax：三地址无栈字节码与 CFG

Syntax.lean是框架的“语法心脏”（见 Syntax.lean），它消费的是 Move 无栈字节码的单态化片段（对应stackless_bytecode.rs），程序是基本块的 CFG，与StacklessControlFlowGraph视图一致：

• 指令是三地址形式：所有操作数都是局部变量（LocalIndex），代码中不存在嵌套表达式；
• 基本块 = 一串直线指令 + 终结符（jump/branch/ret/abort）；
• Instr.call dsts op srcs对应Bytecode::Call(dsts, Operation, srcs)，其中Oper是被支持的Operation片段。

Oper归纳类型（见 Syntax.lean）覆盖面很广，可以归纳为几大族：

• 整数算术族：add/sub/mul/div/mod/bitAnd…/shl/shr/cast，每个操作携带NumType（宽度 + 符号性）；有符号与无符号仅在范围检查/回绕上不同，比较操作（lt/le/eq）共享，因为值携带数学量值；
• 结构体与枚举：pack/unpack/packVariant/unpackVariant/testVariant及其带类型实参的*Inst变体，getField/updateField；
• 向量族：vecPack/vecLen/vecGet/vecSet/vecPush/vecPop/vecInsert/vecRemove/vecSwap/vecAppend/vecReverse/vecContains/vecIndexOf/vecTrim/vecRotate/vecDestroyEmpty等，是vector原生函数的值级对应物；越界访问会中止；
• 引用操作：borrowLoc/borrowField/borrowGlobal/readRef/writeRef/freezeRef/borrowVecElem/borrowVariantField/testVariantRef——它们可以执行（引用是运行时值RefTarget），但不能直接验证：在翻译中编译为必然失败的断言，验证必须先经过引用消除；
• 变更代数（mutation algebra）：mkMutLoc/mkMutGlobal/childMutField/childMutIndex/getMut/setMut/isParent/mutPathIndex/isMutLoc/isMutGlobal/mutAddr，对应 TACAS 2022 §3.1 中Mut<T>（Mvp::mklocal/mkglobal/field/get/set/is_*）与 Boogie prelude 的$Mutation/$ChildMutation等概念，是完整引用消除的“残迹”，前端永不产生；
• 全局资源操作：getGlobal/writeGlobal/moveTo/moveFrom/exists及其泛型变体。

FunDecl把每个循环头映射到LoopSpec（用户不变量、成员块、循环可能修改的目标），这捕获了生产 Prover 的fat_loop识别与目标分析输出。

四、执行与检查层：关系型语义与结构化归纳

4.1 Semantics：大步操作语义

Semantics.lean（见 Semantics.lean）给出字节码 CFG 的大步操作语义。核心关系是RunFrom：从块内某位置开始，执行剩余指令与终结符；一次终止的运行产生FrameOutcome（正常返回或带内存与中止码的 abort）。关系只描述终止运行，非终止没有结果——这与验证条件的偏正确性（partial correctness）解释一致。

关键约定：

• Oper.sem是非调用操作上的确定性偏函数：none表示实参类型错误而卡住（stuck），some .abort表示运行期中止（算术溢出、除零、资源错误）；
• 分支于非布尔局部变量、跳到未声明块、调用未声明函数同样是 stuck；
• 局部引用根是帧限定的（frame-qualified），调用传递引用时不改变其根；借用分析保证“callee 局部根不逃逸”且“返回引用派生自输入引用”；
• Move 不允许引用的引用，因此read_ref/write_ref要求无引用的负载，freeze_ref检查目标存活且无引用，borrow_field/borrow_vec_elem校验被引用聚合体与所选位置；
• 调用要求精确的实参个数（args.length = d.numParams），与 VM 一致，否则 stuck；
• 调用是“真实”的：Oper.function执行被调用函数的实际函数体；针对契约的模块化调用是 IR→IVL 翻译的性质（见 Prover/README.md），不属于 IR 执行关系；
• 调用在帧current + 1安装 callee，返回时退出 callee 并恢复 caller，abort 丢弃局部帧状态；借用分析防止 callee 局部根逃逸，因此帧深度可复用。

有意思的实现细节：Oper.abortCode（见 Semantics.lean）为向量类的运行期失败统一返回0x20000（镜像std::vector::EINDEX_OUT_OF_BOUNDS），vecReverseSlice/vecRotate/vecRotateSlice返回0x20001，其余运行期失败保留通用执行失败码runtimeAbortCode = 0。

4.2 Execution：可复用的结构化执行归纳

Execution.lean（见 Execution.lean）把“第一步动作”与“后续执行”分离：InstrNext/InstrStop描述单条非函数指令的继续/中止，TermNext/TermStop描述单个终结符。这些局部判定不含递归执行前提。由于函数调用同时贡献 callee 与 caller 延续两个归纳假设，RunFrom.inductGrouped因此只有6 个情形而非RunFrom的 20 个具体构造子。InstrPath打包有限条连续继续头动作的序列，是“一条源指令变成多条目标指令”时可复用的证书——这正是引用消除、单态化等变换证明反复使用的归纳骨架。

4.3 CodeTyping 与 Checked：静态类型判定与前端检查证书

CodeTyping.lean提供静态 IR 类型判定（WfProg、TypedLocals、TypedMemory）与运行时类型保持引理，对应字节码验证器的纪律。Checked.lean则定义前端提供的“声明、输入、状态、执行、整程序”五类检查证书（CheckedFunDecl、CheckedState、CheckedInput、CheckedExecution、CheckedProgram等）。这些证书是显式的：证明消费它们，而非把它们作为执行的前提内置。

五、可复用证明基础设施：Util / Frame / Liveness

• Util.lean：跨 pass 复用的小型反演引理；
• Frame.lean：与 pass 无关的框架安全谓词（FrameSafe等）与栈索引关系型基础设施，为引用消除等变换提供“借用不逃逸”的证明素材；
• Liveness.lean：向后 may-liveness 分析及其传递与稳定引理，用于确定引用及其派生值死亡（die）的位置，从而释放借用。

六、检查层次结构：显式证书驱动的验证边界

原文档的第二张 mermaid 图展示了检查层次——因为操作语义是有意无类型的，畸形状态可被表示且可能卡住，所以前端的保证被做成显式证书由证明消费：

要点：

• 静态一侧：WfFunDecl（指令与 CFG 类型判定）+ConsistentFunDecl（声明与 CFG 形状）合并出CheckedFunDecl，进而得到CheckedProgram.Static；
• 运行期一侧：RuntimeTyped（类型化局部变量与内存）+RuntimeConsistent（引用与借用一致性）合并出CheckedState，并派生出CheckedInput（类型化边界 + 已检查初始状态）与RunFrom.Invariant（单次运行中沿途保持已检查状态）；
• 汇聚点：CheckedExecution是“模拟一条具体运行”的变换最实用边界，它要求静态、输入与一次已检查的运行；CheckedProgram更强，断言“从已检查输入出发的每一次执行”都满足静态检查与条件保持。程序点证明还可以把这些证书进一步投影为分析专用谓词，如FrameSafe。

七、语义约定速览

原文档列出的语义约定可归纳为七条，是阅读任何 IR 定理的前提：

1. 执行是偏正确性关系：非终止无结果；非法类型操作数、非法 CFG 目标、未声明 callee 均卡住；静态与运行期检查证书在定理需要类型或借用安全时排除这些情况；
2. 局部引用根帧限定：调用传递引用不改变其根；借用正确性保证 callee 局部根不逃逸、返回引用派生自输入引用；
3. 引用相等比较目标处引用无关值的兼容擦除运行时类型形状；读、写、冻结、聚合构造、全局存储都强制 Move 的“禁止嵌套或存储引用”约束；
4. 调用要求精确实参个数，操作要求其语义情形描述的精确操作数与结果形状；
5. 具体调用执行 callee 函数体；针对契约的模块化调用是 IR→IVL 翻译的性质；
6. aborts_if采用生产 Prover 的双状态上下文：定义出口使用退出内存，不透明调用使用入口内存；契约满足同时建立两种视图，从而已验证的定义可支撑模块化调用。

八、完整性与路线图：引用消除证明深潜

原文档的进度表给出了各领域的实现状态：

8.1 引用消除：模型了什么

该 pass 建模了 Move Prover 的引用消除阶段（TACAS 2022, §3.1），包含（见 RefElim/Transform.lean）：

• 带帧限定局部根(frame, local)与字段/向量元素路径的运行时引用语义；
• 不可变引用替换、借用图与活性分析、变更值、动态父级分派、块与边分裂、循环目标扩展；
• 过程间借用摘要，以及可变引用参数的 value-in/finals-out 约定；
• 借用检查器的排他性检查、引用局部变量被覆写时的强图更新，以及拒绝误编译的回归测试；
• 通过refElimProg、masmElim%、moveElim%的整程序前端集成。

变换流程本身镜像生产 pass 的结构：先eliminate_imm_refs把&T局部变量变成T值（不可变借用与读取变成拷贝，freeze_ref变成读取）；再做向后的活性分析确定引用及其派生值的死亡点；接着是前向并查型的借用图分析，记录局部根、全局根与引用局部之间的派生关系（边区分直接拷贝、字段与向量索引；汇合处的多条入边即可能的写回父级）；最后重写：借用检出一个变更值，字段/向量借用派生子变更，读写变成getMut/setMut，借用死亡时把负载写回父变更、局部根或全局资源。动态父级测试在汇合有多候选时守卫写回，用块分裂实现分派（新块分配在body.size之上，保留已有块标识符、循环头与回边），循环目标扩展覆盖插入代码写入的每个局部。

被拒绝的程序同样是显式错误（partial transformation）：嵌套引用；被借用的局部根被读或覆写；引用局部在其先前借用的派生值仍存活时被重用；全局借用存活期间操作观察/替换该资源（move_to/exists例外，因为它们不检查被取走的值）；immCheck拒绝在拷贝式不可变借用存活时修改祖先；父变更在子变更待定时不可用；路径不敏感分析拒绝覆写&mut参数槽、把一个变更传给多个&mut参数，以及活子变更存在分支相关中间父级的汇合。相关反例见 Tests/Interp/RefElimAgree.lean。

8.2 延迟写回与 abort 语义

通过引用写只更新变更负载，全局内存直到借用死亡才更新——这种 read-update-write 纪律使编码无别名。若在全局借用存活期间 abort，abort 内存不包含待定负载更新；这对调用者不可观测（VM 在 abort 时丢弃效果），因此AgreeOutcome要求 abort 码相等、但只对正常返回比较内存。定义侧的aborts_if检查可能检视瞬态退出内存，其验证在变换后仍是独立义务。

8.3 证明边界：三层定理

正确性定理证明的是隔离、无摘要的refElimFun管线（针对这个概念性 IR 模型，而非 Move 语言或生产 pass 的全部特性）；前端入口（MProgram.elim、masmElim%、moveElim%）改用带computeSummaries的过程间refElimProg管线——该跨调用扩展可执行且有示例覆盖，但还不是refElim_correct的推论。被证明的边界是显式的：

• refElim_correct假设源程序与不可变中间程序都满足CheckedProgram、CheckedInput证书，外加引用无关的外部实参；
• ImmCheckedFacts证书暴露操作与调用边界所需的类型/借用检查事实；
• CoreCheckedFacts记录入口状态有效性、动态源唯一性、不相交待定子变更的一致写回、局部指令拼接、emitter 包含性以及变更层消费的分组调用与终结符情形；
• 正常结果在普通返回值上一致（仅追加目标内部可变参数 finals）；abort 结果在码上一致，但内存可能不同（abort 时丢弃延迟写回）。

两个层次定理在显式证书边界处完整：

• elimImm_correct：分组执行模拟覆盖指令、调用、返回、abort 与 CFG 边，然后在显式前端证书下把执行搬运到immProgram；
• elimCore_correct：变更值层安装精确发射的入口块并把其已认证执行搬运到变换后程序。结构证书ElimCoreOutInv保留分析收敛、emitter 输出、致密化与分裂块溯源；CoreBlockTrace/CoreInstrTrace分别投影每个声明源块的精确rewriteBlock转移与每条源指令重写及其后的死亡/写回阶段；CoreFrameRel语义不变量与原始变更操作拼接已建立；局部根、全局根、直接父、递归父写回同时保持CoreFrameRel与CoreWriteReady，递归更新由紧凑的PathUpdate证书表示。核心输出逐字保留发射指令——原先“新鲜局部死存储优化”已被移除，使可执行 CFG 与证明轨迹有完全相同的指令边界。

refElim_correct已表达两层的最终组合；这些证明的可复用部分归属于Execution.lean、Frame.lean、Liveness.lean、Checked.lean，pass 特定关系保留在 RefElim/Correctness.lean。可执行一致性（agreement）与拒绝反例由 Tests/Interp/RefElimAgree.lean 覆盖。

九、解释器：可计算执行与健全性

Interp/Exec.lean提供基于 fuel 的可执行解释器（见 Exec.lean），使前端产出的程序可用#eval直接运行。与关系型语义用函数表示内存/局部变量不同，解释器用关联列表表示内存（IMem := List (ResourceKey × Address × Value)）、用列表表示局部变量（ILocals := List (Option Value)），并提供denote把可执行表示解释回函数值语义。关系语义卡住时解释器返回InterpError.stuck；每次递归调用消耗一单位 fuel，终止性因此是结构性的，调用者须提供足够 fuel。Interp/Correctness.lean 证明其相对RunFrom的健全性（interpFun_sound）。

十、单态化：Mono 变换与正确性

Mono/Transform.lean实现有限 given 类型、运行时标签碰撞与调用闭包的单态化：一个MonoPlan是MonoKey = (source function id, source type arguments)的有限列表，键在列表中的位置即生成的函数 id；对每个条目，pass 依次查找源声明、替换类型实参、移除类型 binder、把源函数调用重写为生成函数 id、把结果声明安装到列表位置。

正确性论证被拆成可独立演化的多层（详见 Mono/Correctness/README.md）：

• 精确运行时标签正确性：执行生成条目与执行对应源实例在类型实参运行时标签相同时一致；
• 有限代表正确性：每个闭源实例都由一个可观察资源标签等值模式相同的生成条目代表，其执行通过全局资源键的重命名相关联。

Types.lean定义TypeArgsTagEq lhs rhs := lhs.map Ty.toTag = rhs.map Ty.toTag；MonoKey相等刻意使用运行时标签而非语法Ty相等，因此struct r与structInst r []这类语法别名会选中同一个生成函数。Coverage.lean发展更弱的SameTagInteractions关系（仅要求键的碰撞结构一致），并提供ObservedKeyRel（功能且单射）与ObservedMemoryEq。Lookup.lean/Instances.lean/Plan.lean/Rewrite.lean/Semantics.lean/Steps.lean/CFG.lean分别处理声明恢复、调用解析、原语语义保持与执行步/路径提升。当前开发证明了结构与精确运行时标签两层，尚未证明“把所有生成代表验证转给每个闭源实例化”的最终定理——该桥接的六个剩余义务（发现覆盖、传递效应、状态与引用重命名、整执行模拟、规格搬运、契约转移）在 Mono/Correctness/README.md 中被列为显式证明义务，而不是隐藏假设。

十一、包边界与开发规范

原文档对目录职责给出明确约定：

• 核心 IR 数据、语义、通用分析与可复用证明模板放MoveModel/IR；
• 直接消费并产出 Move IR 的变换放本目录，且“通用可复用机制”与其正确性证明分离；
• 可执行前端解码与展开（elaboration）放MoveModel/Frontend；
• IVL 与最弱前置条件理论放MoveModel/Prover/Ivl；
• Move IR 到 IVL 的编译器及其充分性证明放MoveModel/Prover/Translate。

规范还要求：每个公共声明都应有简洁的文档注释，说明它表示/证明了什么、属于哪个抽象层。这与Prover/README.md的边界一致：通用 IVL 语法/语义/验证条件理论在Ivl，Move 特有状态与规格解释在Translate，可复用的 IR 概念与分析在MoveModel/IR。

十二、构建与验证

正确性目录与整个 Lean 模型可通过以下命令构建（见 Mono/Correctness/README.md）：

# 构建单态化正确性的三个终端证明模块 lake build \ MoveModel.IR.Mono.Correctness.CFG \ MoveModel.IR.Mono.Correctness.Instances \ MoveModel.IR.Mono.Correctness.Coverage # 构建整个 Lean 模型及其测试 lake build APTOS_MOVE_CLI=/path/to/move lake test

其中APTOS_MOVE_CLI指向 Move CLI 可执行文件，供嵌入 masm/Move 源码的测试使用。正确性目录不含任何 admitted 定理：sorry、admit与证明公理均未被使用。测试位于 MoveModel/Tests，覆盖算术、控制流、全局内存、引用、变更、跨调用引用、向量与变体等场景，Tests/Interp/RefElimAgree.lean专门验证引用消除的可执行一致性与被拒程序反例。

结语

MoveModel/IR是一套围绕 Move 无栈 IR 构建的完整 Lean 形式化框架：从三地址 CFG 语法、帧限定引用与类型索引全局内存，到关系型大步语义、显式检查证书、可复用执行归纳与活性分析，再到可执行解释器、单态化与引用消除两大变换及其正确性证明。它以“证书显式化、证明边界分明”为设计哲学：前端保证以证书形式被消费而非内置为语义前提，未完成的端到端义务以证明义务清单形式透明开放。若要继续深入，建议按 模块索引 依次阅读Syntax.lean→Semantics.lean→Execution.lean→Checked.lean，再进入RefElim/Transform.lean与Mono/Transform.lean的证明开发。

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