企业官网建设流程全解析

Aptos Move 规范推断评测样本解析：AF-account-036 与 revoke_any_signer_capability

【免费下载链接】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 仓库中aptos-move/flow/evaluation/spec-inference评测体系的语料样本AF-account-036为核心，完整剖析一个函数级 Move Prover 规范推断任务的构成：目标函数、编译上下文、透明依赖闭包、可复现的准备补丁以及变异体评分机制。读者读完可掌握如何读懂/构造一个规范推断评测样本，并理解 Move Prover 规范（aborts_if/ensures/modifies）如何在自动化评测中通过变异体验证（Mutation Testing）被严格检验。

样本在评测体系中的定位

AF-account-036是 MoveFlow 项目的"Move 规范推断评测"（Move Specification-Inference Evaluation）框架中corpus-v1.2语料库的一个样本。该框架的目标是可复现地评估 Move Prover 规范推断能力：在同一批 Move 任务上、用同一个模型、同一份配置，对比三种工作流——无辅助推断（unaided inference）、规定 WP 工作流（prescribed WP workflow）与自由工作流（free one），并最终既看生成的规范能否通过 Prover 验证，也看它能否拒绝错误的代码（见 spec-inference/README.md）。

corpus-v1.2是从 Aptos Core 提交950e413e46090d2056740c36dd7a77b1764b6936准备的、共 20 个样本的保留语料库（见 corpus-v1.2/README.md）。AF-account-036是该语料库中针对账户模块签名者能力授予（signer capability offer）撤销函数的评测样本，其完整目录位于 samples/AF-account-036。

目标函数：0x1::account::revoke_any_signer_capability

样本的目标（Target）明确为：

• 目标：0x1::account::revoke_any_signer_capability
• 粒度（Granularity）：function
• 原始源码：aptos-move/framework/aptos-framework/sources/account/account.move
• 共享包内路径：sources/AptosFramework/account/account.move
• 源码根目录：aptos-move/framework/aptos-framework

被推断的目标函数在共享包中的实现如下（见 corpus-v1.2/framework/sources/AptosFramework/account/account.move#L1046-L1052，与主仓库 account.move#L1046-L1052 一致）：

/// Revoke any signer capability offer in the specified account. public entry fun revoke_any_signer_capability(account: &signer) acquires Account { let offerer_addr = signer::address_of(account); assert_account_resource_with_error(offerer_addr, ENO_SUCH_SIGNER_CAPABILITY); let account_resource = &mut Account[signer::address_of(account)]; account_resource.signer_capability_offer.for.extract(); }

从源码结构看，该函数的行为可以归纳为三点契约：

1. 状态变更（state-transition）：通过&mut Account[...]修改Account资源，并将signer_capability_offer.for这个Option<address>字段执行extract()，即清空签名者能力授予。
2. 中止条件（abort）：当账户的Account资源不存在（或默认账户资源特性未启用时的等价检查）时，调用assert_account_resource_with_error中止；当signer_capability_offer.for为None时，Option::extract中止。
3. 正常结果（normal-result）：正常返回后，signer_capability_offer.for必为None。

其中assert_account_resource_with_error是内联辅助函数（见 account.move#L1069-L1078）：

inline fun assert_account_resource_with_error(account: address, error_code: u64) { if (features::is_default_account_resource_enabled()) { assert!( resource_exists_at(account), error::not_found(error_code), ); } else { assert!(exists_at(account), error::not_found(EACCOUNT_DOES_NOT_EXIST)); }; }

它根据DEFAULT_ACCOUNT_RESOURCE特性开关决定走resource_exists_at（特性开启）还是exists_at（特性关闭）两条检查路径——这也是参考规范中aborts_if !exists<Account>(addr)的语义来源。

参考规范（Reference Specification）

评测体系把"正确答案"定义为从共享包中被移除的参考规范块。AF-account-036在account.spec.move中对应的参考块是（见 corpus-v1.2/framework/sources/AptosFramework/account/account.spec.move#L542-L548，与主仓库 account.spec.move#L542-L548 一致）：

spec revoke_any_signer_capability(account: &signer) { modifies global<Account>(signer::address_of(account)); /// [high-level-req-7.4] aborts_if !exists<Account>(signer::address_of(account)); let account_resource = global<Account>(signer::address_of(account)); aborts_if !option::is_some(account_resource.signer_capability_offer.for); }

注意参考规范中通过modifies声明了对global<Account>(signer::address_of(account))的修改；aborts_if覆盖"账户不存在"和"无授予可撤销"两条中止路径；high-level-req-7.4是链接到高层需求的追踪标签。与revoke_any_rotation_capability（见 account.spec.move#L561-L570）不同，revoke_any_signer_capability的参考块没有显式写出ensures后置条件——但变异体评分恰恰通过ensures is_none(offer.for)这样的契约来检验模型是否补全了这一语义，详见下文。

该函数在上层模块中的调用

revoke_any_signer_capability不是孤立函数：multisig_account模块在remove_owners等治理操作中调用它（见 multisig_account.move#L699 与 multisig_account.move#L761），同时同模块的revoke_signer_capability在确认目标地址确实持有授予后也会委托给它（见 account.move#L1034-L1044）。这意味着该规范的准确性会向上游传递，是多签账户治理安全性的底层依赖。

共享包与编译上下文

AF-account-036的样本 README 强调：语料库只存储一个共享的可编辑framework包（corpus-v1.2/framework），其中包含 154 个模块、257 个 Move 源/规范文件——即所有目标模块及其源码级传递模块依赖的并集。该包的模块/文件映射与命名地址解析记录在 framework/corpus-modules.json。

编译上下文有三个层次（各样本一致）：

1. 透明可执行依赖（Opaque/bodyless boundaries）：证明目标时其契约可见的、无函数体边界，AF-account-036的闭包为：

   • 0x1::account::exists_at
   • 0x1::error::canonical
   • 0x1::features::is_default_account_resource_enabled
   • 0x1::option::extract
   • 0x1::signer::borrow_address

2. 这些边界契约引用的传递性规范函数：

   • 0x1::account::spec_exists_at
   • 0x1::features::spec_is_enabled
   • 0x1::option::$borrow
   • 0x1::option::$is_none

3. 编译所需的传递性源码模块：从0x1::account_abstraction、0x1::aggregator一直到0x1::voting的 130 余个模块。这些模块只是编译上下文（compilation context），不是额外的推断目标——样本 README 对此有明确声明。

准备阶段与哈希锚定

样本的"任务化"通过preparation.patch（samples/AF-account-036/preparation.patch）实现。该补丁对共享包做两件事：

1. 新增任务描述文件.move-inference-task.json，其中记录了task_id、granularity、package_module_target、source_commit、source_path、目标函数列表、被调用函数依赖、规范函数依赖、传递函数依赖与传递模块依赖等完整元数据（schema_version: 3）。
2. 从account.spec.move中删除目标参考规范块——revoke_any_signer_capability的 1 个 spec 块被替换为空（见补丁中的@@ -539,14 +539,14 @@段落）。

准备过程的可复现性由两级 SHA-256 锚定：

• 共享包哈希1c41a4a754554758e1632217bb867a0dc8c622072f937edf1e1ef44adaf1f116：对应未打补丁的共享包树；
• 准备后树哈希1857df4f95bceaac4adc76c6be9b369604a0ee01abca0d01d149a868cd72d659：对应应用补丁后的任务工作区。

运行时的流程是：runner 复制共享包 → 应用 preparation.patch → 校验哈希一致 → 才把独立工作区交给 agent。可编辑路径被严格限制为仅两个文件：

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

account.move的可执行实现保持不变，只有 spec 被移除，这正是"只推断规范、不改变行为"的评测约束。

变异体评分：规范质量的客观检验

AF-account-036的评分材料位于 corpus-v1.2/mutants/AF-account-036/mutants.json（该语料库中持有变异体与评分变异体集合同一目录，且该集作为资格门禁（disqualification gate）在轮次后应用，见 spec-inference/README.md#run-a-round 中关于 corpus-v1.2 的--disqualification-mutants-root用法）。三个"本质变异体"（essential mutant）分别钉住参考规范的不同契约条款：

三个变异体均满足validated.outcome: "killed"且killed_by_reference: true——即参考规范能发现这些缺陷，变异体被参考规范"杀死"。这一设计的意义在于：如果 agent 生成的规范能够杀死（拒绝）这些变异体，就证明它达到了与参考规范等价的判别力；反之，若某个变异体在 agent 的规范下存活（不被拒绝），则该规范被判定为不够严格。

评分逻辑本身由 harness/score_round.py、harness/mutants.py 等实现，任务契约的模式定义见 schemas/mutants.schema.json。由于评分在轮次结束后单独进行，且 agent 与评分材料不共享挂载命名空间，可避免"先看到答案再作答"的泄漏。

如何阅读与复现该样本

要在本地理解或复现AF-account-036的完整评测路径，可按以下顺序阅读仓库内的材料：

1. 先读框架总览 spec-inference/README.md，掌握三工作流对比、轮次执行与评分流程；设计文档见 spec-inference/DESIGN.md。
2. 再读语料库说明 corpus-v1.2/README.md 与 manifest.json，了解 20 个样本的选取与哈希记录。
3. 聚焦本样本：README → preparation.patch → 共享包中的目标源码与参考规范 → mutants.json。
4. 对照主仓库中未经任务化的原始文件 account.move 与 account.spec.move，确认共享包与上游源码的一致性。

需要注意的适用范围：corpus-v1.2是"保留的框架语料库"（retained infrastructure），其变异体集作为门禁而非进行中反馈；评测运行还依赖固定的 Aptos Core 提交、固定的 SDK 版本（0.2.139）以及沙箱环境（bubblewrap + Landlock，见 sandbox/README.md），复现时需满足这些前提条件。

小结

AF-account-036是理解 Move 规范推断评测的极佳切片：它以 Aptos 框架中真实且安全敏感的revoke_any_signer_capability为对象，把"推断规范"这一开放任务转化为三个可机械验证的问题——账户缺失是否中止（aborts_if）、无授予是否中止（aborts_if）、授予是否被清空（ensures），并通过三个精心构造的本质变异体对这三条契约逐一检验。这种"以变异体为规范质量试金石"的评测思路，正是 MoveFlow 规范推断评测框架区别于单纯 Prover 验证通过率的核心所在，也为 AI 辅助 Move 开发中"如何客观评价 AI 生成的规范"提供了一个可复现、可审计的工程答案。

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