-
Notifications
You must be signed in to change notification settings - Fork 145
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Start implementing semantics for a Web3 RPC server (#427)
* Skeleton code for Web3 RPC implementation * Implement net_version in web3 * Remove example file * Fix command for kevm interpret * Add top cell and fix formatting * rename web3-json-rpc.md to web3.md * rename WEB3-JSON-RPC to WEB3 * Change control flow to handle multiple calls + optimize * web3.md: Add eth_gasPrice * web3.md: Add eth_blockNumber * web3.md: Add eth_accounts * web3.md: Add eth_getBalance * data.md, web3.md: Add and use handlers for RPC value encodings * data: separate names for different #unparseData * evm, web3: move chainID cell to web3 configuration * web3.md: Fix net_version result format * web3.md: added eth_getStorageAt and eth_getCode * kevm: add run_web3 command * Makefile: add build-web3 target * kevm: no passing CHAINID to kore-json.py, interpreter * web3: formatting * web3: no need to require data * web3.md: Implement web3_clientVersion * web3.md: Implement some getters for JSON sorts
- Loading branch information
Showing
4 changed files
with
195 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,169 @@ | ||
| Web3 RPC JSON Handler | ||
| ==================== | ||
|
|
||
| ```k | ||
| requires "evm.k" | ||
| module WEB3 | ||
| imports EVM | ||
| imports EVM-DATA | ||
| configuration | ||
| <kevm-client> | ||
| <kevm/> | ||
| <blockchain> | ||
| <chainID> $CHAINID:Int </chainID> | ||
| </blockchain> | ||
| <web3request> | ||
| <jsonrpc> "" </jsonrpc> | ||
| <callid> 0 </callid> | ||
| <method> "" </method> | ||
| <params> [ .JSONList ] </params> | ||
| </web3request> | ||
| <web3result> .List </web3result> | ||
| </kevm-client> | ||
| syntax JSON ::= Int | Bool | ||
| | #getJSON ( JSONKey, JSON ) [function] | ||
| // ------------------------------------------------------- | ||
| rule #getJSON( KEY, { KEY : J, _ } ) => J | ||
| rule #getJSON( _, { .JSONList } ) => { .JSONList } | ||
| rule #getJSON( KEY, { KEY2 : _, REST } ) => #getJSON( KEY, { REST } ) | ||
| requires KEY =/=K KEY2 | ||
| syntax Int ::= #getInt ( JSONKey, JSON ) [function] | ||
| // --------------------------------------------------- | ||
| rule #getInt( KEY, { KEY : VALUE:Int, _ } ) => VALUE | ||
| rule #getInt( _ , { .JSONList } ) => 0 // TODO: Need something better for nonexistent key/value | ||
| rule #getInt( KEY, { KEY2 : _, REST } ) => #getInt( KEY, { REST } ) | ||
| requires KEY =/=K KEY2 | ||
| syntax String ::= #getString ( JSONKey, JSON ) [function] | ||
| // --------------------------------------------------------- | ||
| rule #getString( KEY, { KEY : VALUE:String, _ } ) => VALUE | ||
| rule #getString( _ , { .JSONList } ) => "" // TODO: Need something better for nonexistent key/value | ||
| rule #getString( KEY, { KEY2 : _, REST } ) => #getString( KEY, { REST } ) | ||
| requires KEY =/=K KEY2 | ||
| syntax EthereumSimulation ::= List{JSON, " "} | ||
| // --------------------------------------------- | ||
| rule <k> J:JSON REST:EthereumSimulation => #loadRPCCall J ~> REST ... </k> | ||
| rule <k> J:JSON => #loadRPCCall J ... </k> | ||
| syntax KItem ::= "#loadRPCCall" JSON | ||
| // ------------------------------------ | ||
| rule <k> #loadRPCCall J:JSON => #runRPCCall ... </k> | ||
| <jsonrpc> _ => #getString("jsonrpc", J) </jsonrpc> | ||
| <callid> _ => #getInt ("id" , J) </callid> | ||
| <method> _ => #getString("method" , J) </method> | ||
| <params> _ => #getJSON ("params" , J) </params> | ||
| syntax KItem ::= #sendResponse ( JSON ) | ||
| // --------------------------------------- | ||
| rule <k> #sendResponse( J:JSON ) => . ... </k> | ||
| <web3result> ... ( .List => ListItem( J ) ) </web3result> | ||
| syntax KItem ::= "#runRPCCall" | ||
| // ------------------------------ | ||
| rule <k> #runRPCCall => #net_version ... </k> | ||
| <method> "net_version" </method> | ||
| rule <k> #runRPCCall => #web3_clientVersion ... </k> | ||
| <method> "web3_clientVersion" </method> | ||
| rule <k> #runRPCCall => #eth_gasPrice ... </k> | ||
| <method> "eth_gasPrice" </method> | ||
| rule <k> #runRPCCall => #eth_blockNumber ... </k> | ||
| <method> "eth_blockNumber" </method> | ||
| rule <k> #runRPCCall => #eth_accounts ... </k> | ||
| <method> "eth_accounts" </method> | ||
| rule <k> #runRPCCall => #eth_getBalance ... </k> | ||
| <method> "eth_getBalance" </method> | ||
| rule <k> #runRPCCall => #eth_getStorageAt ... </k> | ||
| <method> "eth_getStorageAt" </method> | ||
| rule <k> #runRPCCall => #eth_getCode ... </k> | ||
| <method> "eth_getCode" </method> | ||
| syntax KItem ::= "#net_version" | ||
| // ------------------------------- | ||
| rule <k> #net_version => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : Int2String( CHAINID ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <chainID> CHAINID </chainID> | ||
| syntax KItem ::= "#web3_clientVersion" | ||
| // ------------------------------- | ||
| rule <k> #web3_clientVersion => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : "Firefly RPC/v0.0.1/kevm" } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| syntax KItem ::= "#eth_gasPrice" | ||
| // -------------------------------- | ||
| rule <k> #eth_gasPrice => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( PRICE ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <gasPrice> PRICE </gasPrice> | ||
| syntax KItem ::= "#eth_blockNumber" | ||
| // ----------------------------------- | ||
| rule <k> #eth_blockNumber => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( BLOCKNUM ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <number> BLOCKNUM </number> | ||
| syntax KItem ::= "#eth_accounts" | ||
| // -------------------------------- | ||
| rule <k> #eth_accounts => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : [ #acctsToJArray( ACCTS ) ] } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <activeAccounts> ACCTS </activeAccounts> | ||
| syntax JSONList ::= #acctsToJArray ( Set ) [function] | ||
| // ----------------------------------------------------- | ||
| rule #acctsToJArray( .Set ) => .JSONList | ||
| rule #acctsToJArray( SetItem( ACCT ) ACCTS:Set ) => #unparseData( ACCT, 20 ), #acctsToJArray( ACCTS ) | ||
| syntax KItem ::= "#eth_getBalance" | ||
| // ---------------------------------- | ||
| rule <k> #eth_getBalance ... </k> | ||
| <params> [ (DATA => #parseHexWord(DATA)), _ ] </params> | ||
| rule <k> #eth_getBalance => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( ACCTBALANCE ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <params> [ DATA, TAG, .JSONList ] </params> | ||
| <account> | ||
| <acctID> DATA </acctID> | ||
| <balance> ACCTBALANCE </balance> | ||
| ... | ||
| </account> | ||
| syntax KItem ::= "#eth_getStorageAt" | ||
| // ------------------------------------ | ||
| rule <k> #eth_getStorageAt ... </k> | ||
| <params> [ (DATA => #parseHexWord(DATA)), QUANTITY:Int, _ ] </params> | ||
| rule <k> #eth_getStorageAt => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( #lookup (STORAGE, QUANTITY) ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <params> [ DATA, QUANTITY, TAG, .JSONList ] </params> | ||
| <account> | ||
| <acctID> DATA </acctID> | ||
| <storage> STORAGE </storage> | ||
| ... | ||
| </account> | ||
| syntax KItem ::= "#eth_getCode" | ||
| // ------------------------------- | ||
| rule <k> #eth_getCode ... </k> | ||
| <params> [ (DATA => #parseHexWord(DATA)), _ ] </params> | ||
| rule <k> #eth_getCode => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseDataByteArray( CODE ) } ) ... </k> | ||
| <jsonrpc> JSONRPC </jsonrpc> | ||
| <callid> CALLID </callid> | ||
| <params> [ DATA, TAG, .JSONList ] </params> | ||
| <account> | ||
| <acctID> DATA </acctID> | ||
| <code> CODE </code> | ||
| ... | ||
| </account> | ||
| endmodule | ||
| ``` |