EVM Execution¶
The EVM is a stack 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, the file ethereum.md will define the
interactions with the world state.
requires "data.k"
module EVM
imports STRING
imports EVM-DATA
Configuration¶
The configuration has cells for the current account id, the current opcode, the program counter, the current gas, the gas price, the current program, the word stack, and the local memory. In addition, there are cells for the callstack and execution substate.
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’ve marked which component of the yellowpaper state corresponds to each cell.
configuration <k> $PGM:EthereumSimulation </k>
<exit-code exit=""> 1 </exit-code>
<mode> $MODE:Mode </mode>
<schedule> $SCHEDULE:Schedule </schedule>
<analysis> .Map </analysis>
<ethereum>
// EVM Specific
// ============
<evm>
// Mutable during a single transaction
// -----------------------------------
<output> .WordStack </output> // H_RETURN
<memoryUsed> 0 </memoryUsed> // \mu_i
<callDepth> 0 </callDepth>
<callStack> .List </callStack>
<interimStates> .List </interimStates>
<substateStack> .List </substateStack>
<callLog> .Set </callLog>
<txExecState>
<program> .Map </program> // I_b
<programBytes> .WordStack </programBytes>
// I_*
<id> 0 </id> // I_a
<caller> 0 </caller> // I_s
<callData> .WordStack </callData> // I_d
<callValue> 0 </callValue> // I_v
// \mu_*
<wordStack> .WordStack </wordStack> // \mu_s
<localMem> .Map </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> 0 </gas> // \mu_g
<previousGas> 0 </previousGas>
</txExecState>
// A_* (execution substate)
<substate>
<selfDestruct> .Set </selfDestruct> // A_s
<log> .List </log> // A_l
<refund> 0 </refund> // A_r
</substate>
// Immutable during a single transaction
// -------------------------------------
<gasPrice> 0 </gasPrice> // I_p
<origin> 0 </origin> // I_o
// I_H* (block information)
<previousHash> 0 </previousHash> // I_Hp
<ommersHash> 0 </ommersHash> // I_Ho
<coinbase> 0 </coinbase> // I_Hc
<stateRoot> 0 </stateRoot> // I_Hr
<transactionsRoot> 0 </transactionsRoot> // I_Ht
<receiptsRoot> 0 </receiptsRoot> // I_He
<logsBloom> .WordStack </logsBloom> // I_Hb
<difficulty> 0 </difficulty> // I_Hd
<number> 0 </number> // I_Hi
<gasLimit> 0 </gasLimit> // I_Hl
<gasUsed> 0 </gasUsed> // I_Hg
<timestamp> 0 </timestamp> // I_Hs
<extraData> .WordStack </extraData> // I_Hx
<mixHash> 0 </mixHash> // I_Hm
<blockNonce> 0 </blockNonce> // I_Hn
<ommerBlockHeaders> [ .JSONList ] </ommerBlockHeaders>
<blockhash> .List </blockhash>
</evm>
// Ethereum Network
// ================
<network>
// Accounts Record
// ---------------
<activeAccounts> .Map </activeAccounts>
<accounts>
- UIUC-K and RV-K have slight differences of opinion here.
<account multiplicity="*" type="Bag">
<account multiplicity="*" type="Map">
<acctID> 0 </acctID>
<balance> 0 </balance>
<code> .WordStack </code>
<storage> .Map </storage>
<nonce> 0 </nonce>
</account>
</accounts>
// Transactions Record
// -------------------
<txOrder> .List </txOrder>
<txPending> .List </txPending>
<messages>
- UIUC-K and RV-K have slight differences of opinion here.
<message multiplicity="*" type="Bag">
<message multiplicity="*" type="Map">
<msgID> 0 </msgID>
<txNonce> 0 </txNonce> // T_n
<txGasPrice> 0 </txGasPrice> // T_p
<txGasLimit> 0 </txGasLimit> // T_g
<to> .Account </to> // T_t
<value> 0 </value> // T_v
<v> 0 </v> // T_w
<r> .WordStack </r> // T_r
<s> .WordStack </s> // T_s
<data> .WordStack </data> // T_i/T_e
</message>
</messages>
</network>
</ethereum>
syntax EthereumSimulation
// -------------------------
Modal Semantics¶
Our semantics is modal, with the initial mode being set on the command
line via -cMODE=EXECMODE.
NORMALexecutes as a client on the network would.VMTESTSskipsCALL*andCREATEoperations.
syntax Mode ::= "NORMAL" | "VMTESTS"
#setMode_sets the mode to the supplied one.
syntax Mode ::= "#setMode" Mode
// -------------------------------
rule <k> #setMode EXECMODE => . ... </k> <mode> _ => EXECMODE </mode>
rule <k> EX:Exception ~> (#setMode _ => .) ... </k>
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.#dropCallStackremoves the top element of thecallStack.
syntax State ::= "{" Int "|" Int "|" Map "|" WordStack "|" Int "|" WordStack "|" Int "|" WordStack "|" Map "|" Int "|" Int "|" Int "}"
// --------------------------------------------------------------------------------------------------------------------------------------
syntax InternalOp ::= "#pushCallStack"
// --------------------------------------
rule <k> #pushCallStack => . ... </k>
<callStack> (.List => ListItem({ ACCT | GAVAIL | PGM | BYTES | CR | CD | CV | WS | LM | MUSED | PCOUNT | DEPTH })) ... </callStack>
<id> ACCT </id>
<gas> GAVAIL </gas>
<program> PGM </program>
<programBytes> BYTES </programBytes>
<caller> CR </caller>
<callData> CD </callData>
<callValue> CV </callValue>
<wordStack> WS </wordStack>
<localMem> LM </localMem>
<memoryUsed> MUSED </memoryUsed>
<pc> PCOUNT </pc>
<callDepth> DEPTH </callDepth>
syntax InternalOp ::= "#popCallStack"
// -------------------------------------
rule <k> #popCallStack => . ... </k>
<callStack> (ListItem({ ACCT | GAVAIL | PGM | BYTES | CR | CD | CV | WS | LM | MUSED | PCOUNT | DEPTH }) => .List) ... </callStack>
<id> _ => ACCT </id>
<gas> _ => GAVAIL </gas>
<program> _ => PGM </program>
<programBytes> _ => BYTES </programBytes>
<caller> _ => CR </caller>
<callData> _ => CD </callData>
<callValue> _ => CV </callValue>
<wordStack> _ => WS </wordStack>
<localMem> _ => LM </localMem>
<memoryUsed> _ => MUSED </memoryUsed>
<pc> _ => PCOUNT </pc>
<callDepth> _ => DEPTH </callDepth>
syntax InternalOp ::= "#dropCallStack"
// --------------------------------------
rule <k> #dropCallStack => . ... </k> <callStack> (ListItem(_) => .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.
We use slightly different rules for rv-k versus uiuc-k because uiuc-k does not support storing configuration fragments. The semantics of these two sets of rules are identical, however, the version rv-k uses is substantially faster. We would use that version in both places if not for technical limitations on the prover. In the long term, a new prover will be built capable of supporting the same code in both versions of the semantics.
syntax Account ::= "{" Int "|" Int "|" WordStack "|" Map "|" Int "|" Bool "}"
// -----------------------------------------------------------------------------
syntax InternalOp ::= "#pushWorldState" | "#pushWorldStateAux" Map | "#pushAccount" Int Bool
// --------------------------------------------------------------------------------------------
rule <k> #pushWorldState => #pushWorldStateAux ACCTS ... </k>
<activeAccounts> ACCTS </activeAccounts>
<interimStates> (.List => ListItem(.Set)) ... </interimStates>
rule <k> #pushWorldStateAux .Map => . ... </k>
rule <k> #pushWorldStateAux ((ACCT |-> EMPTY) REST) => #pushAccount ACCT EMPTY ~> #pushWorldStateAux REST ... </k>
rule <k> #pushAccount ACCT EMPTY => . ... </k>
<interimStates> ListItem((.Set => SetItem({ ACCT | BAL | CODE | STORAGE | NONCE | EMPTY })) REST) ... </interimStates>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
<code> CODE </code>
<storage> STORAGE </storage>
<nonce> NONCE </nonce>
</account>
syntax InternalOp ::= "#popWorldState" | "#popWorldStateAux" Set
// ----------------------------------------------------------------
rule <k> #popWorldState => #popWorldStateAux PREVSTATE ... </k>
<interimStates> (ListItem(PREVSTATE) => .List) ... </interimStates>
<activeAccounts> _ => .Map </activeAccounts>
<accounts> _ => .Bag </accounts>
rule <k> #popWorldStateAux .Set => . ... </k>
rule <k> #popWorldStateAux ( (SetItem({ ACCT | BAL | CODE | STORAGE | NONCE | EMPTY }) => .Set) REST ) ... </k>
<activeAccounts> ... (.Map => ACCT |-> EMPTY) </activeAccounts>
<accounts> ( .Bag
=> <account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
<code> CODE </code>
<storage> STORAGE </storage>
<nonce> NONCE </nonce>
</account>
)
...
</accounts>
syntax InternalOp ::= "#dropWorldState"
// ---------------------------------------
rule <k> #dropWorldState => . ... </k> <interimStates> (ListItem(_) => .List) ... </interimStates>
syntax Accounts ::= "{" AccountsCell "|" Map "}"
// ------------------------------------------------
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).#?_:_?#allows for branching control-flow; if it reaches the front of theopcell it takes the first branch, if an exception runs into it it takes the second branch.
syntax KItem ::= Exception
syntax Exception ::= "#exception" | "#end"
// ------------------------------------------
rule <k> EX:Exception ~> (_:Int => .) ... </k>
rule <k> EX:Exception ~> (_:OpCode => .) ... </k>
syntax KItem ::= "#?" K ":" K "?#"
// ----------------------------------
rule <k> #? K : _ ?# => K ... </k>
rule <k> #exception ~> #? _ : K ?# => K ... </k>
rule <k> #end ~> (#? K : _ ?#) => K ~> #end ... </k>
OpCode Execution Cycle¶
OpCode is broken into several subsorts for easier handling. Here all
OpCodes are subsorted into KItem (allowing sequentialization),
and the various sorts of opcodes are subsorted into OpCode.
syntax KItem ::= OpCode
syntax OpCode ::= NullStackOp | UnStackOp | BinStackOp | TernStackOp | QuadStackOp
| InvalidOp | StackOp | InternalOp | CallOp | CallSixOp | PushOp
// --------------------------------------------------------------------------------
#executecalls#nextrepeatedly until it recieves an#endor#exception.#execToexecutes until the next opcode is one of the specified ones.
syntax KItem ::= "#execute"
// ---------------------------
rule <k> (. => #next) ~> #execute ... </k>
rule <k> EX:Exception ~> (#execute => .) ... </k>
syntax InternalOp ::= "#execTo" Set
// -----------------------------------
rule <k> (. => #next) ~> #execTo OPS ... </k>
<pc> PCOUNT </pc>
<program> ... PCOUNT |-> OP ... </program>
requires notBool (OP in OPS)
rule <k> #execTo OPS => . ... </k>
<pc> PCOUNT </pc>
<program> ... PCOUNT |-> OP ... </program>
requires OP in OPS
rule <k> #execTo OPS => #end ... </k>
<pc> PCOUNT </pc>
<program> PGM </program>
requires notBool PCOUNT in keys(PGM)
Execution follows a simple cycle where first the state is checked for exceptions, then if no exceptions will be thrown the opcode is run.
- Regardless of the mode,
#nextwill throw#endor#exceptionif the current program counter is not pointing at an OpCode.
TODO: I think on #next we are supposed to pretend it’s STOP if
it’s in the middle of the program somewhere but is invalid? I suppose
the semantics currently loads INVALID where N is the position in
the bytecode array.
syntax InternalOp ::= "#next"
// -----------------------------
rule <k> #next => #end ... </k>
<pc> PCOUNT </pc>
<program> PGM </program>
requires notBool (PCOUNT in_keys(PGM))
- In
NORMALorVMTESTSmode,#nextchecks if the opcode is exceptional, runs it if not, then increments the program counter.
rule <mode> EXECMODE </mode>
<k> #next
=> #pushCallStack
~> #exceptional? [ OP ] ~> #exec [ OP ] ~> #pc [ OP ]
~> #? #dropCallStack : #popCallStack ~> #exception ?#
...
</k>
<pc> PCOUNT </pc>
<program> ... PCOUNT |-> OP ... </program>
requires EXECMODE in (SetItem(NORMAL) SetItem(VMTESTS))
Exceptional OpCodes¶
Some checks if an opcode will throw an exception are relatively quick and done up front.
#exceptional?checks if the operator is invalid and will not causewordStacksize issues (this implements the functionZin the yellowpaper, section 9.4.2).
syntax InternalOp ::= "#exceptional?" "[" OpCode "]"
// ----------------------------------------------------
rule <k> #exceptional? [ OP ] => #invalid? [ OP ] ~> #stackNeeded? [ OP ] ~> #badJumpDest? [ OP ] ... </k>
#invalid?checks if it’s the designated invalid opcode.
syntax InternalOp ::= "#invalid?" "[" OpCode "]"
// ------------------------------------------------
rule <k> #invalid? [ INVALID ] => #exception ... </k>
rule <k> #invalid? [ OP ] => . ... </k> requires notBool isInvalidOp(OP)
#stackNeeded?checks that the stack will be not be under/overflown.#stackNeeded,#stackAdded, and#stackDeltaare helpers for deciding#stackNeeded?.
syntax InternalOp ::= "#stackNeeded?" "[" OpCode "]"
// ----------------------------------------------------
rule <k> #stackNeeded? [ OP ] => #exception ... </k>
<wordStack> WS </wordStack>
requires #sizeWordStack(WS) <Int #stackNeeded(OP)
orBool #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024
rule <k> #stackNeeded? [ OP ] => .K ... </k>
<wordStack> WS </wordStack>
requires notBool (#sizeWordStack(WS) <Int #stackNeeded(OP)
orBool #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024)
syntax Int ::= #stackNeeded ( OpCode ) [function]
// -------------------------------------------------
rule #stackNeeded(PUSH(_, _)) => 0
rule #stackNeeded(NOP:NullStackOp) => 0
rule #stackNeeded(UOP:UnStackOp) => 1
rule #stackNeeded(BOP:BinStackOp) => 2 requires notBool isLogOp(BOP)
rule #stackNeeded(TOP:TernStackOp) => 3
rule #stackNeeded(QOP:QuadStackOp) => 4
rule #stackNeeded(DUP(N)) => N
rule #stackNeeded(SWAP(N)) => N +Int 1
rule #stackNeeded(LOG(N)) => N +Int 2
rule #stackNeeded(DELEGATECALL) => 6
rule #stackNeeded(COP:CallOp) => 7 requires COP =/=K DELEGATECALL
syntax Int ::= #stackAdded ( OpCode ) [function]
// ------------------------------------------------
rule #stackAdded(CALLDATACOPY) => 0
rule #stackAdded(CODECOPY) => 0
rule #stackAdded(EXTCODECOPY) => 0
rule #stackAdded(POP) => 0
rule #stackAdded(MSTORE) => 0
rule #stackAdded(MSTORE8) => 0
rule #stackAdded(SSTORE) => 0
rule #stackAdded(JUMP) => 0
rule #stackAdded(JUMPI) => 0
rule #stackAdded(JUMPDEST) => 0
rule #stackAdded(STOP) => 0
rule #stackAdded(RETURN) => 0
rule #stackAdded(SELFDESTRUCT) => 0
rule #stackAdded(PUSH(_,_)) => 1
rule #stackAdded(LOG(_)) => 0
rule #stackAdded(SWAP(N)) => N
rule #stackAdded(DUP(N)) => N +Int 1
rule #stackAdded(OP) => 1 [owise]
syntax Int ::= #stackDelta ( OpCode ) [function]
// ------------------------------------------------
rule #stackDelta(OP) => #stackAdded(OP) -Int #stackNeeded(OP)
#badJumpDest?determines if the opcode will result in a bad jump destination.
syntax InternalOp ::= "#badJumpDest?" "[" OpCode "]"
// ----------------------------------------------------
rule <k> #badJumpDest? [ OP ] => . ... </k> requires notBool isJumpOp(OP)
rule <k> #badJumpDest? [ OP ] => . ... </k> <wordStack> DEST : WS </wordStack> <program> ... DEST |-> JUMPDEST ... </program> requires isJumpOp(OP)
rule <k> #badJumpDest? [ JUMPI ] => . ... </k> <wordStack> _ : 0 : WS </wordStack>
rule <k> #badJumpDest? [ JUMP ] => #exception ... </k> <wordStack> DEST : WS </wordStack> <program> ... DEST |-> OP ... </program> requires OP =/=K JUMPDEST
rule <k> #badJumpDest? [ JUMPI ] => #exception ... </k> <wordStack> DEST : W : WS </wordStack> <program> ... DEST |-> OP ... </program> requires OP =/=K JUMPDEST andBool W =/=K 0
rule <k> #badJumpDest? [ JUMP ] => #exception ... </k> <wordStack> DEST : WS </wordStack> <program> PGM </program> requires notBool (DEST in_keys(PGM))
rule <k> #badJumpDest? [ JUMPI ] => #exception ... </k> <wordStack> DEST : W : WS </wordStack> <program> PGM </program> requires (notBool (DEST in_keys(PGM))) andBool W =/=K 0
Execution Step¶
#execwill load the arguments of the opcode (it assumes#stackNeeded?is accurate and has been called) and trigger the subsequent operations.
syntax InternalOp ::= "#exec" "[" OpCode "]"
// --------------------------------------------
rule <k> #exec [ OP ] => #gas [ OP ] ~> OP ... </k> requires isInternalOp(OP) orBool isNullStackOp(OP) orBool isPushOp(OP)
Here we load the correct number of arguments from the wordStack
based on the sort of the opcode. Some of them require an argument to be
interpereted as an address (modulo 160 bits), so the #addr? function
performs that check.
syntax InternalOp ::= UnStackOp Int
| BinStackOp Int Int
| TernStackOp Int Int Int
| QuadStackOp Int Int Int Int
// -------------------------------------------------
rule <k> #exec [ UOP:UnStackOp => UOP #addr?(UOP, W0) ] ... </k> <wordStack> W0 : WS => WS </wordStack>
rule <k> #exec [ BOP:BinStackOp => BOP #addr?(BOP, W0) W1 ] ... </k> <wordStack> W0 : W1 : WS => WS </wordStack>
rule <k> #exec [ TOP:TernStackOp => TOP #addr?(TOP, W0) W1 W2 ] ... </k> <wordStack> W0 : W1 : W2 : WS => WS </wordStack>
rule <k> #exec [ QOP:QuadStackOp => QOP #addr?(QOP, W0) W1 W2 W3 ] ... </k> <wordStack> W0 : W1 : W2 : W3 : WS => WS </wordStack>
syntax Int ::= "#addr?" "(" OpCode "," Int ")" [function]
// ---------------------------------------------------------
rule #addr?(BALANCE, W) => #addr(W)
rule #addr?(EXTCODESIZE, W) => #addr(W)
rule #addr?(EXTCODECOPY, W) => #addr(W)
rule #addr?(SELFDESTRUCT, W) => #addr(W)
rule #addr?(OP, W) => W requires (OP =/=K BALANCE) andBool (OP =/=K EXTCODESIZE) andBool (OP =/=K EXTCODECOPY) andBool (OP =/=K SELFDESTRUCT)
StackOp is used for opcodes which require a large portion of the
stack.
syntax InternalOp ::= StackOp WordStack
// ---------------------------------------
rule <k> #exec [ SO:StackOp => SO WS ] ... </k> <wordStack> WS </wordStack>
The CallOp opcodes all interperet their second argument as an
address.
syntax InternalOp ::= CallSixOp Int Int Int Int Int Int
| CallOp Int Int Int Int Int Int Int
// -----------------------------------------------------------
rule <k> #exec [ CSO:CallSixOp => CSO W0 #addr(W1) W2 W3 W4 W5 ] ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : WS => WS </wordStack>
rule <k> #exec [ CO:CallOp => CO W0 #addr(W1) W2 W3 W4 W5 W6 ] ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS </wordStack>
#gascalculates how much gas this operation costs, and takes into account the memory consumed.
syntax InternalOp ::= "#gas" "[" OpCode "]" | "#deductGas" | "#deductMemory"
// ----------------------------------------------------------------------------
rule <k> #gas [ OP ] => #memory(OP, MU) ~> #deductMemory ~> #gasExec(SCHED, OP) ~> #deductGas ... </k> <memoryUsed> MU </memoryUsed> <schedule> SCHED </schedule>
rule <k> MU':Int ~> #deductMemory => #exception ... </k> requires MU' >=Int pow256
rule <k> MU':Int ~> #deductMemory => (Cmem(SCHED, MU') -Int Cmem(SCHED, MU)) ~> #deductGas ... </k>
<memoryUsed> MU => MU' </memoryUsed> <schedule> SCHED </schedule>
requires MU' <Int pow256
rule <k> G:Int ~> #deductGas => #exception ... </k> <gas> GAVAIL </gas> requires GAVAIL <Int G
rule <k> G:Int ~> #deductGas => . ... </k> <gas> GAVAIL => GAVAIL -Int G </gas> <previousGas> _ => GAVAIL </previousGas> requires GAVAIL >=Int G
syntax Int ::= Cmem ( Schedule , Int ) [function, memo]
// -------------------------------------------------------
rule Cmem(SCHED, N) => (N *Int Gmemory < SCHED >) +Int ((N *Int N) /Int Gquadcoeff < SCHED >)
Program Counter¶
All operators except for PUSH and JUMP* increment the program
counter by 1. The arguments to PUSH must be skipped over (as they
are inline), and the opcode JUMP already affects the program counter
in the correct way.
#pccalculates the next program counter of the given operator.
syntax InternalOp ::= "#pc" "[" OpCode "]"
// ------------------------------------------
rule <k> #pc [ OP ] => . ... </k> <pc> PCOUNT => PCOUNT +Int 1 </pc> requires notBool (isPushOp(OP) orBool isJumpOp(OP))
rule <k> #pc [ PUSH(N, _) ] => . ... </k> <pc> PCOUNT => PCOUNT +Int (1 +Int N) </pc>
rule <k> #pc [ OP ] => . ... </k> requires isJumpOp(OP)
syntax Bool ::= isJumpOp ( OpCode ) [function]
// ----------------------------------------------
rule isJumpOp(OP) => OP ==K JUMP orBool OP ==K JUMPI
Substate Log¶
During execution of a transaction some things are recorded in the
substate log (Section 6.1 in yellowpaper). This is a right cons-list of
SubstateLogEntry (which contains the account ID along with the
specified portions of the wordStack and localMem).
syntax SubstateLogEntry ::= "{" Int "|" WordStack "|" WordStack "}"
// -------------------------------------------------------------------
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 )
// ------------------------------------------
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 +Word BAL </balance>
...
</account>
<activeAccounts> ... ACCT |-> (EMPTY => #if BAL >Int 0 #then false #else EMPTY #fi) ... </activeAccounts>
rule <k> (.K => #newAccount MINER) ~> #finalizeTx(_)... </k>
<mode> NORMAL </mode>
<coinbase> MINER </coinbase>
<activeAccounts> ACCTS </activeAccounts>
requires notBool MINER in_keys(ACCTS)
rule <k> #finalizeTx(false) ... </k>
<mode> NORMAL </mode>
<gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND) </gas>
<refund> REFUND => 0 </refund>
<txPending> ListItem(MSGID:Int) ... </txPending>
<message>
<msgID> MSGID </msgID>
<txGasLimit> GLIMIT </txGasLimit>
...
</message>
requires REFUND =/=Int 0
rule <k> #finalizeTx(false => true) ... </k>
<mode> NORMAL </mode>
<origin> ORG </origin>
<coinbase> MINER </coinbase>
<gas> GAVAIL </gas>
<refund> 0 </refund>
<account>
<acctID> ORG </acctID>
<balance> ORGBAL => ORGBAL +Int GAVAIL *Int GPRICE </balance>
...
</account>
<account>
<acctID> MINER </acctID>
<balance> MINBAL => MINBAL +Int (GLIMIT -Int GAVAIL) *Int GPRICE </balance>
...
</account>
<txPending> ListItem(TXID:Int) => .List ... </txPending>
<message>
<msgID> TXID </msgID>
<txGasLimit> GLIMIT </txGasLimit>
<txGasPrice> GPRICE </txGasPrice>
...
</message>
<activeAccounts> ... ORG |-> (ORGEMPTY => #if GAVAIL *Int GPRICE >Int 0 #then false #else ORGEMPTY #fi) MINER |-> (MINEMPTY => #if (GLIMIT -Int GAVAIL) *Int GPRICE >Int 0 #then false #else MINEMPTY #fi) ... </activeAccounts>
requires ORG =/=Int MINER
rule <k> #finalizeTx(false => true) ... </k>
<mode> NORMAL </mode>
<origin> ACCT </origin>
<coinbase> ACCT </coinbase>
<refund> 0 </refund>
<account>
<acctID> ACCT </acctID>
<balance> BAL => BAL +Int GLIMIT *Int GPRICE </balance>
...
</account>
<txPending> ListItem(MsgId:Int) => .List ... </txPending>
<message>
<msgID> MsgId </msgID>
<txGasLimit> GLIMIT </txGasLimit>
<txGasPrice> GPRICE </txGasPrice>
...
</message>
<activeAccounts> ... ACCT |-> (EMPTY => #if GLIMIT *Int GPRICE >Int 0 #then false #else EMPTY #fi) ... </activeAccounts>
rule <k> #finalizeTx(true) ... </k>
<selfDestruct> ... (SetItem(ACCT) => .Set) </selfDestruct>
<activeAccounts> ... (ACCT |-> _ => .Map) </activeAccounts>
<accounts>
( <account>
<acctID> ACCT </acctID>
...
</account>
=> .Bag
)
...
</accounts>
EVM Programs¶
Lists of opcodes form programs. Deciding if an opcode is in a list will be useful for modeling gas, and converting a program into a map of program-counter to opcode is useful for execution.
Note that _in_ ignores the arguments to operators that are
parametric.
syntax OpCodes ::= ".OpCodes" | OpCode ";" OpCodes
// --------------------------------------------------
syntax Map ::= #asMapOpCodes ( OpCodes ) [function]
| #asMapOpCodes ( Int , OpCodes , Map ) [function, klabel(#asMapOpCodesAux)]
// -----------------------------------------------------------------------------------------
rule #asMapOpCodes( OPS::OpCodes ) => #asMapOpCodes(0, OPS, .Map)
rule #asMapOpCodes( N , .OpCodes , MAP ) => MAP
rule #asMapOpCodes( N , OP:OpCode ; OCS , MAP ) => #asMapOpCodes(N +Int 1, OCS, MAP (N |-> OP)) requires notBool isPushOp(OP)
rule #asMapOpCodes( N , PUSH(M, W) ; OCS , MAP ) => #asMapOpCodes(N +Int 1 +Int M, OCS, MAP (N |-> PUSH(M, W)))
syntax OpCodes ::= #asOpCodes ( Map ) [function]
| #asOpCodes ( Int , Map , OpCodes ) [function, klabel(#asOpCodesAux)]
// ---------------------------------------------------------------------------------------
rule #asOpCodes(M) => #asOpCodes(0, M, .OpCodes)
rule #asOpCodes(N, .Map, OPS) => OPS
rule #asOpCodes(N, N |-> OP M, OPS) => #asOpCodes(N +Int 1, M, OP ; OPS) requires notBool isPushOp(OP)
rule #asOpCodes(N, N |-> PUSH(S, W) M, OPS) => #asOpCodes(N +Int 1 +Int S, M, PUSH(S, W) ; OPS)
EVM OpCodes¶
Each subsection has a different class of opcodes. Organization is based roughly on what parts of the execution state are needed to compute the result of each operator. This sometimes corresponds to the organization in the yellowpaper.
Internal Operations¶
These are just used by the other operators for shuffling local execution state around on the EVM.
#pushwill push an element to thewordStackwithout any checks.#setStack_will set the current stack to the given one.
syntax InternalOp ::= "#push" | "#setStack" WordStack
// -----------------------------------------------------
rule <k> W0:Int ~> #push => . ... </k> <wordStack> WS => W0 : WS </wordStack>
rule <k> #setStack WS => . ... </k> <wordStack> _ => WS </wordStack>
#newAccount_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 ::= "#newAccount" Int
// ---------------------------------------
rule <k> #newAccount ACCT => #exception ... </k>
<account>
<acctID> ACCT </acctID>
<code> CODE </code>
<nonce> NONCE </nonce>
...
</account>
requires CODE =/=K .WordStack orBool NONCE =/=K 0
rule <k> #newAccount ACCT => . ... </k>
<account>
<acctID> ACCT </acctID>
<code> .WordStack </code>
<nonce> 0 </nonce>
<storage> _ => .Map </storage>
...
</account>
rule <k> #newAccount ACCT => . ... </k>
<activeAccounts> ACCTS (.Map => ACCT |-> true) </activeAccounts>
<accounts>
( .Bag
=> <account>
<acctID> ACCT </acctID>
<balance> 0 </balance>
<code> .WordStack </code>
<storage> .Map </storage>
<nonce> 0 </nonce>
</account>
)
...
</accounts>
requires notBool ACCT in_keys(ACCTS)
#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 -Word VALUE </balance>
<nonce> NONCE </nonce>
<code> CODE </code>
...
</account>
<account>
<acctID> ACCTTO </acctID>
<balance> ORIGTO => ORIGTO +Word VALUE </balance>
...
</account>
<activeAccounts> ... ACCTTO |-> (EMPTY => #if VALUE >Int 0 #then false #else EMPTY #fi) ACCTFROM |-> (_ => ORIGFROM ==Int VALUE andBool NONCE ==Int 0 andBool CODE ==K .WordStack) ... </activeAccounts>
requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
rule <k> #transferFunds ACCTFROM ACCTTO VALUE => #exception ... </k>
<account>
<acctID> ACCTFROM </acctID>
<balance> ORIGFROM </balance>
...
</account>
requires VALUE >Int ORIGFROM
rule <k> (. => #newAccount ACCTTO) ~> #transferFunds ACCTFROM ACCTTO VALUE ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires ACCTFROM =/=K ACCTTO andBool notBool ACCTTO in_keys(ACCTS)
rule <k> #transferFunds ACCT ACCT VALUE => . ... </k>
<account>
<acctID> ACCT </acctID>
<balance> ORIGFROM </balance>
...
</account>
requires VALUE <=Int ORIGFROM
Invalid Operator¶
We use INVALID both for marking the designated invalid operator and
for garbage bytes in the input program.
syntax InvalidOp ::= "INVALID"
// ------------------------------
Stack Manipulations¶
Some operators don’t calculate anything, they just push the stack around a bit.
syntax UnStackOp ::= "POP"
// --------------------------
rule <k> POP W => . ... </k>
syntax StackOp ::= DUP ( Int ) | SWAP ( Int )
// ---------------------------------------------
rule <k> DUP(N) WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS) ... </k>
rule <k> SWAP(N) (W0 : WS) => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... </k>
syntax PushOp ::= PUSH ( Int , Int )
// ------------------------------------
rule <k> PUSH(_, W) => W ~> #push ... </k>
Local Memory¶
These operations are getters/setters of the local execution memory.
syntax UnStackOp ::= "MLOAD"
// ----------------------------
rule <k> MLOAD INDEX => #asWord(#range(LM, INDEX, 32)) ~> #push ... </k>
<localMem> LM </localMem>
syntax BinStackOp ::= "MSTORE" | "MSTORE8"
// ------------------------------------------
rule <k> MSTORE INDEX VALUE => . ... </k>
<localMem> LM => LM [ INDEX := #padToWidth(32, #asByteStack(VALUE)) ] </localMem>
rule <k> MSTORE8 INDEX VALUE => . ... </k>
<localMem> LM => LM [ INDEX <- (VALUE %Int 256) ] </localMem>
Expressions¶
Expression calculations are simple and don’t require anything but the
arguments from the wordStack to operate.
NOTE: We have to call the opcode OR by EVMOR instead, because K
has trouble parsing it/compiling the definition otherwise.
syntax UnStackOp ::= "ISZERO" | "NOT"
// -------------------------------------
rule <k> ISZERO 0 => 1 ~> #push ... </k>
rule <k> ISZERO W => 0 ~> #push ... </k> requires W =/=K 0
rule <k> NOT W => ~Word W ~> #push ... </k>
syntax BinStackOp ::= "ADD" | "MUL" | "SUB" | "DIV" | "EXP" | "MOD"
// -------------------------------------------------------------------
rule <k> ADD W0 W1 => W0 +Word W1 ~> #push ... </k>
rule <k> MUL W0 W1 => W0 *Word W1 ~> #push ... </k>
rule <k> SUB W0 W1 => W0 -Word W1 ~> #push ... </k>
rule <k> DIV W0 W1 => W0 /Word W1 ~> #push ... </k>
rule <k> EXP W0 W1 => W0 ^Word W1 ~> #push ... </k>
rule <k> MOD W0 W1 => W0 %Word W1 ~> #push ... </k>
syntax BinStackOp ::= "SDIV" | "SMOD"
// -------------------------------------
rule <k> SDIV W0 W1 => W0 /sWord W1 ~> #push ... </k>
rule <k> SMOD W0 W1 => W0 %sWord W1 ~> #push ... </k>
syntax TernStackOp ::= "ADDMOD" | "MULMOD"
// ------------------------------------------
rule <k> ADDMOD W0 W1 W2 => (W0 +Int W1) %Word W2 ~> #push ... </k>
rule <k> MULMOD W0 W1 W2 => (W0 *Int W1) %Word W2 ~> #push ... </k>
syntax BinStackOp ::= "BYTE" | "SIGNEXTEND"
// -------------------------------------------
rule <k> BYTE INDEX W => byte(INDEX, W) ~> #push ... </k>
rule <k> SIGNEXTEND W0 W1 => signextend(W0, W1) ~> #push ... </k>
syntax BinStackOp ::= "AND" | "EVMOR" | "XOR"
// ---------------------------------------------
rule <k> AND W0 W1 => W0 &Word W1 ~> #push ... </k>
rule <k> EVMOR W0 W1 => W0 |Word W1 ~> #push ... </k>
rule <k> XOR W0 W1 => W0 xorWord W1 ~> #push ... </k>
syntax BinStackOp ::= "LT" | "GT" | "EQ"
// ----------------------------------------
rule <k> LT W0 W1 => 1 ~> #push ... </k> requires W0 <Int W1
rule <k> LT W0 W1 => 0 ~> #push ... </k> requires W0 >=Int W1
rule <k> GT W0 W1 => 1 ~> #push ... </k> requires W0 >Int W1
rule <k> GT W0 W1 => 0 ~> #push ... </k> requires W0 <=Int W1
rule <k> EQ W0 W1 => 1 ~> #push ... </k> requires W0 ==Int W1
rule <k> EQ W0 W1 => 0 ~> #push ... </k> requires W0 =/=Int W1
syntax BinStackOp ::= "SLT" | "SGT"
// -----------------------------------
rule <k> SLT W0 W1 => W0 s<Word W1 ~> #push ... </k>
rule <k> SGT W0 W1 => W1 s<Word W0 ~> #push ... </k>
syntax BinStackOp ::= "SHA3"
// ----------------------------
rule <k> SHA3 MEMSTART MEMWIDTH => keccak(#range(LM, MEMSTART, MEMWIDTH)) ~> #push ... </k>
<localMem> LM </localMem>
Local State¶
These operators make queries about the current execution state.
syntax NullStackOp ::= "PC" | "GAS" | "GASPRICE" | "GASLIMIT"
// -------------------------------------------------------------
rule <k> PC => PCOUNT ~> #push ... </k> <pc> PCOUNT </pc>
rule <k> GAS => GAVAIL ~> #push ... </k> <gas> GAVAIL </gas>
rule <k> GASPRICE => GPRICE ~> #push ... </k> <gasPrice> GPRICE </gasPrice>
rule <k> GASLIMIT => GLIMIT ~> #push ... </k> <gasLimit> GLIMIT </gasLimit>
syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY"
// -------------------------------------------------------------------------
rule <k> COINBASE => CB ~> #push ... </k> <coinbase> CB </coinbase>
rule <k> TIMESTAMP => TS ~> #push ... </k> <timestamp> TS </timestamp>
rule <k> NUMBER => NUMB ~> #push ... </k> <number> NUMB </number>
rule <k> DIFFICULTY => DIFF ~> #push ... </k> <difficulty> DIFF </difficulty>
syntax NullStackOp ::= "ADDRESS" | "ORIGIN" | "CALLER" | "CALLVALUE"
// --------------------------------------------------------------------
rule <k> ADDRESS => ACCT ~> #push ... </k> <id> ACCT </id>
rule <k> ORIGIN => ORG ~> #push ... </k> <origin> ORG </origin>
rule <k> CALLER => CL ~> #push ... </k> <caller> CL </caller>
rule <k> CALLVALUE => CV ~> #push ... </k> <callValue> CV </callValue>
syntax NullStackOp ::= "MSIZE" | "CODESIZE"
// -------------------------------------------
rule <k> MSIZE => 32 *Word MU ~> #push ... </k> <memoryUsed> MU </memoryUsed>
rule <k> CODESIZE => #sizeWordStack(PGM) ~> #push ... </k> <programBytes> PGM </programBytes>
syntax TernStackOp ::= "CODECOPY"
// ---------------------------------
rule <k> CODECOPY MEMSTART PGMSTART WIDTH => . ... </k>
<programBytes> PGM </programBytes>
<localMem> LM => LM [ MEMSTART := PGM [ PGMSTART .. WIDTH ] ] </localMem>
syntax UnStackOp ::= "BLOCKHASH"
// --------------------------------
rule <k> BLOCKHASH N => #if N >=Int HI orBool HI -Int 256 >Int N #then 0 #else #parseHexWord(Keccak256(Int2String(N))) #fi ~> #push ... </k> <number> HI </number> <mode> VMTESTS </mode>
rule <k> BLOCKHASH N => #blockhash(HASHES, N, HI -Int 1, 0) ~> #push ... </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
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]
JUMP*¶
The JUMP* family of operations affect the current program counter.
syntax NullStackOp ::= "JUMPDEST"
// ---------------------------------
rule <k> JUMPDEST => . ... </k>
syntax UnStackOp ::= "JUMP"
// ---------------------------
rule <k> JUMP DEST => . ... </k> <pc> _ => DEST </pc>
syntax BinStackOp ::= "JUMPI"
// -----------------------------
rule <k> JUMPI DEST I => . ... </k> <pc> _ => DEST </pc> requires I =/=K 0
rule <k> JUMPI DEST 0 => . ... </k> <pc> PCOUNT => PCOUNT +Int 1 </pc>
STOP and RETURN¶
syntax NullStackOp ::= "STOP"
// -----------------------------
rule <k> STOP => #end ... </k>
syntax BinStackOp ::= "RETURN"
// ------------------------------
rule <mode> EXECMODE </mode>
<k> RETURN RETSTART RETWIDTH => #end ... </k>
<output> _ => #range(LM, RETSTART, RETWIDTH) </output>
<localMem> LM </localMem>
Call Data¶
These operators query about the current CALL* state.
syntax NullStackOp ::= "CALLDATASIZE"
// -------------------------------------
rule <k> CALLDATASIZE => #sizeWordStack(CD) ~> #push ... </k>
<callData> CD </callData>
syntax UnStackOp ::= "CALLDATALOAD"
// -----------------------------------
rule <k> CALLDATALOAD DATASTART => #asWord(CD [ DATASTART .. 32 ]) ~> #push ... </k>
<callData> CD </callData>
syntax TernStackOp ::= "CALLDATACOPY"
// -------------------------------------
rule <k> CALLDATACOPY MEMSTART DATASTART DATAWIDTH => . ... </k>
<localMem> LM => LM [ MEMSTART := CD [ DATASTART .. DATAWIDTH ] ] </localMem>
<callData> CD </callData>
Log Operations¶
syntax BinStackOp ::= LogOp
syntax LogOp ::= LOG ( Int )
// ----------------------------
rule <k> LOG(N) MEMSTART MEMWIDTH => . ... </k>
<id> ACCT </id>
<wordStack> WS => #drop(N, WS) </wordStack>
<localMem> LM </localMem>
<log> ... (.List => ListItem({ ACCT | #take(N, WS) | #range(LM, MEMSTART, MEMWIDTH) })) </log>
requires #sizeWordStack(WS) >=Int N
Ethereum Network OpCodes¶
Operators that require access to the rest of the Ethereum network world-state can be taken as a first draft of a “blockchain generic” language.
Account Queries¶
TODO: It’s unclear what to do in the case of an account not existing for
these operators. BALANCE is specified to push 0 in this case, but
the others are not specified. For now, I assume that they instantiate an
empty account and use the empty data.
syntax UnStackOp ::= "BALANCE"
// ------------------------------
rule <k> BALANCE ACCT => BAL ~> #push ... </k>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
rule <k> BALANCE ACCT => #newAccount ACCT ~> 0 ~> #push ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in_keys(ACCTS)
syntax UnStackOp ::= "EXTCODESIZE"
// ----------------------------------
rule <k> EXTCODESIZE ACCT => #sizeWordStack(CODE) ~> #push ... </k>
<account>
<acctID> ACCT </acctID>
<code> CODE </code>
...
</account>
rule <k> EXTCODESIZE ACCT => #newAccount ACCT ~> 0 ~> #push ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in_keys(ACCTS)
TODO: What should happen in the case that the account doesn’t exist with
EXTCODECOPY? Should we pad zeros (for the copied “program”)?
syntax QuadStackOp ::= "EXTCODECOPY"
// ------------------------------------
rule <k> EXTCODECOPY ACCT MEMSTART PGMSTART WIDTH => . ... </k>
<localMem> LM => LM [ MEMSTART := PGM [ PGMSTART .. WIDTH ] ] </localMem>
<account>
<acctID> ACCT </acctID>
<code> PGM </code>
...
</account>
rule <k> EXTCODECOPY ACCT MEMSTART PGMSTART WIDTH => #newAccount ACCT ... </k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool ACCT in_keys(ACCTS)
Account Storage Operations¶
These operations interact with the account storage.
syntax UnStackOp ::= "SLOAD"
// ----------------------------
rule <k> SLOAD INDEX => 0 ~> #push ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> STORAGE </storage>
...
</account> requires notBool INDEX in_keys(STORAGE)
rule <k> SLOAD INDEX => VALUE ~> #push ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> ... INDEX |-> VALUE ... </storage>
...
</account>
syntax BinStackOp ::= "SSTORE"
// ------------------------------
rule <k> SSTORE INDEX VALUE => . ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> ... (INDEX |-> (OLD => VALUE)) ... </storage>
...
</account>
<refund> R => #ifInt OLD =/=Int 0 andBool VALUE ==Int 0
#then R +Word Rsstoreclear < SCHED >
#else R
#fi
</refund>
<schedule> SCHED </schedule>
rule <k> SSTORE INDEX VALUE => . ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> STORAGE => STORAGE [ INDEX <- VALUE ] </storage>
...
</account>
requires notBool (INDEX in_keys(STORAGE))
Call Operations¶
The various CALL* (and other inter-contract control flow) operations
will be desugared into these InternalOps.
- The
callLogis used to store theCALL*/CREATEoperations so that we can compare them against the test-set.
syntax Call ::= "{" Int "|" Int "|" Int "|" WordStack "}"
// ---------------------------------------------------------
#call_____takes the calling account, the account to execute as, the account whose code should execute, the gas limit, the amount to transfer, 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, and the arguments.#return__is a placeholder for the calling program, specifying where to place the returned data in memory.
syntax InternalOp ::= "#checkCall" Int Int
| "#call" Int Int Int Int Int Int WordStack
| "#callWithCode" Int Int Map WordStack Int Int Int WordStack
| "#mkCall" Int Int Map WordStack Int Int Int WordStack
// ---------------------------------------------------------------------------
rule <k> #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception ... </k>
<callDepth> CD </callDepth>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
requires VALUE >Int BAL orBool CD >=Int 1024
rule <k> #checkCall ACCT VALUE => . ... </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 ACCTCODE GLIMIT VALUE APPVALUE ARGS
=> #callWithCode ACCTFROM ACCTTO (0 |-> #precompiled(ACCTCODE)) .WordStack GLIMIT VALUE APPVALUE ARGS
...
</k>
requires ACCTCODE >Int 0 andBool ACCTCODE <=Int 4
rule <k> #call ACCTFROM ACCTTO ACCTCODE GLIMIT VALUE APPVALUE ARGS
=> #callWithCode ACCTFROM ACCTTO #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) CODE GLIMIT VALUE APPVALUE ARGS
...
</k>
<schedule> SCHED </schedule>
<acctID> ACCTCODE </acctID>
<code> CODE </code>
requires notBool (ACCTCODE >Int 0 andBool ACCTCODE <=Int 4)
rule <k> #call ACCTFROM ACCTTO ACCTCODE GLIMIT VALUE APPVALUE ARGS
=> #callWithCode ACCTFROM ACCTTO .Map .WordStack GLIMIT VALUE APPVALUE ARGS
...
</k>
<activeAccounts> ACCTS </activeAccounts>
requires notBool (ACCTCODE >Int 0 andBool ACCTCODE <=Int 4) andBool notBool ACCTCODE in_keys(ACCTS)
rule #callWithCode ACCTFROM ACCTTO CODE BYTES GLIMIT VALUE APPVALUE ARGS
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate
~> #transferFunds ACCTFROM ACCTTO VALUE
~> #mkCall ACCTFROM ACCTTO CODE BYTES GLIMIT VALUE APPVALUE ARGS
rule <mode> EXECMODE </mode>
<k> #mkCall ACCTFROM ACCTTO CODE BYTES GLIMIT VALUE APPVALUE ARGS
=> #initVM ~> #if EXECMODE ==K VMTESTS #then #end #else #execute #fi
...
</k>
<callLog> ... (.Set => #ifSet EXECMODE ==K VMTESTS #then SetItem({ ACCTTO | GLIMIT | VALUE | ARGS }) #else .Set #fi) </callLog>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => APPVALUE </callValue>
<id> _ => ACCTTO </id>
<gas> _ => GLIMIT </gas>
<caller> _ => ACCTFROM </caller>
<program> _ => CODE </program>
<programBytes> _ => BYTES </programBytes>
syntax KItem ::= "#initVM"
// --------------------------
rule <k> #initVM => . ... </k>
<pc> _ => 0 </pc>
<memoryUsed> _ => 0 </memoryUsed>
<output> _ => .WordStack </output>
<wordStack> _ => .WordStack </wordStack>
<localMem> _ => .Map </localMem>
syntax KItem ::= "#return" Int Int
// ----------------------------------
rule <k> #exception ~> #return _ _
=> #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push
...
</k>
rule <mode> EXECMODE </mode>
<k> #end ~> #return RETSTART RETWIDTH
=> #popCallStack
~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi
~> #dropSubstate
~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
...
</k>
<output> OUT </output>
<gas> GAVAIL </gas>
syntax InternalOp ::= "#refund" Int
| "#setLocalMem" Int Int WordStack
// ------------------------------------------------------
rule <k> #refund G => . ... </k> <gas> GAVAIL => GAVAIL +Int G </gas>
rule <k> #setLocalMem START WIDTH WS => . ... </k>
<localMem> LM => LM [ START := #take(minInt(WIDTH, #sizeWordStack(WS)), WS) ] </localMem>
For each CALL* operation, we make a corresponding call to #call
and a state-change to setup the custom parts of the calling environment.
syntax CallOp ::= "CALL"
// ------------------------
rule <k> CALL GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, ACCTTO, ACCTS, GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH)
~> #return RETSTART RETWIDTH
...
</k>
<schedule> SCHED </schedule>
<id> ACCTFROM </id>
<localMem> LM </localMem>
<activeAccounts> ACCTS </activeAccounts>
<previousGas> GAVAIL </previousGas>
syntax CallOp ::= "CALLCODE"
// ----------------------------
rule <k> CALLCODE GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTFROM ACCTTO Ccallgas(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH)
~> #return RETSTART RETWIDTH
...
</k>
<schedule> SCHED </schedule>
<id> ACCTFROM </id>
<localMem> LM </localMem>
<activeAccounts> ACCTS </activeAccounts>
<previousGas> GAVAIL </previousGas>
syntax CallSixOp ::= "DELEGATECALL"
// -----------------------------------
rule <k> DELEGATECALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM 0
~> #call ACCTAPPFROM ACCTFROM ACCTTO Ccallgas(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, 0) 0 VALUE #range(LM, ARGSTART, ARGWIDTH)
~> #return RETSTART RETWIDTH
...
</k>
<schedule> SCHED </schedule>
<id> ACCTFROM </id>
<caller> ACCTAPPFROM </caller>
<callValue> VALUE </callValue>
<localMem> LM </localMem>
<activeAccounts> ACCTS </activeAccounts>
<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.
syntax InternalOp ::= "#create" Int Int Int Int WordStack
| "#mkCreate" Int Int WordStack Int Int
| "#checkCreate" Int Int
// --------------------------------------------
rule <k> #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception ... </k>
<callDepth> CD </callDepth>
<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 => #ifInt EXECMODE ==K VMTESTS #then NONCE #else NONCE +Int 1 #fi </nonce>
...
</account>
<activeAccounts> ... ACCT |-> (EMPTY => #if EXECMODE ==K VMTESTS #then EMPTY #else false #fi) ... </activeAccounts>
requires notBool (VALUE >Int BAL orBool CD >=Int 1024)
rule #create ACCTFROM ACCTTO GAVAIL VALUE INITCODE
=> #pushCallStack ~> #pushWorldState ~> #pushSubstate
~> #newAccount ACCTTO
~> #transferFunds ACCTFROM ACCTTO VALUE
~> #mkCreate ACCTFROM ACCTTO INITCODE GAVAIL VALUE
rule <mode> EXECMODE </mode>
<k> #mkCreate ACCTFROM ACCTTO INITCODE GAVAIL VALUE
=> #initVM ~> #if EXECMODE ==K VMTESTS #then #end #else #execute #fi
...
</k>
<schedule> SCHED </schedule>
<id> ACCT => ACCTTO </id>
<gas> OLDGAVAIL => GAVAIL </gas>
<program> _ => #asMapOpCodes(#dasmOpCodes(INITCODE, SCHED)) </program>
<programBytes> _ => INITCODE </programBytes>
<caller> _ => ACCTFROM </caller>
<callLog> ... (.Set => #ifSet EXECMODE ==K VMTESTS #then SetItem({ 0 | OLDGAVAIL +Int GAVAIL | VALUE | INITCODE }) #else .Set #fi) </callLog>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => .WordStack </callData>
<callValue> _ => VALUE </callValue>
<account>
<acctID> ACCTTO </acctID>
<nonce> NONCE => #ifInt Gemptyisnonexistent << SCHED >> #then NONCE +Int 1 #else NONCE #fi </nonce>
...
</account>
<activeAccounts> ... ACCTTO |-> (EMPTY => #if Gemptyisnonexistent << SCHED >> #then false #else EMPTY #fi) ... </activeAccounts>
syntax KItem ::= "#codeDeposit" Int
| "#mkCodeDeposit" Int
| "#finishCodeDeposit" Int WordStack
// ---------------------------------------------------
rule <k> #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... </k>
rule <mode> EXECMODE </mode>
<k> #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... </k>
rule <k> #mkCodeDeposit ACCT
=> #if EXECMODE ==K VMTESTS #then . #else Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas #fi
~> #finishCodeDeposit ACCT OUT
...
</k>
<mode> EXECMODE </mode>
<schedule> SCHED </schedule>
<output> OUT => .WordStack </output>
requires #sizeWordStack(OUT) <=Int maxCodeSize < SCHED >
rule <k> #mkCodeDeposit ACCT => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... </k>
<schedule> SCHED </schedule>
<output> OUT => .WordStack </output>
requires #sizeWordStack(OUT) >Int maxCodeSize < SCHED >
rule <k> #finishCodeDeposit ACCT OUT
=> #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate
~> #refund GAVAIL ~> ACCT ~> #push
...
</k>
<mode> EXECMODE </mode>
<gas> GAVAIL </gas>
<account>
<acctID> ACCT </acctID>
<code> _ => OUT </code>
...
</account>
<activeAccounts> ... ACCT |-> (EMPTY => #if OUT =/=K .WordStack #then false #else EMPTY #fi) ... </activeAccounts>
rule <k> #exception ~> #finishCodeDeposit ACCT _
=> #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate
~> #refund GAVAIL ~> ACCT ~> #push
...
</k>
<mode> EXECMODE </mode>
<gas> GAVAIL </gas>
<schedule> FRONTIER </schedule>
rule <k> #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... </k>
<schedule> SCHED </schedule>
requires SCHED =/=K FRONTIER
CREATE will attempt to #create the account using the
initialization code and cleans up the result with #codeDeposit.
syntax TernStackOp ::= "CREATE"
// -------------------------------
rule <k> CREATE VALUE MEMSTART MEMWIDTH
=> #checkCreate ACCT VALUE
~> #create ACCT #newAddr(ACCT, NONCE) #ifInt Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #range(LM, MEMSTART, MEMWIDTH)
~> #codeDeposit #newAddr(ACCT, NONCE)
...
</k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<gas> GAVAIL => #ifInt Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi </gas>
<localMem> LM </localMem>
<account>
<acctID> ACCT </acctID>
<nonce> NONCE </nonce>
...
</account>
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.
syntax UnStackOp ::= "SELFDESTRUCT"
// -----------------------------------
rule <k> SELFDESTRUCT ACCTTO => #transferFunds ACCT ACCTTO BALFROM ~> #end ... </k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<selfDestruct> SDS (.Set => SetItem(ACCT)) </selfDestruct>
<refund> RF => #ifInt ACCT in SDS #then RF #else RF +Word Rselfdestruct < SCHED > #fi </refund>
<account>
<acctID> ACCT </acctID>
<balance> BALFROM </balance>
...
</account>
requires ACCT =/=Int ACCTTO
rule <k> SELFDESTRUCT ACCT => #end ... </k>
<schedule> SCHED </schedule>
<id> ACCT </id>
<selfDestruct> SDS (.Set => SetItem(ACCT)) </selfDestruct>
<refund> RF => #ifInt ACCT in SDS #then RF #else RF +Word Rselfdestruct < SCHED > #fi </refund>
<account>
<acctID> ACCT </acctID>
<balance> BALFROM => 0 </balance>
<nonce> NONCE </nonce>
<code> CODE </code>
...
</account>
<activeAccounts> ... ACCT |-> (_ => NONCE ==Int 0 andBool CODE ==K .WordStack) ... </activeAccounts>
Precompiled Contracts¶
#precompiledis a placeholder for the 4 pre-compiled contracts at addresses 1 through 4.
syntax NullStackOp ::= PrecompiledOp
syntax PrecompiledOp ::= #precompiled ( Int ) [function]
// --------------------------------------------------------
rule #precompiled(1) => ECREC
rule #precompiled(2) => SHA256
rule #precompiled(3) => RIP160
rule #precompiled(4) => ID
ECRECperforms ECDSA public key recovery.SHA256performs the SHA2-257 hash function.RIP160performs the RIPEMD-160 hash function.IDis the identity function (copies input to output).
syntax PrecompiledOp ::= "ECREC"
// --------------------------------
rule <k> ECREC => #end ... </k>
<callData> DATA </callData>
<output> _ => #ecrec(#sender(#unparseByteStack(DATA [ 0 .. 32 ]), #asWord(DATA [ 32 .. 32 ]), #unparseByteStack(DATA [ 64 .. 32 ]), #unparseByteStack(DATA [ 96 .. 32 ]))) </output>
syntax WordStack ::= #ecrec ( Account ) [function]
// --------------------------------------------------
rule #ecrec(.Account) => .WordStack
rule #ecrec(N:Int) => #padToWidth(32, #asByteStack(N))
syntax PrecompiledOp ::= "SHA256"
// ---------------------------------
rule <k> SHA256 => #end ... </k>
<callData> DATA </callData>
<output> _ => #parseHexBytes(Sha256(#unparseByteStack(DATA))) </output>
syntax PrecompiledOp ::= "RIP160"
// ---------------------------------
rule <k> RIP160 => #end ... </k>
<callData> DATA </callData>
<output> _ => #padToWidth(32, #parseHexBytes(RipEmd160(#unparseByteStack(DATA)))) </output>
syntax PrecompiledOp ::= "ID"
// -----------------------------
rule <k> ID => #end ... </k>
<callData> DATA </callData>
<output> _ => DATA </output>
Ethereum Gas Calculation¶
The gas calculation is designed to mirror the style of the yellowpaper. Gas is consumed either by increasing the amount of memory being used, or by executing opcodes.
Memory Consumption¶
Memory consumed is tracked to determine the appropriate amount of gas to charge for each operation. In the yellowpaper, each opcode is defined to consume zero gas unless specified otherwise next to the semantics of the opcode (appendix H).
#memorycomputes the new memory size given the old size and next operator (with its arguments).#memoryUsageUpdateis the functionMin appendix H of the yellowpaper which helps track the memory used.
syntax Int ::= #memory ( OpCode , Int ) [function]
// --------------------------------------------------
rule #memory ( MLOAD INDEX , MU ) => #memoryUsageUpdate(MU, INDEX, 32)
rule #memory ( MSTORE INDEX _ , MU ) => #memoryUsageUpdate(MU, INDEX, 32)
rule #memory ( MSTORE8 INDEX _ , MU ) => #memoryUsageUpdate(MU, INDEX, 1)
rule #memory ( SHA3 START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( LOG(_) START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( CODECOPY START _ WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( EXTCODECOPY _ START _ WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( CALLDATACOPY START _ WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( CREATE _ START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( RETURN START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH)
rule #memory ( COP:CallOp _ _ _ ARGSTART ARGWIDTH RETSTART RETWIDTH , MU ) => #memoryUsageUpdate(#memoryUsageUpdate(MU, ARGSTART, ARGWIDTH), RETSTART, RETWIDTH)
rule #memory ( CSOP:CallSixOp _ _ ARGSTART ARGWIDTH RETSTART RETWIDTH , MU ) => #memoryUsageUpdate(#memoryUsageUpdate(MU, ARGSTART, ARGWIDTH), RETSTART, RETWIDTH)
Grumble grumble, K sucks at owise.
rule #memory(JUMP _, MU) => MU
rule #memory(JUMPI _ _, MU) => MU
rule #memory(JUMPDEST, MU) => MU
rule #memory(SSTORE _ _, MU) => MU
rule #memory(SLOAD _, MU) => MU
rule #memory(ADD _ _, MU) => MU
rule #memory(SUB _ _, MU) => MU
rule #memory(MUL _ _, MU) => MU
rule #memory(DIV _ _, MU) => MU
rule #memory(EXP _ _, MU) => MU
rule #memory(MOD _ _, MU) => MU
rule #memory(SDIV _ _, MU) => MU
rule #memory(SMOD _ _, MU) => MU
rule #memory(SIGNEXTEND _ _, MU) => MU
rule #memory(ADDMOD _ _ _, MU) => MU
rule #memory(MULMOD _ _ _, MU) => MU
rule #memory(NOT _, MU) => MU
rule #memory(AND _ _, MU) => MU
rule #memory(EVMOR _ _, MU) => MU
rule #memory(XOR _ _, MU) => MU
rule #memory(BYTE _ _, MU) => MU
rule #memory(ISZERO _, MU) => MU
rule #memory(LT _ _, MU) => MU
rule #memory(GT _ _, MU) => MU
rule #memory(SLT _ _, MU) => MU
rule #memory(SGT _ _, MU) => MU
rule #memory(EQ _ _, MU) => MU
rule #memory(POP _, MU) => MU
rule #memory(PUSH(_, _), MU) => MU
rule #memory(DUP(_) _, MU) => MU
rule #memory(SWAP(_) _, MU) => MU
rule #memory(STOP, MU) => MU
rule #memory(ADDRESS, MU) => MU
rule #memory(ORIGIN, MU) => MU
rule #memory(CALLER, MU) => MU
rule #memory(CALLVALUE, MU) => MU
rule #memory(CALLDATASIZE, MU) => MU
rule #memory(CODESIZE, MU) => MU
rule #memory(GASPRICE, MU) => MU
rule #memory(COINBASE, MU) => MU
rule #memory(TIMESTAMP, MU) => MU
rule #memory(NUMBER, MU) => MU
rule #memory(DIFFICULTY, MU) => MU
rule #memory(GASLIMIT, MU) => MU
rule #memory(PC, MU) => MU
rule #memory(MSIZE, MU) => MU
rule #memory(GAS, MU) => MU
rule #memory(SELFDESTRUCT _, MU) => MU
rule #memory(CALLDATALOAD _, MU) => MU
rule #memory(EXTCODESIZE _, MU) => MU
rule #memory(BALANCE _, MU) => MU
rule #memory(BLOCKHASH _, MU) => MU
rule #memory(_:PrecompiledOp, MU) => MU
syntax Int ::= #memoryUsageUpdate ( Int , Int , Int ) [function]
// ----------------------------------------------------------------
rule #memoryUsageUpdate(MU, START, 0) => MU
rule #memoryUsageUpdate(MU, START, WIDTH) => maxInt(MU, (START +Int WIDTH) up/Int 32) requires WIDTH >Int 0
Execution Gas¶
Each opcode has an intrinsic gas cost of execution as well (appendix H of the yellowpaper).
#gasExecloads all the relevant surronding state and uses that to compute the intrinsic execution gas of each opcode.
syntax InternalOp ::= #gasExec ( Schedule , OpCode )
// ----------------------------------------------------
rule <k> #gasExec(SCHED, SSTORE INDEX VALUE) => Csstore(SCHED, VALUE, #lookup(STORAGE, INDEX)) ... </k>
<id> ACCT </id>
<account>
<acctID> ACCT </acctID>
<storage> STORAGE </storage>
...
</account>
rule <k> #gasExec(SCHED, EXP W0 0) => Gexp < SCHED > ... </k>
rule <k> #gasExec(SCHED, EXP W0 W1) => Gexp < SCHED > +Int (Gexpbyte < SCHED > *Int (1 +Int (log256Int(W1)))) ... </k> requires W1 =/=K 0
rule <k> #gasExec(SCHED, CALLDATACOPY _ _ WIDTH) => Gverylow < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... </k>
rule <k> #gasExec(SCHED, CODECOPY _ _ WIDTH) => Gverylow < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... </k>
rule <k> #gasExec(SCHED, EXTCODECOPY _ _ _ WIDTH) => Gextcodecopy < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... </k>
rule <k> #gasExec(SCHED, LOG(N) _ WIDTH) => (Glog < SCHED > +Int (Glogdata < SCHED > *Int WIDTH) +Int (N *Int Glogtopic < SCHED >)) ... </k>
rule <k> #gasExec(SCHED, CALL GCAP ACCTTO VALUE _ _ _ _) => Ccall(SCHED, ACCTTO, ACCTS, GCAP, GAVAIL, VALUE) ... </k>
<activeAccounts> ACCTS </activeAccounts>
<gas> GAVAIL </gas>
rule <k> #gasExec(SCHED, CALLCODE GCAP _ VALUE _ _ _ _) => Ccall(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, VALUE) ... </k>
<id> ACCTFROM </id>
<activeAccounts> ACCTS </activeAccounts>
<gas> GAVAIL </gas>
rule <k> #gasExec(SCHED, DELEGATECALL GCAP _ _ _ _ _) => Ccall(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, 0) ... </k>
<id> ACCTFROM </id>
<activeAccounts> ACCTS </activeAccounts>
<gas> GAVAIL </gas>
rule <k> #gasExec(SCHED, SELFDESTRUCT ACCTTO) => Cselfdestruct(SCHED, ACCTTO, ACCTS, BAL) ... </k>
<activeAccounts> ACCTS </activeAccounts>
<id> ACCTFROM </id>
<account>
<acctID> ACCTFROM </acctID>
<balance> BAL </balance>
...
</account>
rule <k> #gasExec(SCHED, CREATE _ _ _) => Gcreate < SCHED > ... </k>
rule <k> #gasExec(SCHED, SHA3 _ WIDTH) => Gsha3 < SCHED > +Int (Gsha3word < SCHED > *Int (WIDTH up/Int 32)) ... </k>
rule <k> #gasExec(SCHED, JUMPDEST) => Gjumpdest < SCHED > ... </k>
rule <k> #gasExec(SCHED, SLOAD _) => Gsload < SCHED > ... </k>
// Wzero
rule <k> #gasExec(SCHED, STOP) => Gzero < SCHED > ... </k>
rule <k> #gasExec(SCHED, RETURN _ _) => Gzero < SCHED > ... </k>
// Wbase
rule <k> #gasExec(SCHED, ADDRESS) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, ORIGIN) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, CALLER) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, CALLVALUE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, CALLDATASIZE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, CODESIZE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, GASPRICE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, COINBASE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, TIMESTAMP) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, NUMBER) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, DIFFICULTY) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, GASLIMIT) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, POP _) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, PC) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, MSIZE) => Gbase < SCHED > ... </k>
rule <k> #gasExec(SCHED, GAS) => Gbase < SCHED > ... </k>
// Wverylow
rule <k> #gasExec(SCHED, ADD _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SUB _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, NOT _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, LT _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, GT _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SLT _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SGT _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, EQ _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, ISZERO _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, AND _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, EVMOR _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, XOR _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, BYTE _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, CALLDATALOAD _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, MLOAD _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, MSTORE _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, MSTORE8 _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, PUSH(_, _)) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, DUP(_) _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SWAP(_) _) => Gverylow < SCHED > ... </k>
// Wlow
rule <k> #gasExec(SCHED, MUL _ _) => Glow < SCHED > ... </k>
rule <k> #gasExec(SCHED, DIV _ _) => Glow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SDIV _ _) => Glow < SCHED > ... </k>
rule <k> #gasExec(SCHED, MOD _ _) => Glow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SMOD _ _) => Glow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SIGNEXTEND _ _) => Glow < SCHED > ... </k>
// Wmid
rule <k> #gasExec(SCHED, ADDMOD _ _ _) => Gmid < SCHED > ... </k>
rule <k> #gasExec(SCHED, MULMOD _ _ _) => Gmid < SCHED > ... </k>
rule <k> #gasExec(SCHED, JUMP _) => Gmid < SCHED > ... </k>
// Whigh
rule <k> #gasExec(SCHED, JUMPI _ _) => Ghigh < SCHED > ... </k>
rule <k> #gasExec(SCHED, EXTCODESIZE _) => Gextcodesize < SCHED > ... </k>
rule <k> #gasExec(SCHED, BALANCE _) => Gbalance < SCHED > ... </k>
rule <k> #gasExec(SCHED, BLOCKHASH _) => Gblockhash < SCHED > ... </k>
// Precompiled
rule <k> #gasExec(_, ECREC) => 3000 ... </k>
rule <k> #gasExec(_, SHA256) => 60 +Int 12 *Int (#sizeWordStack(DATA) up/Int 32) ... </k> <callData> DATA </callData>
rule <k> #gasExec(_, RIP160) => 600 +Int 120 *Int (#sizeWordStack(DATA) up/Int 32) ... </k> <callData> DATA </callData>
rule <k> #gasExec(_, ID) => 15 +Int 3 *Int (#sizeWordStack(DATA) up/Int 32) ... </k> <callData> DATA </callData>
There are several helpers for calculating gas (most of them also specified in the yellowpaper).
Note: These are all functions as the operator #gasExec has already
loaded all the relevant state.
syntax Int ::= Csstore ( Schedule , Int , Int ) [function]
// ----------------------------------------------------------
rule Csstore(SCHED, VALUE, OLD) => #ifInt VALUE =/=Int 0 andBool OLD ==Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi
syntax Int ::= Ccall ( Schedule , Int , Map , Int , Int , Int ) [function]
| Ccallgas ( Schedule , Int , Map , Int , Int , Int ) [function]
| Cgascap ( Schedule , Int , Int , Int ) [function]
| Cextra ( Schedule , Int , Map , Int ) [function]
| Cxfer ( Schedule , Int ) [function]
| Cnew ( Schedule , Int , Map , Int ) [function]
// -----------------------------------------------------------------------------
rule Ccall(SCHED, ACCT, ACCTS, GCAP, GAVAIL, VALUE) => Cextra(SCHED, ACCT, ACCTS, VALUE) +Int Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ACCT, ACCTS, VALUE))
rule Ccallgas(SCHED, ACCT, ACCTS, GCAP, GAVAIL, 0) => Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ACCT, ACCTS, 0))
rule Ccallgas(SCHED, ACCT, ACCTS, GCAP, GAVAIL, VALUE) => Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ACCT, ACCTS, VALUE)) +Int Gcallstipend < SCHED > requires VALUE =/=K 0
rule Cgascap(SCHED, GCAP, GAVAIL, GEXTRA) => minInt(#allBut64th(GAVAIL -Int GEXTRA), GCAP) requires GAVAIL >=Int GEXTRA andBool notBool Gstaticcalldepth << SCHED >>
rule Cgascap(SCHED, GCAP, GAVAIL, GEXTRA) => GCAP requires GAVAIL <Int GEXTRA orBool Gstaticcalldepth << SCHED >>
rule Cextra(SCHED, ACCT, ACCTS, VALUE) => Gcall < SCHED > +Int Cnew(SCHED, ACCT, ACCTS, VALUE) +Int Cxfer(SCHED, VALUE)
rule Cxfer(SCHED, 0) => 0
rule Cxfer(SCHED, N) => Gcallvalue < SCHED > requires N =/=K 0
rule Cnew(SCHED, ACCT, ACCTS, VALUE) => Gnewaccount < SCHED >
requires #accountNonexistent(SCHED, ACCT, ACCTS) andBool (VALUE =/=Int 0 orBool Gzerovaluenewaccountgas << SCHED >>)
rule Cnew(SCHED, ACCT, ACCTS, VALUE) => 0
requires notBool #accountNonexistent(SCHED, ACCT, ACCTS) orBool (VALUE ==Int 0 andBool notBool Gzerovaluenewaccountgas << SCHED >>)
syntax Int ::= Cselfdestruct ( Schedule , Int , Map , Int ) [function]
// ----------------------------------------------------------------------
rule Cselfdestruct(SCHED, ACCT, ACCTS, BAL) => Gselfdestruct < SCHED > +Int Gnewaccount < SCHED >
requires (#accountNonexistent(SCHED, ACCT, ACCTS)) andBool ( Gselfdestructnewaccount << SCHED >>) andBool (BAL =/=Int 0 orBool Gzerovaluenewaccountgas << SCHED >>)
rule Cselfdestruct(SCHED, ACCT, ACCTS, BAL) => Gselfdestruct < SCHED >
requires (#accountNonexistent(SCHED, ACCT, ACCTS)) andBool (notBool Gselfdestructnewaccount << SCHED >> orBool (BAL ==Int 0 andBool notBool Gzerovaluenewaccountgas << SCHED >>))
rule Cselfdestruct(SCHED, ACCT, ACCTS, BAL) => Gselfdestruct < SCHED >
requires notBool #accountNonexistent(SCHED, ACCT, ACCTS)
syntax Bool ::= #accountNonexistent ( Schedule , Int , Map ) [function]
| #accountEmpty ( Int , Map ) [function]
// -----------------------------------------------------------------------
rule #accountNonexistent(SCHED, ACCT, ACCTS) => notBool ACCT in_keys(ACCTS) orBool (#accountEmpty(ACCT, ACCTS) andBool Gemptyisnonexistent << SCHED >>)
rule #accountEmpty(ACCT, (ACCT |-> EMPTY) _) => EMPTY
syntax Int ::= #allBut64th ( Int ) [function]
// ---------------------------------------------
rule #allBut64th(N) => N -Int (N /Int 64)
syntax Int ::= G0 ( Schedule , WordStack , Bool ) [function]
// ------------------------------------------------------------
rule G0(SCHED, .WordStack, true) => Gtxcreate < SCHED >
rule G0(SCHED, .WordStack, false) => Gtransaction < SCHED >
rule G0(SCHED, 0 : REST, ISCREATE) => Gtxdatazero < SCHED > +Int G0(SCHED, REST, ISCREATE)
rule G0(SCHED, N : REST, ISCREATE) => Gtxdatanonzero < SCHED > +Int G0(SCHED, REST, ISCREATE) requires N =/=Int 0
syntax Int ::= "G*" "(" Int "," Int "," Int ")" [function]
// ----------------------------------------------------------
rule G*(GAVAIL, GLIMIT, REFUND) => GAVAIL +Int minInt((GLIMIT -Int GAVAIL)/Int 2, REFUND)
Fee Schedule from C++ Implementation¶
The C++ Implementation of
EVM specifies several
different “profiles” for how the VM works. Here we provide each protocol
from the C++ implementation, as the yellowpaper does not contain all the
different profiles. Specify which profile by passing in the argument
-cSCHEDULE=<FEE_SCHEDULE> when calling krun (the available
<FEE_SCHEDULE> are supplied here).
A ScheduleFlag is a boolean determined by the fee schedule; applying
a ScheduleFlag to a Schedule yields whether the flag is set or
not.
syntax Bool ::= ScheduleFlag "<<" Schedule ">>" [function]
// ----------------------------------------------------------
syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas"
// --------------------------------------------------------------------------------------------------------------------------
A ScheduleConst is a constant determined by the fee schedule;
applying a ScheduleConst to a Schedule yields the correct
constant for that schedule.
syntax Int ::= ScheduleConst "<" Schedule ">" [function]
// --------------------------------------------------------
syntax ScheduleConst ::= "Gzero" | "Gbase" | "Gverylow" | "Glow" | "Gmid" | "Ghigh"
| "Gextcodesize" | "Gextcodecopy" | "Gbalance" | "Gsload" | "Gjumpdest" | "Gsstoreset"
| "Gsstorereset" | "Rsstoreclear" | "Rselfdestruct" | "Gselfdestruct" | "Gcreate" | "Gcodedeposit"
| "Gcall" | "Gcallvalue" | "Gcallstipend" | "Gnewaccount" | "Gexp" | "Gexpbyte"
| "Gmemory" | "Gtxcreate" | "Gtxdatazero" | "Gtxdatanonzero" | "Gtransaction" | "Glog" | "Glogdata"
| "Glogtopic" | "Gsha3" | "Gsha3word" | "Gcopy" | "Gblockhash" | "Gquadcoeff" | "maxCodeSize"
// ------------------------------------------------------------------------------------------------------------------------------------------------
Defualt Schedule¶
syntax Schedule ::= "DEFAULT"
// -----------------------------
rule Gzero < DEFAULT > => 0
rule Gbase < DEFAULT > => 2
rule Gverylow < DEFAULT > => 3
rule Glow < DEFAULT > => 5
rule Gmid < DEFAULT > => 8
rule Ghigh < DEFAULT > => 10
rule Gexp < DEFAULT > => 10
rule Gexpbyte < DEFAULT > => 10
rule Gsha3 < DEFAULT > => 30
rule Gsha3word < DEFAULT > => 6
rule Gsload < DEFAULT > => 50
rule Gsstoreset < DEFAULT > => 20000
rule Gsstorereset < DEFAULT > => 5000
rule Rsstoreclear < DEFAULT > => 15000
rule Glog < DEFAULT > => 375
rule Glogdata < DEFAULT > => 8
rule Glogtopic < DEFAULT > => 375
rule Gcall < DEFAULT > => 40
rule Gcallstipend < DEFAULT > => 2300
rule Gcallvalue < DEFAULT > => 9000
rule Gnewaccount < DEFAULT > => 25000
rule Gcreate < DEFAULT > => 32000
rule Gcodedeposit < DEFAULT > => 200
rule Gselfdestruct < DEFAULT > => 0
rule Rselfdestruct < DEFAULT > => 24000
rule Gmemory < DEFAULT > => 3
rule Gquadcoeff < DEFAULT > => 512
rule Gcopy < DEFAULT > => 3
rule Gtransaction < DEFAULT > => 21000
rule Gtxcreate < DEFAULT > => 53000
rule Gtxdatazero < DEFAULT > => 4
rule Gtxdatanonzero < DEFAULT > => 68
rule Gjumpdest < DEFAULT > => 1
rule Gbalance < DEFAULT > => 20
rule Gblockhash < DEFAULT > => 20
rule Gextcodesize < DEFAULT > => 20
rule Gextcodecopy < DEFAULT > => 20
rule maxCodeSize < DEFAULT > => 2 ^Int 32 -Int 1
rule Gselfdestructnewaccount << DEFAULT >> => false
rule Gstaticcalldepth << DEFAULT >> => true
rule Gemptyisnonexistent << DEFAULT >> => false
rule Gzerovaluenewaccountgas << DEFAULT >> => true
struct EVMSchedule
{
EVMSchedule(): tierStepGas(std::array<unsigned, 8>{{0, 2, 3, 5, 8, 10, 20, 0}}) {}
EVMSchedule(bool _efcd, bool _hdc, unsigned const& _txCreateGas): exceptionalFailedCodeDeposit(_efcd), haveDelegateCall(_hdc), tierStepGas(std::array<unsigned, 8>{{0, 2, 3, 5, 8, 10, 20, 0}}), txCreateGas(_txCreateGas) {}
bool exceptionalFailedCodeDeposit = true;
bool haveDelegateCall = true;
bool eip150Mode = false;
bool eip158Mode = false;
bool haveRevert = false;
bool haveReturnData = false;
bool haveStaticCall = false;
bool haveCreate2 = false;
std::array<unsigned, 8> tierStepGas;
unsigned expGas = 10;
unsigned expByteGas = 10;
unsigned sha3Gas = 30;
unsigned sha3WordGas = 6;
unsigned sloadGas = 50;
unsigned sstoreSetGas = 20000;
unsigned sstoreResetGas = 5000;
unsigned sstoreRefundGas = 15000;
unsigned logGas = 375;
unsigned logDataGas = 8;
unsigned logTopicGas = 375;
unsigned callGas = 40;
unsigned callStipend = 2300;
unsigned callValueTransferGas = 9000;
unsigned callNewAccountGas = 25000;
unsigned createGas = 32000;
unsigned createDataGas = 200;
unsigned suicideGas = 0;
unsigned suicideRefundGas = 24000;
unsigned memoryGas = 3;
unsigned quadCoeffDiv = 512;
unsigned copyGas = 3;
unsigned txGas = 21000;
unsigned txCreateGas = 53000;
unsigned txDataZeroGas = 4;
unsigned txDataNonZeroGas = 68;
unsigned jumpdestGas = 1;
unsigned balanceGas = 20;
unsigned blockhashGas = 20;
unsigned extcodesizeGas = 20;
unsigned extcodecopyGas = 20;
unsigned maxCodeSize = unsigned(-1);
bool staticCallDepthLimit() const { return !eip150Mode; }
bool suicideNewAccountGas() const { return !eip150Mode; }
bool suicideChargesNewAccountGas() const { return eip150Mode; }
bool emptinessIsNonexistence() const { return eip158Mode; }
bool zeroValueTransferChargesNewAccountGas() const { return !eip158Mode; }
};
Frontier Schedule¶
syntax Schedule ::= "FRONTIER"
// ------------------------------
rule Gtxcreate < FRONTIER > => 21000
rule SCHEDCONST < FRONTIER > => SCHEDCONST < DEFAULT > requires SCHEDCONST =/=K Gtxcreate
rule SCHEDFLAG << FRONTIER >> => SCHEDFLAG << DEFAULT >>
static const EVMSchedule FrontierSchedule = EVMSchedule(false, false, 21000);
Homestead Schedule¶
syntax Schedule ::= "HOMESTEAD"
// -------------------------------
rule SCHEDCONST < HOMESTEAD > => SCHEDCONST < DEFAULT >
rule SCHEDFLAG << HOMESTEAD >> => SCHEDFLAG << DEFAULT >>
static const EVMSchedule HomesteadSchedule = EVMSchedule(true, true, 53000);
EIP150 Schedule¶
syntax Schedule ::= "EIP150"
// ----------------------------
rule Gbalance < EIP150 > => 400
rule Gsload < EIP150 > => 200
rule Gcall < EIP150 > => 700
rule Gselfdestruct < EIP150 > => 5000
rule Gextcodesize < EIP150 > => 700
rule Gextcodecopy < EIP150 > => 700
rule SCHEDCONST < EIP150 > => SCHEDCONST < HOMESTEAD >
requires notBool ( SCHEDCONST ==K Gbalance orBool SCHEDCONST ==K Gsload orBool SCHEDCONST ==K Gcall
orBool SCHEDCONST ==K Gselfdestruct orBool SCHEDCONST ==K Gextcodesize orBool SCHEDCONST ==K Gextcodecopy
)
rule Gselfdestructnewaccount << EIP150 >> => true
rule Gstaticcalldepth << EIP150 >> => false
rule SCHEDCONST << EIP150 >> => SCHEDCONST << HOMESTEAD >>
requires notBool ( SCHEDCONST ==K Gselfdestructnewaccount orBool SCHEDCONST ==K Gstaticcalldepth )
static const EVMSchedule EIP150Schedule = []
{
EVMSchedule schedule = HomesteadSchedule;
schedule.eip150Mode = true;
schedule.extcodesizeGas = 700;
schedule.extcodecopyGas = 700;
schedule.balanceGas = 400;
schedule.sloadGas = 200;
schedule.callGas = 700;
schedule.suicideGas = 5000;
return schedule;
}();
EIP158 Schedule¶
syntax Schedule ::= "EIP158"
// ----------------------------
rule Gexpbyte < EIP158 > => 50
rule maxCodeSize < EIP158 > => 24576
rule SCHEDCONST < EIP158 > => SCHEDCONST < EIP150 > requires SCHEDCONST =/=K Gexpbyte andBool SCHEDCONST =/=K maxCodeSize
rule Gemptyisnonexistent << EIP158 >> => true
rule Gzerovaluenewaccountgas << EIP158 >> => false
rule SCHEDCONST << EIP158 >> => SCHEDCONST << EIP150 >>
requires notBool ( SCHEDCONST ==K Gemptyisnonexistent orBool SCHEDCONST ==K Gzerovaluenewaccountgas )
static const EVMSchedule EIP158Schedule = []
{
EVMSchedule schedule = EIP150Schedule;
schedule.expByteGas = 50;
schedule.eip158Mode = true;
schedule.maxCodeSize = 0x6000;
return schedule;
}();
Byzantium Schedule¶
syntax Schedule ::= "BYZANTIUM"
// -------------------------------
rule SCHEDCONST < BYZANTIUM > => SCHEDCONST < EIP158 >
rule SCHEDFLAG << BYZANTIUM >> => SCHEDFLAG << EIP158 >>
static const EVMSchedule ByzantiumSchedule = []
{
EVMSchedule schedule = EIP158Schedule;
schedule.haveRevert = true;
schedule.haveReturnData = true;
schedule.haveStaticCall = true;
schedule.blockRewardOverwrite = {3 * ether};
return schedule;
}();
Constantinople Schedule¶
syntax Schedule ::= "CONSTANTINOPLE"
// ------------------------------------
rule Gblockhash < CONSTANTINOPLE > => 800
rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM >
requires SCHEDCONST =/=K Gblockhash
rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >>
static const EVMSchedule ConstantinopleSchedule = []
{
EVMSchedule schedule = ByzantiumSchedule;
schedule.blockhashGas = 800;
schedule.haveCreate2 = true;
return schedule;
}();
EVM Program Representations¶
EVM programs are represented algebraically in K, but programs can load
and manipulate program data directly. The opcodes CODECOPY and
EXTCODECOPY rely on the assembled form of the programs being
present. The opcode CREATE relies on being able to interperet EVM
data as a program.
This is a program representation dependence, which we might want to avoid. Perhaps the only program representation dependence we should have is the hash of the program; doing so achieves:
- Program representation independence (different analysis tools on the language don’t have to ensure they have a common representation of programs, just a common interperetation of the data-files holding programs).
- Programming language independence (we wouldn’t even have to commit to a particular language or interperetation of the data-file).
- Only depending on the hash allows us to know that we have exactly the correct data-file (program), and nothing more.
Disassembler¶
After interpreting the strings representing programs as a WordStack,
it should be changed into an OpCodes for use by the EVM semantics.
#dasmOpCodesinterperetsWordStackas anOpCodes.#dasmPUSHhandles the case of aPushOp.#dasmOpCodeinterperets aIntas anOpCode.
syntax OpCodes ::= #dasmOpCodes ( WordStack , Schedule ) [function]
| #dasmOpCodes ( OpCodes , WordStack , Schedule ) [function, klabel(#dasmOpCodesAux)]
| #revOpCodes ( OpCodes , OpCodes ) [function]
// -----------------------------------------------------------------------------
rule #dasmOpCodes( WS, SCHED ) => #revOpCodes(#dasmOpCodes(.OpCodes, WS, SCHED), .OpCodes)
rule #dasmOpCodes( OPS, .WordStack, _ ) => OPS
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(#dasmOpCode(W, SCHED) ; OPS, WS, SCHED) requires W >=Int 0 andBool W <=Int 95
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(#dasmOpCode(W, SCHED) ; OPS, WS, SCHED) requires W >=Int 165 andBool W <=Int 255
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(DUP(W -Int 127) ; OPS, WS, SCHED) requires W >=Int 128 andBool W <=Int 143
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(SWAP(W -Int 143) ; OPS, WS, SCHED) requires W >=Int 144 andBool W <=Int 159
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(LOG(W -Int 160) ; OPS, WS, SCHED) requires W >=Int 160 andBool W <=Int 164
rule #dasmOpCodes( OPS, W : WS, SCHED ) => #dasmOpCodes(PUSH(W -Int 95, #asWord(#take(W -Int 95, WS))) ; OPS, #drop(W -Int 95, WS), SCHED) requires W >=Int 96 andBool W <=Int 127
rule #revOpCodes ( OP ; OPS , OPS' ) => #revOpCodes(OPS, OP ; OPS')
rule #revOpCodes ( .OpCodes , OPS ) => OPS
syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function]
// -----------------------------------------------------------
rule #dasmOpCode( 0, _ ) => STOP
rule #dasmOpCode( 1, _ ) => ADD
rule #dasmOpCode( 2, _ ) => MUL
rule #dasmOpCode( 3, _ ) => SUB
rule #dasmOpCode( 4, _ ) => DIV
rule #dasmOpCode( 5, _ ) => SDIV
rule #dasmOpCode( 6, _ ) => MOD
rule #dasmOpCode( 7, _ ) => SMOD
rule #dasmOpCode( 8, _ ) => ADDMOD
rule #dasmOpCode( 9, _ ) => MULMOD
rule #dasmOpCode( 10, _ ) => EXP
rule #dasmOpCode( 11, _ ) => SIGNEXTEND
rule #dasmOpCode( 16, _ ) => LT
rule #dasmOpCode( 17, _ ) => GT
rule #dasmOpCode( 18, _ ) => SLT
rule #dasmOpCode( 19, _ ) => SGT
rule #dasmOpCode( 20, _ ) => EQ
rule #dasmOpCode( 21, _ ) => ISZERO
rule #dasmOpCode( 22, _ ) => AND
rule #dasmOpCode( 23, _ ) => EVMOR
rule #dasmOpCode( 24, _ ) => XOR
rule #dasmOpCode( 25, _ ) => NOT
rule #dasmOpCode( 26, _ ) => BYTE
rule #dasmOpCode( 32, _ ) => SHA3
rule #dasmOpCode( 48, _ ) => ADDRESS
rule #dasmOpCode( 49, _ ) => BALANCE
rule #dasmOpCode( 50, _ ) => ORIGIN
rule #dasmOpCode( 51, _ ) => CALLER
rule #dasmOpCode( 52, _ ) => CALLVALUE
rule #dasmOpCode( 53, _ ) => CALLDATALOAD
rule #dasmOpCode( 54, _ ) => CALLDATASIZE
rule #dasmOpCode( 55, _ ) => CALLDATACOPY
rule #dasmOpCode( 56, _ ) => CODESIZE
rule #dasmOpCode( 57, _ ) => CODECOPY
rule #dasmOpCode( 58, _ ) => GASPRICE
rule #dasmOpCode( 59, _ ) => EXTCODESIZE
rule #dasmOpCode( 60, _ ) => EXTCODECOPY
rule #dasmOpCode( 64, _ ) => BLOCKHASH
rule #dasmOpCode( 65, _ ) => COINBASE
rule #dasmOpCode( 66, _ ) => TIMESTAMP
rule #dasmOpCode( 67, _ ) => NUMBER
rule #dasmOpCode( 68, _ ) => DIFFICULTY
rule #dasmOpCode( 69, _ ) => GASLIMIT
rule #dasmOpCode( 80, _ ) => POP
rule #dasmOpCode( 81, _ ) => MLOAD
rule #dasmOpCode( 82, _ ) => MSTORE
rule #dasmOpCode( 83, _ ) => MSTORE8
rule #dasmOpCode( 84, _ ) => SLOAD
rule #dasmOpCode( 85, _ ) => SSTORE
rule #dasmOpCode( 86, _ ) => JUMP
rule #dasmOpCode( 87, _ ) => JUMPI
rule #dasmOpCode( 88, _ ) => PC
rule #dasmOpCode( 89, _ ) => MSIZE
rule #dasmOpCode( 90, _ ) => GAS
rule #dasmOpCode( 91, _ ) => JUMPDEST
rule #dasmOpCode( 240, _ ) => CREATE
rule #dasmOpCode( 241, _ ) => CALL
rule #dasmOpCode( 242, _ ) => CALLCODE
rule #dasmOpCode( 243, _ ) => RETURN
rule #dasmOpCode( 244, SCHED ) => DELEGATECALL requires SCHED =/=K FRONTIER
rule #dasmOpCode( 255, _ ) => SELFDESTRUCT
rule #dasmOpCode( W, _ ) => INVALID [owise]
endmodule