fix: immediately halt execution on assert(false) (#572) #624
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: Test external projects | |
| on: | |
| push: | |
| branches: [main, chore-workflows] | |
| workflow_dispatch: | |
| inputs: | |
| halmos-options: | |
| description: "additional halmos options" | |
| required: false | |
| type: string | |
| default: "" | |
| jobs: | |
| test: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| cache-solver: ["", "--cache-solver"] | |
| project: | |
| - repo: "morpho-org/morpho-data-structures" | |
| dir: "morpho-data-structures" | |
| cmd: "--function testProve --loop 4 --solver-threads 3 --disable-gc" | |
| branch: "" | |
| profile: "" | |
| - repo: "morpho-org/morpho-blue" | |
| dir: "morpho-blue" | |
| cmd: "--solver-threads 3" | |
| branch: "" | |
| profile: "test" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "farcasterxyz/contracts" | |
| dir: "farcaster-contracts" | |
| cmd: "--solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "zobront/halmos-solady" | |
| dir: "halmos-solady" | |
| cmd: "--function testCheck --solver bitwuzla --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos-venom" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos-venom" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos-venom" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos-venom" | |
| - repo: "daejunpark/sys-asm-halmos" | |
| dir: "sys-asm-halmos" | |
| cmd: "--solver-threads 3 --loop 2" | |
| branch: "" | |
| profile: "" | |
| steps: | |
| - name: Checkout halmos | |
| uses: actions/checkout@v4 | |
| with: | |
| # we won't be needing tests/lib for this workflow | |
| submodules: false | |
| - name: Build image | |
| run: docker build -t halmos-image . --file packages/halmos/Dockerfile | |
| - name: Run foundryup | |
| run: | | |
| # run foundryup in halmos-image, save the result as a new image | |
| docker run --name halmos-image-foundryup halmos-image foundryup | |
| # commit the result back to halmos-image | |
| docker commit halmos-image-foundryup halmos-image | |
| # for snekmate | |
| - name: Install Vyper | |
| if: ${{ matrix.project.dir == 'snekmate' }} | |
| run: | | |
| docker run --name halmos-image-vyper halmos-image uv pip install git+https://github.com/vyperlang/vyper@master | |
| docker commit halmos-image-vyper halmos-image | |
| # for sys-asm-halmos | |
| - name: Install Geas | |
| run: | | |
| docker run --name tmp-halmos-image halmos-image bash -c "\ | |
| apt-get update && \ | |
| apt-get install -y golang-go && \ | |
| go version && \ | |
| env 'GOBIN=/halmos/bin' go install github.com/fjl/geas/cmd/geas@latest && \ | |
| geas -h" | |
| docker commit tmp-halmos-image halmos-image | |
| - name: Checkout external repo | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: ${{ matrix.project.repo }} | |
| path: ${{ matrix.project.dir }} | |
| ref: ${{ matrix.project.branch }} | |
| submodules: recursive | |
| - name: Print forge version | |
| run: docker run halmos-image forge --version | |
| - name: Print halmos version | |
| run: docker run halmos-image halmos --version | |
| - name: Test external repo | |
| run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} | |
| working-directory: ${{ matrix.project.dir }} | |
| env: | |
| FOUNDRY_PROFILE: ${{ matrix.project.profile }} |