rahxephon89/move-hackathon-tutorial

Move tutorial for the hackathon happening on Dec 7-8

move-hackathon-tutorial

Move tutorial for the hackathon happening on Dec 7-8

Step 0

• Run the setup script to install Move CLI, Shuffle and dependencies:

$ sh step_0/setup.sh

• Include environment variable definitions in ~/.profile by running this command:

$ . ~/.profile

Once this is done, you can alias the move package command to to mpm:

$ alias mpm = "<path_to_diem_repo>/target/debug/df-cli package"
$ alias shuffle = "<path_to_diem_repo>/target/debug/shuffle"

You can check that it is working by running mpm -h. You should see something like this along with a list and description of a number of commands:

move-package 0.1.0
Package and build system for Move code.

USAGE:
    move package [FLAGS] [OPTIONS] <SUBCOMMAND>
...

There is official Move support for VSCode, you can install this extension by opening VSCode and searching for the "move-analyzer" package and installing it. Detailed instructions can be found here.

Step 1: Write my first Move module

To create your first Move module, we first need to create a Move package by calling

$ mpm new <pkg_name>

Now change directory into the package you just created

$ cd <pkg_name>

and look around. You should see a directory called sources -- this is the place where all the Move code for this package will live[1]. You should also see a Move.toml file which specifies dependencies and other information about this package, we'll explore this in a bit. 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.

Let's write some code! Open up sources/FirstModule.move in your editor of choice.

Modules are the building block of Move code, and they always are defined relative to a specific address -- the address that they can be published under. So let's start out by defining our first module, and look at the different parts:

module NamedAddr::Coin {
}

This is defining the module Coin that can be published under the named address NamedAddNamedAddr. Named addresses are a way to parametrize the source code, so that we can compile this module using different values for NamedAddr to get different bytecode.

Let's now define and assign the named address NamedAddr the value 0xDEADBEEF. We can do this by opening the Move.toml in your favorite editor and adding the following:

[addresses]
NamedAddr = "0xDEADBEEF"

Let's now see if it works!

$ mpm build

Let's now define a structure in this module to represent a Coin with a given value:

module NamedAddr::Coin {
    struct Coin has key {
        value: u64,
    }
}

Structures in Move can be given different abilities that describe what can be done with that type. There are four different abilities in Move:

• copy: Allows values of types with this ability to be copied.
• drop: Allows values of types with this ability to be popped/dropped.
• store: Allows values of types with this ability to exist inside a struct in global storage.
• key: Allows the type to serve as a key for global storage operations.

So in this module we are saying that the Coin struct can be used as a key in global storage, and because it has no other abilites, it cannot be copied, dropped, or stored as a non-key value in storage.

We can then add some functions to this module, functions are default private, and can also be public, or public(script). The latter states that this function can be called from a transaction script. public(script) functions can also be called by other public(script) functions.

Let's check that it can build again

$ mpm build

Let's now add a function that mints coins and stores them under an account:

module NamedAddr::Coin {
    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 one of the five different global storage operators move_to. This is where the key ability is imporant -- we couldn't call move_to on Coin unless it had the key ability!

Let's make sure it compiles now:

$ mpm build

Step 2: Add unit tests to my first Move module

Now that we've written our first Move module, lets

Adding dependencies

Exercise?

• Implement withdraw and deposit and add tests for them

Step 3: Design 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 under different addresses.

The signatures of the public Move function are the following:

public fun balance_of(owner: address): u64 acquires Balance;
public(script) fun transfer(from: signer, to: address, amount: u64) acquires Balance;

At the end of each function signature is an acquires list containing all the resources defined in this module accessed by the function.

Notice that balance_of is a public function while transfer is a public script function. Similar to Ethereum, users submit signed transactions to Move-powered blockchains to update the blockchain state. We can invoke transfer method in a transaction script to modify the blockchain state. As mentioned in Step 1, only public script functions can be called from a transaction script. Therefore, we declare transfer as a public script function. And by requiring the from argument be a signer instead of an address, we require that the transfer transaction must be signed by the from account.

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

In most Ethereum contracts, the balance of each address is stored in a state variable of type mapping(address => uint256). This state variable is stored in the storage of a particular smart contract. In Move, however, storage works differently. 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).

The global storage looks roughly like

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:

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

TODO: change the diagrams to get rid of total supply

Roughly the Move blockchain state should look like this: In comparison, a Solidity blockchain state might look like this:

Step 4: Implement my BasicCoin module

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

Method initialize

Unlike Solidity, Move doesn't have a built-in constructor method called at the instantiation of the smart contract. We can, however, define our own initializer that can only be called by the module owner. We enforce this using the
assert statement:

assert!(Signer::address_of(&module_owner) == MODULE_OWNER, ENOT_MODULE_OWNER);

Assert statements in Move can be used in this way: assert!(<predicate>, <abort_code>);. This means that if the <predicate> is false, then abort the transaction with <abort_code>. Here MODULE_OWNER and ENOT_MODULE_OWNER are both constants defined at the beginning of the module.

We then perform two operations in this method:

1. Publish an empty Balance resource under the module owner's address.
2. Deposit a coin with value total_supply to the newly created balance of the module owner.

Method balance_of

Similar to total_supply, we use borrow_global, one of the global storage operators, to read from the global storage.

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

Method transfer

This function withdraws tokens from from's balance and deposits the tokens into tos balance. We take a closer look at withdraw helper function:

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

At the beginning of the method, we assert that the withdrawing account has enough balance. We then use borrow_global_mut to get a mutable reference to the global storage, and &mut is used to create a mutable reference to a field of a struct. We then modify the balance through this mutable reference and return a new coin with the withdrawn amount.

Compiling our code

Now that we have implemented our BasicCoin contract, let's try building it using Move package by running the following command in step_4/BasicCoin folder:

$ mpm build

Exercises

There is a TODO in our module, left as an exercise for the reader:

• Implement deposit method.

The solution to this exercise can be found in step_4_sol.

Bonus exercises

• What would happen if we deposit too many tokens to a balance?
• Is the initializer guaranteed to be called before anything else? If not, how can we change the code to provide this guarantee?

Step 5: Add unit tests to my BasicCoin module

Step 6: Make my BasicCoin module generic

Emphasize key advantage of generics in Move:

• unlike ERC20, we can reuse code
• provide an actual standard implementation as a library module

Advanced steps

Step 7: Write formal specifications for my BasicCoin module

The blockchain requires high assurance. Smart contracts deployed on the blockchain may maniputate high-value assets, which are targets of highly-motivated and well-resourced adversaries. Hundreds of millions of dollars have been lost from bugs on other blockchains. 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. It supports complete specification of functional properties of smart contracts. Properties can be verified automatically efficiently (only slightly slower than a linter). Moreover, it can be integrated in the CI system for re-verification after every change to the code base. In this step, we will define the formal specification of the BasicCoin module.

The property specification is written in the Move Specification Language (MSL). Developers can provide pre and post conditions for functions, which include conditions over (mutable) parameters and global memory. Developers can also provide invariants over data structures, as well as the (state-dependent) content of the global memory. Universal and existential quantification both over bounded domains (like the indices of a vector) as well of unbounded domains (like all memory addresses, all integers, etc.) are supported. In this tutorial, we will learn how to define functional properties for methods.

Method withdraw

The signature of the method withdraw is given below:

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

The method withdraws tokens with value amount from the address addr and returns a created Coin of value amount. The specification is defined in the spec withdraw block:

   spec withdraw {
        // The property of the method withdraw is defined here.
    }

For a function, we usually want to define when it aborts, the expected effect on the global memory, and its return value. MSL provides aborts_if to define conditions under which the function aborts. The method withdraw aborts when 1) addr does not have the resource Balance<CoinType> or 2) the number of tokens in addr is smaller than amount. We can define conditions like this:

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

As we can see here, a spec block can contain let bindings which introduce names for expressions. global<T>(address): T is a built-in function that returns the resource value at addr. balance is the number of tokens owned by addr. exists<T>(address): bool is a built-in function that returns true if the resource T exists at address. Two aborts_if clauses correspond to the two conditions mentioned above. In general, if a function has more than one aborts_if condition, those conditions are or-ed with each other. By default, if a user wants to specify aborts conditions, all possible conditions need to be listed. Otherwise, the prover will generate a verification error. However, if pragma aborts_if_is_partial is defined in the spec block, the combined aborts condition (the or-ed individual conditions) only imply that the function aborts. The reader can refer to the MSL document for more information.

The next step is to define functional properties, which are described in the two ensures clauses below. First, by using the let post binding, balance_post represents the balance of addr after the execution, which should be equal to balance - amount. Then, the return value (denoted as result) should be a coin with value 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 };
    }

Method deposit

The signature of the method deposit is given below:

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

The method deposits the check into addr. The specification is defined below:

    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 represents the number of tokens in addr before execution and check_value represents the number of tokens to be deposited. The method would abort if 1) addr does not have the resource Balance<CoinType> or 2) the sum of balance and check_value is greater than the maxium value of the type u64. The functional property checks that the balance is correctly updated after the execution.

Method transfer

The signature of the method transfer is given below:

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

The method transfers the amount of coin from the account of from to the address to.

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 addr_from != to ==> balance_from_post == balance_from - amount;
        ensures addr_from != to ==> balance_to_post == balance_to + amount;
        ensures addr_from == to ==> balance_from_post == balance_from;
    }

The function Signer::address_of is called to obtain the address of from. Then the balances of addr_from and to before and after the execution are obtained. In the three ensures clauses, p ==> q is used to represented the logical implication between p and q. If the source and the target addresses are the same, the balance remains the same. Otherwise, amount is deducted from addr_from and added to to. The aborts conditions are left as an exercise.

Exercises

• Implement the aborts_if conditions for the transfer method.
• Implement the specification for the initialize and publish_balance method.

The solution to this exercise can be found in step_7_sol.

Step 8: Formally verify my BasicCoin module using Move Prover

We can use the command mpm -p <path/to/BasicCoin> prove to prove properties for the BasicCoin module. More prover options can be found here.

Footnotes

[1] Move code can also live a number of other places, but for more information on that see the documentation on Move packages.

Notes (to be removed in final version):

• We should base things on the assumption that these steps will be run in the Diem repo at the end.