企业官网建设流程全解析

Aptos Move Tutorial：用 basic_coin 示例掌握 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

本文基于 Aptos 官方教程 move-tutorial README 展开，完整继承其九个步骤（Step 0–8）的教学脉络：从编写第一个 Move 模块、添加单元测试，到设计并实现basic_coin代币模块、将其泛型化，最终使用 Move Prover 编写 MSL 形式化规格并验证。所有示例代码均来自仓库中step_x各目录的真实源码，读者可逐步对照复现，最终获得一套可编译、可测试、可形式化验证的 Move 开发工作流。

教程总览：九个步骤与自包含目录结构

该教程定位是“与特定网络无关”的 Move 语言与工具链入门：它不教如何使用 Aptos 框架或向网络提交交易，而是聚焦于编译（compile）、测试（test）、验证（prove）这三类本地工具操作。README 将其组织为九个步骤：

• Step 0：环境准备
• Step 1：编写第一个 Move 模块
• Step 2：为第一个模块添加单元测试
• Step 3：设计basic_coin模块的接口
• Step 4：实现basic_coin模块
• Step 5：为basic_coin编写并运行单元测试
• Step 6：把basic_coin模块泛型化
• Step 7：使用 Move Prover
• Step 8：为basic_coin编写形式化规格

关键的设计约定是：每个step_x目录都是自包含的。例如即使跳过了 Step 1–4，也可以直接进入 step_5 目录，因为此前步骤写的所有代码都已完整复制在该目录中。部分步骤还带有_sol后缀的解答目录（如 step_4_sol、step_5_sol、step_8_sol）。

仓库中还提供了一键校验脚本 test.sh：它维护两份目录清单——COMPILED（step_1、step_2、step_4、step_5、step_6、step_7、step_8 及其_sol变体）和TESTED（step_2 起至 step_8 的目录），分别对每个包执行aptos move compile与aptos move test（见 test.sh#L31-L44）。这也说明本教程示例在仓库 CI 层面是作为可编译、可测试的活代码维护的。

Step 0：环境准备

教程要求两样东西：

1. 本地副本：克隆 aptos-core 仓库后进入aptos-move/move-examples/move-tutorial目录，用ls确认能看到step_1 step_2 step_2_sol step_3 ...等子目录；
2. Aptos CLI：教程写作时使用的版本为aptos 1.0.7（aptos --version可确认）。若使用 IDE，README 推荐 CLion/IntelliJ，其对 Aptos Move 支持较好。

后续所有命令均假设工作目录位于move-tutorial下，路径均以此为基准。

Step 1：编写第一个 Move 模块

进入 step_1/basic_coin 目录，你会看到：

• sources/目录：存放该包全部 Move 代码（类比 Rust 的src/）；
• Move.toml：声明包名、版本与依赖（类比 Rust 的Cargo.toml）。本步骤的 Move.toml 极简，仅两行：

[package] name = "basic_coin" version = "0.0.0"

打开 first_module.move，完整源码只有 9 行：

module 0xCAFE::basic_coin { struct Coin has key { value: u64, } public entry fun mint(account: &signer, value: u64) { move_to(account, Coin { value }) } }

逐点解读：

• 模块与发布地址：module 0xCAFE::basic_coin声明了一个名为basic_coin的模块，绑定地址0xCAFE。模块是 Move 代码的构建块，地址即该模块唯一可发布的地址——也就是说basic_coin只能发布在0xCAFE下。
• 资源结构体：struct Coin has key { value: u64 }定义了携带value的Coin资源。has key表示Coin可充当全局存储的键；由于它没有copy/drop/store能力，Coin既不能被复制，也不能被意外丢弃，更不能作为嵌套字段存入其他资源——这从类型系统层面杜绝了“复制代币”或“丢失代币”的可能。
• mint函数：接收&signer引用（不可伪造的、代表对某地址控制权的令牌）和一个value，用move_to(account, Coin { value })把新铸造的Coin存入account地址下。注意源码中该函数标注为public entry，即可以作为交易入口函数直接调用。
• 编译：在包目录内执行aptos move compile。

进阶要点（README Advanced 部分）：

• 用aptos move init --name <pkg_name>可创建空 Move 包；
• Move.toml的[addresses]段支持命名地址，例如named_addr = "0xC0FFEE"，编译时对named_addr的不同取值可产出不同字节码，便于在不同地址下部署同名模块（本教程 Step 3 起大量使用）；
• Move 四种能力语义：copy（可复制）、drop（可丢弃）、store（可作为非键字段存入全局资源）、key（可作为全局存储的键）；
• 函数默认private，可选public、public(friend)；标注entry的函数可被作为交易调用；
• move_to是五个全局存储操作符之一（其余还包括move_from、exists、borrow_global、borrow_global_mut，后文都会用到）。

Step 2：为第一个模块添加单元测试

进入 step_2/basic_coin，用aptos move test运行测试。Move 单元测试与 Rust 的#[test]相似：普通 Move 函数加上#[test]注解即可。step_2 的 first_module.move 相比 Step 1 多了两处关键内容：

// Only included in compilation for testing. Similar to #[cfg(testing)] // in Rust. Imports the `Signer` module from the MoveStdlib package. #[test_only] use std::signer; ... // Declare a unit test. It takes a signer called `account` with an // address value of `0xC0FFEE`. #[test(account = @0xC0FFEE)] fun test_mint_10(account: &signer) acquires Coin { let addr = signer::address_of(account); mint(account, 10); assert!(borrow_global<Coin>(addr).value == 10, 0); }

要点：

• #[test(account = @0xC0FFEE)]：为account参数构造一个地址为0xC0FFEE的测试 signer；
• acquires Coin：声明本函数会访问全局存储中的Coin资源；
• assert!(borrow_global<Coin>(addr).value == 10, 0)：断言铸造后的资源value为 10，失败则测试失败。因为测试函数与Coin定义在同一模块，所以可以直接访问其私有字段；
• #[test_only]注解等价于 Rust 的#[cfg(testing)]：std::signer仅在测试编译时可见，不污染正式字节码。

README 给出的两道练习：

1. 把断言改成11使测试失败，并找出aptos move test的某个 flag 在测试失败时转储全局状态，输出形如：

   ┌── test_mint_10 ────── │ error[E11001]: test failure │ ... │ 24 │ assert!(borrow_global<Coin>(addr).value == 11, 0); │ │ ^^^^^ Test was not expected to abort but it aborted with 0 here │ ────── Storage state at point of failure ────── │ 0xc0ffee: │ => key 0xcafe::basic_coin::Coin { value: 10 }

2. 找到收集覆盖率信息的 flag，并用aptos move coverage命令查看覆盖率统计与源码级覆盖。

Step 3：设计basic_coin模块的接口与存储模型

step_3/basic_coin.move 只给出了模块骨架：两个资源结构体和四个公开函数的签名（函数体以..占位）：

module named_addr::basic_coin { struct Coin has store { value: u64 } struct Balance has key { coin: Coin } /// Publish an empty balance resource under `account`'s address. public fun publish_balance(account: &signer) { .. } /// Mint `amount` tokens to `mint_addr`. Mint must be approved by the module owner. public fun mint(module_owner: &signer, mint_addr: address, amount: u64) acquires Balance { .. } /// Returns the balance of `owner`. public fun balance_of(owner: address): u64 acquires Balance { .. } /// Transfers `amount` of tokens from `from` to `to`. public fun transfer(from: &signer, to: address, amount: u64) acquires Balance { .. } }

注意此时模块地址已改为named_addr（命名地址），Coin的能力也从key变为store——因为它将作为Balance的字段存在，Balance本身才是key。README 强调：这里的 coin/balance 接口仅用于演示 Move 概念，Aptos 网络实际使用的是一种更丰富的coin类型，属于框架的一部分。

全局存储模型

Move 模块本身没有独立存储，链上状态（全局存储）按地址索引，每个地址下挂模块（代码）与资源（值）。README 用 Rust 伪代码概括这一结构：

struct GlobalStorage { resources: Map<address, Map<ResourceType, ResourceValue>> modules: Map<address, Map<ModuleName, ModuleBytecode>> }

每个地址下每种资源类型至多一个值，因此“地址 → 余额”的映射天然由存储结构提供且类型安全。basic_coin正是利用这一点：用Balance资源表示每个地址持有的代币数量。

与 Solidity 的对比：在多数 ERC-20 合约中，余额保存在特定合约存储内的状态变量mapping(address => uint256)中；而 Move 中余额直接是地址下的资源，合约（模块）与状态（资源）的归属关系不同，这正是上图（diagrams/solidity_state.png）所刻画的区别。

进阶提示：只有带entry修饰的函数能被交易直接调用。若想从交易直接调用transfer，需把签名改为public entry fun transfer(from: signer, to: address, amount: u64) acquires Balance { ... }。

Step 4：实现basic_coin模块

step_4/basic_coin 目录已备好包工程，核心文件 basic_coin.move 在包目录内aptos move compile可编译。该版本的Move.toml（与 step_5 相同）展示了命名地址与依赖声明的完整形态：

[package] name = "basic_coin" version = "0.0.0" [addresses] named_addr = "0xCAFE" [dependencies.AptosStdlib] git = 'https://github.com/aptos-labs/aptos-framework.git' rev = 'main' subdir = 'aptos-stdlib'

模块开头声明了模块所有者与三个错误码（basic_coin.move#L5-L11）：

const MODULE_OWNER: address = @named_addr; const ENOT_MODULE_OWNER: u64 = 0; const EINSUFFICIENT_BALANCE: u64 = 1; const EALREADY_HAS_BALANCE: u64 = 2;

publish_balance：发布空余额资源

该方法用move_to在给定地址下发布Balance资源。任何地址在接收铸币或转账前必须先调用它（basic_coin.move#L24-L28）：

public fun publish_balance(account: &signer) { let empty_coin = Coin { value: 0 }; move_to(account, Balance { coin: empty_coin }); }

mint：仅模块所有者可铸造

public fun mint(module_owner: &signer, mint_addr: address, amount: u64) { // Only the owner of the module can initialize this module assert!(signer::address_of(module_owner) == MODULE_OWNER, ENOT_MODULE_OWNER); // Deposit `amount` of tokens to `mint_addr`'s balance deposit(mint_addr, Coin { value: amount }); }

assert!(<predicate>, <abort_code>)是 Move 的标准断言写法：谓词为假则以<abort_code>中止（abort）交易。Move 执行是事务性的——abort 之后无需任何回滚，该交易的所有变更都不会落盘。错误码可以自定义（如本例），也可以复用标准库error模块中定义的错误分类（标准库位于 move-stdlib）。

balance_of与transfer

读取余额使用只读全局存储操作符borrow_global，语法borrow_global<Balance>(owner).coin.value中，尖括号内是资源类型，其后依次是地址与字段访问路径（basic_coin.move#L40-L42）。转账由私有辅助函数withdraw加deposit组合而成（basic_coin.move#L45-L48、L51-L58）：

public fun transfer(from: &signer, to: address, amount: u64) acquires Balance { let check = withdraw(signer::address_of(from), amount); deposit(to, check); } fun withdraw(addr: address, amount: u64) : Coin acquires Balance { let balance = balance_of(addr); // balance must be greater than the withdraw amount assert!(balance >= amount, EINSUFFICIENT_BALANCE); let balance_ref = &mut borrow_global_mut<Balance>(addr).coin.value; *balance_ref = balance - amount; Coin { value: amount } }

withdraw先断言余额充足，再用borrow_global_mut拿到全局存储的可变引用，&mut创建指向Coin.value字段的可变引用，经引用修改余额后返回面额为amount的Coin；transfer再把这个Coin存入to的余额。

练习与解答

step_4 源码里留了两个 TODO（basic_coin.move#L25、L61-L68）：

1. 在publish_balance中加断言，检查account下尚不存在Balance资源；
2. 仿照withdraw实现deposit。

完整解答见 step_4_sol/basic_coin.move：publish_balance增加assert!(!exists<Balance>(signer::address_of(account)), EALREADY_HAS_BALANCE)（第 26 行），deposit通过borrow_global_mut把check中的value累加进余额（第 61-66 行）。附加思考题：向余额存入过多代币会发生什么？从解答代码*balance_ref = balance + value;看，u64加法溢出会触发 Move 的运行时检查导致交易 abort，这一点在 Step 8 的aborts_if balance + check_value > MAX_U64规格中会得到形式化印证。

Step 5：用单元测试全面覆盖basic_coin

在 step_5/basic_coin 目录执行aptos move test，期望看到 7 个测试全部通过（README 给出的输出形如Test result: OK. Total tests: 7; passed: 7; failed: 0）。对照 step_5 的 basic_coin.move 源码，7 个测试分别覆盖一种行为，并演示了多种测试注解的用法：

README 的练习：在basic_coin模块中写一个只有几行的balance_of_dne测试，验证对不存在Balance资源的地址调用balance_of会中止；解答在 step_5_sol 中。

Step 6：把basic_coin泛型化

Move 支持为结构体和函数引入类型参数，是编写可复用库模块的基石。step_6/basic_coin.move 将模块改造成泛型版本（L10-L16）：

struct Coin<phantom CoinType> has store { value: u64 } struct Balance<phantom CoinType> has key { coin: Coin<CoinType> }

• CoinType声明为phantom（幻影类型参数）：它不参与实际数据布局（Coin根本不用它，Balance仅以Coin<CoinType>形式携带），其作用是区分代币种类——Coin<MyCoinA>与Coin<MyCoinB>在类型层面互不兼容；
• withdraw相应变为fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance，函数体内所有资源访问都要显式实例化，如borrow_global_mut<Balance<CoinType>>(addr)。

更值得关注的是策略委托模式。step_6 的 mint 与 transfer 签名都带一个_witness: CoinType参数，且要求CoinType: drop：

public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance { let check = withdraw<CoinType>(signer::address_of(from), amount); deposit<CoinType>(to, check); }

witness（见证值）必须被调用方构造出来，而只有定义CoinType的模块才能构造它——因此铸造与转账策略天然收归代币类型的所有者模块。示例模块 my_odd_coin.move 演示了这一点：

struct MyOddCoin has drop {} public fun transfer(from: &signer, to: address, amount: u64) { // amount must be odd. assert!(amount % 2 == 1, ENOT_ODD); basic_coin::transfer<MyOddCoin>(from, to, amount, MyOddCoin {}); }

MyOddCoin是一个可drop的空结构体，my_odd_coin模块在调用通用basic_coin之前先断言转账数量必须为奇数，把“只能转奇数枚”的策略固化在类型所有者一侧。模块内附两个测试（L25-L45）：test_odd_success验证转账 7 枚后双方余额分别为 35 与 17；test_not_odd_failure用#[expected_failure]验证转账 8 枚必然失败。用 Step 2/5 学过的aptos move test即可运行。

Step 7：使用 Move Prover 检查中止条件

Move Prover 是针对 Move 智能合约的形式化验证工具：用户用 Move Specification Language（MSL）为函数声明属性，再由证明器静态检查。运行前需先安装 Move Prover 及其依赖工具。

step_7/basic_coin 在balance_of上只加了最小规格（README Step 7 所示）：

spec balance_of { pragma aborts_if_is_strict; }

spec balance_of {...}块包含balance_of的属性规格。pragma aborts_if_is_strict要求完整列举函数所有可能的中止条件——只要还有未覆盖的 abort 路径，证明器就报错。在包目录内执行：

aptos move prove

会输出（README 记录的报错）：

error: abort not covered by any of the `aborts_if` clauses ┌─ ./sources/basic_coin.move:38:5 │ 35 │ borrow_global<Balance<CoinType>>(owner).coin.value │ ------------- abort happened here with execution failure ... = owner = 0x29 = ABORTED

含义是：当owner名下不存在Balance<CoinType>资源时，borrow_global会 abort，而该条件尚未被任何aborts_if子句覆盖。补齐后（与 step_8 源码 L38-L41 的最终形态一致）：

spec balance_of { pragma aborts_if_is_strict; aborts_if !exists<Balance<CoinType>>(owner); }

再次aptos move prove应无验证错误。

Step 8：为basic_coin编写完整形式化规格

step_8 的 basic_coin.move 给出了withdraw、deposit、transfer三个方法的完整 MSL 规格，是学习 MSL 语法的最佳范本。

withdraw：let 绑定 + 双重中止条件 + 后置条件

spec withdraw { let balance = global<Balance<CoinType>>(addr).coin.value; aborts_if !exists<Balance<CoinType>>(addr); aborts_if balance < amount; let post balance_post = global<Balance<CoinType>>(addr).coin.value; ensures result == Coin<CoinType> { value: amount }; ensures balance_post == balance - amount; }

（对应源码 L72-L81）MSL 要点：

• spec 块内可用let为表达式命名：global<T>(address): T是内建函数，返回addr处资源T的值；exists<T>(address): bool判断该资源是否存在；
• 多个aborts_if子句之间是或的关系；在 strict 语义下必须穷举所有中止条件，否则报验证错误；若改用pragma aborts_if_is_partial，则条件组合只表示“在这些条件下函数会 abort”（不充分不排他）；
• let post balance_post = ...引入执行后的平衡值，两条ensures分别约束返回值（result是面额amount的Coin）与状态变化（余额减少amount）。

deposit：溢出条件也要写进规格

spec deposit { let balance = global<Balance<CoinType>>(addr).coin.value; let check_value = check.value; aborts_if !exists<Balance<CoinType>>(addr); aborts_if balance + check_value > MAX_U64; let post balance_post = global<Balance<CoinType>>(addr).coin.value; ensures balance_post == balance + check_value; }

（对应源码 L90-L99）第二条aborts_if正是 Step 4 附加思考题的形式化答案：当余额与存入值之和超过u64最大值MAX_U64时，加法溢出会使交易 abort。

transfer：由验证失败驱动的代码修正

transfer的规格（源码 L52-L62）断言前后余额的变化：

spec transfer { let addr_from = signer::address_of(from); let balance_from = global<Balance<CoinType>>(addr_from).coin.value; let balance_to = global<Balance<CoinType>>(to).coin.value; let post balance_from_post = global<Balance<CoinType>>(addr_from).coin.value; let post balance_to_post = global<Balance<CoinType>>(to).coin.value; ensures balance_from_post == balance_from - amount; ensures balance_to_post == balance_to + amount; }

证明器会报error: post-condition does not hold（指向ensures balance_from_post == balance_from - amount;）。根因：当addr_from == to（自己转给自己）时，两条ensures无法同时成立。教程的解法不是在 spec 里加条件，而是修代码——在transfer中新增断言assert!(from_addr != to, EEQUAL_ADDR);（源码 L45-L50，其中错误码EEQUAL_ADDR: u64 = 4定义于 L9），使等地址转账显式 abort，从而保证余额变化等式对一切非中止路径成立。这是一个典型的“形式化验证发现真实语义歧义”的示例。

练习

• 为transfer补全aborts_if条件；
• 为mint与publish_balance编写规格。

解答位于 step_8_sol。

关键文件索引

小结

这套教程的递进关系值得注意：Step 1–2 建立“编译 + 测试”的最小闭环；Step 3–5 通过一个有真实缺陷空间（越权铸造、重复发布、超额提现、资源缺失）的代币模块，把move_to/borrow_global/borrow_global_mut等全局存储操作符与#[test]/#[expected_failure]等测试注解用透；Step 6 用phantom类型参数与 witness 参数展示了泛型库模块的设计范式；Step 7–8 则从“中止条件穷举”过渡到完整的前置/后置条件规格，并演示了验证失败如何反向修正合约逻辑。由于每个step_x目录自包含，读者可以按自己的基础直接跳到任意一步，配合aptos move compile、aptos move test、aptos move prove三条命令本地复现全部结果。

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