runtimeverification · rv-jenkins · Aug 31, 2023 · Aug 16, 2023 · Aug 21, 2023 · Aug 21, 2023
diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
@@ -21,7 +21,7 @@ runs:
       GROUP=$(id -gn)
       GROUP_ID=$(id -g)
 
-      docker build . --tag ${TAG} --build-arg K_COMMIT="$(cat deps/wasm-semantics/deps/k_release)" --build-arg PYK_VERSION="$(cat deps/wasm-semantics/deps/pyk_release)" --build-arg USER_ID=${USER_ID} --build-arg GROUP_ID=${GROUP_ID} --build-arg USER=${USER} --build-arg GROUP=${GROUP}
+      docker build . --tag ${TAG} --build-arg K_COMMIT="$(cat deps/wasm-semantics/deps/k_release)" --build-arg USER_ID=${USER_ID} --build-arg GROUP_ID=${GROUP_ID} --build-arg USER=${USER} --build-arg GROUP=${GROUP}
 
       docker run                 \
         --name ${CONTAINER_NAME} \

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -12,24 +12,18 @@ jobs:
     name: 'Simple Tests'
     timeout-minutes: 30
     steps:
-      - name: Checkout
+      - name: 'Check out code'
         uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-      - name: Checkout submodules
-        env: 
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-        run: |
-          # https://gist.github.com/taoyuan/bfa3ff87e4b5611b5cbe ; for a repository we don't control the submodules over. 
-          git config --global url."https://github.com/".insteadOf git@github.com:
-          git config --global url."https://".insteadOf git://
-          git submodule update --init --recursive
+        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'
       - name: 'Run Python Unit Tests'
         run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} /bin/bash -c 'make TEST_CONCRETE_BACKEND=llvm unittest-python'
       - name: 'Run Simple Test'
@@ -47,24 +41,18 @@ jobs:
     needs: [simple-tests]
     timeout-minutes: 120
     steps:
-      - name: Checkout
+      - name: 'Check out code'
         uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-      - name: Checkout submodules
-        env: 
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-        run: |
-          # https://gist.github.com/taoyuan/bfa3ff87e4b5611b5cbe ; for a repository we don't control the submodules over. 
-          git config --global url."https://github.com/".insteadOf git@github.com:
-          git config --global url."https://".insteadOf git://
-          git submodule update --init --recursive
+        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'
       - 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'
       - name: 'Run Alloc Feature Test'
@@ -80,24 +68,18 @@ jobs:
     needs: [feature-tests]
     timeout-minutes: 60
     steps:
-      - name: Checkout
+      - name: 'Check out code'
         uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-      - name: Checkout submodules
-        env: 
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-        run: |
-          # https://gist.github.com/taoyuan/bfa3ff87e4b5611b5cbe ; for a repository we don't control the submodules over. 
-          git config --global url."https://github.com/".insteadOf git@github.com:
-          git config --global url."https://".insteadOf git://
-          git submodule update --init --recursive
+        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'
       - 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'
       - name: 'Run Crowdfunding ESDT Contract Test'
@@ -115,24 +97,18 @@ jobs:
     needs: [feature-tests]
     timeout-minutes: 30
     steps:
-      - name: Checkout
+      - name: 'Check out code'
         uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-      - name: Checkout submodules
-        env: 
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-        run: |
-          # https://gist.github.com/taoyuan/bfa3ff87e4b5611b5cbe ; for a repository we don't control the submodules over. 
-          git config --global url."https://github.com/".insteadOf git@github.com:
-          git config --global url."https://".insteadOf git://
-          git submodule update --init --recursive
+        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'
       - 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'
       - name: 'Tear down Docker'

diff --git a/Dockerfile b/Dockerfile
@@ -18,6 +18,9 @@ RUN    apt-get update                      \
                        python3-pip         \
                        python3-venv
 
+RUN    curl -sSL https://install.python-poetry.org | POETRY_HOME=/usr python3 - \
+    && poetry --version
+
 ARG USER=github-user
 ARG GROUP=$USER
 ARG USER_ID=1000
@@ -31,13 +34,7 @@ WORKDIR /home/$USER
 RUN curl https://sh.rustup.rs -sSf | sh -s -- -y --default-toolchain nightly-2023-03-01 --target wasm32-unknown-unknown
 ENV PATH=/home/$USER/.cargo/bin:$PATH
 
-ARG PYK_VERSION
 RUN python3 -m pip install --upgrade pip
-RUN pip3 install --user --upgrade \
-                 cytoolz          \
-                 numpy            \
-                 pycryptodomex    \
-                 git+https://github.com/runtimeverification/pyk.git@${PYK_VERSION}
 
 RUN    git clone 'https://github.com/WebAssembly/wabt' --branch 1.0.13 --recurse-submodules wabt \
     && cd wabt                                                                                   \

diff --git a/Makefile b/Makefile
@@ -262,24 +262,42 @@ $(ELROND_LOADED_JSON): $(ELROND_RUNTIME)
 
 # Elrond Tests
 # ------------
+POETRY     := poetry -C kmultiversx
+POETRY_RUN := $(POETRY) run
 
-TEST_MANDOS := python3 run_elrond_tests.py
+.PHONY: poetry-install
+poetry-install:
+	$(POETRY) install --no-ansi
 
+TEST_MANDOS := $(POETRY_RUN) mandos --definition-dir $(llvm_dir)/mandos-kompiled
+
+# Cargo resolves dependencies to the latest version that satisfy requirements without taking
+# the rustc version into account, which leads to the following error:
+#
+# > error: package `clap_derive v4.4.0` cannot be built because it requires rustc 1.70.0 or newer,
+# > while the currently active rustc version is 1.69.0-nightly
+# 
+# To avoid this, we enforce minimal version resolution before building the contract
+mxpy-build/%:
+	if [ ! -f "$*/Cargo.lock" ]; then \
+	    cargo generate-lockfile --manifest-path $*/Cargo.toml -Z minimal-versions ; \
+	fi
+
+	mxpy contract build "$*" --wasm-symbols --no-wasm-opt
 
 ## Mandos Test
 
 MANDOS_TESTS_DIR := tests/mandos
 mandos_tests=$(sort $(wildcard $(MANDOS_TESTS_DIR)/*.scen.json))
-mandos-test: $(llvm_kompiled)
+mandos-test: $(llvm_kompiled) poetry-install
 	$(TEST_MANDOS) $(mandos_tests)
 
 ## Adder Test
 
 ELROND_ADDER_DIR := $(ELROND_CONTRACT_EXAMPLES)/adder
 elrond_adder_tests=$(shell find $(ELROND_ADDER_DIR) -name "*.scen.json")
 
-test-elrond-adder: $(llvm_kompiled)
-	mxpy contract build "$(ELROND_ADDER_DIR)" --wasm-symbols
+test-elrond-adder: $(llvm_kompiled) poetry-install mxpy-build/$(ELROND_ADDER_DIR)
 	$(TEST_MANDOS) $(elrond_adder_tests)
 
 
@@ -288,17 +306,15 @@ test-elrond-adder: $(llvm_kompiled)
 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)
-	mxpy contract build "$(ELROND_CROWDFUNDING_DIR)" --wasm-symbols
+test-elrond-crowdfunding-esdt: $(llvm_kompiled) poetry-install mxpy-build/$(ELROND_CROWDFUNDING_DIR)
 	$(TEST_MANDOS) $(elrond_crowdfunding_tests)
 
 ## Multisg Test
 
 ELROND_MULTISIG_DIR=$(ELROND_CONTRACT_EXAMPLES)/multisig
 elrond_multisig_tests=$(shell cat tests/multisig.test)
 
-test-elrond-multisig: $(llvm_kompiled)
-	mxpy contract build "$(ELROND_MULTISIG_DIR)" --wasm-symbols
+test-elrond-multisig: $(llvm_kompiled) poetry-install mxpy-build/$(ELROND_MULTISIG_DIR)
 	$(TEST_MANDOS) $(elrond_multisig_tests)
 
 ## Basic Feature Test
@@ -307,13 +323,12 @@ ELROND_BASIC_FEATURES_DIR=$(ELROND_CONTRACT)/feature-tests/basic-features
 ELROND_BASIC_FEATURES_WASM=$(ELROND_BASIC_FEATURES_DIR)/output/basic-features.wasm
 elrond_basic_features_tests=$(shell cat tests/basic_features.test)
 
-$(ELROND_BASIC_FEATURES_WASM):
-	mxpy contract build "$(ELROND_BASIC_FEATURES_DIR)" --wasm-symbols
+$(ELROND_BASIC_FEATURES_WASM): mxpy-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)
+$(ELROND_BASIC_FEATURES_DIR)/scenarios/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_BASIC_FEATURES_WASM) poetry-install
 	$(TEST_MANDOS) $(ELROND_BASIC_FEATURES_DIR)/scenarios/$*.scen.json --log-level none
 
 ## Alloc Features Test
@@ -322,13 +337,12 @@ ELROND_ALLOC_FEATURES_DIR=$(ELROND_CONTRACT)/feature-tests/alloc-features
 ELROND_ALLOC_FEATURES_WASM=$(ELROND_ALLOC_FEATURES_DIR)/output/alloc-features.wasm
 elrond_alloc_features_tests=$(shell cat tests/alloc_features.test)
 
-$(ELROND_ALLOC_FEATURES_WASM):
-	mxpy contract build "$(ELROND_ALLOC_FEATURES_DIR)" --wasm-symbols
+$(ELROND_ALLOC_FEATURES_WASM): mxpy-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)
+$(ELROND_ALLOC_FEATURES_DIR)/scenarios/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_ALLOC_FEATURES_WASM) poetry-install
 	$(TEST_MANDOS) $(ELROND_ALLOC_FEATURES_DIR)/scenarios/$*.scen.json --log-level none
 
 # Custom contract tests
@@ -343,9 +357,10 @@ 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)
-	mxpy contract build "$(ELROND_MYADDER_DIR)" --wasm-symbols
-	mxpy contract build "$(ELROND_ADDERCALLER_DIR)" --wasm-symbols
+test-elrond-addercaller: $(llvm_kompiled)                     \
+                         poetry-install                       \
+                         mxpy-build/$(ELROND_MYADDER_DIR)     \
+                         mxpy-build/$(ELROND_ADDERCALLER_DIR)
 	$(TEST_MANDOS) $(elrond_addercaller_tests)
 
 ## Caller Callee Test
@@ -354,9 +369,10 @@ 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)
-	mxpy contract build "$(ELROND_CALLER_DIR)" --wasm-symbols
-	mxpy contract build "$(ELROND_CALLEE_DIR)" --wasm-symbols
+test-elrond-callercallee: $(llvm_kompiled)                    \
+                          poetry-install                      \
+                          mxpy-build/$(ELROND_CALLER_DIR)     \
+                          mxpy-build/$(ELROND_CALLEE_DIR)
 	$(TEST_MANDOS) $(elrond_callercallee_tests)
 
 # Unit Tests

diff --git a/README.md b/README.md
@@ -1,25 +1,23 @@
 Semantics of Elrond and Mandos
 ==============================
 
-This repository is work-in-progress, and currently a fork of [KWasm](https://github.com/kframework/wasm-semantics).
+This repository the semantics of the [MultiversX](https://multiversx.com/) (formerly Elrond) blockchain in K on top of WebAssembly semantics ([KWasm](https://github.com/kframework/wasm-semantics)).
 
-Elrond-specific code is in `elrond.md` and `run_elrond_tests.py`.
 
 ## Installation
 
 ### Dependencies
 
 * Python3
-* WABT
+* [WABT v1.0.13](https://github.com/WebAssembly/wabt/tree/1.0.13)
 * K framework ([version](./deps/wasm-semantics/deps/k_release))
-* `pyk` ([version](./deps/wasm-semantics/deps/pyk_release))
-* Crypto++
+* [Poetry](https://python-poetry.org/docs/#installing-with-the-official-installer)
 * Rustup
 * [mxpy](https://docs.multiversx.com/sdk-and-tools/sdk-py/installing-mxpy/)
 
-See [Dockerfile](./Dockerfile) for installation.
+See [Dockerfile](./Dockerfile) for installation details.
 
-### Build
+### Building the semantics
 
 Compile the semantics with:
 
@@ -42,6 +40,39 @@ $ make elrond-clean-sources
 $ make elrond-loaded
 ```
 
+### Installing `kmultiversx`
+
+`kmultiversx` is a Python package providing libraries and CLI tools to interact with the semantics.
+To install `kmultiversx` and its dependencies into a virtual environment, run
+
+```
+# from the project's root directory
+poetry -C kmultiversx install
+```
+
+After the installation, the Python package `kmultiversx` and CLI tools `mandos` and `foundry` will be available via the `poetry run` command
+
+```
+poetry -C run mandos --help
+poetry -C run foundry --help
+```
+
+Or you can activate the virtual environment managed by `poetry` and use the commands directly
+
+```
+poetry -C kmultiversx shell
+mandos --help
+```
+
+Alternatively, you can install `kmultiversx` globally
+
+```
+make -C kmultiversx build
+pip install kmultiversx/dist/*.whl
+mandos --help
+foundry --help
+```
+
 ## Run
 
 To run Mandos tests, first build the contract:
@@ -53,13 +84,13 @@ $ mxpy contract build "<path-to-contract-directory>" --wasm-symbols
 Then run Mandos scenarios with:
 
 ```shell
-$ python3 run_elrond_tests.py <path-to-mandos-file>
+poetry -C kmultiversx run mandos --definition .build/defn/llvm/mandos-kompiled <path-to-mandos-file>
 ```
 
-__Important__: `run_elrond_tests.py` makes use of Python modules implemented in the `wasm-semantics` submodule. For the time being, it requires setting the `PYTHONPATH` environment variable.
+Or with a globally installed instance
 
 ```shell
-$ export PYTHONPATH=$(pwd)/deps/wasm-semantics/binary-parser:$PYTHONPATH
+mandos --definition .build/defn/llvm/mandos-kompiled <path-to-mandos-file>
 ```
 
 Example:
@@ -69,7 +100,7 @@ $ mxpy contract build "deps/mx-sdk-rs/contracts/examples/multisig" --wasm-symbol
 ...
 INFO:projects.core:Build ran.
 INFO:projects.core:WASM file generated: /path/to/multisig/output/multisig.wasm
-$ python3 run_elrond_tests.py deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeBoard.scen.json
+$ mandos deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeBoard.scen.json
 ```
 
 ## Rule Coverage
@@ -214,12 +245,13 @@ Build the test contract by executing
 mxpy contract build <path to test contract>
 ```
 
-Run the `run_foundry.py` script with the test contract's path as the argument:
+
+Run the `foundry` tool with the test contract's path as the argument:
 
 ```shell
-python3 run_foundry.py --directory <path to test contract>
+foundry --definition-dir .build/defn/llvm/foundry-kompiled --directory <path to test contract>
 ```
 
-The `run_foundry.py` script will deploy the test contract using the arguments specified in the `foundry.json` file located in the test directory. It will extract the names and argument types of the test endpoints. Subsequently, the script will test these endpoints using random inputs generated with the `hypothesis` library, enabling fuzz testing. If it encounters an input that falsifies the assertions made in the test cases, it attempts to shrink the input and identify a minimal failing example.
+The `foundry` tool will deploy the test contract using the arguments specified in the `foundry.json` file located in the test directory. It will extract the names and argument types of the test endpoints. Subsequently, the script will test these endpoints using random inputs generated with the `hypothesis` library, enabling fuzz testing. If it encounters an input that falsifies the assertions made in the test cases, it attempts to shrink the input and identify a minimal failing example.
 
 By following these steps, you can efficiently and comprehensively evaluate your Smart Contracts, ensuring their correctness and reliability in various scenarios and inputs.
diff --git a/deps/wasm-semantics b/deps/wasm-semantics