From 75370ef69778f70d168ff454e7dd6bb1291bff49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Tue, 10 Dec 2024 14:28:33 +0100 Subject: [PATCH] refactor: simplify require statements --- certora/specs/RevertsERC20.spec | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index ac12d3b..026f1bf 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -16,8 +16,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) { // Safe require as it is verified in delegatedLTEqDelegateeVP. require senderVotingPowerBefore >= balanceOfSenderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower(). - require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore; + // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower(). + require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + senderVotingPowerBefore <= totalSupply(); transfer@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; @@ -33,11 +33,13 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun // Safe require as it is verified in delegatedLTEqDelegateeVP. require holderVotingPowerBefore >= balanceOfHolderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower(). - require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore; + // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower(). + require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply(); transferFrom@withrevert(e, from, to, amount); + bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0; + if (allowanceOfSenderBefore != max_uint256) { assert lastReverted <=> e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions; } else {