ERC7540 Reusable Properties
A collection of reusable properties for ERC-7540 asynchronous vaults.
Written in collaboration with Centrifuge.
Specification
| Property | Description | Category |
|---|---|---|
| 7540-1 | convertToAssets(totalSupply) == totalAssets unless price is 0.0 | High Level |
| 7540-2 | convertToShares(totalAssets) == totalSupply unless price is 0.0 | High Level |
| 7540-3 | max* never reverts | DOS Invariant |
| 7540-4 | claiming more than max always reverts | Stateful Test |
| 7540-5 | requestRedeem reverts if the share balance is less than amount | Stateful Test |
| 7540-6 | preview* always reverts | Stateful Test |
| 7540-7 | if max[method] > 0, then [method] (max) should not revert | DOS Invariant |
Usage
- Install the repo as a dependency to a Foundry project
forge install Recon-Fuzz/erc7540-reusable-properties --no-commit
- Inherit from the
ERC7540Propertiescontract in the contract where you've defined your properties. For a test suite harnessed with Recon it will look something like this:
abstract contract Properties is Setup, Asserts, ERC7540Properties {}
- Add a way to change the
actorstate variable in theERC7540Propertiescontract. The simplest way to do this is by exposing a target function with something like the following implementation:
function setup_switchActor(uint8 actorIndex) public {
actor = actorsArray[actorIndex % actorsArray.length];
}
- The properties defined in the
ERC7540Propertiescontract are meant to hold for a vault implementation conforming to the ERC specification. If your implementation doesn't require certain properties to hold you can simply exclude them from your contract in which you define your properties:
abstract contract Properties is Setup, Asserts, ERC7540Properties {
function crytic_erc7540_1() public returns (bool test) {
test = erc7540_1(address(vault));
}
function crytic_erc7540_2() public returns (bool test) {
test = erc7540_2(address(vault));
}
}
by not adding a wrapper for properties other than erc7540_2 and erc7540_2 the other properties defined in ERC7540Properties don't get evaluated by the fuzzer.