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粒度Granularityfunction原始源码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(); }从源码结构看该函数的行为可以归纳为三点契约状态变更state-transition通过mut Account[...]修改Account资源并将signer_capability_offer.for这个Optionaddress字段执行extract()即清空签名者能力授予。中止条件abort当账户的Account资源不存在或默认账户资源特性未启用时的等价检查时调用assert_account_resource_with_error中止当signer_capability_offer.for为None时Option::extract中止。正常结果normal-result正常返回后signer_capability_offer.for必为None。其中assert_account_resource_with_error是内联辅助函数见 account.move#L1069-L1078inline 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 !existsAccount(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 globalAccount(signer::address_of(account)); /// [high-level-req-7.4] aborts_if !existsAccount(signer::address_of(account)); let account_resource globalAccount(signer::address_of(account)); aborts_if !option::is_some(account_resource.signer_capability_offer.for); }注意参考规范中通过modifies声明了对globalAccount(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。编译上下文有三个层次各样本一致透明可执行依赖Opaque/bodyless boundaries证明目标时其契约可见的、无函数体边界AF-account-036的闭包为0x1::account::exists_at0x1::error::canonical0x1::features::is_default_account_resource_enabled0x1::option::extract0x1::signer::borrow_address这些边界契约引用的传递性规范函数0x1::account::spec_exists_at0x1::features::spec_is_enabled0x1::option::$borrow0x1::option::$is_none编译所需的传递性源码模块从0x1::account_abstraction、0x1::aggregator一直到0x1::voting的 130 余个模块。这些模块只是编译上下文compilation context不是额外的推断目标——样本 README 对此有明确声明。准备阶段与哈希锚定样本的任务化通过preparation.patchsamples/AF-account-036/preparation.patch实现。该补丁对共享包做两件事新增任务描述文件.move-inference-task.json其中记录了task_id、granularity、package_module_target、source_commit、source_path、目标函数列表、被调用函数依赖、规范函数依赖、传递函数依赖与传递模块依赖等完整元数据schema_version: 3。从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.movesources/AptosFramework/account/account.spec.moveaccount.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分别钉住参考规范的不同契约条款变异体 ID注入的缺陷契约类别钉住的规范条款AF-account-036-no-account-check把账户存在性断言替换为if (!existsAccount(offerer_addr)) { return };账户缺失时静默返回而非中止abortaborts_if !existsAccount(addr)AF-account-036-skip-when-none把无条件的extract()改为if (is_some) { extract() };无授予时跳过而不中止abortaborts_if !is_some(offer.for)AF-account-036-read-instead-of-extract把extract()替换为let _ *offer.for.borrow();只读不清空normal-resultensures is_none(offer.for)后置条件三个变异体均满足validated.outcome: killed且killed_by_reference: true——即参考规范能发现这些缺陷变异体被参考规范杀死。这一设计的意义在于如果 agent 生成的规范能够杀死拒绝这些变异体就证明它达到了与参考规范等价的判别力反之若某个变异体在 agent 的规范下存活不被拒绝则该规范被判定为不够严格。评分逻辑本身由 harness/score_round.py、harness/mutants.py 等实现任务契约的模式定义见 schemas/mutants.schema.json。由于评分在轮次结束后单独进行且 agent 与评分材料不共享挂载命名空间可避免先看到答案再作答的泄漏。如何阅读与复现该样本要在本地理解或复现AF-account-036的完整评测路径可按以下顺序阅读仓库内的材料先读框架总览 spec-inference/README.md掌握三工作流对比、轮次执行与评分流程设计文档见 spec-inference/DESIGN.md。再读语料库说明 corpus-v1.2/README.md 与 manifest.json了解 20 个样本的选取与哈希记录。聚焦本样本README → preparation.patch → 共享包中的目标源码与参考规范 → mutants.json。对照主仓库中未经任务化的原始文件 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考