Revert "chore: update specs"

This reverts commit 94fef53.

certora/confs/RevertsMintBurnEthereum.conf

@@ -1,13 +1,12 @@
 {
   "files": [
-    "certora/helpers/MorphoTokenEthereumHarness.sol",
-    "certora/helpers/MorphoTokenOptimismHarness.sol"
+    "src/MorphoTokenEthereum.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenEthereumHarness"
+    "MorphoTokenEthereum"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenEthereumHarness:certora/specs/RevertsMintBurnEthereum.spec",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [

certora/confs/RevertsMintBurnOptimism.conf

@@ -1,13 +1,12 @@
 {
   "files": [
-    "certora/helpers/MorphoTokenEthereumHarness.sol",
-    "certora/helpers/MorphoTokenOptimismHarness.sol"
+    "src/MorphoTokenOptimism.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenOptimismHarness"
+    "MorphoTokenOptimism"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenOptimismHarness:certora/specs/RevertsMintBurnOptimism.spec",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [

certora/specs/RevertsMintBurnEthereum.spec

@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-import "Delegation.spec";
-
 methods {
     function owner() external returns address envfree;
     function totalSupply() external returns uint256 envfree;
@@ -12,36 +10,30 @@ methods {
 
 // Check the revert conditions for the burn function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens.
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
 
-    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
-    require toVotingPowerBefore <= sumOfVotingPower;
+    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
-
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
-    // Safe requires because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => balanceOfSenderBefore <= delegateeVotingPowerBefore;
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
 
-    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
-    require delegateeVotingPowerBefore <= sumOfVotingPower;
-    require amount <= delegateeVotingPowerBefore;
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
+    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;

certora/specs/RevertsMintBurnOptimism.spec

@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-import "Delegation.spec";
-
 methods {
     function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
@@ -11,36 +9,30 @@ methods {
 
 // Check the revert conditions for the mint function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
     // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
-    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
-    require toVotingPowerBefore <= sumOfVotingPower;
-
-
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, address from, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     uint256 balanceOfFromBefore = balanceOf(from);
     uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
 
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
     // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
 
-    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
-    require fromVotingPowerBefore <= sumOfVotingPower;
-    require amount <= fromVotingPowerBefore;
-
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
 }