Equations
- EvmYul.instReprOperationType = { reprPrec := EvmYul.reprOperationType✝ }
Stop and Arithmetic Operations
- STOP
{τ : OperationType}
: SAOp τ
Stop: halts program execution δ: 0 ; α : 0
- ADD
{τ : OperationType}
: SAOp τ
ADD: adds two stack values. δ: 2 ; α : 1
- MUL
{τ : OperationType}
: SAOp τ
MUL: multiplies two stack values. δ: 2 ; α : 1
- SUB
{τ : OperationType}
: SAOp τ
SUB: subtracts two stack values. δ: 2 ; α : 1
- DIV
{τ : OperationType}
: SAOp τ
DIV: divides two stack values. δ: 2 ; α: 1
- SDIV
{τ : OperationType}
: SAOp τ
SDIV: signed integer division δ: 2 ; α: 1
- MOD
{τ : OperationType}
: SAOp τ
MOD: Modulo remainder operation δ: 2 ; α: 1
- SMOD
{τ : OperationType}
: SAOp τ
SMOD: signed integer remainder δ: 2 ; α: 1
- ADDMOD
{τ : OperationType}
: SAOp τ
ADDMOD: addition modulo operation δ: 3 ; α: 1
- MULMOD
{τ : OperationType}
: SAOp τ
MULMOD: multiplication modulo operation δ: 3 ; α: 1
- EXP
{τ : OperationType}
: SAOp τ
EXP: Exponential operation δ:2 ; α: 1
- SIGNEXTEND
{τ : OperationType}
: SAOp τ
SIGNEXTEND: Extend length of two's complement signed integer δ: 2 ; α: 1
Instances For
Equations
- EvmYul.Operation.instReprSAOp = { reprPrec := EvmYul.Operation.reprSAOp✝ }
Comparison & Bitwise Logic Operations
- LT
{τ : OperationType}
: CBLOp τ
LT: less than comparison δ: 2 ; α: 1
- GT
{τ : OperationType}
: CBLOp τ
GT: greater than comparison δ: 2 ; α: 1
- SLT
{τ : OperationType}
: CBLOp τ
SLT: signed less-than comparison δ:2 ; α: 1
- SGT
{τ : OperationType}
: CBLOp τ
SGT: signed greater-than comparison δ: 2 ; α: 1
- EQ
{τ : OperationType}
: CBLOp τ
EQ: equality test δ:2 ; α : 1
- ISZERO
{τ : OperationType}
: CBLOp τ
ISZERO: simple not operation δ: 1 ; α : 1
- AND
{τ : OperationType}
: CBLOp τ
AND: bitwise and δ:2 ; α: 1
- OR
{τ : OperationType}
: CBLOp τ
OR: bitwise or δ: 2 ; α: 1
- XOR
{τ : OperationType}
: CBLOp τ
XOR: bitwise xor δ: 2 ; α: 1
- NOT
{τ : OperationType}
: CBLOp τ
NOT: bitwise not δ:1 ; α: 1
- BYTE
{τ : OperationType}
: CBLOp τ
BYTE: retrieve single byte from a word δ:2 ; α:1
- SHL
{τ : OperationType}
: CBLOp τ
SHL: shift left operation δ:2 ; α: 1
- SHR
{τ : OperationType}
: CBLOp τ
SHR: logical shift right operation δ:2 ; α:1
- SAR
{τ : OperationType}
: CBLOp τ
SAR: arithmetical shift right operation δ:2 ; α:1
Instances For
Equations
- EvmYul.Operation.instReprCBLOp = { reprPrec := EvmYul.Operation.reprCBLOp✝ }
Keccak operation.
- KECCAK256
{τ : OperationType}
: KOp τ
KECCAK256: compute KECCAK256 hash δ:2 ; α: 1
Instances For
Equations
- EvmYul.Operation.instReprKOp = { reprPrec := EvmYul.Operation.reprKOp✝ }
Environment Information.
- ADDRESS
{τ : OperationType}
: EOp τ
ADDRESS: get the address of current executing account δ:0 ; α: 1
- BALANCE
{τ : OperationType}
: EOp τ
BALANCE: get the balance of an input account δ:1 ; α: 1
- ORIGIN
{τ : OperationType}
: EOp τ
ORIGIN: get execution origination address δ:0 ; α: 1
- CALLER
{τ : OperationType}
: EOp τ
CALLER: returns the caller address δ: 0 ; α: 1
- CALLVALUE
{τ : OperationType}
: EOp τ
CALLVALUE: get deposited value by the instruction / transaction responsible for this execution. δ: 0 ; α: 1
- CALLDATALOAD
{τ : OperationType}
: EOp τ
CALLDATALOAD: get input data of current environment δ: 1 ; α: 1
- CALLDATASIZE
{τ : OperationType}
: EOp τ
CALLDATASIZE: get size of input data in current environment δ: 0 ; α: 1
- CALLDATACOPY
{τ : OperationType}
: EOp τ
CALLDATACOPY: copy input data from environment to memory δ: 3 ; α: 0
- GASPRICE
{τ : OperationType}
: EOp τ
CODESIZE: get the size of code running in current environment δ:0 ; α: 1
- CODESIZE
{τ : OperationType}
: EOp τ
CODECOPY: Copy code running in current environment to memory δ: 3 ; α: 0
- CODECOPY
{τ : OperationType}
: EOp τ
GASPRICE: Gas price in current execution environment δ: 0 ; α: 1
- EXTCODESIZE
{τ : OperationType}
: EOp τ
EXTCODESIZE: get the size of an account's code δ:1 ; α: 1
- EXTCODECOPY
{τ : OperationType}
: EOp τ
EXTCODECOPY: copy an account's code to memory δ: 4 ; α: 0
- RETURNDATASIZE
{τ : OperationType}
: EOp τ
RETURNDATASIZE: get the size of output data from the previous call from the current environment. δ: 0 ; α: 1
- RETURNDATACOPY
{τ : OperationType}
: EOp τ
RETURNDATACOPY: copy output data from previous call to memory δ: 3 ; α: 0
- EXTCODEHASH
{τ : OperationType}
: EOp τ
EXTCODEHASH: get hash of an account's code δ: 1 ; α: 1
Instances For
Equations
- EvmYul.Operation.instReprEOp = { reprPrec := EvmYul.Operation.reprEOp✝ }
Block Information.
- BLOCKHASH
{τ : OperationType}
: BOp τ
BLOCKHASH: get the hash of one of the 256 most recent blocks δ:1 ; α: 1
- COINBASE
{τ : OperationType}
: BOp τ
COINBASE: get current's block beneficiary address δ: 0 ; α: 1
- TIMESTAMP
{τ : OperationType}
: BOp τ
TIMESTAMP: get current block's timestamp δ: 0 ; α: 1
- NUMBER
{τ : OperationType}
: BOp τ
NUMBER: get current block's number δ: 0 ; α: 1
- PREVRANDAO {τ : OperationType} : BOp τ
- GASLIMIT
{τ : OperationType}
: BOp τ
GASLIMIT: get the gas limit for the current block δ: 0 ; α: 1
- CHAINID
{τ : OperationType}
: BOp τ
CHAINID: returns the chainid, β δ: 0 ; α: 1
- SELFBALANCE
{τ : OperationType}
: BOp τ
SELFBALANCE: get the balance of the current executing account δ: 0 ; α: 1
- BASEFEE {τ : OperationType} : BOp τ
- BLOBHASH {τ : OperationType} : BOp τ
- BLOBBASEFEE {τ : OperationType} : BOp τ
Instances For
Equations
- EvmYul.Operation.instReprBOp = { reprPrec := EvmYul.Operation.reprBOp✝ }
Stack, Memory, Storage and Flow Operations
- POP
{τ : OperationType}
: SMSFOp τ
POP: remove an item from the stack δ: 1 ; α: 0
- MLOAD
{τ : OperationType}
: SMSFOp τ
MLOAD: load word from memory δ: 1 ; α: 1
- MSTORE
{τ : OperationType}
: SMSFOp τ
MSTORE: save word in memory δ: 2 ; α: 0
- SLOAD
{τ : OperationType}
: SMSFOp τ
SLOAD: load word from storage δ: 1 ; α: 1
- SSTORE
{τ : OperationType}
: SMSFOp τ
SSTORE: Save word to storage δ:2 ; α: 0
- MSTORE8
{τ : OperationType}
: SMSFOp τ
MSTORE8: save byte in memory δ: 2 ; α: 0
- JUMP : SMSFOp OperationType.EVM
JUMP: modify program counter δ:1 ; α: 0
- JUMPI : SMSFOp OperationType.EVM
JUMPI: conditionally modify program counter δ: 2 ; α: 0
- PC : SMSFOp OperationType.EVM
PC: get program counter before increment δ: 0 ; α: 1
- MSIZE
{τ : OperationType}
: SMSFOp τ
MSIZE: get the size of active memory in bytes δ: 0 ; α: 1
- GAS
{τ : OperationType}
: SMSFOp τ
GAS: get the amount of available gas δ: 0 ; α: 1
- JUMPDEST : SMSFOp OperationType.EVM
JUMPDEST: mark a valid destination for jumps δ: 0 ; α: 0
- TLOAD
{τ : OperationType}
: SMSFOp τ
EIP-1153 https://eips.ethereum.org/EIPS/eip-1153 TLOAD: load word from transient memory δ: 1 ; α: 1
- TSTORE
{τ : OperationType}
: SMSFOp τ
EIP-1153 https://eips.ethereum.org/EIPS/eip-1153 TSTORE: Save word to transient memory δ: 2 ; α: 0
- MCOPY
{τ : OperationType}
: SMSFOp τ
EIPS-5656 MCOPY: copy memory areas δ: 3 ; α: 0
Instances For
Equations
- EvmYul.Operation.instReprSMSFOp = { reprPrec := EvmYul.Operation.reprSMSFOp✝ }
Push operations.
PUSH0 : pushes 0 to stack.
δ: 0 ; α: 1
PUSHn : pushes n bytes to stack. δ: 0 ; α: 1
- PUSH0 : POp
- PUSH1 : POp
- PUSH2 : POp
- PUSH3 : POp
- PUSH4 : POp
- PUSH5 : POp
- PUSH6 : POp
- PUSH7 : POp
- PUSH8 : POp
- PUSH9 : POp
- PUSH10 : POp
- PUSH11 : POp
- PUSH12 : POp
- PUSH13 : POp
- PUSH14 : POp
- PUSH15 : POp
- PUSH16 : POp
- PUSH17 : POp
- PUSH18 : POp
- PUSH19 : POp
- PUSH20 : POp
- PUSH21 : POp
- PUSH22 : POp
- PUSH23 : POp
- PUSH24 : POp
- PUSH25 : POp
- PUSH26 : POp
- PUSH27 : POp
- PUSH28 : POp
- PUSH29 : POp
- PUSH30 : POp
- PUSH31 : POp
- PUSH32 : POp
Instances For
Equations
- EvmYul.Operation.instReprPOp = { reprPrec := EvmYul.Operation.reprPOp✝ }
Equations
- EvmYul.Operation.instReprDOp = { reprPrec := EvmYul.Operation.reprDOp✝ }
Exchange Operations.
SWAPn: swaps the 1st and nth element of the stack. δ: n + 1 ; α: n + 1
- SWAP1 : ExOp
- SWAP2 : ExOp
- SWAP3 : ExOp
- SWAP4 : ExOp
- SWAP5 : ExOp
- SWAP6 : ExOp
- SWAP7 : ExOp
- SWAP8 : ExOp
- SWAP9 : ExOp
- SWAP10 : ExOp
- SWAP11 : ExOp
- SWAP12 : ExOp
- SWAP13 : ExOp
- SWAP14 : ExOp
- SWAP15 : ExOp
- SWAP16 : ExOp
Instances For
Equations
- EvmYul.Operation.instReprExOp = { reprPrec := EvmYul.Operation.reprExOp✝ }
Logging Operations.
LOGn: append log record with n topics. δ: n + 2 ; α : 0
- LOG0 {τ : OperationType} : LOp τ
- LOG1 {τ : OperationType} : LOp τ
- LOG2 {τ : OperationType} : LOp τ
- LOG3 {τ : OperationType} : LOp τ
- LOG4 {τ : OperationType} : LOp τ
Instances For
Equations
- EvmYul.Operation.instReprLOp = { reprPrec := EvmYul.Operation.reprLOp✝ }
System Operations.
- CREATE
{τ : OperationType}
: SOp τ
CREATE: create a new account with associated code δ: 3 ; α: 1
- CALL
{τ : OperationType}
: SOp τ
CALL: message call into an account δ: 7 ; α: 1
- CALLCODE
{τ : OperationType}
: SOp τ
CALLCODE: message call into this account with an alternative account's code δ: 7 ; α: 1
- RETURN
{τ : OperationType}
: SOp τ
RETURN: Halt execution returning output data δ: 2 ; α: 0
- DELEGATECALL
{τ : OperationType}
: SOp τ
DELEGATECALL: message call into this account with an alternative account's code but persisting the current values for sender and value δ: 6 ; α: 1
- CREATE2
{τ : OperationType}
: SOp τ
CREATE2: create a new account with associated code δ: 4 ; α: 1
- STATICCALL
{τ : OperationType}
: SOp τ
STATICCALL: static message call into an account δ: 6 ; α: 1
- REVERT
{τ : OperationType}
: SOp τ
REVERT: halt execution reverting state changes but returning data and remaining gas δ: 2 ; α: 0
- INVALID
{τ : OperationType}
: SOp τ
INVALID: invalid opcode δ: ∅ ; α: ∅
- SELFDESTRUCT
{τ : OperationType}
: SOp τ
SELFDESTRUCT: halt and send entire balance to target. Deprecated; see EIP-6780 δ: 1 ; α: 0
Instances For
Equations
- EvmYul.Operation.instReprSOp = { reprPrec := EvmYul.Operation.reprSOp✝ }
- StopArith {τ : OperationType} : SAOp τ → Operation τ
- CompBit {τ : OperationType} : CBLOp τ → Operation τ
- Keccak {τ : OperationType} : KOp τ → Operation τ
- Env {τ : OperationType} : EOp τ → Operation τ
- Block {τ : OperationType} : BOp τ → Operation τ
- StackMemFlow {τ : OperationType} : SMSFOp τ → Operation τ
- Push : POp → Operation OperationType.EVM
- Dup : DOp → Operation OperationType.EVM
- Exchange : ExOp → Operation OperationType.EVM
- Log {τ : OperationType} : LOp τ → Operation τ
- System {τ : OperationType} : SOp τ → Operation τ
Instances For
Equations
- EvmYul.instReprOperation = { reprPrec := EvmYul.reprOperation✝ }