refactor: use new invariants in ERC20 spec

morpho-org · Dec 10, 2024 · 9132208 · 9132208
1 parent bbbee4a
commit 9132208
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
@@ -71,6 +71,7 @@ rule onlyHolderOrSpenderCanChangeAllowance(env e, method f){
 */
 rule transfer(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant twoBalancesLTEqTotalSupply();
     require nonpayable(e);
 
 
@@ -86,9 +87,6 @@ rule transfer(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
-    // Safe require as it's proven by the rule twoBalancesCannotExceedTotalSupply.
-    require holder != recipient => balanceOf(holder) + balanceOf(recipient) <= totalSupply();
-
     // run transaction
     transfer@withrevert(e, recipient, amount);
 
@@ -114,6 +112,7 @@ rule transfer(env e) {
 */
 rule transferFrom(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant twoBalancesLTEqTotalSupply();
     require nonpayable(e);
 
     address spender = e.msg.sender;
@@ -130,9 +129,6 @@ rule transferFrom(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
-    // Safe require as it's proven by the rule twoBalancesCannotExceedTotalSupply.
-    require holder != recipient => balanceOf(holder) + balanceOf(recipient) <= totalSupply();
-
     // run transaction
     transferFrom@withrevert(e, holder, recipient, amount);