Skip to content

feat: support for snapshot cheatcodes (#427) #494

feat: support for snapshot cheatcodes (#427)

feat: support for snapshot cheatcodes (#427) #494

Workflow file for this run

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-command yices-smt2 --solver-threads 3"
branch: ""
profile: ""
- repo: "morpho-org/morpho-blue"
dir: "morpho-blue"
cmd: "--solver-command yices-smt2 --solver-threads 3"
branch: ""
profile: "test"
- repo: "a16z/cicada"
dir: "cicada"
cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3"
branch: ""
profile: ""
- repo: "a16z/cicada"
dir: "cicada"
cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3"
branch: ""
profile: ""
- repo: "farcasterxyz/contracts"
dir: "farcaster-contracts"
cmd: "--solver-command yices-smt2 --solver-threads 3"
branch: ""
profile: ""
- repo: "zobront/halmos-solady"
dir: "halmos-solady"
cmd: "--function testCheck --solver-command yices-smt2 --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"
- 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"
- 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"
- 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"
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
- 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
- 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 }}