Skip to content

Commit

Permalink
Merge branch 'main' into chore-workflows
Browse files Browse the repository at this point in the history
  • Loading branch information
karmacoma-eth authored Jul 17, 2024
2 parents f184c07 + 40cf25a commit d2aff0e
Show file tree
Hide file tree
Showing 19 changed files with 828 additions and 145 deletions.
60 changes: 52 additions & 8 deletions .github/workflows/test-external.yml
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,13 @@ on:
branches: [main]
paths:
- .github/workflows/test-external.yml
# pull_request:
# branches: [main]
workflow_dispatch:
inputs:
halmos-options:
description: "additional halmos options"
required: false
type: string
default: ""

jobs:
test:
Expand All @@ -16,27 +20,38 @@ jobs:
strategy:
fail-fast: false
matrix:
include:
cache-solver: ["", "--cache-solver"]
project:
- repo: "morpho-org/morpho-data-structures"
dir: "morpho-data-structures"
cmd: "halmos --function testProve --loop 4 --symbolic-storage"
branch: ""
profile: ""
- repo: "a16z/cicada"
dir: "cicada"
cmd: "halmos --contract LibUint1024Test --function testProve --loop 256"
branch: ""
profile: ""
- repo: "a16z/cicada"
dir: "cicada"
cmd: "halmos --contract LibPrimeTest --function testProve --loop 256"
branch: ""
profile: ""
- repo: "farcasterxyz/contracts"
dir: "farcaster-contracts"
cmd: "halmos"
branch: ""
profile: ""
- repo: "zobront/halmos-solady"
dir: "halmos-solady"
cmd: "halmos --function testCheck"
branch: ""
profile: ""
- repo: "pcaversaccio/snekmate"
dir: "snekmate"
cmd: "halmos --config test/halmos.toml"
branch: ""
profile: "halmos"

steps:
- name: Checkout
Expand All @@ -49,11 +64,40 @@ jobs:
- name: Checkout external repo
uses: actions/checkout@v4
with:
repository: ${{ matrix.repo }}
path: ${{ matrix.dir }}
ref: ${{ matrix.branch }}
repository: ${{ matrix.project.repo }}
path: ${{ matrix.project.dir }}
ref: ${{ matrix.project.branch }}
submodules: recursive

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1

- name: Set up Python
uses: actions/setup-python@v5
with:
python-version: "3.12"

- name: Install dependencies
run: python -m pip install --upgrade pip

- name: Install Halmos
run: python -m pip install -e ./halmos

- name: Install Vyper
if: ${{ matrix.project.dir == 'snekmate' }}
run: python -m pip install vyper

- name: Install Yices 2 SMT solver
run: |
wget https://github.com/SRI-CSL/yices2/releases/download/Yices-2.6.4/yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
tar -xzvf yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
sudo mv yices-2.6.4/bin/* /usr/local/bin/
sudo mv yices-2.6.4/lib/* /usr/local/lib/
sudo mv yices-2.6.4/include/* /usr/local/include/
rm -rf yices-2.6.4
- name: Test external repo
run: ${{ matrix.cmd }} --statistics --debug --solver-timeout-assertion 0 --solver-threads 4 --solver-command=yices-smt2
working-directory: ${{ matrix.dir }}
run: ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
working-directory: ${{ matrix.project.dir }}
env:
FOUNDRY_PROFILE: ${{ matrix.project.profile }}
19 changes: 13 additions & 6 deletions .github/workflows/test-long.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,12 @@ on:
paths:
- .github/workflows/test-long.yml
workflow_dispatch:
inputs:
halmos-options:
description: "additional halmos options"
required: false
type: string
default: ""

jobs:
test:
Expand All @@ -14,11 +20,12 @@ jobs:
strategy:
fail-fast: false
matrix:
include:
- testname: "tests/solver"
- testname: "examples/simple"
- testname: "examples/tokens/ERC20"
- testname: "examples/tokens/ERC721"
cache-solver: ["", "--cache-solver"]
testname:
- "tests/solver"
- "examples/simple"
- "examples/tokens/ERC20"
- "examples/tokens/ERC721"

steps:
- name: Login to GitHub Container Registry
Expand All @@ -39,4 +46,4 @@ jobs:
- name: Run pytest
run: |
docker run -v .:/workspace --entrypoint pytest halmos -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-v -st --solver-timeout-assertion 0 --solver-threads 6 --solver-command=yices-smt2' -s --log-cli-level=
docker run -v .:/workspace --entrypoint pytest halmos -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level=
13 changes: 12 additions & 1 deletion .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,17 @@ on:
pull_request:
branches: [main]
workflow_dispatch:
inputs:
halmos-options:
description: "additional halmos options"
required: false
type: string
default: ""
pytest-options:
description: "additional pytest options"
required: false
type: string
default: ""

jobs:
test:
Expand Down Expand Up @@ -44,4 +55,4 @@ jobs:
run: python -m pip install -e .

- name: Run pytest
run: pytest -n 4 -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} --solver-timeout-assertion 0"
run: pytest -n 4 -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}
3 changes: 2 additions & 1 deletion examples/simple/foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ src = 'src'
out = 'out'
libs = ["../../tests/lib", 'lib']

# See more config options https://github.com/foundry-rs/foundry/tree/master/config
evm_version = 'cancun'

force = false
# compile options used by halmos (to prevent unnecessary recompilation when running forge test and halmos together)
extra_output = ["storageLayout", "metadata"]
2 changes: 2 additions & 0 deletions examples/tokens/ERC20/foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@
src = "src"
out = "out"
libs = ["../../../tests/lib", "lib"]

evm_version = 'cancun'
2 changes: 2 additions & 0 deletions examples/tokens/ERC721/foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@
src = "src"
out = "out"
libs = ["../../../tests/lib", "lib"]

evm_version = 'cancun'
Loading

0 comments on commit d2aff0e

Please sign in to comment.