refactor: readability

morpho-org · Feb 4, 2025 · 4de56d8 · 4de56d8
1 parent 619435e
commit 4de56d8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
@@ -220,7 +220,6 @@ rule updatedDelegatedVPLTEqTotalSupply(address from, address to) {
     uint256 balanceOfFromBefore = balanceOf(from);
     uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to));
     uint256 totalSupplyBefore = totalSupply();
-    env e;
 
     requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
     assert isTotalSupplyGTEqSumOfVotingPower();
@@ -235,6 +234,7 @@ rule updatedDelegatedVPLTEqTotalSupply(address from, address to) {
 
     require delegatee(from) != 0 => delegatedVotingPower(delegatee(from)) >= balanceOfFromBefore;
 
+    env e;
     // Safe require-statements to perform a ghost call to delegate(from).
     require e.msg.value == 0;
     require e.msg.sender == from;