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 designated INVALID 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 a JUMP* 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 of CALL* or CREATE opcodes.
  • EVMC_INVALID_MEMORY_ACCESS indicates that a bad memory access occured. This can happen when accessing local memory with CODECOPY* or CALLDATACOPY, or when accessing return data with RETURNDATACOPY.
  • EVMC_STATIC_MODE_VIOLATION indicates that a STATICCALL 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 called REVERT.
    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

Resources