Move教程

欢迎来到 Move 语言教程，在本教程中，我们通过一些具体的步骤进行 Move 语言代码的开发，包括 Move 模块的设计、实现、单元测试和形式化验证。

整个过程共包含9个步骤：

• Move教程
  • 0.安装 Move 开发环境
  • 1.编写第一个 Move 模块
  • 2.给模块（Module）添加单元测试
    • 练习
  • 3.设计自己的 BasicCoin 模块（Module）
    • 进阶主题 (Advanced topics) ：
  • 4.BasicCoin 模块（Module）的实现
    • 编译代码
    • 方法的实现
    • 练习
      • 额外练习
  • 5.给 BasicCoin 模块添加单元测试
  • 6.使用泛型（generic）编写 BasicCoin 模块
    • 进阶主题：
    • 进阶步骤
  • 7.使用 Move prover
  • 8.为 BasicCoin 模块编写形式化规范（formal specification）

0.安装 Move 开发环境

如果你还没有安装过 Move，首先打开命令终端(terminal) 并clone Move代码库:

git clone https://github.com/move-language/move.git

进入到 move 文件夹下，执行 dev_setup.sh 脚本:

cd move
./scripts/dev_setup.sh -ypt

根据脚本命令的提示，按顺序安装 Move 的所有依赖项。 脚本将会将(move命令所在路径)环境变量写入到 ~/.profile 文件中。

执行如下命令使环境变量生效：

source ~/.profile

然后执行如下命令来安装 Move 命令行工具：

cargo install --path language/tools/move-cli

通过如下运行命令可以检查 move 命令是否可正常：

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

cargo install --path language/move-analyzer

1.编写第一个 Move 模块

切换当前目录到 step_1/BasicCoin 下，你将看到 sources 子目录 -- 这个包(package)下所有的 Move 代码都在此目录中，同时你还会看到一个 Move.toml 文件。该文件指定当前包的依赖列表和其他信息。 如果您熟悉 Rust 和 Cargo，那 Move.toml 文件类似 Cargo.toml 文件，sources 目录类似 src 目录(它们的作用是一样的)

来一起看看 Move 语言代码内容！ 用你的编辑器打开 sources/FirstModule.move 文件，会看到如下内容：

// sources/FirstModule.move
module 0xCAFE::BasicCoin {
    ...
}

这是一个 Move module(模块)的定义。模块是 Move 语言的代码块, 并且它使用指定的地址(address)进行定义 -- 模块只能在该地址下发布。 当前 BasicCoin 模块只能被发布在 0xCAFE 地址下。

再看这个文件的下一部分，这里定义了一个具有字段 value 的结构体 Coin：

module 0xCAFE::BasicCoin {
    struct Coin has key {
        value: u64,
    }
    ...
}

再看文件剩余部分，我们会看到一个函数，它会创建一个 Coin 结构体，并将其保存在某个账号(account)下：

module 0xCAFE::BasicCoin {
    struct Coin has key {
        value: u64,
    }

    public fun mint(account: signer, value: u64) {
        move_to(&account, Coin { value })
    }
}

让我们来看看这个函数和它的含义:

• 此函数需要一个 signer 参数 -- 表示不可伪造的 token 受此特定地址的控制; 和一个需要铸造的数量参数 value。
• 此函数使用给定的参数值铸造一个 Coin，然后通过 move_to 操作将其保存在(全局存储中)给定的 account 账户下。

我们需要确保它真的执行，这可以通过在包文件夹(step_1/BasicCoin)下的运行 build 命令来完成：

move build

[addresses]
SomeNamedAddress = "0xC0FFEE"

2.给模块（Module）添加单元测试

现在我们已经完成了我们的第一个 Move 模块，我们将切换到目录 step_2/BasicCoin 下并完成一个测试，确保铸币按我们预期的方式工作。 如果你熟悉它们(Move 和 Rust)的话，Move 中的单元测试类似于 Rust 中的单元测试 —— 测试代码使用 #[test] 注解，并像编写普通的 Move 函数一样。

可以通过 move 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 = 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! 断言检查已经铸造成功并保存在(全局)存储中的 Coin 的值是否与期望值一致。如果断言 assert 执行失败，则单元测试失败。

[dependencies]
MoveStdlib = { local = "../../../../move-stdlib/", addr_subst = { "Std" = "0x1" } }

练习

• 将断言值改为 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 模块（Module）

在本节中，我们将设计一个具有基本代币和余额(balance)接口功能的模块，通过他们来实现币的挖矿铸造，不同地址之下钱包的转账。

Move 语言的 public function 签名如下：

/// 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) { ... }

/// 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 { ... }

接下来再看本模块所需要各数据结构.

Move 语言的模块没有自己的数据存储，相反的是 Move 语言提供按地址(addresses) 索引的 全局存储 (也是就是我们所说的区块链状态(blockchain state)). 每个地址之下包含有 Move 模块(代码)和 Move 资源 (数据)。

在 Rust 语法中，全局存储看起来有点像这样：

#![allow(unused)]
fn main() {
struct GlobalStorage {
    resources: Map<address, Map<ResourceType, ResourceValue>>
    modules: Map<address, Map<ModuleName, ModuleBytecode>>
}
}

每个地址下的 Move 资源存储是一个类型到数值的映射。(细心的读者也许已经注意到每个地址, 每个类型下只能对应一个具体值)。这方便地为我们提供了一个按地址索引的本地映射。 在 BasicCoin 模块中，定义了每个 Balance (钱包，余额)资源表示每个地址下持有的币的数量：

/// Struct representing the balance of each address.
struct Balance has key {
    coin: Coin // same Coin from Step 1
}

区块链状态(Move blockchain state)看起来大致如下：

进阶主题 (Advanced topics) ：

public(script) fun transfer(from: signer, to: address, amount: u64) acquires Balance { ... }

4.BasicCoin 模块（Module）的实现

我们已经在 step_4 文件夹上创建了名叫 BasicCoin 的 Move 包。sources 文件夹包含所有的 Move 包(package)的模块源码，包括 BasicCoin.move。在本节中，我们将仔细研究 BasicCoin.move 内部方法的实现。

编译代码

首先尝试在文件夹step_4/BasicCoin中运行以下命令，使用 Move 包构建代码：

move build

方法的实现

现在仔细看看 BasicCoin.move 中内部方法的实现。

let empty_coin = Coin { value: 0 };
move_to(account, Balance { coin:  empty_coin });

assert!(signer::address_of(&module_owner) == MODULE_OWNER, errors::requires_address(ENOT_MODULE_OWNER));

deposit(mint_addr, Coin { value: amount });

borrow_global<Balance>(owner).coin.value
                 |       |       \    /
        resource type  address  field names

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 }
}

练习

在模块中有两个 TODOs，留给读者练习：

• 完成 publish_balance 方法的实现。
• 实现 deposit 方法。

此练习的解决方案可以在step_4_sol文件夹中找到。

额外练习

• 如果我们在余额中存入太多会发生什么？

5.给 BasicCoin 模块添加单元测试

在这一步中，来看看我们为覆盖在 step 4 中编写的代码而编写的所有不同的单元测试。还将看看我们可以用来帮助我们编写测试用例的一些工具。

首先，请在文件夹 step_5/BasicCoin 中运行 move 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

6.使用泛型（generic）编写 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 token standard类似，后者提供了在智能合约中实现可替代代币的接口。使用泛型的一个关键优势是能够重用代码，因为泛型模块库已经提供了标准实现，并且实例化模块可以通过包装标准实现提供定制化功能。

我们提供了一个称为MyOddCoin并实例化 Coin 类型并自定义其转移策略的小模块：只能转移奇数个代币。其还包括两个 tests 来测试这种行为。你可以使用在第 2 步和第 5 步中学到的命令来运行测试。

进阶主题：

进阶步骤

在继续下一步之前，确保您已安装所有的验证器依赖项。

尝试运行 boogie /version。如果出现错误消息“找不到命令：boogie”，你将必须运行安装脚本并更新环境配置(source ~/.profile)：

# run the following in move repo root directory
./scripts/dev_setup.sh -yp
source ~/.profile

7.使用 Move prover

部署在区块链上的智能合约可能会操纵高价值资产。作为一种使用严格的数学方式来描述计算机系统的行为和推理正确性的技术，形式化验证已被用于区块链，以防止智能合约中错误的产生。 Move验证器是一种在进化中、用Move 语言编写的智能合约形式化验证工具。用户可以使用Move语言规范(Move Specification Language (MSL))指定智能合约的功能属性，然后使用验证器自动静态检查它们。 为了说明如何使用验证器，我们在BasicCoin.move中添加了以下代码片段：

    spec balance_of {
        pragma aborts_if_is_strict;
    }

通俗地说，代码块 spec balance_of {...} 包含 balance_of 方法的属性规范说明。

首先在BasicCoin directory目录中使用以下命令运行验证器。

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
   │           ------------- 由于执行失败这里发生中止
   ·
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
   =         中止

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 模块编写形式化规范（formal specification）

fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance

    spec withdraw {
        let balance = global<Balance<CoinType>>(addr).coin.value;
        aborts_if !exists<Balance<CoinType>>(addr);
        aborts_if balance < amount;
    }

    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 };
    }

fun deposit<CoinType>(addr: address, check: Coin<CoinType>) acquires Balance

    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;
    }

public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance

    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
   ┌─ ./sources/BasicCoin.move:57:9
   │
62 │         ensures balance_from_post == balance_from - amount;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   ...