refactor: safe require in MintBurn

morpho-org · Jan 14, 2025 · 2279357 · 2279357
1 parent 6ab5bad
commit 2279357
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 3 deletions.
diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec
@@ -110,12 +110,17 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
+    // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero.
+    require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore;
+
     // run transaction
     burn@withrevert(e, amount);
 
     // check outcome
     if (lastReverted) {
-        assert e.msg.sender == 0x0 ||  fromBalanceBefore < amount || fromVotingPowerBefore < amount ;
+        assert e.msg.sender == 0x0 || fromBalanceBefore < amount;
     } else {
         // updates balance and totalSupply
         assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;

diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec
@@ -112,13 +112,17 @@ rule burn(env e) {
     uint256 otherBalanceBefore = balanceOf(other);
     uint256 totalSupplyBefore  = totalSupply();
 
+    // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero.
+    require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore;
+
     // run transaction
     burn@withrevert(e, from,  amount);
 
     // check outcome
     if (lastReverted) {
-           assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount
-               || e.msg.sender != currentContract.bridge;
+        assert e.msg.sender == 0x0 || fromBalanceBefore < amount || e.msg.sender != currentContract.bridge;
     } else {
         // updates balance and totalSupply
         assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;