refactor: simplify revert causes

morpho-org · Dec 16, 2024 · 6ab5bad · 6ab5bad
1 parent 2ebbdff
commit 6ab5bad
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec
@@ -67,7 +67,6 @@ rule mint(env e) {
 
     // cache state
     uint256 toBalanceBefore    = balanceOf(to);
-    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
@@ -76,8 +75,7 @@ rule mint(env e) {
 
     // check outcome
     if (lastReverted) {
-        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
-            toVotingPowerBefore + amount > max_uint256;
+        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ;
     } else {
         // updates balance and totalSupply
         assert e.msg.sender == owner();

diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec
@@ -68,7 +68,6 @@ rule mint(env e) {
 
     // cache state
     uint256 toBalanceBefore    = balanceOf(to);
-    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
@@ -78,7 +77,7 @@ rule mint(env e) {
     // check outcome
     if (lastReverted) {
         assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
-            toVotingPowerBefore + amount > max_uint256 || e.msg.sender != currentContract.bridge;
+            e.msg.sender != currentContract.bridge;
     } else {
         // updates balance and totalSupply
         assert e.msg.sender == currentContract.bridge;