[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/Delegation.spec

@@ -159,7 +159,6 @@ invariant sumOfTwoDelegatedVPLTEqTotalVP()
         }
     }
 
-
 function isTotalSupplyGTEqSumOfVotingPower() returns bool {
     requireInvariant totalSupplyIsSumOfVirtualVotingPower();
     return totalSupply() >= sumOfVotes[2^160];
@@ -215,3 +214,37 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg
         assert delegatedVotingPower(delegation.delegatee) == delegatedVotingPowerBefore + balanceOf(delegator);
     }
 }
+
+// Check that the delegated voting power of a delegatee after an update is lesser than or equal to the total supply of tokens.
+rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) {
+    // Safe require as implementation woud revert.
+    require amount <= balanceOf(e.msg.sender);
+
+    // Safe rquire as zero address can't initiate transactions.
+    require e.msg.sender != 0;
+
+    // Safe require as since we consider only updates.
+    require delegatee(to) != delegatee(e.msg.sender);
+
+    delegate@withrevert(e, e.msg.sender);
+    if (!lastReverted) {
+           assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0;
+
+           // Safe require that follows from delegatedLTEqDelegateeVP.
+           require amount <= delegatedVotingPower(e.msg.sender) ;
+
+           requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
+           requireInvariant sumOfVotesStartsAtZero();
+           requireInvariant sumOfVotesGrowsCorrectly();
+           requireInvariant sumOfVotesMonotone();
+           requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+           requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
+
+           assert isTotalSupplyGTEqSumOfVotingPower();
+
+           assert delegatedVotingPower(to) + amount <=  totalSupply();
+       } else {
+           // Do not check anything
+           assert true;
+       }
+}

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();
@@ -112,12 +110,17 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
+    // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero.
+    require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore;
+
     // run transaction
     burn@withrevert(e, amount);
 
     // check outcome
     if (lastReverted) {
-        assert e.msg.sender == 0x0 ||  fromBalanceBefore < amount || fromVotingPowerBefore < amount ;
+        assert e.msg.sender == 0x0 || fromBalanceBefore < amount;
     } else {
         // updates balance and totalSupply
         assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;

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;
@@ -113,13 +112,17 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
+    // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero.
+    require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore;
+
     // run transaction
     burn@withrevert(e, from,  amount);
 
     // check outcome
     if (lastReverted) {
-           assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount
-               || e.msg.sender != currentContract.bridge;
+        assert e.msg.sender == 0x0 || fromBalanceBefore < amount || e.msg.sender != currentContract.bridge;
     } else {
         // updates balance and totalSupply
         assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;

certora/specs/RevertsERC20.spec

@@ -15,9 +15,10 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require senderVotingPowerBefore >= balanceOfSenderBefore;
-    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
-    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + senderVotingPowerBefore <= totalSupply();
+    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply.
+    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -31,9 +32,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require holderVotingPowerBefore >= balanceOfHolderBefore;
-    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
-    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply();
+    require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply
+    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);
 

certora/specs/RevertsMintBurnEthereum.spec

@@ -33,7 +33,7 @@ rule burnRevertConditions(env e, uint256 amount) {
     require delegatee(0) == 0;
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require delegateeVotingPowerBefore >= balanceOfSenderBefore;
+    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;

certora/specs/RevertsMintBurnOptimism.spec

@@ -31,7 +31,7 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     require delegatee(0) == 0;
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require fromVotingPowerBefore >= balanceOfFromBefore;
+    require  delegatee(from) != 0 =>fromVotingPowerBefore >= balanceOfFromBefore;
 
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;