Option --extra-module for including lemmas modules dynamically in kontrol prove
#5018
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| --- | |
| name: 'Test PR' | |
| on: | |
| pull_request: | |
| branches: | |
| - 'master' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| code-quality-checks: | |
| name: 'Code Quality Checks' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| - name: 'Install Poetry' | |
| uses: Gr1N/setup-poetry@v8 | |
| - name: 'Run code quality checks' | |
| run: make check | |
| - name: 'Run pyupgrade' | |
| run: make pyupgrade | |
| unit-tests: | |
| needs: code-quality-checks | |
| name: 'Unit Tests' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| - name: 'Install Poetry' | |
| uses: Gr1N/setup-poetry@v8 | |
| - name: 'Run unit tests' | |
| run: make cov-unit | |
| profile: | |
| needs: code-quality-checks | |
| name: 'Profiling' | |
| runs-on: [self-hosted, linux, normal] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: ['legacy', 'booster'] | |
| timeout-minutes: 30 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-profile-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.foundry' | |
| - name: 'Run profiling' | |
| run: | | |
| PROF_ARGS=--numprocesses=8 | |
| [ ${{ matrix.backend }} == 'legacy' ] && PROF_ARGS+=' --no-use-booster' | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-profile-${GITHUB_SHA} | |
| integration-tests: | |
| needs: code-quality-checks | |
| name: 'Integration Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: ['legacy', 'booster'] | |
| timeout-minutes: 120 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-integration-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' | |
| - name: 'Run integration tests' | |
| run: | | |
| TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)"' | |
| if [ ${{ matrix.backend }} == 'legacy' ]; then | |
| TEST_ARGS+=' --no-use-booster --numprocesses=6' | |
| else | |
| TEST_ARGS+=' --numprocesses=4' | |
| fi | |
| docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA} | |
| cse-tests: | |
| needs: code-quality-checks | |
| name: 'CSE Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| timeout-minutes: 120 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-integration-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' | |
| - name: 'Run CSE and Minimize tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=8 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"' | |
| docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA} | |
| end-to-end-tests: | |
| needs: code-quality-checks | |
| name: 'End to End Sanity Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| timeout-minutes: 35 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-integration-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' | |
| - name: 'Run end-to-end tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_end_to_end"' | |
| docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA} | |
| docker: | |
| needs: code-quality-checks | |
| name: 'Docker Tests' | |
| runs-on: [self-hosted, linux, normal] | |
| timeout-minutes: 30 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set environment' | |
| run: | | |
| echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}" >> ${GITHUB_ENV} | |
| echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV} | |
| echo "DOCKER_USER=user" >> ${GITHUB_ENV} | |
| echo "DOCKER_GROUP=user" >> ${GITHUB_ENV} | |
| echo "FOUNDRY_ROOT=/home/user/foundry" >> ${GITHUB_ENV} | |
| - name: 'Build Docker image' | |
| run: | | |
| K_VERSION=$(cat deps/k_release) | |
| Z3_VERSION=$(cat deps/z3) | |
| docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION} | |
| - name: 'Start Docker container' | |
| run: | | |
| docker run \ | |
| --name ${CONTAINER_NAME} \ | |
| --rm \ | |
| --interactive \ | |
| --tty \ | |
| --detach \ | |
| --user root \ | |
| ${IMAGE_TAG} | |
| docker cp src/tests/integration/test-data/foundry ${CONTAINER_NAME}:${FOUNDRY_ROOT} | |
| docker exec ${CONTAINER_NAME} chown -R ${DOCKER_USER}:${DOCKER_GROUP} ${FOUNDRY_ROOT} | |
| - name: 'Run forge build' | |
| run: | | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git foundry-rs/forge-std@75f1746 | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git runtimeverification/kontrol-cheatcodes@a5dd4b0 | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge build | |
| - name: 'Run kontrol build' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build -O2 | |
| - name: 'Run kontrol prove' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()' | |
| - name: 'Run kontrol show' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()' | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 ${CONTAINER_NAME} | |
| nix: | |
| needs: code-quality-checks | |
| name: 'Nix Tests' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| runner: [ubuntu-latest, macos-13, MacM1] # MacM1 is self-hosted | |
| runs-on: ${{ matrix.runner }} | |
| timeout-minutes: 60 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Install Nix' | |
| if: ${{ matrix.runner != 'MacM1' }} | |
| uses: cachix/install-nix-action@v22 | |
| with: | |
| install_url: https://releases.nixos.org/nix/nix-2.13.3/install | |
| extra_nix_config: | | |
| substituters = http://cache.nixos.org https://cache.iog.io | |
| trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= | |
| - name: 'Install Cachix' | |
| if: ${{ matrix.runner != 'MacM1' }} | |
| uses: cachix/cachix-action@v12 | |
| with: | |
| name: k-framework | |
| - name: 'Build Kontrol' | |
| env: | |
| NIX_PATH: 'nixpkgs=http://nixos.org/channels/nixos-22.05/nixexprs.tar.xz' | |
| GC_DONT_GC: '1' | |
| run: | | |
| set -euxo pipefail | |
| nix --version | |
| JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/jq | |
| KONTROL_BIN=$(nix build .#kontrol.solc_0_8_13 --print-build-logs --json | $JQ -r '.[].outputs | to_entries[].value')/bin | |
| echo $KONTROL_BIN >> $GITHUB_PATH | |
| - name: 'Run smoke test' | |
| run: cd package && ./test-package.sh |