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
@@ -7,29 +7,36 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  python-code-quality-checks:
+    name: 'Code Quality Checks'
+    runs-on: ubuntu-latest
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:    
+          submodules: recursive
+      - name: 'Install Poetry'
+        uses: Gr1N/setup-poetry@v8
+      - name: 'Build and run code quality checks'
+        run: make -C kmultiversx check
   simple-tests:
     runs-on: [self-hosted, linux, normal]
     name: 'Simple Tests'
+    needs: [python-code-quality-checks]
     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 +54,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 +81,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 +110,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