Inter-connected multi-contracts

Hello team, I have some inter-connected contracts which depend on each other’s codes. So I replaced the interfaces with code implementations for verification. Please have a look at the following contracts:

Math.sol

// SPDX-License-Identifier: GPL-3.0
pragma solidity ^0.7.0;

import "./Variable.sol";

contract Math{
   Variable varContract;

   function add(uint x, uint y) external view returns (uint z) {
        require((z = x + y + varContract.myVar()) >= x, "ds-math-add-overflow");
    }

    function sub(uint x, uint y) external view returns (uint z) {
        require((z = x - y - varContract.myVar()) <= x, "ds-math-sub-underflow");
    }
}

Variable.sol

// SPDX-License-Identifier: GPL-3.0
pragma solidity ^0.7.0;

import "./Math.sol";
import "./Function.sol";

contract Variable {
    Math math;
    Function func;
    uint public myVar = 1;

    function increaseVar(uint x, uint y) external {
       myVar = math.add(x, y);
    }

    function decreaseVar(uint x, uint y) external {
       myVar = math.sub(x, y);
    }

    function knowDiff() external view returns(uint) {
        return myVar - func.myVar2();
    }
}

Function.sol

// SPDX-License-Identifier: GPL-3.0
pragma solidity ^0.7.0;

import "./Math.sol";
import "./Variable.sol";

contract Function {
    Math math;
    Variable varContract;
    uint public myVar2 = 0;

    function increaseVar2() external {
       myVar2 = math.add(varContract.myVar(), myVar2);
    }

    function decreaseVar() external {
       myVar2 = math.sub(varContract.myVar(), myVar2);
    }

}

Wrote a simple spec: all.spec

methods {
    myVar2() returns uint256 envfree
}
rule Var2Inc() {
    before = myVar2();
    
    env e;
    increaseVar2(e);

    after = myVar2();

    assert after > before, "Didn't increase";
}

And used the following command:

certoraRun ./Contracts/Function.sol ./Contracts/Math.sol ./Contracts/Variable.sol --link Function:math=Math Function:varContract=Variable --verify Function:all.spec --solc solc7.6

Ant I got this error:

DeclarationError: Identifier already declared.
contract Function {
^ (Relevant source part starts here and spans across multiple lines).

The previous declaration is here:
import "./Math.sol";
^------------------^

Can you please guide me on this?

I have a wild guess, but seems to me that you import Math.sol twice, first explicitly in the Function contract and also in Variable.sol, implicitly. Does it compile when you remove that same import in Function.sol ?

Yea it’s compiling, It shows the following error now:

DeclarationError: Identifier already declared.
contract Function {
^ (Relevant source part starts here and spans across multiple lines).

The previous declaration is here:
import "./Variable.sol";
^----------------------^

I guess the main problem here is, importing Variable in Function and vice-versa.

Basically it is a Solidity programming issue, not a CVL issue.
Is this inter-connection design a necessity?
I mean, probably there is a better way to connect contracts which is non-cyclic.

I was thinking the same, but it compiled so thought this won’t be a problem.
Not necessary maybe, but both contracts need each other’s code in some way. And if we can’t use interfaces, then this cyclic method is what comes to mind.
Could you suggest a better way to connect these contracts with each other?

My suggestion, however not necessarily optimal, would transform Math and Function to libraries, whose functions have three arguments instead of two. The third argument being your special variable.
I guess passing all those variables as arguments will remove this cyclic-complexity you have, then calling all functions (whether from Math or Function) from the Variable contract, being the only dependent one, might solve this issue.

I think you can just integrate Function into Variable, combining them to a single contract, but I haven’t gone too deep to your implementation details.

Actually, the code I mentioned was just a simple example of much more complex implementation.

You can see those contracts here:

These were originally connected through interfaces, but for verification purposes, I had to import respective implementations.

What I’m trying to say is, that the contracts are required to be kept as contracts. Converting them to libraries would alter the original objective. Could you suggest a way?

If you have the freedom to change the functions’ interfaces, I would suggest just transferring all the variables as input arguments to the functions, and keeping the real values in a separate contract such that there is no cyclic-dependence.
If not, I need to think of a more elaborate way.

Yea that would be nice, but will that work for even functions of the contracts? I don’t just have variables that are interconnected, there are even functions that interact with each other.

For example:

These are two functions in two contracts that call each other.

Hey, I adjusted my implementation to remove that cyclic importing.
Now while verifying my 1st property, I faced a weird case, contrary asserts are both passing:

rule starter{
    address _master;
    require _master != 0;
    address _account;
    address _connectors;

    address owner;
    require owner != 0;


    env e;
    setBasics(e, _master, _account, _connectors); 
    address dsa = build(e, owner, 2, 0);
    assert dsa == 0, "not";
    assert dsa != 0, "not";
}

Am I doing something wrong in spec file?

If not, could you please have a quick look on functions used in the above property:
setBasics
build

looks like setBasics requires master to equal 0 but you require it to not equal 0 so there are no non-reverting paths and the asserts are reached. Your rule is vacuous. You can use the --rule_sanity flag in your script to find these kinds of vacuous rules.

docs
tutorials

Ohh, but setBasics require the state variable master to be equal to zero, the one in spec file is the _master which is the function parameter.
To give some context, setBasics sets the initial configuration of the contract hence the mater is required to be zero (the default value on initialization)
Will try using --rule_sanity flag as well.

On using --rule_sanity flag, it’s showing me this violation:
reachability check FAILED (assertion is unreachable):
Is this some other issue or is it due to contrary asserts?

Yes this is the tool catching the issue with your rule. It says the asserting is unreachable which means the rule is vacuous ( there are no non-reverting paths ).

Oh okay, thanks!
Could you please help me understand what should be corrected here?

I found the problem in the rule
The rule is passing, but there is a call resolution:
v

What can be the reason for this?

This happens for external calls that aren’t defined in the scope of the verification. You can add the InstaAccount contract in the run script as a contract the tool can access. See Multicontract — Certora Prover Documentation 0.0 documentation