From 06b6407b16f39bb7b8e45ba12cf0d3f8b2bb2e21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 20 Jan 2025 16:23:43 +0100
Subject: [PATCH] fix: usage and docs of rule

---
 certora/specs/Delegation.spec   | 21 +++++++--------------
 certora/specs/RevertsERC20.spec | 17 ++++++++++++++---
 2 files changed, 21 insertions(+), 17 deletions(-)

diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
index d264a09..6c46d18 100644
--- a/certora/specs/Delegation.spec
+++ b/certora/specs/Delegation.spec
@@ -217,34 +217,27 @@ 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) {
-    // Safe require as the ERC20 implementation woud revert.
-    require amount <= balanceOf(e.msg.sender);
-
-    // Safe require as zero address can't initiate transactions.
-    require e.msg.sender != 0;
-    // Safe require as transfers are non-payable functions.
     require e.msg.value == 0;
+    require e.msg.sender != 0;
 
-    // Safe require as since we consider only updates.
+    require amount <= balanceOf(e.msg.sender);
     require delegatee(to) != delegatee(e.msg.sender);
 
     requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
     assert isTotalSupplyGTEqSumOfVotingPower();
 
-    // Safe require as zeroVirtualVotingPower accounts for the delegated votes to address zero.
+    // This require avoids an impossible revert as zeroVirtualVotingPower operations comme from munging.
     require delegatee(e.msg.sender) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(e.msg.sender);
 
-    // Safe require as it is proven by delegatedLTEqDelegateeVP.
-    // The invariant itself can't be required as it's using a parameterized variable.
+    // 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);
 
     delegate@withrevert(e, e.msg.sender);
-    assert(!lastReverted);
 
-    assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0;
+    assert(!lastReverted);
 
-    // Safe require that follows from delegatedLTEqDelegateeVP.
-    require amount <= delegatedVotingPower(e.msg.sender) ;
+    assert delegatee(e.msg.sender) == e.msg.sender;
 
     assert delegatedVotingPower(to) + amount <=  totalSupply();
 }
diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 782f007..e87281d 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -16,9 +16,14 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require as it is verified in sumOfTwoDelegatedVPLTEqTotalVP.
+    require senderVotingPowerBefore + recipientVotingPowerBefore <= totalSupply();
 
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
-    require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
+    require
+      e.msg.sender != 0 => e.msg.value == 0 =>
+      amount <= balanceOfSenderBefore =>
+      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;
@@ -33,15 +38,21 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Safe require as it is verified in sumOfTwoDelegatedVPLTEqTotalVP.
+    require holderVotingPowerBefore + recipientVotingPowerBefore <= totalSupply();
+
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
-    require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
+    require
+      from != 0 => e.msg.value == 0 =>
+      amount <= balanceOfHolderBefore =>
+      delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);
 
     bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
 
     if (allowanceOfSenderBefore != max_uint256) {
-        assert lastReverted <=>  e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
+        assert lastReverted <=> e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
     } else {
         assert lastReverted <=> generalRevertConditions;
     }