Multicontract doubt

General Discussion
1

Hello team, I am having the following doubt:
I have a contract A:

contract A{
    function foo() external {
        // does something
    }

    function foo2() public view returns(uint){
        // returns somehting
    } 
}

contract A is deployed and I need to use it in another contract B:

interface IA {
    function foo() external {},
    function foo2() public view returns(uint)
}

contract B {
    IA a;
    constructor(address _a) {
        a = IA(_a);
    }

    function bar() external {
        a.foo();
        // does something
    }

    function bar2() external {
        uint256 variable = a.foo2();
        // does something
    }
}

Can you give me an example of spec file for contract B verification?

2

You can use certoraRun A.sol B.sol --link B:a=A --verify B:spec.spec to tell the prover that the field a of contract B has code A. If you want to call methods of the A instance in the spec file, you can write using A as aImpl at the top, and then call aImpl.foo().

See Linking Contracts — Certora Prover Documentation 0.0 documentation and Multicontract — Certora Prover Documentation 0.0 documentation (which will be migrated to the “reference manual” section in the future).

3

Thanks a lot.
Also, is there a way where I can use contract A without having it’s implementation? And just feed the contract address along with interface?

4

depends what you mean by that.
If you dont have an implementation and there is a call in your verified contract (A) to that external contract (B), then the prover needs you to specify to it how you wish this call to be resolved.

By default the call will havoc everything, meaning it will forget any past info it had about storage vars because as far as the prover concerned the implementation is unknown, and so anything can happen including changing every var you’ve tracked to this point. This is the model since we want to over-approximate the states to make sure that we dont miss anything.

What you can do?
You need to specify to the prover what to do when this external call is being made - you can read more about function summarizations here.

In short you can do many things including telling the prover to return a specific value every time this function is called (ALWAYS), return a deterministic arbitrary constant (CONSTANT), invoke a CVL function or return a ghost value.

Hope that helps

5

Hello @MichaelM, thanks a lot for the detailed explanation. It helped me clear some doubts.

Can you please have a look at the following contracts:

  • I want to verify the InstaIndex contract. It uses InstaList (ListInterface) and InstaDefaultImplementation (AccountInterface)
  • The last function (setBasics) in InstaIndex runs only once while the contract is deployed and takes the address of the InstaList contract.
  • InstaIndex is basically a factory contract, and makes new accounts. These new account addresses are passed as AccountInterface to make the initial configuration. (see build function in InstaIndex)

I’m unable to understand how I should proceed with verification with these contracts.

Can you please guide me with this?
Regards!

6

@Rushank this is quite a wide question.
Before i take a look maybe try to explain what properties exactly are you trying to verify?

Remember: you are writing a specification, meaning, your job is to describe the acceptable behavior of the contract(s) using CVL.
The Prover will make your life easier by taking the specification document you wrote and checking it against the actual implementation.

That being said, there are things that the prover does not cover, for example, you cannot check whether a constant address (say of a contract) that you’re using in your implementation is really the relevant contract or even if it exists on the blockchain. This is because this is not the intended use case of the Certora Prover. The specification you write should mainly describe a correct behavior of the methods, e.g. if we start from a certain state and applying a function, what should be the acceptable outputs, otherwise you can describe invariants of the system.

Hope it helps

7

I would like to verify properties like the dsa built by build() function in InstaIndex do have the owner as passed in the input. Whether or not the output is a valid address, and more.

My main doubt here is if you see InstaIndex, it uses InstaList and InstaDefaultImplementation by their respective interfaces (ListInterface & AccountInterface). And contract pointers are set within the functions of InstaIndex by passing addresses.
So for verification, do I need to make modifications to these contracts to directly import their implementations and remove Interfaces?

I will give one example, InstaIndex is a factory contract for making accounts:
Check this line, the build() function returns _account(address) which is type of AccountInterface. Hence the newly formed account uses the interface to call a function within.

I’m unable to figure how do I start with verification when my contracts are so connected with each other.

Hope I was able to explain where exactly I’m facing problem.
Regards!

8

Hello, writing this to follow up.
Thanks!

9

@Rushank If your verification depends on the implementation of these interfaces then you will need to implement them as normal contracts and import and link them. If it doesn’t you can define their methods in the specification’s methods block and summarize them as NONDET which will assign them a random output value.

10

Thanks! I understood.