Invariant does not hold in multi-contract call

CVL Support
1

Hi,
I’m trying to check my understanding of invariant and requireInvariant but hitting a roadblock. Here’s the scenario:
I have two simple contracts, First.sol and Second.sol. Here is the code:

First.sol

// SPDX-License-Identifier: MIT
pragma solidity 0.8.0;
import "./Second.sol";

contract First is Second {
    uint256 valueFirst;

    function changeValue(uint256 valueX) external {
        valueFirst = valueX + valueSecond;
    }
}

And,

Second.sol

// SPDX-License-Identifier: MIT
pragma solidity 0.8.0;

contract Second {
    uint256 valueSecond;

    constructor() {
        valueSecond = 52;
    }

    function getValueSecond() external view returns(uint256) {
        return valueSecond;
    }
}

I want to verify that the valueSecond variable always has a value of 52. So, here’s my Multi.spec :

using Second as sec

methods {
    sec.getValueSecond() returns(uint256) envfree;
}

invariant valueSecond_is_constant()
    sec.getValueSecond() == 52

rule arbitRule(env e, uint256 x) {
    requireInvariant valueSecond_is_constant();
    changeValue(e, x);
    assert sec.getValueSecond() == 52, "valueSecond changed!";
}

And I run this via -

certoraRun contracts/Multi/First.sol contracts/Multi/Second.sol \
--verify First:specs/Multi/Multi.spec \
--solc solc \
--msg "Multi_Invariant_Spec_Style1"

The Prover fails saying valueSecond_is_constant_instate → invariant violated in post-state

Can someone help me understand what am I missing? Any help or pointers would be much appreciated!

Thanks

2

AFAIR constructors of external contracts (not the one that you verify (–verify)) aren’t triggered. They are havoced. That’s why there can be any value.

There is no way to filter out instate part of the invariant. So you can either rewrite it as a rule or leave it like this and being able to use as require invariant

3

Thanks for the help!

4

you can also simply remove sec. , as First inherits from Second, this spec works :

methods {
    getValueSecond() returns(uint256) envfree;
}

invariant valueSecond_is_constant()
    getValueSecond() == 52
5

Makes sense. Thanks!