diff --git a/Makefile b/Makefile index 579e60eacd..01607cba78 100644 --- a/Makefile +++ b/Makefile @@ -36,7 +36,7 @@ export LUA_PATH .PHONY: all clean clean-submodules distclean install uninstall \ deps all-deps llvm-deps haskell-deps repo-deps system-deps k-deps ocaml-deps plugin-deps libsecp256k1 libff \ - build build-ocaml build-java build-node build-kore split-tests \ + build build-ocaml build-java build-node build-llvm build-web3 split-tests \ defn java-defn ocaml-defn node-defn haskell-defn llvm-defn \ test test-all test-conformance test-slow-conformance test-all-conformance \ test-vm test-slow-vm test-all-vm test-bchain test-slow-bchain test-all-bchain \ @@ -166,13 +166,17 @@ build-node: $(node_kompiled) build-haskell: $(haskell_kompiled) build-llvm: $(llvm_kompiled) +build-web3: MAIN_MODULE=WEB3 +build-web3: MAIN_DEFN_FILE=web3 +build-web3: $(llvm_kompiled) + # Tangle definition from *.md files concrete_tangle:=.k:not(.node):not(.symbolic),.standalone,.concrete symbolic_tangle:=.k:not(.node):not(.concrete),.standalone,.symbolic node_tangle:=.k:not(.standalone):not(.symbolic),.node,.concrete -k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k +k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k EXTRA_K_FILES+=$(MAIN_DEFN_FILE).k ALL_K_FILES:=$(k_files) $(EXTRA_K_FILES) diff --git a/data.md b/data.md index a79991f3b7..597c202dad 100644 --- a/data.md +++ b/data.md @@ -816,6 +816,18 @@ We need to interperet a `ByteArray` as a `String` again so that we can call `Kec // ----------------------------------------------- rule #padByte( S ) => S requires lengthString(S) ==K 2 rule #padByte( S ) => "0" +String S requires lengthString(S) ==K 1 + + syntax String ::= #unparseQuantity( Int ) [function] + // ---------------------------------------------------- + rule #unparseQuantity( I ) => "0x" +String Base2String(I, 16) + + syntax String ::= #unparseData ( Int, Int ) [function] + | #unparseDataByteArray ( ByteArray ) [function] + // ---------------------------------------------------------------- + rule #unparseData( _, 0 ) => "0x" + rule #unparseData( DATA, LENGTH ) => #unparseDataByteArray(#padToWidth(LENGTH,#asByteStack(DATA))) + + rule #unparseDataByteArray( DATA ) => replaceFirst(Base2String(#asInteger(#asByteStack(1) ++ DATA), 16), "1", "0x") ``` Recursive Length Prefix (RLP) diff --git a/kevm b/kevm index 04416bbb22..54b61f1bbb 100755 --- a/kevm +++ b/kevm @@ -67,6 +67,10 @@ run_search() { run_krun --search --pattern "$search_pattern" "$@" } +run_web3() { + run_krun -cCHAINID="$cCHAINID" -pCHAINID='printf %s' "$@" +} + run_klab() { local run_mode klab_log @@ -140,6 +144,7 @@ if [[ "$run_command" == 'help' ]]; then $0 kast [--backend (ocaml|java)] * $0 prove [--backend (java|haskell)] * -m $0 search [--backend (java|haskell)] * + $0 web3 [--backend (llvm)] * $0 klab-run * $0 klab-prove * -m $0 klab-view @@ -149,6 +154,7 @@ if [[ "$run_command" == 'help' ]]; then $0 kast : Parse an EVM program and output it in a supported format $0 prove : Run an EVM K proof $0 search : Search for a K pattern in an EVM program execution + $0 web3 : Run version of semantics which understand Web3 RPC (**UNDER CONSTRUCTION**) $0 klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read $0 klab-view : View the statelog associated with a given program or spec @@ -181,6 +187,7 @@ run_file="$1" ; shift cMODE="\`${MODE:-NORMAL}\`(.KList)" cSCHEDULE="\`${SCHEDULE:-BYZANTIUM}_EVM\`(.KList)" +cCHAINID="#token(\"${CHAINID:-28346}\",\"Int\")" case "$run_command-$backend" in @@ -190,6 +197,7 @@ case "$run_command-$backend" in interpret-@(ocaml|llvm) ) run_interpret "$@" ;; prove-@(java|haskell) ) run_prove "$@" ;; search-@(java|haskell) ) run_search "$@" ;; + web3-@(llvm) ) run_web3 "$@" ;; klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;; klab-view-java ) view_klab "$@" ;; *) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;; diff --git a/web3.md b/web3.md new file mode 100644 index 0000000000..21d9c57e85 --- /dev/null +++ b/web3.md @@ -0,0 +1,169 @@ +Web3 RPC JSON Handler +==================== + +```k +requires "evm.k" + +module WEB3 + imports EVM + imports EVM-DATA + + configuration + + + + $CHAINID:Int + + + "" + 0 + "" + [ .JSONList ] + + .List + + + 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 J:JSON REST:EthereumSimulation => #loadRPCCall J ~> REST ... + rule J:JSON => #loadRPCCall J ... + + syntax KItem ::= "#loadRPCCall" JSON + // ------------------------------------ + rule #loadRPCCall J:JSON => #runRPCCall ... + _ => #getString("jsonrpc", J) + _ => #getInt ("id" , J) + _ => #getString("method" , J) + _ => #getJSON ("params" , J) + + syntax KItem ::= #sendResponse ( JSON ) + // --------------------------------------- + rule #sendResponse( J:JSON ) => . ... + ... ( .List => ListItem( J ) ) + + syntax KItem ::= "#runRPCCall" + // ------------------------------ + rule #runRPCCall => #net_version ... + "net_version" + rule #runRPCCall => #web3_clientVersion ... + "web3_clientVersion" + rule #runRPCCall => #eth_gasPrice ... + "eth_gasPrice" + rule #runRPCCall => #eth_blockNumber ... + "eth_blockNumber" + rule #runRPCCall => #eth_accounts ... + "eth_accounts" + rule #runRPCCall => #eth_getBalance ... + "eth_getBalance" + rule #runRPCCall => #eth_getStorageAt ... + "eth_getStorageAt" + rule #runRPCCall => #eth_getCode ... + "eth_getCode" + + syntax KItem ::= "#net_version" + // ------------------------------- + rule #net_version => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : Int2String( CHAINID ) } ) ... + JSONRPC + CALLID + CHAINID + + syntax KItem ::= "#web3_clientVersion" + // ------------------------------- + rule #web3_clientVersion => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : "Firefly RPC/v0.0.1/kevm" } ) ... + JSONRPC + CALLID + + syntax KItem ::= "#eth_gasPrice" + // -------------------------------- + rule #eth_gasPrice => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( PRICE ) } ) ... + JSONRPC + CALLID + PRICE + + syntax KItem ::= "#eth_blockNumber" + // ----------------------------------- + rule #eth_blockNumber => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( BLOCKNUM ) } ) ... + JSONRPC + CALLID + BLOCKNUM + + syntax KItem ::= "#eth_accounts" + // -------------------------------- + rule #eth_accounts => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : [ #acctsToJArray( ACCTS ) ] } ) ... + JSONRPC + CALLID + ACCTS + + 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 #eth_getBalance ... + [ (DATA => #parseHexWord(DATA)), _ ] + + rule #eth_getBalance => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( ACCTBALANCE ) } ) ... + JSONRPC + CALLID + [ DATA, TAG, .JSONList ] + + DATA + ACCTBALANCE + ... + + + syntax KItem ::= "#eth_getStorageAt" + // ------------------------------------ + rule #eth_getStorageAt ... + [ (DATA => #parseHexWord(DATA)), QUANTITY:Int, _ ] + + rule #eth_getStorageAt => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseQuantity( #lookup (STORAGE, QUANTITY) ) } ) ... + JSONRPC + CALLID + [ DATA, QUANTITY, TAG, .JSONList ] + + DATA + STORAGE + ... + + + syntax KItem ::= "#eth_getCode" + // ------------------------------- + rule #eth_getCode ... + [ (DATA => #parseHexWord(DATA)), _ ] + + rule #eth_getCode => #sendResponse( { "id" : CALLID, "jsonrpc" : JSONRPC, "result" : #unparseDataByteArray( CODE ) } ) ... + JSONRPC + CALLID + [ DATA, TAG, .JSONList ] + + DATA + CODE + ... + +endmodule +```