👁️ Halmos symbolic tests #1211
This file contains hidden or 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: 👁️ Halmos symbolic tests | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| schedule: | |
| - cron: "30 3 * * *" | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| halmos: | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| python_version: | |
| - 3.14 | |
| architecture: | |
| - x64 | |
| halmos: | |
| - "--config test/halmos.toml" | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - name: Setup Python | |
| uses: actions/setup-python@v6 | |
| with: | |
| python-version: ${{ matrix.python_version }} | |
| architecture: ${{ matrix.architecture }} | |
| - name: Install Vyper | |
| run: pip install git+https://github.com/vyperlang/vyper.git@master | |
| - name: Show the Vyper version | |
| run: vyper --version | |
| - name: Install Foundry | |
| uses: foundry-rs/foundry-toolchain@v1 | |
| with: | |
| version: nightly | |
| - name: Install `setuptools` | |
| run: pip install setuptools | |
| - name: Install Halmos | |
| run: pip install git+https://github.com/a16z/halmos.git@main | |
| - name: Show the Halmos version | |
| run: halmos --version | |
| - name: Install the Yices 2 SMT solver | |
| run: | | |
| set -Eeuo pipefail | |
| wget -q https://github.com/SRI-CSL/yices2/releases/download/yices-2.7.0/yices-2.7.0-x86_64-pc-linux-gnu-static-gmp.tar.gz | |
| sudo tar -xzf yices-2.7.0-x86_64-pc-linux-gnu-static-gmp.tar.gz --strip-components=2 -C /usr/local/bin yices-2.7.0/bin | |
| rm yices-2.7.0-x86_64-pc-linux-gnu-static-gmp.tar.gz | |
| - name: Install the Bitwuzla SMT solver | |
| run: | | |
| set -Eeuo pipefail | |
| wget -q https://github.com/bitwuzla/bitwuzla/releases/download/0.8.2/Bitwuzla-Linux-x86_64-static.zip | |
| unzip -q Bitwuzla-Linux-x86_64-static.zip | |
| sudo mv Bitwuzla-Linux-x86_64-static/bin/* /usr/local/bin/ | |
| rm -rf Bitwuzla-Linux-x86_64-static.zip Bitwuzla-Linux-x86_64-static | |
| - name: Prioritise the system binaries in `PATH` | |
| run: echo "/usr/local/bin" >> $GITHUB_PATH | |
| - name: Show the Yices 2 SMT solver version | |
| run: yices-smt2 --version | |
| - name: Show the Bitwuzla SMT solver version | |
| run: bitwuzla --version | |
| - name: Install `jsi` | |
| run: pip install just-solve-it | |
| - name: Show the Foundry Halmos config | |
| run: forge config | |
| env: | |
| FOUNDRY_PROFILE: halmos | |
| FOUNDRY_DISABLE_NIGHTLY_WARNING: "1" | |
| - name: Run Halmos ERC-20 symbolic tests | |
| run: halmos --contract ERC20TestHalmos ${{ matrix.halmos }} | |
| env: | |
| FOUNDRY_PROFILE: halmos | |
| FOUNDRY_DISABLE_NIGHTLY_WARNING: "1" | |
| - name: Run Halmos ERC-721 symbolic tests | |
| run: halmos --contract ERC721TestHalmos ${{ matrix.halmos }} | |
| env: | |
| FOUNDRY_PROFILE: halmos | |
| FOUNDRY_DISABLE_NIGHTLY_WARNING: "1" | |
| - name: Run Halmos ERC-1155 symbolic tests | |
| run: halmos --contract ERC1155TestHalmos ${{ matrix.halmos }} | |
| env: | |
| FOUNDRY_PROFILE: halmos | |
| FOUNDRY_DISABLE_NIGHTLY_WARNING: "1" | |
| - name: Run Halmos math symbolic tests | |
| run: halmos --contract MathTestHalmos ${{ matrix.halmos }} | |
| env: | |
| FOUNDRY_PROFILE: halmos | |
| FOUNDRY_DISABLE_NIGHTLY_WARNING: "1" |