From 675256402d3ca7aa79e54aa2354826ba2f5e70be Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 15 Oct 2024 13:04:11 -0300 Subject: [PATCH 1/6] chore: run invariant tests via medusa instead of echidna --- medusa.json | 89 ++++++++++++++++++++++++++++++++++++++++++++++++++++ package.json | 2 +- 2 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 medusa.json diff --git a/medusa.json b/medusa.json new file mode 100644 index 00000000..dc61b33d --- /dev/null +++ b/medusa.json @@ -0,0 +1,89 @@ +{ + "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 0, + "shrinkLimit": 5000, + "callSequenceLength": 100, + "corpusDirectory": "", + "coverageEnabled": true, + "coverageFormats": [ + "html", + "lcov" + ], + "targetContracts": ["InvariantGreeter"], + "predeployedContracts": {}, + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": [ + "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, + "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/Greeter.t.sol", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false + } +} diff --git a/package.json b/package.json index 88242ec3..e2956573 100644 --- a/package.json +++ b/package.json @@ -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", From 2453dd6c9540d4e80a21da8801736b32f7637bb5 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 15 Oct 2024 14:00:32 -0300 Subject: [PATCH 2/6] chore: refactor fuzzing campaign so it more closely resembles what we use in production --- test/invariants/PROPERTIES.md | 8 +++--- test/invariants/fuzz/Greeter.t.sol | 45 ++++++++++++++++-------------- 2 files changed, 28 insertions(+), 25 deletions(-) diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index e48439c9..bb8837e9 100644 --- a/test/invariants/PROPERTIES.md +++ b/test/invariants/PROPERTIES.md @@ -1,4 +1,4 @@ -| Properties | Type | -|---------------------------------------------------|------------| -| Greeting should never be empty | Valid state | -| Only the owner can set the greeting | State transition | \ No newline at end of file +| id | Properties | Type | +| --- | --------------------------------------------------- | ------------ | +| 1 | Greeting should never be empty | Valid state | +| 2 | Only the owner can set the greeting | State transition | diff --git a/test/invariants/fuzz/Greeter.t.sol b/test/invariants/fuzz/Greeter.t.sol index 96e2b1eb..a8f6cf95 100644 --- a/test/invariants/fuzz/Greeter.t.sol +++ b/test/invariants/fuzz/Greeter.t.sol @@ -2,36 +2,39 @@ pragma solidity 0.8.23; import {Greeter, IERC20} from 'contracts/Greeter.sol'; +import {CommonBase} from 'forge-std/Base.sol'; -interface IHevm { - function prank(address) external; -} - -contract InvariantGreeter { - IHevm internal _hevm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D); - +contract InvariantGreeter is CommonBase { Greeter internal _targetContract; constructor() { _targetContract = new Greeter('a', IERC20(address(1))); } - function checkGreeterNeverEmpty(string memory _newGreeting) public { - // Execution - (bool _success,) = address(_targetContract).call(abi.encodeCall(Greeter.setGreeting, _newGreeting)); - - // Check output condition - assert((_success && keccak256(bytes(_targetContract.greeting())) != keccak256(bytes(''))) || !_success); + /// @custom:property-id 2 + /// @custom:property Only the owner can set the greeting + function handler_unguided_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('')); + } } - function checkOnlyOwnerSetsGreeting(address _caller) public { - // Input conditions - _hevm.prank(_caller); - - // Execution - (bool _success,) = address(this).call(abi.encodeCall(Greeter.setGreeting, 'hello')); + function handler_guided_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('')); + } + } - // Check output condition - assert((_success && msg.sender == _targetContract.OWNER()) || (!_success && msg.sender != _targetContract.OWNER())); + /// @custom:property-id 1 + /// @custom:property Greeting should never be empty + function property_greetingIsNeverEmpty() external view { + assert(keccak256(bytes(_targetContract.greeting())) != keccak256('')); } } From c0b513111a7dd0e9398f7beb1c6e3e8ff833bd01 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 15 Oct 2024 14:01:47 -0300 Subject: [PATCH 3/6] docs: update readme --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 5a4d6546..a703167d 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@
Sample Integration, Unit, Property-based fuzzed and symbolic tests
Example tests showcasing mocking, assertions and configuration for mainnet forking. As well it includes everything needed in order to check code coverage.
Unit tests are built based on the Branched-Tree Technique, using Bulloak. -
Formal verification and property-based fuzzing are achieved with Halmos and Echidna (resp.). +
Formal verification and property-based fuzzing are achieved with Halmos and medusa (resp.).
Linter
Simple and fast solidity linting thanks to forge fmt.
@@ -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 just run 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 From 92d1d9e8b082b56bc9cb18a2a99e491e51c2abf0 Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 15 Oct 2024 18:50:13 -0300 Subject: [PATCH 4/6] ci: remove echidna ci step --- .github/workflows/tests.yml | 36 ------------------------------------ 1 file changed, 36 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index a9b5fdbb..7fd53390 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -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 From dd7ea8dec04735ee521496cf16e9f3014512513f Mon Sep 17 00:00:00 2001 From: teddy Date: Fri, 18 Oct 2024 17:42:40 -0300 Subject: [PATCH 5/6] fix: feedback from gas --- medusa.json | 4 +- test/invariants/PROPERTIES.md | 2 +- test/invariants/fuzz/FuzzTest.t.sol | 8 ++++ test/invariants/fuzz/Greeter.t.sol | 40 ------------------- .../fuzz/handlers/guided/Greeter.t.sol | 15 +++++++ .../fuzz/handlers/unguided/Greeter.t.sol | 18 +++++++++ test/invariants/fuzz/properties/Greeter.t.sol | 12 ++++++ test/invariants/fuzz/setup/Greeter.t.sol | 13 ++++++ 8 files changed, 69 insertions(+), 43 deletions(-) create mode 100644 test/invariants/fuzz/FuzzTest.t.sol delete mode 100644 test/invariants/fuzz/Greeter.t.sol create mode 100644 test/invariants/fuzz/handlers/guided/Greeter.t.sol create mode 100644 test/invariants/fuzz/handlers/unguided/Greeter.t.sol create mode 100644 test/invariants/fuzz/properties/Greeter.t.sol create mode 100644 test/invariants/fuzz/setup/Greeter.t.sol diff --git a/medusa.json b/medusa.json index dc61b33d..31227c5b 100644 --- a/medusa.json +++ b/medusa.json @@ -12,7 +12,7 @@ "html", "lcov" ], - "targetContracts": ["InvariantGreeter"], + "targetContracts": ["FuzzTest"], "predeployedContracts": {}, "targetContractsBalances": [], "constructorArgs": {}, @@ -75,7 +75,7 @@ "compilation": { "platform": "crytic-compile", "platformConfig": { - "target": "test/invariants/fuzz/Greeter.t.sol", + "target": "test/invariants/fuzz/FuzzTest.t.sol", "solcVersion": "", "exportDirectory": "", "args": [] diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index bb8837e9..bbf31df4 100644 --- a/test/invariants/PROPERTIES.md +++ b/test/invariants/PROPERTIES.md @@ -1,4 +1,4 @@ -| id | Properties | Type | +| Id | Properties | Type | | --- | --------------------------------------------------- | ------------ | | 1 | Greeting should never be empty | Valid state | | 2 | Only the owner can set the greeting | State transition | diff --git a/test/invariants/fuzz/FuzzTest.t.sol b/test/invariants/fuzz/FuzzTest.t.sol new file mode 100644 index 00000000..02a127bf --- /dev/null +++ b/test/invariants/fuzz/FuzzTest.t.sol @@ -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 {} diff --git a/test/invariants/fuzz/Greeter.t.sol b/test/invariants/fuzz/Greeter.t.sol deleted file mode 100644 index a8f6cf95..00000000 --- a/test/invariants/fuzz/Greeter.t.sol +++ /dev/null @@ -1,40 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity 0.8.23; - -import {Greeter, IERC20} from 'contracts/Greeter.sol'; -import {CommonBase} from 'forge-std/Base.sol'; - -contract InvariantGreeter is CommonBase { - Greeter internal _targetContract; - - constructor() { - _targetContract = new Greeter('a', IERC20(address(1))); - } - - /// @custom:property-id 2 - /// @custom:property Only the owner can set the greeting - function handler_unguided_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('')); - } - } - - function handler_guided_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('')); - } - } - - /// @custom:property-id 1 - /// @custom:property Greeting should never be empty - function property_greetingIsNeverEmpty() external view { - assert(keccak256(bytes(_targetContract.greeting())) != keccak256('')); - } -} diff --git a/test/invariants/fuzz/handlers/guided/Greeter.t.sol b/test/invariants/fuzz/handlers/guided/Greeter.t.sol new file mode 100644 index 00000000..732e105e --- /dev/null +++ b/test/invariants/fuzz/handlers/guided/Greeter.t.sol @@ -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('')); + } + } +} diff --git a/test/invariants/fuzz/handlers/unguided/Greeter.t.sol b/test/invariants/fuzz/handlers/unguided/Greeter.t.sol new file mode 100644 index 00000000..213d73bc --- /dev/null +++ b/test/invariants/fuzz/handlers/unguided/Greeter.t.sol @@ -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('')); + } + } +} diff --git a/test/invariants/fuzz/properties/Greeter.t.sol b/test/invariants/fuzz/properties/Greeter.t.sol new file mode 100644 index 00000000..979d278f --- /dev/null +++ b/test/invariants/fuzz/properties/Greeter.t.sol @@ -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('')); + } +} diff --git a/test/invariants/fuzz/setup/Greeter.t.sol b/test/invariants/fuzz/setup/Greeter.t.sol new file mode 100644 index 00000000..ee6676f1 --- /dev/null +++ b/test/invariants/fuzz/setup/Greeter.t.sol @@ -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))); + } +} From b993e925f896264bc26ea696a22ec2065cfac19e Mon Sep 17 00:00:00 2001 From: teddy Date: Tue, 22 Oct 2024 12:17:05 -0300 Subject: [PATCH 6/6] fix: updates to readme suggested by gas --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index a703167d..c35ee249 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@
Sample Integration, Unit, Property-based fuzzed and symbolic tests
Example tests showcasing mocking, assertions and configuration for mainnet forking. As well it includes everything needed in order to check code coverage.
Unit tests are built based on the Branched-Tree Technique, using Bulloak. -
Formal verification and property-based fuzzing are achieved with Halmos and medusa (resp.). +
Formal verification and property-based fuzzing are achieved with Halmos and Medusa (resp.).
Linter
Simple and fast solidity linting thanks to forge fmt.
@@ -80,7 +80,7 @@ In order to just run integration tests, run: yarn test:integration ``` -In order to just run the medusa fuzzing campaign (requires [Medusa](https://github.com/crytic/medusa/blob/master/docs/src/getting_started/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 @@ -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) \ No newline at end of file +The primary license for the boilerplate is MIT, see [`LICENSE`](https://github.com/defi-wonderland/solidity-foundry-boilerplate/blob/main/LICENSE)