web3 Event loop (#436)

* Makefile: build system for web3 client

* deps/plugin: update submodule

* web3: event loop in evm-semantics

* Dockerfile: tests depend on netcat

* Makefile, tests/web3: add tests for web3 client

* Jenkinsfile: run tests for web3

* Makefile: update to latest option parsing

* web3: fix for json getters

* web3: refactor #sendResponse

* web3: add strategies

* web3: checkRPCCall

* web3: method not found

* deps/k: update submodule

* deps/plugin: update submodule

* web3: better fix for invalid request with invalid id

* Makefile: fix bug

* tests/web3: update output files

* web3: workaround bug in k

* tests/web3: add more tests

* deps/plugin: update submodule

* fix kevm web3

* don't use strategy

* Jenkinsfile: fix make target name

* Dockerfile: missing dependency

* deps/k: update submodule

* web3: formatting

* Makefile: formatting

* tests/web3/get_port: use python3

* kevm: formatting, documentation

Author: dwightguth

Dockerfile

@@ -8,7 +8,7 @@ RUN    apt-get update                                                         \
         libprotobuf-dev libsecp256k1-dev libssl-dev libtool libyaml-dev lld-8 \
         llvm-8-tools make maven opam openjdk-11-jdk pandoc pkg-config         \
         protobuf-compiler python3 python-pygments python-recommonmark         \
-        python-sphinx time zlib1g-dev
+        python-sphinx time zlib1g-dev netcat-openbsd rapidjson-dev
 
 ADD deps/k/haskell-backend/src/main/native/haskell-backend/scripts/install-stack.sh /.install-stack/
 RUN /.install-stack/install-stack.sh

Jenkinsfile

@@ -38,7 +38,7 @@ pipeline {
         stage('Build') {
           steps {
             sh '''
-              make build build-llvm build-haskell build-node -j4
+              make build build-llvm build-haskell build-node build-web3 -j4
             '''
           }
         }
@@ -63,6 +63,15 @@ pipeline {
                 '''
               }
             }
+            stage('Conformance (Web3)') {
+              steps {
+                sh '''
+                  nprocs=$(nproc)
+                  [ "$nprocs" -gt '16' ] && nprocs='16'
+                  make test-web3 -j"$nprocs"
+                '''
+              }
+            }
           }
         }
         stage('Test Proofs (Java)') {

Makefile

@@ -37,9 +37,10 @@ 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-llvm build-web3 split-tests \
-        defn java-defn ocaml-defn node-defn haskell-defn llvm-defn \
+        defn java-defn ocaml-defn node-defn web3-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 \
+        test-web3 \
         test-prove test-klab-prove test-parse test-failure \
         test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search test-interactive-firefly \
         media media-pdf sphinx metropolis-theme
@@ -156,20 +157,18 @@ LLVM_KOMPILE_OPTS:=
 ocaml_kompiled:=$(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE)-kompiled/interpreter
 java_kompiled:=$(DEFN_DIR)/java/$(MAIN_DEFN_FILE)-kompiled/timestamp
 node_kompiled:=$(DEFN_DIR)/vm/kevm-vm
+web3_kompiled:=$(DEFN_DIR)/web3/kevm-client
 haskell_kompiled:=$(DEFN_DIR)/haskell/$(MAIN_DEFN_FILE)-kompiled/definition.kore
 llvm_kompiled:=$(DEFN_DIR)/llvm/$(MAIN_DEFN_FILE)-kompiled/interpreter
 
 build: build-ocaml build-java
 build-ocaml: $(ocaml_kompiled)
 build-java: $(java_kompiled)
 build-node: $(node_kompiled)
+build-web3: $(web3_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
@@ -185,14 +184,16 @@ llvm_files=$(patsubst %, $(DEFN_DIR)/llvm/%, $(ALL_K_FILES))
 java_files=$(patsubst %, $(DEFN_DIR)/java/%, $(ALL_K_FILES))
 haskell_files=$(patsubst %, $(DEFN_DIR)/haskell/%, $(ALL_K_FILES))
 node_files=$(patsubst %, $(DEFN_DIR)/node/%, $(ALL_K_FILES))
-defn_files=$(ocaml_files) $(llvm_file) $(java_files) $(haskell_files) $(node_files)
+web3_files=$(patsubst %, $(DEFN_DIR)/web3/%, $(ALL_K_FILES))
+defn_files=$(ocaml_files) $(llvm_file) $(java_files) $(haskell_files) $(node_files) $(web3_files)
 
 defn: $(defn_files)
 ocaml-defn: $(ocaml_files)
 llvm-defn: $(llvm_files)
 java-defn: $(java_files)
 haskell-defn: $(haskell_files)
 node-defn: $(node_files)
+web3-defn: $(web3_files)
 
 $(DEFN_DIR)/ocaml/%.k: %.md $(TANGLER)
 	@echo "==  tangle: $@"
@@ -219,6 +220,11 @@ $(DEFN_DIR)/node/%.k: %.md $(TANGLER)
 	mkdir -p $(dir $@)
 	pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(node_tangle)" $< > $@
 
+$(DEFN_DIR)/web3/%.k: %.md $(TANGLER)
+	@echo "==  tangle: $@"
+	mkdir -p $(dir $@)
+	pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(node_tangle)" $< > $@
+
 # Java Backend
 
 $(java_kompiled): $(java_files)
@@ -309,13 +315,36 @@ $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/plugin/proto/msg.pb.cc: $(PLUGIN_SUB
 
 $(node_kompiled): $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/interpreter $(libff_out)
 	mkdir -p $(DEFN_DIR)/vm
-	$(K_BIN)/llvm-kompile $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/definition.kore $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/dt library $(PLUGIN_SUBMODULE)/vm-c/main.cpp $(PLUGIN_SUBMODULE)/vm-c/vm.cpp \
+	$(K_BIN)/llvm-kompile $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/definition.kore $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/dt library $(PLUGIN_SUBMODULE)/vm-c/init.cpp $(PLUGIN_SUBMODULE)/vm-c/main.cpp $(PLUGIN_SUBMODULE)/vm-c/vm.cpp \
 	                      $(PLUGIN_SUBMODULE)/plugin-c/*.cpp $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/plugin/proto/msg.pb.cc $(PLUGIN_SUBMODULE)/vm-c/kevm/semantics.cpp -o $@ -g -O2 \
 	                      -I $(PLUGIN_SUBMODULE)/plugin-c/ -I $(DEFN_DIR)/node/$(MAIN_DEFN_FILE)-kompiled/plugin -I $(PLUGIN_SUBMODULE)/vm-c/ -I $(PLUGIN_SUBMODULE)/vm-c/kevm/ -I node/ \
 	                      $(LLVM_KOMPILE_OPTS) \
 	                      -L$(LIBRARY_PATH) \
 	                      -lff -lprotobuf -lgmp $(LINK_PROCPS) -lcryptopp -lsecp256k1
 
+# Web3 Backend
+
+$(DEFN_DIR)/web3/web3-kompiled/interpreter: $(web3_files) $(libff_out)
+	@echo "== kompile: $@"
+	$(K_BIN)/kompile --debug --main-module WEB3 --backend llvm \
+	                 --syntax-module WEB3 $(DEFN_DIR)/web3/web3.k \
+	                 --directory $(DEFN_DIR)/web3 -I $(DEFN_DIR)/web3 \
+	                 --hook-namespaces "KRYPTO BLOCKCHAIN JSON" \
+	                 --iterated \
+	                 $(KOMPILE_OPTS) \
+	                 -ccopt $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp -ccopt $(PLUGIN_SUBMODULE)/client-c/json.cpp \
+	                 -ccopt -L$(LIBRARY_PATH) -ccopt -I -ccopt $(PLUGIN_SUBMODULE)/vm-c \
+	                 -ccopt -lff -ccopt -lcryptopp -ccopt -lsecp256k1 $(addprefix -ccopt ,$(LINK_PROCPS)) -ccopt -g -ccopt -std=c++11 -ccopt -O2
+
+$(web3_kompiled): $(DEFN_DIR)/web3/web3-kompiled/interpreter $(libff_out)
+	mkdir -p $(DEFN_DIR)/web3
+	$(K_BIN)/llvm-kompile $(DEFN_DIR)/web3/web3-kompiled/definition.kore $(DEFN_DIR)/web3/web3-kompiled/dt library $(PLUGIN_SUBMODULE)/vm-c/init.cpp $(PLUGIN_SUBMODULE)/client-c/main.cpp $(PLUGIN_SUBMODULE)/client-c/json.cpp \
+	                      $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp -o $@ -g -O2 \
+	                      -I $(PLUGIN_SUBMODULE)/vm-c/ -I $(PLUGIN_SUBMODULE)/plugin-c/ -I node/ \
+	                      $(LLVM_KOMPILE_OPTS) \
+	                      -L$(LIBRARY_PATH) \
+	                      -lff -lgmp $(LINK_PROCPS) -lcryptopp -lsecp256k1
+
 # LLVM Backend
 
 $(llvm_kompiled): $(llvm_files) $(libff_out)
@@ -390,6 +419,16 @@ tests/%.run-expected: tests/% tests/%.expected
 	    || $(CHECK) tests/$*.expected tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 
+tests/%.run-web3: tests/%.in.json
+	PORT=`tests/web3/get_port.py`;                                                     \
+	    ./kevm web3 -p $$PORT &                                                        \
+	    while ! netcat -z 127.0.0.1 $$PORT; do                                         \
+	        sleep 0.1;                                                                 \
+	    done;                                                                          \
+	    cat $^ | netcat 127.0.0.1 $$PORT -q 0 | diff - tests/$*.out.json; RESULT=$$? ; \
+	    pkill kevm-client -P $$$$ ;                                                    \
+	    [ $$? -eq 0 ]
+
 tests/%.parse: tests/%
 	$(TEST) kast --backend $(TEST_CONCRETE_BACKEND) $< kast > $@-out
 	$(CHECK) $@-expected $@-out
@@ -443,10 +482,14 @@ failing_bchain_tests=$(shell cat tests/failing.$(TEST_CONCRETE_BACKEND))
 all_bchain_tests=$(filter-out $(bad_bchain_tests), $(filter-out $(failing_bchain_tests), $(bchain_tests)))
 quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(all_bchain_tests))
 
+web3_tests=$(wildcard tests/web3/*.in.json)
+
 test-all-bchain: $(all_bchain_tests:=.run)
 test-slow-bchain: $(slow_bchain_tests:=.run)
 test-bchain: $(quick_bchain_tests:=.run)
 
+test-web3: $(web3_tests:.in.json=.run-web3)
+
 # Proof Tests
 
 prove_specs_dir:=tests/specs

deps/k

@@ -68,7 +68,7 @@ run_search() {
 }
 
 run_web3() {
-    run_krun -cCHAINID="$cCHAINID" -pCHAINID='printf %s' "$@"
+    exec -a "$0 web3" ${defn_dir}/web3/kevm-client "$@"
 }
 
 run_klab() {
@@ -144,7 +144,7 @@ if [[ "$run_command" == 'help' ]]; then
                $0 kast       [--backend (ocaml|java)]              <pgm>  <output format> <K arg>*
                $0 prove      [--backend (java|haskell)]            <spec> <K arg>* -m <def_module>
                $0 search     [--backend (java|haskell)]            <pgm>  <pattern> <K arg>*
-               $0 web3       [--backend (llvm)]                    <pgm>  <K arg>*
+               $0 web3       [--backend (llvm)]                    -p <port>
                $0 klab-run                                         <pgm>  <K arg>*
                $0 klab-prove                                       <spec> <K arg>* -m <def_module>
                $0 klab-view                                        <spec>
@@ -164,6 +164,7 @@ if [[ "$run_command" == 'help' ]]; then
                  <interpreter arg> is an argument you want to pass to the derived interpreter.
                  <output format> is the format for Kast to output the term in.
                  <pattern> is the configuration pattern to search for.
+                 <port> is the port to listen on for Web3 JSON RPC requests.
                  <def_module> is the module to take as axioms when doing verification.
 
            klab-view: Make sure that the 'klab/bin' directory is on your PATH to use this option.
@@ -174,6 +175,7 @@ fi
 backend="ocaml"
 [[ ! "$run_command" == 'prove' ]] || backend='java'
 [[ ! "$run_command" =~ klab*   ]] || backend='java'
+[[ ! "$run_command" =~ web3*   ]] || backend='llvm'
 if [[ $# -gt 0 ]] && [[ $1 == '--backend' ]]; then
     backend="$2"
     shift 2
@@ -182,8 +184,10 @@ backend_dir="$defn_dir/$backend"
 [[ ! "$backend" == "ocaml" ]] || eval $(opam config env)
 
 # get the run file
-run_file="$1" ; shift
-[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
+if [[ ! "$run_command" == 'web3' ]]; then
+    run_file="$1" ; shift
+    [[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
+fi
 
 cMODE="\`${MODE:-NORMAL}\`(.KList)"
 cSCHEDULE="\`${SCHEDULE:-BYZANTIUM}_EVM\`(.KList)"

deps/plugin

@@ -0,0 +1,8 @@
+#!/usr/bin/env python3
+import socket
+
+s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+s.bind(('', 0))
+addr = s.getsockname()
+print(str(addr[1]))
+s.close()

kevm

@@ -0,0 +1,6 @@
+{
+  "jsonrpc": "2.0",
+  "id": {},
+  "method": "net_version",
+  "params": []
+}

tests/web3/get_port.py

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}}

tests/web3/invalid_id.in.json

@@ -0,0 +1,6 @@
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": 3,
+  "params": []
+}