Network State
This file represents all the network state present in the EVM. It will incrementally build up to supporting the entire EVM-C API.
module NETWORK
imports STRING-SYNTAX
syntax String ::= StatusCode2String(StatusCode) [function]
// ----------------------------------------------------------
EVM Status Codes
Exceptional Codes
The following codes all indicate that the VM ended execution with an exception, but give details about how.
EVMC_FAILURE
is a catch-all for generic execution failure.EVMC_INVALID_INSTRUCTION
indicates reaching the designatedINVALID
opcode.EVMC_UNDEFINED_INSTRUCTION
indicates that an undefined opcode has been reached.EVMC_OUT_OF_GAS
indicates that execution exhausted the gas supply.EVMC_BAD_JUMP_DESTINATION
indicates aJUMP*
to a non-JUMPDEST
location.EVMC_STACK_OVERFLOW
indicates pushing more than 1024 elements onto the wordstack.EVMC_STACK_UNDERFLOW
indicates popping elements off an empty wordstack.EVMC_CALL_DEPTH_EXCEEDED
indicates that we have executed too deeply a nested sequence ofCALL*
orCREATE
opcodes.EVMC_INVALID_MEMORY_ACCESS
indicates that a bad memory access occured. This can happen when accessing local memory withCODECOPY*
orCALLDATACOPY
, or when accessing return data withRETURNDATACOPY
.EVMC_STATIC_MODE_VIOLATION
indicates that aSTATICCALL
tried to change state. TODO: Avoid_ERROR
suffix that suggests fatal error.EVMC_PRECOMPILE_FAILURE
indicates an errors in the precompiled contracts (eg. invalid points handed to elliptic curve functions).
syntax ExceptionalStatusCode ::= "EVMC_FAILURE"
| "EVMC_INVALID_INSTRUCTION"
| "EVMC_UNDEFINED_INSTRUCTION"
| "EVMC_OUT_OF_GAS"
| "EVMC_BAD_JUMP_DESTINATION"
| "EVMC_STACK_OVERFLOW"
| "EVMC_STACK_UNDERFLOW"
| "EVMC_CALL_DEPTH_EXCEEDED"
| "EVMC_INVALID_MEMORY_ACCESS"
| "EVMC_STATIC_MODE_VIOLATION"
| "EVMC_PRECOMPILE_FAILURE"
| "EVMC_NONCE_EXCEEDED"
// -------------------------------------------------------------
rule StatusCode2String(EVMC_FAILURE) => "EVMC_FAILURE"
rule StatusCode2String(EVMC_INVALID_INSTRUCTION) => "EVMC_INVALID_INSTRUCTION"
rule StatusCode2String(EVMC_UNDEFINED_INSTRUCTION) => "EVMC_UNDEFINED_INSTRUCTION"
rule StatusCode2String(EVMC_OUT_OF_GAS) => "EVMC_OUT_OF_GAS"
rule StatusCode2String(EVMC_BAD_JUMP_DESTINATION) => "EVMC_BAD_JUMP_DESTINATION"
rule StatusCode2String(EVMC_STACK_OVERFLOW) => "EVMC_STACK_OVERFLOW"
rule StatusCode2String(EVMC_STACK_UNDERFLOW) => "EVMC_STACK_UNDERFLOW"
rule StatusCode2String(EVMC_CALL_DEPTH_EXCEEDED) => "EVMC_CALL_DEPTH_EXCEEDED"
rule StatusCode2String(EVMC_INVALID_MEMORY_ACCESS) => "EVMC_INVALID_MEMORY_ACCESS"
rule StatusCode2String(EVMC_STATIC_MODE_VIOLATION) => "EVMC_STATIC_MODE_VIOLATION"
rule StatusCode2String(EVMC_PRECOMPILE_FAILURE) => "EVMC_PRECOMPILE_FAILURE"
rule StatusCode2String(EVMC_NONCE_EXCEEDED) => "EVMC_NONCE_EXCEEDED"
Ending Codes
These additional status codes indicate that execution has ended in some non-exceptional way.
EVMC_SUCCESS
indicates successful end of execution.EVMC_REVERT
indicates that the contract calledREVERT
.
syntax EndStatusCode ::= ExceptionalStatusCode
| "EVMC_SUCCESS"
| "EVMC_REVERT"
// --------------------------------------
rule StatusCode2String(EVMC_SUCCESS) => "EVMC_SUCCESS"
rule StatusCode2String(EVMC_REVERT) => "EVMC_REVERT"
Other Codes
The following codes indicate other non-execution errors with the VM.
EVMC_REJECTED
indicates malformed or wrong-version EVM bytecode.EVMC_INTERNAL_ERROR
indicates some other error that is unrecoverable but not due to the bytecode..StatusCode
is an extra code added for "unset or unknown".
syntax StatusCode ::= EndStatusCode
| "EVMC_REJECTED"
| "EVMC_INTERNAL_ERROR"
| ".StatusCode"
// -----------------------------------
rule StatusCode2String(EVMC_REJECTED) => "EVMC_REJECTED"
rule StatusCode2String(EVMC_INTERNAL_ERROR) => "EVMC_INTERNAL_ERROR"
rule StatusCode2String(.StatusCode) => ""
Client/Network Codes
The following are status codes used to report network state failures to the EVM from the client. These are not present in the EVM-C API.
EVMC_ACCOUNT_ALREADY_EXISTS
indicates that a newly created account already exists.EVMC_BALANCE_UNDERFLOW
indicates an attempt to create an account which already exists.
syntax ExceptionalStatusCode ::= "EVMC_ACCOUNT_ALREADY_EXISTS"
| "EVMC_BALANCE_UNDERFLOW"
// ---------------------------------------------------------
rule StatusCode2String(EVMC_ACCOUNT_ALREADY_EXISTS) => "EVMC_ACCOUNT_ALREADY_EXISTS"
rule StatusCode2String(EVMC_BALANCE_UNDERFLOW) => "EVMC_BALANCE_UNDERFLOW"
endmodule