From 3fb5d42be3cc7e6e8e9de8d94cab4ce2f32fd922 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 3 Feb 2025 18:33:13 +0100 Subject: [PATCH] fix: implement review suggestions --- certora/specs/Delegation.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index 6c46d18..90eb28a 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -229,6 +229,8 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { // This require avoids an impossible revert as zeroVirtualVotingPower operations comme from munging. require delegatee(e.msg.sender) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(e.msg.sender); + uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to)); + // This invariant can't be required as it's using a parameterized variable. // But it is proven by delegatedLTEqDelegateeVP. require delegatee(e.msg.sender) != 0 => delegatedVotingPower(delegatee(e.msg.sender)) >= balanceOf(e.msg.sender); @@ -239,5 +241,5 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { assert delegatee(e.msg.sender) == e.msg.sender; - assert delegatedVotingPower(to) + amount <= totalSupply(); + assert delegatedVotingPowerDelegateeToBefore + amount <= totalSupply(); }