[Certora] Handle overflows

certora/README.md

@@ -51,7 +51,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`ExternalCalls.spec`](specs/ExternalCalls.spec) checks that the Morpho token implementation is reentrancy safe by ensuring that no function is making and external calls and, that the implementation is immutable as it doesn't perform any delegate call;
 - [`ERC20Invariants.spec`](specs/ERC20Invariants.spec) common hooks and invariants to be shared in different specs;
 - [`ERC20.spec`](specs/ERC20.spec) ensures that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification, we also check Morpho token `burn` and `mint` functions in [`MintBurnEthereum`](specs/MintBurnEthereum.spec) and [`MintBurnOptimism`](specs/MintBurnOptimism.spec);
-- [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation.
+- [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation;
 - [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec) check that conditions for reverts and inputs are correctly validated.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version.

certora/specs/ERC20.spec

@@ -87,14 +87,17 @@ rule transfer(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require holderBalanceBefore <= holderVotingPowerBefore;
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply();
+
     // run transaction
     transfer@withrevert(e, recipient, amount);
 
     // check outcome
     if (lastReverted) {
-        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore ||
-            // Handle overflows in delegation, should not be possible.
-            recipientVotingPowerBefore + amount > max_uint256 || holderVotingPowerBefore < amount ;
+        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
     } else {
         // balances of holder and recipient are updated
         assert to_mathint(balanceOf(holder))    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
@@ -129,14 +132,17 @@ rule transferFrom(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require holderBalanceBefore <= holderVotingPowerBefore;
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply();
+
     // run transaction
     transferFrom@withrevert(e, holder, recipient, amount);
 
     // check outcome
     if (lastReverted) {
-        assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore
-            // Handle overflows in delegation, should not be possible.
-            ||  amount + recipientVotingPowerBefore > max_uint256 || holderVotingPowerBefore < amount ;
+        assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
     } else {
         // allowance is valid & updated
         assert allowanceBefore            >= amount;

certora/specs/MintBurnEthereum.spec

@@ -67,7 +67,6 @@ rule mint(env e) {
 
     // cache state
     uint256 toBalanceBefore    = balanceOf(to);
-    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
@@ -76,8 +75,7 @@ rule mint(env e) {
 
     // check outcome
     if (lastReverted) {
-        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
-            toVotingPowerBefore + amount > max_uint256;
+        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ;
     } else {
         // updates balance and totalSupply
         assert e.msg.sender == owner();

certora/specs/MintBurnOptimism.spec

@@ -68,7 +68,6 @@ rule mint(env e) {
 
     // cache state
     uint256 toBalanceBefore    = balanceOf(to);
-    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
@@ -78,7 +77,7 @@ rule mint(env e) {
     // check outcome
     if (lastReverted) {
         assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
-            toVotingPowerBefore + amount > max_uint256 || e.msg.sender != currentContract.bridge;
+            e.msg.sender != currentContract.bridge;
     } else {
         // updates balance and totalSupply
         assert e.msg.sender == currentContract.bridge;