Skip to content

Commit

Permalink
docs: apply suggestions from code review
Browse files Browse the repository at this point in the history
Signed-off-by: Colin | Morpho 🦋 <colin@morpho.xyz>
  • Loading branch information
colin-morpho authored Dec 10, 2024
1 parent a712cf9 commit de8f6e2
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions certora/specs/RevertsERC20.spec
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) {

// 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.
// Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;

transfer@withrevert(e, to, amount);
Expand All @@ -33,7 +33,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
// 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.
// Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;

transferFrom@withrevert(e, from, to, amount);
Expand Down

0 comments on commit de8f6e2

Please sign in to comment.