Aptos Move 规范推断样本 AF-aptos-coin-010：模块级 aptos_coin 验证任务的构造与还原

Aptos Move 规范推断样本 AF-aptos-coin-010模块级 aptos_coin 验证任务的构造与还原【免费下载链接】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-coreAF-aptos-coin-010 是 Aptos 仓库 aptos-move/flow/evaluation/spec-inference 中 Move 规范推断评估语料库corpus-v1.2下的一个样本任务。它把 Aptos 核心模块0x1::aptos_coin包装成一个配方recipe式任务运行时复制共享的 framework 包、应用 preparation.patch、校验哈希后交给独立工作区中的智能体要求其仅凭可编辑的两个源文件重新推断出该模块的参考规范。读完本文你将掌握该样本的目标定义、编译上下文、依赖闭包、准备preparation变换细节以及如何把它与真实源码、Prover 规范相互印证。样本概览一个可复现的模块级推断任务整个语料库只保存一份可编辑的 Move 包framework/154 个模块、257 个 Move 源/规范文件每个样本都是覆盖在其上的小配方运行时控制器controller复制共享包、应用样本自己的 preparation patch只删除该目标的参考规范并加入任务描述符不存在逐样本的框架快照见 corpus-v1.2/README.md。AF-aptos-coin-010 正是这种机制的一个典型实例Target0x1::aptos_coinGranularitymodule模块级需为整个模块的多个目标函数写规范Original sourceaptos-move/framework/aptos-framework/sources/aptos_coin.moveSource inside the shared packagesources/AptosFramework/aptos_coin.moveSource rootaptos-move/framework/aptos-frameworkAptos Core commit950e413e46090d2056740c36dd7a77b1764b6936Shared package SHA-2561c41a4a754554758e1632217bb867a0dc8c622072f937edf1e1ef44adaf1f116Prepared tree SHA-256f042541e1e8c5364ea4cd62ae64486fbe81e9442d950ce0dbb375679fcdc328eRequired contract categoriesnormal-result、abort、state-transition、frame、loop-invariant任务 ID 中的AF前缀表示目标属于 Aptos Framework0x1010是该集合内的序号同语料库中还有针对0x7AptosExperimental 模块前缀AX的样本如 AF-account-025 的function粒度任务。从 manifest.json 与 metadata/selection.json 可查看完整的 20 个样本选择记录与哈希。目标函数与必须覆盖的合约类别本样本要求为以下三个函数推断规范函数角色initialize仅在创世期间调用初始化 APT 币断言框架地址、调用coin::initialize、move_to存放MintCapStore、销毁冻结能力并返回烧毁/铸造能力destroy_mint_cap仅在创世期间调用销毁 Aptos 框架账户的铸造能力find_delegation在Delegations中线性查找某地址的委托下标返回Optionu64required_contract_categories要求推断结果覆盖五类合约normal-result正常返回值的ensures、abortaborts_if、state-transition全局状态写入、frame栈帧/借用框架相关主要用于证明器的模块级验证、loop-invariant循环不变量。在 schemas/task-recipe.schema.json 中可以看到这些类别被定义为required_contract_categories的枚举且minItems: 1、uniqueItems: true——这是一个结构化任务配方的一部分该 schema 还要求schema_version、source_commit、pristine_sha256、prepared_sha256、preparation_patch_sha256等字段确保任务可复现且可审计。编译上下文共享包与模块/文件映射共享包framework/包含目标模块与其完整源码级传递模块依赖的并集。其模块/文件映射与已解析命名地址记录在 framework/corpus-modules.json 中。README 明确声明除本样本目标外的其他模块只是编译上下文不是额外的推断目标——这正是保证评估公平性的关键设计避免智能体被海量目标淹没同时保证包可独立编译并被 Move Prover 处理。包的命名地址配置见 framework/Move.tomlaptos_framework 0x1、aptos_std 0x1、std 0x1、core_resources 0xA550C18、aptos_experimental 0x7、aptos_trading 0x5等。其中core_resources地址在find_delegation/destroy_mint_cap的规范中会以core_resources形式出现。不透明边界opaque/bodyless boundaries证明本目标时其合约可见的不透明无函数体边界会暴露给智能体这些边界通过透明可执行被调函数与可达合约引用的行为谓词遍历得到。README 列出的 10 个边界函数包括0x1::coin::coin_address0x1::error::canonical0x1::option::none/0x1::option::some0x1::optional_aggregator::new0x1::signer::borrow_address0x1::string::utf80x1::system_addresses::assert_aptos_framework0x1::vector::borrow/0x1::vector::length这些函数在真实源码中均有对应实现system_addresses::assert_aptos_framework位于 system_addresses.moveinitialize与destroy_mint_cap的第一行都调用它做框架地址断言string::utf8与string::spec_internal_check_utf8位于 string.move。传递规范函数依赖边界合约引用的传递规范函数spec function共有 16 个例如0x1::aggregator::spec_aggregator_get_val/spec_get_limit聚合器取值与上限optional_aggregator相关0x1::coin::spec_fun_supply_trackedmonitor_supply标志的规范投影0x1::option::$borrow/$is_some/spec_none/spec_somefind_delegation的Option结果0x1::optional_aggregator::$is_parallelizable/optional_aggregator_limit/optional_aggregator_value0x1::signer::$address_of/$borrow_address0x1::string::spec_internal_check_utf8/spec_utf8initialize中bAptos Coin、bAPT的 UTF-8 校验0x1::type_info::$type_of/spec_is_struct它们与corpus-modules.json中记录的模块映射一一对应智能体可在共享包内查到这些 spec 函数的定义以理解边界行为。传递源模块依赖编译所需README 列出了 94 个传递源模块覆盖0x1::account、0x1::coin、0x1::aptos_governance、0x1::stake、0x1::table、0x1::type_info、0x1::vector等。这些模块以源码形式存在于共享包sources/AptosFramework/、sources/AptosStdlib/、sources/MoveStdlib/等目录智能体可以自由阅读它们来理解被调用函数的行为但不能编辑它们。这种全量依赖可见、仅目标可编辑的布局与 prepare.py 等 harness 脚本的职责一致——准备阶段负责生成任务配方并校验快照哈希。Preparation参考规范被剥离后的可编辑面准备变换由 preparation.patch 定义它是可复现的。其要点是新增任务描述符.move-inference-task.json包含task_id、granularity: module、package_module_target: 0x1::aptos_coin、source_commit、target_functions、called_function_dependencies、spec_function_dependencies、transitive_called_function_dependencies、transitive_function_dependencies、transitive_module_dependencies等字段schema_version: 3。该 JSON 就是 README 中各类依赖清单的结构化形式。剥离参考规范sources/AptosFramework/aptos_coin.spec.move删除initialize1 个 spec 块、destroy_mint_cap1 个 spec 块、find_delegation1 个 spec 块sources/AptosFramework/aptos_coin.move删除find_delegation内的 1 个内联 spec 块循环不变量共 3 条invariant。被删除的循环不变量原文来自补丁的 diff 上下文为while (i len) { let element delegations.borrow(i); if (element.to addr) { index option::some(i); break }; i 1; } spec { invariant i len; invariant option::is_none(index); invariant forall k in 0..i: delegations[k].to ! addr; }; index这三条不变量分别刻画下标不越界、找到前index始终为none、以及前i个元素都未命中addr。required_contract_categories中的loop-invariant正是要求智能体在推断时重新给出这类约束。限制可编辑路径智能体只能编辑sources/AptosFramework/aptos_coin.movesources/AptosFramework/aptos_coin.spec.move其余 265 个 Move 文件与配置文件均为只读编译上下文。注意补丁还保留了一个细节configure_accounts_for_test、mint、delegate_mint_capability、claim_mint_capability的 spec 块含pragma verify false不在删除之列因为它们属于测试专用函数不需要验证。而spec module { pragma verify true; pragma aborts_if_is_partial; }也被保留表明该模块整体参与验证且中止条件是部分规格。剥离后的目标源码形态应用补丁后智能体看到的 aptos_coin.move 中find_delegation的循环 spec 块被替换为空语句aptos_coin.spec.move中三个目标的 spec 块被清空。智能体需要从以下可执行实现中重新推断契约initializesystem_addresses::assert_aptos_framework(aptos_framework)→coin::initializeAptosCoin(..., bAptos Coin, bAPT, 8 /* decimals */, true /* monitor_supply */)→move_to(aptos_framework, MintCapStore { mint_cap })→coin::destroy_freeze_cap(freeze_cap)→ 返回(burn_cap, mint_cap)destroy_mint_capassert_aptos_framework→move_fromMintCapStore(aptos_framework)解构出mint_cap→coin::destroy_mint_cap(mint_cap)find_delegationborrow_globalDelegations(core_resources).inner线性扫描delegations比较.to addr命中即option::some(i)并break。与真实源码的对应关系本样本的参考规范与真实仓库完全一致。将共享包中的 aptos_coin.spec.move 与仓库原始 aptos_coin.spec.move 对照可见模块头部记录了 4 条高层需求high-level-reqAPT 必须在创世期间初始化、APT 币只能创建一次、铸造能力应可转移/复制/销毁、未注册币种的用户操作应失败。其中需求 1 和 3 通过[high-level-req-1]、[high-level-req-3]注释与initialize的ensures条款挂钩。initialize的参考规范见补丁中被删除的 diff 段包含let addr signer::address_of(aptos_framework)后aborts_if addr ! aptos_framework、aborts_if !string::spec_internal_check_utf8(bAptos Coin)、aborts_if !string::spec_internal_check_utf8(bAPT)、aborts_if existsMintCapStore(addr)、aborts_if existscoin::CoinInfoAptosCoin(addr)ensures existsMintCapStore(addr)、ensures globalMintCapStore(addr).mint_cap MintCapabilityAptosCoin {}、ensures existscoin::CoinInfoAptosCoin(addr)、ensures result_1 BurnCapabilityAptosCoin {}、ensures result_2 MintCapabilityAptosCoin {}。destroy_mint_cap的参考规范aborts_if addr ! aptos_framework、aborts_if !existsMintCapStore(aptos_framework)。find_delegation的参考规范aborts_if !existsDelegations(core_resources)并给出三条ensures刻画is_some/is_none情形结果下标合法且指向目标地址、结果之前无重复目标、none时全表无目标。这组参考规范正是评估中被隐藏的答案智能体推断出的规范将1在 Move Prover 下验证通过2在变异测试mutant scoring下拒绝错误代码见 corpus-v1.2/README.md 与 README.md 中关于score_round与--disqualification-mutants-root corpus-v1.2/mutants的说明。验证与运行方式本样本由 corpus-v1.2 的调度与运行管线驱动。总体运行说明见 spec-inference/README.md该文件是 runbook如何运行而非如何工作设计动机见 DESIGN.md编辑规范见 CLAUDE.md。与样本直接相关的要点校验语料可复现corpus-v1.2 针对 commit950e413e46090d2056740c36dd7a77b1764b6936生成每个样本的源树哈希一致manifest.json的corpus_status是轮次就绪状态的权威来源。调度只有screening_status ready的样本才会进入调度本样本的筛选证据在 screening/results/AF-aptos-coin-010.json元数据在 metadata/mutation-validation-005/AF-aptos-coin-010.json变异与评分数据分别在 mutants/AF-aptos-coin-010/ 与 mutants-scoring/AF-aptos-coin-010/。评分corpus-v1.2 采用扣留式变异集--disqualification-mutants-root corpus-v1.2/mutants运行时不提供给智能体作为反驳素材轮次结束后作为门槛——若某变异存活则反驳对应合约并取消该轮成绩而非仅降低分数。智能体工作区通过harness/下的脚本prepare.py、pilot.py、controller.py 等在沙箱中准备、调度、运行与审计沙箱威胁模型与两层隔离见 sandbox/README.md。小结AF-aptos-coin-010 展示了 spec-inference 语料库共享包 覆盖式配方的核心模式以模块0x1::aptos_coin为粒度剥离initialize、destroy_mint_cap、find_delegation三个目标的参考规范含find_delegation的循环不变量保留全部 94 个传递编译依赖与 10 个不透明边界、16 个传递规范函数作为上下文最终以两个 SHA-256共享包与准备后树保证任何实验臂拿到同一份字节。读者若要复现该任务可对照 preparation.patch 手工还原可编辑面再以 aptos_coin.spec.move 作为参考答案在 Move Prover 下验证自己推断的规范是否与参考规范在正常结果、中止条件、状态转换、框架与循环不变量五个维度上等价。【免费下载链接】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），仅供参考