View on GitHub

evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)

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.

    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"
 // ----------------------------------------------------------
    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"

Ending Codes

These additional status codes indicate that execution has ended in some non-exceptional way.

    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.

    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.

    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