Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: use medusa instead of echidna #87

Merged
merged 6 commits into from
Dec 16, 2024
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
36 changes: 0 additions & 36 deletions .github/workflows/tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -64,42 +64,6 @@ jobs:
- name: Run tests
run: yarn test:integration

echidna-tests:
name: Echidna Test
runs-on: ubuntu-latest

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

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

- name: Use Node.js
uses: actions/setup-node@v4
with:
node-version: 20.x
cache: 'yarn'

- name: Install dependencies
run: yarn --frozen-lockfile --network-concurrency 1

- name: Compile contracts
run: |
forge build --build-info

- name: Run Echidna
uses: crytic/echidna-action@v2
with:
files: .
contract: InvariantGreeter
test-mode: assertion
crytic-args: --ignore-compile

halmos-tests:
name: Run symbolic execution tests
runs-on: ubuntu-latest
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
<dt>Sample Integration, Unit, Property-based fuzzed and symbolic tests</dt>
<dd>Example tests showcasing mocking, assertions and configuration for mainnet forking. As well it includes everything needed in order to check code coverage.</dd>
<dd>Unit tests are built based on the <a href="https://twitter.com/PaulRBerg/status/1682346315806539776">Branched-Tree Technique</a>, using <a href="https://github.com/alexfertel/bulloak">Bulloak</a>.
<dd>Formal verification and property-based fuzzing are achieved with <a href="https://github.com/a16z/halmos">Halmos</a> and <a href="https://github.com/crytic/echidna">Echidna</a> (resp.).
<dd>Formal verification and property-based fuzzing are achieved with <a href="https://github.com/a16z/halmos">Halmos</a> and <a href="https://github.com/crytic/medusa">Medusa</a> (resp.).

<dt>Linter</dt>
<dd>Simple and fast solidity linting thanks to forge fmt.</dd>
Expand Down Expand Up @@ -80,7 +80,7 @@ In order to just run integration tests, run:
yarn test:integration
```

In order to just run the echidna fuzzing campaign (requires [Echidna](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/introduction/installation.md) installed), run:
In order to start the Medusa fuzzing campaign (requires [Medusa](https://github.com/crytic/medusa/blob/master/docs/src/getting_started/installation.md) installed), run:

```bash
yarn test:fuzz
Expand Down Expand Up @@ -171,4 +171,4 @@ Also, remember to update the `package_name` param to your package name:
You can take a look at our [solidity-exporter-action](https://github.com/defi-wonderland/solidity-exporter-action) repository for more information and usage examples.

## Licensing
The primary license for the boilerplate is MIT, see [`LICENSE`](https://github.com/defi-wonderland/solidity-foundry-boilerplate/blob/main/LICENSE)
The primary license for the boilerplate is MIT, see [`LICENSE`](https://github.com/defi-wonderland/solidity-foundry-boilerplate/blob/main/LICENSE)
89 changes: 89 additions & 0 deletions medusa.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
{
"fuzzing": {
"workers": 10,
"workerResetLimit": 50,
"timeout": 0,
"testLimit": 0,
"shrinkLimit": 5000,
"callSequenceLength": 100,
"corpusDirectory": "",
"coverageEnabled": true,
"coverageFormats": [
"html",
"lcov"
],
"targetContracts": ["FuzzTest"],
"predeployedContracts": {},
"targetContractsBalances": [],
"constructorArgs": {},
"deployerAddress": "0x30000",
"senderAddresses": [
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we are not using these.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we are not taking advantage of the various sender addresses in the simple boilerplate example, but they are usually later used in our actor setups for bigger projects, so I lean on leaving them in

what should be the alternative? using only one? I believe medusa wont run if they key is deleted or has an empty array as a value

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would use just one only if somehow it enhance the performance.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

afaik having one vs many doesnt affect performance (as long as having many users doesnt make the domain of possible states grow at a relevant rate, which is not the case for the humble greeter)

"0x10000",
"0x20000",
"0x30000"
],
"blockNumberDelayMax": 60480,
"blockTimestampDelayMax": 604800,
"blockGasLimit": 125000000,
"transactionGasLimit": 12500000,
"testing": {
"stopOnFailedTest": true,
"stopOnFailedContractMatching": false,
"stopOnNoTests": true,
"testAllContracts": false,
"traceAll": false,
"assertionTesting": {
"enabled": true,
"testViewMethods": true,
"panicCodeConfig": {
"failOnCompilerInsertedPanic": false,
"failOnAssertion": true,
"failOnArithmeticUnderflow": false,
"failOnDivideByZero": false,
"failOnEnumTypeConversionOutOfBounds": false,
"failOnIncorrectStorageAccess": false,
"failOnPopEmptyArray": false,
"failOnOutOfBoundsArrayAccess": false,
"failOnAllocateTooMuchMemory": false,
"failOnCallUninitializedVariable": false
}
},
"propertyTesting": {
"enabled": false,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

true by default (avoiding incidents)?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the idea is for the boilerplate to closely resemble what we run in production, and afaik we are disabling property testing in all projects to reduce complexity (2 kinds of tests vs 1) and help avoid mistakes where the property testing mode is disabled down the line and property tests are executed as assertion tests, causing a false negative, since that false negative would be present when the test is initially developed, making it evident

"testPrefixes": [
"property_"
]
},
"optimizationTesting": {
"enabled": false,
"testPrefixes": [
"optimize_"
]
},
"targetFunctionSignatures": [],
"excludeFunctionSignatures": []
},
"chainConfig": {
"codeSizeCheckDisabled": true,
"cheatCodes": {
"cheatCodesEnabled": true,
"enableFFI": false
},
"skipAccountChecks": true
}
},
"compilation": {
"platform": "crytic-compile",
"platformConfig": {
"target": "test/invariants/fuzz/FuzzTest.t.sol",
"solcVersion": "",
"exportDirectory": "",
"args": []
}
},
"logging": {
"level": "info",
"logDirectory": "",
"noColor": false
}
}
2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"lint:sol": "solhint 'src/**/*.sol' 'script/**/*.sol' 'test/**/*.sol'",
"prepare": "husky",
"test": "forge test -vvv",
"test:fuzz": "echidna test/invariants/fuzz/Greeter.t.sol --contract InvariantGreeter --corpus-dir test/invariants/fuzz/echidna_coverage/ --test-mode assertion",
"test:fuzz": "medusa fuzz",
"test:integration": "forge test --match-contract Integration -vvv",
"test:symbolic": "halmos",
"test:unit": "forge test --match-contract Unit -vvv",
Expand Down
8 changes: 4 additions & 4 deletions test/invariants/PROPERTIES.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
| Properties | Type |
|---------------------------------------------------|------------|
| Greeting should never be empty | Valid state |
| Only the owner can set the greeting | State transition |
| Id | Properties | Type |
| --- | --------------------------------------------------- | ------------ |
| 1 | Greeting should never be empty | Valid state |
| 2 | Only the owner can set the greeting | State transition |
8 changes: 8 additions & 0 deletions test/invariants/fuzz/FuzzTest.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {GreeterGuidedHandlers} from './handlers/guided/Greeter.t.sol';
import {GreeterUnguidedHandlers} from './handlers/unguided/Greeter.t.sol';
import {GreeterProperties} from './properties/Greeter.t.sol';

contract FuzzTest is GreeterGuidedHandlers, GreeterUnguidedHandlers, GreeterProperties {}
37 changes: 0 additions & 37 deletions test/invariants/fuzz/Greeter.t.sol

This file was deleted.

15 changes: 15 additions & 0 deletions test/invariants/fuzz/handlers/guided/Greeter.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {GreeterSetup} from '../../setup/Greeter.t.sol';

contract GreeterGuidedHandlers is GreeterSetup {
function handler_setGreeting(string memory _newGreeting) external {
// no need to prank since this contract deployed the greeter and is therefore its owner
try _targetContract.setGreeting(_newGreeting) {
assert(keccak256(bytes(_targetContract.greeting())) == keccak256(bytes(_newGreeting)));
} catch {
assert(keccak256(bytes(_newGreeting)) == keccak256(''));
}
}
}
18 changes: 18 additions & 0 deletions test/invariants/fuzz/handlers/unguided/Greeter.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {GreeterSetup} from '../../setup/Greeter.t.sol';

contract GreeterUnguidedHandlers is GreeterSetup {
/// @custom:property-id 2
/// @custom:property Only the owner can set the greeting
function handler_setGreeting(address _caller, string memory _newGreeting) external {
vm.prank(_caller);
try _targetContract.setGreeting(_newGreeting) {
assert(keccak256(bytes(_targetContract.greeting())) == keccak256(bytes(_newGreeting)));
assert(_caller == _targetContract.OWNER());
} catch {
assert(_caller != _targetContract.OWNER() || keccak256(bytes(_newGreeting)) == keccak256(''));
}
}
}
12 changes: 12 additions & 0 deletions test/invariants/fuzz/properties/Greeter.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {GreeterSetup} from '../setup/Greeter.t.sol';

contract GreeterProperties is GreeterSetup {
/// @custom:property-id 1
/// @custom:property Greeting should never be empty
function property_greetingIsNeverEmpty() external view {
assert(keccak256(bytes(_targetContract.greeting())) != keccak256(''));
}
}
13 changes: 13 additions & 0 deletions test/invariants/fuzz/setup/Greeter.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {Greeter, IERC20} from 'contracts/Greeter.sol';
import {CommonBase} from 'forge-std/Base.sol';

contract GreeterSetup is CommonBase {
Greeter internal _targetContract;

constructor() {
_targetContract = new Greeter('a', IERC20(address(1)));
}
}
Loading