View on GitHub

evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)

EVM Integration with Production Client

Contained in this file is glue code needed in order to enable the ability to use KEVM as a VM for an actual Ethereum node.

```{.k .node} requires “evm.k”

module EVM-NODE imports EVM imports K-REFLECTION imports COLLECTIONS imports BYTES


### State loading operations.

In order to enable scalable execution of transactions on an entire blockchain, it is necessary to avoid serializing/deserializing the entire state of all accounts when constructing the initial configuration for KEVM.
To do this, we assume that accounts not present in the `<accounts>` cell might not exist and need to be loaded on each access.
We also defer loading of storage entries and the actual code byte string until it is needed.
Because the same account may be loaded more than once, implementations of this interface are expected to cache the actual query to the Ethereum client.

-   `#unloaded` represents the code of an account that has not had its code loaded yet. Unloaded code may not be empty.
-   Empty code is detected without lazy evaluation by means of checking the code hash, and therefore will always be represented in the `<code>` cell as `.WordStack`.

```{.k .node}
    syntax AccountCode ::= #unloaded(Int)

```{.k .node} syntax Int ::= #getBalance ( Int ) [function, hook(BLOCKCHAIN.getBalance)] | #getNonce ( Int ) [function, hook(BLOCKCHAIN.getNonce)] | #getCodeHash ( Int ) [function, hook(BLOCKCHAIN.getCodeHash)] // —————————————————————————–

syntax Bool ::= #isCodeEmpty   ( Int ) [function, hook(BLOCKCHAIN.isCodeEmpty)]
              | #accountExists ( Int ) [function, hook(BLOCKCHAIN.accountExists)]  // --------------------------------------------------------------------------------- ```

```{.k .node} rule #loadAccount ACCT => . ... ACCTS (.Set => SetItem(ACCT)) ( .Bag => ACCT #getBalance(ACCT) #if #isCodeEmpty(ACCT) #then .ByteArray #else #unloaded(#getCodeHash(ACCT)) #fi .Map .Map #getNonce(ACCT) ) ... requires notBool ACCT in ACCTS andBool #accountExists(ACCT)

rule <k> #loadAccount ACCT => . ... </k>
     <activeAccounts> ACCTS </activeAccounts>
  requires ACCT in ACCTS orBool notBool #accountExists(ACCT) ```

```{.k .node} syntax Int ::= #getStorageData ( Int , Int ) [function, hook(BLOCKCHAIN.getStorageData)] // —————————————————————————————- rule #lookupStorage ACCT INDEX => . ... ACCT STORAGE => STORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] ORIGSTORAGE => ORIGSTORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] ... requires notBool INDEX in_keys(STORAGE)

rule <k> #lookupStorage ACCT INDEX => . ... </k>
     <account>
       <acctID> ACCT </acctID>
       <storage> STORAGE:Map </storage>
       ...
     </account>
  requires INDEX in_keys(STORAGE)

rule <k> #lookupStorage ACCT _ => . ... </k>
  requires notBool #accountExists(ACCT) ```

```{.k .node} syntax String ::= #getCode ( Int ) [function, hook(BLOCKCHAIN.getCode)] // ———————————————————————– rule #lookupCode ACCT => . ... ACCT #unloaded(_) => #parseByteStackRaw(#getCode(ACCT)) ...

rule <k> #lookupCode ACCT => . ... </k>
     <account>
       <acctID> ACCT </acctID>
       <code> _:ByteArray </code>
       ...
     </account>

rule <k> #lookupCode ACCT => . ... </k>
  requires notBool #accountExists(ACCT) ```

```{.k .node} syntax Int ::= #getBlockhash ( Int ) [function, hook(BLOCKCHAIN.getBlockhash)] // —————————————————————————— rule BLOCKHASH N => #getBlockhash(N) ~> #push ... NORMAL requires N >=Int 0 andBool N <Int 256 rule BLOCKHASH N => 0 ~> #push ... NORMAL requires N <Int 0 orBool N >=Int 256


```{.k .node}
    rule <k> EXTCODEHASH ACCT => HASH ~> #push ... </k>
         <account>
           <acctID> ACCT </acctID>
           <code> #unloaded(HASH) </code>
           <nonce> NONCE </nonce>
           <balance> BAL </balance>
           ...
         </account>

Transaction Execution

```{.k .node} syntax EthereumSimulation ::= runVM ( iscreate: Bool , to: Int , from: Int , code: String , args: String , value: Int , gasprice: Int , gas: Int , beneficiary: Int , difficulty: Int , number: Int , gaslimit: Int , timestamp: Int , unused: String ) [symbol] // ———————————————————————————————————————————————————————- rule (.K => #loadAccount ACCTFROM) ~> runVM(... from: ACCTFROM) ... .Set

rule <k> runVM(true, _, ACCTFROM, _, ARGS, VALUE, GPRICE, GAVAIL, CB, DIFF, NUMB, GLIMIT, TS, _)
      => #loadAccount #newAddr(ACCTFROM, NONCE -Int 1)
      ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE -Int 1) VALUE #parseByteStackRaw(ARGS)
      ~> #codeDeposit #newAddr(ACCTFROM, NONCE -Int 1)
      ~> #endCreate
     ...
     </k>
     <schedule> SCHED </schedule>
     <gasPrice> _ => GPRICE </gasPrice>
     <callGas> _ => GAVAIL </callGas>
     <origin> _ => ACCTFROM </origin>
     <callDepth> _ => -1 </callDepth>
     <coinbase> _ => CB </coinbase>
     <difficulty> _ => DIFF </difficulty>
     <number> _ => NUMB </number>
     <gasLimit> _ => GLIMIT </gasLimit>
     <timestamp> _ => TS </timestamp>
     <account>
       <acctID> ACCTFROM </acctID>
       <nonce> NONCE </nonce>
       ...
     </account>
     <touchedAccounts> _ => SetItem(CB) </touchedAccounts>
     <activeAccounts> ACCTS </activeAccounts>
  requires ACCTFROM in ACCTS

rule <k> runVM(false, ACCTTO, ACCTFROM, _, ARGS, VALUE, GPRICE, GAVAIL, CB, DIFF, NUMB, GLIMIT, TS, _)
      => #loadAccount ACCTTO
      ~> #lookupCode ACCTTO
      ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE #parseByteStackRaw(ARGS) false
      ~> #endVM
     ...
     </k>
     <schedule> SCHED </schedule>
     <gasPrice> _ => GPRICE </gasPrice>
     <callGas> _ => GAVAIL </callGas>
     <origin> _ => ACCTFROM </origin>
     <callDepth> _ => -1 </callDepth>
     <coinbase> _ => CB </coinbase>
     <difficulty> _ => DIFF </difficulty>
     <number> _ => NUMB </number>
     <gasLimit> _ => GLIMIT </gasLimit>
     <timestamp> _ => TS </timestamp>
     <touchedAccounts> _ => SetItem(CB) </touchedAccounts>
     <activeAccounts> ACCTS </activeAccounts>
  requires ACCTFROM in ACCTS ```

```{.k .node} syntax KItem ::= “#endVM” | “#endCreate” // —————————————- rule _:ExceptionalStatusCode #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0 _ => .ByteArray

rule <statusCode> EVMC_REVERT </statusCode>
     <k> #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
     <gas> GAVAIL </gas>

rule <statusCode> EVMC_SUCCESS </statusCode>
     <k> #halt ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 </k>
     <gas> GAVAIL </gas>

rule <k> #endCreate => W ... </k> <wordStack> W : WS </wordStack> ```

Primitive operations expected to exist by the blockchain-k-plugin

```{.k .node} syntax KItem ::= vmResult ( return: String , gas: Int , refund: Int , status: Int , selfdestruct: Set , logs: List , AccountsCell , touched: Set , statusCode: String ) syntax KItem ::= extractConfig() [function, symbol] // ————————————————— rule [[ extractConfig() => vmResult(#unparseByteStack(OUT), GAVAIL, REFUND, STATUS, SD, LOGS, ACCTS , TOUCHED, StatusCode2String(STATUSCODE)) ]] OUT GAVAIL REFUND STATUS:Int SD LOGS ACCTS TOUCHED STATUSCODE


-   `contractBytes` takes the contents of the `<code>` cell and returns its binary representation as a String.

```{.k .node}
    syntax String ::= contractBytes(AccountCode) [function, symbol]
 // ---------------------------------------------------------------
    rule contractBytes(WS) => #unparseByteStack(WS)

The following are expected to exist in the client, but are already defined in [data.md].

{.k .node} endmodule