fix: update to new invariants

morpho-org · Dec 10, 2024 · d648654 · d648654
1 parent 9132208
commit d648654
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 12 deletions.
diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec
@@ -56,6 +56,7 @@ rule noChangeTotalSupply(env e) {
 rule mint(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     requireInvariant balancesLTEqTotalSupply();
+    requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
     assert isTotalSupplyGTEqSumOfVotingPower();
     requireInvariant zeroAddressNoVotingPower();
     require nonpayable(e);
@@ -70,9 +71,6 @@ rule mint(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
-    // Safe require thats follows from delegatedVotingPowerLTEqTotalVotingPower.
-    require toVotingPowerBefore <= sumOfVotingPower;
-
     // run transaction
     mint@withrevert(e, to, amount);
 
@@ -100,6 +98,7 @@ rule burn(env e) {
     requireInvariant balancesLTEqTotalSupply();
     assert isTotalSupplyGTEqSumOfVotingPower();
     requireInvariant zeroAddressNoVotingPower();
+    requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
     require nonpayable(e);
 
     address from;
@@ -113,9 +112,6 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
-    // Safe require that follows from delegatedVotingPowerLTEqTotalVotingPower. 
-    require fromVotingPowerBefore <= sumOfVotingPower;
-
     // run transaction
     burn@withrevert(e, amount);
 

diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec
@@ -58,6 +58,7 @@ rule mint(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     requireInvariant balancesLTEqTotalSupply();
     assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
     requireInvariant zeroAddressNoVotingPower();
     require nonpayable(e);
 
@@ -71,9 +72,6 @@ rule mint(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
-    // Safe require that follows from delegatedVotingPowerLTEqTotalVotingPower. 
-    require toVotingPowerBefore <= sumOfVotingPower;
-
     // run transaction
     mint@withrevert(e, to, amount);
 
@@ -100,6 +98,7 @@ rule mint(env e) {
 rule burn(env e) {
     requireInvariant balancesLTEqTotalSupply();
     assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
     requireInvariant zeroAddressNoVotingPower();
     require nonpayable(e);
 
@@ -114,9 +113,6 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
-    // Safe require that follows from delegatedVotingPowerLTEqTotalVotingPower. 
-    require fromVotingPowerBefore <= sumOfVotingPower;
-
     // run transaction
     burn@withrevert(e, from,  amount);