External trait attributes

[mrRachar]

Changes

• External trait attributes replace addressed external traits with a more versatile syntax, allowing Libra to be represented in Flint 956a427 @mrRachar
• Improved Move IR generation diagnostics c45e54e @mrRachar
• Updates to documentation to include Move information and installation instructions 6cd516f @mrRachar

External trait attributes

Although the Solidity translation only allows for external contracts, in Move contracts don't exist (although a module/resource combination can mimic them, and is what the Move translation does), and structs and resources play a much more important role. Their use is so ubiquitous, especially in contexts such as money, that the Move translation needs to interface with them. However, it is still important that traditional contract-style setups can be handled to allowing interfacing with other resources on the Libra block-chain.

As external traits are so target dependant, providing a way to deal with target-language code, it seems sensible to have a way to tell the compiler more information about the external trait, a sort of compiler directive. This could also allow the compiler to know about which external traits describe data, and which describe other contracts.

To solve this external trait attributes have been implemented, which work similarly to the already-implemented function attributes. They allow further information to be provided with the external trait to let the compiler handle different kinds and different restrictions on them. These attributes have no effect on the rest of the language, only being used, as would be expected for something external which interfaces with the target language, by the final stages which are target specific.

These external trait attributes also allow Libra to be handled by Flint. Although as of yet not standard Libra implementation has been implemented, an Move test demonstrating Libra in Flint has been provided, which shows how it can be done.

Changes to Flint

• External trait addresses introduced in Move #476 have been removed in favour of @module(address: ...) attributes
• External trait attributes introduce a new way of provided the compiler more information about an external trait

Syntax

@(<function call> | <identifier>)
external trait <name> { ... }

Move external trait attributes

Move needs a series of external trait attributes to allow it to know enough to produce accurate code. Currently the following are available, although this might be rationalised in the future:

• @module(address:) ─ This allows the module address to be provided, which is necessary for Flint to know where to import the module from. This replaces Move #476 's addressed external trait syntax as part of a more general system.

• @data ─ This indicates that the external trait provides the interface for data (such as a struct or resource) rather than for an external contract

• @resource ─ This indicates that the external trait provides the interface specifically for a MoveIR resource, and thus must be handled with care (resources are Move's equivalent of Assests, and are linear types). It must be used with the @data attribute to represent a resource datatype in MoveIR.

Example

@data
@resource
@module(address: 0x0)
external trait Libra {
  public func getValue() -> uint64
  public func withdraw(amount: uint64) -> Libra
  public func transfer(to: inout Libra)
}

contract Account {
  visible var value: Libra
}

Account :: sender <- (any) {
  public init() {
    value = Libra(0x0)
  }

  public func balance() -> Int {
    return (call! value.getValue()) as! Int
  }

  func transfer(to: inout Libra) mutates (value) {
    call! value.transfer(to: &to)
  }
}

Note: There are currently no external trait attributes for the EVM target

[SusanEisenbach]

I’m not sure that having @DaTa and @DaTa, @resource is best. Why is it better than @struct and @resource?

[SusanEisenbach]

Small query on review.

[mrRachar]

The reason we're avoiding @struct is that it poses a syntax issue, struct being a keyword, it would require an even more lenient and lax parsing rule for it. However, merging @data @resource -> @resource (or alternatively @data(type: resource), @data(resource)) are both valid alternatives that are probably going to replace the current syntax if we get time to clean it up properly at the end (as there are also some other issues in the main compiler system that this change exposed during development)