Deep Interpretation of the White Paper – Move: A New Programming Language for Facebook Libra Blockchain

Note: Some English proper nouns have no corresponding Chinese translation, and the original author and the Blockore team reserve the correct space for translation.

Overview and motivation

This article takes you on a preliminary look at the 26-page technical white paper on Facebook Libra's new programming language Move . As a developer of Ethereum and a blockchain community enthusiast, I hope to introduce this article quickly to everyone who is curious about this new language and let everyone know his highlights 🙂

I hope you will like it!

Summary

Move is an executable bytecode language for executing custom items and smart contracts.

Compared to Solidity, there are two things to note:

  • Move is a bytecode language that can be executed directly in Move's VM, but Solidity (Ethernet's Smart Contract Language) is a higher level language that needs to be executed before EVM (Ethernet's virtual machine) Compile into a byte code.
  • Move can be used not only for smart contracts, but also for customizations (which will be explained later in this article), while Solidity is only available for smart contracts on Ethereum.

The key feature of Move is the ability to define custom resource types with semantics inspired by linear logic: a resource can never be copied or implicitly discarded, only moved between program storage locations.

This is a feature similar to Rust. The value in Rust can only be assigned to one name at a time. If you assign a value to a different name, it will no longer be able to access the value with the previous name.

For example, the following code snippet will output an error: Use of moved value 'x' . This is because Rust has no garbage collection. When variables are out of range, the memory they reference is also freed. In simple terms, we can understand that data can only have one "owner" at a time. In the following example, x is the original owner and then y becomes the owner.

Reference: http://squidarth.com/rc/rust/2018/05/31/rust-borrowing-and-ownership.html

2. Encoding digital assets in an open system

Physical assets have two attributes that are difficult to code in digital assets:

  • Scarcity: The supply of assets in the system should be controlled. Copying an existing asset should be banned and creating a new asset should be a privilege.
  • Authority management of asset ownership: Participant assets in the system should be protected by asset control regulations.

It points out the two main characteristics of digital assets that need to be realized for physical assets. For example, rare metals are naturally scarce, while traditional physical assets do not need to be managed as rights to assets, because the money spent on the money will be handed over to the merchant, and it is not easy to have double payment of electronic cash (the same banknote can be paid multiple times) ).

To illustrate how we propose these two attributes, let us start with the following proposal:

Proposal #1: The simplest rule, no scarcity and permission management

The simplest state assessment rules, no scarcity and authority management.

  • G[K]:=n indicates that the value stored in the global area blockchain and the key K is updated to K.
  • Transaction ⟨Alice, 100⟩ means that Alice's account balance is set to 100.

The above indicates that there are serious problems:

  • Alice can have unlimited coins by sending a transaction ⟨Alice, 100⟩.
  • The coins Alice sends to Bob are worthless because Bob can use the same technology to send an unlimited amount of tokens to himself.

Proposal #2: Considering scarcity

The second proposal only considers scarcity

Now we are forced to set the number of coins stored under the transfer before the transfer to at least ?.

However, while this solves the scarcity problem, there is no ownership check for people who can send money to Alice. (Anyone can do this according to this evaluation rule)

Proposal #3: Consider both scarcity and rights management


The third proposal considers scarcity and rights management at the same time

We deal with this problem by using the digital signature mechanism verify_sig before checking for scarcity. This means that Alice uses her private key to sign the transaction and proves that she is the owner of the token.

2.1 Existing blockchain language

The existing blockchain language faces the following issues (all of which have been resolved in Move):

  • Indirectly representing assets: Assets are encoded using integers, but integer values ​​are not essentially the same as assets. In fact, there are currently no types or values ​​representing Bitcoin/Ether/StrawCoin! This makes writing programs that use assets inconvenient and error-prone. Patterns such as the process of transferring assets into or out of assets, or storing assets in a data structure, require some special support from the programming language.
  • Scarcity is not scalable: this language represents only a scarce asset. In addition, scarcity protection is hard-coded directly in the semantics of programming languages. When programmers want to create custom assets, they must carefully implement the scarcity feature without language support.

These are the problems in the Ethereum smart contract. Custom assets such as ERC-20 tokens use integers to represent their value and their total supply. Whenever a new token is generated, the smart contract code must manually check for scarcity (in this case, total supply).

In addition, due to the indirect representation of asset issues, it is more likely to introduce serious errors such as duplication, reuse or asset loss.

  • Permission management is not flexible: the existing model architecture, the only strategy for enforcing permission management, is based on the signature of the public key. Like scarcity protection, the rights management strategy is deeply embedded in the semantics of programming languages. The answer is not obvious as to how the language can be extended and the programmer is allowed to develop a custom rights management strategy.

The same is true in Ethereum, where smart contracts do not have any native language support in the process of using public key-private key cryptography for rights management. Developers must manually write rights management, such as using OnlyOwner .

Despite my loyal fans of Ethereum, I agree that these asset attributes should be supported by the language itself for security purposes.

In particular, moving Ethernet to smart contracts involves dynamic scheduling, which leads to a new class of errors called re-intrusion loopholes.

Dynamic scheduling here means that the code execution logic will be determined at runtime (dynamic) rather than at compile time (static). Therefore, in Solidity, when Contract A calls the function of Contract B, Contract B can run the code that the designer of Contract A did not anticipate, which may lead to a re-invasion of the vulnerability (Contract A accidentally performs the function of Contract B, so that The funds are withdrawn before the actual deduction of the account balance).

3. Move design concept

3.1 First-class resources

At a higher level, the relationship between modules/resources/procedures in Move is similar to the relationship between classes/objects/methods in the object-oriented program. Move's module is similar to smart contracts in other blockchain languages. Module declares the resource type and procedure. These resource types and programs are used to code the rules when creating, destroying, and updating their declared resources.

Modules/resources/procedure is just some of the terms in Move. We will use an example to illustrate these later in this article 😉

3.2 Flexibility

Move adds flexibility to Libra through (transaction scripts). Each Libra transaction contains a transaction script, which is actually the main process of the transaction.

Scripts can execute expressive one-off behaviors (such as paying a specific set of recipients) or reusable behavior (by calling a single program that encapsulates reusable logic)

From the above we can see that Move's transcation script introduces more flexibility because it can achieve one-time behavior and reusable behavior, while Ethereum can only perform reusable behavior (this is a call to a single smart contract) Methods). The reason it was named "reusable" is because the smart contract feature can be executed multiple times.

3.3 Security

The execution format of Move is a typed byte code that is more advanced than the assembly language but lower level than the source language. The byte code checks the resource, type, and memory security on the chain by the bit code verifier, which is then directly executed by the bytecode interpreter. This option allows Move to provide security guarantees that are typically associated with the source language, but does not add the source compiler to a trusted computing library or compile the cost to the critical path of executing the transaction.

For Move, being a bytecode language is a very succinct design. Since it doesn't need to be compiled from source code to bytecode like Solidity, there is no need to worry about failures or attacks that might occur in the compiler.

3.4 Verifiability

Our approach is to perform as much as possible on-chain verification of critical security attributes, but at the same time design Move to support static verification tools under the advanced chain.

From here we can see that Move prefers to perform static verification instead of performing chain verification. Still, as they are mentioned at the end of the paper, verification tools are left for future development.

3.5 Modularization

The Move module enforces data abstraction and localizes key operations on the resource. The package used by the module, combined with the protection enforced by the Move system, ensures that the properties of the module type are not affected by the code external to the module.

This is also a very good data abstract design! This means that the data in the smart contract can only be modified within the scope of the contract, and cannot be modified from the outside.

From: https : //libra.org/en-US/open-source-developers/#move_carousel

4. Move overview

The transaction script for this example demonstrates a malicious or careless programmer who cannot violate the critical security invariants of the module resources outside the module.

This section will introduce you to the modules, modules, resources, and procedures in writing a programming language.

4.1 Peer-to-peer payment transaction script

The currency amount will be transferred from the sender of the transaction to the payee

Here are a few new symbols (red small text is my own note XD):

  • 0x0 : store the account address of the module
  • Currency : the name of the module
  • Coin :resource type
  • Coin is a value returned by the procedure. It is a resource value of type 0x0.Currency.Coin
  • Move() : This value cannot be used again
  • Copy() : This value can be used later

Code details:

In the first step, the sender calls the procedure named withdraw_from_sender from the module stored in 0x0.Currency.

In the second step, the sender transfers the funds to the payee by moving the resource value of the currency to the deposit of the 0x0.Currency module.

Here are 3 code examples that will be rejected:

1. Copy move(coin) to copy(coin) to copy the currency amount

Resource values ​​can only be moved. Attempting to copy a resource value (for example, using copy(coin) in the above example) will result in an error in the bytecode verification.

Because coin is a resource value, it can only be moved.

2. Re-use the currency by moving (coin) twice

Adding 0x0.Currency.deposit(copy(some_other_payee), move(coin)) to the example above will cause the sender to "spend" twice the currency – the first time with the payee, the second with some_other_payee. This bad behavior cannot be achieved in the case of physical assets. Fortunately, Move will not allow the implementation of such programs.

3. Lose money by removing move(coin)

When a mobile resource fails (for example, by deleting the line containing the move(coin) in the example above), the bytecode verification error will be triggered. This prevents programmers who use Move from accidentally or intentionally losing track of resources.

4.2 Currency module

4.2.1 Getting Started: Move execution model

Each account can contain zero or more modules (for the rectangle above) and one or more resource values ​​(for the cylinder above). For example, an account at address 0x0 has a module 0x0.Currency and a resource value of type 0x0.Currency.Coin. The account at address 0x1 has two resource values ​​and one module; the account at address 0x2 has two modules and one resource value.

Some noteworthy points:

  • Execution of the transaction script is all or nothing
  • Module is a long-term code published in a global state
  • The global state structure is a map from the account address to the account
  • The account can only contain at most one resource value of a given type, and a module with the given name (the account at address 0x0 is not allowed to contain other resources of type 0x0.Currency.Coin or another module named Currency. group)
  • The address of the declaring module is part of the type (0x0.Currency.Coin and 0x1.Currency.Coin are different types that cannot be used interchangeably)
  • The programmer can still customize multiple wrapped instances of a given resource type in the account by defining a packaged resource ( resource TwoCoins { c1: 0x0.Currency.Coin, c2: 0x0.Currency.Coin } )
  • Rules are fine, as long as you can still reference resources by their name without conflicts, for example you can reference both resources using TwoCoins.c1 and TwoCoins.c2.

4.2.2 Declaring currency resources

A module group called Currency and a resource type called Coin managed by the module

Some noteworthy points:

  • Coin is a structure type whose single field value type is u64 (64-bit unsigned integer)
  • Only the procedure of the Currency module can create or destroy values ​​of type Coin.
  • Other modules (modules) and transaction scripts (transaction scripts) can only write or reference fields of values ​​through the module's exposed procedure.

4.2.3 Implementing deposits

This process uses the Coin resource as an input and combines it with the Coin resource stored in the payee's account by following these steps:

  1. Destroy the input Coin and record its value.
  2. Get a reference to the unique Coin resource stored under the payee account.
  3. Increase the value of the payee Coin by passing the value of Coin to the procedure.

Some noteworthy points:

  • Unpack, BorrowGlobal is a built-in procedure (program)
  • Unpack<T> is the only way to delete a resource of type T. It takes a resource of type T as input, destroys it, and returns the value of the field bound to the resource.
  • BorrowGlobal<T> takes the address as input and returns a reference to the unique type T instance published under this address. &mut Coin is a mutable reference to the Coin resource, not to Coin

4.2.4 Implementing withdraw_from_sender

This procedure (procedure):

  1. Get a reference to the unique resource of the Coin type published under the sender's account.
  2. Reduce the value of the referenced Coin by the amount of input.
  3. Create and return a new Coin with a value of the amount.

Some noteworthy points:

  • Anyone can call Deposit, but withdraw_from_sender has a limit, it can only be managed by the permissions of the coin owner.
  • GetTxnSenderAddress is similar to msg.sender in Solidity
  • RejectUnless is similar to require in Solidity. If this check fails, execution of the current transaction script will stop and any actions it performs will not be applied to the global state
  • Pack<T> is also a built-in procedure (procedure), which is used to create a new resource of type T. Similar to Unpack<T>, Pack<T> can only be called within the declaration module of resource T.

to sum up

Now that you have a preliminary understanding of the main features of Move, its difference from Ethereum, and its basic syntax.

Finally, I highly recommend reading the original text of the white paper . It contains a lot of details about the principles of programming language design and many good references.

Thank you very much for your reading time. Any suggestions are welcome!

Author: Li Tingting

Translation: Blockore