fix: soundness issue and improve readability

certora/specs/Delegation.spec

@@ -216,30 +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 amount) {
+    require from != 0;
+
+    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 amount <= balanceOf(from);
+    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 >= balanceOf(from);
 
     uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to));
+    uint256 totalSupplyBefore = totalSupply();
 
     // 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)) >= balanceOf(from);
 
-    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 delegatedVotingPowerDelegateeToBefore + amount <=  totalSupply();
+    assert delegatedVotingPowerDelegateeToBefore + amount <= totalSupplyBefore;
 }

certora/specs/RevertsERC20.spec

@@ -21,7 +21,7 @@ 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 =>
+      e.msg.sender != 0 =>
       amount <= balanceOfSenderBefore =>
       delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
 
@@ -43,7 +43,7 @@ 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 =>
+      from != 0 =>
       amount <= balanceOfHolderBefore =>
       delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();