No info on instate violation

CVL Support
1

Trying basic ‘TotalSupplylsSumOfBalances’ invariant on WETH9 and got this error ‘invariant violated in post state’, but with no more info ?

constructor is empty, so no balance can be set > 0 , so no reason to violate the invariant :thinking:

(Certora - Report)

2

Hey @zapaz,
It seems that totalSupply(), which is the ETH balance of the contract, is initialized with an arbitrary value (which is not a storage value), therefore your invariant, implying equality is trivially violated since the contract can start with an ETH balance before the constructor.

3

so how to say in CVL that totalSupply() is initially equal to 0 ?

something like for ghost function ?

ghost sum() returns uint256 {
  init_state axiom sum() == 0;
}

is this available for real function ?

4

AFAIK, no. so the simplest way is to rewrite it as a rule, thus there is no instate check for invariant.

5

ok thanks, rule only :neutral_face: