Move 教程
本文将通过开发Move代码的一些步骤,包括Move模块的设计、实现、单元测试和形式验证,全文总共有九个步骤。
总共有九个步骤:
- 第0步:安装
- 第1步:编写我的第一个Move 模块
- 第2步:为我的第一个Move 模块添加单元测试
- 第3步:设计我的 `BasicCoin `模块
- 第4步:实现我的 `BaseCoin `模块
- 第5步:在 `BasicCoin `模块中添加和使用单元测试
- 第6步:使我的 `BasicCoin `模块通用化
- 第7步:使用 Move 验证器(Move prover)
- 第8步:为 `BasicCoin `模块编写正式规范
每个步骤都被设计成在相应的`step_x`文件夹中自成一体。例如,如果你想跳过第1到第4步的内容,请随意跳到第5步,因为我们在第5步之前写的所有代码都在`step_5`文件夹中。在一些步骤的末尾,我们还包括更多高级主题的补充材料。
> 教程代码: https://github.com/move-language/move/tree/main/language/documentation/tutorial
现在让我们开始吧!
## 第0步:安装
如果你还没有,打开你的终端并克隆[Move repository](https://github.com/move-language/move)。
```
git clone https://github.com/move-language/move.git
```
进入`move`目录并运行`dev_setup.sh`脚本。
```
cd move
./scripts/dev_setup.sh -ypt
```
按照脚本的提示来安装Move的所有依赖项。
该脚本将环境变量定义添加到你的`~/.profile`文件中。通过运行这条命令将其包含在内。
```
source ~/.profile
```
接下来,通过运行以下命令来安装Move的命令行工具。
```
cargo install --path language/tools/move-cli
```
你可以通过运行以下命令来检查它是否工作。
```
move --help
```
你应该看到类似这样的东西,以及一些命令的列表和描述。
```
move-package
Execute a package command. Executed in the current directory or the closest containing Move package
USAGE:
move [OPTIONS] <SUBCOMMAND>
OPTIONS:
--abi Generate ABIs for packages
...
```
如果你想找到哪些命令是可用的以及它们的作用,运行带有`--help`标志的命令或子命令将打印出文档。
在运行接下来的步骤之前,`cd`到教程目录。
```
cd <path_to_move>/language/documentation/tutorial
```
**Visual Studio代码Move支持**
Visual Studio Code有官方的Move支持。你需要先安装Move分析器:
```
cargo install --path language/move-analyzer
```
现在你可以通过打开VS Code,在扩展窗格中搜索 `move-analyzer `来安装VS扩展,并安装它。更详细的说明可以在扩展的[README](https://github.com/move-language/move/tree/main/language/move-analyzer/editors/code) 中找到
## 第1步:编写第一个Move模块
改变目录进入[`step_1/BasicCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_1/BasicCoin)目录。你应该看到一个叫做 `sources `的目录 -- 这是这个包的所有Move代码所在的地方。你还应该看到一个`Move.toml`文件。如果你熟悉Rust和Cargo,`Move.toml`文件与`Cargo.toml`文件相似,`sources`目录与`src`目录相似。
让我们来看看一些Move的代码! 在你选择的编辑器中打开[`sources/FirstModule.move`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_1/BasicCoin/sources/FirstModule.move)。你会看到的内容就是这个:
```rust
// sources/FirstModule.move
module 0xCAFE::BasicCoin {
...
}
```
这是定义了一个Move[模块](https://move-language.github.io/move/modules-and-scripts.html)。模块是Move代码的组成部分,它被定义为一个特定的地址: 模块可以被发布的地址。在这个例子中,`BasicCoin`模块只能在`0xCAFE`下发布。
> 译者注: 模块在发布者的地址下发布。标准库在 0x1 地址下发布。
现在让我们看看这个文件的下一部分,我们定义一个[结构体](https://move-language.github.io/move/structs-and-resources.html)来表示一个具有给定 `Value`的 `Coin`。
```rust
module 0xCAFE::BasicCoin {
struct Coin has key {
value: u64,
}
...
}
```
看一下文件的其余部分,我们看到一个函数定义,它创建了一个 `Coin `结构体并将其存储在一个账户下:
```rust
module 0xCAFE::BasicCoin {
struct Coin has key {
value: u64,
}
public fun mint(account: signer, value: u64) {
move_to(&account, Coin { value })
}
}
```
让我们看一下这个函数和它的内容:
- 它需要一个[`signer`](https://move-language.github.io/move/signer.html) -- 一个不可伪造代币,代表对一个特定地址的控制权,以及一个`value`来铸币。
- 它用给定的值创建一个`Coin`,并使用`move_to`操作符将其存储在`account`下。
让我们确保它可构建! 这可以通过在软件包文件夹中([`step_1/BasicCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_1/BasicCoin))下,用`build`命令来完成。
```
move build
```
**高级概念和参考资料:**
- 你可以通过命令创建一个空的Move包:
```
move new <pkg_name>
```
- Move代码也可以放在其他一些地方。关于Move包系统的更多信息可以在[Move 册子](https://move-language.github.io/move/packages.html)中找到。
- 关于`Move.toml`文件的更多信息可以在[Move册子的包部分](https://move-language.github.io/move/packages.html#movetoml)中找到。
- Move也支持[命名地址](https://move-language.github.io/move/address.html#named-addresses)的想法,命名地址是一种将Move源代码参数化的方式,这样你就可以使用不同的`NamedAddr`值来编译模块,从而得到不同的字节码,你可以根据你所控制的地址来进行部署。如果频繁使用,可以在`Move.toml`文件中的`[address]`部分进行定义,例如:
```
[addresses]
SomeNamedAddress = "0xC0FFEE"
```
- Move中的[结构体](https://move-language.github.io/move/structs-and-resources.html)可以被赋予不同的[能力(abilities)](https://move-language.github.io/move/abilities.html),这些能力描述了可以用该类型做什么。有四种不同的能力:
- `copy`:允许具有这种能力的类型的值被复制。
- `drop`:允许具有这种能力的类型的值被丢弃(销毁)。
- `store`:允许具有这种能力的类型的值存在于全局存储的结构体中。
- `key`: 允许该类型作为全局存储操作的键。
因此,在 `BasicCoin `模块中,我们说 `Coin `结构体可以作为全局存储的一个键,由于它没有其他能力,它不能被复制、丢弃,或作为非键值存储在存储中。因此,你不能复制Coin,也不能意外地丢失Coin
- [函数](https://move-language.github.io/move/functions.html)默认是private(私有的),也可以是`public(公共的)`,[`public(friend)`](https://move-language.github.io/move/friends.html),或`public(script)`。其中最后一种说明这个函数可以从交易脚本中调用。`public(script)`函数也可以被其他`public(script)`函数调用。
- `move_to`是[五个不同的全局存储操作符](https://move-language.github.io/move/global-storage-operators.html)之一。
## 第2步:为第一个Move模块添加单元测试
现在我们已经看了我们的第一个Move模块,我们进行一下测试,以确保通过改变目录到[`step_2/BasicCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_2/BasicCoin),使铸币以我们期望的方式工作。Move中的单元测试与Rust中的单元测试相似,如果你熟悉它们的话 -- 测试用`#[test]`来注释,并像普通的Move函数一样编写。
你可以用`package test`命令来运行测试。
```
move test
```
现在让我们看看[`FirstModule.move`文件](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_2/BasicCoin/sources/FirstModule.move)的内容。你将看到这个测试。
```rust
module 0xCAFE::BasicCoin {
...
// 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 = 0x1::signer::address_of(&account);
mint(account, 10);
// Make sure there is a `Coin` resource under `addr` with a value of `10`.
// We can access this resource and its value since we are in the
// same module that defined the `Coin` resource.
assert!(borrow_global<Coin>(addr).value == 10, 0);
}
}
```
这是在声明一个名为 `test_mint_10 `的单元测试,在 `account `下铸造一个 `value`为 `10 `的 `Coin `结构体。然后检查存储中的铸币是否与`assert!`调用的预期值一致。如果断言失败,单元测试就会失败。
### 高级概念和练习
- 有许多与测试有关的注解是值得探讨的,它们可以在[这里](https://github.com/move-language/move/blob/main/language/changes/4-unit-testing.md#testing-annotations-their-meaning-and-usage)找到。你会在步骤5中看到其中的一些使用。
- 在运行单元测试之前,你总是需要添加一个对Move标准库的依赖。这可以通过在 `Move.toml `的`[dependencies]`部分添加一个条目来完成,例如:
```toml
[dependencies]
MoveStdlib = { local = `../../../../move-stdlib/`, addr_subst = { `std` = `0x1` } }
```
注意,你可能需要改变路径,使其指向`<path_to_move>/language`下的`move-stdlib`目录。你也可以指定git的依赖性。你可以在[这里](https://move-language.github.io/move/packages.html#movetoml)阅读更多关于Move软件包依赖性的内容。
#### 练习
- 将断言改为`11`,这样测试就会失败。找到一个可以传递给`move test`命令的参数,它将显示测试失败时的全局状态。它应该看起来像这样:
```
┌── test_mint_10 ──────
│ error[E11001]: test failure
│ ┌─ ./sources/FirstModule.move:24:9
│ │
│ 18 │ fun test_mint_10(account: signer) acquires Coin {
│ │ ------------ In this function in 0xcafe::BasicCoin
│ ·
│ 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::BasicCoin::Coin {
│ value: 10
│ }
│
└──────────────────
```
* 找到一个允许你收集测试覆盖率信息的参数,然后使用`move coverage`命令查看覆盖率统计和源代码覆盖率。
## 第3步:设计`BasicCoin`模块
在这一节中,我们将设计一个实现基本Coin和余额接口的模块,Coin可以在不同地址下持有的余额之间被铸造和转移。
公共Move函数的签名如下:
```rust
/// Publish an empty balance resource under `account`'s address. This function must be called before
/// minting or transferring to the account.
public fun publish_balance(account: &signer) { ... }
/// 铸造 `amount` tokens 到 `mint_addr`. 需要模块的 owner 授权
public fun mint(module_owner: &signer, mint_addr: address, amount: u64) acquires Balance { ... }
/// 返回 `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 { ... }
```
接下来我们看一下这个模块需要的数据结构。
一个Move模块并没有自己的存储空间。相反,Move的 "全局存储"(我们称之为我们的区块链状态)是根据地址索引的。每个地址下都有Move模块(代码)和Move资源(值)。
全局存储在Rust语法中看起来大致是这样的。
```rust
struct GlobalStorage {
resources: Map<address, Map<ResourceType, ResourceValue>>
modules: Map<address, Map<ModuleName, ModuleBytecode>>
}
```
每个地址下的Move资源存储是一个从类型到值的映射。(一个善于观察的读者可能会注意到,这意味着每个地址只能有每个类型的一个值)。这方便地为我们提供了一个以地址为索引的本地映射。在我们的 `BasicCoin `模块中,我们定义了以下 `Balance `资源,代表每个地址拥有的Coin数量。
```rust
/// Struct representing the balance of each address.
struct Balance has key {
coin: Coin // same Coin from Step 1
}
```
大致上,Move区块链状态应该是这样的:
![img](https://img.learnblockchain.cn/pics/20220921154923.png)
### 高级主题
#### `public(script)`函数
只有具有`public(script)`可见性的函数可以在交易中直接调用。因此,如果你想从交易中直接调用`transfer`方法,你要把它的签名改为:
```rust
public(script) fun transfer(from: signer, to: address, amount: u64) acquires Balance { ... }
```
在[这里](https://move-language.github.io/move/functions.html#visibility)阅读更多关于Move 函数可见性的说明。
#### 与以太坊/Solidity的比较
在大多数以太坊 ERC-20合约中,每个地址的余额被存储在一个`mapping(address => uint256)`类型的状态变量中。这个状态变量存储在特定智能合约的存储中。
以太坊区块链的状态可能看起来像这样:
![](https://img.learnblockchain.cn/pics/20220921155027.png)
## 第4步:实现`BaseCoin`模块
我们已经在`step_4`文件夹中为你创建了一个Move包,名为`BasicCoin`。`sources`文件夹包含了包中所有Move模块的源代码,包括`BasicCoin.move`。在这一节中,我们将仔细研究一下[`BasicCoin.move`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_4/sources/BasicCoin.move)里面的方法的实现。
### 编译我们的代码
让我们首先在[`step_4/BasicCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_4/BasicCoin)文件夹中运行以下命令,尝试使用Move包构建代码。
```
move build
```
### 方法的实现
现在让我们仔细看看[`BasicCoin.move`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_4/BasicCoin/sources/BasicCoin.move)里面的方法的实现。
**方法 `publish_balance`.**
这个方法发布一个`Balance`资源到一个给定的地址。因为这个资源需要通过铸币或转账来接收Coin,所以`publish_balance`方法必须由用户(包括模块所有者)在接收coin之前调用。
这个方法使用`move_to`操作来发布资源。
```
let empty_coin = Coin { value: 0 };
move_to(account, Balance { coin: empty_coin });
```
**方法 `mint `**
`mint`方法为一个给定的账户铸造Coin。这里我们要求`mint`必须得到模块所有者的授权。我们使用 assert 语句来强制执行。
```
assert!(signer::address_of(&module_owner) == MODULE_OWNER, errors::requires_address(ENOT_MODULE_OWNER));
```
Move中的断言语句可以这样使用:`assert! (<predicate>, <abort_code>);`。这意味着如果`<predicate>`为假,那么就用`<abort_code>`中止交易。这里`MODULE_OWNER`和`ENOT_MODULE_OWNER`都是在模块的开头定义的常量。而`errors`模块定义了我们可以使用的常见错误类别。值得注意的是,Move在执行过程中是事务性的 -- 所以如果出现[abort](https://move-language.github.io/move/abort-and-assert.html),不需要对状态进行解除,因为该交易的变化不会被持久化到区块链上。
然后我们将一个价值为`amount`的Coin存入`mint_addr`的余额。
```
deposit(mint_addr, Coin { value: amount });
```
**方法 `balance_of` **
我们使用`borrow_global`,全局存储操作符之一,从全局存储中读取。
```
borrow_global<Balance>(owner).coin.value
| | \ /
resource type address field names
```
**方法 `transfer `**
这个函数从`from`的余额中提取代币并将代币存入`to`的余额中。我们仔细研究一下`withdraw`辅助函数:
```rust
fun withdraw(addr: address, amount: u64) : Coin acquires Balance {
let balance = balance_of(addr);
assert!(balance >= amount, EINSUFFICIENT_BALANCE);
let balance_ref = &mut borrow_global_mut<Balance>(addr).coin.value;
*balance_ref = balance - amount;
Coin { value: amount }
}
```
在方法的开始,我们断言取款的账户有足够的余额。然后我们使用`borrow_global_mut`来获取全局存储的可变引用,`&mut`被用来创建一个结构体的[可变引用](https://move-language.github.io/move/references.html)。然后我们通过这个可变引用来修改余额,并返回一个带有提取金额的新Coin。
### 练习
我们的模块中有两个 "TODO",作为练习留给读者。
- 完成实现`publish_balance`方法。
- 实现 `deposit `方法。
这个练习的解决方案可以在[`step_4_sol`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_4_sol)文件夹中找到。
**奖励练习**
- 如果我们把太多的代币存入余额,会发生什么?
## 第5步:添加和使用`BasicCoin`模块的单元测试
在这一步中,我们要看一下我们写的所有不同的单元测试,以覆盖我们在第四步中写的代码。我们还将看一下可以用来帮助我们写测试的一些工具。
为了开始工作,在[`step_5/BasicCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_5/BasicCoin)文件夹中运行`package test`命令:
```
move test
```
你应该看到类似这样的东西:
```
INCLUDING DEPENDENCY MoveStdlib
BUILDING BasicCoin
Running Move unit tests
[ PASS ] 0xcafe::BasicCoin::can_withdraw_amount
[ PASS ] 0xcafe::BasicCoin::init_check_balance
[ PASS ] 0xcafe::BasicCoin::init_non_owner
[ PASS ] 0xcafe::BasicCoin::publish_balance_already_exists
[ PASS ] 0xcafe::BasicCoin::publish_balance_has_zero
[ PASS ] 0xcafe::BasicCoin::withdraw_dne
[ PASS ] 0xcafe::BasicCoin::withdraw_too_much
Test result: OK. Total tests: 7; passed: 7; failed: 0
```
看看[`BasicCoin`模块](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_5/BasicCoin/sources/BasicCoin.move)中的测试,我们试图让每个单元测试保持在测试一个特定的行为。
### 练习
看完测试后,试着在`BasicCoin`模块中写一个名为`balance_of_dne`的单元测试,测试在`balance_of`被调用的地址下不存在`Balance`资源的情况。它应该只有几行!
这个练习的解决方案可以在[`step_5_sol`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_5_sol)找到。
## 第6步:使`BasicCoin`模块通用化
在Move中,我们可以使用泛型来定义不同输入数据类型的函数和结构体。泛型是库代码的一个很好的构建块。在本节中,我们将使简单的`BasicCoin`模块成为泛型,这样它就可以作为一个库模块,被其他用户模块使用。
首先,我们为数据结构添加类型参数:
```rust
struct Coin<phantom CoinType> has store {
value: u64
}
struct Balance<phantom CoinType> has key {
coin: Coin<CoinType>
}
```
也以同样的方式向方法添加类型参数。例如,`withdraw`变成了下面的内容:
```rust
fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance {
let balance = balance_of<CoinType>(addr);
assert!(balance >= amount, EINSUFFICIENT_BALANCE);
let balance_ref = &mut borrow_global_mut<Balance<CoinType>>(addr).coin.value;
*balance_ref = balance - amount;
Coin<CoinType> { value: amount }
}
```
看看[`step_6/BasicCoin/sources/BasicCoin.move`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_6/BasicCoin/sources/BasicCoin.move)来看看完整的实现。
在这一点上,熟悉以太坊的读者可能会注意到,这个模块与[ERC20代币标准](https://ethereum.org/en/developers/docs/standards/tokens/erc-20/)的目的相似,它为在智能合约中实现可替换的代币提供了一个接口。使用泛型的一个关键优势是能够重用代码,因为泛型库模块已经提供了一个标准实现,而实例化模块可以通过包装标准实现来提供定制。
我们提供了一个名为[`MyOddCoin`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_6/BasicCoin/sources/MyOddCoin.move)的小模块,它实例化了`Coin`类型并定制了其转移策略:只能转移奇数的Coin。我们还包括两个[测试](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_6/BasicCoin/sources/MyOddCoin.move)来测试这个行为。你可以使用你在第2步和第5步学到的命令来运行这些测试。
### 高级主题
`phantom`类型参数
在`Coin`和`Balance`的定义中,我们声明类型参数`CoinType`是`phantom` ,因为`CoinType`在结构体定义中没有使用,或者只作为`phantom` 类型参数使用。
[这里](https://move-language.github.io/move/generics.html#phantom-type-parameters)阅读更多关于`phantom`类型参数的信息。
## 高级步骤
在进入下一个步骤之前,让我们确保你已经安装了所有的验证器依赖项。
尝试运行`boogie /version`。如果出现 `command not found: boogie `的错误信息,你将不得不运行设置脚本和应用配置文件。
```bash
# run the following in move repo root directory
./scripts/dev_setup.sh -yp
source ~/.profile
```
## 第7步:使用Move验证器
部署在区块链上的智能合约可能会操纵高价值资产。作为一种使用严格的数学方法来描述行为和推理计算机系统的正确性的技术,形式验证已被用于区块链,以防止智能合约中的错误。[The Move prover](https://github.com/move-language/move/blob/main/language/move-prover/doc/user/prover-guide.md)是一个不断发展的形式验证工具,用于用Move语言编写的智能合约。用户可以使用[Move Specification Language (MSL)](https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md)来指定智能合约的功能属性,然后使用验证器来自动静态地检查它们。为了说明如何使用验证器,我们在[BasicCoin.move](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_7/BasicCoin/sources/BasicCoin.move)中加入了以下代码片段。
```
spec balance_of {
pragma aborts_if_is_strict;
}
```
非正式地说,代码块`spec balance_of {...}`包含方法`balance_of`的属性规范。
让我们首先在[`BasicCoin`目录](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_7/BasicCoin)内使用以下命令运行验证器:
```
move prove
```
其中输出以下错误信息:
```
error: abort not covered by any of the `aborts_if` clauses
┌─ ./sources/BasicCoin.move:38:5
│
35 │ borrow_global<Balance<CoinType>>(owner).coin.value
│ ------------- abort happened here with execution failure
·
38 │ ╭ spec balance_of {
39 │ │ pragma aborts_if_is_strict;
40 │ │ }
│ ╰─────^
│
= at ./sources/BasicCoin.move:34: balance_of
= owner = 0x29
= at ./sources/BasicCoin.move:35: balance_of
= ABORTED
Error: exiting with verification errors
```
该验证器基本上告诉我们,我们需要明确指定函数`balance_of`将中止的条件,这是在`owner`不拥有资源`Balance<CoinType>`时调用函数`borrow_global`造成的。为了删除这个错误信息,我们添加了一个`aborts_if`条件,如下:
```
spec balance_of {
pragma aborts_if_is_strict;
aborts_if !exists<Balance<CoinType>>(owner);
}
```
添加这个条件后,再次尝试运行`prove`命令,以确认没有验证错误。
```
move prove
```
除了中止条件外,我们还想定义功能属性。在第8步中,我们将通过为定义了 `BasicCoin `模块的方法指定属性来对验证器进行更详细的介绍。
## 第8步:为 `BasicCoin `模块编写正式规范
### withdraw 方法
方法 `withdraw `的签名在下面给出:
```
fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance
```
该方法从地址`addr`提取价值为`amount`的代币,并返回一个创建的价值为`amount`的Coin。当1)`addr`没有资源`Balance<CoinType>`或2)`addr`中的代币数量小于`amount`时,方法`withdraw`中止。我们可以这样定义条件。
```rust
spec withdraw {
let balance = global<Balance<CoinType>>(addr).coin.value;
aborts_if !exists<Balance<CoinType>>(addr);
aborts_if balance < amount;
}
```
正如我们在这里看到的,一个规范块可以包含let绑定,它为表达式引入名称。`global<T>(address)。T `是一个内置函数,返回 `addr `处的资源值。`balance`是`addr`所拥有的代币的数量。`exists<T>(address): bool`是一个内置函数,如果资源T在地址处存在,则返回true。两个`aborts_if`子句对应上面提到的两个条件。一般来说,如果一个函数有一个以上的`aborts_if`条件,这些条件就会相互or-ed。默认情况下,如果用户想指定中止条件,需要列出所有可能的条件。否则,验证器将产生一个验证错误。然而,如果`pragma aborts_if_is_partial`在spec块中被定义,组合的中止条件(or-ed的单个条件)只意味着函数的中止。读者可以参考[MSL](https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md)文件了解更多信息。
下一步是定义功能属性,在下面的两个 `ensures `语句中描述。首先,通过使用`let post`绑定,`balance_post`表示执行后`addr`的余额,它应该等于`balance - amount`。然后,返回值(表示为`result`)应该是一个价值为`amount`的Coin。
```rust
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 balance_post == balance - amount;
ensures result == Coin<CoinType> { value: amount };
}
```
### `deposit `方法
方法 `deposit `的签名如下:
```
fun deposit<CoinType>(addr: address, check: Coin<CoinType>) acquires Balance
```
该方法将 `check`存入 `addr`。该规范定义如下:
```rust
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;
}
```
`balance`代表执行前`addr`中的代币数量,`check_value`代表要存入的代币数量。如果1)`addr`没有资源`Balance<CoinType>`或2)`balance`和`check_value`之和大于`u64`类型的最大值,该方法将终止。该功能属性检查余额在执行后是否被正确更新。
### `transfer` 方法
方法 `transfer `的签名如下:
```
public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance
```
该方法从`from`的账户向`to`的地址转移`amount`的Coin。说明如下:
```rust
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;
}
```
`addr_from`是`from`的地址。然后得到`addr_from`和`to`在执行前和执行后的余额。`ensures `语句规定,从`addr_from`中扣除`amount`的代币数量,并添加到`to`中。然而,验证器将产生如下错误信息。
```
error: post-condition does not hold
┌─ ./sources/BasicCoin.move:57:9
│
62 │ ensures balance_from_post == balance_from - amount;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
...
```
当`addr_from`等于`to`时,该属性不被持有。因此,我们可以在方法中添加一个断言`assert!(from_addr != to)`,以确保`addr_from`不等于`to`。
### 练习
- 为 `transfer `方法实现 `aborts_if `条件。
- 实现`mint`和`publish_balance`方法的规范。
这个练习的解决方案可以在[`step_8_sol`](https://github.com/solana-labs/move/blob/main/language/documentation/tutorial/step_8_sol)找到。
原文: https://github.com/move-language/move/tree/main/language/documentation/tutorial
欢迎来到Move教程! 在本教程中,我们将通过开发Move代码的一些步骤,包括Move模块的设计、实现、单元测试和形式验证。
总共有九个步骤:
- 第0步:安装
- 第1步:编写我的第一个Move 模块
- 第2步:为我的第一个Move 模块添加单元测试
- 第3步:设计我的
BasicCoin
模块 - 第4步:实现我的
BaseCoin
模块 - 第5步:在
BasicCoin
模块中添加和使用单元测试 - 第6步:使我的
BasicCoin
模块通用化 - 第7步:使用 Move 验证器(Move prover)
- 第8步:为
BasicCoin
模块编写正式规范
每个步骤都被设计成在相应的step_x
文件夹中自成一体。例如,如果你想跳过第1到第4步的内容,请随意跳到第5步,因为我们在第5步之前写的所有代码都在step_5
文件夹中。在一些步骤的末尾,我们还包括更多高级主题的补充材料。
教程代码: https://github.com/move-language/move/tree/main/language/documentation/tutorial
现在让我们开始吧!
第0步:安装
如果你还没有,打开你的终端并克隆Move repository。
git clone https://github.com/move-language/move.git
进入move
目录并运行dev_setup.sh
脚本。
cd move
./scripts/dev_setup.sh -ypt
按照脚本的提示来安装Move的所有依赖项。
该脚本将环境变量定义添加到你的~/.profile
文件中。通过运行这条命令将其包含在内。
source ~/.profile
接下来,通过运行以下命令来安装Move的命令行工具。
cargo install --path language/tools/move-cli
你可以通过运行以下命令来检查它是否工作。
move --help
你应该看到类似这样的东西,以及一些命令的列表和描述。
move-package
Execute a package command. Executed in the current directory or the closest containing Move package
USAGE:
move [OPTIONS] <SUBCOMMAND>
OPTIONS:
--abi Generate ABIs for packages
...
如果你想找到哪些命令是可用的以及它们的作用,运行带有--help
标志的命令或子命令将打印出文档。
在运行接下来的步骤之前,cd
到教程目录。
cd <path_to_move>/language/documentation/tutorial
Visual Studio代码Move支持
Visual Studio Code有官方的Move支持。你需要先安装Move分析器:
cargo install --path language/move-analyzer
现在你可以通过打开VS Code,在扩展窗格中搜索 move-analyzer
来安装VS扩展,并安装它。更详细的说明可以在扩展的README 中找到
第1步:编写第一个Move模块
改变目录进入step_1/BasicCoin
目录。你应该看到一个叫做 sources
的目录 -- 这是这个包的所有Move代码所在的地方。你还应该看到一个Move.toml
文件。如果你熟悉Rust和Cargo,Move.toml
文件与Cargo.toml
文件相似,sources
目录与src
目录相似。
让我们来看看一些Move的代码! 在你选择的编辑器中打开sources/FirstModule.move
。你会看到的内容就是这个:
// sources/FirstModule.move
module 0xCAFE::BasicCoin {
...
}
这是定义了一个Move模块。模块是Move代码的组成部分,它被定义为一个特定的地址: 模块可以被发布的地址。在这个例子中,BasicCoin
模块只能在0xCAFE
下发布。
译者注: 模块在发布者的地址下发布。标准库在 0x1 地址下发布。
现在让我们看看这个文件的下一部分,我们定义一个结构体来表示一个具有给定 Value
的 Coin
。
module 0xCAFE::BasicCoin {
struct Coin has key {
value: u64,
}
...
}
看一下文件的其余部分,我们看到一个函数定义,它创建了一个 Coin
结构体并将其存储在一个账户下:
module 0xCAFE::BasicCoin {
struct Coin has key {
value: u64,
}
public fun mint(account: signer, value: u64) {
move_to(&account, Coin { value })
}
}
让我们看一下这个函数和它的内容:
- 它需要一个
signer
-- 一个不可伪造代币,代表对一个特定地址的控制权,以及一个value
来铸币。 - 它用给定的值创建一个
Coin
,并使用move_to
操作符将其存储在account
下。
让我们确保它可构建! 这可以通过在软件包文件夹中(step_1/BasicCoin
)下,用build
命令来完成。
move build
高级概念和参考资料:
- 你可以通过命令创建一个空的Move包:
move new <pkg_name>
-
Move代码也可以放在其他一些地方。关于Move包系统的更多信息可以在Move 册子中找到。
-
关于
Move.toml
文件的更多信息可以在Move册子的包部分中找到。 -
Move也支持命名地址的想法,命名地址是一种将Move源代码参数化的方式,这样你就可以使用不同的
NamedAddr
值来编译模块,从而得到不同的字节码,你可以根据你所控制的地址来进行部署。如果频繁使用,可以在Move.toml
文件中的[address]
部分进行定义,例如:
[addresses]
SomeNamedAddress = "0xC0FFEE"
- Move中的结构体可以被赋予不同的能力(abilities),这些能力描述了可以用该类型做什么。有四种不同的能力:
copy
:允许具有这种能力的类型的值被复制。drop
:允许具有这种能力的类型的值被丢弃(销毁)。store
:允许具有这种能力的类型的值存在于全局存储的结构体中。key
: 允许该类型作为全局存储操作的键。
因此,在 BasicCoin
模块中,我们说 Coin
结构体可以作为全局存储的一个键,由于它没有其他能力,它不能被复制、丢弃,或作为非键值存储在存储中。因此,你不能复制Coin,也不能意外地丢失Coin
-
函数默认是private(私有的),也可以是
public(公共的)
,public(friend)
,或public(script)
。其中最后一种说明这个函数可以从交易脚本中调用。public(script)
函数也可以被其他public(script)
函数调用。 -
move_to
是五个不同的全局存储操作符之一。
第2步:为第一个Move模块添加单元测试
现在我们已经看了我们的第一个Move模块,我们进行一下测试,以确保通过改变目录到step_2/BasicCoin
,使铸币以我们期望的方式工作。Move中的单元测试与Rust中的单元测试相似,如果你熟悉它们的话 -- 测试用#[test]
来注释,并像普通的Move函数一样编写。
你可以用package test
命令来运行测试。
move test
现在让我们看看FirstModule.move
文件的内容。你将看到这个测试。
module 0xCAFE::BasicCoin {
...
// 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 = 0x1::signer::address_of(&account);
mint(account, 10);
// Make sure there is a `Coin` resource under `addr` with a value of `10`.
// We can access this resource and its value since we are in the
// same module that defined the `Coin` resource.
assert!(borrow_global<Coin>(addr).value == 10, 0);
}
}
这是在声明一个名为 test_mint_10
的单元测试,在 account
下铸造一个 value
为 10
的 Coin
结构体。然后检查存储中的铸币是否与assert!
调用的预期值一致。如果断言失败,单元测试就会失败。
高级概念和练习
-
有许多与测试有关的注解是值得探讨的,它们可以在这里找到。你会在步骤5中看到其中的一些使用。
-
在运行单元测试之前,你总是需要添加一个对Move标准库的依赖。这可以通过在
Move.toml
的[dependencies]
部分添加一个条目来完成,例如:
[dependencies]
MoveStdlib = { local = `../../../../move-stdlib/`, addr_subst = { `std` = `0x1` } }
注意,你可能需要改变路径,使其指向<path_to_move>/language
下的move-stdlib
目录。你也可以指定git的依赖性。你可以在这里阅读更多关于Move软件包依赖性的内容。
练习
- 将断言改为
11
,这样测试就会失败。找到一个可以传递给move test
命令的参数,它将显示测试失败时的全局状态。它应该看起来像这样:
┌── test_mint_10 ──────
│ error[E11001]: test failure
│ ┌─ ./sources/FirstModule.move:24:9
│ │
│ 18 │ fun test_mint_10(account: signer) acquires Coin {
│ │ ------------ In this function in 0xcafe::BasicCoin
│ ·
│ 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::BasicCoin::Coin {
│ value: 10
│ }
│
└──────────────────
- 找到一个允许你收集测试覆盖率信息的参数,然后使用
move coverage
命令查看覆盖率统计和源代码覆盖率。
第3步:设计BasicCoin
模块
在这一节中,我们将设计一个实现基本Coin和余额接口的模块,Coin可以在不同地址下持有的余额之间被铸造和转移。
公共Move函数的签名如下:
/// Publish an empty balance resource under `account`'s address. This function must be called before
/// minting or transferring to the account.
public fun publish_balance(account: &signer) { ... }
/// 铸造 `amount` tokens 到 `mint_addr`. 需要模块的 owner 授权
public fun mint(module_owner: &signer, mint_addr: address, amount: u64) acquires Balance { ... }
/// 返回 `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 { ... }
接下来我们看一下这个模块需要的数据结构。
一个Move模块并没有自己的存储空间。相反,Move的 "全局存储"(我们称之为我们的区块链状态)是根据地址索引的。每个地址下都有Move模块(代码)和Move资源(值)。
全局存储在Rust语法中看起来大致是这样的。
struct GlobalStorage {
resources: Map<address, Map<ResourceType, ResourceValue>>
modules: Map<address, Map<ModuleName, ModuleBytecode>>
}
每个地址下的Move资源存储是一个从类型到值的映射。(一个善于观察的读者可能会注意到,这意味着每个地址只能有每个类型的一个值)。这方便地为我们提供了一个以地址为索引的本地映射。在我们的 BasicCoin
模块中,我们定义了以下 Balance
资源,代表每个地址拥有的Coin数量。
/// Struct representing the balance of each address.
struct Balance has key {
coin: Coin // same Coin from Step 1
}
大致上,Move区块链状态应该是这样的:
高级主题
public(script)
函数
只有具有public(script)
可见性的函数可以在交易中直接调用。因此,如果你想从交易中直接调用transfer
方法,你要把它的签名改为:
public(script) fun transfer(from: signer, to: address, amount: u64) acquires Balance { ... }
在这里阅读更多关于Move 函数可见性的说明。
与以太坊/Solidity的比较
在大多数以太坊 ERC-20合约中,每个地址的余额被存储在一个mapping(address => uint256)
类型的状态变量中。这个状态变量存储在特定智能合约的存储中。
以太坊区块链的状态可能看起来像这样:
第4步:实现BaseCoin
模块
我们已经在step_4
文件夹中为你创建了一个Move包,名为BasicCoin
。sources
文件夹包含了包中所有Move模块的源代码,包括BasicCoin.move
。在这一节中,我们将仔细研究一下BasicCoin.move
里面的方法的实现。
编译我们的代码
让我们首先在step_4/BasicCoin
文件夹中运行以下命令,尝试使用Move包构建代码。
move build
方法的实现
现在让我们仔细看看BasicCoin.move
里面的方法的实现。
方法 publish_balance
.
这个方法发布一个Balance
资源到一个给定的地址。因为这个资源需要通过铸币或转账来接收Coin,所以publish_balance
方法必须由用户(包括模块所有者)在接收coin之前调用。
这个方法使用move_to
操作来发布资源。
let empty_coin = Coin { value: 0 };
move_to(account, Balance { coin: empty_coin });
方法 mint
mint
方法为一个给定的账户铸造Coin。这里我们要求mint
必须得到模块所有者的授权。我们使用 assert 语句来强制执行。
assert!(signer::address_of(&module_owner) == MODULE_OWNER, errors::requires_address(ENOT_MODULE_OWNER));
Move中的断言语句可以这样使用:assert! (<predicate>, <abort_code>);
。这意味着如果<predicate>
为假,那么就用<abort_code>
中止交易。这里MODULE_OWNER
和ENOT_MODULE_OWNER
都是在模块的开头定义的常量。而errors
模块定义了我们可以使用的常见错误类别。值得注意的是,Move在执行过程中是事务性的 -- 所以如果出现abort,不需要对状态进行解除,因为该交易的变化不会被持久化到区块链上。
然后我们将一个价值为amount
的Coin存入mint_addr
的余额。
deposit(mint_addr, Coin { value: amount });
方法 balance_of
我们使用borrow_global
,全局存储操作符之一,从全局存储中读取。
borrow_global<Balance>(owner).coin.value
| | \ /
resource type address field names
方法 transfer
这个函数从from
的余额中提取代币并将代币存入to
的余额中。我们仔细研究一下withdraw
辅助函数:
fun withdraw(addr: address, amount: u64) : Coin acquires Balance {
let balance = balance_of(addr);
assert!(balance >= amount, EINSUFFICIENT_BALANCE);
let balance_ref = &mut borrow_global_mut<Balance>(addr).coin.value;
*balance_ref = balance - amount;
Coin { value: amount }
}
在方法的开始,我们断言取款的账户有足够的余额。然后我们使用borrow_global_mut
来获取全局存储的可变引用,&mut
被用来创建一个结构体的可变引用。然后我们通过这个可变引用来修改余额,并返回一个带有提取金额的新Coin。
练习
我们的模块中有两个 "TODO",作为练习留给读者。
- 完成实现
publish_balance
方法。 - 实现
deposit
方法。
这个练习的解决方案可以在step_4_sol
文件夹中找到。
奖励练习
- 如果我们把太多的代币存入余额,会发生什么?
第5步:添加和使用BasicCoin
模块的单元测试
在这一步中,我们要看一下我们写的所有不同的单元测试,以覆盖我们在第四步中写的代码。我们还将看一下可以用来帮助我们写测试的一些工具。
为了开始工作,在step_5/BasicCoin
文件夹中运行package test
命令:
move test
你应该看到类似这样的东西:
INCLUDING DEPENDENCY MoveStdlib
BUILDING BasicCoin
Running Move unit tests
[ PASS ] 0xcafe::BasicCoin::can_withdraw_amount
[ PASS ] 0xcafe::BasicCoin::init_check_balance
[ PASS ] 0xcafe::BasicCoin::init_non_owner
[ PASS ] 0xcafe::BasicCoin::publish_balance_already_exists
[ PASS ] 0xcafe::BasicCoin::publish_balance_has_zero
[ PASS ] 0xcafe::BasicCoin::withdraw_dne
[ PASS ] 0xcafe::BasicCoin::withdraw_too_much
Test result: OK. Total tests: 7; passed: 7; failed: 0
看看BasicCoin
模块中的测试,我们试图让每个单元测试保持在测试一个特定的行为。
练习
看完测试后,试着在BasicCoin
模块中写一个名为balance_of_dne
的单元测试,测试在balance_of
被调用的地址下不存在Balance
资源的情况。它应该只有几行!
这个练习的解决方案可以在step_5_sol
找到。
第6步:使BasicCoin
模块通用化
在Move中,我们可以使用泛型来定义不同输入数据类型的函数和结构体。泛型是库代码的一个很好的构建块。在本节中,我们将使简单的BasicCoin
模块成为泛型,这样它就可以作为一个库模块,被其他用户模块使用。
首先,我们为数据结构添加类型参数:
struct Coin<phantom CoinType> has store {
value: u64
}
struct Balance<phantom CoinType> has key {
coin: Coin<CoinType>
}
也以同样的方式向方法添加类型参数。例如,withdraw
变成了下面的内容:
fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance {
let balance = balance_of<CoinType>(addr);
assert!(balance >= amount, EINSUFFICIENT_BALANCE);
let balance_ref = &mut borrow_global_mut<Balance<CoinType>>(addr).coin.value;
*balance_ref = balance - amount;
Coin<CoinType> { value: amount }
}
看看step_6/BasicCoin/sources/BasicCoin.move
来看看完整的实现。
在这一点上,熟悉以太坊的读者可能会注意到,这个模块与ERC20代币标准的目的相似,它为在智能合约中实现可替换的代币提供了一个接口。使用泛型的一个关键优势是能够重用代码,因为泛型库模块已经提供了一个标准实现,而实例化模块可以通过包装标准实现来提供定制。
我们提供了一个名为MyOddCoin
的小模块,它实例化了Coin
类型并定制了其转移策略:只能转移奇数的Coin。我们还包括两个测试来测试这个行为。你可以使用你在第2步和第5步学到的命令来运行这些测试。
高级主题
phantom
类型参数
在Coin
和Balance
的定义中,我们声明类型参数CoinType
是phantom
,因为CoinType
在结构体定义中没有使用,或者只作为phantom
类型参数使用。
这里阅读更多关于phantom
类型参数的信息。
高级步骤
在进入下一个步骤之前,让我们确保你已经安装了所有的验证器依赖项。
尝试运行boogie /version
。如果出现 command not found: boogie
的错误信息,你将不得不运行设置脚本和应用配置文件。
# run the following in move repo root directory
./scripts/dev_setup.sh -yp
source ~/.profile
第7步:使用Move验证器
部署在区块链上的智能合约可能会操纵高价值资产。作为一种使用严格的数学方法来描述行为和推理计算机系统的正确性的技术,形式验证已被用于区块链,以防止智能合约中的错误。The Move prover是一个不断发展的形式验证工具,用于用Move语言编写的智能合约。用户可以使用Move Specification Language (MSL)来指定智能合约的功能属性,然后使用验证器来自动静态地检查它们。为了说明如何使用验证器,我们在BasicCoin.move中加入了以下代码片段。
spec balance_of {
pragma aborts_if_is_strict;
}
非正式地说,代码块spec balance_of {...}
包含方法balance_of
的属性规范。
让我们首先在BasicCoin
目录内使用以下命令运行验证器:
move prove
其中输出以下错误信息:
error: abort not covered by any of the `aborts_if` clauses
┌─ ./sources/BasicCoin.move:38:5
│
35 │ borrow_global<Balance<CoinType>>(owner).coin.value
│ ------------- abort happened here with execution failure
·
38 │ ╭ spec balance_of {
39 │ │ pragma aborts_if_is_strict;
40 │ │ }
│ ╰─────^
│
= at ./sources/BasicCoin.move:34: balance_of
= owner = 0x29
= at ./sources/BasicCoin.move:35: balance_of
= ABORTED
Error: exiting with verification errors
该验证器基本上告诉我们,我们需要明确指定函数balance_of
将中止的条件,这是在owner
不拥有资源Balance<CoinType>
时调用函数borrow_global
造成的。为了删除这个错误信息,我们添加了一个aborts_if
条件,如下:
spec balance_of {
pragma aborts_if_is_strict;
aborts_if !exists<Balance<CoinType>>(owner);
}
添加这个条件后,再次尝试运行prove
命令,以确认没有验证错误。
move prove
除了中止条件外,我们还想定义功能属性。在第8步中,我们将通过为定义了 BasicCoin
模块的方法指定属性来对验证器进行更详细的介绍。
第8步:为 BasicCoin
模块编写正式规范
withdraw 方法
方法 withdraw
的签名在下面给出:
fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance
该方法从地址addr
提取价值为amount
的代币,并返回一个创建的价值为amount
的Coin。当1)addr
没有资源Balance<CoinType>
或2)addr
中的代币数量小于amount
时,方法withdraw
中止。我们可以这样定义条件。
spec withdraw {
let balance = global<Balance<CoinType>>(addr).coin.value;
aborts_if !exists<Balance<CoinType>>(addr);
aborts_if balance < amount;
}
正如我们在这里看到的,一个规范块可以包含let绑定,它为表达式引入名称。global<T>(address)。T
是一个内置函数,返回 addr
处的资源值。balance
是addr
所拥有的代币的数量。exists<T>(address): bool
是一个内置函数,如果资源T在地址处存在,则返回true。两个aborts_if
子句对应上面提到的两个条件。一般来说,如果一个函数有一个以上的aborts_if
条件,这些条件就会相互or-ed。默认情况下,如果用户想指定中止条件,需要列出所有可能的条件。否则,验证器将产生一个验证错误。然而,如果pragma aborts_if_is_partial
在spec块中被定义,组合的中止条件(or-ed的单个条件)只意味着函数的中止。读者可以参考MSL文件了解更多信息。
下一步是定义功能属性,在下面的两个 ensures
语句中描述。首先,通过使用let post
绑定,balance_post
表示执行后addr
的余额,它应该等于balance - amount
。然后,返回值(表示为result
)应该是一个价值为amount
的Coin。
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 balance_post == balance - amount;
ensures result == Coin<CoinType> { value: amount };
}
deposit
方法
方法 deposit
的签名如下:
fun deposit<CoinType>(addr: address, check: Coin<CoinType>) acquires Balance
该方法将 check
存入 addr
。该规范定义如下:
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;
}
balance
代表执行前addr
中的代币数量,check_value
代表要存入的代币数量。如果1)addr
没有资源Balance<CoinType>
或2)balance
和check_value
之和大于u64
类型的最大值,该方法将终止。该功能属性检查余额在执行后是否被正确更新。
transfer
方法
方法 transfer
的签名如下:
public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance
该方法从from
的账户向to
的地址转移amount
的Coin。说明如下:
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;
}
addr_from
是from
的地址。然后得到addr_from
和to
在执行前和执行后的余额。ensures
语句规定,从addr_from
中扣除amount
的代币数量,并添加到to
中。然而,验证器将产生如下错误信息。
error: post-condition does not hold
┌─ ./sources/BasicCoin.move:57:9
│
62 │ ensures balance_from_post == balance_from - amount;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
...
当addr_from
等于to
时,该属性不被持有。因此,我们可以在方法中添加一个断言assert!(from_addr != to)
,以确保addr_from
不等于to
。
练习
- 为
transfer
方法实现aborts_if
条件。 - 实现
mint
和publish_balance
方法的规范。
这个练习的解决方案可以在step_8_sol
找到。
原文: https://github.com/move-language/move/tree/main/language/documentation/tutorial
本文参与区块链技术网 ,好文好收益,欢迎正在阅读的你也加入。
- 发表于 2022-09-22 16:29
- 阅读 ( 1754 )
- 学分 ( 187 )
- 分类:Move
评论