feat: tweak to conform to diff

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

Hide file tree

Showing 3 changed files with 36 additions and 56 deletions.
diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
@@ -32,6 +32,33 @@ 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
@@ -1,40 +1,17 @@
-import "Delegation.spec";
+// This is spec is taken from the Open Zeppelin repositories at https://github.com/OpenZeppelin/openzeppelin-contracts/blob/448efeea6640bbbc09373f03fbc9c88e280147ba/certora/specs/ERC20.spec, and patched to support the DelegationToken.
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ 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)
-    );
-}
+import "Delegation.spec";
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rules: only mint and burn can change total supply                                                                   │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule noChangeTotalSupply(env e, method f) {
+rule noChangeTotalSupply(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     requireInvariant balancesLTEqTotalSupply();
 
+    method f;
     calldataarg args;
 
     uint256 totalSupplyBefore = totalSupply();

diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec
@@ -1,41 +1,17 @@
-import "Delegation.spec";
+// This is spec is taken from the Open Zeppelin repositories at https://github.com/OpenZeppelin/openzeppelin-contracts/blob/448efeea6640bbbc09373f03fbc9c88e280147ba/certora/specs/ERC20.spec, and patched to support the DelegationToken.
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ 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)
-    );
-}
+import "Delegation.spec";
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rules: only mint and burn can change total supply                                                                   │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule noChangeTotalSupply(env e, method f) {
+rule noChangeTotalSupply(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     requireInvariant balancesLTEqTotalSupply();
 
+    method f;
     calldataarg args;
 
     uint256 totalSupplyBefore = totalSupply();
@@ -119,7 +95,7 @@ rule burn(env e) {
 
     // check outcome
     if (lastReverted) {
-           assert e.msg.sender == 0x0 ||  fromBalanceBefore < amount || fromVotingPowerBefore < amount
+           assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount
                || e.msg.sender != currentContract.bridge;
     } else {
         // updates balance and totalSupply