Did Certora not support interface cast?

CVL Support
1

Hi,

When verifying a property that involves a call to the following function (where _token has value address(underlying))

function _transferAndCheckInputToken(address _from, address _token,uint256 _amount) internal {
    uint256 balanceBefore = IERC20(_token).balanceOf(address(this));
    IERC20(_token).safeTransferFrom(_from, address(this), _amount);
    uint256 balanceAfter = IERC20(_token).balanceOf(address(this));
}

Certora fails to verify. But when I adjust to this

function _transferAndCheckInputToken(address _from, address _token,uint256 _amount) internal {
    uint256 balanceBefore = underlying.balanceOf(address(this));
    underlying.safeTransferFrom(_from, address(this), _amount);
    uint256 balanceAfter = underlying.balanceOf(address(this));
}

It works. Is that the expected behavior or am I performing some mistake?

Cheers!

2

Where is this underlying object declared? im not sure i understand fully the 2nd example.

As for your question regarding the 1st code block:
We do indeed support this casting. Obviously this IERC20 type is declared in an import line at the top of the contract and points to an interface. However, in order for the Prover to know how to handle this cast we have to supply it with the appropriate implementation and some instructions how to handle the function call of this object.

Let’s have a look at the following example from a recent project we did Aave-Starknet Bridge.
If we look at the BridgeL2Harness.sol we can see that we make a cast for a type called IERC20_Extended in line 89.
In our run command (script) we included implementations of this interface, for example the one corresponding to line 89 is the staticAToken, but if you look at the implementations themselves also the ATokenWithPool inherit from it.
Now in the spec we commanded the Prover to act with DISPATCHER(true) (described here), whenever the this burn signature is met by the Prover see in the spec.

hope that’s clear

3

First of all, thank you very much MichaelM!!! In principle I already have done what you have indicated (I linked the contract to the interface implementation using variable underlying of type IERC20Metadata):
–link VaultCertora:underlying=MockUST
Is the problem because the variable is a function parameter?

function _transferAndCheckInputToken(address _from, address _token, uint256 _amount) internal {
    uint256 balanceBefore = /*IERC20(_token)*/underlying.balanceOf(address(this));
    /*IERC20(_token)*/underlying.safeTransferFrom(_from, address(this), _amount);
    uint256 balanceAfter = /*IERC20(_token)*/underlying.balanceOf(address(this));
}

Thanks again!

4

im kind of out of context here.
The code block you sent is a solidity function. Is the underlying object a public variable of the type IERC20?
I presume MockUST is an implementation of IERC20, but you say it’s of type IERC20Metadata, is the latter inheriting from IERC20?

Anyway I can’t quite understand what error/problem you encounter. Can you please make it more clear?