[Certora] Handle overflows

[colin-morpho]

Replace absurd revert conditions with safe requirements that have been proven.
Fixes a very small typo in the certora/README.md.
Closes #97.

[colin-morpho]

I think it's even possible to actually require the invariants themselves.

[QGarchery]

Looks great, but it seems like there are more of the same to do in MintBurn specification. For example:

morpho-token/certora/specs/MintBurnEthereum.spec

Line 80 in 2ebbdff

toVotingPowerBefore + amount > max_uint256;

[colin-morpho]

I think it's even possible to actually require the invariants themselves.

Actually it isn't because the invriants require the munging setup which introduce new possible owerflows related to the zero virtual voting power.

toVotingPowerBefore + amount > max_uint256;

@QGarchery I think this is a legitimate reason to revert, isn't it?

Fixed in 6ab5bad.

[QGarchery]

A couple more to fix :

morpho-token/certora/specs/MintBurnEthereum.spec

Line 118 in 6ab5bad

assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount ;

[colin-morpho]

A couple more to fix :

@QGarchery, I haven't managed to get these ones do not go through because of the same reason as :

Actually it isn't because the invriants require the munging setup which introduce new possible owerflows related to the zero virtual voting power.

In particular, when votes are delegated to zero, burn subtracts the amount from the zeroVirtualVotingPower causing a revert that is caught by fromVotingPowerBefore < amount .

[QGarchery]

In particular, when votes are delegated to zero, burn subtracts the amount from the zeroVirtualVotingPower causing a revert that is caught by fromVotingPowerBefore < amount

Good point, but I think we can still frame it in terms of a "safe require". Here the invariant that we would want is that the balance of the sender is less that _zeroVirtualVotingPower in case where the sender delegates to 0

[colin-morpho]

Good point, but I think we can still frame it in terms of a "safe require". Here the invariant that we would want is that the balance of the sender is less that _zeroVirtualVotingPower in case where the sender delegates to 0

Just requiring the delegatee(from) == 0 => fromBalanceBefore <= _zeroVirtualVotingPower isn't enough (see this run), it looks like the prover isn't able to figure out that amount <= fromBalanceBefore <= fromVotingPowerBefore.