diff --git a/.github/workflows/medusa.yaml b/.github/workflows/medusa.yaml index c4ca71d..e71b210 100644 --- a/.github/workflows/medusa.yaml +++ b/.github/workflows/medusa.yaml @@ -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 @@ -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 @@ -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 diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..62dc1e8 --- /dev/null +++ b/CLAUDE.md @@ -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///` 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//internal/properties/` and `external/properties/` +2. For external properties, update the interface in `contracts//util/` +3. Add test in `contracts//*/test/` to verify property catches violations +4. Update `PROPERTIES.md` table +5. Update `contracts//README.md` if present + +## Branch Naming + +- Features: `dev-` (e.g., `dev-add-properties-for-erc20-transfers`) +- Bug fixes: `fix-` (e.g., `fix-typo-in-readme`) diff --git a/PROPERTIES.md b/PROPERTIES.md index 063dd83..39b10c4 100644 --- a/PROPERTIES.md +++ b/PROPERTIES.md @@ -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) @@ -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` @@ -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. | diff --git a/README.md b/README.md index 0c0cebf..40e475f 100644 --- a/README.md +++ b/README.md @@ -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) @@ -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. diff --git a/package.json b/package.json index 58777b9..07a8068 100644 --- a/package.json +++ b/package.json @@ -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", diff --git a/tests/ERC20/hardhat/medusa-config-ext.json b/tests/ERC20/hardhat/medusa-config-ext.json index a77d593..600166a 100644 --- a/tests/ERC20/hardhat/medusa-config-ext.json +++ b/tests/ERC20/hardhat/medusa-config-ext.json @@ -69,7 +69,7 @@ "target": ".", "solcVersion": "", "exportDirectory": "", - "args": [] + "args": ["--compile-force-framework", "hardhat"] } }, "logging": { diff --git a/tests/ERC20/hardhat/medusa-config.json b/tests/ERC20/hardhat/medusa-config.json index 317cdc8..081569f 100644 --- a/tests/ERC20/hardhat/medusa-config.json +++ b/tests/ERC20/hardhat/medusa-config.json @@ -69,7 +69,7 @@ "target": ".", "solcVersion": "", "exportDirectory": "", - "args": [] + "args": ["--compile-force-framework", "hardhat"] } }, "logging": { diff --git a/tests/ERC4626/hardhat/medusa-config.json b/tests/ERC4626/hardhat/medusa-config.json index fc71aeb..3f0e55b 100644 --- a/tests/ERC4626/hardhat/medusa-config.json +++ b/tests/ERC4626/hardhat/medusa-config.json @@ -55,7 +55,7 @@ "target": ".", "solcVersion": "", "exportDirectory": "", - "args": [] + "args": ["--compile-force-framework", "hardhat"] } } }