企业官网建设流程全解析

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）会：

1. 拷贝该包；
2. 应用preparation.patch；
3. 校验结果哈希（Prepared tree SHA-256）后，才把独立工作区交给 Agent。

目标（Target）元数据

目标函数共 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_active）；
• transitive_called_function_dependencies与transitive_function_dependencies：传递闭包，覆盖big_ordered_map的 B 树内部操作、vector、option、table、storage_slots_allocator、ordered_map等上百个函数；
• transitive_module_dependencies：16 个传递依赖模块。

三、目标模块源码级剖析：native 交易的授权层

理解评测任务必须先理解目标模块本身。trading_native_capability.move的注释点明了其职责：native 交易存储的授权层——用TradingNativeCapability令牌门控写操作，用位于@aptos_experimental（0x7）的ExchangeRegistry决定谁能铸造令牌。治理方register/deny交易所，交易所每笔交易通过get_capability铸造一个能力令牌。

核心数据结构

/// Zero-sized value type for the `BigOrderedMap` sets (satisfies the /// map's constant-serialized-size requirement). struct Empty has copy, drop, store {} /// `store` so the exchange can hold it across transactions; not /// `copy`, so it can't 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: BigOrderedMap<address, Empty>, denied: BigOrderedMap<address, Empty>, }, }

设计要点（源码注释明确说明）：

• TradingNativeCapability只有store, drop而没有copy，因此不能复制，防止令牌被无限拷贝；
• 有效性（已注册、未被 deny、feature flag 开启）在每次写入时通过assert_valid重新检查，所以已存储的令牌会在治理方 deny 交易所的瞬间失效；
• ExchangeRegistry使用BigOrderedMap且以Empty零尺寸结构作为值，满足该映射常量序列化尺寸的要求；BigOrderedMap让每个条目独占一个 slot，对不同地址的写入在 block-STM 下互不争用。

错误码约定

注意错误码经error::permission_denied包装后，实际 abort code 为0x50000 + 码值——源码测试中的0x50001/0x50002/0x50003分别对应 feature 未启用、未注册、已被 deny。

8 个目标函数的执行语义

1. init_module(deployer)：部署初始化。断言signer::address_of(deployer) == @aptos_experimental，否则以ENOT_DEPLOYER拒绝；若注册表不存在则用两个空BigOrderedMap初始化ExchangeRegistry::V1。由 vm-genesis 调用（重发布时由 VM 调用）。
2. register(framework, exchange)：仅治理方可调用（system_addresses::assert_aptos_framework），且要求TRADING_NATIVE已启用；幂等地将交易所加入registered。
3. assert_active(addr)：内部辅助函数，三重检查——feature 已启用、地址已注册、地址未被 deny，任一不满足即 abort。
4. assert_valid(cap)：公开函数，每次 native 持仓写入前调用，转发到assert_active(cap.exchange)，实现"存留令牌即时失效"。
5. deny(framework, exchange)：仅治理方可调用，幂等地将交易所加入denied。刻意不检查TRADING_NATIVEflag——即使 flag 关闭，治理方也必须能锁定交易所。
6. get_capability(exchange)：为已注册且未被 deny 的交易所铸造能力令牌，内部先执行assert_active(addr)，返回TradingNativeCapability { exchange: addr }。
7. is_denied(exchange)：查询denied集合是否包含该地址。
8. reenable(framework, exchange)：仅治理方可调用，幂等地从denied集合移除地址，恢复交易所资格；与deny一样不检查 flag。

测试用例佐证语义

源码内置 9 个测试（#[test]）直接印证上述语义，可作为推断任务的"行为真值"：

• test_register_then_get_capability：注册后可正常铸造且exchange(&cap) == addr；
• test_get_capability_unregistered_aborts：未注册则 abort0x50002；
• test_denied_exchange_cannot_get_capability：deny 后is_denied为真且铸造 abort0x50003；
• test_reenable_restores_capability：deny 再 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 或关 flag，assert_valid立即 abort（0x50003/0x50001）。

四、参考规范：推断任务的"标准答案"

参考规范文件trading_native_capability.spec.move定义了每个目标函数应有的规范合约。注意：这份参考规范在准备阶段会被补丁全部移除（见下节），它存在的意义是供评测打分时比对。

规范的核心是两条共享辅助规范函数：

spec fun spec_registry(): ExchangeRegistry { global<ExchangeRegistry>(@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) || !exists<ExchangeRegistry>(@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都直接引用它——这是"行为谓词复用"的典型写法。

各目标函数的规范要点：

这些规范演示了 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.move：

• register（1 块）
• init_module（1 块）
• assert_active（1 块）
• assert_valid（1 块）
• deny（1 块）
• get_capability（1 块）
• is_denied（1 块）
• reenable（1 块）

补丁同时新增任务描述符.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属于以0x7（aptos_experimental，Aptos 交易/订单簿实验模块）为目标的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.md；v1.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