|
| 1 | +Web3 RPC JSON Handler |
| 2 | +==================== |
| 3 | + |
| 4 | +```k |
| 5 | +requires "evm.k" |
| 6 | +
|
| 7 | +module WEB3 |
| 8 | + imports EVM |
| 9 | + imports EVM-DATA |
| 10 | +
|
| 11 | + configuration |
| 12 | + <kevm-client> |
| 13 | + <kevm/> |
| 14 | + <blockchain> |
| 15 | + <chainID> $CHAINID:Int </chainID> |
| 16 | + </blockchain> |
| 17 | + <web3request> |
| 18 | + <jsonrpc> "" </jsonrpc> |
| 19 | + <callid> 0 </callid> |
| 20 | + <method> "" </method> |
| 21 | + <params> [ .JSONList ] </params> |
| 22 | + </web3request> |
| 23 | + <web3result> .List </web3result> |
| 24 | + </kevm-client> |
| 25 | +
|
| 26 | + syntax JSON ::= Int | Bool |
| 27 | + | #getJSON ( JSONKey, JSON ) [function] |
| 28 | + // ------------------------------------------------------- |
| 29 | + rule #getJSON( KEY, { KEY : J, _ } ) => J |
| 30 | + rule #getJSON( _, { .JSONList } ) => { .JSONList } |
| 31 | + rule #getJSON( KEY, { KEY2 : _, REST } ) => #getJSON( KEY, { REST } ) |
| 32 | + requires KEY =/=K KEY2 |
| 33 | +
|
| 34 | + syntax Int ::= #getInt ( JSONKey, JSON ) [function] |
| 35 | + // --------------------------------------------------- |
| 36 | + rule #getInt( KEY, { KEY : VALUE:Int, _ } ) => VALUE |
| 37 | + rule #getInt( _ , { .JSONList } ) => 0 // TODO: Need something better for nonexistent key/value |
| 38 | + rule #getInt( KEY, { KEY2 : _, REST } ) => #getInt( KEY, { REST } ) |
| 39 | + requires KEY =/=K KEY2 |
| 40 | +
|
| 41 | + syntax String ::= #getString ( JSONKey, JSON ) [function] |
| 42 | + // --------------------------------------------------------- |
| 43 | + rule #getString( KEY, { KEY : VALUE:String, _ } ) => VALUE |
| 44 | + rule #getString( _ , { .JSONList } ) => "" // TODO: Need something better for nonexistent key/value |
| 45 | + rule #getString( KEY, { KEY2 : _, REST } ) => #getString( KEY, { REST } ) |
| 46 | + requires KEY =/=K KEY2 |
| 47 | +
|
| 48 | + syntax EthereumSimulation ::= List{JSON, " "} |
| 49 | + // --------------------------------------------- |
| 50 | + rule <k> J:JSON REST:EthereumSimulation => #loadRPCCall J ~> REST ... </k> |
| 51 | + rule <k> J:JSON => #loadRPCCall J ... </k> |
| 52 | +
|
| 53 | + syntax KItem ::= "#loadRPCCall" JSON |
| 54 | + // ------------------------------------ |
| 55 | + rule <k> #loadRPCCall J:JSON => #runRPCCall ... </k> |
| 56 | + <jsonrpc> _ => #getString("jsonrpc", J) </jsonrpc> |
| 57 | + <callid> _ => #getInt ("id" , J) </callid> |
| 58 | + <method> _ => #getString("method" , J) </method> |
| 59 | + <params> _ => #getJSON ("params" , J) </params> |
| 60 | +
|
| 61 | + syntax KItem ::= #sendResponse ( JSON ) |
| 62 | + // --------------------------------------- |
| 63 | + rule <k> #sendResponse( J:JSON ) => . ... </k> |
| 64 | + <web3result> ... ( .List => ListItem( J ) ) </web3result> |
| 65 | +
|
| 66 | + syntax KItem ::= "#runRPCCall" |
| 67 | + // ------------------------------ |
| 68 | + rule <k> #runRPCCall => #net_version ... </k> |
| 69 | + <method> "net_version" </method> |
| 70 | + rule <k> #runRPCCall => #web3_clientVersion ... </k> |
| 71 | + <method> "web3_clientVersion" </method> |
| 72 | + rule <k> #runRPCCall => #eth_gasPrice ... </k> |
| 73 | + <method> "eth_gasPrice" </method> |
| 74 | + rule <k> #runRPCCall => #eth_blockNumber ... </k> |
| 75 | + <method> "eth_blockNumber" </method> |
| 76 | + rule <k> #runRPCCall => #eth_accounts ... </k> |
| 77 | + <method> "eth_accounts" </method> |
| 78 | + rule <k> #runRPCCall => #eth_getBalance ... </k> |
| 79 | + <method> "eth_getBalance" </method> |
| 80 | + rule <k> #runRPCCall => #eth_getStorageAt ... </k> |
| 81 | + <method> "eth_getStorageAt" </method> |
| 82 | + rule <k> #runRPCCall => #eth_getCode ... </k> |
| 83 | + <method> "eth_getCode" </method> |
| 84 | +
|
| 85 | + syntax KItem ::= "#net_version" |
| 86 | + // ------------------------------- |
| 87 | + rule <k> #net_version => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : Int2String( CHAINID ) } ) ... </k> |
| 88 | + <jsonrpc> JSONRPC </jsonrpc> |
| 89 | + <callid> CALLID </callid> |
| 90 | + <chainID> CHAINID </chainID> |
| 91 | +
|
| 92 | + syntax KItem ::= "#web3_clientVersion" |
| 93 | + // ------------------------------- |
| 94 | + rule <k> #web3_clientVersion => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : "Firefly RPC/v0.0.1/kevm" } ) ... </k> |
| 95 | + <jsonrpc> JSONRPC </jsonrpc> |
| 96 | + <callid> CALLID </callid> |
| 97 | +
|
| 98 | + syntax KItem ::= "#eth_gasPrice" |
| 99 | + // -------------------------------- |
| 100 | + rule <k> #eth_gasPrice => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( PRICE ) } ) ... </k> |
| 101 | + <jsonrpc> JSONRPC </jsonrpc> |
| 102 | + <callid> CALLID </callid> |
| 103 | + <gasPrice> PRICE </gasPrice> |
| 104 | +
|
| 105 | + syntax KItem ::= "#eth_blockNumber" |
| 106 | + // ----------------------------------- |
| 107 | + rule <k> #eth_blockNumber => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( BLOCKNUM ) } ) ... </k> |
| 108 | + <jsonrpc> JSONRPC </jsonrpc> |
| 109 | + <callid> CALLID </callid> |
| 110 | + <number> BLOCKNUM </number> |
| 111 | +
|
| 112 | + syntax KItem ::= "#eth_accounts" |
| 113 | + // -------------------------------- |
| 114 | + rule <k> #eth_accounts => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : [ #acctsToJArray( ACCTS ) ] } ) ... </k> |
| 115 | + <jsonrpc> JSONRPC </jsonrpc> |
| 116 | + <callid> CALLID </callid> |
| 117 | + <activeAccounts> ACCTS </activeAccounts> |
| 118 | +
|
| 119 | + syntax JSONList ::= #acctsToJArray ( Set ) [function] |
| 120 | + // ----------------------------------------------------- |
| 121 | + rule #acctsToJArray( .Set ) => .JSONList |
| 122 | + rule #acctsToJArray( SetItem( ACCT ) ACCTS:Set ) => #unparseData( ACCT, 20 ), #acctsToJArray( ACCTS ) |
| 123 | +
|
| 124 | + syntax KItem ::= "#eth_getBalance" |
| 125 | + // ---------------------------------- |
| 126 | + rule <k> #eth_getBalance ... </k> |
| 127 | + <params> [ (DATA => #parseHexWord(DATA)), _ ] </params> |
| 128 | +
|
| 129 | + rule <k> #eth_getBalance => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( ACCTBALANCE ) } ) ... </k> |
| 130 | + <jsonrpc> JSONRPC </jsonrpc> |
| 131 | + <callid> CALLID </callid> |
| 132 | + <params> [ DATA, TAG, .JSONList ] </params> |
| 133 | + <account> |
| 134 | + <acctID> DATA </acctID> |
| 135 | + <balance> ACCTBALANCE </balance> |
| 136 | + ... |
| 137 | + </account> |
| 138 | +
|
| 139 | + syntax KItem ::= "#eth_getStorageAt" |
| 140 | + // ------------------------------------ |
| 141 | + rule <k> #eth_getStorageAt ... </k> |
| 142 | + <params> [ (DATA => #parseHexWord(DATA)), QUANTITY:Int, _ ] </params> |
| 143 | +
|
| 144 | + rule <k> #eth_getStorageAt => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( #lookup (STORAGE, QUANTITY) ) } ) ... </k> |
| 145 | + <jsonrpc> JSONRPC </jsonrpc> |
| 146 | + <callid> CALLID </callid> |
| 147 | + <params> [ DATA, QUANTITY, TAG, .JSONList ] </params> |
| 148 | + <account> |
| 149 | + <acctID> DATA </acctID> |
| 150 | + <storage> STORAGE </storage> |
| 151 | + ... |
| 152 | + </account> |
| 153 | +
|
| 154 | + syntax KItem ::= "#eth_getCode" |
| 155 | + // ------------------------------- |
| 156 | + rule <k> #eth_getCode ... </k> |
| 157 | + <params> [ (DATA => #parseHexWord(DATA)), _ ] </params> |
| 158 | +
|
| 159 | + rule <k> #eth_getCode => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseDataByteArray( CODE ) } ) ... </k> |
| 160 | + <jsonrpc> JSONRPC </jsonrpc> |
| 161 | + <callid> CALLID </callid> |
| 162 | + <params> [ DATA, TAG, .JSONList ] </params> |
| 163 | + <account> |
| 164 | + <acctID> DATA </acctID> |
| 165 | + <code> CODE </code> |
| 166 | + ... |
| 167 | + </account> |
| 168 | +endmodule |
| 169 | +``` |
0 commit comments