Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions .github/workflows/medusa.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,16 @@ jobs:
- name: Go setup
uses: actions/setup-go@v4
with:
go-version: "^1.18.1"
go-version: "^1.18.1"

- name: Install medusa
run: |
git clone https://github.com/crytic/medusa.git
cd medusa
go build -o medusa -v .
go install -v .
sudo cp medusa /usr/bin
pip install crytic-compile
git clone https://github.com/crytic/medusa.git
cd medusa
go build -o medusa -v .
go install -v .
sudo cp medusa /usr/bin
pip install crytic-compile

- name: Compile ERC20 Foundry example
working-directory: tests/ERC20/foundry
Expand All @@ -52,7 +52,7 @@ jobs:
run: |
medusa fuzz --target-contracts CryticERC20ExternalHarness --config medusa-config-ext.json

- name: Compile ERC4646 Foundry example
- name: Compile ERC4626 Foundry example
working-directory: tests/ERC4626/foundry
run: forge build --build-info

Expand Down Expand Up @@ -90,16 +90,16 @@ jobs:
- name: Go setup
uses: actions/setup-go@v4
with:
go-version: "^1.18.1"
go-version: "^1.18.1"

- name: Install medusa
run: |
git clone https://github.com/crytic/medusa.git
cd medusa
go build -o medusa -v .
go install -v .
sudo cp medusa /usr/bin
pip install crytic-compile
git clone https://github.com/crytic/medusa.git
cd medusa
go build -o medusa -v .
go install -v .
sudo cp medusa /usr/bin
pip install crytic-compile

- name: Run Medusa for Internal ERC20 tests
working-directory: tests/ERC20/hardhat
Expand Down
88 changes: 88 additions & 0 deletions CLAUDE.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
# CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

## Project Overview

This repository by Trail of Bits provides 168 pre-made Solidity property tests for fuzz testing smart contracts with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa). It covers:
- ERC20 tokens (25 properties)
- ERC721 tokens (19 properties)
- ERC4626 vaults (37 properties)
- ABDKMath64x64 fixed-point library (106 properties)

## Build Commands

**Root level (Foundry):**
```bash
forge build # Compile contracts
```

**Root level (Hardhat):**
```bash
npm install # Install dependencies
npm run compile # Compile contracts
```

**Linting and formatting:**
```bash
npm run format # Format code with Prettier
npm run lint # Check formatting and markdown links
```

## Running Fuzz Tests

Tests are organized in `tests/<standard>/<framework>/` directories (e.g., `tests/ERC20/foundry/`).

**Echidna (from test directory):**
```bash
# Internal testing
echidna . --contract CryticERC20InternalHarness --config echidna-config.yaml

# External testing
echidna . --contract CryticERC20ExternalHarness --config echidna-config-ext.yaml
```

**Medusa (from test directory):**
```bash
# Build first
forge build --build-info

# Run fuzzer
medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-config.json
```

## Architecture

### Directory Structure
- `contracts/` - Property contracts by standard
- `ERC20/`, `ERC721/`, `ERC4626/` - Each split into `internal/` and `external/` testing
- `Math/ABDKMath64x64/` - Fixed-point math properties
- `util/` - Helper functions (PropertiesHelper.sol, Hevm.sol, PropertiesConstants.sol)
- `tests/` - Example test harnesses for Foundry and Hardhat
- `PROPERTIES.md` - Complete property reference table

### Testing Approaches

**Internal testing**: Test contract inherits from both the token and property contracts. Properties access internal state directly.

**External testing**: Separate harness contract interacts with token through its external interface. Requires `allContracts: true` in Echidna config.

### Key Patterns

1. **Harness contracts** inherit from `CryticERC*Properties` and initialize test state (mint to USER1, USER2, USER3)
2. **PropertiesConstants** provides standard addresses: `USER1=0x10000`, `USER2=0x20000`, `USER3=0x30000`, `INITIAL_BALANCE=1000e18`
3. **PropertiesHelper** provides `assertEq`, `assertWithMsg`, `clampBetween`, and `LogXxx` events for debugging
4. **Echidna/Medusa configs** use assertion mode (`testMode: assertion`) with deployer `0x10000`

## Adding New Properties

1. Add property to appropriate file in `contracts/<standard>/internal/properties/` and `external/properties/`
2. For external properties, update the interface in `contracts/<standard>/util/`
3. Add test in `contracts/<standard>/*/test/` to verify property catches violations
4. Update `PROPERTIES.md` table
5. Update `contracts/<standard>/README.md` if present

## Branch Naming

- Features: `dev-<description>` (e.g., `dev-add-properties-for-erc20-transfers`)
- Bug fixes: `fix-<description>` (e.g., `fix-typo-in-readme`)
10 changes: 5 additions & 5 deletions PROPERTIES.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ This file lists all the currently implemented Echidna property tests for ERC20,
- [Tests for mintable tokens](#tests-for-mintable-tokens)
- [Tests for pausable tokens](#tests-for-pausable-tokens)
- [Tests for tokens implementing `increaseAllowance` and `decreaseAllowance`](#tests-for-tokens-implementing-increaseallowance-and-decreaseallowance)
- [ERC721](#erc721)
- [ERC721](#erc721)
- [Basic properties for standard functions](#basic-properties-for-standard-functions-1)
- [Tests for burnable tokens](#tests-for-burnable-tokens-1)
- [Tests for mintable tokens](#tests-for-mintable-tokens-1)
Expand Down Expand Up @@ -55,14 +55,14 @@ This file lists all the currently implemented Echidna property tests for ERC20,

| ID | Name | Invariant tested |
| ------------------ | ------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------ |
| ERC20-MINTABLE-001 | [test_ERC20_mintTokens](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20MintableProperties.sol#L19) | User balance and total supply should be updated correctly after minting. |
| ERC20-MINTABLE-001 | [test_ERC20_mintTokens](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20MintableProperties.sol#L18) | User balance and total supply should be updated correctly after minting. |

### Tests for pausable tokens

| ID | Name | Invariant tested |
| ------------------ | --------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------- |
| ERC20-PAUSABLE-001 | [test_ERC20_pausedTransfer](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20PausableProperties.sol#L35) | Token `transfer`s should not be possible when paused state is enabled. |
| ERC20-PAUSABLE-002 | [test_ERC20_pausedTransferFrom](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20PausableProperties.sol#L52) | Token `transferFrom`s should not be possible when paused state is enabled. |
| ERC20-PAUSABLE-001 | [test_ERC20_pausedTransfer](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20PausableProperties.sol#L37) | Token `transfer`s should not be possible when paused state is enabled. |
| ERC20-PAUSABLE-002 | [test_ERC20_pausedTransferFrom](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20PausableProperties.sol#L62) | Token `transferFrom`s should not be possible when paused state is enabled. |

### Tests for tokens implementing `increaseAllowance` and `decreaseAllowance`

Expand Down Expand Up @@ -113,7 +113,7 @@ This file lists all the currently implemented Echidna property tests for ERC20,
| ID | Name | Invariant tested |
| ----------- | ---------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------- |
| ERC4626-001 | [verify_assetMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L10) | `asset` must not revert. |
| ERC4626-002 | [verify_totalAssetsMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L20) | `totalAssets` must not revert. |
| ERC4626-002 | [verify_totalAssetsMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L23) | `totalAssets` must not revert. |
| ERC4626-003 | [verify_convertToAssetsMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L30) | `convertToAssets` must not revert for reasonable values. |
| ERC4626-004 | [verify_convertToSharesMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L54) | `convertToShares` must not revert for reasonable values. |
| ERC4626-005 | [verify_maxDepositMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L71) | `maxDeposit` must not revert. |
Expand Down
19 changes: 17 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,24 @@
- [Properties](#properties)
- [Testing the properties with fuzzing](#testing-the-properties-with-fuzzing)
- [ERC20 tests](#erc20-tests)
- [ERC721 Tests](#erc721-tests)
- [Integration](#integration)
- [Configuration](#configuration)
- [Run](#run)
- [Example: Output for a compliant token](#example-output-for-a-compliant-token)
- [Example: Output for a non-compliant token](#example-output-for-a-non-compliant-token)
- [ERC721 tests](#erc721-tests)
- [Integration](#integration-1)
- [Configuration](#configuration-1)
- [Run](#run-1)
- [Example: Output for a compliant token](#example-output-for-a-compliant-token-1)
- [Example: Output for a non-compliant token](#example-output-for-a-non-compliant-token-1)
- [ERC4626 Tests](#erc4626-tests)
- [Integration](#integration-2)
- [Configuration](#configuration-2)
- [Run](#run-2)
- [ABDKMath64x64 tests](#abdkmath64x64-tests)
- [Integration](#integration-3)
- [Run](#run-3)
- [Additional resources](#additional-resources)
- [Helper functions](#helper-functions)
- [Usage examples](#usage-examples)
Expand Down Expand Up @@ -558,7 +573,7 @@ contract TestProperties is PropertiesAsserts {

# HEVM cheat codes support

Since version 2.0.5, Echidna supports [HEVM cheat codes](https://hevm.dev/ds-test-tutorial.html#supported-cheat-codes). This repository contains a [`Hevm.sol`](contracts/util/Hevm.sol) contract that exposes cheat codes for easy integration into contracts under test.
Since version 2.0.5, Echidna supports [HEVM cheat codes](https://hevm.dev/std-test-tutorial.html#supported-cheat-codes). This repository contains a [`Hevm.sol`](contracts/util/Hevm.sol) contract that exposes cheat codes for easy integration into contracts under test.

Cheat codes should be used with care, since they can alter the execution environment in ways that are not expected, and may introduce false positives or false negatives.

Expand Down
2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
"format-embedded-solidity": "prettier --write \"**/*.md\" --embedded-language-formatting=auto --plugin prettier-plugin-solidity --tab-width 4 --print-width 120 && prettier --write \"**/*.md\"",
"lint": "npm run lint-check-format && npm run lint-check-links",
"lint-check-format": "prettier --check .",
"lint-check-links": "find . -name '*.md' -not -path './node_modules/*' -print0 | xargs -0 -n1 markdown-link-check"
"lint-check-links": "find . -name '*.md' -not -path './node_modules/*' -not -path './lib/*' -not -path './contracts/Math/ABDKMath64x64/*' -print0 | xargs -0 -n1 markdown-link-check"
},
"repository": {
"type": "git",
Expand Down
2 changes: 1 addition & 1 deletion tests/ERC20/hardhat/medusa-config-ext.json
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@
"target": ".",
"solcVersion": "",
"exportDirectory": "",
"args": []
"args": ["--compile-force-framework", "hardhat"]
}
},
"logging": {
Expand Down
2 changes: 1 addition & 1 deletion tests/ERC20/hardhat/medusa-config.json
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@
"target": ".",
"solcVersion": "",
"exportDirectory": "",
"args": []
"args": ["--compile-force-framework", "hardhat"]
}
},
"logging": {
Expand Down
2 changes: 1 addition & 1 deletion tests/ERC4626/hardhat/medusa-config.json
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@
"target": ".",
"solcVersion": "",
"exportDirectory": "",
"args": []
"args": ["--compile-force-framework", "hardhat"]
}
}
}
Loading