Aptos Move 规范推断评测样本解析以 trading_native_capability 模块为目标的 AX-trading-native-capability-010【免费下载链接】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目录下的 Move 规范推断Specification Inference评测语料库深入解析样本AX-trading-native-capability-010。该样本以 Aptos 实验性框架aptos-experimental中的0x7::trading_native_capability模块为推断目标完整记录了目标函数清单、编译上下文、不透明依赖边界、参考规范与可复现的准备preparation流程。读完本文你将理解Aptos 如何用语料库 样本配方 参考规范 变异体打分的方式评测 Move Prover 规范推断能力以及一个真实交易权限控制模块的源码、规范与评测任务的对应关系。一、评测语料库背景样本从何而来该样本属于aptos-move/flow/evaluation/spec-inference/corpus-v1.2语料库v1.2 保留框架语料与构建管线v3.2 为基准评测语料。根据 corpus-v1.2/README.md语料库从 Aptos Core 提交950e413e46090d2056740c36dd7a77b1764b6936构建共收录 20 个样本每个样本的目标要么是单个函数function粒度要么是整模块module粒度。语料库的关键设计是共享可编辑框架整个语料只存一个 Move 包——framework/内含 154 个模块、257 个 Move 源/规范文件是所有目标及其源码级传递依赖的并集命名地址、原始路径与模块到文件的精确映射记录在framework/corpus-modules.json每个样本只是一份轻量覆盖配方overlay recipe运行时控制器拷贝共享包、应用样本的准备补丁仅移除该目标的参考规范并写入任务描述符不存在逐样本的框架快照。AX-trading-native-capability-010正是这 20 个样本之一同时也是 v1.2 语料中少数几个以整模块为粒度的任务其余为函数粒度参见 samples 清单。二、样本配方一份任务说明书的结构样本 README即本任务核心文档位于 samples/AX-trading-native-capability-010/README.md其结构即评测任务的标准元数据模板由以下几个部分构成。配方机制Recipe样本是对语料库唯一可编辑包framework/的覆盖配方。运行器runner会拷贝该包应用preparation.patch校验结果哈希Prepared tree SHA-256后才把独立工作区交给 Agent。目标Target元数据字段值目标0x7::trading_native_capability粒度module整模块推断原始源码aptos-move/framework/aptos-experimental/sources/trading/position/trading_native_capability.move共享包内路径sources/AptosExperimental/trading/position/trading_native_capability.move源根aptos-move/framework/aptos-experimentalAptos Core 提交950e413e46090d2056740c36dd7a77b1764b6936共享包 SHA-2561c41a4a754554758e1632217bb867a0dc8c622072f937edf1e1ef44adaf1f116准备后树 SHA-256ccb2a50785e3284c2c94494d59180901c5b2a9ff30aa3d1c6ea8477f54cd72ef必需合约类别normal-result、abort、state-transition、frame目标函数共 8 个register、init_module、assert_active、assert_valid、deny、get_capability、is_denied、reenable。这些元数据同时被结构化写入准备补丁新增的任务描述符.move-inference-task.json见 preparation.patch其中schema_version: 3、task_id、granularity、package_module_target、source_commit、target_functions与 README 一一对应。.move-inference-task.json还额外记录了三级依赖清单called_function_dependencies直接调用的函数9 个如0x1::big_ordered_map::add、0x1::system_addresses::assert_aptos_framework、0x7::trading_native_capability::assert_activetransitive_called_function_dependencies与transitive_function_dependencies传递闭包覆盖big_ordered_map的 B 树内部操作、vector、option、table、storage_slots_allocator、ordered_map等上百个函数transitive_module_dependencies16 个传递依赖模块。三、目标模块源码级剖析native 交易的授权层理解评测任务必须先理解目标模块本身。trading_native_capability.move的注释点明了其职责native 交易存储的授权层——用TradingNativeCapability令牌门控写操作用位于aptos_experimental0x7的ExchangeRegistry决定谁能铸造令牌。治理方register/deny交易所交易所每笔交易通过get_capability铸造一个能力令牌。核心数据结构/// Zero-sized value type for the BigOrderedMap sets (satisfies the /// maps constant-serialized-size requirement). struct Empty has copy, drop, store {} /// store so the exchange can hold it across transactions; not /// copy, so it cant be duplicated. struct TradingNativeCapability has store, drop { exchange: address, } /// Registered exchanges and the governance deny-list, at /// aptos_experimental. enum ExchangeRegistry has key { V1 { registered: BigOrderedMapaddress, Empty, denied: BigOrderedMapaddress, Empty, }, }设计要点源码注释明确说明TradingNativeCapability只有store, drop而没有copy因此不能复制防止令牌被无限拷贝有效性已注册、未被 deny、feature flag 开启在每次写入时通过assert_valid重新检查所以已存储的令牌会在治理方 deny 交易所的瞬间失效ExchangeRegistry使用BigOrderedMap且以Empty零尺寸结构作为值满足该映射常量序列化尺寸的要求BigOrderedMap让每个条目独占一个 slot对不同地址的写入在 block-STM 下互不争用。错误码约定常量值含义EFEATURE_DISABLED1链上未启用TRADING_NATIVEfeatureEEXCHANGE_NOT_REGISTERED2交易所尚未注册EEXCHANGE_DENIED3交易所已被治理方禁用ENOT_DEPLOYER4init_module的调用者不是aptos_experimental注意错误码经error::permission_denied包装后实际 abort code 为0x50000 码值——源码测试中的0x50001/0x50002/0x50003分别对应 feature 未启用、未注册、已被 deny。8 个目标函数的执行语义init_module(deployer)部署初始化。断言signer::address_of(deployer) aptos_experimental否则以ENOT_DEPLOYER拒绝若注册表不存在则用两个空BigOrderedMap初始化ExchangeRegistry::V1。由 vm-genesis 调用重发布时由 VM 调用。register(framework, exchange)仅治理方可调用system_addresses::assert_aptos_framework且要求TRADING_NATIVE已启用幂等地将交易所加入registered。assert_active(addr)内部辅助函数三重检查——feature 已启用、地址已注册、地址未被 deny任一不满足即 abort。assert_valid(cap)公开函数每次 native 持仓写入前调用转发到assert_active(cap.exchange)实现存留令牌即时失效。deny(framework, exchange)仅治理方可调用幂等地将交易所加入denied。刻意不检查TRADING_NATIVEflag——即使 flag 关闭治理方也必须能锁定交易所。get_capability(exchange)为已注册且未被 deny 的交易所铸造能力令牌内部先执行assert_active(addr)返回TradingNativeCapability { exchange: addr }。is_denied(exchange)查询denied集合是否包含该地址。reenable(framework, exchange)仅治理方可调用幂等地从denied集合移除地址恢复交易所资格与deny一样不检查 flag。测试用例佐证语义源码内置 9 个测试#[test]直接印证上述语义可作为推断任务的行为真值test_register_then_get_capability注册后可正常铸造且exchange(cap) addrtest_get_capability_unregistered_aborts未注册则 abort0x50002test_denied_exchange_cannot_get_capabilitydeny 后is_denied为真且铸造 abort0x50003test_reenable_restores_capabilitydeny 再 reenable 后恢复铸造能力test_get_capability_requires_trading_native_flag先注册再关闭 flag铸造 abort0x50001总开关 kill-switch 生效test_assert_valid_passes_when_active活跃状态下assert_valid通过test_held_cap_invalidated_by_deny/test_held_cap_invalidated_by_flag_off持有令牌后 deny 或关 flagassert_valid立即 abort0x50003/0x50001。四、参考规范推断任务的标准答案参考规范文件trading_native_capability.spec.move定义了每个目标函数应有的规范合约。注意这份参考规范在准备阶段会被补丁全部移除见下节它存在的意义是供评测打分时比对。规范的核心是两条共享辅助规范函数spec fun spec_registry(): ExchangeRegistry { globalExchangeRegistry(aptos_experimental) } /// The feature flag, registration and denial checks every capability use /// shares. spec fun spec_active_aborts(addr: address): bool { !features::spec_is_enabled(TRADING_NATIVE) || !existsExchangeRegistry(aptos_experimental) || !big_ordered_map::spec_contains_key(spec_registry().registered, addr) || big_ordered_map::spec_contains_key(spec_registry().denied, addr) }spec_active_aborts用一个布尔表达式把assert_active的三种 abort 条件统一建模所有能力相关函数assert_active、get_capability、assert_valid的aborts_if都直接引用它——这是行为谓词复用的典型写法。各目标函数的规范要点函数pragmaaborts_if关键条件ensures关键性质init_moduleopaque部署者不是aptos_experimental注册表存在已存在则不变新建则两个集合长度为 0is_deniedopaque注册表不存在返回值 denied包含该地址registeropaque调用者不是aptos_frameworkflag 关闭注册表不存在registered包含该地址denied不变registered按幂等语义更新已存在则不变否则spec_set加入assert_activeopaquespec_active_aborts(addr)—get_capabilityopaquespec_active_aborts(signer::address_of(exchange))返回值 TradingNativeCapability { exchange: signer::address_of(exchange) }assert_validopaquespec_active_aborts(cap.exchange)—denyopaque调用者不是aptos_framework注册表不存在denied包含该地址registered不变denied按幂等语义更新reenableopaque调用者不是aptos_framework注册表不存在denied不包含该地址registered不变denied按幂等语义移除exchangeopaque永不 abort返回值 cap.exchange这些规范演示了 Move Prover 规范语言spec 块的核心要素pragma opaque将函数体视为黑盒、仅按合约推理、aborts_if中止条件、modifies全局状态修改面、ensures后置条件含old()与蕴含、以及spec_*辅助函数对行为谓词的抽取。五、编译上下文依赖闭包的组成样本 README 的Compilation context一节说明共享包包含目标模块与其完整源码级传递模块依赖的并集模块/文件映射与解析后的命名地址记录在framework/corpus-modules.json。除本样本目标之外的其他模块只是编译上下文compilation context不是额外推断目标。不透明/无函数体边界Opaque boundaries证明本目标时可见合约的边界共 9 个其闭包遍历了透明的可执行被调用者transparent executable callees与被触及合约中引用的行为谓词0x1::big_ordered_map::add / contains / new / remove 0x1::error::canonical 0x1::features::is_enabled 0x1::signer::borrow_address 0x1::system_addresses::assert_aptos_framework 0x7::trading_native_capability::assert_active这些边界函数以有合约、无函数体的形式参与证明恰好对应模块中使用的库能力BigOrderedMap的增删查、错误构造、feature 查询、signer 取地址与系统地址校验。边界合约引用的传递规范函数0x1::big_ordered_map::spec_contains_key 0x1::features::spec_is_enabled 0x1::signer::$address_of 0x1::signer::$borrow_address 0x7::trading_native_capability::spec_active_aborts 0x7::trading_native_capability::spec_registry注意最后两项是目标模块自身的spec_*辅助函数——即使函数体在 Agent 视角被移除参考规范中的行为谓词依然作为边界合约的依赖参与证明这解释了为什么spec_active_aborts/spec_registry会出现在依赖清单里。编译所需的传递源码模块共 16 个模块bcs、big_ordered_map、cmp、error、features、fixed_point32、math64、mem、option、ordered_map、signer、storage_slots_allocator、system_addresses、table、table_with_length、vector。它们与.move-inference-task.json中的transitive_module_dependencies完全一致可在共享包的sources/下逐一找到如AptosFramework/datastructures/big_ordered_map.move、MoveStdlib/features.move、AptosStdlib/data_structures/storage_slots_allocator.move等。六、准备流程可复现的去参考化变换准备阶段的核心原则是可执行的 Move 实现保持不变仅移除 Agent 可见源码中的目标参考规范块。根据 preparation.patch共移除 8 个规范块全部位于sources/AptosExperimental/trading/position/trading_native_capability.spec.moveregister1 块init_module1 块assert_active1 块assert_valid1 块deny1 块get_capability1 块is_denied1 块reenable1 块补丁同时新增任务描述符.move-inference-task.json并将规范文件中被移除的块替换为空白行以保持行号/结构可读。补丁保留了spec exchange与两条spec_*辅助函数spec_registry、spec_active_aborts——它们是证明的公共基础设施不属于单函数目标块。补丁后的约束十分明确The agent may edit only:sources/AptosExperimental/trading/position/trading_native_capability.move即 Agent 只能编辑目标模块的可执行源码文件不得改动依赖模块、不得修改任务描述符这保证了不同实验臂arm在同一任务上面对完全相同的源码哈希README 明确每个样本对每个实验臂提供相同的源码哈希治疗方案相关的技能与工具单独存放。包配置Move.toml声明包名InferenceCorpusFramework、版本1.0.0并解析命名地址aptos_experimental 0x7、aptos_framework 0x1、aptos_trading 0x5、Extensions 0x1、std 0x1等——这正是 README 中0x7::trading_native_capability前缀的来源。Prover.toml声明borrow_natives [storage_slot::borrow_storage_slot_resource_mut]配置 Move Prover 对存储槽原生函数的借用建模。七、评测定位该样本在语料中的角色从 corpus-v1.2 样本总表看AX-trading-native-capability-010属于以0x7aptos_experimentalAptos 交易/订单簿实验模块为目标的AX-*系列之一同系列还包括AX-bulk-order-book-009、AX-order-book-006、AX-native-position-types-005等。该样本的评测价值体现在模块级粒度要求 Agent 一次性为 8 个函数含内部辅助函数assert_active给出完整规范比单函数任务更能考察对模块内共享行为谓词spec_active_aborts的抽取能力幂等治理语义register/deny/reenable的ensures需要表达集合按幂等语义更新的条件式if contains ... else spec_set/spec_remove对规范表达能力要求高两类 abort 来源并存既有治理方身份校验aptos_framework/aptos_experimental又有 feature flag 与集合成员检查覆盖normal-result、abort、state-transition、frame四类必需合约类别立即失效性质assert_valid的语义存留令牌被 deny 后即时失效对状态变迁类规范是很好的测试点。整个评测框架的完整方法论三种工作流对比、打分方式、变异体拒绝检测等参见 spec-inference/README.md 与 DESIGN.mdv1.2 语料的筛选状态与兼容性证据记录在corpus-v1.2/screening/目录。结语AX-trading-native-capability-010是理解 Aptos Move 规范推断评测管线的一块理想样本它用一份轻量 README 串联起真实框架模块源码 → 参考规范 → 依赖闭包 → 去参考化补丁 → 任务描述符的完整链路。透过它可以看到评测系统的目标不是让 Agent 凭空写规范而是在严格控制源码哈希、只允许编辑单个文件、依赖边界合约完全可见的前提下衡量推断出的规范能否通过 Prover 验证、能否拒绝错误代码变异体。对希望深入 Move Prover 规范编写或复现该评测管线的读者建议按 spec-inference/README.md 的 Runbook 顺序从语料校验、插件渲染、调度到打分逐步运行。【免费下载链接】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），仅供参考