How to verify a function that uses a struct as parameter (and an array within)?

CVL Support
1

Hi,

I am trying to verify this function: function deposit(DepositParams calldata _params), where DepositParams is the following structure

struct DepositParams {
    address inputToken;
    uint64 lockDuration;
    uint256 amount;
    ClaimParams[] claims;
    string name;
    uint256 slippage;
}

I saw that Certora does not support such a structure (due to an array inside it). Thus, I used a calldataarg doing this in the spec file

calldataarg arg;
deposit(eV, arg);

Is this the only way to deal with such a situation?

Best regards!

2

Hey acmCertora,
You are right, we are currently supporting structs and complex types only partially. In any case that CVL cannot handle direct access or calls to state variables, we have a way to access these variables.

We call this method harnessing:

  • Create a solidity file that inherits from the original contract you desire to verify, for example if you want to verify contract A we’ll create a contract AHarness which inherits from contract A.

  • On this AHarness contract you can implement getters that retrieve the desired values.

  • Since this harness contract inherits from your original contract, verifying it is generally equivalent to verifying the original contract because it has access to the entire contract A functionality.

  • When you do it make sure to be careful with what you add. pure and view functions are generally safe; any setters or additional methods may alter the original functionality of the original contract.

This a workaround until we incorporate a native access to all types from within CVL.

EDIT:
Here’s an example you can follow - LINK. I recommend to have a look at the graph on the report: LINK

Hope that helps.

3

Thank you very much, MichelM! It worked!

1 Like