Prover bug on NONDET with zero address

[zapaz]

This rule fails whereas there are no bug in the solidity code :

// Ensure rewardOracle cannot be set to zero
rule cannotSetRewardOracleWithoutPrice(method f, env e, calldataarg args) filtered {
   f -> !f.isView
}{
  address _rewardOracle = getRewardOracle(e, Reward);
  f(e, args);
  address rewardOracle_ = getRewardOracle(e, Reward);

  assert _rewardOracle != 0  => rewardOracle_ != 0 ;
}

Is should be impossible to set rewardOracle to 0 , but it looks like it does...

Problem comes from rewardOracle.latestAnswer() NONDET that produce random output... even when rewardOracle is zero address => Prover should instead reverts (like solidity code does)

[MichaelMorami]

You are completely right @zapaz.
Our summarization is not fully realistic. This is a miss that we had in the setup, but this sometimes happen when setup is being done separately from brainstorming a list of properties.
A setup, should methodically over-approximate or precisely describe reality, while usually looking to reduce complexity. The setup should be built and tailored based on the properties that the researcher tries to prove. For example, if we want to prove that an index is ever growing (can't be decreased), and we get lots of timeouts due to non-linear math operations, we can summarize those functions to return some non-deterministic results that are bound to some elementary constrains: - when we multiplying x * y, if x > RAY or y > RAY, then result > y or result > x respectively. This kind of summarization isn't precise, but it preserve the underlying property of multiplication, while over-approximating - the result can be any number greater than x or y. That includes the actual result of multiplication and beyond.

Since we didn't brainstorm for a thorough list of properties, and since we didn't create a mutation that addresses oracle or lastAnswer, we missed this unreal over-approximation.
A better summarization could've been a cvl/mock function that returns a value greater than 0 if an oracle exist, or 0 otherwise.

Thanks for the feedback and good catch :)