Move

[mrRachar]

Changes

• Support for Flint translation to Move, the IR language for Facebook's Libra block-chain, through a new compiler target @matteobilardi @mrRachar

Move support

Move is the IR language for Facebook's new Libra block-chain. Currently, Libra doesn't have a higher-level language targeting it, and so this is an attempt to make Flint the first high-level language to target Libra. This includes a complete translation for all non-external Flint constructs and external traits, however, LibraCoin support has proven difficult and is yet unimplemented. Doing so has required some changes to the compiler to allow multiple targets; some of the ground work for which has already been included and used upstream, however, most of it will come with this pull request.

Changes to Flint

• Addressed external traits: To allow MoveIR support, where implementation and instance are separated, external traits can now be optionally addressed: external trait 0x1337.TraitName { ... }. This is ignored in the Solidity translation, as it has no meaning there, and may produce a warning in the future
• Solidity types are now known as external types─this is almost entirely a back-end change, but also affects documentation

Mathematical and logical operations

Basic mathematical and logical operations are converted using the built-in operators in Move. As Move will revert on overflow, there is now no need to differentiate between overflow-safe and overflowing operators, so both are translated to the same raw Move operator. There is, however, no power operator in Move. This is resolved through an iterative power computation over integers provided in the Move runtime, which any power operations ** end up using.

Contract and behaviour declarations

As Move splits up data from actions through its module and resources system, we needed to settle on a standard transformation into Move for Flint's contract construct. The translation involves creating a resource T to hold contract properties, inside a module which has the same name as the contract. Then any methods provided in behaviour declarations on the contract take in the resource as the first argument. This means roughly the follow translation occurs:

contract A {
  var a: Int = 0
}

Contract :: (any) {
  func f(x: Int) -> {
    return x + a
  }
}

is translated to

module Contract {
  resource T {
    a: u64
  }

  // This is not exactly what happens,
  //  see wrapper methods and automatic reference handling below
  f(this: &mut T, x: u64): u64 {
    return *&move(this).a + copy(x);
  }
}

Wrapper methods

To allow calls into our Move module, we provide wrapper methods which take in an address and borrows the resource published at that address. That means that the actual translation of f above is closer to:

public f(__this_address: address, x: u64): u64 acquires T {
  let this: &mut T;
  this = borrow_global<T>(address);
  return f(move(this), move(x))
}

Contract$f(this: &mut T, x: u64): u64 { ... }

These wrapper functions are only used as entry points (and thus only generated for public functions) to the Flint contract from other Move modules.

Automatic reference handling

Move has a complex system of referencing, moving, and copying. Flint on the other hand doesn't have any of these concepts, so the compiler has to infer and generate the necessary code, including releasing references when they're finished. References may also only be used once per statement (due to all references generated being mutable); double reference protection makes sure that if two references are used, they are split into multiple statements. Also, as the function cannot return until the references are released but the return statement might require those references, an intermediary variable must store the return value. Thus the innocent looking

public func area() -> Int {
  return rectangle.width * rectangle.height
}

ends up in the Move translation as the slight less clear

area(this: &mut Self.T): u64 {
  let ret: u64;
  let _$temp$3: &mut Self.Rectangle;
  _$temp$3 = &mut copy(this).rectangle;
  ret = (*&mut copy(_$temp$3).width * *&mut copy(_$temp$3).height);
  _ = move(_$temp$3);  // This is how references are currently released in Move
  _ = move(this);
  return move(ret);
}

Some pre-assigments are also down to limited operations allowed within arguments to functions and only one level deep of x.y permitted at a time.

Constructors

In Move an object cannot be constructed until all the properties are known. This means that until all variables have been assigned, no other methods may be called from a constructor. To simulate instance variables, every field is accessible initially as a separate variable which can be used and assigned. These are then used to construct the object.

public Rectangle$new$Int_Int(size: u64): Self.Rectangle {
  let __this_width: u64;
  let __this_height: u64;
  __this_width = copy(_size) * 2;              // self.width = size * 2
  __this_height = copy(__this_width) / 2;      // self.height = width / 2
  return Rectangle {
    width: move(__this_width),
    height: move(__this_height)
  };
}

If the constructor does contain further operations, such as re-assignments or function calls, the Move resource is constructed, and then a reference is generated which is used exactly as if you weren't in a constructor. The following translation shows all cases of operations involving self in a constructor:

contract C {
  var v: V = V(2)
  var u: Int
}

C :: (any) {
  public init() {
    u = 1
    self.v = V(3)   // First re-assignment, as v already has a default assignment
    v.x = 4
    v()
    u = 2
    let x: Int = u
    assert(u == x)
  }
}

... // Struct V declared elsewhere

is translated to

module C {
  resource T {
    v: Self.V,
    u: u64
  }

  new(): Self.T {
    let _flint$self_raw: Self.T;
    let this: &mut Self.T;
    let __this_v: Self.V;
    let __this_u: u64;
    let _$temp$1: &mut Self.V;
    let _x: u64;
    __this_v = Self.V$new$Int(2);
    __this_u = 1;
    _flint$self_raw = T {
      u: move(__this_u),
      v: move(__this_v)
    };
    this = &mut _flint$self_raw;  // Switch to reference to self rather than independent variables.
    *&mut copy(this).v = Self.V$new$Int(3);
    _$temp$1 = &mut copy(this).v;
    *&mut copy(_$temp$1).x = 4;
    _ = move(_$temp$1);
    Self.C$v(copy(this));  // `this` reference needed for method call
    *&mut copy(this).u = 2;
    _x = *&mut copy(this).u;
    Self.Flint$Global$assert$Bool((*&mut copy(this).u == copy(_x)));
    _ = move(this);
    return move(_flint$self_raw);
  }
}

If a programme contains a method call before the instance can be constructed, this will result in a compilation error. This is seen as reasonable as the semantics of undefined properties are questionable at best, especially in Move, and code which does this should be refactored anyway.

Type states and caller protections

Type states and caller protections are implemented through assertions in the external wrapper methods. This means any attempt to call the function externally whilst in the wrong state or without permission will result in the transaction reverting. It was not seen as necessary to add protections in internal methods as Flint's semantic analyser will ensure correctness. The error thrown on an incorrect call is the line number in Flint to allow easier debugging and testing.

public increment(__address_this: address) acquires T {
  let __caller: address;
  let this: &mut Self.T;
  this = borrow_global<T>(move(__address_this));
  __caller = get_txn_sender();  // This is implementing caller protections, so get the caller's address
  assert((*&mut copy(this).owner == copy(__caller)), 14);  // 14 is the line number in Flint for this function
  Self.Counter$increment(copy(this));
  _ = move(this);
  return;
}

Structs, in-out arguments, and local struct variables

Structs are translated similarly to contracts, with methods converted into functions with the receiver as the first argument. The difference is no wrapper methods are generated, and the datatype created is a struct not a resource, named the same as the Flint struct. In-out arguments are translated to a reference type to allow structs to be passed around in the Move in a way which preserves the semantics of Flint.

Local structs however cannot be references, since they must be stored somewhere. Thus these are actually handled in Move as raw structs, and are referenced by the ARH when necessary (as is inevitably the case as Move requires references for operations such as property access, and all Flint functions take in struct references)

var v: V = V(1)
assert(v.x == 1)
v.x = 2

let _v: Self.V;
let _$temp$3: &mut Self.V;
let _$temp$5: &mut Self.V;
_v = Self.V$new$Int(1);
_$temp$3 = &mut _v;
Self.Flint$Global$assert$Bool((*&mut copy(_$temp$3).x == 1));
_ = move(_$temp$3);
_$temp$5 = &mut _v;
*&mut copy(_$temp$5).x = 1;
_ = move(_$temp$5);
_ = move(this);
return;

External traits

As Move separates behaviour and state, Flint needs two addresses, one of which should be the same for all instances, and is instead related to the type. To allow the module address to be specified, a change to the language has been instituted where an address may proceed an external trait name. This is currently optional throughout all common steps of the compiler, being ignored if present in the Solidity translation and may in the future be disallowed there, but is necessary for targeting Move.

External traits allow Flint-written code to interact with other Move modules, as long as they meet the the same interface as the translation of a Flint contract into Move. This means resources must be published at an address, and methods take this address as their first argument. Unfortunately, this also means structs cannot currently be handled, which is the current barrier to full Libra implementation (although you can access LibraAccounts in Move if you provide the interface). This requirement means a Move module that interfaces with Flint for the following external trait:

external trait 0x1337.BaseCounter {  // 0x1337 is the adddress the module is published
  public func add(n: uint64)

  public func count() -> uint64
}

must look something like

module Counter {
  resource T {
    value: u64
  }

  public publish(start: u64) {
    let t: Self.T;
    t = T { value: move(start) };
    move_to_sender<T>(move(t));
    return;
  }

  public add(this_address: address, n: u64) acquires T {
    let this: &mut Self.T;
    let newValue: u64;
    this = borrow_global<T>(move(this_address));
    newValue = *&copy(this).value + move(n);
    *&mut copy(this).value = move(newValue);
    _ = move(this);
    return;
  }

  public count(this_address: address): u64 acquires T {
    let this: &mut Self.T;
    this = borrow_global<T>(move(this_address));
    return *&move(this).value;
  }
}

In Flint code external traits may be used exactly as expected. The need for this particular interface (functions taking in an address) is not seen as a large problem as a programmer can wrap a different style Move module in a module with this style of interface.

Test suite

To ensure that the Move translation works as expected, and doesn't break as the compiler develops, a test suite has been implemented in Python. This allows Flint files to be tested through compilation (in Move if it compiles it must have been verified), or provided with a .mvir file of the same name which will interact with the Flint contract to test its functionality. It also provides two testing directives, //! expect fail <line-number> and //! provide module which allow respectively tests to be expected to fail, and external Move modules to be provided. More information is provided in the test runner programme and the tests should provide enough information on how to write further tests. Currently the following tests pass

• assert
• callerprotections-counter
• counter
• defaultparams
• enums
• externaltraits-counter
• factorial
• forloop
• inits
• memory
• operators
• propertymodification
• rockpaperscissors
• self
• shapes
• structs
• traits
• typestates-counter

Basic standard library

The full complement of the EVM target standard library is not supported as of yet in the Move translation, as money is currently not supported in the translation. However, other functionality is currently supported:

• assert(p: Bool)
• fatalError()

Future work

• Add an implementation of either external traits of structs (as well as contracts), or a special case built-in Libra implementation
• Target future Move features such as vectors after they are released

[SusanEisenbach]

Is there any problem that might arise when skipping verifier?

[mrRachar]

@SusanEisenbach There shouldn't be, the verifier is skip-able anyway with the command line option. The verifier is unfortunately very built around Ethereum─has Wei built in, etc.─and so we can't just verify programmes for Move IR without a little work, which is not seen as a priority. As variable specific mutates checking has been moved into the semantic analyser, you don't lose the core Flint guarantees, do any useless work, or have to fill things in that aren't used with dummy values as had to be done before when skipping the verifier.