fix: change style

morpho-org · Jan 15, 2025 · a73bda1 · a73bda1
1 parent 273104e
commit a73bda1
Showing 1 changed file with 12 additions and 14 deletions.
diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
@@ -227,23 +227,21 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) {
     require delegatee(to) != delegatee(e.msg.sender);
 
     delegate@withrevert(e, e.msg.sender);
+    bool reverted = lastReverted;
 
-    if (!lastReverted) {
+    assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0;
 
-        assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0;
+    // Safe require that follows from delegatedLTEqDelegateeVP.
+    require amount <= delegatedVotingPower(e.msg.sender) ;
 
-        // Safe require that follows from delegatedLTEqDelegateeVP.
-        require amount <= delegatedVotingPower(e.msg.sender) ;
-
-        requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
-        requireInvariant sumOfVotesStartsAtZero();
-        requireInvariant sumOfVotesGrowsCorrectly();
-        requireInvariant sumOfVotesMonotone();
-        requireInvariant totalSupplyIsSumOfVirtualVotingPower();
-        requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
+    requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
+    requireInvariant sumOfVotesStartsAtZero();
+    requireInvariant sumOfVotesGrowsCorrectly();
+    requireInvariant sumOfVotesMonotone();
+    requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+    requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
 
-        assert isTotalSupplyGTEqSumOfVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
 
-        assert delegatedVotingPower(to) + amount <=  totalSupply();
-    }
+    assert !reverted => delegatedVotingPower(to) + amount <=  totalSupply();
 }