Here we define the textual syntax of IELE assembly code. The syntax represented here has some syntactic sugar which is removed by the assembler. However, a fragment of this textual encoding is used by the semantics to express the rules of the language itself. The iele-examples directory contains various sample IELE contracts, such as:
The best way to understand the meaning of the IELE syntactic constructs is to read their actual formal semantics in iele.md.
IELE uses alphanumeric names for identifying registers, labels, functions, and contracts. IELE "keywords" are also valid identifiers.
module IELE-SYNTAX
imports IELE-COMMON
syntax IeleNameToken ::= r"(?<![A-Za-z0-9\\_\\.\\-\\$])[a-zA-Z\\.\\_\\$][0-9a-zA-Z\\.\\_\\-\\$]*" [token, notInRules, prec(3)]
syntax Keyword ::= "load" [token] | "store" [token] | "sload" [token] | "sstore" [token] | "iszero" [token] | "not" [token] | "add" [token] | "mul" [token] | "sub" [token] | "div" [token]
| "exp" [token] | "mod" [token] | "addmod" [token] | "mulmod" [token] | "expmod" [token] | "byte" [token] | "sext" [token] | "twos" [token] | "and" [token] | "or" [token]
| "xor" [token] | "shift" [token] | "lt" [token] | "le" [token] | "gt" [token] | "ge" [token] | "eq" [token] | "ne" [token] | "cmp" [token] | "sha3" [token]
syntax Keyword ::= "br" [token] | "call" [token] | "staticcall" [token] | "at" [token] | "send" [token] | "gaslimit" [token] | "ret" [token] | "void" [token] | "revert" [token]
| "log" [token] | "create" [token] | "copycreate" [token] | "selfdestruct" [token] | "contract" [token] | "external" [token] | "define" [token] | "public" [token]
| "log2" [token] | "bswap" [token] | "calladdress" [token]
syntax IeleNameToken ::= Keyword [token]
syntax NumericIeleName ::= r"[0-9]+" [token]
syntax StringIeleName ::= r"\\\"(([^\\\"\\\\])|(\\\\[0-9a-fA-F]{2}))*\\\"" [token]
endmodule
Local register names are desugared to integers when assembling an IELE program
module IELE-COMMON
imports DOMAINS-SYNTAX
imports INT-SYNTAX
syntax KResult
syntax NumericIeleName ::= Int
syntax StringIeleName [token]
syntax IeleName ::= NumericIeleName
syntax IeleNameToken [token]
syntax IeleName ::= IeleNameToken
syntax IeleName ::= StringIeleName [klabel(StringIeleName), avoid, symbol, function]
IELE has two categories of identifiers: local and global names.
- Local names have function-wide scope, are used for naming registers, and begin with
%. - Global names have contract-wide scope, are used for naming globals and functions, and begin with
@.
syntax GlobalName ::= "@" IeleName
syntax LocalName ::= "%" IeleName
syntax LocalNames ::= List{LocalName, ","} [klabel(localNameList)]
- IELE constants include unbounded signed integer literals and globals.
- IELE globals serve as names with contract-wide scope that hold a constant value (cannot be modified).
syntax Constant ::= IntConstant | GlobalName
syntax IntConstant ::= Int | Bool | HexConstant
syntax HexConstant ::= r"0x[0-9a-fA-F]+" [token]
IELE instruction operands are used at the left- and right-hand side of IELE instructions.
- One or more
LValuescan be used at the left-hand side of various IELE instructions - Zero or more
Operandscan be used at the right-hand side of various IELE instructions and as actual argument lists in function calls. - Constants can only be used as right-hand side operands, while registers can be used as both left- and right-hand side operands.
- Each right-hand side operand will be heated to an unbounded signed integer value during execution.
syntax LValue ::= LocalName
syntax LValues ::= NeList{LValue, ","} [klabel(lvalueList)]
syntax Operand ::= LValue | Constant
syntax Operands ::= List{Operand, ","} [klabel(operandList)]
syntax NonEmptyOperands ::= NeList{Operand, ","} [klabel(operandList)]
syntax Ints ::= List{Int, ","} [klabel(operandList)]
syntax Operands ::= Ints
syntax Operands ::= NonEmptyOperands
syntax Ints ::= NonEmptyInts
syntax NonEmptyOperands ::= NonEmptyInts
syntax NonEmptyInts ::= NeList{Int, ","} [klabel(operandList)]
Simple copy assignment that loads a value into a register.
syntax AssignInst ::= LValue "=" Operand
Instructions that provide access to the local execution memory. For more details see here.
syntax LoadInst ::= LValue "=" "load" /* cell */ Operand [hybrid, strict(2)]
syntax LoadInst ::= LValue "=" "load" /* cell */ Operand "," /* offset in bytes */ Operand "," /* width in bytes */ Operand [hybrid, seqstrict(2,3,4)]
syntax StoreInst ::= "store" /* value */ Operand "," /* cell */ Operand [hybrid, seqstrict(1,2)]
syntax StoreInst ::= "store" /* value */ Operand "," /* cell */ Operand "," /* offset in bytes */ Operand "," /* width in bytes */ Operand [hybrid, seqstrict(1,2,3,4)]
Instructions that provide access to the account storage. For more details see here.
syntax SLoadInst ::= LValue "=" "sload" /* index */ Operand [hybrid, strict(2)]
syntax SStoreInst ::= "sstore" /* value */ Operand "," /* index */ Operand [hybrid, seqstrict(1,2)]
Various expressions over unbounded signed integers. For more details see here.
syntax IsZeroInst ::= LValue "=" "iszero" Operand [hybrid, strict(2)]
syntax NotInst ::= LValue "=" "not" Operand [hybrid, strict(2)]
syntax AddInst ::= LValue "=" "add" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax MulInst ::= LValue "=" "mul" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax SubInst ::= LValue "=" "sub" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax DivInst ::= LValue "=" "div" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax ExpInst ::= LValue "=" "exp" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax ModInst ::= LValue "=" "mod" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax AddModInst ::= LValue "=" "addmod" Operand "," Operand "," Operand [hybrid, seqstrict(2,3,4)]
syntax MulModInst ::= LValue "=" "mulmod" Operand "," Operand "," Operand [hybrid, seqstrict(2,3,4)]
syntax ExpModInst ::= LValue "=" "expmod" Operand "," Operand "," Operand [hybrid, seqstrict(2,3,4)]
syntax LogInst ::= LValue "=" "log2" Operand [hybrid, strict(2)]
syntax ByteInst ::= LValue "=" "byte" /* byte index, 0 being the LSB */ Operand "," Operand [hybrid, seqstrict(2,3)]
syntax SExtInst ::= LValue "=" "sext" /* width in bytes */ Operand "," Operand [hybrid, seqstrict(2,3)]
syntax TwosInst ::= LValue "=" "twos" /* width in bytes */ Operand "," Operand [hybrid, seqstrict(2,3)]
syntax BswapInst ::= LValue "=" "bswap" /* width in bytes */ Operand "," Operand [hybrid, seqstrict(2,3)]
syntax AndInst ::= LValue "=" "and" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax OrInst ::= LValue "=" "or" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax XorInst ::= LValue "=" "xor" Operand "," Operand [hybrid, seqstrict(2,3)]
syntax ShiftInst ::= LValue "=" "shift" Operand "," /* shift amount */ Operand [hybrid, seqstrict(2,3)]
syntax Predicate ::= "lt" | "le" | "gt" | "ge" | "eq" | "ne"
syntax CmpInst ::= LValue "=" "cmp" Predicate Operand "," Operand [hybrid, seqstrict(3,4)]
syntax SHA3Inst ::= LValue "=" "sha3" Operand [hybrid, strict(2)]
Instructions for conditional and unconditional jumps within the function's body. For more details see here.
syntax JumpInst ::= "br" IeleName
syntax CondJumpInst ::= "br" Operand "," IeleName [hybrid, strict(1)]
Instructions for local functions calls to other functions of the same contract, as well as contract function calls to public functions of contracts deployed in other accounts. For more details see here.
syntax LocalCallInst ::= "call" Operand "(" Operands ")"
| LValues "=" "call" Operand "(" Operands ")" [hybrid, strict(2,3)]
syntax AccountCallInst ::= LValues "=" "call" Operand "at" Operand "(" Operands ")" "send" Operand "," "gaslimit" Operand [hybrid, seqstrict(2,3,4,5,6)]
syntax AccountCallInst ::= LValues "=" "staticcall" Operand "at" Operand "(" Operands ")" "gaslimit" Operand [hybrid, seqstrict(2,3,4,5)]
syntax CallAddressInst ::= LValue "=" "calladdress" GlobalName "at" Operand [hybrid, strict(3)]
syntax ReturnInst ::= "ret" NonEmptyOperands [hybrid, strict(1)]
| "ret" "void"
syntax RevertInst ::= "revert" Operand [hybrid, strict(1)]
Instructions to append information to the substate log. These variations append the entire content of a local execution memory cell to the log along with zero to four log topics.
syntax LogInst ::= "log" /* cell */ Operand [hybrid, strict(1)]
| "log" /* cell */ Operand "," NonEmptyOperands [hybrid, seqstrict(1,2)]
Instructions to create and/or delete a new account with a contract deployed with it. For more details see here.
syntax CreateInst ::= /* exit status */ LValue "," /* new account address */ LValue "=" "create" /* contract name */ IeleName "(" Operands ")" "send" Operand [hybrid, seqstrict(4,5)]
syntax CreateInst ::= /* exit status */ LValue "," /* new account address */ LValue "=" "copycreate" /* contract address */ Operand "(" Operands ")" "send" Operand [hybrid, seqstrict(3,4,5)]
syntax SelfdestructInst ::= "selfdestruct" /* account to send balance */ Operand [hybrid, strict(1)]
These accessors are implemented as builtins that can be called using the same syntax as in a local call, e.g. %pc = call @iele.pc() or %balance = call @iele.balance(%bank.account). The names of the builtins follow the IELE convention for intrinsics: Their name is a valid global name that starts with the prefix iele.. This means that no user-defined global name can start with the prefix iele..
syntax IeleNameToken ::= "iele.invalid" [token]
// local state queries
syntax IeleNameToken ::= "iele.gas" [token]
syntax IeleNameToken ::= "iele.gasprice" [token]
syntax IeleNameToken ::= "iele.gaslimit" [token]
syntax IeleNameToken ::= "iele.beneficiary" [token]
syntax IeleNameToken ::= "iele.timestamp" [token]
syntax IeleNameToken ::= "iele.number" [token]
syntax IeleNameToken ::= "iele.difficulty" [token]
syntax IeleNameToken ::= "iele.address" [token]
syntax IeleNameToken ::= "iele.origin" [token]
syntax IeleNameToken ::= "iele.caller" [token]
syntax IeleNameToken ::= "iele.callvalue" [token]
syntax IeleNameToken ::= "iele.msize" [token]
syntax IeleNameToken ::= "iele.codesize" [token]
syntax IeleNameToken ::= "iele.blockhash" [token]
// account queries
syntax IeleNameToken ::= "iele.balance" [token]
syntax IeleNameToken ::= "iele.extcodesize" [token]
Precompiled contracts are also available as IELE builtins but they should be called using the syntax for an account call targeting the account with address 1 (e.g. %res = call @iele.sha256 at 1 ( %len, %data ) send %val, gaslimit %gas).
syntax IeleNameToken ::= "iele.ecrec" [token]
syntax IeleNameToken ::= "iele.sha256" [token]
syntax IeleNameToken ::= "iele.rip160" [token]
syntax IeleNameToken ::= "iele.id" [token]
syntax IeleNameToken ::= "iele.ecadd" [token]
syntax IeleNameToken ::= "iele.ecmul" [token]
syntax IeleNameToken ::= "iele.ecpairing" [token]
syntax Instruction ::=
AssignInst
| LoadInst
| StoreInst
| SLoadInst
| SStoreInst
| IsZeroInst
| NotInst
| AddInst
| MulInst
| SubInst
| DivInst
| ExpInst
| ModInst
| AddModInst
| MulModInst
| ExpModInst
| ByteInst
| SExtInst
| TwosInst
| BswapInst
| AndInst
| OrInst
| XorInst
| ShiftInst
| CmpInst
| SHA3Inst
| JumpInst
| CondJumpInst
| LocalCallInst
| AccountCallInst
| CallAddressInst
| ReturnInst
| RevertInst
| LogInst
| CreateInst
| SelfdestructInst
syntax Instructions ::= List{Instruction, ""} [klabel(instructionList), format(%1%2%n%3)]
A contract is a compilation unit of code to be deployed with an account in the blockchain.
- A IELE program consists of a list of one or more contracts.
- The last contract in the list is the main contract.
- Each contract has a name and consists of a list of top-level definitions.
- Top-level definitions include external contract declarations, global definitions, and function definitions.
For more details see below and here.
syntax TopLevelDefinition ::=
FunctionDefinition
| GlobalDefinition
| ContractDeclaration
syntax TopLevelDefinitions ::= List{TopLevelDefinition, ""} [klabel(topLevelDefinitionList), format(%1%2%n%3)]
syntax ContractDefinition ::= "contract" IeleName "{" TopLevelDefinitions "}" [format(%1 %2 %3%n%i%4%d%n%5)]
syntax Contract ::= List{ContractDefinition, ""} [klabel(contractDefinitionList)]
A contract can only create accounts with deployed contracts that have been externaly declared within its top-level. A corresponding contract definition for each external contract declaration should precede this contract definition. This design decision ensures that a contract can only create new accounts with deployed contracts for which the code is available to it.
syntax ContractDeclaration ::= "external" "contract" IeleName
Definition of globals and their constant values. Globals are accessible from within any function of the contract and their value cannot be modified.
syntax GlobalDefinition ::= GlobalName "=" IntConstant [klabel(globalDefinition)]
Function definitions consist of a function signature (function name and names of formal arguments) and a function body (a list of blocks containing the code of the function). Functions can be defined as public meaning that they can be called from a contract deployed with another account. Non-public functions can only be called locally within the contract.
syntax FunctionSignature ::= GlobalName "(" FunctionParameters ")"
syntax FunctionParameters ::= LocalNames
syntax FunctionDefinition ::=
"define" FunctionSignature "{" Blocks "}" [format(%1 %2 %3%i%n%4%d%n%5%n)]
| "define" "public" FunctionSignature "{" Blocks "}" [format(%1 %2 %3 %4%i%n%5%d%n%6%n)]
The body of a function is a list of blocks, where each block is a list of IELE instructions. Each block except the first one has to be preceded by a label, making the first instruction of the block a valid target of a local jump. The first block can also be optionally labeled.
syntax LabeledBlock ::= IeleName ":" Instructions
syntax LabeledBlocks ::= List{LabeledBlock, ""} [klabel(labeledBlockList)]
syntax UnlabeledBlock ::= Instructions
syntax Blocks [flatPredicate]
syntax Blocks ::= UnlabeledBlock LabeledBlocks [avoid] | LabeledBlocks
- An account to which code has never been deployed contains an implicit contract with one public function named
@depositwhich takes no arguments, returns no values, and does nothing. This function exists to allow such accounts to receive payments. - A special private function named
@initshould be defined for every contract and will be called when an account is created with this contract.
syntax IeleNameToken ::= "deposit" [token]
syntax IeleNameToken ::= "init" [token]
Finally, following are macros for desugaring empty LValues and Operands lists in calls and returns.
rule call NAME ( ARGS ) => .LValues = call NAME ( ARGS ) [alias]
rule ret void => ret .NonEmptyOperands [alias]
endmodule