Unsound "safe" require delegatedLTEqDelegateeVP

[QGarchery]

The invariant delegatedLTEqDelegateeVP proves that:
forall A, A != 0 => balanceOf(A) <= delegatedVotingPower(delegatee(A))
Notice the clause A != 0, which comes from:

morpho-token/certora/specs/ERC20Invariants.spec

Line 13 in d828ef0

axiom A != 0;

However, it seems like it is used without this clause:

• morpho-token/certora/specs/RevertsERC20.spec

  Lines 17 to 18 in d828ef0

  	// Safe require as it is verified in delegatedLTEqDelegateeVP.
  	require senderVotingPowerBefore >= balanceOfSenderBefore;

• morpho-token/certora/specs/RevertsERC20.spec

  Lines 33 to 34 in d828ef0

  	// Safe require as it is verified in delegatedLTEqDelegateeVP.
  	require holderVotingPowerBefore >= balanceOfHolderBefore;

• morpho-token/certora/specs/RevertsMintBurnEthereum.spec

  Lines 35 to 36 in d828ef0

  	// Safe require as it is verified in delegatedLTEqDelegateeVP.
  	require delegateeVotingPowerBefore >= balanceOfSenderBefore;

• morpho-token/certora/specs/RevertsMintBurnOptimism.spec

  Lines 33 to 34 in d828ef0

  	// Safe require as it is verified in delegatedLTEqDelegateeVP.
  	require fromVotingPowerBefore >= balanceOfFromBefore;

[colin-morpho]

Is it though, for instance in

morpho-token/certora/specs/RevertsERC20.spec

Line 23 in d828ef0

assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;

we show that if the sender = 0 then it reverts, so implicitly we check our hypothesis A != 0. Also, this is why it's not assumed, as we want to check it. The other assumption is only to avoid overflows related to computing the _zerorVirtualVotingPower. I'm not convinced that there's a real issue here.

[QGarchery]

we show that if the sender=0 then it reverts, so implicitly we check our hypothesis A != 0.

I don't think so, because if the sender=0 then you make an assumption with require senderVotingPowerBefore >= balanceOfSenderBefore; and then it is checked that it reverts. This assumption may remove cases where you wanted to check that it reverts.

In general I think we should be very careful with require statements, and not simplify them. Notably, I tried adding the premise and the prover didn't succeed, so for now I'm quite convinced that there is an issue in this case

[colin-morpho]

Ok, so approximation is not really unsound. This is because of the rule delegatingUpdatesVotingPower, msg.sender can execute delegateVotingPower(msg.sender) to re-delagate to himself, which makes the case delegatee(e.msg.sender) == 0 trivial in all situations. This is proved in f55c098.

[QGarchery]

Nice ! So as a default we can add the exact formula that is proven, and then refine later and add proofs as you did