From 1c09db876fdef798444ac9922867c90f8d816660 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 9 Dec 2024 16:53:48 +0100 Subject: [PATCH] refactor: change require-statements and improve docs --- certora/specs/RevertsERC20.spec | 9 +++++---- certora/specs/RevertsMintBurnEthereum.spec | 12 ++++++------ certora/specs/RevertsMintBurnOptimism.spec | 10 +++++----- 3 files changed, 16 insertions(+), 15 deletions(-) diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index 1fa7738..22567a4 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -14,8 +14,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) { uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender)); uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to)); - // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. - require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require senderVotingPowerBefore >= balanceOfSenderBefore; // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance. require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore; @@ -30,8 +30,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from)); uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to)); - // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. - require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require holderVotingPowerBefore >= balanceOfHolderBefore; + // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance. require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore; diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec index 63a1d1f..bbc5d1b 100644 --- a/certora/specs/RevertsMintBurnEthereum.spec +++ b/certora/specs/RevertsMintBurnEthereum.spec @@ -14,11 +14,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) { uint256 balanceOfSenderBefore = balanceOf(e.msg.sender); uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); - // Safe require as zero address can't possibly delegate voting power. + // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower . require delegatee(0) == 0; - // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens - require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply(); + // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. + require toVotingPowerBefore <= totalSupply(); mint@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256; @@ -29,11 +29,11 @@ rule burnRevertConditions(env e, uint256 amount) { uint256 balanceOfSenderBefore = balanceOf(e.msg.sender); uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender)); - // Safe require as zero address can't possibly delegate voting power. + // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower . require delegatee(0) == 0; - // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. - require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require delegateeVotingPowerBefore >= balanceOfSenderBefore; burn@withrevert(e, amount); assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec index 5d2b1fe..cfcb818 100644 --- a/certora/specs/RevertsMintBurnOptimism.spec +++ b/certora/specs/RevertsMintBurnOptimism.spec @@ -12,11 +12,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) { mathint totalSupplyBefore = totalSupply(); uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); - // Safe require as zero address can't possibly delegate voting power. + // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower . require delegatee(0) == 0; - // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens - require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply(); + // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. + require toVotingPowerBefore <= totalSupply(); mint@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256; @@ -30,8 +30,8 @@ rule burnRevertConditions(env e, address from, uint256 amount) { // Safe require as zero address can't possibly delegate voting power. require delegatee(0) == 0; - // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. - require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require fromVotingPowerBefore >= balanceOfFromBefore; burn@withrevert(e, from, amount); assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount || e.msg.value != 0;