Lemmas on Boolean reasoning, set reasoning, map lookup #5965
Workflow file for this run
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: | |
version-bump: | |
name: 'Version Bump' | |
runs-on: ubuntu-latest | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
token: ${{ secrets.JENKINS_GITHUB_PAT }} | |
# fetch-depth 0 means deep clone the repo | |
fetch-depth: 0 | |
ref: ${{ github.event.pull_request.head.sha }} | |
- name: 'Configure GitHub user' | |
run: | | |
git config user.name devops | |
git config user.email devops@runtimeverification.com | |
- name: 'Update version' | |
run: | | |
og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) | |
./package/version.sh bump ${og_version} | |
./package/version.sh sub | |
git add --update && git commit --message "Set Version: $(cat package/version)" || true | |
- name: 'Push updates' | |
run: git push origin HEAD:${GITHUB_HEAD_REF} | |
kevm-pyk-code-quality-checks: | |
needs: version-bump | |
name: 'Code Quality Checks' | |
runs-on: ubuntu-latest | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
- name: 'Install Poetry' | |
uses: Gr1N/setup-poetry@v8 | |
- name: 'Run code quality checks' | |
run: make -C kevm-pyk check | |
- name: 'Run pyupgrade' | |
run: make -C kevm-pyk pyupgrade | |
kevm-pyk-unit-tests: | |
needs: kevm-pyk-code-quality-checks | |
name: 'Unit Tests' | |
runs-on: ubuntu-latest | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: true | |
fetch-depth: 0 | |
- name: 'Install Poetry' | |
uses: Gr1N/setup-poetry@v8 | |
- name: 'Build kevm' | |
run: make build-kevm -j8 | |
- name: 'Run unit tests' | |
run: | | |
export PATH=$(pwd)/.build/usr/bin:${PATH} | |
make -C kevm-pyk cov-unit | |
kevm-pyk-profile: | |
needs: kevm-pyk-code-quality-checks | |
name: 'Profiling' | |
runs-on: [self-hosted, linux, normal] | |
timeout-minutes: 15 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
fetch-depth: 0 | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-profile-${{ github.sha }} | |
- name: 'Build kevm-pyk' | |
run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make poetry' | |
- name: 'Build Foundry' | |
run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make build-foundry' | |
- name: 'Run profiling' | |
run: | | |
docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make profile' | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-ci-profile-${GITHUB_SHA} | |
test-concrete-execution: | |
name: 'Build and Test KEVM concrete execution' | |
needs: kevm-pyk-code-quality-checks | |
runs-on: [self-hosted, linux, normal] | |
timeout-minutes: 45 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
fetch-depth: 0 | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-concrete-${{ github.sha }} | |
- name: 'Build kevm-pyk' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make poetry' | |
- name: 'Build blockchain-k-plugin-deps' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make CXX=clang++-14 plugin-deps' | |
- name: 'Build kevm' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make build-kevm build-haskell build-llvm build-node -j`nproc` RELEASE=true' | |
- name: 'Test kevm-pyk' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-integration' | |
- name: 'Test conformance' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-conformance' | |
- name: 'Test llvm krun' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-interactive-run TEST_CONCRETE_BACKEND=llvm' | |
- name: 'Test node' | |
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-node -j`nproc`' | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-ci-concrete-${GITHUB_SHA} | |
test-prove-haskell: | |
name: 'Build and Test KEVM haskell proofs' | |
needs: kevm-pyk-code-quality-checks | |
runs-on: [self-hosted, linux, normal] | |
timeout-minutes: 120 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
fetch-depth: 0 | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-haskell-${{ github.sha }} | |
- name: 'Prove Haskell' | |
run: docker exec -u github-user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove' | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-ci-haskell-${GITHUB_SHA} | |
test-prove-foundry: | |
name: 'Build and Test KEVM Foundry proofs' | |
needs: kevm-pyk-code-quality-checks | |
runs-on: [self-hosted, linux, normal] | |
timeout-minutes: 150 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
fetch-depth: 0 | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-foundry-${{ github.sha }} | |
- name: 'Build kevm-pyk' | |
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make poetry' | |
- name: 'Build Foundry' | |
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2' | |
- name: 'Foundry Prove' | |
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS=-vv' | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-ci-foundry-${GITHUB_SHA} | |
test-prove-foundry-booster: | |
name: 'Build and Test KEVM Foundry proofs (booster)' | |
needs: kevm-pyk-code-quality-checks | |
runs-on: [self-hosted, linux, normal] | |
timeout-minutes: 150 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
fetch-depth: 0 | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-booster-${{ github.sha }} | |
- name: 'Build kevm-pyk' | |
run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make poetry' | |
- name: 'Build blockchain-k-plugin-deps' | |
run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make CXX=clang++-14 plugin-deps' | |
- name: 'Build Foundry' | |
run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2' | |
- name: 'Foundry Prove' | |
run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS="-vv --use-booster"' | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-ci-booster-${GITHUB_SHA} | |
nix: | |
name: 'Nix' | |
strategy: | |
fail-fast: false | |
matrix: | |
include: | |
- runner: normal | |
- runner: macos-13 | |
- runner: ARM64 | |
needs: kevm-pyk-code-quality-checks | |
runs-on: ${{ matrix.runner }} | |
timeout-minutes: 60 | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
# Check out pull request HEAD instead of merge commit. | |
ref: ${{ github.event.pull_request.head.sha }} | |
- name: 'Install Nix' | |
if: ${{ matrix.runner == 'macos-13' }} | |
uses: cachix/install-nix-action@v19 | |
with: | |
install_url: https://releases.nixos.org/nix/nix-2.13.3/install | |
extra_nix_config: | | |
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} | |
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 == 'macos-13' }} | |
uses: cachix/cachix-action@v12 | |
with: | |
name: k-framework | |
authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }} | |
- name: 'Build KEVM' | |
run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs | |
- name: 'Test KEVM' | |
run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kevm-test | |
build-deb-package: | |
name: 'Build Ubuntu Jammy DockerHub Image' | |
runs-on: [self-hosted, linux, normal] | |
needs: kevm-pyk-code-quality-checks | |
steps: | |
- name: 'Check out code' | |
uses: actions/checkout@v3 | |
with: | |
submodules: recursive | |
ref: ${{ github.event.push.head.sha }} | |
- name: 'Set up Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-package-jammy-${{ github.sha }} | |
- name: 'Build Package' | |
run: | | |
set -euxo pipefail | |
version=$(cat package/version) | |
docker exec -u github-user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'package/debian/package jammy' | |
docker cp kevm-package-jammy-${GITHUB_SHA}:/home/github-user/kevm_${version}_amd64.deb ./ | |
- name: 'Setup Foundry Test Docker' | |
uses: ./.github/actions/with-docker | |
with: | |
container-name: kevm-ci-test-${{ github.sha }} | |
dockerfile: package/docker/Dockerfile | |
- name: 'KEVM Foundry Test' | |
run: | | |
set -euxo pipefail | |
docker cp ./tests/foundry kevm-ci-test-${GITHUB_SHA}:/home/github-user/foundry | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "sudo chown github-user:github-user -R /home/github-user/foundry" | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "forge build --root /home/github-user/foundry" | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "kevm foundry-kompile --foundry-project-root /home/github-user/foundry --verbose" | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "kevm foundry-prove --foundry-project-root /home/github-user/foundry --verbose --test AssertTest.test_assert_true_branch" | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "kevm foundry-show --foundry-project-root /home/github-user/foundry --verbose AssertTest.test_assert_true_branch" | |
docker exec -u github-user kevm-ci-test-${GITHUB_SHA} /bin/bash -c "kevm foundry-list --foundry-project-root /home/github-user/foundry --verbose" | |
- name: 'Tear down Docker' | |
if: always() | |
run: | | |
docker stop --time=0 kevm-package-jammy-${GITHUB_SHA} | |
docker stop --time=0 kevm-ci-test-${GITHUB_SHA} |