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?