fix: add missing hypothesis in transfer rules

morpho-org · Jan 16, 2025 · f121755 · f121755
1 parent f6f5b89
commit f121755
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
@@ -88,9 +88,9 @@ rule transfer(env e) {
     uint256 otherBalanceBefore     = balanceOf(other);
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require holderBalanceBefore <= holderVotingPowerBefore;
+    require delegatee(holder) != 0 => holderBalanceBefore <= holderVotingPowerBefore;
     // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
-    require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply();
+    require delegatee(holder) != delegatee(recipient) => recipientVotingPowerBefore + holderBalanceBefore <= totalSupply();
 
     // run transaction
     transfer@withrevert(e, recipient, amount);
@@ -133,9 +133,9 @@ rule transferFrom(env e) {
     uint256 otherBalanceBefore     = balanceOf(other);
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
-    require holderBalanceBefore <= holderVotingPowerBefore;
+    require delegatee(holder) != 0 => holderBalanceBefore <= holderVotingPowerBefore;
     // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
-    require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply();
+    require delegatee(holder) != delegatee(recipient) => recipientVotingPowerBefore + holderBalanceBefore <= totalSupply();
 
     // run transaction
     transferFrom@withrevert(e, holder, recipient, amount);