Aptos MoveFlow 规格推断语料详解：以 AF-account-025 账户序号自增函数为例

Aptos MoveFlow 规格推断语料详解：以 AF-account-025 账户序号自增函数为例

【免费下载链接】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 仓库中 MoveFlow 项目的规格（specification）推断评测体系，以语料样本AF-account-025（目标函数0x1::account::increment_sequence_number）为完整案例，拆解"共享可编辑框架包 + 样例覆层配方（recipe）"的任务构造机制、依赖闭包与哈希校验流程。读完本文，你将理解 Move 形式化规格推断评测中任务样本的完整数据结构，掌握如何基于语料包复现、审查并驱动一个函数级规格推断任务。

一、背景：MoveFlow 与规格推断评测语料

MoveFlow（aptos-move/flow/README.md）是 Aptos 生态中面向 AI 辅助 Move 合约开发的工具链，提供插件生成器、MCP 服务器与编辑钩子。其中一条核心能力是"规格推断"（specification inference）：给定一个缺失规格标注的 Move 函数，让 AI Agent 推断出可用 Move Prover 验证的规范（pre/post 条件、abort 条件等），并用move_spec_check、move_package_wp等 MCP 工具完成验收。

本文章所涉及的语料位于 aptos-move/flow/evaluation/spec-inference/corpus-v1.2/README.md。它是从 Aptos Core 提交950e413e46090d2056740c36dd7a77b1764b6936提取的"人可审查的源码目录"（human-inspectable source catalog），所有实验分支（experimental arm）针对同一份样本使用相同的源码哈希，治疗手段（skills/tools）则单独存放。

语料包含 20 个样本记录（见 manifest.json，其中corpus_status字段（当前为screened）是轮次就绪状态的权威依据），以及编译期 AST 源帧（metadata/candidate-inventory.json）、入选/排除/替补决策（metadata/selection.json）与兼容性证据（screening/summary.json）。

二、AF-account-025 样本概览：一个"覆层配方"

样本 AF-account-025 自身并不是一份独立的框架快照，而是语料中唯一可编辑framework/包之上的一个轻量覆层配方。其运行机制为：

1. 运行控制器（controller）复制共享包 framework/；
2. 应用该样本的preparation.patch；
3. 校验应用补丁后整棵目录树的哈希值；
4. 将验证通过的独立工作区交给 Agent 执行规格推断任务。

该包内含 154 个模块、257 个 Move 源文件/规格文件，是全部目标模块及其"源码级传递依赖"（source-level transitive dependencies）的并集；模块与文件的精确映射、命名地址等记录在 framework/corpus-modules.json。除本样本目标外的模块仅作为编译上下文（compilation context），不是额外的推断目标——这一点保证了每个样本的任务边界清晰可复现。

样本关键元数据一览

其中两个哈希值构成可复现性契约的核心：Shared package SHA-256锁定"复制出来的共享包内容不变"，Prepared tree SHA-256锁定"应用 preparation.patch 之后的工作区状态唯一"。控制器在把工作区交给 Agent 之前必须验证该哈希，任何对共享包的意外改动都会导致校验失败。

三、目标任务：increment_sequence_number 及其参考规格

3.1 目标函数的真实实现

从仓库源码 account.move（共享包内对应 sources/AptosFramework/account/account.move）可以看到目标函数的可执行实现：

public(friend) fun increment_sequence_number(addr: address) acquires Account { ensure_resource_exists(addr); let sequence_number = &mut Account[addr].sequence_number; assert!( (*sequence_number as u128) < MAX_U64, error::out_of_range(ESEQUENCE_NUMBER_TOO_BIG) ); *sequence_number += 1; }

这是一个public(friend)函数，语义要点包括：

• 调用内联函数ensure_resource_exists(addr)（同文件第 420-426 行）保证Account资源存在：当default_account_resourcefeature 开启时自动创建账户（create_account_if_does_not_exist），否则在账户不存在时以error::not_found(EACCOUNT_DOES_NOT_EXIST)中止；
• 通过acquires Account获取可变引用，将sequence_number与MAX_U64比较，超过则abort error::out_of_range(ESEQUENCE_NUMBER_TOO_BIG)；
• 正常路径下将序号加 1——这正是交易防重放（replay protection）机制的基础原语。

3.2 被移除的参考规格

manifest.json 的preparation.records记录了本样本移除的参考块：sources/AptosFramework/account/account.spec.move中increment_sequence_number的1 个规格块。

被移除的参考规格原文位于仓库 account.spec.move：

spec increment_sequence_number(addr: address) { include EnsureResourceExistsAbortsIf; let sequence_number_pre = if (exists<Account>(addr)) global<Account>(addr).sequence_number else 0; /// [high-level-req-4] aborts_if sequence_number_pre == MAX_U64; modifies global<Account>(addr); ensures global<Account>(addr).sequence_number == sequence_number_pre + 1; }

该规格块是任务"标准答案"的锚点，可拆解为四类契约：

• 正常结果（normal-result）：ensures保证函数返回后sequence_number严格等于前置值 + 1；
• 中止（abort）：aborts_if sequence_number_pre == MAX_U64，即序号已到u64上限时以out_of_range中止；同时通过include EnsureResourceExistsAbortsIf继承账户资源不存在时（且 feature 未开启）的中止条件；
• 状态迁移（state-transition）：modifies global<Account>(addr)声明只修改目标地址的Account资源；
• 帧（frame）：let sequence_number_pre = ...定义了前置状态快照，将"迁移前后对比"表达为可验证的等式。

这四条契约类别（normal-result、abort、state-transition、frame）正是任务要求 Agent 覆盖的Required contract categories，也是move_spec_check工具做"契约覆盖率"验收的维度依据。

四、编译上下文：依赖闭包的精确边界

规格推断不是孤立的单函数任务。Agent 写出的规格要能被 Move Prover 编译验证，就必须在完整的依赖闭包内工作。AF-account-025 的 README 明确给出了三层依赖信息：

4.1 不透明（bodyless）边界

证明目标函数时，契约可见但实现不可见的边界函数有：

• 0x1::account::ensure_resource_exists
• 0x1::error::canonical

这些函数是"可传递调用的透明执行目标 + 可达契约中引用的行为谓词"闭包遍历的结果。Agent 在写规格时可以把它们当作带规范的黑盒使用。

4.2 边界契约引用的传递规格函数

• 0x1::bcs::$to_bytes
• 0x1::features::spec_is_enabled

前者服务于序列化类规格（如get_authentication_key中的bcs::to_bytes），后者服务于 feature flag 的规格化判断（如spec_get_sequence_number中对DEFAULT_ACCOUNT_RESOURCE的判断）。

4.3 编译所需传递源模块

README 列出了完整清单（均为0x1::命名空间下），从account_abstraction、aggregator、aggregator_factory、aggregator_v2、any、aptos_account、aptos_coin、aptos_governance、aptos_hash、auth_data、bcs、bcs_stream、big_ordered_map、block，到bls12381、bn254_algebra、chain_id、chain_status、chunky_dkg、chunky_dkg_config、chunky_dkg_config_seqnum、cmp、code、coin、comparator、confidential_amount、confidential_asset、confidential_balance、confidential_range_proofs、config_buffer、consensus_config、copyable_any、create_signer、crypto_algebra、decryption、delegation_pool、dispatchable_fungible_asset、dkg、ed25519、epoch_timeout_config、error、event、execution_config、features、federated_keyless、fixed_point32、fixed_point64、from_bcs、function_info、fungible_asset、gas_schedule、genesis、governance_proposal、guid、hash、init、jwk_consensus_config、jwks、keyless、keyless_account、math128、math64、math_fixed64、mem、multi_ed25519、multi_key、multisig_account、nonce_validation、object、option、optional_aggregator、ordered_map、pool_u64、pool_u64_unbound、primary_fungible_store、randomness、randomness_api_v0_config、randomness_config、randomness_config_seqnum、reconfiguration、reconfiguration_state、reconfiguration_with_dkg、reflect、resource_account、result、ristretto255、ristretto255_bulletproofs、ristretto255_pedersen、secp256k1、secp256r1、sigma_protocol、sigma_protocol_fiat_shamir、sigma_protocol_homomorphism、sigma_protocol_key_rotation、sigma_protocol_proof、sigma_protocol_registration、sigma_protocol_representation、sigma_protocol_representation_vec、sigma_protocol_statement、sigma_protocol_statement_builder、sigma_protocol_transfer、sigma_protocol_utils、sigma_protocol_withdraw、sigma_protocol_witness、signer、simple_map、single_key、smart_table、stake、staking_config、staking_contract、state_storage、storage_gas、storage_slots_allocator、string、string_utils、system_addresses、table、table_with_length、timestamp、transaction_context、transaction_fee、transaction_limits、transaction_validation、type_info、util、validator_consensus_info、vector、version、vesting、voting。

这 100+ 个模块全部存在于共享包的sources/AptosFramework、sources/AptosStdlib、sources/MoveStdlib等目录下（可对照 framework 目录树），编译上下文因此是完整自洽的——无需再从仓库外部拉取任何依赖。

五、预处理机制：可复现转换与编辑边界

5.1 preparation.patch 做了什么

preparation.patch是该样本唯一的可复现转换，做两件事：

1. 删除参考规格：将sources/AptosFramework/account/account.spec.move中increment_sequence_number的整个spec块替换为空行，使任务对 Agent 而言是"规格缺失"状态；
2. 注入任务描述符：新增根目录文件.move-inference-task.json，承载该任务的机器可读元数据。

5.2 任务描述符结构（.move-inference-task.json）

补丁中新增的任务描述符（schema_version: 3）字段如下：

transitive_function_dependencies完整清单包括：0x1::account::create_account_if_does_not_exist、0x1::account::create_account_unchecked、0x1::account::ensure_resource_exists、0x1::account::exists_at、0x1::bcs::to_bytes、0x1::create_signer::create_signer、0x1::error::canonical、0x1::error::invalid_argument、0x1::error::not_found、0x1::error::out_of_range、0x1::event::new_event_handle、0x1::features::contains、0x1::features::is_default_account_resource_enabled、0x1::features::is_enabled、0x1::guid::create、0x1::option::none、0x1::vector::borrow、0x1::vector::length。

注意描述符区分了called_function_dependencies（Agent 写规格时必须直接面向的边界）与transitive_called_function_dependencies（完整传递闭包），后者为控制器/审查者提供全量调用图证据。

5.3 编辑边界（可编辑白名单）

README 明确规定 Agent只能修改以下两个文件：

• sources/AptosFramework/account/account.move
• sources/AptosFramework/account/account.spec.move

可执行 Move 实现保持不变（"The executable Move implementation is unchanged"）——这是评测公平性的关键设计：Agent 的任务是为既有实现补全规格，而非通过改写实现来"作弊式"满足规格。这与 MoveFlow 评测工具链中move-flow experiment compare-implementation（通过对比编译后的 Move 模块拒绝运行时代码改动）的设计意图一脉相承（见 aptos-move/flow/README.md）。

六、评测闭环：从语料到验收

将 AF-account-025 放回 MoveFlow 的评测框架看，一个规格推断任务的生命周期是：

1. 构造：控制器复制 framework/ 共享包 → 应用preparation.patch→ 校验prepared_sha256（dc22fda6257f239bd445546956ab17ae573e75c186cc544cff387ad8e1bf74e5）；
2. 推断：Agent 在/move-inf（默认hybrid-guided战术，WP 诊断驱动不变量工作）或agent-only战术下，只读/只改上述两个白名单文件，产出规格；hybrid 战术下可调用 MCP 工具move_package_wp（推断并注入最弱前置条件规格）与move_spec_check（编译、可接受性、契约覆盖、Prover 验收）；
3. 验收：move_spec_check按normal-result、abort、state-transition、frame四类契约覆盖要求检查 Agent 产出，并通过 Move Prover 验证；外部裁判可用compare-implementation拒绝运行时代码改动；
4. 记录：评测模式下生成的move-flow-manifest.json记录战术、评测标志、渲染后的推断技能哈希与 MCP 工具清单哈希，保证同一评测会话的完全可复现（aptos-move/flow/README.md）。

语料侧对应的证据链则是：样本 README（本任务的 provenance 记录）→ manifest.json（20 样本记录与哈希、removed_reference_blocks清单）→ 语料总 README（样本总表）。

七、结语：为什么这样设计

AF-account-025 这类样本的文档结构体现了一个成熟评测语料的核心诉求——可复现、可审计、边界清晰：

• 共享单包 + 覆层配方避免了 20 个样本各自复制 154 模块的巨大冗余，同时让"全部样本共享同一份源码哈希"成为可能；
• 双哈希校验（共享包哈希 + 预处理树哈希）把"应用补丁、验证结果"变成机器可验的确定性过程；
• 三层依赖闭包（不透明边界 / 规格函数 / 传递模块）为 Prover 提供自洽编译环境，也为规格作者标明"哪些函数必须当作黑盒规范使用"；
• 编辑白名单 + 参考块移除确保评测只测"规格推断能力"，不测"实现改写能力"。

如果你希望把该语料用于自己的规格推断实验，可以从阅读 corpus-v1.2/README.md 与 manifest.json 开始，以 AF-account-025 为最小复现样例：复制共享包、应用preparation.patch、比对dc22fda...哈希，即可获得一个与官方评测完全一致的函数级规格推断工作区；参考规格的"标准答案"则可对照仓库中的 account.spec.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