A := B
:=
is used to define A
as B
.BC
B
B_header
S
S_system
S_machine
P_modify_state
T
T_code
T_data
T_value
T_depth
CALL
s or CREATE
s being executed at present)G
G_rem
G_price
A
A_code_owner
A_tx_sender
A_code_executor
F_apply
CREATE
, CALL
and CALLCODE
. Finally, gas may be charged due to an increase in memory usage.G
is a tuple of 37 scalar values corresponding to the relative costs, in gas, of a number of abstract operations that a transaction may incur. For other tables such as Precompiled contracts
and accounts
, please refer to this document​G_zero
W_zero
G_base
W_base
G_verylow
W_verylow
G_low
W_low
G_mid
W_mid
G_high
W_high
G_blockhash
BLOCKHASH
operationG_extcode
W_extcode
G_balance
BALANCE
operationG_sload
SLOAD
operationG_jumpdest
JUMPDEST
operationG_sset
SSTORE
operation when the storage value is set to nonzero from zeroG_sreset
SSTORE
operation when the storage value remains unchanged at zero or is set to zeroR_sclear
R_selfdestruct
G_selfdestruct
SELFDESTRUCT
operationG_create
CREATE
operationG_codedeposit
CREATE
operation that succeeds in placing code into stateG_call
CALL
operationG_callvalue
CALL
operationW_zero
= {STOP
, RETURN
, REVERT
}W_base
= {ADDRESS
, ORIGIN
, CALLER
, CALLVALUE
, CALLDATASIZE
, CODESIZE
, GASPRICE
, COINBASE
, TIMESTAMP
, NUMBER
, DIFFICULTY
, GASLIMIT
, RETURNDATASIZE
, POP
, PC
, MSIZE
, GAS
}W_verylow
= {ADD
, SUB
, LT
, GT
, SLT
, SGT
, EQ
, ISZERO
, AND
, OR
, XOR
, NOT
, BYTE
, CALLDATALOAD
, MLOAD
, MSTORE
, MSTORE8
, PUSH
, DUP
, SWAP
}W_low
= {MUL
, DIV
, SDIV
, MOD
, SMOD
, SIGNEXTEND
}W_mid
= {ADDMOD
, MULMOD
, JUMP
}W_high
= {JUMPI
}W_extcode
= {EXTCODESIZE
}C
, is defined as follows:C(S_system, S_machine, I) := C_mem(S_machine,i') - C_mem(S_machine, i) +
C_SSTORE(S_system, S_machine)
, if w == SSTORE
G_exp
, if (w == EXP) && (S_machine[1] == 0)
G_exp + G_expbyte x (1 + floor(log_256(S_machine,sp[1])))
,(w == EXP) && (S_machine,sp[1] > 0)
G_verylow + G_copy x ceil(S_machine,sp[2] / 32)
,w == CALLDATACOPY || CODECOPY || RETURNDATACOPY
G_extcode + G_copy x ceil(S_machine,sp[3] / 32)
,w == EXTCODECOPY
G_log + G_logdata x S_machine,sp[1]
,w == LOG0
G_log + G_logdata x S_machine,sp[1] + G_logtopic
,w == LOG1
G_log + G_logdata x S_machine,sp[1] + 2 x G_logtopic
,w == LOG2
G_log + G_logdata x S_machine,sp[1] + 3 x G_logtopic
,w == LOG3
G_log + G_logdata x S_machine,sp[1] + 4 x G_logtopic
,w == LOG4
C_CALL(S_system, S_machine)
,w == CALL || CALLCODE || DELEGATECALL
C_SELFDESTRUCT(S_system, S_machine)
,w == SELFDESTRUCT
G_create
, if w == CREATE
G_sha3 + G_sha3word x ceil(s[1] / 32)
,w == SHA3
G_jumpdest
, if w == JUMPDEST
G_sload
, if w == SLOAD
G_zero
, if w
in W_zero
G_base
, if w
in W_base
G_verylow
, if w
in W_verylow
G_low
, if w
in W_low
G_mid
, if w
in W_mid
G__high</sub>
, if w
in W_high
G_extcode
, if w
in W_extcode
G_balance
, if w == BALANCE
G_blockhash
, if w == BLOCKHASH
w
isT_code[S_machine,pc]
,S_machine,pc < length(T_code)
STOP
, otherwiseC_mem(a) := G_memory x a + floor(a^2 / 512)
C_CALL
, C_SELFDESTRUCT
and C_SSTORE
which will be described in the future.S_system
, the remaining gas for computation G_rem
, and the information I
that the execution agent provides. I
is a tuple defined as shown below:I := (B_header, T_code, T_depth, T_value, T_data, A_tx_sender, A_code_executor, A_code_owner, G_price, P_modify_state)
F_apply
, which can compute the resultant state S_system'
, the remaining gas G_rem'
, the accrued substate A
and the resultant output O_result
when given these definitions. For the present context, we will define it as follows:(S_system', G_rem', A, O_result) = F_apply(S_system, G_rem, I)
A
, the accrued substate, is defined as the tuple of the suicides set Set_suicide
, the log series L
, the touched accounts Set_touched_accounts
and the refunds G_refund
:A := (Set_suicide, L, Set_touched_accounts, G_refund)
F_apply
will be modeled as an iterative progression of the pair comprising the full system state S_system
and the machine state S_machine
. Formally, we define it recursively with a function X
that uses an iterator function O
(which defines the result of a single cycle of the state machine) together with functions Z
, which determines if the present state is an exceptional halted machine state, and H
, which specifies the output data of an instruction if and only if the present state is a normal halted machine state.()
, is not equal to the empty set, denoted as Set_empty
; this is important when interpreting the output of H
, which evaluates to Set_empty
when execution is to continue but to a series (potentially empty) when execution should halt.F_apply(S_machine, G_rem, I, T) := (S_system', S_machine,g', A, o)
(S_system', S_machine,g', A, ..., o) := X((S_system, S_machine, A^0, I))
S_machine,g := G_rem
S_machine,pc := 0
S_machine,memory := (0, 0, ...)
S_machine,i := 0
S_machine,stack := ()
S_machine,o := ()
X((S_system, S_machine, A, I)) :=
(Set_empty, S_machine, A^0, I, Set_empty)
if Z(S_system, S_machine, I)
(Set_empty, S_machine', A^0, I, o)
if w = REVERT
O(S_system, S_machine, A, I) · o
if o != Set_empty
X(O(S_system, S_machine, A, I))
otherwiseo := H(S_machine, I)
(a, b, c, d) · e := (a, b, c, d, e)
S_machine' := S_machine
exceptS_machine,g' := S_machine,g - C(S_system, S_machine, I)
F_apply
, weS_machine,g'
from theS_machine'
.X
is thus cycled (recursively here, but implementations are generally expected to use a simple iterative loop) until either Z
becomes true, indicating that the present state is exceptional and that the machine must be halted and any changes are discarded, or until H
becomes a series (rather than the empty set), indicating that the machine has reached a controlled halt.S_machine
is defined as a tuple (g, pc, memory, i, stack)
, which represent the available gas, the program counter pc
(64-bit unsigned integer), the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents S_machine,memory
are a series of zeroes of size 2^256.ADD
) should be interpreted as their numeric equivalents; the full table of instructions and their specifics is given in the Instruction Set section.Z
, H
and O
, we define w
as the current operation to be executed:w := T_code[S_machine,pc]
if S_machine,pc < len(T_code)
w :=STOP
otherwise