IELE Execution
IELE is a register-based abstract machine over some simple opcodes.
Most of the opcodes are "local" to the execution state of the machine, but some of them must interact with the world state.
This file only defines the local execution operations. A separate cardano.md will eventually be created to describe the remainder
of the transaction protocol.
requires "data.md"
requires "iele-syntax.md"
requires "iele-gas.md"
requires "well-formedness.md"
module IELE-CONFIGURATION
imports STRING
imports IELE-DATA
imports IELE-COMMON
imports IELE-WELL-FORMEDNESS
Configuration
We've broken up the configuration into two components; those parts of the state that mutate during execution of a single transaction and those that are static throughout. In the comments next to each cell, we explain the purpose of the cell.
rule initKCell(INIT) => <k> {INIT[#token("$PGM","KConfigVar")]}:>K </k> [priority(25)]
configuration
<kiele>
<well-formedness/>
<mode> $MODE:Mode </mode> // Execution mode: VMTESTS or NORMAL
<schedule> $SCHEDULE:Schedule </schedule> // Gas Schedule: DEFAULT or ALBE
<checkGas> true </checkGas> // Enables/disables gas check in test driver
// IELE Specific
// =============
<iele>
// Mutable during a single transaction
// -----------------------------------
<output> .Ints </output> // Return registers of current call frame
<callStack> .List </callStack> // Inter-contract call stack
<interimStates> .List </interimStates> // Checkpointed network state for rollback
<substateStack> .List </substateStack> // Checkpointed substate for rollback
// A single contract call frame
// ----------------------------
<callFrame>
// The loaded state of a IELE program
// ----------------------------------
<program>
<functions>
<function multiplicity="*" type="Map">
<funcId> deposit:IeleName </funcId> // The name of the function
<nparams> 0 </nparams> // The number of parameters of the function
<instructions> (.Instructions .LabeledBlocks):Blocks </instructions> // The blocks of the function
<jumpTable> .Map </jumpTable> // Map from jump label to blocks, for branch instruction
<nregs> 0 </nregs> // Number of registers used by this function
</function>
</functions>
<funcIds> .Set </funcIds> // Set of all names of functions in <functions> cell
<funcLabels> .Map </funcLabels> // Map of integer function IDS to all function names in the <functions> cell
<exported> .Set </exported> // Set of all names of functions defined with define public
<programSize> 0 </programSize> // Size in bytes of currently loaded contract
<contractCode> .Contract </contractCode> // Disassembled entire contract
</program>
<callDepth> 0 </callDepth> // Inter-contract call stack depth
<localCalls> .List </localCalls> // Intra-contract call stack
// I_*
<id> 0 </id> // Currently executing contract
<caller> 0 </caller> // Contract that called current contract
<callData> .Ints </callData> // Copy of register arguments
<callValue> 0 </callValue> // Value in funds passed to contract
// \mu_*
<regs> .Array </regs> // Current values of registers
<localMem> .Map </localMem> // Current values of local memory
<peakMemory> 0 </peakMemory> // Maximum memory used so far in call frame
<currentMemory> 0 </currentMemory> // Current memory used in call frame
<fid> deposit:IeleName </fid> // Name of currently executing function
<gas> 0 </gas> // Current gas remaining
<previousGas> 0 </previousGas> // Gas remaining prior to last decrease
<static> false </static> // Whether the call frame came from a staticcall
</callFrame>
// A_* (execution substate)
<substate>
<selfDestruct> .Set </selfDestruct> // Set of contract ids that were destroyed by this transaction
<logData> .List </logData> // Log entries for this transaction
<refund> 0 </refund> // Refund for this transaction
</substate>
// Immutable during a single transaction
// -------------------------------------
<gasPrice> 0 </gasPrice> // Price of gas for this transaction
<origin> 0 </origin> // Sender of current transaction
// I_H* (block information)
<beneficiary> 0 </beneficiary> // Miner of current block
<difficulty> 0 </difficulty> // Difficulty of current block
<number> 0 </number> // Number of current block
<gasLimit> 0 </gasLimit> // Gas limit of current block
<gasUsed> 0 </gasUsed> // Gas used by current block
<timestamp> 0 </timestamp> // Timestamp of current block
<blockhash> .List </blockhash> // List of previous block's hashes
</iele>
// IELE Network Layer
// ==================
<network>
// Accounts Record
// ---------------
<activeAccounts> .Set </activeAccounts> // Set of keys in the accounts cell.
<accounts>
<account multiplicity="*" type="Map">
<acctID> 0 </acctID> // ID of account
<balance> 0 </balance> // Balance of funds in account
<code> #emptyCode </code> // Disassembled contract of account
<storage> .Map </storage> // Permanent storage of account (for sload/sstore)
<nonce> 0 </nonce> // Nonce of account
</account>
</accounts>
// Transactions Record
// -------------------
<txOrder> .List </txOrder> // Order of transactions in block
<txPending> .List </txPending> // Remaining transactions in block
<messages>
<message multiplicity="*" type="Map">
<msgID> 0 </msgID> // Unique ID of transaction
<txNonce> 0 </txNonce> // Nonce of transaction (not checked)
<txGasPrice> 0 </txGasPrice> // Gas price of transaction
<txGasLimit> 0 </txGasLimit> // Gas limit of transaction
<sendto> .Account </sendto> // Destination of transaction (.Account for account creation)
<func> deposit:IeleName </func> // Function to call by transaction
<value> 0 </value> // Value in funds to transfer by transaction
<from> 0 </from> // Sender of transaction
<data> .Bytes </data> // Arguments to function called by transaction
<args> .Ints </args>
</message>
</messages>
</network>
</kiele>
syntax IELESimulation
syntax Mode
syntax Schedule
syntax Contract ::= "#emptyCode"
// --------------------------------
Uninitialized Accounts
An account to which code has never been deployed has a size in bytes of zero, but contains an implicit public function @deposit which takes
no arguments, returns no values, and does nothing. This function exists to allow accounts to receive payment even if they do not have a contract
deployed to them. Note that a contract can forbid payments by refusing to declare the @deposit function, and explicitly raising an exception
if any of its entry points are invoked with a balance transfer.
Note that the syntax used in the following #emptyCode macro is desugared IELE syntax, where contracts have a size in bytes metadata attachment (!0 here) and argument lists are replaced with an integer value representing arity (0 here).
syntax IeleNameToken ::= "Main" [token]
| "iele.Wallet" [token]
syntax ContractDefinition ::= "contract" IeleName "!" /* size in bytes */ Int /* byte string */ String "{" TopLevelDefinitions "}" /* when desugared to include the code size */
// --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
rule #emptyCode => contract iele.Wallet !0 "" { define public @deposit ( 0 ) { ret .NonEmptyOperands .Instructions .LabeledBlocks } } .Contract [macro]
endmodule
The network state is closely based on the EVM blockchain, with the state mainly consisting of information on a set of accounts, and funds being held by accounts rather than following the Bitcoin "UTXO" model.
Accounts are divided into smart contracts, which accept calls and disburse funds according only to their code, and simple wallets which can receive deposits but contain no smart contract code, and are operated by a person off-chain system holding a corresponding private key.
There is no clear division in the address space between smart contracts and wallets, but it is intended to be impossible for a smart contract to exist at an address for which anybody knows a corresponding private key, so that clients of that contract can be sure that its funds will only be used according to the contract code.
When calling a function on an account, the caller may
include funds to be given to the receiver. In the syntax
of the call instruction this quantity comes after the
send keyword.
This is also the only way to transfer funds between accounts.
To allow sending funds to simple wallets, those accounts
act as if they have a single public function named deposit
which takes no arguments and immediately returns successfully
when called (thus keeping any funds which were sent).
To allow people to set up a simple wallet without needing
to send any blockchain transactions, we need to allow deposit
to be called on accounts that have never previously been
mentioned on the blockchain.
In this case the account is initialized as an "empty" account,
which has a balance but no contract code.
A complication is that a call to deposit can create such
an "empty account" at the address where a new smart contract
will later be created, because it is sometimes feasible
to predict the addresses of new contracts.
The prevent this from being a possible denial of service attack,
we allow the new smart contract to be created anyway in this case,
setting up its code an persistent storage and inheriting any
funds which were already held at that address.
This is a bit unfortunate but it doesn't compromise the
security guarantee that a smart contract account never exists at
an address for which anybody knows a private key.
module IELE-INFRASTRUCTURE
imports IELE-CONFIGURATION
imports IELE-CONSTANTS
Hardware
The callStack cell stores a list of previous VM execution states.
#pushCallStacksaves a copy of VM execution state on thecallStack.#popCallStackrestores the top element of thecallStack.
syntax InternalOp ::= "#pushCallStack"
// --------------------------------------
rule <k> #pushCallStack => . ... </k>
<callFrame> FRAME </callFrame>
<callStack> (.List => ListItem(<callFrame> FRAME </callFrame>)) ... </callStack>
syntax InternalOp ::= "#popCallStack"
// -------------------------------------
rule <k> #popCallStack => . ... </k>
<callFrame> _ => FRAME </callFrame>
<callStack> (ListItem(<callFrame> FRAME </callFrame>) => .List) ... </callStack>
The interimStates cell stores a list of previous world states.
#pushWorldStatestores a copy of the current accounts at the top of theinterimStatescell.#popWorldStaterestores the top element of theinterimStates.#dropWorldStateremoves the top element of theinterimStates.
syntax Accounts ::= "{" AccountsCell "|" Set "}"
// ------------------------------------------------
syntax InternalOp ::= "#pushWorldState"
// ---------------------------------------
rule <k> #pushWorldState => .K ... </k>
<activeAccounts> ACCTS </activeAccounts>
<accounts> ACCTDATA </accounts>
<interimStates> (.List => ListItem({ <accounts> ACCTDATA </accounts> | ACCTS })) ... </interimStates>
syntax InternalOp ::= "#popWorldState"
// --------------------------------------
rule <k> #popWorldState => .K ... </k>
<interimStates> (ListItem({ <accounts> ACCTDATA </accounts> | ACCTS }) => .List) ... </interimStates>
<activeAccounts> _ => ACCTS </activeAccounts>
<accounts> _ => ACCTDATA </accounts>
syntax InternalOp ::= "#dropWorldState"
// ---------------------------------------
rule <k> #dropWorldState => . ... </k> <interimStates> (ListItem(_) => .List) ... </interimStates>
The substateStack cell stores a list of previous substate logs.
#pushSubstatestores a copy of the current substate at the top of thesubstateStackcell.#popSubstaterestores the top element of thesubstateStack.#dropSubstateremoves the top element of thesubstateStack.
syntax InternalOp ::= "#pushSubstate"
// -------------------------------------
rule <k> #pushSubstate => .K ... </k>
<substate> SUBSTATE </substate>
<substateStack> (.List => ListItem(<substate> SUBSTATE </substate>)) ... </substateStack>
syntax InternalOp ::= "#popSubstate"
// ------------------------------------
rule <k> #popSubstate => .K ... </k>
<substate> _ => SUBSTATE </substate>
<substateStack> (ListItem(<substate> SUBSTATE </substate>) => .List) ... </substateStack>
syntax InternalOp ::= "#dropSubstate"
// -------------------------------------
rule <k> #dropSubstate => .K ... </k> <substateStack> (ListItem(_) => .List) ... </substateStack>
Simple commands controlling exceptions provide control-flow.
#endis used to indicate the (non-exceptional) end of execution.#exceptionis used to indicate exceptional states (it consumes any operations to be performed after it).#revertis used to indicate the contract terminated with the revert instruction (exceptional return with error message, refunding gas).
syntax KItem ::= Exception
syntax Exception ::= "#exception" Int | "#end" | "#revert" Int
// --------------------------------------------------------------
rule <k> _:Exception ~> (_:Int => .) ... </k>
rule <k> _:Exception ~> (_:Instruction => .) ... </k>
rule <k> _:Exception ~> (_:Blocks => .) ... </k>
rule <k> _:Exception ~> (_:InternalOp => .) ... </k>
syntax Int ::= "FUNC_NOT_FOUND"
| "FUNC_WRONG_SIG"
| "CONTRACT_NOT_FOUND"
| "USER_ERROR"
| "OUT_OF_GAS"
| "ACCT_COLLISION"
| "OUT_OF_FUNDS"
| "CALL_STACK_OVERFLOW"
| "CONTRACT_INVALID"
// ------------------------------------
rule FUNC_NOT_FOUND => 1 [macro]
rule FUNC_WRONG_SIG => 2 [macro]
rule CONTRACT_NOT_FOUND => 3 [macro]
rule USER_ERROR => 4 [macro]
rule OUT_OF_GAS => 5 [macro]
rule ACCT_COLLISION => 6 [macro]
rule OUT_OF_FUNDS => 7 [macro]
rule CALL_STACK_OVERFLOW => 8 [macro]
rule CONTRACT_INVALID => 9 [macro]
Description of registers.
- Registers begin with
% - Registers are evaluated using heating to the values they contain.
#regRange(N)generates the registers 0 to N-1.
syntax KResult ::= Constant
// ---------------------------
rule <k> % REG:Int => REGS [ REG ] ... </k> <regs> REGS </regs> <typeChecking> false </typeChecking>
syntax KResult ::= Ints
// -----------------------
rule isKResult(.Operands) => true
syntax NonEmptyInts ::= lookupRegisters(Operands, Array) [function]
// -----------------------------------------------------------
rule <k> % REG:Int , OPS => lookupRegisters(% REG, OPS, REGS) ... </k> <regs> REGS </regs> <typeChecking> false </typeChecking>
rule lookupRegisters(% REG:Int, OPS, REGS) => getInt(REGS [ REG ]) , lookupRegisters(OPS, REGS)
rule lookupRegisters(.Operands, _) => .NonEmptyInts
syntax LValues ::= #regRange ( Int ) [function]
| #regRange ( Int , Int ) [function, klabel(#regRangeAux)]
// ---------------------------------------------------------------------------
rule #regRange(N) => #regRange(0, N)
rule #regRange(_, 0) => .LValues
rule #regRange(N, 1) => % N , .LValues
rule #regRange(N, M) => % N , #regRange(N +Int 1, M -Int 1) [owise]
Execution Step
When an instruction reaches the top of the K cell, we first heat its registers, then compute gas cost, then execute the instruction itself.
syntax InternalOp ::= "#exec" Instruction
| "#gas" "[" Instruction "]"
// ------------------------------------------------
rule <k> OP:Instruction => #gas [ #addr?(OP) ] ~> #exec #addr?(OP) ... </k> requires isKResult(OP)
The following types of instructions do not require any register heating.
syntax KResult ::= AssignInst
syntax KResult ::= JumpInst
Some instructions require an argument to be interpreted as an address (modulo 160 bits) or a memory cell (modulo 256 bits), so the #addr? function performs that check.
syntax Instruction ::= "#addr?" "(" Instruction ")" [function]
// --------------------------------------------------------------
rule #addr?(REG = call @iele.balance(W)) => REG = call @iele.balance(#addr(W))
rule #addr?(REG = call @iele.extcodesize(W)) => REG = call @iele.extcodesize(#addr(W))
rule #addr?(REG1 , REG2 = copycreate W0 (REGS1) send W1) => REG1 , REG2 = copycreate #addr(W0) (REGS1) send W1
rule #addr?(selfdestruct W) => selfdestruct #addr(W)
rule #addr?(REGS1 = call LABEL at W0 (REGS2) send W1 , gaslimit W2) => REGS1 = call LABEL at #addr(W0) (REGS2) send W1 , gaslimit W2
rule #addr?(REGS1 = staticcall LABEL at W0 (REGS2) gaslimit W1) => REGS1 = staticcall LABEL at #addr(W0) (REGS2) gaslimit W1
rule #addr?(REG = calladdress LABEL at W0) => REG = calladdress LABEL at #addr(W0)
rule #addr?(REG = load CELL, OFFSET, WIDTH) => REG = load chop(CELL), OFFSET, WIDTH
rule #addr?(REG = load CELL) => REG = load chop(CELL)
rule #addr?(store VALUE, CELL, OFFSET, WIDTH) => store VALUE, chop(CELL), OFFSET, WIDTH
rule #addr?(store VALUE, CELL) => store VALUE, chop(CELL)
rule #addr?(REG = sha3 CELL) => REG = sha3 chop(CELL)
rule #addr?(log CELL) => log chop(CELL)
rule #addr?(log CELL, ARGS) => log chop(CELL), ARGS
rule #addr?(OP) => OP [owise]
Internal Operations
#loadAccount_allows declaring a new empty account with the given address (and assumes the rounding to 160 bits has already occured). If the account already exists with non-zero nonce or non-empty code, an exception is thrown. Otherwise, if the account already exists, the storage is cleared.
syntax InternalOp ::= "#loadAccount" Int
| "#initAccount" Int
// ----------------------------------------
rule <k> #initAccount ACCT => #exception ACCT_COLLISION ... </k>
<account>
<acctID> ACCT </acctID>
<code> CODE </code>
<nonce> NONCE </nonce>
...
</account>
requires CODE =/=K #emptyCode orBool NONCE =/=K 0
rule <k> #initAccount ACCT => . ... </k>
<account>
<acctID> ACCT </acctID>
<code> #emptyCode </code>
<nonce> 0 </nonce>
<storage> _ => .Map </storage>
...
</account>
rule <k> (.K => #loadAccount ACCT) ~> #initAccount ACCT ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in ACCTS
rule <k> #loadAccount ACCT => . ... </k>
<activeAccounts> ACCTS (.Set => SetItem(ACCT)) </activeAccounts>
<accounts>
( .Bag
=> <account>
<acctID> ACCT </acctID>
...
</account>
)
...
</accounts>
requires notBool ACCT in ACCTS
#lookupStorageloads the<storage>cell with the storage value for a particular key in the account.
syntax InternalOp ::= #lookupStorage ( Int , Int )
// --------------------------------------------------
rule <k> #lookupStorage(ACCT, INDEX) => . ... </k>
<account>
<acctID> ACCT </acctID>
<storage> STORAGE </storage>
...
</account>
requires INDEX in_keys(STORAGE)
rule <k> #lookupStorage(ACCT, INDEX) => . ... </k>
<account>
<acctID> ACCT </acctID>
<storage> STORAGE => STORAGE [ INDEX <- 0 ] </storage>
...
</account>
requires notBool INDEX in_keys(STORAGE)
#lookupCodeloads the<code>cell with the code for a particular account.
syntax InternalOp ::= #lookupCode ( Int )
// -----------------------------------------
#transferFundsmoves money from one account into another, creating the destination account if it doesn't exist.
syntax InternalOp ::= "#transferFunds" Int Int Int
// --------------------------------------------------
rule <k> #transferFunds ACCTFROM ACCTTO VALUE => . ... </k>
<account>
<acctID> ACCTFROM </acctID>
<balance> ORIGFROM => ORIGFROM -Int VALUE </balance>
...
</account>
<account>
<acctID> ACCTTO </acctID>
<balance> ORIGTO => ORIGTO +Int VALUE </balance>
...
</account>
requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => #exception OUT_OF_FUNDS ... </k>
<account>
<acctID> ACCTFROM </acctID>
<balance> ORIGFROM </balance>
...
</account>
requires VALUE >Int ORIGFROM
rule <k> (. => #loadAccount ACCTTO) ~> #transferFunds ACCTFROM ACCTTO VALUE ... </k>
<activeAccounts> ACCTS </activeAccounts>
<account>
<acctID> ACCTFROM </acctID>
<balance> ORIGFROM </balance>
...
</account>
requires ACCTFROM =/=K ACCTTO andBool notBool ACCTTO in ACCTS andBool VALUE <=Int ORIGFROM
rule <k> #transferFunds ACCT ACCT VALUE => . ... </k>
<account>
<acctID> ACCT </acctID>
<balance> ORIGFROM </balance>
...
</account>
requires VALUE <=Int ORIGFROM
endmodule
Instruction Execution Cycle
#executeloads the code of the currently-executing function into thekcell, where it executes until the function returns. It is an exception if we try to execute a function that does not exist.
module IELE
imports IELE-GAS
imports IELE-PRECOMPILED
imports IELE-PROGRAM-LOADING
imports IELE-INFRASTRUCTURE
syntax KItem ::= "#execute"
// ---------------------------
rule <k> #execute => CODE ... </k> <fid> FUNC </fid> <funcId> FUNC </funcId> <instructions> CODE </instructions>
Execution follows a simple cycle where first the state is checked for exceptions, then if no exceptions will be thrown the opcode is run.
- If we reach the end of the function, we execute an implicit
ret voidinstruction.
rule <k> .LabeledBlocks => ret .NonEmptyOperands .Instructions .LabeledBlocks ... </k>
<typeChecking> false </typeChecking>
- The rule for sequential composition checks if the instruction is exceptional, runs it if not, then executes the next instruction (assuming the instruction doesn't execute a transfer of control flow).
rule <k> OP::Instruction OPS::Instructions BLOCKS::LabeledBlocks
=> #exceptional? [ OP ] ~> OP
~> OPS BLOCKS
...
</k>
<typeChecking> false </typeChecking>
When execution reaches the end of a block, we fall through to the immediately next block.
rule <k> .Instructions BLOCKS::LabeledBlocks => BLOCKS ... </k>
<typeChecking> false </typeChecking>
Exceptional Ops
Some checks if an opcode will throw an exception are relatively quick and done up front.
#exceptional?checks if the operator is invalid.
syntax InternalOp ::= "#exceptional?" "[" Instruction "]"
// ---------------------------------------------------------
rule <k> #exceptional? [ OP ] => #invalid? [ OP ] ~> #static? [ OP ] ~> #negativeCall? [ OP ] ... </k>
#invalid?checks if it's the designated invalid opcode.
syntax K ::= "#invalid?" "[" Instruction "]" [function]
// -------------------------------------------------------
rule #invalid? [ _ = call @iele.invalid(.Operands) ] => #exception USER_ERROR
rule #invalid? [ _OP ] => . [owise]
#static?determines if the opcode should throw an exception due to the static flag (i.e., an attempt to change state inside a contract called withstaticcall)
syntax InternalOp ::= "#static?" "[" Instruction "]"
// ----------------------------------------------------
rule <k> #static? [ _OP ] => . ... </k> <static> false </static>
rule <k> #static? [ OP ] => . ... </k> <regs> REGS </regs> <static> true </static> requires notBool #changesState(OP, REGS)
rule <k> #static? [ OP ] => #exception USER_ERROR ... </k> <regs> REGS </regs> <static> true </static> requires #changesState(OP, REGS)
syntax Bool ::= #changesState ( Instruction , Array ) [function]
// ----------------------------------------------------------------
rule #changesState(log _, _) => true
rule #changesState(log _ , _, _) => true
rule #changesState(sstore _ , _, _) => true
rule #changesState(_ = call _ at _ (_) send % VALUE , gaslimit _, REGS) => true requires REGS [ VALUE ] =/=K 0
rule #changesState(_ , _ = create _ (_) send _, _) => true
rule #changesState(_ , _ = copycreate _ (_) send _, _) => true
rule #changesState(selfdestruct _, _) => true
rule #changesState(...) => false [owise]
#negativeCall?throws an exception if we are making a contract call with negative value or gas limit.
syntax InternalOp ::= "#negativeCall?" "[" Instruction "]"
// ----------------------------------------------------------
rule <k> #negativeCall? [ OP ] => . ... </k> requires notBool isAccountCallInst(OP) andBool notBool isCreateInst(OP)
rule <k> #negativeCall? [ _ = call _ at _ ( _ ) send % REG1 , gaslimit % REG2 ] => #if getInt(REGS [ REG1 ]) <Int 0 orBool getInt(REGS [ REG2 ]) <Int 0 #then #exception USER_ERROR #else . #fi ... </k> <regs> REGS </regs>
rule <k> #negativeCall? [ _ = staticcall _ at _ ( _ ) gaslimit % REG ] => #if getInt(REGS [ REG ]) <Int 0 #then #exception USER_ERROR #else . #fi ... </k> <regs> REGS </regs>
rule <k> #negativeCall? [ _ , _ = create _ ( _ ) send % REG ] => #if getInt(REGS [ REG ]) <Int 0 #then #exception USER_ERROR #else . #fi ... </k> <regs> REGS </regs>
rule <k> #negativeCall? [ _ , _ = copycreate _ ( _ ) send % REG ] => #if getInt(REGS [ REG ]) <Int 0 #then #exception USER_ERROR #else . #fi ... </k> <regs> REGS </regs>
Substate Log
After executing a transaction, it's necessary to have the effect of the substate log recorded.
#finalizeTxmakes the substate log actually have an effect on the state.
syntax InternalOp ::= #finalizeTx ( Bool )
| #deleteAccounts ( List )
// ----------------------------------------------
rule <k> #finalizeTx(true) => . ... </k>
<selfDestruct> .Set </selfDestruct>
rule <k> #finalizeTx(false => true) ... </k>
<mode> VMTESTS </mode>
<id> ACCT </id>
<refund> BAL => 0 </refund>
<account>
<acctID> ACCT </acctID>
<balance> CURRBAL => CURRBAL +Int BAL </balance>
...
</account>
rule <k> (.K => #loadAccount MINER) ~> #finalizeTx(_)... </k>
<mode> NORMAL </mode>
<beneficiary> MINER </beneficiary>
<activeAccounts> ACCTS </activeAccounts>
requires notBool MINER in ACCTS
rule <k> #finalizeTx(false => true) ... </k>
<mode> NORMAL </mode>
<txPending> ListItem(_) => .List ... </txPending>
rule <k> (. => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ... </k>
<selfDestruct> ACCTS => .Set </selfDestruct>
requires size(ACCTS) >Int 0
rule <k> #deleteAccounts(ListItem(ACCT) ACCTS) => #deleteAccounts(ACCTS) ... </k>
<activeAccounts> ... (SetItem(ACCT) => .Set) </activeAccounts>
<accounts>
( <account>
<acctID> ACCT </acctID>
...
</account>
=> .Bag
)
...
</accounts>
rule #deleteAccounts(.List) => .
IELE Programs
Lists of instructions form functions in a contract.
IELE Instructions
Each subsection has a different class of instructions. Organization is based roughly on what parts of the execution state are needed to compute the result of each operator.
Invalid Operator
We use an explicit call to @iele.invalid both for marking the designated invalid operator and for garbage bytes in the input program.
Executing the INVALID instruction results in an exception.
Register Manipulations
Some operators don't calculate anything, they just manipulate the state of registers.
-
Assigning an integer to a register is used to load immediate values into registers.
-
Assigning one register to another copies the value of the source register into the destination.
-
#loadsloads a list of integers into a list of registers. It is an exception if the number of values do not match.
rule <k> #exec REG = W:Int => #load REG W ... </k>
rule <k> #exec REG1 = % REG2 => #load REG1 getInt( REGS [ REG2 ] ) ... </k> <regs> REGS </regs>
syntax InternalOp ::= "#load" LValue Int
| "#load" Int Int Int [klabel(#loadAux)]
// ------------------------------------------------------------
rule <k> #load % REG VALUE => #load REG VALUE getInt(REGS [ REG ]) ... </k> <regs> REGS </regs>
rule <k> #load REG VALUE OLD => . ... </k> <regs> REGS => REGS [ REG <- VALUE ] </regs> <currentMemory> CURR => CURR -Int intSize(OLD) +Int intSize(VALUE) </currentMemory>
syntax InternalOp ::= "#loads" LValues Ints
// -------------------------------------------
rule <k> #loads (REG , REGS) (VALUE , VALUES) => #load REG VALUE ~> #loads REGS VALUES ... </k>
rule <k> #loads .LValues .Ints => .K ... </k>
rule <k> #loads (_REG , _REGS) .Ints => #exception FUNC_WRONG_SIG ... </k>
rule <k> #loads .LValues (_VALUE , _VALUES) => #exception FUNC_WRONG_SIG ... </k>
Local Memory
These operations are getters/setters of the local execution memory.
REG = load CELL, OFFSET, WIDTHloads WIDTH bytes starting at OFFSET in the specified memory CELL into REG, interpreted as a signed integer.REG = load CELLloads the entire value in CELL into REG, interpreted as a signed integer.REG = store VALUE, CELL, OFFSET, WIDTHstores VALUE into the specified memory CELL at OFFSET, interpreting it modulo 256^WIDTH.REG = store VALUE, CELLstores VALUE into the specified memory CELL, overwriting the previous value of the entire cell.
rule <k> #exec REG = load CELL , OFFSET , WIDTH => #load REG Bytes2Int(LM [ OFFSET .. WIDTH ], LE, Unsigned) ... </k>
<localMem>... CELL |-> LM ...</localMem>
rule <k> #exec REG = load CELL , _OFFSET , _WIDTH => #load REG 0 ... </k>
<localMem> LM </localMem>
requires notBool CELL in_keys(LM)
rule <k> #exec REG = load CELL => #load REG Bytes2Int(LM, LE, Signed) ... </k>
<localMem>... CELL |-> LM ...</localMem>
rule <k> #exec REG = load CELL => #load REG 0 ... </k>
<localMem> LM </localMem>
requires notBool CELL in_keys(LM)
rule <k> #exec store VALUE , CELL , OFFSET , WIDTH => . ... </k>
<localMem>... CELL |-> (LM => LM [ OFFSET := Int2Bytes(chop(WIDTH), twos(chop(WIDTH), VALUE), LE) ]) </localMem>
rule <k> #exec store _ , CELL , _ , WIDTH ... </k>
<localMem> LM (.Map => CELL |-> .Bytes) </localMem>
requires notBool CELL in_keys(LM) andBool WIDTH =/=Int 0
rule <k> #exec store _ , CELL , _ , 0 => . ... </k>
<localMem> LM </localMem>
requires notBool CELL in_keys(LM)
rule <k> #exec store VALUE , CELL => . ... </k>
<localMem> LM => #if VALUE ==Int 0 andBool notBool CELL in_keys(LM) #then LM #else LM [ CELL <- Int2Bytes(VALUE, LE, Signed) ] #fi </localMem>
Expressions
Expression calculations are simple and don't require anything but the arguments from the regs to operate.
-
REG = iszero Wperforms boolean negation on W. -
REG = not Wperforms bitwise negation on W. -
REG = add W0, W1performs arbitrary-precision addition on W0 and W1. -
REG = sub W0, W1performs arbitrary-precision subtraction on W0 and W1. -
REG = mul W0, W1performs arbitrary-precision multiplication on W0 and W1. -
REG = div W0, W1performs arbitrary-precision t-division on W0 and W1. It is an exception to divide by zero. -
REG = mod W0, W1performs arbitrary-precision t-modulus on W0 and W1. It is an exception to modulus by zero. -
REG = exp W0, W1performs arbitrary-precision exponentiation on W0 and W1. It is an exception to exponentiate by a negative number. -
REG = addmod W0, W1, W2performs addition of W0 and W1 modulo W2. It is an exception to modulus by zero. -
REG = mulmod W0, W1, W2performs multiplication of W0 and W1 modulo W2. It is an exception to modulus by zero. -
REG = expmod W0, W1, W2performs exponentiation of W0 and W1 modulo W2. It is an exception to exponentiate by a negative number or modulus by zero. -
REG = log2 Wperforms the floored logarithm base 2 of W. It is an exception to compute the logarithm of 0 or of a negative number. -
REG = and W0, W1performs bitwise AND on W0 and W1. -
REG = or W0, W1performs bitwise inclusive OR on W0 and W1. -
REG = xor W0, W1performs bitwise exclusive OR on W0 and W1. -
REG = shift W0, W1performs bitwise shifting of W0 by W1 bits. If W1 is positive, a left shift occurs; if W1 is negative, a right shift occurs. -
REG = cmp lt W0, W1computes if W0 is less than W1. -
REG = cmp le W0, W1computes if W0 is less than or equal to W1. -
REG = cmp gt W0, W1computes if W0 is greater than W1. -
REG = cmp ge W0, W1computes if W0 is greater than or equal to W1. -
REG = cmp eq W0, W1computes if W0 is equal to W1. -
REG = cmp ne W0, W1computes if W0 is not equal to W1.
rule <k> #exec REG = iszero 0 => #load REG 1 ... </k>
rule <k> #exec REG = iszero W => #load REG 0 ... </k> requires W =/=K 0
rule <k> #exec REG = not W => #load REG ~Int W ... </k>
rule <k> #exec REG = add W0 , W1 => #load REG W0 +Int W1 ... </k>
rule <k> #exec REG = mul W0 , W1 => #load REG W0 *Int W1 ... </k>
rule <k> #exec REG = sub W0 , W1 => #load REG W0 -Int W1 ... </k>
rule <k> #exec REG = div W0 , W1 => #load REG W0 /Int W1 ... </k> requires W1 =/=Int 0
rule <k> #exec _REG = div _ , 0 => #exception USER_ERROR ... </k>
rule <k> #exec REG = exp W0 , W1 => #load REG W0 ^Int W1 ... </k> requires W1 >=Int 0
rule <k> #exec _REG = exp _ , W1 => #exception USER_ERROR ... </k> requires W1 <Int 0
rule <k> #exec REG = mod W0 , W1 => #load REG W0 %Int W1 ... </k> requires W1 =/=Int 0
rule <k> #exec _REG = mod _ , 0 => #exception USER_ERROR ... </k>
rule <k> #exec REG = addmod W0 , W1 , W2 => #load REG (W0 +Int W1) %Int W2 ... </k> requires W2 =/=Int 0
rule <k> #exec _REG = addmod _ , _ , 0 => #exception USER_ERROR ... </k>
rule <k> #exec REG = mulmod W0 , W1 , W2 => #load REG (W0 *Int W1) %Int W2 ... </k> requires W2 =/=Int 0
rule <k> #exec _REG = mulmod _ , _ , 0 => #exception USER_ERROR ... </k>
rule <k> #exec REG = expmod W0 , W1 , W2 => #load REG powmod(W0,W1,W2) ... </k> requires W2 =/=Int 0 andBool (W1 >=Int 0 orBool gcdInt(W0, W2) ==Int 1)
rule <k> #exec _REG = expmod _ , _ , 0 => #exception USER_ERROR ... </k>
rule <k> #exec _REG = expmod W0 , W1 , W2 => #exception USER_ERROR ... </k> requires W1 <Int 0 andBool gcdInt(W0, W2) =/=Int 1
rule <k> #exec REG = byte INDEX , W => #load REG byte(chop(INDEX), W) ... </k>
rule <k> #exec REG = sext WIDTH , W => #load REG signextend(chop(WIDTH), W) ... </k> requires W >=Int 0
rule <k> #exec _REG = sext _ , W => #exception USER_ERROR ... </k> requires W <Int 0
rule <k> #exec REG = twos WIDTH , W => #load REG twos(chop(WIDTH), W) ... </k>
rule <k> #exec REG = bswap WIDTH , W => #load REG bswap(chop(WIDTH), W) ... </k> requires WIDTH >=Int 0
rule <k> #exec _REG = bswap WIDTH , _ => #exception USER_ERROR ... </k> requires WIDTH <Int 0
rule <k> #exec REG = log2 W => #load REG log2Int(W) ... </k> requires W >Int 0
rule <k> #exec _REG = log2 W => #exception USER_ERROR ... </k> requires W <=Int 0
rule <k> #exec REG = and W0 , W1 => #load REG W0 &Int W1 ... </k>
rule <k> #exec REG = or W0 , W1 => #load REG W0 |Int W1 ... </k>
rule <k> #exec REG = xor W0 , W1 => #load REG W0 xorInt W1 ... </k>
rule <k> #exec REG = shift W0 , W1 => #load REG W0 <<Int W1 ... </k> requires W1 >=Int 0
rule <k> #exec REG = shift W0 , W1 => #load REG W0 >>Int (0 -Int W1) ... </k> requires W1 <Int 0
rule <k> #exec REG = cmp lt W0 , W1 => #load REG 1 ... </k> requires W0 <Int W1
rule <k> #exec REG = cmp lt W0 , W1 => #load REG 0 ... </k> requires W0 >=Int W1
rule <k> #exec REG = cmp le W0 , W1 => #load REG 1 ... </k> requires W0 <=Int W1
rule <k> #exec REG = cmp le W0 , W1 => #load REG 0 ... </k> requires W0 >Int W1
rule <k> #exec REG = cmp gt W0 , W1 => #load REG 1 ... </k> requires W0 >Int W1
rule <k> #exec REG = cmp gt W0 , W1 => #load REG 0 ... </k> requires W0 <=Int W1
rule <k> #exec REG = cmp ge W0 , W1 => #load REG 1 ... </k> requires W0 >=Int W1
rule <k> #exec REG = cmp ge W0 , W1 => #load REG 0 ... </k> requires W0 <Int W1
rule <k> #exec REG = cmp eq W0 , W1 => #load REG 1 ... </k> requires W0 ==Int W1
rule <k> #exec REG = cmp eq W0 , W1 => #load REG 0 ... </k> requires W0 =/=Int W1
rule <k> #exec REG = cmp ne W0 , W1 => #load REG 1 ... </k> requires W0 =/=Int W1
rule <k> #exec REG = cmp ne W0 , W1 => #load REG 0 ... </k> requires W0 ==Int W1
Hashing
The sha3 instruction computes the keccak256 hash of an entire memory cell.
rule <k> #exec REG = sha3 MEMINDEX => #load REG keccak(LM) ... </k>
<localMem>... MEMINDEX |-> LM ...</localMem>
rule <k> #exec REG = sha3 MEMINDEX => #load REG keccak(.Bytes) ... </k>
<localMem> LM </localMem>
requires notBool MEMINDEX in_keys(LM)
Local State
These operators make queries about the current execution state.
REG = call @iele.gas()returns the gas remaining after executing the current instruction.REG = call @iele.gasprice()returns the gas price of the transaction. This will be removed when we migrate to Cardano.REG = call @iele.gaslimit()returns the gas limit of the current block.REG = call @iele.beneficiary()returns the account who receives payment for mining the current transaction.REG = call @iele.timestamp()returns the time stamp of the current block.REG = call @iele.number()returns the block number of the current block.REG = call @iele.difficulty()returns the difficulty of the current block. This will be removed when we migrate to Cardano.REG = call @iele.address()returns the address of the currently executing account.REG = call @iele.origin()returns the original sender of the current transaction.REG = call @iele.caller()returns the caller of the current contract call.REG = call @iele.callvalue()returns the value transfer of the current contract call.REG = call @iele.msize()returns the current peak memory usage of the current contract call.REG = call @iele.codesize()returns the size in bytes of the currently executing contract.REG = call @iele.blockhash(N)returns the hash of the block header of the Nth previous block.
rule <k> #exec REG = call @iele.gas ( .Ints ) => #load REG (GAVAIL /Int Sgasdivisor < SCHED >) ... </k> <gas> GAVAIL </gas> <schedule> SCHED </schedule>
rule <k> #exec REG = call @iele.gasprice ( .Ints ) => #load REG GPRICE ... </k> <gasPrice> GPRICE </gasPrice>
rule <k> #exec REG = call @iele.gaslimit ( .Ints ) => #load REG GLIMIT ... </k> <gasLimit> GLIMIT </gasLimit>
rule <k> #exec REG = call @iele.beneficiary ( .Ints ) => #load REG CB ... </k> <beneficiary> CB </beneficiary>
rule <k> #exec REG = call @iele.timestamp ( .Ints ) => #load REG TS ... </k> <timestamp> TS </timestamp>
rule <k> #exec REG = call @iele.number ( .Ints ) => #load REG NUMB ... </k> <number> NUMB </number>
rule <k> #exec REG = call @iele.difficulty ( .Ints ) => #load REG DIFF ... </k> <difficulty> DIFF </difficulty>
rule <k> #exec REG = call @iele.address ( .Ints ) => #load REG ACCT ... </k> <id> ACCT </id>
rule <k> #exec REG = call @iele.origin ( .Ints ) => #load REG ORG ... </k> <origin> ORG </origin>
rule <k> #exec REG = call @iele.caller ( .Ints ) => #load REG CL ... </k> <caller> CL </caller>
rule <k> #exec REG = call @iele.callvalue ( .Ints ) => #load REG CV ... </k> <callValue> CV </callValue>
rule <k> #exec REG = call @iele.msize ( .Ints ) => #load REG (MU <<Int 3) ... </k> <peakMemory> MU </peakMemory>
rule <k> #exec REG = call @iele.codesize ( .Ints ) => #load REG SIZE ... </k> <programSize> SIZE </programSize>
rule <k> #exec REG = call @iele.blockhash ( N ) => #load REG #if N >=Int HI orBool HI -Int 256 >Int N orBool N <Int 0 #then 0 #else #parseHexWord(Keccak256(Int2String(N))) #fi ... </k> <number> HI </number> <mode> VMTESTS </mode>
rule <k> #exec REG = call @iele.blockhash ( N ) => #load REG #blockhash(HASHES, N, HI -Int 1, 0) ... </k> <number> HI </number> <blockhash> HASHES </blockhash> <mode> NORMAL </mode>
syntax Int ::= #blockhash ( List , Int , Int , Int ) [function]
// ---------------------------------------------------------------
rule #blockhash(_, N, HI, _) => 0 requires N >Int HI orBool N <Int 0
rule #blockhash(_, _, _, 256) => 0
rule #blockhash(ListItem(0) _, _, _, _) => 0
rule #blockhash(ListItem(H) _, N, N, _) => H
rule #blockhash(ListItem(_) L, N, HI, A) => #blockhash(L, N, HI -Int 1, A +Int 1) [owise]
Branch and Local Call
The br instruction jumps to a specified label, either unconditionally, or if its argument is nonzero.
The call instruction for local calls (i.e. the form which does not specify an account, value, or gas limit), calls a function in the current contract.
The called function executes in the same contract call frame (i.e. with the same value, gas limit, and memory), but with a fresh set of local registers.
When execution of the callee reaches a ret instruction, control returns to the instruction following the call, and local registers are restored.
rule <k> _:IeleName : INSTRS BLOCKS::LabeledBlocks => INSTRS BLOCKS ... </k>
<typeChecking> false </typeChecking>
rule <k> #exec br LABEL ~> _:Blocks => CODE ... </k> <fid> FUNC </fid> <function>... <funcId> FUNC </funcId> <jumpTable> ... LABEL |-> CODE </jumpTable> </function>
rule <k> #exec br I:Int , LABEL ~> _:Blocks => CODE ... </k> <fid> FUNC </fid> <function>... <funcId> FUNC </funcId> <jumpTable> ... LABEL |-> CODE </jumpTable> </function> requires I =/=K 0
rule <k> #exec br 0 , _LABEL => . ... </k>
syntax LocalCall ::= "{" Blocks "|" IeleName "|" LValues "|" Array "}"
// ----------------------------------------------------------------------
rule <k> #exec RETURNS = call @ LABEL ( ARGS ) ~> OPS:Blocks => #loads #regRange(#sizeRegs(ARGS)) ARGS ~> #execute ... </k>
<fid> FUNC => LABEL </fid>
<regs> REGS => .Array </regs>
<localCalls> .List => ListItem({ OPS | FUNC | RETURNS | REGS }) ... </localCalls>
requires notBool isIeleBuiltin(LABEL)
rule <k> #exec _ = call (IDX:Int => @ LABEL) ( ARGS ) ... </k>
<funcLabels> ... IDX |-> LABEL ... </funcLabels>
<funcId> LABEL </funcId>
<nparams> NPARAMS </nparams>
requires #sizeRegs(ARGS) ==Int NPARAMS
rule <k> #exec _ = call IDX:Int ( _ ) => #exception FUNC_NOT_FOUND ...</k>
<funcLabels> LBLS </funcLabels>
requires notBool IDX in_keys(LBLS)
rule <k> #exec _ = call IDX:Int ( ARGS ) => #if LABEL ==K init andBool SCHED =/=K ALBE #then FUNC_NOT_FOUND #else #exception FUNC_WRONG_SIG #fi ... </k>
<funcLabels> ... IDX |-> LABEL ... </funcLabels>
<funcId> LABEL </funcId>
<nparams> NPARAMS </nparams>
<schedule> SCHED </schedule>
requires #sizeRegs(ARGS) =/=Int NPARAMS orBool (LABEL ==K init andBool SCHED =/=K ALBE)
syntax Bool ::= isIeleBuiltin(IeleName) [function]
// --------------------------------------------------
rule isIeleBuiltin(iele.invalid) => true
rule isIeleBuiltin(iele.gas) => true
rule isIeleBuiltin(iele.gasprice) => true
rule isIeleBuiltin(iele.gaslimit) => true
rule isIeleBuiltin(iele.beneficiary) => true
rule isIeleBuiltin(iele.timestamp) => true
rule isIeleBuiltin(iele.number) => true
rule isIeleBuiltin(iele.difficulty) => true
rule isIeleBuiltin(iele.address) => true
rule isIeleBuiltin(iele.origin) => true
rule isIeleBuiltin(iele.caller) => true
rule isIeleBuiltin(iele.callvalue) => true
rule isIeleBuiltin(iele.msize) => true
rule isIeleBuiltin(iele.codesize) => true
rule isIeleBuiltin(iele.blockhash) => true
rule isIeleBuiltin(iele.balance) => true
rule isIeleBuiltin(iele.extcodesize) => true
rule isIeleBuiltin(iele.ecrec) => true
rule isIeleBuiltin(iele.sha256) => true
rule isIeleBuiltin(iele.rip160) => true
rule isIeleBuiltin(iele.id) => true
rule isIeleBuiltin(iele.ecadd) => true
rule isIeleBuiltin(iele.ecmul) => true
rule isIeleBuiltin(iele.ecpairing) => true
rule isIeleBuiltin( ... ) => false [owise]
ret and revert
retreturns the values contained in the specified list of registers to the caller. If we are executing inside a previous local call, the contract call frame persists unchanged, and only the instruction position and local register are affected. If we are executing at the top-level local call of a contract call frame, we return to the contract call's caller.revertreturns the value of the single specified register to the contract call's caller, but signifies that the contract has failed, which rolls back state changes and returns an error code to the caller.
rule <k> #exec ret VALUES => #end ... </k>
<output> _ => VALUES </output>
<localCalls> .List </localCalls>
rule <k> #exec ret VALUES ~> _:Blocks => #registerDeltas(RETURNS, VALUES) ~> #loads RETURNS VALUES ~> OPS ... </k>
<fid> _ => FUNC </fid>
<regs> _ => REGS </regs>
<localCalls> ListItem({ OPS | FUNC | RETURNS | REGS }) => .List ... </localCalls>
rule <k> #exec revert VALUE => #revert VALUE ... </k>
<output> _ => .Ints </output>
Log Operations
During execution of a transaction some things are recorded in the substate log.
This is a right cons-list of SubstateLogEntry (which contains the account ID along with the specified portions of the wordStack and localMem).
The log instruction logs an entire memory cell to the substate log with zero to four log topics.
syntax SubstateLogEntry ::= "{" Int "|" List "|" Bytes "}" [klabel(logEntry)]
// ---------------------------------------------------------------------------------
rule #exec log MEMINDEX => #log MEMINDEX .List
rule #exec log MEMINDEX , W0 => #log MEMINDEX ListItem(chop(W0))
rule #exec log MEMINDEX , W0 , W1 => #log MEMINDEX ListItem(chop(W0)) ListItem(chop(W1))
rule #exec log MEMINDEX , W0 , W1 , W2 => #log MEMINDEX ListItem(chop(W0)) ListItem(chop(W1)) ListItem(chop(W2))
rule #exec log MEMINDEX , W0 , W1 , W2 , W3 => #log MEMINDEX ListItem(chop(W0)) ListItem(chop(W1)) ListItem(chop(W2)) ListItem(chop(W3))
syntax InternalOp ::= "#log" Int List
// -------------------------------------
rule <k> #log MEMINDEX TOPICS => . ... </k>
<id> ACCT </id>
<localMem>... MEMINDEX |-> LM ...</localMem>
<logData> ... (.List => ListItem({ ACCT | TOPICS | LM })) </logData>
Network Ops
Operators that require access to the rest of the IELE network world-state can be taken as a first draft of a "blockchain generic" language.
Account Queries
REG = call @iele.balance(ACCT)returns the balance of the specified account (zero if the account does not exist).REG = call @iele.extcodesize(ACCT)returns the code si of the specified account (zero if the account does not exist).REG = calladdress NAME at ACCTreturns the function pointer pointing to the function named NAME on the specified account (zero if the function does not exist)
rule <k> #exec REG = call @iele.balance ( ACCT ) => #load REG BAL ... </k>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
rule <k> (.K => #loadAccount ACCT) ~> #exec _REG = call @iele.balance ( ACCT ) ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in ACCTS
rule <k> #exec REG = call @iele.extcodesize ( ACCT ) => #load REG #contractSize(CODE, #mainContract(CODE)) ... </k>
<account>
<acctID> ACCT </acctID>
<code> CODE </code>
...
</account>
requires CODE =/=K .Contract
rule <k> (.K => #lookupCode(ACCT)) ~> #exec _ = call @iele.extcodesize ( ACCT ) ... </k>
<account>
<acctID> ACCT </acctID>
<code> .Contract </code>
...
</account>
rule <k> (.K => #loadAccount ACCT) ~> #exec _ = call @iele.extcodesize ( ACCT ) ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in ACCTS
rule <k> (.K => #loadAccount ACCT) ~> #exec _ = calladdress _ at ACCT ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in ACCTS
rule <k> (.K => #lookupCode(ACCT)) ~> #exec _ = calladdress _ at ACCT ... </k>
<account>
<acctID> ACCT </acctID>
<code> .Contract </code>
...
</account>
rule <k> #exec REG = calladdress @ NAME at ACCT => #load REG #callAddress(CODE, #mainContract(CODE), NAME) ... </k>
<account>
<acctID> ACCT </acctID>
<code> CODE </code>
...
</account>
requires CODE =/=K .Contract
Account Storage Operations
These operations interact with the account storage.
REG = sload INDEXloads the word at INDEX from the account storage.sstore VALUE, INDEXstores the VALUE at INDEX in the account storage.
rule <k> #exec REG = sload INDEX => #load REG VALUE ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> ... INDEX |-> VALUE ... </storage>
...
</account>
rule <k> #exec sstore VALUE , INDEX => . ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> ... (INDEX |-> (OLD => VALUE)) ... </storage>
...
</account>
<refund> R => R +Int Rsstoreset < SCHED > *Int maxInt(0, intSize(OLD) -Int intSize(VALUE)) </refund>
<schedule> SCHED </schedule>
Call Operations
The various call* (and other inter-contract control flow) operations will be desugared into these InternalOps.
#checkCallchecks that the current account has the balance necessary to invoke the contract call, and that the contract call stack depth limit has not been reached.#call_____takes the calling account, the account to execute as, the account whose code should execute, the gas limit, the amount to transfer, the function to call, and the arguments.#callWithCode______takes the calling account, the accout to execute as, the code to execute (as a map), the gas limit, the amount to transfer, the function to call, and the arguments.#return__is a placeholder for the calling program, specifying where to place the returned data in registers.
syntax InternalOp ::= "#checkCall" Int Int Int
| "#call" Int Int Constant Operand Int Ints Bool [strict(4)]
| "#callWithCode" Int Int ProgramCell Constant Int Int Ints Bool
| "#mkCall" Int Int ProgramCell IeleName Int Int Ints Bool
// ----------------------------------------------------------------------------------
rule <k> #checkCall ACCT VALUE _GCAP ~> #call _ _ _ GLIMIT _ _ _ => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception (#if VALUE >Int BAL #then OUT_OF_FUNDS #else CALL_STACK_OVERFLOW #fi) ... </k>
<callDepth> CD </callDepth>
<output> _ => .Ints </output>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
requires VALUE >Int BAL orBool CD >=Int 1024
rule <k> #checkCall ACCT VALUE _GCAP => . ... </k>
<callDepth> CD </callDepth>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
requires notBool (VALUE >Int BAL orBool CD >=Int 1024)
rule <k> #call ACCTFROM ACCTTO FUNC GLIMIT:Int VALUE ARGS STATIC
=> #callWithCode ACCTFROM ACCTTO #precompiled FUNC GLIMIT VALUE ARGS STATIC
...
</k>
requires ACCTTO ==Int #precompiledAccount
rule <k> #call ACCTFROM ACCTTO FUNC GLIMIT:Int VALUE ARGS STATIC
=> #callWithCode ACCTFROM ACCTTO #loadCode(CODE) FUNC GLIMIT VALUE ARGS STATIC
...
</k>
<acctID> ACCTTO </acctID>
<code> CODE </code>
requires ACCTTO =/=Int #precompiledAccount andBool CODE =/=K .Contract
rule <k> (.K => #lookupCode(ACCT)) ~> #call _ ACCT _ _ _ _ _ ... </k>
<acctID> ACCT </acctID>
<code> .Contract </code>
requires ACCT =/=Int #precompiledAccount
rule <k> (.K => #loadAccount ACCT) ~> #call _ ACCT _ _ _ _ _ ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires ACCT =/=Int #precompiledAccount andBool notBool ACCT in ACCTS
rule #callWithCode ACCTFROM ACCTTO CODE @ FUNC GLIMIT VALUE ARGS STATIC
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate
~> #transferFunds ACCTFROM ACCTTO VALUE
~> #mkCall ACCTFROM ACCTTO CODE FUNC GLIMIT VALUE ARGS STATIC
rule #callWithCode _ACCTFROM _ACCTTO <program>... <funcLabels> LBLS </funcLabels> ...</program> IDX:Int _GLIMIT _VALUE _ARGS _STATIC
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception FUNC_NOT_FOUND
requires notBool IDX in_keys(LBLS)
rule #callWithCode ACCTFROM ACCTTO (<program>... <funcLabels>... IDX |-> FUNC </funcLabels> ...</program> #as CODE) IDX:Int GLIMIT VALUE ARGS STATIC
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate
~> #transferFunds ACCTFROM ACCTTO VALUE
~> #mkCall ACCTFROM ACCTTO CODE FUNC GLIMIT VALUE ARGS STATIC
rule <k> #mkCall ACCTFROM ACCTTO CODE FUNC GLIMIT VALUE ARGS STATIC:Bool
=> #initVM(ARGS) ~> #initFun(FUNC, #sizeRegs(ARGS), false)
...
</k>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => VALUE </callValue>
<id> _ => ACCTTO </id>
<gas> _ => GLIMIT </gas>
<caller> _ => ACCTFROM </caller>
(<program> _ </program> => CODE:ProgramCell)
<static> OLDSTATIC:Bool => OLDSTATIC orBool STATIC </static>
The VM starts out with empty memory, output, registers, and local call stack. If the function being called is not public, does not exist, or has the wrong number of arguments, an exception is raised.
syntax KItem ::= #initVM ( Ints )
| #initFun ( IeleName , Int , Bool )
// ---------------------------------------------------
rule <k> #initVM(ARGS) => #loads #regRange(#sizeRegs(ARGS)) ARGS ... </k>
<currentMemory> _ => 0 </currentMemory>
<peakMemory> _ => 0 </peakMemory>
<output> _ => .Ints </output>
<regs> _ => .Array </regs>
<localMem> _ => .Map </localMem>
<localCalls> _ => .List </localCalls>
rule <k> #initFun(LABEL, _, false) => #exception FUNC_NOT_FOUND ... </k>
<exported> FUNCS </exported>
<funcIds> LABELS </funcIds>
requires notBool LABEL in FUNCS
andBool LABEL in LABELS
rule <k> #initFun(LABEL, _, _) => #exception (#if SIZE ==Int 0 #then CONTRACT_NOT_FOUND #else FUNC_NOT_FOUND #fi) ... </k>
<funcIds> LABELS </funcIds>
<programSize> SIZE </programSize>
requires notBool LABEL in LABELS
rule <k> #initFun(LABEL, NARGS, _) => #exception FUNC_WRONG_SIG ... </k>
<funcId> LABEL </funcId>
<nparams> NPARAMS </nparams>
requires NARGS =/=Int NPARAMS
rule <k> #initFun(LABEL, NARGS, ISCREATE:Bool) => #if EXECMODE ==K VMTESTS #then #end #else #execute #fi ... </k>
<mode> EXECMODE </mode>
<funcIds> ... SetItem(LABEL) </funcIds>
<exported> FUNCS </exported>
<fid> _ => LABEL </fid>
<nregs> REGISTERS </nregs>
<currentMemory> _ => REGISTERS </currentMemory>
<peakMemory> _ => REGISTERS </peakMemory>
<funcId> LABEL </funcId>
<nparams> NPARAMS </nparams>
requires (LABEL in FUNCS orBool ISCREATE) andBool (NPARAMS ==Int NARGS)
syntax KItem ::= "#return" LValues LValue
// -----------------------------------------
rule <k> #exception STATUS ~> #return _ REG
=> #popCallStack ~> #popWorldState ~> #popSubstate ~> #registerDelta(REG, 1) ~> #load REG STATUS
...
</k>
<output> _ => .Ints </output>
rule <k> #revert OUT ~> #return _ REG
=> #popCallStack
~> #popWorldState
~> #popSubstate
~> #registerDelta(REG, intSize(OUT))
~> #load REG OUT ~> #refund GAVAIL
...
</k>
<gas> GAVAIL </gas>
rule <mode> EXECMODE </mode>
<k> #end ~> #return REGS REG
=> #popCallStack
~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi
~> #dropSubstate
~> #registerDelta(REG, 1)
~> #registerDeltas(REGS, OUT)
~> #load REG 0 ~> #refund GAVAIL ~> #if EXECMODE ==K VMTESTS #then .K #else #loads REGS OUT #fi
...
</k>
<output> OUT </output>
<gas> GAVAIL </gas>
syntax InternalOp ::= "#refund" Operand [strict]
// -----------------------------------
rule <k> #refund G:Int => . ... </k> <gas> GAVAIL => GAVAIL +Int G </gas>
For each call* operation, we make a corresponding call to #call and a state-change to setup the custom parts of the calling environment.
rule <k> #exec REG , REGS = call LABEL at ACCTTO ( ARGS ) send VALUE , gaslimit GCAP
=> #checkCall ACCTFROM VALUE GCAP
~> #call ACCTFROM ACCTTO LABEL Ccallgas(SCHED, #accountEmpty(ACCTTO), GCAP *Int Sgasdivisor < SCHED >, GAVAIL, VALUE, #sizeLVals(REGS), Ccallarg(SCHED, ARGS)) VALUE ARGS false
~> #return REGS REG
...
</k>
<schedule> SCHED </schedule>
<id> ACCTFROM </id>
<previousGas> GAVAIL </previousGas>
rule <k> #exec REG , REGS = staticcall LABEL at ACCTTO ( ARGS ) gaslimit GCAP
=> #checkCall ACCTFROM 0 GCAP
~> #call ACCTFROM ACCTTO LABEL Ccallgas(SCHED, #accountEmpty(ACCTTO), GCAP *Int Sgasdivisor < SCHED >, GAVAIL, 0, #sizeLVals(REGS), Ccallarg(SCHED, ARGS)) 0 ARGS true
~> #return REGS REG
...
</k>
<schedule> SCHED </schedule>
<id> ACCTFROM </id>
<previousGas> GAVAIL </previousGas>
Account Creation/Deletion
#create____transfers the endowment to the new account and triggers the execution of the initialization code.#codeDeposit_checks the result of initialization code and whether the code deposit can be paid, indicating an error if not.#checkCreatechecks that the account has sufficient balance for the balance transfer, that the call depth limit is not reached, and increments the nonce of the creator account.
syntax InternalOp ::= "#create" Int Int Int Int Contract Ints
| "#mkCreate" Int Int Contract Int Int Ints
| "#checkCreate" Int Int
| "#checkContract" Contract
| "#finishTypeChecking"
syntax Contract ::= "#illFormed"
// --------------------------------
rule <k> #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception (#if VALUE >Int BAL #then OUT_OF_FUNDS #else CALL_STACK_OVERFLOW #fi) ... </k>
<callDepth> CD </callDepth>
<output> _ => .Ints </output>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
requires VALUE >Int BAL orBool CD >=Int 1024
rule <k> #checkCreate ACCT VALUE => . ... </k>
<mode> EXECMODE </mode>
<callDepth> CD </callDepth>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
<nonce> NONCE => #if EXECMODE ==K VMTESTS #then NONCE #else NONCE +Int 1 #fi </nonce>
...
</account>
requires notBool (VALUE >Int BAL orBool VALUE <Int 0 orBool CD >=Int 1024)
rule <k> #checkContract CONTRACT => CONTRACT ~> #finishTypeChecking ... </k>
(_:WellFormednessCheckerCell =>
<well-formedness-checker>
<typeChecking> true </typeChecking>
<well-formedness-schedule> SCHED </well-formedness-schedule>
...
</well-formedness-checker>)
<schedule> SCHED </schedule>
rule <k> #finishTypeChecking => . ... </k>
<typeChecking> _ => false </typeChecking>
rule <k> . => #illFormed ... </k>
<typeChecking> true </typeChecking>
[owise]
rule <k> #illFormed ~> (K:KItem => .) ... </k>
requires K =/=K #finishTypeChecking
rule <k> #illFormed ~> #finishTypeChecking ~> #create _ _ GAVAIL _ _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception CONTRACT_INVALID ... </k>
<typeChecking> true => false </typeChecking>
rule #create ACCTFROM ACCTTO GAVAIL VALUE CODE ARGS
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate
~> #initAccount ACCTTO
~> #transferFunds ACCTFROM ACCTTO VALUE
~> #mkCreate ACCTFROM ACCTTO CODE GAVAIL VALUE ARGS
rule <k> #mkCreate ACCTFROM ACCTTO CODE GAVAIL VALUE ARGS
=> #initVM(ARGS) ~> #initFun(init, #sizeRegs(ARGS), true)
...
</k>
<id> _ => ACCTTO </id>
<gas> _ => GAVAIL </gas>
(<program> _ </program> => #loadCode(CODE))
<caller> _ => ACCTFROM </caller>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => .Ints </callData>
<callValue> _ => VALUE </callValue>
<account>
<acctID> ACCTTO </acctID>
<nonce> NONCE => NONCE +Int 1 </nonce>
<code> _ => CODE </code>
...
</account>
syntax Contract ::= #subcontract ( Contract , IeleName ) [function]
// -------------------------------------------------------------------
rule #subcontract ( (contract NAME ! _ _ { _ } #as CONTRACT) _, NAME ) => CONTRACT .Contract
rule #subcontract ( CONTRACT CONTRACTS, NAME ) => CONTRACT #subcontract(CONTRACTS, NAME) [owise]
syntax KItem ::= "#codeDeposit" Int Int LValue LValue Bool
| "#mkCodeDeposit" Int Int LValue LValue Bool
| "#finishCodeDeposit" Int LValue LValue Bool
// ----------------------------------------------------------------
rule <k> #exception STATUS ~> #codeDeposit _ _ REG _ NEW:Bool => #popCallStack ~> #popWorldState ~> #popSubstate ~> #if NEW #then STATUS #else #registerDelta(REG, 1) ~> #load REG STATUS #fi ... </k> <output> _ => .Ints </output>
rule <k> #revert OUT ~> #codeDeposit _ _ REG _ NEW:Bool => #popCallStack ~> #popWorldState ~> #popSubstate ~> #if NEW #then #refund GAVAIL ~> OUT #else #registerDelta(REG, intSize(OUT)) ~> #refund GAVAIL ~> #load REG OUT #fi ... </k>
<gas> GAVAIL </gas>
rule <k> #end ~> #codeDeposit ACCT LEN STATUS ACCTOUT NEW => #mkCodeDeposit ACCT LEN STATUS ACCTOUT NEW ... </k>
rule <k> #mkCodeDeposit ACCT LEN STATUS ACCTOUT NEW:Bool
=> #if EXECMODE ==K VMTESTS orBool notBool NEW #then . #else Gcodedeposit < SCHED > *Int LEN ~> #deductGas #fi
~> #finishCodeDeposit ACCT STATUS ACCTOUT NEW
...
</k>
<mode> EXECMODE </mode>
<schedule> SCHED </schedule>
<output> .Ints </output>
rule <k> #finishCodeDeposit ACCT STATUS ACCTOUT NEW:Bool
=> #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate
~> #if NEW #then #refund GAVAIL ~> 0 #else #registerDelta(STATUS, 1) ~> #registerDelta(ACCTOUT, 3) ~> #refund GAVAIL ~> #load STATUS 0 ~> #load ACCTOUT ACCT #fi
...
</k>
<mode> EXECMODE </mode>
<gas> GAVAIL </gas>
<output> _ => ACCT , .Ints </output>
rule <k> #exception STATUS ~> #finishCodeDeposit _ REG _ NEW:Bool => #popCallStack ~> #popWorldState ~> #popSubstate ~> #if NEW #then STATUS #else #registerDelta(REG, 1) ~> #load REG STATUS #fi ... </k>
createwill attempt to#createthe named contract using the initialization code and cleans up the result with#codeDeposit.copycreatewill attempt to#createa copy of the contract at the specified address using the initialization code and cleans up the result with#codeDeposit
rule <k> #exec STATUS , ACCTOUT = create NAME ( ARGS ) send VALUE
=> #checkCreate ACCT VALUE
~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #subcontract(CODE, NAME) ARGS
~> #codeDeposit #newAddr(ACCT, NONCE) #contractSize(CODE, NAME) STATUS ACCTOUT false
...
</k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<gas> GAVAIL => #if Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi </gas>
<account>
<acctID> ACCT </acctID>
<nonce> NONCE </nonce>
...
</account>
<contractCode> CODE </contractCode>
rule <k> #exec STATUS , ACCTOUT = copycreate ACCTCODE ( ARGS ) send VALUE
=> #checkCreate ACCT VALUE
~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE CODE ARGS
~> #codeDeposit #newAddr(ACCT, NONCE) #contractSize(CODE, #mainContract(CODE)) STATUS ACCTOUT false
...
</k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<gas> GAVAIL => #if Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi </gas>
<account>
<acctID> ACCT </acctID>
<nonce> NONCE </nonce>
...
</account>
<account>
<acctID> ACCTCODE </acctID>
<code> CODE </code>
...
</account>
requires ACCT =/=Int ACCTCODE andBool CODE =/=K .Contract
rule <k> (.K => #lookupCode(ACCTCODE)) ~> #exec _ , _ = copycreate ACCTCODE ( _ ) send _ ... </k>
<account>
<acctID> ACCTCODE </acctID>
<code> .Contract </code>
...
</account>
rule <k> #exec STATUS , ACCTOUT = copycreate ACCT ( ARGS ) send VALUE
=> #checkCreate ACCT VALUE
~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE CODE ARGS
~> #codeDeposit #newAddr(ACCT, NONCE) #contractSize(CODE, #mainContract(CODE)) STATUS ACCTOUT false
...
</k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<gas> GAVAIL => #if Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi </gas>
<account>
<acctID> ACCT </acctID>
<nonce> NONCE </nonce>
<code> CODE </code>
...
</account>
rule <k> (.K => #loadAccount ACCT) ~> #exec _ , _ = copycreate ACCT ( _ ) send _ ... </k> <activeAccounts> ACCTS </activeAccounts> requires notBool ACCT in ACCTS
selfdestruct marks the current account for deletion and transfers funds out of the current account.
Self destructing to yourself, unlike a regular transfer, destroys the balance in the account, irreparably losing it.
rule <k> #exec selfdestruct ACCTTO => #transferFunds ACCT ACCTTO BALFROM ~> #end ... </k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<selfDestruct> SDS (.Set => SetItem(ACCT)) </selfDestruct>
<refund> RF => #if ACCT in SDS #then RF #else RF +Int Rselfdestruct < SCHED > #fi </refund>
<account>
<acctID> ACCT </acctID>
<balance> BALFROM </balance>
...
</account>
<output> _ => .Ints </output>
requires ACCT =/=Int ACCTTO
rule <k> #exec selfdestruct ACCT => #end ... </k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<selfDestruct> SDS (.Set => SetItem(ACCT)) </selfDestruct>
<refund> RF => #if ACCT in SDS #then RF #else RF +Int Rselfdestruct < SCHED > #fi </refund>
<account>
<acctID> ACCT </acctID>
<balance> _ => 0 </balance>
...
</account>
<output> _ => .Ints </output>
endmodule
Precompiled Contract
#precompiledis a placeholder for the pre-compiled contracts at addresses 1.
module IELE-PRECOMPILED
imports IELE-DATA
imports IELE-CONFIGURATION
imports IELE-INFRASTRUCTURE
syntax Int ::= "#precompiledAccount" [function]
// -----------------------------------------------
rule #precompiledAccount => 1
syntax ProgramCell ::= "#precompiled" [function]
// ------------------------------------------------
rule #precompiled =>
<program>
<functions>
<function> <funcId> iele.ecrec </funcId> <instructions> ECREC .Instructions .LabeledBlocks </instructions> <nparams> 4 </nparams> ... </function>
<function> <funcId> iele.sha256 </funcId> <instructions> SHA256 .Instructions .LabeledBlocks </instructions> <nparams> 2 </nparams> ... </function>
<function> <funcId> iele.rip160 </funcId> <instructions> RIP160 .Instructions .LabeledBlocks </instructions> <nparams> 2 </nparams> ... </function>
<function> <funcId> iele.id </funcId> <instructions> ID .Instructions .LabeledBlocks </instructions> <nparams> 1 </nparams> ... </function>
<function> <funcId> iele.ecadd </funcId> <instructions> ECADD .Instructions .LabeledBlocks </instructions> <nparams> 4 </nparams> ... </function>
<function> <funcId> iele.ecmul </funcId> <instructions> ECMUL .Instructions .LabeledBlocks </instructions> <nparams> 3 </nparams> ... </function>
<function> <funcId> iele.ecpairing </funcId> <instructions> ECPAIRING .Instructions .LabeledBlocks </instructions> <nparams> 3 </nparams> ... </function>
</functions>
<funcIds>
SetItem(iele.ecrec)
SetItem(iele.sha256)
SetItem(iele.rip160)
SetItem(iele.id)
SetItem(iele.ecadd)
SetItem(iele.ecmul)
SetItem(iele.ecpairing)
</funcIds>
<exported>
SetItem(iele.ecrec)
SetItem(iele.sha256)
SetItem(iele.rip160)
SetItem(iele.id)
SetItem(iele.ecadd)
SetItem(iele.ecmul)
SetItem(iele.ecpairing)
</exported>
<funcLabels>
1 |-> iele.ecrec
2 |-> iele.sha256
3 |-> iele.rip160
4 |-> iele.id
5 |-> iele.ecadd
6 |-> iele.ecmul
7 |-> iele.ecpairing
</funcLabels>
...
</program>
@iele.ecrecperforms ECDSA public key recovery.@iele.sha256performs the SHA2-256 hash function.@iele.rip160performs the RIPEMD-160 hash function.@iele.idis the identity function (copies input to output).@iele.ecaddis the BN128 elliptic curve addition function.@iele.ecmulis the BN128 elliptic curve scalar multiplication function.@iele.ecpairingis the BN128 elliptic curve pairing check function.
syntax Instruction ::= PrecompiledOp
syntax KResult ::= PrecompiledOp
syntax PrecompiledOp ::= "ECREC"
// --------------------------------
rule <k> #exec ECREC => #end ... </k>
<callData> HASH , V , R , S , .Ints </callData>
<output> _ => #ecrec(#sender(Bytes2String(Int2Bytes(32, HASH, BE)), V, Bytes2String(Int2Bytes(32, R, BE)), Bytes2String(Int2Bytes(32, S, BE)))) </output>
requires HASH >=Int 0 andBool V >=Int 0 andBool R >=Int 0 andBool S >=Int 0
rule <k> #exec ECREC => #exception USER_ERROR ... </k>
<callData> HASH , V , R , S , .Ints </callData>
requires notBool (HASH >=Int 0 andBool V >=Int 0 andBool R >=Int 0 andBool S >=Int 0)
syntax Ints ::= #ecrec ( Account ) [function]
// ---------------------------------------------
rule #ecrec(.Account) => -1 , .Ints
rule #ecrec(N:Int) => N , .Ints
syntax PrecompiledOp ::= "SHA256"
// ---------------------------------
rule <k> #exec SHA256 => #end ... </k>
<callData> LEN , DATA , .Ints </callData>
<output> _ => #parseHexWord(Sha256(Bytes2String(Int2Bytes(LEN, DATA, BE)))), .Ints </output>
requires LEN >=Int 0 andBool DATA >=Int 0
rule <k> #exec SHA256 => #exception USER_ERROR ... </k>
<callData> LEN , DATA , .Ints </callData>
requires notBool (LEN >=Int 0 andBool DATA >=Int 0)
syntax PrecompiledOp ::= "RIP160"
// ---------------------------------
rule <k> #exec RIP160 => #end ... </k>
<callData> LEN , DATA , .Ints </callData>
<output> _ => #parseHexWord(RipEmd160(Bytes2String(Int2Bytes(LEN, DATA, BE)))), .Ints </output>
requires LEN >=Int 0 andBool DATA >=Int 0
rule <k> #exec RIP160 => #exception USER_ERROR ... </k>
<callData> LEN , DATA , .Ints </callData>
requires notBool (LEN >=Int 0 andBool DATA >=Int 0)
syntax PrecompiledOp ::= "ID"
// -----------------------------
rule <k> #exec ID => #end ... </k>
<callData> DATA </callData>
<output> _ => DATA </output>
syntax PrecompiledOp ::= "ECADD"
// --------------------------------
rule <k> #exec ECADD => #ecadd((X1, Y1), (X2, Y2)) ... </k>
<callData> X1 , Y1 , X2 , Y2 , .Ints </callData>
syntax InternalOp ::= #ecadd(G1Point, G1Point)
// ----------------------------------------------
rule #ecadd(P1, P2) => #exception USER_ERROR
requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2)
rule <k> #ecadd(P1, P2) => #end ... </k> <output> _ => #point(BN128Add(P1, P2)) </output>
requires isValidPoint(P1) andBool isValidPoint(P2)
syntax PrecompiledOp ::= "ECMUL"
// --------------------------------
rule <k> #exec ECMUL => #ecmul((X, Y), S) ... </k>
<callData> X , Y , S , .Ints </callData>
syntax InternalOp ::= #ecmul(G1Point, Int)
// ------------------------------------------
rule #ecmul(P, _) => #exception USER_ERROR
requires notBool isValidPoint(P)
rule <k> #ecmul(P, S) => #end ... </k> <output> _ => #point(BN128Mul(P, S)) </output>
requires isValidPoint(P)
syntax Ints ::= #point(G1Point) [function]
// ------------------------------------------
rule #point((X, Y)) => X , Y , .Ints
syntax PrecompiledOp ::= "ECPAIRING"
// ------------------------------------
rule <k> #exec ECPAIRING => #ecpairing(.List, .List, Int2Bytes(chop(LEN) *Int 64, G1, LE), Int2Bytes(chop(LEN) *Int 128, G2, LE), LEN) ... </k>
<callData> LEN, G1, G2, .Ints </callData>
syntax InternalOp ::= #ecpairing(List, List, Bytes, Bytes, Int)
// -----------------------------------------------------------------------
rule (.K => #checkPoint) ~> #ecpairing((.List => ListItem((#asUnsigned(0, 32, G1), #asUnsigned(32, 32, G1))::G1Point)) _, (.List => ListItem((#asUnsigned(32, 32, G2) x #asUnsigned(0, 32, G2) , #asUnsigned(96, 32, G2) x #asUnsigned(64, 32, G2)))) _, G1 => G1 [ 64 .. lengthBytes(G1) ], G2 => G2 [ 128 .. lengthBytes(G2) ], LEN => LEN -Int 1)
requires LEN >Int 0
rule <k> #ecpairing(A, B, _, _, 0) => #end ... </k>
<output> _ => bool2Word(BN128AtePairing(A, B)) , .Ints </output>
syntax InternalOp ::= "#checkPoint"
// -----------------------------------
rule (#checkPoint => .) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _)
requires isValidPoint(AK) andBool isValidPoint(BK)
rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception USER_ERROR
requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK)
endmodule
IELE Program Representations
The following code processes a Contract and loads it into the <program> cell.
module IELE-PROGRAM-LOADING
imports IELE-COMMON
imports IELE-CONFIGURATION
// when type checking contracts
rule contract NAME ! _ _ { DEFS } => contract NAME { DEFS }
syntax FunctionParameters ::= Int /* when desugared to just the number of parameters */
syntax ProgramCell ::= #loadCode ( Contract ) [function]
| #loadCode ( Contract , Contract ) [klabel(#loadCodeAux), function]
// -----------------------------------------------------------------------------------------
rule #loadCode(contract _ ! _ _ { _ } CONTRACTS, CONTRACT) => #loadCode(CONTRACTS, CONTRACT)
requires CONTRACTS =/=K .Contract
rule #loadCode(contract _ ! SIZE _ { DEFS }, CONTRACT)
=> #loadDeclarations(DEFS,
<program>
<functions> .Bag </functions>
<funcIds> .Set </funcIds>
<funcLabels> .Map </funcLabels>
<programSize> SIZE </programSize>
<exported> .Set </exported>
<contractCode> CONTRACT </contractCode>
</program>, 1)
[owise]
rule #loadCode(CONTRACT) => #loadCode(CONTRACT, CONTRACT)
syntax ProgramCell ::= #loadDeclarations ( TopLevelDefinitions , ProgramCell , Int ) [function]
| #loadFunction ( TopLevelDefinitions , Blocks , ProgramCell , IeleName , FunctionCell , Int ) [function]
// -------------------------------------------------------------------------------------------------------------------------
rule #loadDeclarations(define @ NAME ( NARGS:Int ) { BLOCKS } FUNCS, <program> PROG </program>, IDX)
=> #loadFunction(FUNCS, BLOCKS, <program> PROG </program>, NAME, <function> <funcId> NAME </funcId> <nparams> NARGS </nparams> ... </function>, IDX)
rule #loadDeclarations(define public @ NAME ( NARGS:Int ) { BLOCKS } FUNCS, <program> <exported> EXPORTS </exported> REST </program>, IDX)
=> #loadFunction(FUNCS, BLOCKS, <program> <exported> SetItem(NAME) EXPORTS </exported> REST </program>, NAME, <function> <funcId> NAME </funcId> <nparams> NARGS </nparams> ... </function>, IDX)
rule #loadDeclarations(external contract _ FUNCS, <program> PROG </program>, IDX)
=> #loadDeclarations(FUNCS, <program> PROG </program>, IDX)
rule #loadDeclarations(.TopLevelDefinitions, <program> PROG </program>, _) => <program> PROG </program>
rule #loadFunction(FUNCS, BLOCKS, <program> PROG <functions> REST </functions> <funcIds> NAMES </funcIds> <funcLabels> LBLS </funcLabels> </program>, NAME, <function> FUNC <instructions> _ </instructions> <jumpTable> _ </jumpTable> <nregs> _ </nregs> </function>, IDX)
=> #loadDeclarations(FUNCS, <program> PROG <funcIds> NAMES SetItem(NAME) </funcIds> <funcLabels> LBLS #if NAME =/=K init #then IDX |-> NAME #else .Map #fi </funcLabels> <functions> REST <function> FUNC <instructions> BLOCKS </instructions> <jumpTable> #computeJumpTable(BLOCKS) </jumpTable> <nregs> #computeNRegs(BLOCKS) </nregs> </function> </functions> </program>, #if NAME ==K init #then IDX #else IDX +Int 1 #fi)
syntax IeleName ::= #mainContract ( Contract ) [function]
syntax Int ::= #contractSize ( Contract , IeleName ) [function]
syntax String ::= #contractBytes ( Contract ) [function, klabel(contractBytes), symbol]
| #contractBytes ( Contract , IeleName ) [function, klabel(#contractBytesAux)]
syntax Int ::= #callAddress ( Contract , IeleName , IeleName ) [function]
| #callAddress ( TopLevelDefinitions , IeleName , Int ) [function, klabel(#callAddressAux)]
// --------------------------------------------------------------------------------------------------------
rule #mainContract(contract NAME ! _ _ { _ }) => NAME
rule #mainContract(contract _ ! _ _ { _ } REST) => #mainContract(REST) [owise]
rule #contractSize(contract NAME ! SIZE _ { _ } _, NAME) => SIZE
rule #contractSize(contract _ ! _ _ { _ } REST, NAME) => #contractSize(REST, NAME) [owise]
rule #callAddress(contract NAME ! _ _ { FUNCS } _, NAME, FUNC) => #callAddress(FUNCS, FUNC, 1)
rule #callAddress(contract _ ! _ _ { _ } REST, NAME, FUNC) => #callAddress(REST, NAME, FUNC) [owise]
rule #callAddress(define public @ NAME ( _ ) { _ } _REST, NAME, IDX) => IDX
rule #callAddress(define @init ( _ ) { _ } REST, FUNC, IDX) => #callAddress(REST, FUNC, IDX)
rule #callAddress(define @ NAME ( _ ) { _ } REST, FUNC, IDX) => #callAddress(REST, FUNC, IDX +Int 1)
requires NAME =/=K init
rule #callAddress(define public @ NAME ( _ ) { _ } REST, FUNC, IDX) => #callAddress(REST, FUNC, IDX +Int 1)
requires NAME =/=K FUNC
rule #callAddress(_::TopLevelDefinition REST, FUNC, IDX) => #callAddress(REST, FUNC, IDX) [owise]
rule #callAddress(.TopLevelDefinitions, _, _) => 0
rule #contractBytes(CONTRACT) => #contractBytes(CONTRACT, #mainContract(CONTRACT))
requires CONTRACT =/=K .Contract
rule #contractBytes(.Contract) => ""
rule #contractBytes(contract NAME ! _ BYTES { _ } _, NAME) => BYTES
rule #contractBytes(contract _ ! _ _ { _ } REST, NAME) => #contractBytes(REST, NAME) [owise]
syntax Map ::= #computeJumpTable ( Blocks ) [function]
| #computeJumpTable ( Blocks , Map , Set ) [function, klabel(#computeJumpTableAux)]
// ------------------------------------------------------------------------------------------------
rule #computeJumpTable(BLOCKS) => #computeJumpTable(BLOCKS, .Map, .Set)
rule #computeJumpTable(.LabeledBlocks, JUMPS, _) => JUMPS
rule #computeJumpTable(LABEL : INSTRS BLOCKS, JUMPS, LABELS) => #computeJumpTable(BLOCKS, JUMPS [ LABEL <- INSTRS BLOCKS ], LABELS SetItem(LABEL)) requires notBool LABEL in LABELS
rule #computeJumpTable(_::LabeledBlock BLOCKS, JUMPS, LABELS) => #computeJumpTable(BLOCKS, JUMPS, LABELS) [owise]
rule #computeJumpTable(_::UnlabeledBlock BLOCKS, JUMPS, LABELS) => #computeJumpTable(BLOCKS, JUMPS, LABELS) [owise]
syntax Int ::= #registers ( Instruction ) [function]
| #registers ( LValues ) [function, klabel(registersLValues)]
| #registers ( Operands ) [function, klabel(registersOperands)]
syntax Int ::= #computeNRegs ( Blocks ) [function]
| #computeNRegs ( Blocks , Int ) [function, klabel(#computeNRegsAux)]
// ----------------------------------------------------------------------------------
rule #computeNRegs(BLOCKS) => #computeNRegs(BLOCKS, 0)
rule #computeNRegs(.LabeledBlocks, NREGS) => NREGS
rule #computeNRegs(_LABEL : INSTRS BLOCKS, REGS) => #computeNRegs(INSTRS BLOCKS, REGS)
rule #computeNRegs(INSTR INSTRS::Instructions BLOCKS::LabeledBlocks, NREGS) => #computeNRegs(INSTRS BLOCKS, maxInt(#registers(INSTR) +Int 1, NREGS))
rule #computeNRegs(.Instructions BLOCKS, REGS) => #computeNRegs(BLOCKS, REGS)
rule #registers(% R1 = _:Int) => R1
rule #registers(% R1 = % R2) => maxInt(R1, R2)
rule #registers(% R1 = load % R2) => maxInt(R1, R2)
rule #registers(% R1 = load % R2, % R3, % R4) => maxInt(R1, maxInt(R2, maxInt(R3, R4)))
rule #registers(store % R1, % R2) => maxInt(R1, R2)
rule #registers(store % R1, % R2, % R3, % R4) => maxInt(R1, maxInt(R2, maxInt(R3, R4)))
rule #registers(% R1 = sload % R2) => maxInt(R1, R2)
rule #registers(sstore % R1, % R2) => maxInt(R1, R2)
rule #registers(% R1 = iszero % R2) => maxInt(R1, R2)
rule #registers(% R1 = not % R2) => maxInt(R1, R2)
rule #registers(% R1 = log2 % R2) => maxInt(R1, R2)
rule #registers(% R1 = add % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = mul % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = sub % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = div % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = exp % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = mod % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = addmod % R2, % R3, % R4) => maxInt(R1, maxInt(R2, maxInt(R3, R4)))
rule #registers(% R1 = mulmod % R2, % R3, % R4) => maxInt(R1, maxInt(R2, maxInt(R3, R4)))
rule #registers(% R1 = expmod % R2, % R3, % R4) => maxInt(R1, maxInt(R2, maxInt(R3, R4)))
rule #registers(% R1 = byte % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = sext % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = twos % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = bswap % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = and % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = or % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = xor % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = shift % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = cmp _ % R2, % R3) => maxInt(R1, maxInt(R2, R3))
rule #registers(% R1 = sha3 % R2) => maxInt(R1, R2)
rule #registers(br _) => -1
rule #registers(br % R1, _) => R1
rule #registers(R1 = call @ _ ( R2 )) => maxInt(#registers(R1), #registers(R2))
rule #registers(R1 = call @ _ at % R2 ( R3 ) send % R4, gaslimit % R5) => maxInt(#registers(R1), maxInt(R2, maxInt(#registers(R3), maxInt(R4, R5))))
rule #registers(R1 = staticcall @ _ at % R2 ( R3 ) gaslimit % R4) => maxInt(#registers(R1), maxInt(R2, maxInt(#registers(R3), R4)))
rule #registers(R1 = call % R3 ( R2 )) => maxInt(R3, maxInt(#registers(R1), #registers(R2)))
rule #registers(R1 = call % R6 at % R2 ( R3 ) send % R4, gaslimit % R5) => maxInt(#registers(R1), maxInt(R2, maxInt(#registers(R3), maxInt(R4, maxInt(R5, R6)))))
rule #registers(% R1 = calladdress _ at % R2) => maxInt(R1, R2)
rule #registers(R1 = staticcall % R5 at % R2 ( R3 ) gaslimit % R4) => maxInt(#registers(R1), maxInt(R2, maxInt(#registers(R3), maxInt(R4, R5))))
rule #registers(ret R1::NonEmptyOperands) => #registers(R1)
rule #registers(revert % R1) => R1
rule #registers(log % R1) => R1
rule #registers(log % R1, R2) => maxInt(R1, #registers(R2))
rule #registers(% R1, % R2 = create _ ( R3 ) send % R4) => maxInt(R1, maxInt(R2, maxInt(#registers(R3), R4)))
rule #registers(% R1, % R2 = copycreate % R3 ( R4 ) send % R5) => maxInt(R1, maxInt(R2, maxInt(R3, maxInt(#registers(R4), R5))))
rule #registers(selfdestruct % R1) => R1
rule #registers(% REG, REGS::LValues) => maxInt(REG, #registers(REGS))
rule #registers(% REG, REGS::Operands) => maxInt(REG, #registers(REGS))
rule #registers(.LValues) => -1
rule #registers(.Operands) => -1
endmodule