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. .. code-block:: k 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. .. code-block:: k configuration $PGM:EthereumSimulation 1 $MODE:Mode $SCHEDULE:Schedule .Map // EVM Specific // ============ // Mutable during a single transaction // ----------------------------------- .WordStack // H_RETURN 0 // \mu_i 0 .List .List .List .Set .Map // I_b .WordStack // I_* 0 // I_a 0 // I_s .WordStack // I_d 0 // I_v // \mu_* .WordStack // \mu_s .Map // \mu_m 0 // \mu_pc 0 // \mu_g 0 // A_* (execution substate) .Set // A_s .List // A_l 0 // A_r // Immutable during a single transaction // ------------------------------------- 0 // I_p 0 // I_o // I_H* (block information) 0 // I_Hp 0 // I_Ho 0 // I_Hc 0 // I_Hr 0 // I_Ht 0 // I_He .WordStack // I_Hb 0 // I_Hd 0 // I_Hi 0 // I_Hl 0 // I_Hg 0 // I_Hs .WordStack // I_Hx 0 // I_Hm 0 // I_Hn [ .JSONList ] .List // Ethereum Network // ================ // Accounts Record // --------------- .Map - UIUC-K and RV-K have slight differences of opinion here. .. code-block:: k .. code-block:: k .. code-block:: k 0 0 .WordStack .Map 0 // Transactions Record // ------------------- .List .List - UIUC-K and RV-K have slight differences of opinion here. .. code-block:: k .. code-block:: k .. code-block:: k 0 0 // T_n 0 // T_p 0 // T_g .Account // T_t 0 // T_v 0 // T_w .WordStack // T_r .WordStack // T_s .WordStack // T_i/T_e syntax EthereumSimulation // ------------------------- Modal Semantics --------------- Our semantics is modal, with the initial mode being set on the command line via ``-cMODE=EXECMODE``. - ``NORMAL`` executes as a client on the network would. - ``VMTESTS`` skips ``CALL*`` and ``CREATE`` operations. .. code-block:: k syntax Mode ::= "NORMAL" | "VMTESTS" - ``#setMode_`` sets the mode to the supplied one. .. code-block:: k syntax Mode ::= "#setMode" Mode // ------------------------------- rule #setMode EXECMODE => . ... _ => EXECMODE rule EX:Exception ~> (#setMode _ => .) ... Hardware -------- The ``callStack`` cell stores a list of previous VM execution states. - ``#pushCallStack`` saves a copy of VM execution state on the ``callStack``. - ``#popCallStack`` restores the top element of the ``callStack``. - ``#dropCallStack`` removes the top element of the ``callStack``. .. code-block:: k syntax State ::= "{" Int "|" Int "|" Map "|" WordStack "|" Int "|" WordStack "|" Int "|" WordStack "|" Map "|" Int "|" Int "|" Int "}" // -------------------------------------------------------------------------------------------------------------------------------------- syntax InternalOp ::= "#pushCallStack" // -------------------------------------- rule #pushCallStack => . ... (.List => ListItem({ ACCT | GAVAIL | PGM | BYTES | CR | CD | CV | WS | LM | MUSED | PCOUNT | DEPTH })) ... ACCT GAVAIL PGM BYTES CR CD CV WS LM MUSED PCOUNT DEPTH syntax InternalOp ::= "#popCallStack" // ------------------------------------- rule #popCallStack => . ... (ListItem({ ACCT | GAVAIL | PGM | BYTES | CR | CD | CV | WS | LM | MUSED | PCOUNT | DEPTH }) => .List) ... _ => ACCT _ => GAVAIL _ => PGM _ => BYTES _ => CR _ => CD _ => CV _ => WS _ => LM _ => MUSED _ => PCOUNT _ => DEPTH syntax InternalOp ::= "#dropCallStack" // -------------------------------------- rule #dropCallStack => . ... (ListItem(_) => .List) ... The ``interimStates`` cell stores a list of previous world states. - ``#pushWorldState`` stores a copy of the current accounts at the top of the ``interimStates`` cell. - ``#popWorldState`` restores the top element of the ``interimStates``. - ``#dropWorldState`` removes the top element of the ``interimStates``. 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. .. code-block:: k syntax Account ::= "{" Int "|" Int "|" WordStack "|" Map "|" Int "|" Bool "}" // ----------------------------------------------------------------------------- syntax InternalOp ::= "#pushWorldState" | "#pushWorldStateAux" Map | "#pushAccount" Int Bool // -------------------------------------------------------------------------------------------- rule #pushWorldState => #pushWorldStateAux ACCTS ... ACCTS (.List => ListItem(.Set)) ... rule #pushWorldStateAux .Map => . ... rule #pushWorldStateAux ((ACCT |-> EMPTY) REST) => #pushAccount ACCT EMPTY ~> #pushWorldStateAux REST ... rule #pushAccount ACCT EMPTY => . ... ListItem((.Set => SetItem({ ACCT | BAL | CODE | STORAGE | NONCE | EMPTY })) REST) ... ACCT BAL CODE STORAGE NONCE syntax InternalOp ::= "#popWorldState" | "#popWorldStateAux" Set // ---------------------------------------------------------------- rule #popWorldState => #popWorldStateAux PREVSTATE ... (ListItem(PREVSTATE) => .List) ... _ => .Map _ => .Bag rule #popWorldStateAux .Set => . ... rule #popWorldStateAux ( (SetItem({ ACCT | BAL | CODE | STORAGE | NONCE | EMPTY }) => .Set) REST ) ... ... (.Map => ACCT |-> EMPTY) ( .Bag => ACCT BAL CODE STORAGE NONCE ) ... syntax InternalOp ::= "#dropWorldState" // --------------------------------------- rule #dropWorldState => . ... (ListItem(_) => .List) ... .. code-block:: k syntax Accounts ::= "{" AccountsCell "|" Map "}" // ------------------------------------------------ syntax InternalOp ::= "#pushWorldState" // --------------------------------------- rule #pushWorldState => .K ... ACCTS ACCTDATA (.List => ListItem({ ACCTDATA | ACCTS })) ... syntax InternalOp ::= "#popWorldState" // -------------------------------------- rule #popWorldState => .K ... (ListItem({ ACCTDATA | ACCTS }) => .List) ... _ => ACCTS _ => ACCTDATA syntax InternalOp ::= "#dropWorldState" // --------------------------------------- rule #dropWorldState => . ... (ListItem(_) => .List) ... The ``substateStack`` cell stores a list of previous substate logs. - ``#pushSubstate`` stores a copy of the current substate at the top of the ``substateStack`` cell. - ``#popSubstate`` restores the top element of the ``substateStack``. - ``#dropSubstate`` removes the top element of the ``substateStack``. .. code-block:: k syntax InternalOp ::= "#pushSubstate" // ------------------------------------- rule #pushSubstate => .K ... SUBSTATE (.List => ListItem( SUBSTATE )) ... syntax InternalOp ::= "#popSubstate" // ------------------------------------ rule #popSubstate => .K ... _ => SUBSTATE (ListItem( SUBSTATE ) => .List) ... syntax InternalOp ::= "#dropSubstate" // ------------------------------------- rule #dropSubstate => .K ... (ListItem(_) => .List) ... Simple commands controlling exceptions provide control-flow. - ``#end`` is used to indicate the (non-exceptional) end of execution. - ``#exception`` is 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 the ``op`` cell it takes the first branch, if an exception runs into it it takes the second branch. .. code-block:: k syntax KItem ::= Exception syntax Exception ::= "#exception" | "#end" // ------------------------------------------ rule EX:Exception ~> (_:Int => .) ... rule EX:Exception ~> (_:OpCode => .) ... syntax KItem ::= "#?" K ":" K "?#" // ---------------------------------- rule #? K : _ ?# => K ... rule #exception ~> #? _ : K ?# => K ... rule #end ~> (#? K : _ ?#) => K ~> #end ... OpCode Execution Cycle ---------------------- ``OpCode`` is broken into several subsorts for easier handling. Here all ``OpCode``\ s are subsorted into ``KItem`` (allowing sequentialization), and the various sorts of opcodes are subsorted into ``OpCode``. .. code-block:: k syntax KItem ::= OpCode syntax OpCode ::= NullStackOp | UnStackOp | BinStackOp | TernStackOp | QuadStackOp | InvalidOp | StackOp | InternalOp | CallOp | CallSixOp | PushOp // -------------------------------------------------------------------------------- - ``#execute`` calls ``#next`` repeatedly until it recieves an ``#end`` or ``#exception``. - ``#execTo`` executes until the next opcode is one of the specified ones. .. code-block:: k syntax KItem ::= "#execute" // --------------------------- rule (. => #next) ~> #execute ... rule EX:Exception ~> (#execute => .) ... syntax InternalOp ::= "#execTo" Set // ----------------------------------- rule (. => #next) ~> #execTo OPS ... PCOUNT ... PCOUNT |-> OP ... requires notBool (OP in OPS) rule #execTo OPS => . ... PCOUNT ... PCOUNT |-> OP ... requires OP in OPS rule #execTo OPS => #end ... PCOUNT PGM 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, ``#next`` will throw ``#end`` or ``#exception`` if 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. .. code-block:: k syntax InternalOp ::= "#next" // ----------------------------- rule #next => #end ... PCOUNT PGM requires notBool (PCOUNT in_keys(PGM)) - In ``NORMAL`` or ``VMTESTS`` mode, ``#next`` checks if the opcode is exceptional, runs it if not, then increments the program counter. .. code-block:: k rule EXECMODE #next => #pushCallStack ~> #exceptional? [ OP ] ~> #exec [ OP ] ~> #pc [ OP ] ~> #? #dropCallStack : #popCallStack ~> #exception ?# ... PCOUNT ... PCOUNT |-> OP ... 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 cause ``wordStack`` size issues (this implements the function ``Z`` in the yellowpaper, section 9.4.2). .. code-block:: k syntax InternalOp ::= "#exceptional?" "[" OpCode "]" // ---------------------------------------------------- rule #exceptional? [ OP ] => #invalid? [ OP ] ~> #stackNeeded? [ OP ] ~> #badJumpDest? [ OP ] ... - ``#invalid?`` checks if it's the designated invalid opcode. .. code-block:: k syntax InternalOp ::= "#invalid?" "[" OpCode "]" // ------------------------------------------------ rule #invalid? [ INVALID ] => #exception ... rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) - ``#stackNeeded?`` checks that the stack will be not be under/overflown. - ``#stackNeeded``, ``#stackAdded``, and ``#stackDelta`` are helpers for deciding ``#stackNeeded?``. .. code-block:: k syntax InternalOp ::= "#stackNeeded?" "[" OpCode "]" // ---------------------------------------------------- rule #stackNeeded? [ OP ] => #exception ... WS requires #sizeWordStack(WS) Int 1024 rule #stackNeeded? [ OP ] => .K ... WS requires notBool (#sizeWordStack(WS) 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. .. code-block:: k syntax InternalOp ::= "#badJumpDest?" "[" OpCode "]" // ---------------------------------------------------- rule #badJumpDest? [ OP ] => . ... requires notBool isJumpOp(OP) rule #badJumpDest? [ OP ] => . ... DEST : WS ... DEST |-> JUMPDEST ... requires isJumpOp(OP) rule #badJumpDest? [ JUMPI ] => . ... _ : 0 : WS rule #badJumpDest? [ JUMP ] => #exception ... DEST : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST rule #badJumpDest? [ JUMPI ] => #exception ... DEST : W : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST andBool W =/=K 0 rule #badJumpDest? [ JUMP ] => #exception ... DEST : WS PGM requires notBool (DEST in_keys(PGM)) rule #badJumpDest? [ JUMPI ] => #exception ... DEST : W : WS PGM requires (notBool (DEST in_keys(PGM))) andBool W =/=K 0 Execution Step ~~~~~~~~~~~~~~ - ``#exec`` will load the arguments of the opcode (it assumes ``#stackNeeded?`` is accurate and has been called) and trigger the subsequent operations. .. code-block:: k syntax InternalOp ::= "#exec" "[" OpCode "]" // -------------------------------------------- rule #exec [ OP ] => #gas [ OP ] ~> OP ... 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. .. code-block:: k syntax InternalOp ::= UnStackOp Int | BinStackOp Int Int | TernStackOp Int Int Int | QuadStackOp Int Int Int Int // ------------------------------------------------- rule #exec [ UOP:UnStackOp => UOP #addr?(UOP, W0) ] ... W0 : WS => WS rule #exec [ BOP:BinStackOp => BOP #addr?(BOP, W0) W1 ] ... W0 : W1 : WS => WS rule #exec [ TOP:TernStackOp => TOP #addr?(TOP, W0) W1 W2 ] ... W0 : W1 : W2 : WS => WS rule #exec [ QOP:QuadStackOp => QOP #addr?(QOP, W0) W1 W2 W3 ] ... W0 : W1 : W2 : W3 : WS => WS 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. .. code-block:: k syntax InternalOp ::= StackOp WordStack // --------------------------------------- rule #exec [ SO:StackOp => SO WS ] ... WS The ``CallOp`` opcodes all interperet their second argument as an address. .. code-block:: k syntax InternalOp ::= CallSixOp Int Int Int Int Int Int | CallOp Int Int Int Int Int Int Int // ----------------------------------------------------------- rule #exec [ CSO:CallSixOp => CSO W0 #addr(W1) W2 W3 W4 W5 ] ... W0 : W1 : W2 : W3 : W4 : W5 : WS => WS rule #exec [ CO:CallOp => CO W0 #addr(W1) W2 W3 W4 W5 W6 ] ... W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS - ``#gas`` calculates how much gas this operation costs, and takes into account the memory consumed. .. code-block:: k syntax InternalOp ::= "#gas" "[" OpCode "]" | "#deductGas" | "#deductMemory" // ---------------------------------------------------------------------------- rule #gas [ OP ] => #memory(OP, MU) ~> #deductMemory ~> #gasExec(SCHED, OP) ~> #deductGas ... MU SCHED rule MU':Int ~> #deductMemory => #exception ... requires MU' >=Int pow256 rule MU':Int ~> #deductMemory => (Cmem(SCHED, MU') -Int Cmem(SCHED, MU)) ~> #deductGas ... MU => MU' SCHED requires MU' G:Int ~> #deductGas => #exception ... GAVAIL requires GAVAIL G:Int ~> #deductGas => . ... GAVAIL => GAVAIL -Int G _ => GAVAIL 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. - ``#pc`` calculates the next program counter of the given operator. .. code-block:: k syntax InternalOp ::= "#pc" "[" OpCode "]" // ------------------------------------------ rule #pc [ OP ] => . ... PCOUNT => PCOUNT +Int 1 requires notBool (isPushOp(OP) orBool isJumpOp(OP)) rule #pc [ PUSH(N, _) ] => . ... PCOUNT => PCOUNT +Int (1 +Int N) rule #pc [ OP ] => . ... 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``). .. code-block:: k syntax SubstateLogEntry ::= "{" Int "|" WordStack "|" WordStack "}" // ------------------------------------------------------------------- After executing a transaction, it's necessary to have the effect of the substate log recorded. - ``#finalizeTx`` makes the substate log actually have an effect on the state. .. code-block:: k syntax InternalOp ::= #finalizeTx ( Bool ) // ------------------------------------------ rule #finalizeTx(true) => . ... .Set rule #finalizeTx(false => true) ... VMTESTS ACCT BAL => 0 ACCT CURRBAL => CURRBAL +Word BAL ... ... ACCT |-> (EMPTY => #if BAL >Int 0 #then false #else EMPTY #fi) ... rule (.K => #newAccount MINER) ~> #finalizeTx(_)... NORMAL MINER ACCTS requires notBool MINER in_keys(ACCTS) rule #finalizeTx(false) ... NORMAL GAVAIL => G*(GAVAIL, GLIMIT, REFUND) REFUND => 0 ListItem(MSGID:Int) ... MSGID GLIMIT ... requires REFUND =/=Int 0 rule #finalizeTx(false => true) ... NORMAL ORG MINER GAVAIL 0 ORG ORGBAL => ORGBAL +Int GAVAIL *Int GPRICE ... MINER MINBAL => MINBAL +Int (GLIMIT -Int GAVAIL) *Int GPRICE ... ListItem(TXID:Int) => .List ... TXID GLIMIT GPRICE ... ... 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) ... requires ORG =/=Int MINER rule #finalizeTx(false => true) ... NORMAL ACCT ACCT 0 ACCT BAL => BAL +Int GLIMIT *Int GPRICE ... ListItem(MsgId:Int) => .List ... MsgId GLIMIT GPRICE ... ... ACCT |-> (EMPTY => #if GLIMIT *Int GPRICE >Int 0 #then false #else EMPTY #fi) ... rule #finalizeTx(true) ... ... (SetItem(ACCT) => .Set) ... (ACCT |-> _ => .Map) ( ACCT ... => .Bag ) ... 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. .. code-block:: k 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. - ``#push`` will push an element to the ``wordStack`` without any checks. - ``#setStack_`` will set the current stack to the given one. .. code-block:: k syntax InternalOp ::= "#push" | "#setStack" WordStack // ----------------------------------------------------- rule W0:Int ~> #push => . ... WS => W0 : WS rule #setStack WS => . ... _ => WS - ``#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. .. code-block:: k syntax InternalOp ::= "#newAccount" Int // --------------------------------------- rule #newAccount ACCT => #exception ... ACCT CODE NONCE ... requires CODE =/=K .WordStack orBool NONCE =/=K 0 rule #newAccount ACCT => . ... ACCT .WordStack 0 _ => .Map ... rule #newAccount ACCT => . ... ACCTS (.Map => ACCT |-> true) ( .Bag => ACCT 0 .WordStack .Map 0 ) ... requires notBool ACCT in_keys(ACCTS) - ``#transferFunds`` moves money from one account into another, creating the destination account if it doesn't exist. .. code-block:: k syntax InternalOp ::= "#transferFunds" Int Int Int // -------------------------------------------------- rule #transferFunds ACCTFROM ACCTTO VALUE => . ... ACCTFROM ORIGFROM => ORIGFROM -Word VALUE NONCE CODE ... ACCTTO ORIGTO => ORIGTO +Word VALUE ... ... ACCTTO |-> (EMPTY => #if VALUE >Int 0 #then false #else EMPTY #fi) ACCTFROM |-> (_ => ORIGFROM ==Int VALUE andBool NONCE ==Int 0 andBool CODE ==K .WordStack) ... requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM rule #transferFunds ACCTFROM ACCTTO VALUE => #exception ... ACCTFROM ORIGFROM ... requires VALUE >Int ORIGFROM rule (. => #newAccount ACCTTO) ~> #transferFunds ACCTFROM ACCTTO VALUE ... ACCTS requires ACCTFROM =/=K ACCTTO andBool notBool ACCTTO in_keys(ACCTS) rule #transferFunds ACCT ACCT VALUE => . ... ACCT ORIGFROM ... requires VALUE <=Int ORIGFROM Invalid Operator ~~~~~~~~~~~~~~~~ We use ``INVALID`` both for marking the designated invalid operator and for garbage bytes in the input program. .. code-block:: k syntax InvalidOp ::= "INVALID" // ------------------------------ Stack Manipulations ~~~~~~~~~~~~~~~~~~~ Some operators don't calculate anything, they just push the stack around a bit. .. code-block:: k syntax UnStackOp ::= "POP" // -------------------------- rule POP W => . ... syntax StackOp ::= DUP ( Int ) | SWAP ( Int ) // --------------------------------------------- rule DUP(N) WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS) ... rule SWAP(N) (W0 : WS) => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... syntax PushOp ::= PUSH ( Int , Int ) // ------------------------------------ rule PUSH(_, W) => W ~> #push ... Local Memory ~~~~~~~~~~~~ These operations are getters/setters of the local execution memory. .. code-block:: k syntax UnStackOp ::= "MLOAD" // ---------------------------- rule MLOAD INDEX => #asWord(#range(LM, INDEX, 32)) ~> #push ... LM syntax BinStackOp ::= "MSTORE" | "MSTORE8" // ------------------------------------------ rule MSTORE INDEX VALUE => . ... LM => LM [ INDEX := #padToWidth(32, #asByteStack(VALUE)) ] rule MSTORE8 INDEX VALUE => . ... LM => LM [ INDEX <- (VALUE %Int 256) ] 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. .. code-block:: k syntax UnStackOp ::= "ISZERO" | "NOT" // ------------------------------------- rule ISZERO 0 => 1 ~> #push ... rule ISZERO W => 0 ~> #push ... requires W =/=K 0 rule NOT W => ~Word W ~> #push ... syntax BinStackOp ::= "ADD" | "MUL" | "SUB" | "DIV" | "EXP" | "MOD" // ------------------------------------------------------------------- rule ADD W0 W1 => W0 +Word W1 ~> #push ... rule MUL W0 W1 => W0 *Word W1 ~> #push ... rule SUB W0 W1 => W0 -Word W1 ~> #push ... rule DIV W0 W1 => W0 /Word W1 ~> #push ... rule EXP W0 W1 => W0 ^Word W1 ~> #push ... rule MOD W0 W1 => W0 %Word W1 ~> #push ... syntax BinStackOp ::= "SDIV" | "SMOD" // ------------------------------------- rule SDIV W0 W1 => W0 /sWord W1 ~> #push ... rule SMOD W0 W1 => W0 %sWord W1 ~> #push ... syntax TernStackOp ::= "ADDMOD" | "MULMOD" // ------------------------------------------ rule ADDMOD W0 W1 W2 => (W0 +Int W1) %Word W2 ~> #push ... rule MULMOD W0 W1 W2 => (W0 *Int W1) %Word W2 ~> #push ... syntax BinStackOp ::= "BYTE" | "SIGNEXTEND" // ------------------------------------------- rule BYTE INDEX W => byte(INDEX, W) ~> #push ... rule SIGNEXTEND W0 W1 => signextend(W0, W1) ~> #push ... syntax BinStackOp ::= "AND" | "EVMOR" | "XOR" // --------------------------------------------- rule AND W0 W1 => W0 &Word W1 ~> #push ... rule EVMOR W0 W1 => W0 |Word W1 ~> #push ... rule XOR W0 W1 => W0 xorWord W1 ~> #push ... syntax BinStackOp ::= "LT" | "GT" | "EQ" // ---------------------------------------- rule LT W0 W1 => 1 ~> #push ... requires W0 LT W0 W1 => 0 ~> #push ... requires W0 >=Int W1 rule GT W0 W1 => 1 ~> #push ... requires W0 >Int W1 rule GT W0 W1 => 0 ~> #push ... requires W0 <=Int W1 rule EQ W0 W1 => 1 ~> #push ... requires W0 ==Int W1 rule EQ W0 W1 => 0 ~> #push ... requires W0 =/=Int W1 syntax BinStackOp ::= "SLT" | "SGT" // ----------------------------------- rule SLT W0 W1 => W0 s #push ... rule SGT W0 W1 => W1 s #push ... syntax BinStackOp ::= "SHA3" // ---------------------------- rule SHA3 MEMSTART MEMWIDTH => keccak(#range(LM, MEMSTART, MEMWIDTH)) ~> #push ... LM Local State ~~~~~~~~~~~ These operators make queries about the current execution state. .. code-block:: k syntax NullStackOp ::= "PC" | "GAS" | "GASPRICE" | "GASLIMIT" // ------------------------------------------------------------- rule PC => PCOUNT ~> #push ... PCOUNT rule GAS => GAVAIL ~> #push ... GAVAIL rule GASPRICE => GPRICE ~> #push ... GPRICE rule GASLIMIT => GLIMIT ~> #push ... GLIMIT syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" // ------------------------------------------------------------------------- rule COINBASE => CB ~> #push ... CB rule TIMESTAMP => TS ~> #push ... TS rule NUMBER => NUMB ~> #push ... NUMB rule DIFFICULTY => DIFF ~> #push ... DIFF syntax NullStackOp ::= "ADDRESS" | "ORIGIN" | "CALLER" | "CALLVALUE" // -------------------------------------------------------------------- rule ADDRESS => ACCT ~> #push ... ACCT rule ORIGIN => ORG ~> #push ... ORG rule CALLER => CL ~> #push ... CL rule CALLVALUE => CV ~> #push ... CV syntax NullStackOp ::= "MSIZE" | "CODESIZE" // ------------------------------------------- rule MSIZE => 32 *Word MU ~> #push ... MU rule CODESIZE => #sizeWordStack(PGM) ~> #push ... PGM syntax TernStackOp ::= "CODECOPY" // --------------------------------- rule CODECOPY MEMSTART PGMSTART WIDTH => . ... PGM LM => LM [ MEMSTART := PGM [ PGMSTART .. WIDTH ] ] syntax UnStackOp ::= "BLOCKHASH" // -------------------------------- rule BLOCKHASH N => #if N >=Int HI orBool HI -Int 256 >Int N #then 0 #else #parseHexWord(Keccak256(Int2String(N))) #fi ~> #push ... HI VMTESTS rule BLOCKHASH N => #blockhash(HASHES, N, HI -Int 1, 0) ~> #push ... HI HASHES NORMAL 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. .. code-block:: k syntax NullStackOp ::= "JUMPDEST" // --------------------------------- rule JUMPDEST => . ... syntax UnStackOp ::= "JUMP" // --------------------------- rule JUMP DEST => . ... _ => DEST syntax BinStackOp ::= "JUMPI" // ----------------------------- rule JUMPI DEST I => . ... _ => DEST requires I =/=K 0 rule JUMPI DEST 0 => . ... PCOUNT => PCOUNT +Int 1 ``STOP`` and ``RETURN`` ~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: k syntax NullStackOp ::= "STOP" // ----------------------------- rule STOP => #end ... syntax BinStackOp ::= "RETURN" // ------------------------------ rule EXECMODE RETURN RETSTART RETWIDTH => #end ... _ => #range(LM, RETSTART, RETWIDTH) LM Call Data ~~~~~~~~~ These operators query about the current ``CALL*`` state. .. code-block:: k syntax NullStackOp ::= "CALLDATASIZE" // ------------------------------------- rule CALLDATASIZE => #sizeWordStack(CD) ~> #push ... CD syntax UnStackOp ::= "CALLDATALOAD" // ----------------------------------- rule CALLDATALOAD DATASTART => #asWord(CD [ DATASTART .. 32 ]) ~> #push ... CD syntax TernStackOp ::= "CALLDATACOPY" // ------------------------------------- rule CALLDATACOPY MEMSTART DATASTART DATAWIDTH => . ... LM => LM [ MEMSTART := CD [ DATASTART .. DATAWIDTH ] ] CD Log Operations ~~~~~~~~~~~~~~ .. code-block:: k syntax BinStackOp ::= LogOp syntax LogOp ::= LOG ( Int ) // ---------------------------- rule LOG(N) MEMSTART MEMWIDTH => . ... ACCT WS => #drop(N, WS) LM ... (.List => ListItem({ ACCT | #take(N, WS) | #range(LM, MEMSTART, MEMWIDTH) })) 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. .. code-block:: k syntax UnStackOp ::= "BALANCE" // ------------------------------ rule BALANCE ACCT => BAL ~> #push ... ACCT BAL ... rule BALANCE ACCT => #newAccount ACCT ~> 0 ~> #push ... ACCTS requires notBool ACCT in_keys(ACCTS) syntax UnStackOp ::= "EXTCODESIZE" // ---------------------------------- rule EXTCODESIZE ACCT => #sizeWordStack(CODE) ~> #push ... ACCT CODE ... rule EXTCODESIZE ACCT => #newAccount ACCT ~> 0 ~> #push ... ACCTS 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")? .. code-block:: k syntax QuadStackOp ::= "EXTCODECOPY" // ------------------------------------ rule EXTCODECOPY ACCT MEMSTART PGMSTART WIDTH => . ... LM => LM [ MEMSTART := PGM [ PGMSTART .. WIDTH ] ] ACCT PGM ... rule EXTCODECOPY ACCT MEMSTART PGMSTART WIDTH => #newAccount ACCT ... ACCTS requires notBool ACCT in_keys(ACCTS) Account Storage Operations ~~~~~~~~~~~~~~~~~~~~~~~~~~ These operations interact with the account storage. .. code-block:: k syntax UnStackOp ::= "SLOAD" // ---------------------------- rule SLOAD INDEX => 0 ~> #push ... ACCT ACCT STORAGE ... requires notBool INDEX in_keys(STORAGE) rule SLOAD INDEX => VALUE ~> #push ... ACCT ACCT ... INDEX |-> VALUE ... ... syntax BinStackOp ::= "SSTORE" // ------------------------------ rule SSTORE INDEX VALUE => . ... ACCT ACCT ... (INDEX |-> (OLD => VALUE)) ... ... R => #ifInt OLD =/=Int 0 andBool VALUE ==Int 0 #then R +Word Rsstoreclear < SCHED > #else R #fi SCHED rule SSTORE INDEX VALUE => . ... ACCT ACCT STORAGE => STORAGE [ INDEX <- VALUE ] ... requires notBool (INDEX in_keys(STORAGE)) Call Operations ~~~~~~~~~~~~~~~ The various ``CALL*`` (and other inter-contract control flow) operations will be desugared into these ``InternalOp``\ s. - The ``callLog`` is used to store the ``CALL*``/``CREATE`` operations so that we can compare them against the test-set. .. code-block:: k 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. .. code-block:: k 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 #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception ... CD ACCT BAL ... requires VALUE >Int BAL orBool CD >=Int 1024 rule #checkCall ACCT VALUE => . ... CD ACCT BAL ... requires notBool (VALUE >Int BAL orBool CD >=Int 1024) rule #call ACCTFROM ACCTTO ACCTCODE GLIMIT VALUE APPVALUE ARGS => #callWithCode ACCTFROM ACCTTO (0 |-> #precompiled(ACCTCODE)) .WordStack GLIMIT VALUE APPVALUE ARGS ... requires ACCTCODE >Int 0 andBool ACCTCODE <=Int 4 rule #call ACCTFROM ACCTTO ACCTCODE GLIMIT VALUE APPVALUE ARGS => #callWithCode ACCTFROM ACCTTO #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) CODE GLIMIT VALUE APPVALUE ARGS ... SCHED ACCTCODE CODE requires notBool (ACCTCODE >Int 0 andBool ACCTCODE <=Int 4) rule #call ACCTFROM ACCTTO ACCTCODE GLIMIT VALUE APPVALUE ARGS => #callWithCode ACCTFROM ACCTTO .Map .WordStack GLIMIT VALUE APPVALUE ARGS ... ACCTS 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 EXECMODE #mkCall ACCTFROM ACCTTO CODE BYTES GLIMIT VALUE APPVALUE ARGS => #initVM ~> #if EXECMODE ==K VMTESTS #then #end #else #execute #fi ... ... (.Set => #ifSet EXECMODE ==K VMTESTS #then SetItem({ ACCTTO | GLIMIT | VALUE | ARGS }) #else .Set #fi) CD => CD +Int 1 _ => ARGS _ => APPVALUE _ => ACCTTO _ => GLIMIT _ => ACCTFROM _ => CODE _ => BYTES syntax KItem ::= "#initVM" // -------------------------- rule #initVM => . ... _ => 0 _ => 0 _ => .WordStack _ => .WordStack _ => .Map syntax KItem ::= "#return" Int Int // ---------------------------------- rule #exception ~> #return _ _ => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... rule EXECMODE #end ~> #return RETSTART RETWIDTH => #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT GAVAIL syntax InternalOp ::= "#refund" Int | "#setLocalMem" Int Int WordStack // ------------------------------------------------------ rule #refund G => . ... GAVAIL => GAVAIL +Int G rule #setLocalMem START WIDTH WS => . ... LM => LM [ START := #take(minInt(WIDTH, #sizeWordStack(WS)), WS) ] For each ``CALL*`` operation, we make a corresponding call to ``#call`` and a state-change to setup the custom parts of the calling environment. .. code-block:: k syntax CallOp ::= "CALL" // ------------------------ rule 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 ... SCHED ACCTFROM LM ACCTS GAVAIL syntax CallOp ::= "CALLCODE" // ---------------------------- rule 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 ... SCHED ACCTFROM LM ACCTS GAVAIL syntax CallSixOp ::= "DELEGATECALL" // ----------------------------------- rule 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 ... SCHED ACCTFROM ACCTAPPFROM VALUE LM ACCTS GAVAIL 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. .. code-block:: k syntax InternalOp ::= "#create" Int Int Int Int WordStack | "#mkCreate" Int Int WordStack Int Int | "#checkCreate" Int Int // -------------------------------------------- rule #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #pushSubstate ~> #exception ... CD ACCT BAL ... requires VALUE >Int BAL orBool CD >=Int 1024 rule #checkCreate ACCT VALUE => . ... EXECMODE CD ACCT BAL NONCE => #ifInt EXECMODE ==K VMTESTS #then NONCE #else NONCE +Int 1 #fi ... ... ACCT |-> (EMPTY => #if EXECMODE ==K VMTESTS #then EMPTY #else false #fi) ... 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 EXECMODE #mkCreate ACCTFROM ACCTTO INITCODE GAVAIL VALUE => #initVM ~> #if EXECMODE ==K VMTESTS #then #end #else #execute #fi ... SCHED ACCT => ACCTTO OLDGAVAIL => GAVAIL _ => #asMapOpCodes(#dasmOpCodes(INITCODE, SCHED)) _ => INITCODE _ => ACCTFROM ... (.Set => #ifSet EXECMODE ==K VMTESTS #then SetItem({ 0 | OLDGAVAIL +Int GAVAIL | VALUE | INITCODE }) #else .Set #fi) CD => CD +Int 1 _ => .WordStack _ => VALUE ACCTTO NONCE => #ifInt Gemptyisnonexistent << SCHED >> #then NONCE +Int 1 #else NONCE #fi ... ... ACCTTO |-> (EMPTY => #if Gemptyisnonexistent << SCHED >> #then false #else EMPTY #fi) ... syntax KItem ::= "#codeDeposit" Int | "#mkCodeDeposit" Int | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- rule #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... rule EXECMODE #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => #if EXECMODE ==K VMTESTS #then . #else Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas #fi ~> #finishCodeDeposit ACCT OUT ... EXECMODE SCHED OUT => .WordStack requires #sizeWordStack(OUT) <=Int maxCodeSize < SCHED > rule #mkCodeDeposit ACCT => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... SCHED OUT => .WordStack requires #sizeWordStack(OUT) >Int maxCodeSize < SCHED > rule #finishCodeDeposit ACCT OUT => #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate ~> #refund GAVAIL ~> ACCT ~> #push ... EXECMODE GAVAIL ACCT _ => OUT ... ... ACCT |-> (EMPTY => #if OUT =/=K .WordStack #then false #else EMPTY #fi) ... rule #exception ~> #finishCodeDeposit ACCT _ => #popCallStack ~> #if EXECMODE ==K VMTESTS #then #popWorldState #else #dropWorldState #fi ~> #dropSubstate ~> #refund GAVAIL ~> ACCT ~> #push ... EXECMODE GAVAIL FRONTIER rule #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER ``CREATE`` will attempt to ``#create`` the account using the initialization code and cleans up the result with ``#codeDeposit``. .. code-block:: k syntax TernStackOp ::= "CREATE" // ------------------------------- rule 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) ... SCHED ACCT GAVAIL => #ifInt Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi LM ACCT NONCE ... ``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. .. code-block:: k syntax UnStackOp ::= "SELFDESTRUCT" // ----------------------------------- rule SELFDESTRUCT ACCTTO => #transferFunds ACCT ACCTTO BALFROM ~> #end ... SCHED ACCT SDS (.Set => SetItem(ACCT)) RF => #ifInt ACCT in SDS #then RF #else RF +Word Rselfdestruct < SCHED > #fi ACCT BALFROM ... requires ACCT =/=Int ACCTTO rule SELFDESTRUCT ACCT => #end ... SCHED ACCT SDS (.Set => SetItem(ACCT)) RF => #ifInt ACCT in SDS #then RF #else RF +Word Rselfdestruct < SCHED > #fi ACCT BALFROM => 0 NONCE CODE ... ... ACCT |-> (_ => NONCE ==Int 0 andBool CODE ==K .WordStack) ... Precompiled Contracts ===================== - ``#precompiled`` is a placeholder for the 4 pre-compiled contracts at addresses 1 through 4. .. code-block:: k syntax NullStackOp ::= PrecompiledOp syntax PrecompiledOp ::= #precompiled ( Int ) [function] // -------------------------------------------------------- rule #precompiled(1) => ECREC rule #precompiled(2) => SHA256 rule #precompiled(3) => RIP160 rule #precompiled(4) => ID - ``ECREC`` performs ECDSA public key recovery. - ``SHA256`` performs the SHA2-257 hash function. - ``RIP160`` performs the RIPEMD-160 hash function. - ``ID`` is the identity function (copies input to output). .. code-block:: k syntax PrecompiledOp ::= "ECREC" // -------------------------------- rule ECREC => #end ... DATA _ => #ecrec(#sender(#unparseByteStack(DATA [ 0 .. 32 ]), #asWord(DATA [ 32 .. 32 ]), #unparseByteStack(DATA [ 64 .. 32 ]), #unparseByteStack(DATA [ 96 .. 32 ]))) syntax WordStack ::= #ecrec ( Account ) [function] // -------------------------------------------------- rule #ecrec(.Account) => .WordStack rule #ecrec(N:Int) => #padToWidth(32, #asByteStack(N)) syntax PrecompiledOp ::= "SHA256" // --------------------------------- rule SHA256 => #end ... DATA _ => #parseHexBytes(Sha256(#unparseByteStack(DATA))) syntax PrecompiledOp ::= "RIP160" // --------------------------------- rule RIP160 => #end ... DATA _ => #padToWidth(32, #parseHexBytes(RipEmd160(#unparseByteStack(DATA)))) syntax PrecompiledOp ::= "ID" // ----------------------------- rule ID => #end ... DATA _ => DATA 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). - ``#memory`` computes the new memory size given the old size and next operator (with its arguments). - ``#memoryUsageUpdate`` is the function ``M`` in appendix H of the yellowpaper which helps track the memory used. .. code-block:: k 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``. .. code-block:: k 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). - ``#gasExec`` loads all the relevant surronding state and uses that to compute the intrinsic execution gas of each opcode. .. code-block:: k syntax InternalOp ::= #gasExec ( Schedule , OpCode ) // ---------------------------------------------------- rule #gasExec(SCHED, SSTORE INDEX VALUE) => Csstore(SCHED, VALUE, #lookup(STORAGE, INDEX)) ... ACCT ACCT STORAGE ... rule #gasExec(SCHED, EXP W0 0) => Gexp < SCHED > ... rule #gasExec(SCHED, EXP W0 W1) => Gexp < SCHED > +Int (Gexpbyte < SCHED > *Int (1 +Int (log256Int(W1)))) ... requires W1 =/=K 0 rule #gasExec(SCHED, CALLDATACOPY _ _ WIDTH) => Gverylow < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... rule #gasExec(SCHED, CODECOPY _ _ WIDTH) => Gverylow < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... rule #gasExec(SCHED, EXTCODECOPY _ _ _ WIDTH) => Gextcodecopy < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) ... rule #gasExec(SCHED, LOG(N) _ WIDTH) => (Glog < SCHED > +Int (Glogdata < SCHED > *Int WIDTH) +Int (N *Int Glogtopic < SCHED >)) ... rule #gasExec(SCHED, CALL GCAP ACCTTO VALUE _ _ _ _) => Ccall(SCHED, ACCTTO, ACCTS, GCAP, GAVAIL, VALUE) ... ACCTS GAVAIL rule #gasExec(SCHED, CALLCODE GCAP _ VALUE _ _ _ _) => Ccall(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, VALUE) ... ACCTFROM ACCTS GAVAIL rule #gasExec(SCHED, DELEGATECALL GCAP _ _ _ _ _) => Ccall(SCHED, ACCTFROM, ACCTS, GCAP, GAVAIL, 0) ... ACCTFROM ACCTS GAVAIL rule #gasExec(SCHED, SELFDESTRUCT ACCTTO) => Cselfdestruct(SCHED, ACCTTO, ACCTS, BAL) ... ACCTS ACCTFROM ACCTFROM BAL ... rule #gasExec(SCHED, CREATE _ _ _) => Gcreate < SCHED > ... rule #gasExec(SCHED, SHA3 _ WIDTH) => Gsha3 < SCHED > +Int (Gsha3word < SCHED > *Int (WIDTH up/Int 32)) ... rule #gasExec(SCHED, JUMPDEST) => Gjumpdest < SCHED > ... rule #gasExec(SCHED, SLOAD _) => Gsload < SCHED > ... // Wzero rule #gasExec(SCHED, STOP) => Gzero < SCHED > ... rule #gasExec(SCHED, RETURN _ _) => Gzero < SCHED > ... // Wbase rule #gasExec(SCHED, ADDRESS) => Gbase < SCHED > ... rule #gasExec(SCHED, ORIGIN) => Gbase < SCHED > ... rule #gasExec(SCHED, CALLER) => Gbase < SCHED > ... rule #gasExec(SCHED, CALLVALUE) => Gbase < SCHED > ... rule #gasExec(SCHED, CALLDATASIZE) => Gbase < SCHED > ... rule #gasExec(SCHED, CODESIZE) => Gbase < SCHED > ... rule #gasExec(SCHED, GASPRICE) => Gbase < SCHED > ... rule #gasExec(SCHED, COINBASE) => Gbase < SCHED > ... rule #gasExec(SCHED, TIMESTAMP) => Gbase < SCHED > ... rule #gasExec(SCHED, NUMBER) => Gbase < SCHED > ... rule #gasExec(SCHED, DIFFICULTY) => Gbase < SCHED > ... rule #gasExec(SCHED, GASLIMIT) => Gbase < SCHED > ... rule #gasExec(SCHED, POP _) => Gbase < SCHED > ... rule #gasExec(SCHED, PC) => Gbase < SCHED > ... rule #gasExec(SCHED, MSIZE) => Gbase < SCHED > ... rule #gasExec(SCHED, GAS) => Gbase < SCHED > ... // Wverylow rule #gasExec(SCHED, ADD _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SUB _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, NOT _) => Gverylow < SCHED > ... rule #gasExec(SCHED, LT _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, GT _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SLT _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SGT _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, EQ _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, ISZERO _) => Gverylow < SCHED > ... rule #gasExec(SCHED, AND _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, EVMOR _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, XOR _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, BYTE _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, CALLDATALOAD _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MLOAD _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MSTORE _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MSTORE8 _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, PUSH(_, _)) => Gverylow < SCHED > ... rule #gasExec(SCHED, DUP(_) _) => Gverylow < SCHED > ... rule #gasExec(SCHED, SWAP(_) _) => Gverylow < SCHED > ... // Wlow rule #gasExec(SCHED, MUL _ _) => Glow < SCHED > ... rule #gasExec(SCHED, DIV _ _) => Glow < SCHED > ... rule #gasExec(SCHED, SDIV _ _) => Glow < SCHED > ... rule #gasExec(SCHED, MOD _ _) => Glow < SCHED > ... rule #gasExec(SCHED, SMOD _ _) => Glow < SCHED > ... rule #gasExec(SCHED, SIGNEXTEND _ _) => Glow < SCHED > ... // Wmid rule #gasExec(SCHED, ADDMOD _ _ _) => Gmid < SCHED > ... rule #gasExec(SCHED, MULMOD _ _ _) => Gmid < SCHED > ... rule #gasExec(SCHED, JUMP _) => Gmid < SCHED > ... // Whigh rule #gasExec(SCHED, JUMPI _ _) => Ghigh < SCHED > ... rule #gasExec(SCHED, EXTCODESIZE _) => Gextcodesize < SCHED > ... rule #gasExec(SCHED, BALANCE _) => Gbalance < SCHED > ... rule #gasExec(SCHED, BLOCKHASH _) => Gblockhash < SCHED > ... // Precompiled rule #gasExec(_, ECREC) => 3000 ... rule #gasExec(_, SHA256) => 60 +Int 12 *Int (#sizeWordStack(DATA) up/Int 32) ... DATA rule #gasExec(_, RIP160) => 600 +Int 120 *Int (#sizeWordStack(DATA) up/Int 32) ... DATA rule #gasExec(_, ID) => 15 +Int 3 *Int (#sizeWordStack(DATA) up/Int 32) ... DATA 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. .. code-block:: k 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 > 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=`` when calling ``krun`` (the available ```` 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. .. code-block:: k 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. .. code-block:: k 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 ~~~~~~~~~~~~~~~~ .. code-block:: k 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 .. code:: cpp struct EVMSchedule { EVMSchedule(): tierStepGas(std::array{{0, 2, 3, 5, 8, 10, 20, 0}}) {} EVMSchedule(bool _efcd, bool _hdc, unsigned const& _txCreateGas): exceptionalFailedCodeDeposit(_efcd), haveDelegateCall(_hdc), tierStepGas(std::array{{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 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 ~~~~~~~~~~~~~~~~~ .. code-block:: k syntax Schedule ::= "FRONTIER" // ------------------------------ rule Gtxcreate < FRONTIER > => 21000 rule SCHEDCONST < FRONTIER > => SCHEDCONST < DEFAULT > requires SCHEDCONST =/=K Gtxcreate rule SCHEDFLAG << FRONTIER >> => SCHEDFLAG << DEFAULT >> .. code:: cpp static const EVMSchedule FrontierSchedule = EVMSchedule(false, false, 21000); Homestead Schedule ~~~~~~~~~~~~~~~~~~ .. code-block:: k syntax Schedule ::= "HOMESTEAD" // ------------------------------- rule SCHEDCONST < HOMESTEAD > => SCHEDCONST < DEFAULT > rule SCHEDFLAG << HOMESTEAD >> => SCHEDFLAG << DEFAULT >> .. code:: cpp static const EVMSchedule HomesteadSchedule = EVMSchedule(true, true, 53000); EIP150 Schedule ~~~~~~~~~~~~~~~ .. code-block:: k 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 ) .. code:: cpp 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 ~~~~~~~~~~~~~~~ .. code-block:: k 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 ) .. code:: cpp static const EVMSchedule EIP158Schedule = [] { EVMSchedule schedule = EIP150Schedule; schedule.expByteGas = 50; schedule.eip158Mode = true; schedule.maxCodeSize = 0x6000; return schedule; }(); Byzantium Schedule ~~~~~~~~~~~~~~~~~~ .. code-block:: k syntax Schedule ::= "BYZANTIUM" // ------------------------------- rule SCHEDCONST < BYZANTIUM > => SCHEDCONST < EIP158 > rule SCHEDFLAG << BYZANTIUM >> => SCHEDFLAG << EIP158 >> .. code:: cpp static const EVMSchedule ByzantiumSchedule = [] { EVMSchedule schedule = EIP158Schedule; schedule.haveRevert = true; schedule.haveReturnData = true; schedule.haveStaticCall = true; schedule.blockRewardOverwrite = {3 * ether}; return schedule; }(); Constantinople Schedule ~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: k syntax Schedule ::= "CONSTANTINOPLE" // ------------------------------------ rule Gblockhash < CONSTANTINOPLE > => 800 rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > requires SCHEDCONST =/=K Gblockhash rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> .. code:: cpp 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. - ``#dasmOpCodes`` interperets ``WordStack`` as an ``OpCodes``. - ``#dasmPUSH`` handles the case of a ``PushOp``. - ``#dasmOpCode`` interperets a ``Int`` as an ``OpCode``. .. code-block:: k 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