企业官网建设流程全解析

Move 规范推断任务配方深度剖析：Aptos Core 语料库 AF-code-017 与0x1::code模块

【免费下载链接】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 Core 仓库中 Move 规范推断（spec-inference）评估语料库corpus-v1.2的样本AF-code-017为线索，完整讲解一个可复现的 Move Prover 规范推断任务是如何构造的：从任务目标与元数据、共享可编辑包机制、依赖闭包边界，到准备补丁、哈希验证与变异评分。读者读完可以掌握这套语料库的"配方"（recipe）设计思想，理解如何把一个真实 Aptos 框架模块（0x1::code）变成可供模型推断规范、并可被自动验证与评分的工作区。

背景：规范推断评估框架与"配方"样本

aptos-move/flow/evaluation/spec-inference/目录下维护着一套可复现的 Move Prover 规范推断评估框架，其总览 README 说明它的目标是在同一批 Move 任务、同一个模型、同一份配置上对比三种工作流（无辅助推断、规定 WP 工作流、自由工作流），并从"是否通过验证"和"是否拒绝错误代码"两个维度给推断出的规范打分。

corpus-v1.2是其中保留的框架语料库（retained framework corpus）。根据 corpus-v1.2/README.md，整个语料库只存储一个可编辑的 Move 包framework/，它包含 154 个模块、257 个 Move 源/规范文件——即所有目标模块及其源码级传递依赖的并集。每个样本只是一个轻量"叠加配方"（overlay recipe）：运行时，控制器复制共享包并应用该样本的preparation.patch，该补丁只移除对应目标的参考规范并写入任务描述符，不存在逐样本的快照。AF-code-017就是这 20 个样本中的一个，专门针对链上代码发布与升级模块0x1::code。

AF-code-017 任务概览：目标、来源与哈希

样本的 README.md 首先给出了完整的目标元数据，这是任务可复现性的根基：

需要说明的是：1c41a4a...是共享包（未应用准备补丁）的哈希，5946660b...是准备后工作树（已应用preparation.patch）的哈希。运行时控制器先复制共享包、应用补丁、再校验哈希一致后才把独立工作区交给 agent——两个哈希的存在使"输入与实验材料未被篡改"成为可机械验证的事实。

目标函数共 5 个：initialize、check_upgradability、freeze_code_object、get_module_names、publish_package。粒度选module意味着 agent 需要为整个模块的这 5 个公开行为写出可验证的规范，而非只盯一个函数。

共享包与编译上下文：模块/文件映射与命名地址

任务配方的关键设计是编译上下文共享。README 明确指出：共享包包含目标模块与其完整源码级传递依赖的并集，模块/文件映射和已解析的命名地址记录在framework/corpus-modules.json中；除本样本目标外的模块都只是编译上下文（compilation context），不是额外的推断目标。

共享包的Move.toml展示了命名地址别名如何被统一解析：

[addresses] Extensions = "0x1" aptos_experimental = "0x7" aptos_framework = "0x1" aptos_fungible_asset = "0xA" aptos_std = "0x1" aptos_token = "0x3" aptos_trading = "0x5" core_resources = "0xA550C18" std = "0x1" vm = "0x0" vm_reserved = "0x0"

注意aptos_framework、aptos_std、std、Extensions都映射到0x1，aptos_experimental/aptos_trading等映射到0x7/0x5，这是 Move 框架地址归一化后的实际形态。文档中列出的"传递源码模块"清单包含约 140 个模块（0x1::account、0x1::object、0x1::ordered_map、0x1::features、0x1::init、0x1::system_addresses、0x1::string等），覆盖了 Aptos 框架的绝大部分，这保证了code.move里引用的任何源码级依赖都能就地编译。

Prover.toml中配置了唯一的 Prover 选项：borrow_natives = ["storage_slot::borrow_storage_slot_resource_mut"]，这是为处理 Move Prover 原生借用的已知边界所必需的。

目标函数解析：结合源码理解推断难点

要理解为什么这 5 个函数构成一个有挑战的推断目标，需要看code.move的实现（共享包内路径sources/AptosFramework/code.move）：

initialize（约 L146）：创世初始化。要求调用者是框架地址（assert_aptos_framework），然后为package_owner创建或追加PackageRegistry。其规范核心是modifies global<PackageRegistry>(owner_addr)、aborts_if !system_addresses::is_aptos_framework_address(...)、ensures exists<PackageRegistry>(owner_addr)——覆盖"状态转移"与"中止"两类合约。

publish_package（约 L159）：包发布/升级入口。它先断言升级策略不是arbitrary，然后执行依赖检查（check_dependencies）、模块名收集（get_module_names）、与既有包逐一比对（同名则check_upgradability，否则check_coexistence）、维护upgrade_number单调递增，最后调用原生request_publish/request_publish_with_allowed_deps。函数中还有多个while循环（遍历旧包、遍历模块、重置初始化状态），是"循环不变量"合约的集中地带。

check_upgradability（约 L297）：判定旧包能否升级到新包。三个断言依次为：旧策略不得是 immutable（EUPGRADE_IMMUTABLE）、策略只能加强不能削弱（can_change_upgrade_policy_to）、新包必须包含旧包全部模块（EMODULE_MISSING）。参考规范用aborts_if_is_partial+ 两个aborts_if表达。

freeze_code_object（约 L240）：冻结代码对象，把所有包升级策略置为 immutable。源码中两个while循环都带内联spec { invariant ... }块（一个断言len(frozen) == i，一个断言i <= len(packages)），这正是文档 Preparation 一节要移除的"内联块"。注意源码注释明确写到"effectful HOF verification does not scale yet (TODO(#20391))"，因此用显式循环 + 重建 vector 而非for_each_mut原地修改——这解释了为什么这些循环不变量是必需的推断材料。

get_module_names（约 L408）：从包的modules收集模块名。循环同样带内联不变量（len(module_names) == i且逐项等于pack.modules[i].name），参考规范以pragma opaque+ensures给出后置条件。

可以看到，这 5 个函数覆盖了状态修改（initialize/freeze_code_object）、中止条件（check_upgradability）、普通结果后置条件（get_module_names）、以及多个带循环不变量的循环——恰好对应 README 要求的 5 类合约类别：normal-result、abort、state-transition、frame、loop-invariant。

准备机制：preparation.patch 移除了什么

任务配方把"可执行实现"与"参考规范"严格分离。README 的 Preparation 一节说明：可执行 Move 实现保持不变，只从 agent 可见的源码中移除目标参考块。具体到 AF-code-017，被移除的是：

• code.spec.move：initialize（1 个块）、check_upgradability（1 个块）、freeze_code_object（1 个块）、get_module_names（1 个块）、publish_package（1 个块）
• code.move：freeze_code_object（2 个内联块）、get_module_names（1 个内联块）

这个可复现变换就是preparation.patch。补丁同时做了两件事：把目标 spec 块替换为空（例如把spec initialize(...)整块抹去），并把code.move中带spec { invariant ... }的内联块替换成空语句。agent 被允许编辑的只有两个文件：

• sources/AptosFramework/code.move
• sources/AptosFramework/code.spec.move

而参考规范在code.spec.move中保留完整（供研究者对照，但实验时对 agent 隐藏）。值得注意的是，该文件顶部还带有一段<high-level-req>高级需求注释，列出 7 条人工审计的安全需求（如"任意升级策略永远不该被使用""升级策略不能超过依赖项的严格程度"），它们是规范推断的语义背景。辅助 spec 函数（spec_deps_abort_from、spec_allowed_deps、spec_module_deps、spec_first_package_named、spec_dep_step_aborts、spec_dep_allowed、spec_is_policy_exempted_address）并未被移除，它们描述了check_dependencies依赖检查循环的递归语义，供 agent 在推断时引用。

不透明边界与依赖契约：opaque 函数的闭包

0x1::code的实现依赖大量原生（native）与外部函数，这些函数对 Prover 是不透明的（opaque），但它们的契约必须可见，证明才能通过。README 将其分为两组：

直接调用的 opaque/无体边界（called function dependencies）共 25 个，例如：

• 0x1::code::request_publish/request_publish_with_allowed_deps（原生发布调用，code.spec.move中以pragma opaque的临时 mock 形式给出契约）
• 0x1::create_signer::create_signer、0x1::event::emit、0x1::features::is_enabled
• 0x1::object::exists_at/is_owner、0x1::ordered_map::*、0x1::vector::*系列
• 0x1::system_addresses::assert_aptos_framework、0x1::signer::borrow_address

这些边界契约引用的传递性 spec 函数共 17 个，如0x1::code::spec_deps_abort_from、0x1::object::spec_exists_at、0x1::string::spec_utf8、0x1::from_bcs::deserializable、0x1::signer::$address_of等。

闭包的遍历规则是：穿过透明的可执行被调方（transparent executable callees）以及从已触达契约中引用的行为谓词。这保证了 agent 在推断publish_package时，check_dependencies虽未透明展开，但其aborts_if/ensures契约（基于辅助 spec 函数表达）足以支撑推理。preparation.patch生成的.move-inference-task.json任务描述符（schema_version 3）把这三类依赖（called / spec / transitive）与source_commit、task_id一起固化，是调度器校验任务输入的依据。

变异评分：合约类别如何被机械化检验

推断出的规范不仅要"能通过 Prover 验证"，还要"能拒绝错误代码"。语料库为 AF-code-017 准备了变异体集合，见mutants/AF-code-017/mutants.json。已收录并验证的变异体包括：

每个变异体都记录了锚点（anchor 的 offset/length/sha256）、编辑（edit 的 kind/length/to）、评审意见，以及验证结果validated.outcome = "killed"——即参考规范能杀死该变异体。评分时，若 agent 推断的规范放过了某个被参考规范杀死的变异体，该变异体就"存活"（survive），规范被判定不合格。由此，"拒绝错误代码"这一目标从抽象口号变成了可判定的机械检查。从语料库设计看，mutants/用于向 agent 展示反例（refutation），mutants-scoring/是保留的评分集（held-out），两者在运行时由控制器强制隔离，避免"在展示过的题上自证"。

复现与运行：从配方到一轮实验

AF-code-017 样本本身不携带独立运行入口，它通过corpus-v1.2的调度管线被消费。完整的运行手册在 spec-inference/README.md，与本文相关的关键点是：

1. 环境准备：Python 3 虚拟环境 + 可选 SDK 依赖（pip install -e '.[claude]'），credentialed 命令经sandbox/with-glm-env.sh包装（读取ZAI_API_KEY映射为 bearer token，且只转发ANTHROPIC_AUTH_TOKEN，不打印密钥）。
2. 验证语料库可复现：python3 corpus-v3.2/build.py --verify（v1.2 的等价物是校验各样本 README 中记录的两个 SHA-256）。
3. 调度：move-inference-pilot读取--corpus-manifest corpus-v1.2/manifest.json、--mutants-root corpus-v1.2/mutants-scoring，结合--source-commit 950e413e...生成调度；v1.2 的持有集通过--disqualification-mutants-root corpus-v1.2/mutants传入，运行时不再给第二次机会。
4. 执行与审计：真实会话只在沙箱内运行（scripts/pilot-sandbox），preflight 校验 SDK/CLI 版本、哈希、排练；审计检查缺失工件、越权路径泄露、令牌不一致等。
5. 评分：harness.score_round --mutants-root corpus-v1.2/mutants-scoring --disqualification-mutants-root corpus-v1.2/mutants——变异体被参考规范杀死则通过，存活则拒斥该契约、整轮被取消资格而非计量。

关于哈希的工程细节：内容哈希基于文件树而非 git 历史，因此即使source_commit因 squash-merge 而不再可达，哈希校验依然成立；但已入库的轮次报告必须调度在已落地的 commit 上（v1.2 的 provenance 即950e413e...），以保证后续可获取。

小结

AF-code-017 展示了规范推断任务配方的完整形态：以0x1::code模块为目标、module粒度、5 个覆盖四类合约的函数、单一共享包加准备补丁的轻量复用、三层依赖闭包（直接调用边界 / spec 函数 / 传递模块）、双重哈希锚定可复现性，以及按义务类别组织、与参考规范互相印证的变异体评分集。无论是想复现这轮评估、理解 Move Prover 在真实框架模块上的推断难度，还是研究如何为其他模块构造同类任务，这个样本都是一份可以直接研读与借鉴的模板。进一步的阅读入口：语料库总览 corpus-v1.2/README.md、框架设计说明 DESIGN.md、以及目标模块的原始实现 aptos-move/framework/aptos-framework/sources/code.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