refactor: change require-statements and improve docs

certora/specs/RevertsERC20.spec

@@ -14,8 +14,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require senderVotingPowerBefore >= balanceOfSenderBefore;
     // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
     require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
@@ -30,8 +30,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require holderVotingPowerBefore >= balanceOfHolderBefore;
+
     // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
     require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 

certora/specs/RevertsMintBurnEthereum.spec

@@ -14,11 +14,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -29,11 +29,11 @@ rule burnRevertConditions(env e, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;

certora/specs/RevertsMintBurnOptimism.spec

@@ -12,11 +12,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -30,8 +30,8 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require fromVotingPowerBefore >= balanceOfFromBefore;
 
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;