Reusable Properties for ERC7540 Vaults

How to implement properties developed by the Recon + Centrifuge teams for ERC7540 vaults

Motivation

The ERC7540 vault specification was developed by the Centrifuge protocol team because they needed a way to handle asynchronous deposits/withdrawals from an ERC4626 vault.

Their system uses their own Centrifuge chain to first process deposit/withdrawal requests, then transmit a message back to Ethereum where the user that created a request receives their vault token (tranche token) or the underlying asset. The asynchronous nature of this process required additional safeguards so that users don’t instantaneously receive tokens before their request is processed by the Centrifuge chain.

In this example we’ll walk through how you can use the erc7540-reusable-properties repo that the Recon team developed in collaboration with Centrifuge during our engagement with them.

Getting Started

For our example we’ll be using the liquidity-pools repo where Centrifuge has defined an ERC7540 vault that we can scaffold our tests onto (to follow along with our example see this repo).

After cloning the existing repo and removing the existing tests so we can implement our own, we can add a harness for the ERC7540Vault contract using the Recon builder. We then just need to add our ERC7540Vault contract to the Setup contract so it can be targeted:

Then we select the functions of interest in our target contract, which we add to the TargetFunctions contract:

A barebones TargetFunctions contract that only exposes handlers for the core functionality of the vault: depositing and withdrawing.

Next we add the reusable properties as a dependency with:

forge install Recon-Fuzz/erc7540-reusable-properties --no-commit

To use the properties, we simply inherit the ERC7540Properties and CallTestAndUndo (provides utilities for undoing state changes to use assertion tests in the same manner as boolean property tests in Echidna) contracts into the base Properties contract so they can be tested on our TargetFunctions every time we run Echidna.

Additionally, the ERC7540Properties contract requires that we add a way for the fuzzer to switch the actor state variable defined in it, in our example we do this by adding a target function that switches the actor every time the fuzzer calls it:

Since our setup only uses a single actor, we just set the actor using the admin value which gets set to CryticTester (our echidna entrypoint) in the Setup contract, we can then extend this to a multi-actor setup later if we choose which allows the fuzzer to cycle between different actors and more realistically evaluate properties dependent on multiple users depositing into the vault.

Use Only What You Need

To allow the fuzzer to call the functions in the ERC7540Properties contract in assertion testing mode we just need to wrap them with handler functions:

The handlers above use the _doTestAndReturnResult function defined in CallTestAndUndo to test the properties in ERC7540Properties in assertion mode while reverting any state changes that may occur as a result of the test execution, therefore allowing them to behave the same as boolean property tests in Echidna. The benefit of having these tests defined using assertions is that since Echidna can only run in one testing mode at a time (unlike Medusa) you can evaluate these and any other assertion tests in a single run rather than having to do separate runs in assertion and property mode.

Since the properties in ERC7540Properties are meant to be generally applicable to implementations conforming to the ERC7540 vault standard, in real world implementations certain properties may not hold due to varying from the specification. To exclude certain properties that may not hold from being tested in these instances and as a result wasting fuzz runs on them, you can simple remove them from the ERC7540Properties contract.

That’s it! Once you’ve followed the steps above you can easily add more properties to test on your specific vault implementation directly to the Properties contract while knowing that any properties you’ve included handlers for will automatically be tested.