chore: revert onlyAuthorizeCanTransfer refactor

morpho-org · Dec 9, 2024 · 1c74c95 · 1c74c95
1 parent 1ee1291
commit 1c74c95
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 27 deletions.
diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
@@ -32,33 +32,6 @@ use invariant totalSupplyIsSumOfBalances;
 
 use invariant zeroAddressNoBalance;
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyAuthorizedCanTransfer(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-    requireInvariant balancesLTEqTotalSupply();
-    requireInvariant twoBalancesLTEqTotalSupply();
-
-    method f;
-    calldataarg args;
-    address account;
-
-    uint256 allowanceBefore = allowance(account, e.msg.sender);
-    uint256 balanceBefore   = balanceOf(account);
-    f(e, args);
-    uint256 balanceAfter    = balanceOf(account);
-
-    assert (
-        balanceAfter < balanceBefore
-    ) => (
-        e.msg.sender == account ||
-        f.selector == sig:transferFrom(address, address, uint256).selector && balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
-    );
-}
-
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it          │

diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec
@@ -2,6 +2,32 @@
 
 import "Delegation.spec";
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    requireInvariant twoBalancesLTEqTotalSupply();
+
+    calldataarg args;
+    address account;
+
+    uint256 allowanceBefore = allowance(account, e.msg.sender);
+    uint256 balanceBefore   = balanceOf(account);
+    f(e, args);
+    uint256 balanceAfter    = balanceOf(account);
+
+    assert (
+        balanceAfter < balanceBefore
+    ) => (
+        e.msg.sender == account ||
+        f.selector == sig:transferFrom(address, address, uint256).selector && balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
+    );
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rules: only mint and burn can change total supply                                                                   │

diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec
@@ -2,6 +2,33 @@
 
 import "Delegation.spec";
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    requireInvariant twoBalancesLTEqTotalSupply();
+
+    calldataarg args;
+    address account;
+
+    uint256 allowanceBefore = allowance(account, e.msg.sender);
+    uint256 balanceBefore   = balanceOf(account);
+    f(e, args);
+    uint256 balanceAfter    = balanceOf(account);
+
+    assert (
+        balanceAfter < balanceBefore
+    ) => (
+        f.selector == sig:burn(address, uint256).selector ||
+        e.msg.sender == account ||
+        f.selector == sig:transferFrom(address, address, uint256).selector && balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
+    );
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rules: only mint and burn can change total supply                                                                   │