[Certora] Check underflow and overflows.

[gd-colin]

The ERC20 specification is patched to take support the possible (in practice impossible) overflows.
We should prove that these operations are safe.

[QGarchery]

Related comments:

• ERC20.spec
• MintAndBurn.spec

[gd-colin]

As of today, proving properties w.r.t delegatee's voting power with Certora seem really difficult. Instead, in a61550f we assume them to be true and prove that there are no overflows under these hypothesis. Closing this issue as we see no way to prove the required properties.

[gd-colin]

In #102 #104 we have managed to prove these invariants, they are now used in ERC20 and MintBurn specs instead of require-statements. I think this issue can be closed now, w.d.y.t. @QGarchery ?

[QGarchery]

It would be best if we could only add "safe requires" and not change the spec of overflows because of the delegation feature.
For example, here we have the condition holderVotingPowerBefore < amount. But I think this could be replaced by something like require holderBalanceHefore <= holderVotingPowerBefore, which would be added before the "check outcome" comment