[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.
Fixes #107.

[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.

[QGarchery]

Which implementation ? This is not as other rules, this one is to be used as an invariant. This means that you can require what you want, it will just have to be added in the premisses. For example, if you have the following rule:

require A;
require B;
assert C;

then later on you will be able to have the following "safe require":
require A => B => C;

[colin-morpho]

You're right indeed!

[colin-morpho]

I changed the require in fdbcc97.

[QGarchery]

The commit linked does not change this part of the code right ?

[QGarchery]

The new code still mentions "safe require because XXX implementation would revert", but this rule is not tied to any particular function called. Indeed this will be used as an invariant.
Those require statements are "safe" because then you would add them as premises when you use use that property. This is the same as in my message above, by doing require A => B => C. This would be similar as doing requireInvariant inv() if inv is the invariant A => B => C. You wouldn't say that, in such an invariant, A or B is a safe premise because a particular implementation would revert