Grammar

Identifiers

f ∈ FieldName     // [a-zA-Z$_][a-zA-Z0-9$_]*
p ∈ ProcedureName // [a-zA-Z$_][a-zA-Z0-9$_]*
m ∈ ModuleName    // [a-zA-Z$_][a-zA-Z0-9$_]*
n ∈ StructName    // [a-zA-Z$_][a-zA-Z0-9$_]*
x ∈ Var           // [a-zA-Z$_][a-zA-Z0-9$_]*

Types

k ∈ Kind ::=
  | R // Linear resource struct value. Must be used, cannot be copied
  | V // Non-resource struct value. Can be silently discarded, can be copied

g ∈ GroundType ::=
  | bool
  | u64       // unsigned 64 bit integer
  | address   // 32 byte account address
  | bytearray // immutable, arbitrarily sized array of bytes

d ∈ ModuleAlias ::=
  | m         // module name that is an alias to a declared module, addr.m
  | Self      // current module

t ∈ BaseType ::=
  | g     // ground type
  | k#d.n // struct 'n' declared in the module referenced by 'd' with kind 'k'
          // the kind 'k' cannot differ from the declared kind

𝛕 ∈ Type ::=
  | t      // base type
  | &t     // immutable reference to a base type
  | &mut t // mutable reference to a base type

𝛕-list ∈ [Type] ::=
  | unit            // empty type list.
                    // in the actual syntax, it is represented by the abscense of a type
  | 𝛕_1 * ... * 𝛕_j // 'j' >= 1. list of multiple types. used for multiple return values

Values

u ∈ Unsigned64        // Unsigned, 64-bit Integer
addr ∈ AccountAddress // addresses of blockchain accounts
bytes ∈ ByteArray     // byte array of arbitrary length
v ∈ Value ::=
  | true
  | false
  | u        // u64 literal
  | 0xaddr   // 32 byte address literal
  | b"bytes" // arbitrary length bytearray literal

Expressions

o ∈ VarOp ::=
  | copy(x) // returns value bound to 'x'
  | move(x) // moves the value out of 'x', i.e. returns the value and makes 'x' unusable

r ∈ ReferenceOp ::=
  | &x        // type: 't -> &mut t'
              // creates an exclusive, mutable reference to a local
  | &e.f      // type: '&t_1 -> &t_2' or '&mut t_1 -> &mut t_2'
              // borrows a new reference to field 'f' of the struct 't_1'. inherits exclusive or shared from parent
              // 't_1' must be a struct declared in the current module, i.e. 'f' is "private"
  | *e        // type: '&t -> t' or '&mut t -> t'. Dereferencing. Not valid for resources

e ∈ Exp ::=
  | v
  | o
  | r
  | n { f_1: e_1, ... , f_j: e_j } // type: '𝛕-list -> k#Self.n'
                                   // "constructor" for 'n'
                                   // "packs" the values, binding them to the fields, and creates a new instance of 'n'
                                   // 'n' must be declared in the current module
  // boolean operators
  | !e_1
  | e_1 || e_2
  | e_1 && e_2
  // u64 operators
  | e_1 >= e_2
  | e_1 <= e_2
  | e_1 > e_2
  | e_1 < e_2
  | e_1 + e_2
  | e_1 - e_2
  | e_1 * e_2
  | e_1 / e_2
  | e_1 % e_2
  | e_1 ^ e_2
  | e_1 | e_2
  | e_g & e_2
  // operators over any ground type
  | e_1 == e_2
  | e_1 != e_2

Commands

// module operators are available only inside the module that declares n.
mop ∈ ModuleOp ::=
  | move_to_sender<n>(e) // type: 'Self.n -> unit'
                         // publishes resource struct 'n' under sender's address
                         // fails if there is already a resource present for 'Self.n'
  | move_from<n>(e)      // type: 'address -> Self.n'
                         // removes the resource struct 'n' at the specified address
                         // fails if there is no resource present for 'Self.n'
  | borrow_global<n>(e)  // type: 'address -> &mut Self.n'
                         // borrows a mutable reference to the resource struct 'n' at the specified address
                         // fails if there is no resource
                         // fails if it is already borrowed in this transaction's execution
  | exists<n>(e)         // type: 'address -> bool', s.t. 'n' is a resource struct
                         // returns 'true' if the resource struct 'n' at the specified address exists
                         // returns 'false' otherwise

builtin ∈ Builtin ::=
  | create_account(e)         // type: 'addr -> unit'
                              // creates new account at the specified address, failing if it already exists
  | release(e)                // type: '&t -> unit' or '&mut t -> unit'
                              // releases the reference given
  | freeze(x)                 // type: '&mut t -> &t'
                              // coerce a mutable reference to an immutable reference
  | get_txn_gas_unit_price()  // type: 'unit -> u64'
                              // gives the price specified per gas unit
  | get_txn_max_gas_units()   // type: 'unit -> u64'
                              // gives the tranaction's maximum amount of usable gas units
  | get_txn_public_key()      // type: 'unit -> bytearray'
                              // gives the transaction's public key
  | get_txn_sender()          // type: 'unit -> address'
                              // gives the transaction's sender's account address
  | get_txn_sequence_number() // type: 'unit -> u64'
                              // gives the sequence number for this transaction
  | get_gas_remaining()       // type: 'unit -> u64'
                              // gives the amount of gas gas units remaining before the transaction execution will be forced to halt execution

call ∈ Call ::=
  | mop
  | builtin
  | d.p(e_1, ..., e_j) // procedure 'p' defined in the module referenced by 'd'

c ∈ Cmd ::=
  | x = e                               // assign the result of evaluating 'e' to 'x'
  | x_1, ..., x_j = call                // Invokes 'call', assigns result to 'x_1' to 'x_j'
  | call                                // Invokes 'call' that has a return type of 'unit'
  | *x = e                              // mutation, s.t. 'x: &mut t' and 'e: t' and 't' is not of resource kind
  | assert(e_1, e_2)                    // type: 'bool * u64 -> unit'
                                        // halts execution with error code 'e_2' if 'e_1' evaluates to 'false'
  | break                               // exit a loop
  | continue                            // return to the top of a loop
  | return e_1, ..., e_n                // return values from procedure
  | n { f_1: x_1, ... , f_j: x_j } = e  // "de-constructor" for 'n'
                                        // "unpacks" a struct value 'e: _#Self.n'
                                        // value for 'f_i' is bound to local 'x_i'

Statements

s ∈ Stmt ::=
  | if (e) { s_1 } else { s_2 } // conditional
  | if (e) { s }                // conditional without else branch
  | while (e) { s }             // while loop
  | loop { s }                  // loops forever
  | c;                          // command
  | s_1 s_2                     // sequencing

Imports

 idecl ∈ Import ::=
   | import addr.m_1 as m_2; // imports 'addr.m_1' with the alias 'm_2'
   | import addr.m_1;        // imports 'addr.m_1' with the alias 'm_1'

Modules

sdecl ∈ StructDecl ::=
  | resource n { f_1: t_1, ..., f_j: t_j } // declaration of a resource struct
  | struct n { f_1: t_1, ..., f_j: t_j }   // declaration of a non-resource (value) struct
                                           // s.t. any 't_i' is not of resource kind

body ∈ ProcedureBody ::=
 | let x_1; ... let x_j; s // The locals declared in this procedure, and the code for that procedure

pdecl ∈ ProcedureDecl ::=
  | (public?) p(x_1: 𝛕_1, ..., x_j: 𝛕_j): 𝛕-list { body } // declaration of a defined procedure
                                                         // the procedure may be public, or internal to the module
  | native (public?) p(x_1: 𝛕_1, ..., x_j: 𝛕_j): 𝛕-list; // declaration of a native procedure
                                                        // the implementation is provided by the VM
                                                        // the procedure may be public, or internal to the module

mdecl ∈ ModuleDecl ::=
  | module m { idecl_1 ... idecl_i sdecl_1 ... sdecl_j pdecl_1 ... pdecl_k }

Transaction Scripts

TransactionScript ::=
  // declaration of the transaction scripts procedure
  // the 'main' procedure must be 'public' and any parameters must have a ground type
  | idecl_1 ... idecl_i public main(x_1: g_1, ..., x_j: g_j) { s }