[Certora] Handle overflows

certora/specs/Delegation.spec

@@ -216,28 +216,34 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg
 }
 
 // Check that the updated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens.
-rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) {
+rule updatedDelegatedVPLTEqTotalSupply(address from, address to) {
+    uint256 balanceOfFromBefore = balanceOf(from);
+    uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to));
+    uint256 totalSupplyBefore = totalSupply();
+    env e;
+
     require e.msg.value == 0;
-    require e.msg.sender != 0;
+    require e.msg.sender == from;
 
-    require amount <= balanceOf(e.msg.sender);
-    require delegatee(to) != delegatee(e.msg.sender);
+    require from != 0;
+    require delegatee(to) != delegatee(from);
 
     requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
     assert isTotalSupplyGTEqSumOfVotingPower();
 
     // This require avoids an impossible revert as zeroVirtualVotingPower operations comme from munging.
-    require delegatee(e.msg.sender) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(e.msg.sender);
+    require delegatee(from) == 0 => currentContract._zeroVirtualVotingPower >=  balanceOfFromBefore;
+
 
     // This invariant can't be required as it's using a parameterized variable.
     // But it is proven by delegatedLTEqDelegateeVP.
-    require delegatee(e.msg.sender) != 0 => delegatedVotingPower(delegatee(e.msg.sender)) >= balanceOf(e.msg.sender);
+    require delegatee(from) != 0 => delegatedVotingPower(delegatee(from)) >= balanceOfFromBefore;
 
-    delegate@withrevert(e, e.msg.sender);
+    delegate@withrevert(e, from);
 
     assert(!lastReverted);
 
-    assert delegatee(e.msg.sender) == e.msg.sender;
+    assert delegatee(from) == from;
 
-    assert delegatedVotingPower(to) + amount <=  totalSupply();
+    assert delegatedVotingPowerDelegateeToBefore + balanceOfFromBefore <= totalSupplyBefore;
 }

certora/specs/RevertsERC20.spec

@@ -21,9 +21,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
 
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require
-      e.msg.sender != 0 => e.msg.value == 0 =>
-      amount <= balanceOfSenderBefore =>
-      delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
+      e.msg.sender != 0 =>
+      delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + balanceOfSenderBefore <= totalSupply();
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -43,9 +42,8 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
 
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require
-      from != 0 => e.msg.value == 0 =>
-      amount <= balanceOfHolderBefore =>
-      delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
+      from != 0 =>
+      delegatee(to) != delegatee(from) => recipientVotingPowerBefore +  balanceOfHolderBefore <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);