Add Remote ULM-Wasm Build

Makefile

@@ -48,16 +48,29 @@ ULM_WASM_SRC=$(wildcard $(ULM_WASM_SRC_DIR)/*.md $(ULM_WASM_SRC_DIR)/data/*.k)
 
 ULM_WASM_COMPILER_TARGET=$(ULM_BUILD_DIR)/ulm-contract-compiler
 
+## Depedencies
+
 ULM_KRYPTO_DIR=$(ULM_DEP_DIR)/plugin
 ULM_KRYPTO_LIB=krypto.a
 ULM_KRYPTO_TARGET=$(ULM_LIB_DIR)/$(ULM_KRYPTO_LIB)
 
-ULM_HOOKS_CLONE_DIR=$(ULM_DEP_DIR)/ulm
-ULM_HOOKS_DIR=$(ULM_HOOKS_CLONE_DIR)/kllvm
+ULM_KEVM_DIR=$(ULM_DEP_DIR)/evm-semantics
+ULM_KEVM_BUILD_DIR=$(ULM_KEVM_DIR)/libkevm
+ULM_KEVM_BRANCH=ulm
+ULM_KEVM_LIB=libkevm.so
+ULM_KEVM_TARGET=$(ULM_LIB_DIR)/$(ULM_KEVM_LIB)
+
+ULM_CLONE_DIR=$(ULM_DEP_DIR)/ulm
+ULM_HOOKS_DIR=$(ULM_CLONE_DIR)/kllvm
 ULM_HOOKS_SRC=ulm_kllvm.cpp ulm_hooks.cpp ulm_kllvm_c.cpp
 ULM_HOOKS_LIB=libulmkllvm.so
 ULM_HOOKS_TARGET=$(ULM_LIB_DIR)/$(ULM_HOOKS_LIB)
 
+ULM_SRC_GETH=$(shell find "$(ULM_CLONE_DIR)/op-geth" -type f -a '(' -name '*.cpp' -or -name '*.h' -or -name '*.go' ')')
+ULM_SRC_HOOKS=$(shell find "$(ULM_CLONE_DIR)/kllvm" -type f -a '(' -name '*.cpp' -or -name '*.h' -or -name '*.k' ')')
+
+ULM_GETH_TARGET=$(ULM_BUILD_DIR)/geth
+
 ### ULM Crypto Plugin
 
 $(ULM_KRYPTO_DIR)/.git:
@@ -69,20 +82,20 @@ $(ULM_KRYPTO_DIR)/.git:
 
 $(ULM_KRYPTO_TARGET): | $(ULM_KRYPTO_DIR)/.git
 	@mkdir -p $(ULM_LIB_DIR)
-	$(if $(ULM_CXX), CXX=$(ULM_CXX)) make -C "$(ULM_KRYPTO_DIR)" build
+	$(if $(ULM_CXX), CXX=$(ULM_CXX)) $(MAKE) -C "$(ULM_KRYPTO_DIR)" build
 	cp "$(ULM_KRYPTO_DIR)/build/krypto/lib/krypto.a" "$(ULM_LIB_DIR)"
 
 .PHONY: ulm-krypto-build
 ulm-krypto-build: $(ULM_KRYPTO_TARGET)
 
 ### ULM Hooks
 
-$(ULM_HOOKS_CLONE_DIR)/.git:
+$(ULM_CLONE_DIR)/.git:
 	@mkdir -p $(ULM_DEP_DIR)
 	cd $(ULM_DEP_DIR); \
 	  git clone --depth 1 https://github.com/pi-squared-inc/ulm
 
-$(ULM_HOOKS_TARGET): | $(ULM_HOOKS_CLONE_DIR)/.git
+$(ULM_HOOKS_TARGET): $(ULM_SRC_HOOKS) | $(ULM_CLONE_DIR)/.git
 	@mkdir -p $(ULM_LIB_DIR)
 	cd $(ULM_HOOKS_DIR); \
 	  $(CXX) -shared -o "$(ULM_HOOKS_LIB)" $(ULM_HOOKS_SRC) -I "$(ULM_KF_INCLUDE_DIR)" -I "$(ULM_KF_INCLUDE_DIR)/kllvm" \
@@ -92,6 +105,60 @@ $(ULM_HOOKS_TARGET): | $(ULM_HOOKS_CLONE_DIR)/.git
 .PHONY: ulm-hooks-build
 ulm-hooks-build: $(ULM_HOOKS_TARGET)
 
+### KEVM
+
+$(ULM_KEVM_DIR)/.git:
+	@mkdir -p $(ULM_DEP_DIR)
+	cd $(ULM_DEP_DIR); \
+	  git clone --depth 1 https://github.com/pi-squared-inc/evm-semantics -b $(ULM_KEVM_BRANCH) evm-semantics
+
+$(ULM_KEVM_TARGET): $(ULM_KRYPTO_TARGET) $(ULM_HOOKS_TARGET) | $(ULM_KEVM_DIR)/.git
+	@mkdir -p $(ULM_LIB_DIR)
+	kompile "$(ULM_KEVM_DIR)/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md" \
+	--main-module EVM \
+	--syntax-module EVM \
+	-I "$(ULM_KEVM_DIR)/kevm-pyk/src/kevm_pyk/kproj/evm-semantics" \
+	-I "$(ULM_KRYPTO_DIR)" \
+	-I "$(ULM_HOOKS_DIR)" \
+	--md-selector 'k & ! symbolic' \
+	--hook-namespaces 'JSON KRYPTO ULM' \
+	--backend llvm \
+	-O3 \
+	-ccopt -std=c++20 \
+	-ccopt -lssl \
+	-ccopt -lcrypto \
+	-ccopt -lsecp256k1 \
+	-ccopt "$(ULM_LIB_DIR)/krypto.a" \
+	-ccopt -Wno-deprecated-declarations \
+	--output-definition "$(ULM_KEVM_BUILD_DIR)" \
+	--type-inference-mode simplesub \
+	--verbose \
+	-ccopt -L"$(ULM_LIB_DIR)" \
+	-ccopt -lulmkllvm \
+	--llvm-kompile-type library \
+	--llvm-kompile-output libkevm.so \
+	-ccopt -g \
+	--llvm-mutable-bytes \
+	-ccopt "$(ULM_HOOKS_DIR)/lang/ulm_language_entry.cpp" \
+	-ccopt -I"$(ULM_HOOKS_DIR)" \
+	-ccopt -DULM_LANG_ID=kevm \
+	--llvm-hidden-visibility \
+	-ccopt -fPIC \
+	-ccopt -shared
+	cp "$(ULM_KEVM_BUILD_DIR)"/libkevm.so "$(ULM_LIB_DIR)"
+
+.PHONY: kevm-build
+kevm-build: $(ULM_KEVM_TARGET)
+
+### ULM
+
+$(ULM_GETH_TARGET): $(ULM_KEVM_TARGET) $(ULM_SRC_HOOKS) $(ULM_SRC_GETH) | $(ULM_CLONE_DIR)/.git
+	cd $(ULM_CLONE_DIR)/op-geth && $(MAKE)
+	cp $(ULM_CLONE_DIR)/op-geth/build/bin/geth $(ULM_BUILD_DIR)
+
+.PHONY: ulm-build
+ulm-build: $(ULM_GETH_TARGET)
+
 ### ULM Wasm
 
 ULM_WASM_TYPE = $(if $(ULM_TEST),main,library)

README.md

@@ -145,6 +145,12 @@ To locally build the ULM-integrated version of the semantics, run:
 make ULM_TEST=1 ulm-wasm
 ```
 
+To build the remote ULM-integrated version of the semantics, run:
+
+```sh
+make ulm-wasm
+```
+
 ### Media and documents
 
 The `media/` directory contains presentations and reports about about KWasm.
@@ -171,6 +177,8 @@ The target `test` contains all the currently passing tests.
 make test
 ```
 
+### ULM-Integrated Wasm Local Testing
+
 To execute the Wasm VM locally, you can use the `wasm` Poetry script from the repo root as follows:
 
 ```sh
@@ -183,6 +191,25 @@ For example, after locally building the ULM-integrated Wasm, the local build of
 poetry -C pykwasm run wasm ./build/wasm pykwasm/src/tests/integration/binary/basic-features.wat -gas:Int=0 -create:Bool=false -entry:String=init
 ```
 
+### ULM-Integrated Wasm Remote Testing
+
+To execute the Wasm VM remotely, you need to build the ULM by running:
+
+```sh
+make ulm-build
+```
+
+Then, you can start the ULM locally and load the Wasm VM into it by running:
+
+```sh
+./scripts/run-dev-ulm &
+./scripts/ulm-load-lang ./build/lib/libwasm.so
+```
+
+Then, you can invoke Wasm programs by doing the following:
+
+**TODO**
+
 Resources
 ---------
 

scripts/run-dev-ulm

@@ -0,0 +1,20 @@
+#!/bin/bash
+set -eu
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+[ -n "${DEBUG+x}"   ] && FLAGS+=" --debugger"
+set +u
+export LD_LIBRARY_PATH="$SCRIPT_DIR/../build/lib:$LD_LIBRARY_PATH"
+set -u
+FLAGS=(--dev --allow-insecure-unlock\
+       --gcmode archive\
+       --dev.period 5\
+       --http\
+       --http.addr 0.0.0.0\
+       --http.corsdomain '*'\
+       --http.vhosts '*'\
+       --http.api debug,personal,web3,eth,net,txpool\
+       --ws\
+       --ws.addr 0.0.0.0\
+       --ws.origins '*')
+[ -n "${VERBOSE+x}" ] && set -x
+"$SCRIPT_DIR/../build/geth" "${FLAGS[@]}" "$@"

scripts/ulm-load-lang

@@ -0,0 +1,7 @@
+#!/bin/bash
+set -eu
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+[ -n "${VERBOSE+x}" ] && set -x
+[ $# -ne 1 ] && { echo "usage: $(basename $0) <path/to/ulm-lang-lib.so>"; echo "       NOTE: requires a running ULM server"; exit 1; }
+LANG=$1
+curl -X POST -H "Content-Type: application/json" --data '{"jsonrpc":"2.0","method":"debug_loadLanguage","params":["'"$LANG"'"],"id":1}' localhost:8545