Move 教程(Move Tutorial)

Welcome to the Move Tutorial! In this tutorial, we are going to go through some steps of developing Move code including design, implementation, unit testing and formal verification of Move modules.

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

There are nine steps in total:

• Step 0: Installation
• Step 1: Writing my first Move module
• Step 2: Adding unit tests to my first Move module
• Step 3: Designing my BasicCoin module
• Step 4: Implementing my BasicCoin module
• Step 5: Adding and using unit tests with the BasicCoin module
• Step 6: Making my BasicCoin module generic
• Step 7: Use the Move prover
• Step 8: Writing formal specifications for the BasicCoin module

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

• Step 0: 安装 Move 开发环境
• Step 1: 编写第一个 Move 模块(Move Module)
• Step 2: 给模块(Module)添加单元测试
• Step 3: 设计自己的 BasicCoin 模块(Module)
• Step 4: BasicCoin 模块(Module)的实现
• Step 5: 给 BasicCoin 模块添加单元测试
• Step 6: 使用泛型(generic)编写 BasicCoin 模块
• Step 7: 使用 Move prover
• Step 8: 为 BasicCoin 模块编写形式化规范(formal specifications)

Each step is designed to be self-contained in the corresponding step_x folder. For example, if you would like to skip the contents in step 1 through 4, feel free to jump to step 5 since all the code we have written before step 5 will be in step_5 folder. At the end of some steps, we also include additional material on more advanced topics.

其中每一步都被设计为自包含的文件夹, 相应名字为 step_x。 例如，如果您愿意跳过 step 1 到 step 4 的内容，可直接跳到 step 5，因为所有在 step 5 之前的代码均在在step_5 文件夹之下。在部分步骤结束时，我们还引入有关更高级主题的附加资料。

Now let's get started!

好了，我们现在开始！

Step 0: 安装 Move 开发环境 (Step 0: Installation)

If you haven't already, open your terminal and clone the Move repository:

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

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

Go to the move directory and run the dev_setup.sh script:

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

cd move
./scripts/dev_setup.sh -ypt

Follow the script's prompts in order to install all of Move's dependencies.

The script adds environment variable definitions to your ~/.profile file. Include them by running this command:

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

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

source ~/.profile

Next, install Move's command-line tool by running this commands:

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

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

You can check that it is working by running the following command:

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

move --help

You should see something like this along with a list and description of a number of commands:

您应该会看到类似这样的内容以及许多命令的列表和描述：

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

If you want to find what commands are available and what they do, running a command or subcommand with the --help flag will print documentation.

如果想了解有支持哪引命令及其作用, 执行命令或子命令时添加 --help 标记，此时会打印帮助文档。

Before running the next steps, cd to the tutorial directory:

在执行下一步骤之前，请先执行 cd 命令进入到教程对应目录下:

cd <path_to_move>/language/documentation/tutorial

cargo install --path language/move-analyzer

Step 1: 编写第一个Move模块 (Writing my first Move module)

Change directory into the step_1/BasicCoin directory. You should see a directory called sources -- this is the place where all the Move code for this package lives. You should also see a Move.toml file as well. This file specifies dependencies and other information about the package; if you're familiar with Rust and Cargo, the Move.toml file is similar to the Cargo.toml file, and the sources directory similar to the src directory.

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

Let's take a look at some Move code! Open up sources/FirstModule.move in your editor of choice. The first thing you'll see is this:

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

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

This is defining a Move module. Modules are the building block of Move code, and are defined with a specific address -- the address that the module can be published under. In this case, the BasicCoin module can only be published under 0xCAFE.

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

Let's now take a look at the next part of this file where we define a struct to represent a Coin with a given value:

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

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

Looking at the rest of the file, we see a function definition that creates a Coin struct and stores it under an account:

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

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

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

Let's take a look at this function and what it's saying:

• It takes a signer -- an unforgeable token that represents control over a particular address, and a value to mint.
• It creates a Coin with the given value and stores it under the account using the move_to operator.

Let's make sure it builds! This can be done with the build command from within the package folder (step_1/BasicCoin):

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

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

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

move build

Step 2: 给模块(Module)添加单元测试 (Adding unit tests to my first Move module)

Now that we've taken a look at our first Move module, we'll take a look at a test to make sure minting works the way we expect it to by changing directory to step_2/BasicCoin. Unit tests in Move are similar to unit tests in Rust if you're familiar with them -- tests are annotated with #[test] and written like normal Move functions.

You can run the tests with the move test command: (原文是 package test，应该有误)

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

可以通过 move test 命令来执行测试:

move test

Let's now take a look at the contents of the FirstModule.movefile. The first new thing you'll see is this 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);
    }
}

This is declaring a unit test called test_mint_10 that mints a Coin struct under the account with a value of 10. It is then checking that the minted coin in storage has the value that is expected with the assert! call. If the assertion fails the unit test will fail.

这里声明了一个命名为 test_mint_10 的单元测试，它在 account 账户地址下铸造了一个包含 value 为 10的 Coin，然后通过 assert! 断言检查已经铸造成功并保存在(全局)存储中的 Coin 的值是否与期望值一致。如果断言 assert 执行失败，则单元测试失败。

Step 3: 设计 BasicCoin 模块(Module) (Designing my BasicCoin module)

In this section, we are going to design a module implementing a basic coin and balance interface, where coins can be minted and transferred between balances held under different addresses.

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

The signatures of the public Move function are the following:

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

Next we look at the data structs we need for this module.

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

A Move module doesn't have its own storage. Instead, Move "global storage" (what we call our blockchain state) is indexed by addresses. Under each address there are Move modules (code) and Move resources (values).

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

The global storage looks roughly like this in Rust syntax:

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

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

The Move resource storage under each address is a map from types to values. (An observant reader might observe that this means each address can only have one value of each type.) This conveniently provides us a native mapping indexed by addresses. In our BasicCoin module, we define the following Balance resource representing the number of coins each address holds:

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

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

Roughly the Move blockchain state should look like this:

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

进阶主题 (Advanced topics) ：

Only functions with public(script) visibility can be invoked directly in transactions. So if you would like to call the transfer method directly from a transaction, you'll want to change its signature to:

只有public(script)可见行的函数才能直接被交易调用，所以如果你要直接在交易内调用transfer方法，那么需要将函数签改成如下格式:

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

Read more on Move function visibilities here.

关于函数可见性的更多信息，请参阅Move function visibilities。

Step 4: 实现 BasicCoin 模块span id="Step4"> (Implementing my BasicCoin module)

We have created a Move package for you in folder step_4 called BasicCoin. The sources folder contains source code for all your Move modules in the package, including BasicCoin.move. In this section, we will take a closer look at the implementation of the methods inside BasicCoin.move.

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

编译代码 (Compiling our code)

Let's first try building the code using Move package by running the following command in step_4/BasicCoin folder:

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

move build

方法的实现 (Implementation of methods)

Now let's take a closer look at the implementation of the methods inside BasicCoin.move.

现在仔细看看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 }
}

练习 (Exercises)

There are two TODOs in our module, left as exercises for the reader:

• Finish implementing the publish_balance method.
• Implement the deposit method.

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

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

The solution to this exercise can be found in step_4_sol folder.

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

额外练习 (Bonus exercise)

• What would happen if we deposit too many tokens to a balance?
• 如果我们在余额中存入太多会发生什么？

Step 5: 在模块 BasicCoin 中添加和使用单元测试 (Adding and using unit tests with the BasicCoin module)

In this step we're going to take a look at all the different unit tests we've written to cover the code we wrote in step 4. We're also going to take a look at some tools we can use to help us write tests.

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

To get started, run the move test command in the step_5/BasicCoin folder

首先，请在文件夹 step_5/BasicCoin中 运行 move test 命令。

move test

You should see something like this:

您应该看到如下内容：

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

Taking a look at the tests in the BasicCoin module we've tried to keep each unit test to testing one particular behavior.

看看 BasicCoin 模块中的测试，我们试图让每个单元测试都测试一个具体的行为。

Step 6: BasicCoin 模块泛型化（Making my BasicCoin module generic）

In Move, we can use generics to define functions and structs over different input data types. Generics are a great building block for library code. In this section, we are going to make our simple BasicCoin module generic so that it can serve as a library module that can be used by other user modules.

在 Move 语言中，我们可以使用泛型来定义不同输入数据类型的函数和结构体。泛型是库代码的重要组成部分。在本节中，我们将使我们的简单 BasicCoin 模块泛型化，以便它可以用作其他用户模块可以使用的模块库。

First, we add type parameters to our data structs:

首先，我们将类型参数添加到我们的数据结构中：

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

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

We also add type parameters to our methods in the same manner. For example, withdraw becomes the following:

我们还以相同的方式将类型参数添加到我们的方法中。例如，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 }
}

Take a look at step_6/BasicCoin/sources/BasicCoin.move to see the full implementation.

查看step_6/BasicCoin/sources/BasicCoin.move完整的实现。

At this point, readers who are familiar with Ethereum might notice that this module serves a similar purpose as the ERC20 token standard, which provides an interface for implementing fungible tokens in smart contracts. One key advantage of using generics is the ability to reuse code since the generic library module already provides a standard implementation and the instantiating module can provide customizations by wrapping the standard implementation.

此时，熟悉以太坊的读者可能会注意到，该模块的用途与ERC20 token standard类似，后者提供了在智能合约中实现可替代代币的接口。使用泛型的一个关键优势是能够重用代码，因为泛型模块库已经提供了标准实现，并且实例化模块可以通过包装标准实现提供定制化功能。

We provide a little module called MyOddCoin that instantiates the Coin type and customizes its transfer policy: only odd number of coins can be transferred. We also include two tests to test this behavior. You can use the commands you learned in step 2 and step 5 to run the tests.

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

进阶主题 (Advanced topics):

进阶步骤 (Advanced steps)

Before moving on to the next steps, let's make sure you have all the prover dependencies installed.

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

Try running boogie /version . If an error message shows up saying "command not found: boogie", you will have to run the setup script and source your profile:

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

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

Step 7: 使用Move验证器（Use the Move prover）

Smart contracts deployed on the blockchain may manipulate high-value assets. As a technique that uses strict mathematical methods to describe behavior and reason correctness of computer systems, formal verification has been used in blockchains to prevent bugs in smart contracts. The Move prover is an evolving formal verification tool for smart contracts written in the Move language. The user can specify functional properties of smart contracts using the Move Specification Language (MSL) and then use the prover to automatically check them statically. To illustrate how the prover is used, we have added the following code snippet to the BasicCoin.move:

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

    spec balance_of {
        pragma aborts_if_is_strict;
    }

Informally speaking, the block spec balance_of {...} contains the property specification of the method balance_of.

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

Let's first run the prover using the following command inside BasicCoin directory:

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

move prove

which outputs the following error information:

它输出以下错误信息：

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

The prover basically tells us that we need to explicitly specify the condition under which the function balance_of will abort, which is caused by calling the function borrow_global when owner does not own the resource Balance<CoinType>. To remove this error information, we add an aborts_if condition as follows:

验证器大体上告诉我们，我们需要明确指定函数 balance_of 中止的条件，中止原因是 owner(函数调用者)在没有资源 Balance<CoinType> 的情况下调用 borrow_global 函数导致的。要去掉此错误信息，我们添加如下 aborts_if 条件：

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

After adding this condition, try running the prove command again to confirm that there are no verification errors:

添加此条件后，再次尝试运行prove命令，确认没有验证错误：

move prove

Apart from the abort condition, we also want to define the functional properties. In Step 8, we will give more detailed introduction to the prover by specifying properties for the methods defined the BasicCoin module.

除了中止条件，我们还想定义功能属性。在第 8 步中，我们将通过为定义 BasicCoin 模块的方法指定属性来更详细地介绍验证器。

第 8 步：为 BasicCoin 模块编写正式规范（Write formal specifications for the BasicCoin module）

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;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   ...