diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 8c0731c1..7638cebc 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -39,7 +39,7 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Install Poetry' uses: Gr1N/setup-poetry@v8 @@ -53,16 +53,14 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build Haskell' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build-haskell RELEASE=true -j4' - - name: 'Build Haskell' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build-haskell-kasmer RELEASE=true -j4' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build-haskell' - name: 'Tear down Docker' if: always() run: | @@ -76,22 +74,20 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build RELEASE=true -j4' - - name: 'Install Kmultiversx' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make poetry-install' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build' - name: 'Run Python Unit Tests' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm unittest-python' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make unittest-python' - name: 'Run Simple Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-simple -j6' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-simple -j6' - name: 'Run Mandos Tests' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm mandos-test -j6' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make mandos-test -j6' - name: 'Tear down Docker' if: always() run: | @@ -105,20 +101,18 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build RELEASE=true -j4' - - name: 'Install Kmultiversx' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make poetry-install' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build' - name: 'Run Basic Feature Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-elrond-basic-features -j6' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-elrond-basic-features -j6' - name: 'Run Alloc Feature Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-elrond-alloc-features -j6' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-elrond-alloc-features -j6' - name: 'Tear down Docker' if: always() run: | @@ -132,22 +126,20 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build RELEASE=true -j4' - - name: 'Install Kmultiversx' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make poetry-install' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build' - name: 'Run Adder Contract Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-elrond-adder' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-elrond-adder' - name: 'Run Crowdfunding ESDT Contract Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-elrond-crowdfunding-esdt' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-elrond-crowdfunding-esdt' - name: 'Run Multisig Contract Test' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-elrond-multisig' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-elrond-multisig' - name: 'Tear down Docker' if: always() run: | @@ -161,18 +153,16 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build RELEASE=true -j4' - - name: 'Install Kmultiversx' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make poetry-install' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build' - name: 'Run Custom Contract Tests' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm test-custom-contracts' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-custom-contracts' - name: 'Tear down Docker' if: always() run: | @@ -185,22 +175,18 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: elrond-semantics-ci-${{ github.sha }} - name: 'Build Kasmer' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build-kasmer -j4' - - name: 'Install Kmultiversx' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make poetry-install' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make build-kasmer' - name: 'Run tests' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c \ - 'make -C kmultiversx test TEST_ARGS="--kasmer-llvm-dir ../.build/defn/llvm/kasmer-kompiled/"' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make -C kmultiversx test' - name: 'Run TestApi tests' - run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c \ - 'make test-testapi' + run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make test-testapi' - name: 'Tear down Docker' if: always() run: | diff --git a/.gitignore b/.gitignore index 46cac1c8..1cce33d9 100644 --- a/.gitignore +++ b/.gitignore @@ -9,8 +9,7 @@ tmp .krun* .kprove* .kompile* -kdist *.pyc venv -.hypothesis \ No newline at end of file +.hypothesis diff --git a/Makefile b/Makefile index 022f288a..4b6dc4e6 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,5 @@ -.PHONY: all clean deps wasm-deps \ - build build-llvm build-haskell build-kasmer \ - plugin-deps \ - test unittest-python mandos-test test-elrond-contracts \ +.PHONY: all \ test-elrond-adder test-elrond-crowdfunding-esdt \ test-elrond-multisig test-elrond-basic-features \ test-elrond-alloc-features \ @@ -12,23 +9,7 @@ # Settings # -------- -UNAME_S := $(shell uname -s) - -BUILD_DIR := .build DEPS_DIR := deps -DEFN_DIR := $(BUILD_DIR)/defn -BUILD_LOCAL := $(abspath $(BUILD_DIR)/local) -LOCAL_LIB := $(BUILD_LOCAL)/lib -LOCAL_INCLUDE := $(BUILD_LOCAL)/include -K_INCLUDE_DIR := $(abspath $(DEPS_DIR)) - -LIBRARY_PATH := $(LOCAL_LIB) -C_INCLUDE_PATH += :$(BUILD_LOCAL)/include -CPLUS_INCLUDE_PATH += :$(BUILD_LOCAL)/include - -export LIBRARY_PATH -export C_INCLUDE_PATH -export CPLUS_INCLUDE_PATH PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/plugin) export PLUGIN_SUBMODULE @@ -41,171 +22,51 @@ ELROND_SDK_SUBMODULE := $(DEPS_DIR)/mx-sdk-rs ELROND_CONTRACT := $(ELROND_SDK_SUBMODULE)/contracts ELROND_CONTRACT_EXAMPLES := $(ELROND_CONTRACT)/examples -ifneq (,$(wildcard $(K_SUBMODULE)/k-distribution/target/release/k/bin/*)) - K_RELEASE ?= $(abspath $(K_SUBMODULE)/k-distribution/target/release/k) -else - K_RELEASE ?= $(dir $(shell which kompile)).. -endif -K_BIN := $(K_RELEASE)/bin -K_LIB := $(K_RELEASE)/lib/kframework -export K_OPTS ?= -Xmx8G -Xss512m -export K_RELEASE PYTHONPATH := $(K_LIB):$(KWASM_BINARY_PARSER):$(PYTHONPATH) export PYTHONPATH -KWASM_DIR := . -KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) -export KWASM_DIR all: build -clean: - rm -rf $(BUILD_DIR) - $(MAKE) -C $(PLUGIN_SUBMODULE) clean -# Non-K Dependencies -# ------------------ +# Building Definition +# ------------------- +K_OPTS := -Xmx8G -Xss512m +POETRY := poetry -C kmultiversx +POETRY_RUN := $(POETRY) run + + +.PHONY: plugin-deps plugin-deps: $(MAKE) -C $(PLUGIN_SUBMODULE) blake2 libcryptopp libff -j8 -# Build Dependencies (K Submodule) -# -------------------------------- +.PHONY: kmultiversx +kmultiversx: + $(POETRY) install --no-ansi + +.PHONY: build +build: build-mandos -K_JAR := $(K_SUBMODULE)/k-distribution/target/release/k/lib/java/kernel-1.0-SNAPSHOT.jar +.PHONY: build-mandos +build-mandos: kmultiversx plugin-deps + K_OPTS='$(K_OPTS)' $(POETRY) run kdist -v build mx-semantics.llvm-mandos -deps: wasm-deps +.PHONY: build-kasmer +build-kasmer: kmultiversx plugin-deps + K_OPTS='$(K_OPTS)' $(POETRY) run kdist -v build mx-semantics.llvm-kasmer -wasm-deps: - $(KWASM_MAKE) deps +.PHONY: build-haskell +build-haskell: kmultiversx + $(POETRY) run kdist -v build mx-semantics.haskell-\* -j2 + +.PHONY: clean +clean: kmultiversx + $(POETRY) run kdist clean + $(MAKE) -C $(PLUGIN_SUBMODULE) clean -# Building Definition -# ------------------- -HOOK_NAMESPACES := KRYPTO -KOMPILE_OPTS := --hook-namespaces \"$(HOOK_NAMESPACES)\" -I $(CURDIR) - -ifneq (,$(K_COVERAGE)) - KOMPILE_OPTS += --coverage -endif - -LLVM_KOMPILE_OPTS := -std=c++17 -g \ - $(PLUGIN_SUBMODULE)/build/blake2/lib/blake2.a \ - -I$(PLUGIN_SUBMODULE)/build/blake2/include \ - $(PLUGIN_SUBMODULE)/build/libcryptopp/lib/libcryptopp.a \ - -I$(PLUGIN_SUBMODULE)/build/libcryptopp/include \ - $(PLUGIN_SUBMODULE)/build/libff/lib/libff.a \ - -I$(PLUGIN_SUBMODULE)/build/libff/include \ - $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp \ - $(PLUGIN_SUBMODULE)/plugin-c/plugin_util.cpp \ - -lcrypto -lprocps -lsecp256k1 -lssl - -MAIN_MODULE := MANDOS -MAIN_SYNTAX_MODULE := MANDOS-SYNTAX -MAIN_DEFN_FILE := mandos -KASMER_MODULE := KASMER -KASMER_SYNTAX_MODULE := KASMER-SYNTAX -KASMER_DEFN_FILE := kasmer - -ELROND_FILE_NAMES := elrond.md \ - elrond-config.md \ - elrond-node.md \ - esdt.md \ - auto-allocate.md \ - mandos.md \ - kasmer.md \ - $(wildcard data/*.k) \ - $(wildcard vmhooks/*.md) - -PLUGIN_FILE_NAMES := blockchain-k-plugin/krypto.md -EXTRA_SOURCES := $(ELROND_FILE_NAMES) $(PLUGIN_FILE_NAMES) -ELROND_FILES_KWASM_DIR := $(patsubst %,$(KWASM_SUBMODULE)/%,$(ELROND_FILE_NAMES)) -PLUGIN_FILES_KWASM_DIR := $(patsubst %,$(KWASM_SUBMODULE)/%,$(PLUGIN_FILE_NAMES)) - -build: build-llvm - -# Semantics Build -# --------------- -llvm_dir := $(DEFN_DIR)/llvm -llvm_kompiled := $(llvm_dir)/mandos-kompiled/interpreter - - -build-llvm: $(llvm_kompiled) - -$(llvm_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) plugin-deps - $(KWASM_MAKE) build-llvm \ - DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \ - llvm_main_module=$(MAIN_MODULE) \ - llvm_syntax_module=$(MAIN_SYNTAX_MODULE) \ - llvm_main_file=$(MAIN_DEFN_FILE) \ - EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \ - KOMPILE_OPTS="$(KOMPILE_OPTS)" \ - LLVM_KOMPILE_OPTS="$(LLVM_KOMPILE_OPTS)" \ - K_INCLUDE_DIR=$(K_INCLUDE_DIR) - -$(KWASM_SUBMODULE)/%.md: %.md - cp $< $@ - -$(KWASM_SUBMODULE)/blockchain-k-plugin/%.md: $(PLUGIN_SUBMODULE)/plugin/%.md - @mkdir -p $(dir $@) - cp $< $@ - -$(KWASM_SUBMODULE)/vmhooks/%.md: vmhooks/%.md - @mkdir -p $(dir $@) - cp $< $@ - -$(KWASM_SUBMODULE)/data/%.k: data/%.k - @mkdir -p $(dir $@) - cp $< $@ - -# Kasmer Build -kasmer_kompiled := $(llvm_dir)/kasmer-kompiled/interpreter - -build-kasmer: $(kasmer_kompiled) - -# runs llvm-kompile separately to reduce max memory usage -$(kasmer_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) plugin-deps - $(KWASM_MAKE) build-llvm \ - DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \ - llvm_main_module=KASMER \ - llvm_syntax_module=KASMER-SYNTAX \ - llvm_main_file=kasmer \ - EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \ - KOMPILE_OPTS="$(KOMPILE_OPTS)" \ - LLVM_KOMPILE_OPTS="$(LLVM_KOMPILE_OPTS)" \ - K_INCLUDE_DIR=$(K_INCLUDE_DIR) - -# Haskell build -# The Haskell target is not currently in use. It is only for testing whether the symbolic modules compile successfully. -haskell_dir := $(DEFN_DIR)/haskell -haskell_kompiled := $(haskell_dir)/mandos-kompiled/interpreter - -haskell_kasmer_kompiled := $(haskell_dir)/kasmer-kompiled/interpreter - -build-haskell: $(haskell_kompiled) - -build-haskell-kasmer: $(haskell_kasmer_kompiled) - -$(haskell_kasmer_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) plugin-deps - $(KWASM_MAKE) build-haskell \ - DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \ - haskell_main_module=$(KASMER_MODULE) \ - haskell_syntax_module=$(KASMER_SYNTAX_MODULE) \ - haskell_main_file=$(KASMER_DEFN_FILE) \ - EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \ - KOMPILE_OPTS="$(KOMPILE_OPTS) --warnings-to-errors" \ - K_INCLUDE_DIR=$(K_INCLUDE_DIR) - -$(haskell_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) plugin-deps - $(KWASM_MAKE) build-haskell \ - DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \ - haskell_main_module=$(MAIN_MODULE) \ - haskell_syntax_module=$(MAIN_SYNTAX_MODULE) \ - haskell_main_file=$(MAIN_DEFN_FILE) \ - EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \ - KOMPILE_OPTS="$(KOMPILE_OPTS) --warnings-to-errors" \ - K_INCLUDE_DIR=$(K_INCLUDE_DIR) # Testing # ------- @@ -240,14 +101,8 @@ test-simple: $(simple_tests:=.run) # Elrond Tests # ------------ -POETRY := poetry -C kmultiversx -POETRY_RUN := $(POETRY) run - -.PHONY: poetry-install -poetry-install: - $(POETRY) install --no-ansi -TEST_MANDOS := $(POETRY_RUN) mandos --definition-dir $(llvm_dir)/mandos-kompiled +TEST_MANDOS := $(POETRY_RUN) mandos sc-build/%: sc-meta all build --path $* --wasm-symbols --no-wasm-opt @@ -256,7 +111,7 @@ sc-build/%: MANDOS_TESTS_DIR := tests/mandos mandos_tests=$(sort $(wildcard $(MANDOS_TESTS_DIR)/*.scen.json)) -mandos-test: $(llvm_kompiled) poetry-install +mandos-test: build $(TEST_MANDOS) $(mandos_tests) ## Adder Test @@ -264,7 +119,7 @@ mandos-test: $(llvm_kompiled) poetry-install ELROND_ADDER_DIR := $(ELROND_CONTRACT_EXAMPLES)/adder elrond_adder_tests=$(shell find $(ELROND_ADDER_DIR) -name "*.scen.json") -test-elrond-adder: $(llvm_kompiled) poetry-install sc-build/$(ELROND_ADDER_DIR) +test-elrond-adder: build sc-build/$(ELROND_ADDER_DIR) $(TEST_MANDOS) $(elrond_adder_tests) @@ -273,7 +128,7 @@ test-elrond-adder: $(llvm_kompiled) poetry-install sc-build/$(ELROND_ADDER_DIR) ELROND_CROWDFUNDING_DIR := $(ELROND_CONTRACT_EXAMPLES)/crowdfunding-esdt elrond_crowdfunding_tests=$(shell find $(ELROND_CROWDFUNDING_DIR) -name "*.scen.json") -test-elrond-crowdfunding-esdt: $(llvm_kompiled) poetry-install sc-build/$(ELROND_CROWDFUNDING_DIR) +test-elrond-crowdfunding-esdt: build sc-build/$(ELROND_CROWDFUNDING_DIR) $(TEST_MANDOS) $(elrond_crowdfunding_tests) ## Multisg Test @@ -281,7 +136,7 @@ test-elrond-crowdfunding-esdt: $(llvm_kompiled) poetry-install sc-build/$(ELROND ELROND_MULTISIG_DIR=$(ELROND_CONTRACT_EXAMPLES)/multisig elrond_multisig_tests=$(shell cat tests/multisig.test) -test-elrond-multisig: $(llvm_kompiled) poetry-install sc-build/$(ELROND_MULTISIG_DIR) +test-elrond-multisig: build sc-build/$(ELROND_MULTISIG_DIR) $(TEST_MANDOS) $(elrond_multisig_tests) ## Basic Feature Test @@ -295,10 +150,10 @@ $(ELROND_BASIC_FEATURES_WASM): sc-build/$(ELROND_BASIC_FEATURES_DIR) # TODO optimize test runner and enable logging test-elrond-basic-features: $(elrond_basic_features_tests:=.mandos) -$(ELROND_BASIC_FEATURES_DIR)/scenarios/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_BASIC_FEATURES_WASM) poetry-install +$(ELROND_BASIC_FEATURES_DIR)/scenarios/%.scen.json.mandos: build $(ELROND_BASIC_FEATURES_WASM) $(TEST_MANDOS) $(ELROND_BASIC_FEATURES_DIR)/scenarios/$*.scen.json --log-level none -tests/custom-scenarios/basic-features/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_BASIC_FEATURES_WASM) poetry-install +tests/custom-scenarios/basic-features/%.scen.json.mandos: build $(ELROND_BASIC_FEATURES_WASM) $(TEST_MANDOS) tests/custom-scenarios/basic-features/$*.scen.json --log-level none ## Alloc Features Test @@ -312,12 +167,12 @@ $(ELROND_ALLOC_FEATURES_WASM): sc-build/$(ELROND_ALLOC_FEATURES_DIR) # TODO optimize test runner and enable logging test-elrond-alloc-features: $(elrond_alloc_features_tests:=.mandos) -$(ELROND_ALLOC_FEATURES_DIR)/scenarios/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_ALLOC_FEATURES_WASM) poetry-install +$(ELROND_ALLOC_FEATURES_DIR)/scenarios/%.scen.json.mandos: build $(ELROND_ALLOC_FEATURES_WASM) $(TEST_MANDOS) $(ELROND_ALLOC_FEATURES_DIR)/scenarios/$*.scen.json --log-level none # Custom contract tests -custom-contracts := test-elrond-addercaller \ +custom-contracts := test-elrond-addercaller \ test-elrond-callercallee test-custom-contracts: $(custom-contracts) @@ -327,10 +182,7 @@ ELROND_ADDERCALLER_DIR := tests/contracts/addercaller elrond_addercaller_tests=$(shell find $(ELROND_ADDERCALLER_DIR) -name "*.scen.json") ELROND_MYADDER_DIR := tests/contracts/myadder -test-elrond-addercaller: $(llvm_kompiled) \ - poetry-install \ - sc-build/$(ELROND_MYADDER_DIR) \ - sc-build/$(ELROND_ADDERCALLER_DIR) +test-elrond-addercaller: build sc-build/$(ELROND_MYADDER_DIR) sc-build/$(ELROND_ADDERCALLER_DIR) $(TEST_MANDOS) $(elrond_addercaller_tests) ## Caller Callee Test @@ -339,22 +191,17 @@ ELROND_CALLER_DIR := tests/contracts/caller ELROND_CALLEE_DIR := tests/contracts/callee elrond_callercallee_tests=$(shell find $(ELROND_CALLER_DIR) -name "*.scen.json") -test-elrond-callercallee: $(llvm_kompiled) \ - poetry-install \ - sc-build/$(ELROND_CALLER_DIR) \ - sc-build/$(ELROND_CALLEE_DIR) +test-elrond-callercallee: build sc-build/$(ELROND_CALLER_DIR) sc-build/$(ELROND_CALLEE_DIR) $(TEST_MANDOS) $(elrond_callercallee_tests) ## Kasmer Test API tests -TEST_KASMER := $(POETRY_RUN) kasmer --definition-dir $(llvm_dir)/kasmer-kompiled +TEST_KASMER := $(POETRY_RUN) kasmer TEST_TESTAPI_DIR := tests/contracts/test_testapi testapi_tests=$(shell find $(TEST_TESTAPI_DIR) -name "*.scen.json") -test-testapi: $(kasmer_kompiled) \ - poetry-install \ - sc-build/$(TEST_TESTAPI_DIR) +test-testapi: build sc-build/$(TEST_TESTAPI_DIR) $(TEST_KASMER) -d $(TEST_TESTAPI_DIR) # Unit Tests @@ -362,11 +209,25 @@ test-testapi: $(kasmer_kompiled) \ PYTHON_UNITTEST_FILES = unittest-python: $(PYTHON_UNITTEST_FILES:=.unit) +MANDOS_KOMPILED := $(shell $(POETRY_RUN) kdist which mx-semantics.llvm-mandos) +KWASM_SRC_DIR := $(shell $(POETRY_RUN) python -c 'from pykwasm.kdist.plugin import K_DIR; print(K_DIR)') + +ELROND_FILE_NAMES := elrond.md \ + elrond-config.md \ + elrond-node.md \ + esdt.md \ + auto-allocate.md \ + mandos.md \ + kasmer.md \ + $(wildcard data/*.k) \ + $(wildcard vmhooks/*.md) +ELROND_FILES_KWASM_DIR := $(patsubst %,$(KWASM_SRC_DIR)/%,$(ELROND_FILE_NAMES)) + %.unit: % python3 $< rule-coverage: - python3 rule_coverage.py $(llvm_dir)/mandos-kompiled $(ELROND_FILES_KWASM_DIR) + python3 rule_coverage.py $(MANDOS_KOMPILED) $(ELROND_FILES_KWASM_DIR) clean-coverage: - rm $(llvm_dir)/mandos-kompiled/*_coverage.txt $(llvm_dir)/mandos-kompiled/coverage.txt + rm $(MANDOS_KOMPILED)/*_coverage.txt $(MANDOS_KOMPILED)/coverage.txt diff --git a/deps/kwasm_release b/deps/kwasm_release index 7db26729..5ef49d2f 100644 --- a/deps/kwasm_release +++ b/deps/kwasm_release @@ -1 +1 @@ -0.1.26 +0.1.29 diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 424b1ba8..0ea9fedf 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 424b1ba80170cfae942c0bd7a505657a8f6bfbc6 +Subproject commit 0ea9fedffb3ee6b266a56711bd718bb73e8c555a diff --git a/generate-claims.sh b/generate-claims.sh index b2750ed6..12e6bd76 100755 --- a/generate-claims.sh +++ b/generate-claims.sh @@ -8,7 +8,7 @@ poetry -C kmultiversx install sc-meta all build --path deps/mx-sdk-rs/contracts/examples/adder --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/foundrylike --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --definition-dir $(kbuild which llvm-kasmer) --directory "tests/contracts/foundrylike" --gen-claims 2>&1 | tee kasmer.log +K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/foundrylike" --gen-claims 2>&1 | tee kasmer.log # Coindrip @@ -19,22 +19,22 @@ do done sc-meta all build --path deps/coindrip-protocol-sc --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_coindrip --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --definition-dir $(kbuild which llvm-kasmer) --directory "tests/contracts/test_coindrip" --gen-claims 2>&1 | tee kasmer.log +K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_coindrip" --gen-claims 2>&1 | tee kasmer.log # Crowdfunding sc-meta all build --path deps/mx-sdk-rs/contracts/examples/crowdfunding-esdt --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_crowdfunding-esdt --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --definition-dir $(kbuild which llvm-kasmer) --directory "tests/contracts/test_crowdfunding-esdt" --gen-claims 2>&1 | tee kasmer.log +K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_crowdfunding-esdt" --gen-claims 2>&1 | tee kasmer.log # Pair sc-meta all build --path deps/mx-exchange-sc/dex/pair --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_pair --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --definition-dir $(kbuild which llvm-kasmer) --directory "tests/contracts/test_pair" --gen-claims 2>&1 | tee kasmer.log +K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_pair" --gen-claims 2>&1 | tee kasmer.log # Multisig sc-meta all build --path deps/mx-sdk-rs/contracts/examples/multisig --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_multisig --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --definition-dir $(kbuild which llvm-kasmer) --directory "tests/contracts/test_multisig" --gen-claims 2>&1 | tee kasmer.log +K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_multisig" --gen-claims 2>&1 | tee kasmer.log diff --git a/kbuild.toml b/kbuild.toml deleted file mode 100644 index 8802f04d..00000000 --- a/kbuild.toml +++ /dev/null @@ -1,23 +0,0 @@ -[project] -name = "elrond-semantics" -version = "0.1.0" -source = "." - -[dependencies] -wasm-semantics={ path = "deps/wasm-semantics" } - -[targets.llvm] -main-file = 'mandos.md' -backend='llvm' - -[targets.haskell] -main-file = 'mandos.md' -backend='haskell' - -[targets.llvm-kasmer] -main-file = 'kasmer.md' -backend='llvm' - -[targets.haskell-kasmer] -main-file = 'kasmer.md' -backend='haskell' diff --git a/kelrond b/kelrond index 750cf701..649cdf7c 100755 --- a/kelrond +++ b/kelrond @@ -8,7 +8,8 @@ fatal() { echo "[FATAL] $@" ; exit 1 ; } kelrond_dir="${KELROND_DIR:-$(dirname $0)}" build_dir="$kelrond_dir/.build" -defn_dir="${KELROND_DEFN_DIR:-$build_dir/defn}" +kdist_dir="$(poetry -C kmultiversx run -- kdist which)" +defn_dir="${KELROND_DEFN_DIR:-$kdist_dir}/mx-semantics" kwasm_dir=$kelrond_dir/deps/wasm-semantics @@ -116,10 +117,7 @@ while [[ $# -gt 0 ]]; do done set -- "${args[@]}" -backend_dir="$defn_dir/$backend" - -# kompiled_dir = .build/defn//-kompiled -kompiled_dir="$backend_dir/$main_file-kompiled" +kompiled_dir="$defn_dir/$backend-$main_file" # get the run file [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to run on." diff --git a/kmultiversx/poetry.lock b/kmultiversx/poetry.lock index 483abca2..e88f3714 100644 --- a/kmultiversx/poetry.lock +++ b/kmultiversx/poetry.lock @@ -36,33 +36,33 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} [[package]] name = "black" -version = "24.3.0" +version = "24.4.0" description = "The uncompromising code formatter." optional = false python-versions = ">=3.8" files = [ - {file = "black-24.3.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:7d5e026f8da0322b5662fa7a8e752b3fa2dac1c1cbc213c3d7ff9bdd0ab12395"}, - {file = "black-24.3.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:9f50ea1132e2189d8dff0115ab75b65590a3e97de1e143795adb4ce317934995"}, - {file = "black-24.3.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e2af80566f43c85f5797365077fb64a393861a3730bd110971ab7a0c94e873e7"}, - {file = "black-24.3.0-cp310-cp310-win_amd64.whl", hash = "sha256:4be5bb28e090456adfc1255e03967fb67ca846a03be7aadf6249096100ee32d0"}, - {file = "black-24.3.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:4f1373a7808a8f135b774039f61d59e4be7eb56b2513d3d2f02a8b9365b8a8a9"}, - {file = "black-24.3.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:aadf7a02d947936ee418777e0247ea114f78aff0d0959461057cae8a04f20597"}, - {file = "black-24.3.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:65c02e4ea2ae09d16314d30912a58ada9a5c4fdfedf9512d23326128ac08ac3d"}, - {file = "black-24.3.0-cp311-cp311-win_amd64.whl", hash = "sha256:bf21b7b230718a5f08bd32d5e4f1db7fc8788345c8aea1d155fc17852b3410f5"}, - {file = "black-24.3.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:2818cf72dfd5d289e48f37ccfa08b460bf469e67fb7c4abb07edc2e9f16fb63f"}, - {file = "black-24.3.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:4acf672def7eb1725f41f38bf6bf425c8237248bb0804faa3965c036f7672d11"}, - {file = "black-24.3.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c7ed6668cbbfcd231fa0dc1b137d3e40c04c7f786e626b405c62bcd5db5857e4"}, - {file = "black-24.3.0-cp312-cp312-win_amd64.whl", hash = "sha256:56f52cfbd3dabe2798d76dbdd299faa046a901041faf2cf33288bc4e6dae57b5"}, - {file = "black-24.3.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:79dcf34b33e38ed1b17434693763301d7ccbd1c5860674a8f871bd15139e7837"}, - {file = "black-24.3.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:e19cb1c6365fd6dc38a6eae2dcb691d7d83935c10215aef8e6c38edee3f77abd"}, - {file = "black-24.3.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:65b76c275e4c1c5ce6e9870911384bff5ca31ab63d19c76811cb1fb162678213"}, - {file = "black-24.3.0-cp38-cp38-win_amd64.whl", hash = "sha256:b5991d523eee14756f3c8d5df5231550ae8993e2286b8014e2fdea7156ed0959"}, - {file = "black-24.3.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:c45f8dff244b3c431b36e3224b6be4a127c6aca780853574c00faf99258041eb"}, - {file = "black-24.3.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:6905238a754ceb7788a73f02b45637d820b2f5478b20fec82ea865e4f5d4d9f7"}, - {file = "black-24.3.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d7de8d330763c66663661a1ffd432274a2f92f07feeddd89ffd085b5744f85e7"}, - {file = "black-24.3.0-cp39-cp39-win_amd64.whl", hash = "sha256:7bb041dca0d784697af4646d3b62ba4a6b028276ae878e53f6b4f74ddd6db99f"}, - {file = "black-24.3.0-py3-none-any.whl", hash = "sha256:41622020d7120e01d377f74249e677039d20e6344ff5851de8a10f11f513bf93"}, - {file = "black-24.3.0.tar.gz", hash = "sha256:a0c9c4a0771afc6919578cec71ce82a3e31e054904e7197deacbc9382671c41f"}, + {file = "black-24.4.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6ad001a9ddd9b8dfd1b434d566be39b1cd502802c8d38bbb1ba612afda2ef436"}, + {file = "black-24.4.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:e3a3a092b8b756c643fe45f4624dbd5a389f770a4ac294cf4d0fce6af86addaf"}, + {file = "black-24.4.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:dae79397f367ac8d7adb6c779813328f6d690943f64b32983e896bcccd18cbad"}, + {file = "black-24.4.0-cp310-cp310-win_amd64.whl", hash = "sha256:71d998b73c957444fb7c52096c3843875f4b6b47a54972598741fe9a7f737fcb"}, + {file = "black-24.4.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:8e5537f456a22cf5cfcb2707803431d2feeb82ab3748ade280d6ccd0b40ed2e8"}, + {file = "black-24.4.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:64e60a7edd71fd542a10a9643bf369bfd2644de95ec71e86790b063aa02ff745"}, + {file = "black-24.4.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5cd5b4f76056cecce3e69b0d4c228326d2595f506797f40b9233424e2524c070"}, + {file = "black-24.4.0-cp311-cp311-win_amd64.whl", hash = "sha256:64578cf99b6b46a6301bc28bdb89f9d6f9b592b1c5837818a177c98525dbe397"}, + {file = "black-24.4.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:f95cece33329dc4aa3b0e1a771c41075812e46cf3d6e3f1dfe3d91ff09826ed2"}, + {file = "black-24.4.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:4396ca365a4310beef84d446ca5016f671b10f07abdba3e4e4304218d2c71d33"}, + {file = "black-24.4.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:44d99dfdf37a2a00a6f7a8dcbd19edf361d056ee51093b2445de7ca09adac965"}, + {file = "black-24.4.0-cp312-cp312-win_amd64.whl", hash = "sha256:21f9407063ec71c5580b8ad975653c66508d6a9f57bd008bb8691d273705adcd"}, + {file = "black-24.4.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:652e55bb722ca026299eb74e53880ee2315b181dfdd44dca98e43448620ddec1"}, + {file = "black-24.4.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:7f2966b9b2b3b7104fca9d75b2ee856fe3fdd7ed9e47c753a4bb1a675f2caab8"}, + {file = "black-24.4.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:1bb9ca06e556a09f7f7177bc7cb604e5ed2d2df1e9119e4f7d2f1f7071c32e5d"}, + {file = "black-24.4.0-cp38-cp38-win_amd64.whl", hash = "sha256:d4e71cdebdc8efeb6deaf5f2deb28325f8614d48426bed118ecc2dcaefb9ebf3"}, + {file = "black-24.4.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:6644f97a7ef6f401a150cca551a1ff97e03c25d8519ee0bbc9b0058772882665"}, + {file = "black-24.4.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:75a2d0b4f5eb81f7eebc31f788f9830a6ce10a68c91fbe0fade34fff7a2836e6"}, + {file = "black-24.4.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:eb949f56a63c5e134dfdca12091e98ffb5fd446293ebae123d10fc1abad00b9e"}, + {file = "black-24.4.0-cp39-cp39-win_amd64.whl", hash = "sha256:7852b05d02b5b9a8c893ab95863ef8986e4dda29af80bbbda94d7aee1abf8702"}, + {file = "black-24.4.0-py3-none-any.whl", hash = "sha256:74eb9b5420e26b42c00a3ff470dc0cd144b80a766128b1771d07643165e08d0e"}, + {file = "black-24.4.0.tar.gz", hash = "sha256:f07b69fda20578367eaebbd670ff8fc653ab181e1ff95d84497f9fa20e7d0641"}, ] [package.dependencies] @@ -997,7 +997,7 @@ resolved_reference = "f705bcd96224b80a35619a8e4112f7880bcaae81" [[package]] name = "pykwasm" -version = "0.1.26" +version = "0.1.29" description = "" optional = false python-versions = "^3.10" @@ -1013,8 +1013,8 @@ pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.778"} [package.source] type = "git" url = "https://github.com/runtimeverification/wasm-semantics.git" -reference = "v0.1.26" -resolved_reference = "424b1ba80170cfae942c0bd7a505657a8f6bfbc6" +reference = "v0.1.29" +resolved_reference = "0ea9fedffb3ee6b266a56711bd718bb73e8c555a" subdirectory = "pykwasm" [[package]] @@ -1292,4 +1292,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "b9b5fe23b10622f8ead7cba3c2b084ce999926d4362f36871697f44798af4b3a" +content-hash = "d989b38a4c495fed75816fa1073c3757401c8ae4f1d6b62ae49729e3968871a9" diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 44daf64e..de8f8dba 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,15 +4,18 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.28" +version = "0.1.29" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", ] +[tool.poetry.plugins.kdist] +mx-semantics = "kmultiversx.kdist.plugin" + [tool.poetry.dependencies] python = "^3.10" -pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.26", subdirectory = "pykwasm" } +pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.29", subdirectory = "pykwasm" } pycryptodomex = "^3.18.0" hypothesis = "^6.82.6" diff --git a/kmultiversx/src/kmultiversx/kasmer.py b/kmultiversx/src/kmultiversx/kasmer.py index bdbe46a2..6bc48e8e 100644 --- a/kmultiversx/src/kmultiversx/kasmer.py +++ b/kmultiversx/src/kmultiversx/kasmer.py @@ -16,6 +16,7 @@ from pyk.cterm import CTerm, cterm_build_claim from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst from pyk.kast.manip import split_config_from +from pyk.kdist import kdist from pyk.ktool.krun import KRun from pyk.prelude.collections import list_of, map_of, set_of from pyk.prelude.kint import leInt @@ -473,7 +474,6 @@ def main() -> None: parser = argparse.ArgumentParser(description='Symbolic testing for MultiversX contracts') parser.add_argument( '--definition-dir', - default=None, dest='definition_dir', type=dir_path, help='Path to Foundry LLVM definition to use.', @@ -509,6 +509,11 @@ def main() -> None: ) args = parser.parse_args() + definition_dir = args.definition_dir + if definition_dir is None: + definition_dir = kdist.get('mx-semantics.llvm-kasmer') + krun = KRun(definition_dir) + test_dir = args.directory # Load test parameters in JSON @@ -522,8 +527,6 @@ def main() -> None: wasm_paths = (join(test_dir, p) for p in input_json['contract_paths']) contract_wasms = load_contract_wasms(wasm_paths) - krun = KRun(args.definition_dir) - print('Initializing the test...') sym_conf, init_subst = deploy_test(krun, test_wasm, contract_wasms) print('Initialization done.') diff --git a/kmultiversx/src/kmultiversx/kdist/__init__.py b/kmultiversx/src/kmultiversx/kdist/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/auto-allocate.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/auto-allocate.md similarity index 100% rename from auto-allocate.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/auto-allocate.md diff --git a/data/bytes-type.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/bytes-type.k similarity index 100% rename from data/bytes-type.k rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/data/bytes-type.k diff --git a/data/int-type.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k similarity index 100% rename from data/int-type.k rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k diff --git a/data/list-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k similarity index 100% rename from data/list-bytes.k rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k diff --git a/data/map-bytes-to-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-bytes-to-bytes.k similarity index 100% rename from data/map-bytes-to-bytes.k rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-bytes-to-bytes.k diff --git a/data/map-int-to-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k similarity index 100% rename from data/map-int-to-bytes.k rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k diff --git a/elrond-config.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md similarity index 99% rename from elrond-config.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md index 32dd9bdd..35d935e8 100644 --- a/elrond-config.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md @@ -4,11 +4,11 @@ Elrond Configuration Combine Elrond node with Wasm. ```k +requires "wasm-semantics/wasm-text.md" +requires "plugin/krypto.md" requires "auto-allocate.md" -requires "deps/plugin/plugin/krypto.md" requires "elrond-node.md" requires "esdt.md" -requires "wasm-semantics/wasm-text.md" module ELROND-CONFIG imports KRYPTO diff --git a/elrond-node.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md similarity index 100% rename from elrond-node.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md index ea861a0d..464563fe 100644 --- a/elrond-node.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md @@ -2,10 +2,10 @@ Elrond Node =========== ```k +requires "wasm-semantics/wasm.md" requires "data/list-bytes.k" requires "data/map-bytes-to-bytes.k" requires "data/map-int-to-bytes.k" -requires "wasm-semantics/wasm.md" module ELROND-NODE imports DOMAINS diff --git a/elrond.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond.md similarity index 100% rename from elrond.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond.md diff --git a/esdt.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md similarity index 100% rename from esdt.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md diff --git a/kasmer.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md similarity index 100% rename from kasmer.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md diff --git a/mandos.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/mandos.md similarity index 100% rename from mandos.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/mandos.md diff --git a/vmhooks/baseOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/baseOps.md similarity index 100% rename from vmhooks/baseOps.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/baseOps.md diff --git a/vmhooks/bigIntOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/bigIntOps.md similarity index 100% rename from vmhooks/bigIntOps.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/bigIntOps.md diff --git a/vmhooks/cryptoei.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/cryptoei.md similarity index 100% rename from vmhooks/cryptoei.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/cryptoei.md diff --git a/vmhooks/eei-helpers.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/eei-helpers.md similarity index 100% rename from vmhooks/eei-helpers.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/eei-helpers.md diff --git a/vmhooks/manBufOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md similarity index 100% rename from vmhooks/manBufOps.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md diff --git a/vmhooks/managedConversions.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/managedConversions.md similarity index 100% rename from vmhooks/managedConversions.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/managedConversions.md diff --git a/vmhooks/managedei.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/managedei.md similarity index 100% rename from vmhooks/managedei.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/managedei.md diff --git a/vmhooks/smallIntOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md similarity index 100% rename from vmhooks/smallIntOps.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md diff --git a/vmhooks/utils.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/utils.md similarity index 100% rename from vmhooks/utils.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/utils.md diff --git a/vmhooks/vmhooks.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/vmhooks.md similarity index 100% rename from vmhooks/vmhooks.md rename to kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/vmhooks.md diff --git a/kmultiversx/src/kmultiversx/kdist/plugin.py b/kmultiversx/src/kmultiversx/kdist/plugin.py new file mode 100644 index 00000000..fcadde26 --- /dev/null +++ b/kmultiversx/src/kmultiversx/kdist/plugin.py @@ -0,0 +1,93 @@ +from __future__ import annotations + +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.kbuild.utils import k_version +from pyk.kdist.api import Target +from pyk.ktool.kompile import KompileBackend, kompile +from pykwasm.kdist.plugin import SOURCE_DIR as WASM_DIR + +if TYPE_CHECKING: + from collections.abc import Mapping + from typing import Any, Final + + +CURRENT_DIR: Final = Path(__file__).parent +SOURCE_DIR: Final = CURRENT_DIR / 'mx-semantics' +PLUGIN_DIR: Final = CURRENT_DIR.parents[3] / 'deps/plugin' # TODO Distribute plugin files with Python + + +class KompileTarget(Target): + _kompile_args: dict[str, Any] + + def __init__(self, kompile_args: Mapping[str, Any]): + self._kompile_args = dict(kompile_args) + + def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None: + # TODO Pass K_OPTS='-Xmx8G -Xss512m' + kompile( + output_dir=output_dir, + verbose=verbose, + **self._kompile_args, + ) + + def source(self) -> tuple[Path, ...]: + return (SOURCE_DIR,) + + def context(self) -> dict[str, str]: + return {'k-version': k_version().text} + + +def llvm_target(main_file: Path, main_module: str, syntax_module: str) -> KompileTarget: + return KompileTarget( + { + 'backend': KompileBackend.LLVM, + 'main_file': main_file, + 'main_module': main_module, + 'syntax_module': syntax_module, + 'include_dirs': [WASM_DIR, PLUGIN_DIR], + 'md_selector': 'k', + 'hook_namespaces': ['KRYPTO'], + 'opt_level': 2, + 'ccopts': [ + '-g', + '-std=c++17', + '-lcrypto', + '-lprocps', + '-lsecp256k1', + '-lssl', + f"{PLUGIN_DIR / 'build/blake2/lib/blake2.a'}", + f"-I{PLUGIN_DIR / 'build/blake2/include'}", + f"{PLUGIN_DIR / 'build/libcryptopp/lib/libcryptopp.a'}", + f"-I{PLUGIN_DIR / 'build/libcryptopp/include'}", + f"{PLUGIN_DIR / 'build/libff/lib/libff.a'}", + f"-I{PLUGIN_DIR / 'build/libff/include'}", + f"{PLUGIN_DIR / 'plugin-c/crypto.cpp'}", + f"{PLUGIN_DIR / 'plugin-c/plugin_util.cpp'}", + ], + }, + ) + + +def haskell_target(main_file: Path, main_module: str, syntax_module: str) -> KompileTarget: + return KompileTarget( + { + 'backend': KompileBackend.HASKELL, + 'main_file': main_file, + 'main_module': main_module, + 'syntax_module': syntax_module, + 'include_dirs': [WASM_DIR, PLUGIN_DIR], + 'md_selector': 'k', + 'hook_namespaces': ['KRYPTO'], + 'warning_to_error': True, + }, + ) + + +__TARGETS__: Final = { + 'llvm-mandos': llvm_target(SOURCE_DIR / 'mandos.md', 'MANDOS', 'MANDOS-SYNTAX'), + 'llvm-kasmer': llvm_target(SOURCE_DIR / 'kasmer.md', 'KASMER', 'KASMER-SYNTAX'), + 'haskell-mandos': haskell_target(SOURCE_DIR / 'mandos.md', 'MANDOS', 'MANDOS-SYNTAX'), + 'haskell-kasmer': haskell_target(SOURCE_DIR / 'kasmer.md', 'KASMER', 'KASMER-SYNTAX'), +} diff --git a/kmultiversx/src/kmultiversx/scenario.py b/kmultiversx/src/kmultiversx/scenario.py old mode 100755 new mode 100644 index 1c5f2115..2d493217 --- a/kmultiversx/src/kmultiversx/scenario.py +++ b/kmultiversx/src/kmultiversx/scenario.py @@ -13,6 +13,7 @@ from pyk.cli.utils import dir_path from pyk.kast.inner import KApply, KSequence, KToken, Subst from pyk.kast.manip import split_config_from +from pyk.kdist import kdist from pyk.ktool.krun import KRun from pyk.prelude.collections import set_of from pykwasm.kwasm_ast import KBytes, KInt, KString @@ -761,28 +762,25 @@ def log_intermediate_state(krun: KRun, name: str, config: KInner, output_dir: st f.write(pretty) -# Main Script -args = None - - def run_tests() -> None: - global args test_args = argparse.ArgumentParser(description='') test_args.add_argument('files', metavar='N', type=str, nargs='+', help='') test_args.add_argument('--log-level', choices=['none', 'per-file', 'per-step'], default='per-file') test_args.add_argument('--verbose', action='store_true', help='') test_args.add_argument( '--definition-dir', - default=None, - required=True, dest='definition_dir', type=dir_path, help='Path to Mandos LLVM definition to use.', ) args = test_args.parse_args() - tests = args.files - krun = KRun(args.definition_dir) + definition_dir = args.definition_dir + if definition_dir is None: + definition_dir = kdist.get('mx-semantics.llvm-mandos') + krun = KRun(definition_dir) + + tests = args.files template_wasm_config = krun.definition.init_config(GENERATED_TOP_CELL) diff --git a/kmultiversx/src/tests/conftest.py b/kmultiversx/src/tests/conftest.py index 178c04aa..9c803852 100644 --- a/kmultiversx/src/tests/conftest.py +++ b/kmultiversx/src/tests/conftest.py @@ -1,9 +1,15 @@ -from pathlib import Path +from __future__ import annotations + +from typing import TYPE_CHECKING import pytest from pyk.cli.utils import dir_path +from pyk.kdist import kdist from pyk.ktool.krun import KRun +if TYPE_CHECKING: + from pathlib import Path + def pytest_addoption(parser: pytest.Parser) -> None: parser.addoption( @@ -15,12 +21,19 @@ def pytest_addoption(parser: pytest.Parser) -> None: @pytest.fixture(scope='session') -def kasmer_llvm_dir(pytestconfig: pytest.Config) -> Path: - ldir = pytestconfig.getoption('kasmer_llvm_dir') - assert isinstance(ldir, Path) - return ldir +def kasmer_llvm_dir(pytestconfig: pytest.Config) -> Path | None: + return pytestconfig.getoption('kasmer_llvm_dir') @pytest.fixture(scope='session') -def kasmer_llvm_krun(kasmer_llvm_dir: Path) -> KRun: +def kasmer_llvm_krun(kasmer_llvm_dir: Path | None) -> KRun: + if kasmer_llvm_dir is not None: + return KRun(kasmer_llvm_dir) + + kasmer_llvm_dir = kdist.which('mx-semantics.llvm-kasmer') + if not kasmer_llvm_dir.is_dir(): + raise ValueError( + 'Kasmer LLVM definition not found. Run make from the repository root, or pass --kasmer-llvm-dir' + ) + return KRun(kasmer_llvm_dir) diff --git a/package/version b/package/version index baec65a9..5ef49d2f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.28 +0.1.29