Aptos Move 验证单态化Monomorphization正确性证明从可执行变换到端到端可靠性【免费下载链接】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 开源仓库aptos-core中 Lean 版 Move 逻辑模型third_party/move/lean/v0/move-model的核心组件——验证用单态化verification monomorphization及其形式化正确性证明。文章以MoveModel/IR/Mono/Correctness/README.md为骨架结合同目录九个 Lean 证明模块与Prover/Translate/Mono.lean的源码系统讲解单态化变换做什么、证明如何分层组织、当前已证明到哪一层、以及通向端到端可靠性定理还差哪些显式义务。读者读完可以掌握该证明工程的模块划分、每个证明层的核心结论与依赖关系并理解运行时类型标签商runtime type-tag quotient这一单态化正确性论证中的关键语义思想。一、背景为什么 Move Prover 需要验证单态化Move 是泛型语言函数可以带类型参数例如fun idT(x: T): T。泛型代码在链上运行时通过运行时类型标签runtime type tag调度——Move 虚拟机在运行时擦除大部分类型参数但对全局存储global storage上的泛型资源操作类型标签会直接影响存储键的构造。对于验证器Prover而言一个核心难题是一个泛型函数对应无穷多个类型实例化而现有的中间验证语言IVL验证链是单态monomorphic的只能验证没有类型参数的函数。Aptos 采用的策略来自 TACAS22 Move Prover 论文先把泛型函数转化为有限多个单态代表实例representative instances再对每个代表运行既有的单态 IVL 验证链。这个无限到有限的转化就是验证单态化verification monomorphization也就是本仓库 Transform.lean 所实现、Correctness/目录所证明正确性的对象。该变换位于MoveModel.IR.Mono命名空间是整个 Lean 逻辑模型中Prover 翻译阶段Prover/Translate/Mono.lean的前置输入其输入端是编译器 v2 产出的 XIR输出端是可供单态 IVL 验证链直接消费的有限模块视图。二、变换本身MonoPlan 与五步流水线2.1 核心数据结构单态化变换的输入输出围绕两个核心结构定义见 Transform.leanstructure MonoKey where funId : FunId typeArgs : List Ty structure MonoPlan where entries : List MonoKeyMonoKey一个待单态化的源函数 id 源类型实参对即(source function id, source type arguments)MonoPlan一个有限的MonoKey列表。采用确定性列表而非有限映射其精妙之处在于键在列表中的位置position就是它生成后的函数 idgenerated function id——不需要额外的编号簿。2.2 每个计划条目的五步变换README 描述的流水线对应源码中Module.specializeFun?Transform.lean查找源声明通过m.decl? key.funId在模块有限函数范围内定位源函数替换类型实参source.instantiate key.typeArgs把条目的类型实参代入函数体与规格删除类型绑定器生成后的声明不带任何typeParams由theorem specializeFun_typeParams_empty保证 binder-free改写调用目标plan.rewriteCfg把函数体内的泛型调用改写到生成的单态函数 id安装声明Module.monomorphize把改写后的声明安装到计划条目所在位置numFuns plan.entries.length且元数据中生成的函数命名为name$mono{generated}Transform.lean。2.3 计划是如何发现的discoverMonoPlanTransform.lean以三类种子出发做闭包given-type 实例每个仍自由的声明参数先被rigidifyTypeArgs变成刚性 given typegivenTypeIndex用 Cantor 对角化把(owner, index)编码为一个全局唯一的参数下标见 Transform.lean标签碰撞实例discoverCollisionArgs对函数观察到的所有资源效果TagEffect做两两运行时标签合一unifyTypeArgs找出两个资源类型在某个替换下运行时标签相同的替换组合闭包closeTypeArgs在兼容的部分替换之间做组合闭包从而覆盖同时碰撞的情形如RT Ru64且SU ST调用闭包对已生成条目中被实例化的调用目标做传递闭包instantiatedCalls。整个发现过程是可执行的计算MonoPlan.validateTransform.lean在可执行层面检查条目去重、maxMonoInstances 1024上限、实参个数与声明类型参数个数一致、以及调用闭包。maxMonoInstances是对递归增长的类型实例化的硬性防护——编译器的 v2 前端在产生 XIR 前就拒绝这类循环但 Lean 通道仍然自己再查一次而不是依赖外部事实。2.4 两层语义陈述README 强调正确性陈述分为两层两层之间的区别是全文的枢纽精确运行时标签正确性exact runtime-tag correctness当生成条目与对应源实例的类型实参具有相同的运行时标签时执行它们结果一致有限代表正确性finite representative correctness每个闭的closed源实例都被某个生成条目代表该代表与它有相同的可观察资源标签相等模式其执行通过一次全局资源键的重命名renaming相关联。区别为什么重要因为相关的别名模式相同即第一层需要的标签相等并不蕴含资源键逐字相等——两个替换可能碰撞结构相同但具体键不同。于是第一层可以用普通的内存相等memory equality第二层必须使用内存重命名关系memory-renaming relation。这正是Correctness/中Types.lean与Coverage.lean分工的根源。三、两种类型实参关系3.1 运行时标签相等TypeArgsTagEqTypes.lean 定义def TypeArgsTagEq (lhs rhs : List Ty) : Prop : lhs.map Ty.toTag rhs.map Ty.toTag该关系说两个实参列表中对应位置的类型具有完全相同的运行时编码。它足够强可以推出README 列出的五条均有对应定理替换后产生相同的运行时类型标签Ty.toTag_instantiate_eq互递归定理对Ty全构造归纳实例化的泛型资源产生相等的ResourceKeyresourceKey_instantiateTypes_eqMonoKey.beq判定MonoKey.RuntimeEqMonoKey.beq_eq_true_iff_runtimeEq这是可执行beq与证明侧RuntimeEq之间的桥在运行时等价的调用方下实例化调用产生运行时等价的被调用方键MonoKey.RuntimeEq.instantiatedCall查找生成 id 返回运行时等价的计划条目MonoPlan.generatedFunId?_isSome_of_runtimeEq_mem与MonoPlan.entry_of_generatedFunId?_eq_some。关键设计决策MonoKey的相等刻意使用运行时标签而非语法Ty相等。于是像struct r与structInst r []这类语法别名会选择同一个生成函数——这正对应可执行计划基于运行时标签的去重MonoKey.beq比较funId 与typeArgs.map Ty.toTag 见 Transform.lean。3.2 标签交互相等SameTagInteractionsCoverage.lean 发展较弱的关系SameTagInteractions。给定声明观察到的效果集它断言对每对资源表达式e₁、e₂key(concrete, e₁) key(concrete, e₂) iff key(representative, e₁) key(representative, e₂)两个执行中的键不必相等只要碰撞结构一致即可。配套定义ObservedKeyRel把每个具体观察键与其代表键配对SameTagInteractions.observedKeyRel_right_unique/left_unique证明该对应是函数性的且单射的ObservedMemoryEq两个内存在所有配对的观察键上取值一致未观察的全局键有意保持自由这是给未来代表执行模拟用的状态关系。两层之间的连接定理是TypeArgsTagEq.sameTagInteractionsCoverage.lean精确标签相等总是蕴含相等的交互模式。这也解释了为什么第一层精确层的证明可以复用到第二层覆盖层——精确是覆盖的充分条件。该关系的根源在变换侧SameTagInteractions的定义与CoversTagInteractions每个闭替换都存在代表都位于 Transform.lean。四、证明依赖图与分层模块README 给出了完整的 mermaid 依赖图。按源码实际 import 关系核对依赖链为Transform.lean ├─ Lookup.lean ──────────── Plan.lean ──── Rewrite.lean ──┐ ├─ Types.lean ──┬─ Plan.lean经 Lookup │ │ └─ Semantics.lean ── Steps.lean ── CFG.lean │ ├─ Types.lean ── Coverage.lean │ └─ Lookup.lean ── Instances.lean │ ▼ MonoVerification.specializedSoundProver/Translate/Mono.lean目录中有意没有聚合 import 包装器只做变换的客户端 import Transform.lean证明客户端按需 import 各自消费的正确性层而 importCFG、Instances、Coverage会通过其普通依赖把当前所有已证明层一起拉进来。各模块的分工与 README 的说明一致文件作用关键结论节选Lookup.lean有界查找特征化生成声明来自计划条目且 binder-free单态化不改动结构声明monomorphize_structsTypes.lean标签相等引理库TypeArgsTagEq的 refl/symm/trans、MonoKey.beq与RuntimeEq等价Plan.lean调用闭包证书 → 具体生成 idgeneratedEntryForCall证书解析的调用必有计划内生成目标Rewrite.lean改写只改调用目标保留操作数、CFG 入口、CFG 大小、终止子Semantics.lean原语语义同余Oper.sem_instantiate_eq标签等价替换下原语语义不变Steps.lean提升到执行步InstrNext/InstrStop/InstrPath传输定理CFG.leanCFG 实例化结构从实例化块查找还原源块入口/大小/终止子不变Instances.lean生成实例查找链键 → 生成 id → 等价条目 → 源声明 → 改写声明运行时实参个数保持Coverage.lean覆盖商SameTagInteractions等价关系、ObservedKeyRel函数性/单射、ObservedMemoryEq五、已证明层的组合方式5.1 恢复生成声明Lookup InstancesLookup.lean 特征化三种查找有界模块查找Module.decl?、特化查找specializeFun?、以及生成程序的查找。核心结论每个生成声明来自某个计划条目且无类型绑定器Module.monomorphize_fun_typeParams_empty。Instances.lean 把查找链打包成模拟证明需要的形式requested key - generated id - runtime-equivalent plan entry - source declaration - instantiated and call-rewritten generated declaration对应定理Module.generatedDecl_of_generatedFunId?_eq_someInstances.lean从generatedFunId?成功与源声明查找成功能同时析出计划条目、entry.RuntimeEq key、生成声明内容以及它与源实例 改写的等式。它还证明了物化保留源声明的运行时参数个数Module.generatedDecl_numParams——这呼应了 IR 语义中调用要求实参个数与d.numParams精确一致的规则见 IR/Semantics.lean。5.2 解析生成调用Plan RewritePlan.lean 消费MonoPlan.Certificate.callClosure。对一个计划内调用方中出现的调用它产出三件事生成的被调用方 id存储在该 id 处的计划条目该条目与实例化后的源调用目标运行时等价的证明。证书用MonoKey.RuntimeEq与可执行计划基于运行时标签的去重一致Transform.lean。Rewrite.lean 随后证明rewriteOper、rewriteInstr、rewriteCfg恰好安装这些生成目标同时保留操作数rewriteInstr_call、CFG 入口rewriteCfg_entry、CFG 大小rewriteCfg_size与终止子块映射只改instrs。这些都是[simp]的展开式定理直接把物化只改调用目标这一事实固定下来。5.3 保持原语语义SemanticsSemantics.lean 证明中心局部方程(op.instantiate lhs).sem ... (op.instantiate rhs).sem ...前提是TypeArgsTagEq lhs rhs定理Oper.sem_instantiate_eq见 Semantics.lean。证明的结构性洞察大多数操作完全擦除类型实参——unpackInst、unpackVariantInst、testVariantInst、getFieldInst的无关性通过模式匹配直接rfl或按值构造归纳。真正有趣的是泛型全局操作getGlobalInst、moveToInst、moveFromInst、existsInst的结果依赖实例化后的ResourceKey因此其证明落到resourceKey_instantiateTypes_eq标签等价替换产生相同键。函数调用与引用操作不通过Oper.sem处理Oper.sem对它们返回none而是由RunFrom关系性地处理——这保持了Oper.sem作为确定偏函数的纯粹性。5.4 提升到执行步与路径Steps CFGSteps.lean 把原语等价提升到 IR/Execution.lean 中的结构化执行判定InstrNext继续指令InstrNext.instantiate_of_typeArgsTagEqInstrStop中止指令InstrStop.instantiate_of_typeArgsTagEqInstrPath有限继续直线路径的逐点传输InstrPath.map_instantiate_of_typeArgsTagEq。值得注意的特殊处理是泛型borrow_global规则InstrNext.borrowGlobalInst/InstrStop.borrowGlobalInst它们构造包含资源键的引用因此证明中要用resourceKey_instantiateTypes_eq把hpresent资源存在性前提与目标态中的键同时改写Steps.lean——运行时标签相等使引用目标相等。CFG.lean 提供互补的结构事实从成功的实例化块查找还原源块Cfg.instantiate_blocks_eq_some_iff并记录实例化保持 CFG 入口、大小与终止子而只映射指令列表。Steps.lean与CFG.lean合起来就是未来对RunFrom/RunFrom.inductGrouped做归纳所需的局部原料——inductGrouped把执行归纳划分为六类语义动作InstrNextCase、InstrStopCase、CallOkCase、CallAbortCase、CallInstOkCase、CallInstAbortCase、TermNextCase、TermStopCase见 Execution.lean。六、与 IVL 可靠性的关系正确性证明的下游消费者是 Prover/Translate/Mono.lean。其中MonoVerification结构体打包四件独立可检查的事实structure MonoVerification (m : Module) (plan : MonoPlan) : Prop where validPlan : plan.validate m .ok () coverage : MonoPlan.Certificate m plan wfProgram : WfProg (m.monomorphize plan).program wfLoops : ... verified : ∀ f d, ... → Verified (m.monomorphize plan).program fMonoVerification.specializedSoundMono.lean把既有的单态 IVL 充分性定理prover_sound对整个生成模块应用一次从而建立每个生成的代表实例满足其生成契约contract注意 README 的精确表述这个定理有意不声称下面这句更强的陈述每个闭的泛型源实例满足其源契约后者要求把任意闭实例连接到其有限代表包括重命名的全局存储与规格环境。这就是下一节列出的剩余义务的由来。另一个设计要点MonoVerification把语义覆盖证书coverage : MonoPlan.Certificate m plan与可执行计划校验一起打包防止调用方仅仅因为物化成功validPlan通过就为任意不完整的实例列表出示成功的 IVL 结果——不完整的计划无法仅凭物化成功而免责。七、剩余的端到端义务README 明确列出通向最终定理的六项补充作为显式证明义务而非隐藏假设发现覆盖discovery coverage证明discoverCollisionArgs、兼容替换下的闭包与调用闭包能对每个闭替换兑现MonoPlan.Certificate.tagCoverage传递效果transitive effects把调用方的可观察效果沿可达被调用方取闭包——FunDecl.tagEffectsTransform.lean目前只记录直接效果整调用内存模拟需要传递集状态与引用重命名state and reference renaming把ObservedKeyRel从资源键提升到全局引用根、值、内存、MoveState与FrameOutcome并证明读、写、移除、借用与调用/返回保持该关系整执行模拟whole-execution simulation对RunFrom.inductGrouped归纳普通指令用Steps.lean控制流边用CFG.lean普通/泛型/递归/互递归调用用Plan.lean与Instances.lean规格传输specification transport在同一键重命名下关联前置/后置规格环境、量词论域、足迹与泛型资源选择器契约转移contract transfer把执行模拟与规格传输结合MonoVerification.specializedSound导出每个被覆盖的闭源实例的契约满足。这些义务以MonoPlan.Certificate为界分离了可执行计划校验与语义覆盖定理——一个不完整的计划不能因为物化成功而被正当化。README 也坦率指出当前开发证明的是结构层与精确运行时标签层最终定理尚未完成这是对证明状态的如实描述。八、如何检查证明开发README 给出了两条构建路径均在third_party/move/lean/v0/move-model目录下该目录是独立的 Lean 工程lakefile.toml定义move-model库与MoveModelTests测试驱动构建终端证明模块即当前已证明层的收口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指向 Aptos CLI 可执行文件因为部分前端嵌入测试masm%/move%在 elaboration 阶段调用aptos move exchange见 lakefile.toml 中的说明。质量红线Correctness/目录中不含任何 admitted 定理——sorry、admit与证明公理均未使用。这是该证明工程可信度的硬性保证也是读者在扩展证明时应当维持的约束。九、关键源码索引以下文件是深入阅读本文所有结论的第一手依据相对仓库根目录变换实现third_party/move/lean/v0/move-model/MoveModel/IR/Mono/Transform.lean正确性证明本文主体third_party/move/lean/v0/move-model/MoveModel/IR/Mono/Correctness/README.md 及同目录Lookup.lean、Types.lean、Plan.lean、Rewrite.lean、Semantics.lean、Steps.lean、CFG.lean、Instances.lean、Coverage.lean下游 IVL 边界third_party/move/lean/v0/move-model/MoveModel/Prover/Translate/Mono.lean执行语义RunFrom、inductGroupedthird_party/move/lean/v0/move-model/MoveModel/IR/Execution.leanIR 原语语义Oper.sem约定third_party/move/lean/v0/move-model/MoveModel/IR/Semantics.leanLean 工程配置third_party/move/lean/v0/move-model/lakefile.toml【免费下载链接】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），仅供参考