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 ProverStep 8为basic_coin编写形式化规格关键的设计约定是每个step_x目录都是自包含的。例如即使跳过了 Step 1–4也可以直接进入 step_5 目录因为此前步骤写的所有代码都已完整复制在该目录中。部分步骤还带有_sol后缀的解答目录如 step_4_sol、step_5_sol、step_8_sol。仓库中还提供了一键校验脚本 test.sh它维护两份目录清单——COMPILEDstep_1、step_2、step_4、step_5、step_6、step_7、step_8 及其_sol变体和TESTEDstep_2 起至 step_8 的目录分别对每个包执行aptos move compile与aptos move test见 test.sh#L31-L44。这也说明本教程示例在仓库 CI 层面是作为可编译、可测试的活代码维护的。Step 0环境准备教程要求两样东西本地副本克隆 aptos-core 仓库后进入aptos-move/move-examples/move-tutorial目录用ls确认能看到step_1 step_2 step_2_sol step_3 ...等子目录Aptos CLI教程写作时使用的版本为aptos 1.0.7aptos --version可确认。若使用 IDEREADME 推荐 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_globalCoin(addr).value 10, 0); }要点#[test(account 0xC0FFEE)]为account参数构造一个地址为0xC0FFEE的测试 signeracquires Coin声明本函数会访问全局存储中的Coin资源assert!(borrow_globalCoin(addr).value 10, 0)断言铸造后的资源value为 10失败则测试失败。因为测试函数与Coin定义在同一模块所以可以直接访问其私有字段#[test_only]注解等价于 Rust 的#[cfg(testing)]std::signer仅在测试编译时可见不污染正式字节码。README 给出的两道练习把断言改成11使测试失败并找出aptos move test的某个 flag 在测试失败时转储全局状态输出形如┌── test_mint_10 ────── │ error[E11001]: test failure │ ... │ 24 │ assert!(borrow_globalCoin(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 }找到收集覆盖率信息的 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 accounts 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: Mapaddress, MapResourceType, ResourceValue modules: Mapaddress, MapModuleName, 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-L11const 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-L28public 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_addrs 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_globalBalance(owner).coin.value中尖括号内是资源类型其后依次是地址与字段访问路径basic_coin.move#L40-L42。转账由私有辅助函数withdraw加deposit组合而成basic_coin.move#L45-L48、L51-L58public 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_mutBalance(addr).coin.value; *balance_ref balance - amount; Coin { value: amount } }withdraw先断言余额充足再用borrow_global_mut拿到全局存储的可变引用mut创建指向Coin.value字段的可变引用经引用修改余额后返回面额为amount的Cointransfer再把这个Coin存入to的余额。练习与解答step_4 源码里留了两个 TODObasic_coin.move#L25、L61-L68在publish_balance中加断言检查account下尚不存在Balance资源仿照withdraw实现deposit。完整解答见 step_4_sol/basic_coin.movepublish_balance增加assert!(!existsBalance(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 个测试分别覆盖一种行为并演示了多种测试注解的用法测试函数注解覆盖的行为mint_non_ownerL68-L76#[test(account 0x1)]#[expected_failure]非所有者调用mint必须 abort测试先断言0x1确实不等于MODULE_OWNERmint_check_balanceL78-L84#[test(account named_addr)]所有者铸造 42 后balance_of等于 42publish_balance_has_zeroL86-L91#[test(account 0x1)]发布后初始余额为 0publish_balance_already_existsL93-L98#[expected_failure(abort_code 2, location Self)]重复发布必须 abort且可精确指定期望的中止码EALREADY_HAS_BALANCE 2与中止位置withdraw_dneL102-L107#[expected_failure]地址下不存在Balance时withdraw中止注意返回的Coin资源必须用Coin { value: _ } ...解包withdraw_too_muchL109-L115#[expected_failure]零余额账户提现 1 必须中止can_withdraw_amountL117-L125#[test(account named_addr)]铸造 1000 后可完整提现并校验面额README 的练习在basic_coin模块中写一个只有几行的balance_of_dne测试验证对不存在Balance资源的地址调用balance_of会中止解答在 step_5_sol 中。Step 6把basic_coin泛型化Move 支持为结构体和函数引入类型参数是编写可复用库模块的基石。step_6/basic_coin.move 将模块改造成泛型版本L10-L16struct Coinphantom CoinType has store { value: u64 } struct Balancephantom CoinType has key { coin: CoinCoinType }CoinType声明为phantom幻影类型参数它不参与实际数据布局Coin根本不用它Balance仅以CoinCoinType形式携带其作用是区分代币种类——CoinMyCoinA与CoinMyCoinB在类型层面互不兼容withdraw相应变为fun withdrawCoinType(addr: address, amount: u64) : CoinCoinType acquires Balance函数体内所有资源访问都要显式实例化如borrow_global_mutBalanceCoinType(addr)。更值得关注的是策略委托模式。step_6 的 mint 与 transfer 签名都带一个_witness: CoinType参数且要求CoinType: droppublic fun transferCoinType: drop(from: signer, to: address, amount: u64, _witness: CoinType) acquires Balance { let check withdrawCoinType(signer::address_of(from), amount); depositCoinType(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::transferMyOddCoin(from, to, amount, MyOddCoin {}); }MyOddCoin是一个可drop的空结构体my_odd_coin模块在调用通用basic_coin之前先断言转账数量必须为奇数把“只能转奇数枚”的策略固化在类型所有者一侧。模块内附两个测试L25-L45test_odd_success验证转账 7 枚后双方余额分别为 35 与 17test_not_odd_failure用#[expected_failure]验证转账 8 枚必然失败。用 Step 2/5 学过的aptos move test即可运行。Step 7使用 Move Prover 检查中止条件Move Prover 是针对 Move 智能合约的形式化验证工具用户用 Move Specification LanguageMSL为函数声明属性再由证明器静态检查。运行前需先安装 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_globalBalanceCoinType(owner).coin.value │ ------------- abort happened here with execution failure ... owner 0x29 ABORTED含义是当owner名下不存在BalanceCoinType资源时borrow_global会 abort而该条件尚未被任何aborts_if子句覆盖。补齐后与 step_8 源码 L38-L41 的最终形态一致spec balance_of { pragma aborts_if_is_strict; aborts_if !existsBalanceCoinType(owner); }再次aptos move prove应无验证错误。Step 8为basic_coin编写完整形式化规格step_8 的 basic_coin.move 给出了withdraw、deposit、transfer三个方法的完整 MSL 规格是学习 MSL 语法的最佳范本。withdrawlet 绑定 双重中止条件 后置条件spec withdraw { let balance globalBalanceCoinType(addr).coin.value; aborts_if !existsBalanceCoinType(addr); aborts_if balance amount; let post balance_post globalBalanceCoinType(addr).coin.value; ensures result CoinCoinType { value: amount }; ensures balance_post balance - amount; }对应源码 L72-L81MSL 要点spec 块内可用let为表达式命名globalT(address): T是内建函数返回addr处资源T的值existsT(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 globalBalanceCoinType(addr).coin.value; let check_value check.value; aborts_if !existsBalanceCoinType(addr); aborts_if balance check_value MAX_U64; let post balance_post globalBalanceCoinType(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 globalBalanceCoinType(addr_from).coin.value; let balance_to globalBalanceCoinType(to).coin.value; let post balance_from_post globalBalanceCoinType(addr_from).coin.value; let post balance_to_post globalBalanceCoinType(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。关键文件索引内容路径教程主文档aptos-move/move-examples/move-tutorial/README.mdStep 1 第一个模块step_1/basic_coin/sources/first_module.moveStep 2 单元测试示例step_2/basic_coin/sources/first_module.moveStep 3 接口设计step_3/basic_coin.moveStep 4 带 TODO 的实现step_4/basic_coin/sources/basic_coin.moveStep 4 解答step_4_sol/basic_coin/sources/basic_coin.moveStep 5 七个单元测试step_5/basic_coin/sources/basic_coin.moveStep 6 泛型模块step_6/basic_coin/sources/basic_coin.moveStep 6 奇数币示例step_6/basic_coin/sources/my_odd_coin.moveStep 8 完整 MSL 规格step_8/basic_coin/sources/basic_coin.moveStep 8 解答step_8_sol/basic_coin/sources/basic_coin.move一键编译/测试脚本test.sh小结这套教程的递进关系值得注意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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
Aptos Move Tutorial：用 basic_coin 示例掌握 Move 编译、单元测试与 Move Prover 形式化验证
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 ProverStep 8为basic_coin编写形式化规格关键的设计约定是每个step_x目录都是自包含的。例如即使跳过了 Step 1–4也可以直接进入 step_5 目录因为此前步骤写的所有代码都已完整复制在该目录中。部分步骤还带有_sol后缀的解答目录如 step_4_sol、step_5_sol、step_8_sol。仓库中还提供了一键校验脚本 test.sh它维护两份目录清单——COMPILEDstep_1、step_2、step_4、step_5、step_6、step_7、step_8 及其_sol变体和TESTEDstep_2 起至 step_8 的目录分别对每个包执行aptos move compile与aptos move test见 test.sh#L31-L44。这也说明本教程示例在仓库 CI 层面是作为可编译、可测试的活代码维护的。Step 0环境准备教程要求两样东西本地副本克隆 aptos-core 仓库后进入aptos-move/move-examples/move-tutorial目录用ls确认能看到step_1 step_2 step_2_sol step_3 ...等子目录Aptos CLI教程写作时使用的版本为aptos 1.0.7aptos --version可确认。若使用 IDEREADME 推荐 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_globalCoin(addr).value 10, 0); }要点#[test(account 0xC0FFEE)]为account参数构造一个地址为0xC0FFEE的测试 signeracquires Coin声明本函数会访问全局存储中的Coin资源assert!(borrow_globalCoin(addr).value 10, 0)断言铸造后的资源value为 10失败则测试失败。因为测试函数与Coin定义在同一模块所以可以直接访问其私有字段#[test_only]注解等价于 Rust 的#[cfg(testing)]std::signer仅在测试编译时可见不污染正式字节码。README 给出的两道练习把断言改成11使测试失败并找出aptos move test的某个 flag 在测试失败时转储全局状态输出形如┌── test_mint_10 ────── │ error[E11001]: test failure │ ... │ 24 │ assert!(borrow_globalCoin(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 }找到收集覆盖率信息的 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 accounts 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: Mapaddress, MapResourceType, ResourceValue modules: Mapaddress, MapModuleName, 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-L11const 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-L28public 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_addrs 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_globalBalance(owner).coin.value中尖括号内是资源类型其后依次是地址与字段访问路径basic_coin.move#L40-L42。转账由私有辅助函数withdraw加deposit组合而成basic_coin.move#L45-L48、L51-L58public 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_mutBalance(addr).coin.value; *balance_ref balance - amount; Coin { value: amount } }withdraw先断言余额充足再用borrow_global_mut拿到全局存储的可变引用mut创建指向Coin.value字段的可变引用经引用修改余额后返回面额为amount的Cointransfer再把这个Coin存入to的余额。练习与解答step_4 源码里留了两个 TODObasic_coin.move#L25、L61-L68在publish_balance中加断言检查account下尚不存在Balance资源仿照withdraw实现deposit。完整解答见 step_4_sol/basic_coin.movepublish_balance增加assert!(!existsBalance(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 个测试分别覆盖一种行为并演示了多种测试注解的用法测试函数注解覆盖的行为mint_non_ownerL68-L76#[test(account 0x1)]#[expected_failure]非所有者调用mint必须 abort测试先断言0x1确实不等于MODULE_OWNERmint_check_balanceL78-L84#[test(account named_addr)]所有者铸造 42 后balance_of等于 42publish_balance_has_zeroL86-L91#[test(account 0x1)]发布后初始余额为 0publish_balance_already_existsL93-L98#[expected_failure(abort_code 2, location Self)]重复发布必须 abort且可精确指定期望的中止码EALREADY_HAS_BALANCE 2与中止位置withdraw_dneL102-L107#[expected_failure]地址下不存在Balance时withdraw中止注意返回的Coin资源必须用Coin { value: _ } ...解包withdraw_too_muchL109-L115#[expected_failure]零余额账户提现 1 必须中止can_withdraw_amountL117-L125#[test(account named_addr)]铸造 1000 后可完整提现并校验面额README 的练习在basic_coin模块中写一个只有几行的balance_of_dne测试验证对不存在Balance资源的地址调用balance_of会中止解答在 step_5_sol 中。Step 6把basic_coin泛型化Move 支持为结构体和函数引入类型参数是编写可复用库模块的基石。step_6/basic_coin.move 将模块改造成泛型版本L10-L16struct Coinphantom CoinType has store { value: u64 } struct Balancephantom CoinType has key { coin: CoinCoinType }CoinType声明为phantom幻影类型参数它不参与实际数据布局Coin根本不用它Balance仅以CoinCoinType形式携带其作用是区分代币种类——CoinMyCoinA与CoinMyCoinB在类型层面互不兼容withdraw相应变为fun withdrawCoinType(addr: address, amount: u64) : CoinCoinType acquires Balance函数体内所有资源访问都要显式实例化如borrow_global_mutBalanceCoinType(addr)。更值得关注的是策略委托模式。step_6 的 mint 与 transfer 签名都带一个_witness: CoinType参数且要求CoinType: droppublic fun transferCoinType: drop(from: signer, to: address, amount: u64, _witness: CoinType) acquires Balance { let check withdrawCoinType(signer::address_of(from), amount); depositCoinType(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::transferMyOddCoin(from, to, amount, MyOddCoin {}); }MyOddCoin是一个可drop的空结构体my_odd_coin模块在调用通用basic_coin之前先断言转账数量必须为奇数把“只能转奇数枚”的策略固化在类型所有者一侧。模块内附两个测试L25-L45test_odd_success验证转账 7 枚后双方余额分别为 35 与 17test_not_odd_failure用#[expected_failure]验证转账 8 枚必然失败。用 Step 2/5 学过的aptos move test即可运行。Step 7使用 Move Prover 检查中止条件Move Prover 是针对 Move 智能合约的形式化验证工具用户用 Move Specification LanguageMSL为函数声明属性再由证明器静态检查。运行前需先安装 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_globalBalanceCoinType(owner).coin.value │ ------------- abort happened here with execution failure ... owner 0x29 ABORTED含义是当owner名下不存在BalanceCoinType资源时borrow_global会 abort而该条件尚未被任何aborts_if子句覆盖。补齐后与 step_8 源码 L38-L41 的最终形态一致spec balance_of { pragma aborts_if_is_strict; aborts_if !existsBalanceCoinType(owner); }再次aptos move prove应无验证错误。Step 8为basic_coin编写完整形式化规格step_8 的 basic_coin.move 给出了withdraw、deposit、transfer三个方法的完整 MSL 规格是学习 MSL 语法的最佳范本。withdrawlet 绑定 双重中止条件 后置条件spec withdraw { let balance globalBalanceCoinType(addr).coin.value; aborts_if !existsBalanceCoinType(addr); aborts_if balance amount; let post balance_post globalBalanceCoinType(addr).coin.value; ensures result CoinCoinType { value: amount }; ensures balance_post balance - amount; }对应源码 L72-L81MSL 要点spec 块内可用let为表达式命名globalT(address): T是内建函数返回addr处资源T的值existsT(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 globalBalanceCoinType(addr).coin.value; let check_value check.value; aborts_if !existsBalanceCoinType(addr); aborts_if balance check_value MAX_U64; let post balance_post globalBalanceCoinType(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 globalBalanceCoinType(addr_from).coin.value; let balance_to globalBalanceCoinType(to).coin.value; let post balance_from_post globalBalanceCoinType(addr_from).coin.value; let post balance_to_post globalBalanceCoinType(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。关键文件索引内容路径教程主文档aptos-move/move-examples/move-tutorial/README.mdStep 1 第一个模块step_1/basic_coin/sources/first_module.moveStep 2 单元测试示例step_2/basic_coin/sources/first_module.moveStep 3 接口设计step_3/basic_coin.moveStep 4 带 TODO 的实现step_4/basic_coin/sources/basic_coin.moveStep 4 解答step_4_sol/basic_coin/sources/basic_coin.moveStep 5 七个单元测试step_5/basic_coin/sources/basic_coin.moveStep 6 泛型模块step_6/basic_coin/sources/basic_coin.moveStep 6 奇数币示例step_6/basic_coin/sources/my_odd_coin.moveStep 8 完整 MSL 规格step_8/basic_coin/sources/basic_coin.moveStep 8 解答step_8_sol/basic_coin/sources/basic_coin.move一键编译/测试脚本test.sh小结这套教程的递进关系值得注意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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考