Skip to content

Commit

Permalink
πŸ‘·β€β™‚οΈ Add venom-Based CI Tests (#268)
Browse files Browse the repository at this point in the history
### πŸ•“ Changelog

This PR integrates `venom`-based unit, stateless, and stateful fuzzing
(incl. Echidna) tests, and Halmos-based symbolic tests into the CI
pipeline.

---------

Signed-off-by: sudo rm -rf --no-preserve-root / <pcaversaccio@users.noreply.github.com>
  • Loading branch information
pcaversaccio authored Oct 7, 2024
1 parent ceb76b5 commit c91e80a
Show file tree
Hide file tree
Showing 5 changed files with 255 additions and 2 deletions.
87 changes: 87 additions & 0 deletions .github/workflows/halmos-venom.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
name: βš—οΈ Venom-based Halmos symbolic tests

on:
schedule:
- cron: "30 3 * * *"
workflow_dispatch:

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

jobs:
halmos:
runs-on: ${{ matrix.os }}
strategy:
matrix:
os:
- ubuntu-latest
python_version:
- 3.12
architecture:
- x64
halmos:
- "--config test/halmos.toml"

steps:
- name: Checkout
uses: actions/checkout@v4
with:
submodules: recursive

- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python_version }}
architecture: ${{ matrix.architecture }}

- name: Install Vyper
run: pip install git+https://github.com/vyperlang/vyper@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 Yices 2 SMT solver
run: |
wget -q https://github.com/SRI-CSL/yices2/releases/download/Yices-2.6.4/yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
sudo tar -xzf yices-2.6.4-x86_64-pc-linux-gnu.tar.gz -C /usr/local --strip-components=1
sudo rm yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
- name: Show the Foundry Halmos config
run: forge config
env:
FOUNDRY_PROFILE: halmos-venom

- name: Run Halmos ERC-20 symbolic tests
run: halmos --contract ERC20TestHalmos ${{ matrix.halmos }}
env:
FOUNDRY_PROFILE: halmos-venom

- name: Run Halmos ERC-721 symbolic tests
run: halmos --contract ERC721TestHalmos ${{ matrix.halmos }}
env:
FOUNDRY_PROFILE: halmos-venom

- name: Run Halmos ERC-1155 symbolic tests
run: halmos --contract ERC1155TestHalmos ${{ matrix.halmos }}
env:
FOUNDRY_PROFILE: halmos-venom

- name: Run Halmos math symbolic tests
run: halmos --contract MathTestHalmos ${{ matrix.halmos }}
env:
FOUNDRY_PROFILE: halmos-venom
118 changes: 118 additions & 0 deletions .github/workflows/test-contracts-venom.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
name: πŸ§ͺ Venom-based smart contract tests

on: [push, pull_request, workflow_dispatch]

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

jobs:
tests:
runs-on: ${{ matrix.os }}
strategy:
matrix:
os:
- ubuntu-latest
python_version:
- 3.12
architecture:
- x64
node_version:
- 20
echidna:
- "--config test/echidna.yaml"

steps:
- name: Checkout
uses: actions/checkout@v4
with:
submodules: recursive

- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python_version }}
architecture: ${{ matrix.architecture }}

- name: Install Vyper
run: pip install git+https://github.com/vyperlang/vyper@master

- name: Install pnpm
uses: pnpm/action-setup@v3
with:
version: latest
run_install: false

- name: Get pnpm cache directory path
id: pnpm-cache-dir-path
run: echo "dir=$(pnpm store path --silent)" >> $GITHUB_OUTPUT

- name: Restore pnpm cache
uses: actions/cache@v4
id: pnpm-cache
with:
path: ${{ steps.pnpm-cache-dir-path.outputs.dir }}
key: ${{ runner.os }}-pnpm-store-${{ hashFiles('**/pnpm-lock.yaml') }}
restore-keys: ${{ runner.os }}-pnpm-store-

- name: Use Node.js ${{ matrix.node_version }}
uses: actions/setup-node@v4
with:
node-version: ${{ matrix.node_version }}

- name: Install pnpm project with a clean slate
run: pnpm install --prefer-offline --frozen-lockfile

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

- name: Show the Foundry CI config
run: forge config
env:
FOUNDRY_PROFILE: ci-venom

- name: Foundry tests
run: forge test
env:
FOUNDRY_PROFILE: ci-venom

- name: Show the Foundry default config
run: forge config
env:
FOUNDRY_PROFILE: default-venom

- name: Run snapshot
run: NO_COLOR=1 forge snapshot >> $GITHUB_STEP_SUMMARY
env:
FOUNDRY_PROFILE: default-venom

- name: Install Homebrew
uses: Homebrew/actions/setup-homebrew@master

- name: Install Echidna
run: brew install echidna

- name: Show the Echidna version
run: echidna --version

- name: Show the Foundry Echidna config
run: forge config
env:
FOUNDRY_PROFILE: echidna-venom

- name: Compile the Echidna test contracts
run: forge build --build-info
env:
FOUNDRY_PROFILE: echidna-venom

- name: Run Echidna ERC-20 property tests
run: echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness ${{ matrix.echidna }}
env:
FOUNDRY_PROFILE: echidna-venom

- name: Run Echidna ERC-721 property tests
run: echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness ${{ matrix.echidna }}
env:
FOUNDRY_PROFILE: echidna-venom
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,8 @@

### πŸ₯’ Test Coverage

- All 🐍 snekmate contract tests, i.e. unit tests, stateless and stateful fuzzing tests (including Echidna), and Halmos-based symbolic tests, are now also run against the experimental Venom backend. ([#268](https://github.com/pcaversaccio/snekmate/pull/268))

- **Tokens**
- [`erc20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc20.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273))
- [`erc721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc721.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273))
Expand Down
24 changes: 24 additions & 0 deletions foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -37,3 +37,27 @@ evm_version = "shanghai" # Set the EVM t
[profile.halmos]
force = true # Perform always a clean build.
evm_version = "shanghai" # Set the EVM target version to `shanghai`.

# Default overrides for the Venom-based tests.
[profile.default-venom]
vyper = { experimental_codegen = true } # Enable experimental code generation using the Venom backend.

# Default overrides for the Venom-based CI tests.
[profile.ci-venom]
force = true # Perform always a clean build.
verbosity = 4 # Increase the verbosity level for the tests.
fuzz = { runs = 10_000, max_test_rejects = 350_000 } # Increase the number of fuzz runs and maximum number of combined inputs that may be rejected for the tests.
invariant = { runs = 375, depth = 500 } # Increase the number of runs (while preserving the default depth) for each invariant test group.
vyper = { experimental_codegen = true } # Enable experimental code generation using the Venom backend.

# Default overrides for the the Venom-based Echidna tests.
[profile.echidna-venom]
force = true # Perform always a clean build.
evm_version = "shanghai" # Set the EVM target version to `shanghai`.
vyper = { experimental_codegen = true } # Enable experimental code generation using the Venom backend.

# Default overrides for the Venom-based Halmos tests.
[profile.halmos-venom]
force = true # Perform always a clean build.
evm_version = "shanghai" # Set the EVM target version to `shanghai`.
vyper = { experimental_codegen = true } # Enable experimental code generation using the Venom backend.
26 changes: 24 additions & 2 deletions lib/utils/compile.py
Original file line number Diff line number Diff line change
@@ -1,8 +1,30 @@
import sys, subprocess

result = subprocess.run(["vyper"] + sys.argv[1:], capture_output=True, text=True)

# Check if `experimental_codegen` is enabled in the
# Foundry profile.
def is_experimental_codegen():
return (
subprocess.run(
["bash", "-c", 'forge config --json | jq -r ".vyper.experimental_codegen"'],
capture_output=True,
text=True,
)
.stdout.strip()
.lower()
== "true"
)


# Build the Vyper command.
command = (
["vyper", "--experimental-codegen"] if is_experimental_codegen() else ["vyper"]
)
command += sys.argv[1:]

result = subprocess.run(command, capture_output=True, text=True)
if result.returncode != 0:
raise Exception("Error compiling: " + sys.argv[1])
raise Exception(f"Error compiling: {sys.argv[1]}")

# Remove any leading and trailing whitespace characters
# from the compilation result.
Expand Down

0 comments on commit c91e80a

Please sign in to comment.