Skip to content

Commit

Permalink
docs: improve comment
Browse files Browse the repository at this point in the history
  • Loading branch information
colin-morpho committed Jan 16, 2025
1 parent 376c4fd commit 65567c2
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 @@ -17,7 +17,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
// Safe require as it is verified in delegatedLTEqDelegateeVP.
require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;

// Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply.
// Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();

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 delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
// Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply
// Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();

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

0 comments on commit 65567c2

Please sign in to comment.