fix: change unsafe require

certora/specs/Delegation.spec

@@ -159,7 +159,6 @@ invariant sumOfTwoDelegatedVPLTEqTotalVP()
         }
     }
 
-
 function isTotalSupplyGTEqSumOfVotingPower() returns bool {
     requireInvariant totalSupplyIsSumOfVirtualVotingPower();
     return totalSupply() >= sumOfVotes[2^160];
@@ -215,3 +214,33 @@ 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(e, e.msg.sender);
+
+    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();
+}

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;