diff --git a/.gitignore b/.gitignore index 71f35f8..6b51f75 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,10 @@ out/ node_modules package-lock.json .env + +#certora +.certora* +.certora*.json +**.last_conf* +certora-logs +resource_errors.json diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol new file mode 100644 index 0000000..c9371d4 --- /dev/null +++ b/certora/harness/AaveTokenV3Harness.sol @@ -0,0 +1,452 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import {VersionedInitializable} from '../../src/utils/VersionedInitializable.sol'; +import {IGovernancePowerDelegationToken} from '../../src/interfaces/IGovernancePowerDelegationToken.sol'; +import {BaseAaveTokenV2} from './BaseAaveTokenV2Harness.sol'; + +contract AaveTokenV3 is BaseAaveTokenV2, IGovernancePowerDelegationToken { + mapping(address => address) internal _votingDelegateeV2; + mapping(address => address) internal _propositionDelegateeV2; + + /// @dev we assume that for the governance system 18 decimals of precision is not needed, + // by this constant we reduce it by 10, to 8 decimals + uint256 public constant POWER_SCALE_FACTOR = 1e10; + + bytes32 public constant DELEGATE_BY_TYPE_TYPEHASH = + keccak256( + 'DelegateByType(address delegator,address delegatee,GovernancePowerType delegationType,uint256 nonce,uint256 deadline)' + ); + bytes32 public constant DELEGATE_TYPEHASH = + keccak256('Delegate(address delegator,address delegatee,uint256 nonce,uint256 deadline)'); + + /// @inheritdoc IGovernancePowerDelegationToken + function delegateByType(address delegatee, GovernancePowerType delegationType) + external + virtual + override + { + _delegateByType(msg.sender, delegatee, delegationType); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function delegate(address delegatee) external override { + _delegateByType(msg.sender, delegatee, GovernancePowerType.VOTING); + _delegateByType(msg.sender, delegatee, GovernancePowerType.PROPOSITION); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function getDelegateeByType(address delegator, GovernancePowerType delegationType) + external + view + override + returns (address) + { + return _getDelegateeByType(delegator, _balances[delegator], delegationType); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function getDelegates(address delegator) external view override returns (address, address) { + DelegationAwareBalance memory delegatorBalance = _balances[delegator]; + return ( + _getDelegateeByType(delegator, delegatorBalance, GovernancePowerType.VOTING), + _getDelegateeByType(delegator, delegatorBalance, GovernancePowerType.PROPOSITION) + ); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function getPowerCurrent(address user, GovernancePowerType delegationType) + public + view + override + returns (uint256) + { + DelegationAwareBalance memory userState = _balances[user]; + uint256 userOwnPower = uint8(userState.delegationState) & (uint8(delegationType) + 1) == 0 + ? _balances[user].balance + : 0; + uint256 userDelegatedPower = _getDelegatedPowerByType(userState, delegationType); + return userOwnPower + userDelegatedPower; + } + + /// @inheritdoc IGovernancePowerDelegationToken + function getPowersCurrent(address user) external view override returns (uint256, uint256) { + return ( + getPowerCurrent(user, GovernancePowerType.VOTING), + getPowerCurrent(user, GovernancePowerType.PROPOSITION) + ); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function metaDelegateByType( + address delegator, + address delegatee, + GovernancePowerType delegationType, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external override { + require(delegator != address(0), 'INVALID_OWNER'); + //solium-disable-next-line + require(block.timestamp <= deadline, 'INVALID_EXPIRATION'); + uint256 currentValidNonce = _nonces[delegator]; + bytes32 digest = keccak256( + abi.encodePacked( + '\x19\x01', + DOMAIN_SEPARATOR, + keccak256( + abi.encode( + DELEGATE_BY_TYPE_TYPEHASH, + delegator, + delegatee, + delegationType, + currentValidNonce, + deadline + ) + ) + ) + ); + + require(delegator == ecrecover(digest, v, r, s), 'INVALID_SIGNATURE'); + unchecked { + // Does not make sense to check because it's not realistic to reach uint256.max in nonce + _nonces[delegator] = currentValidNonce + 1; + } + _delegateByType(delegator, delegatee, delegationType); + } + + /// @inheritdoc IGovernancePowerDelegationToken + function metaDelegate( + address delegator, + address delegatee, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external override { + require(delegator != address(0), 'INVALID_OWNER'); + //solium-disable-next-line + require(block.timestamp <= deadline, 'INVALID_EXPIRATION'); + uint256 currentValidNonce = _nonces[delegator]; + bytes32 digest = keccak256( + abi.encodePacked( + '\x19\x01', + DOMAIN_SEPARATOR, + keccak256(abi.encode(DELEGATE_TYPEHASH, delegator, delegatee, currentValidNonce, deadline)) + ) + ); + + require(delegator == ecrecover(digest, v, r, s), 'INVALID_SIGNATURE'); + unchecked { + // does not make sense to check because it's not realistic to reach uint256.max in nonce + _nonces[delegator] = currentValidNonce + 1; + } + _delegateByType(delegator, delegatee, GovernancePowerType.VOTING); + _delegateByType(delegator, delegatee, GovernancePowerType.PROPOSITION); + } + + /** + * @dev Modifies the delegated power of a `delegatee` account by type (VOTING, PROPOSITION). + * Passing the impact on the delegation of `delegatee` account before and after to reduce conditionals and not lose + * any precision. + * @param impactOnDelegationBefore how much impact a balance of another account had over the delegation of a `delegatee` + * before an action. + * For example, if the action is a delegation from one account to another, the impact before the action will be 0. + * @param impactOnDelegationAfter how much impact a balance of another account will have over the delegation of a `delegatee` + * after an action. + * For example, if the action is a delegation from one account to another, the impact after the action will be the whole balance + * of the account changing the delegatee. + * @param delegatee the user whom delegated governance power will be changed + * @param delegationType the type of governance power delegation (VOTING, PROPOSITION) + **/ + function _governancePowerTransferByType( + uint104 impactOnDelegationBefore, + uint104 impactOnDelegationAfter, + address delegatee, + GovernancePowerType delegationType + ) public { // public instead of internal for testing a particular condition in this function + if (delegatee == address(0)) return; + if (impactOnDelegationBefore == impactOnDelegationAfter) return; + + // To make delegated balance fit into uint72 we're decreasing precision of delegated balance by POWER_SCALE_FACTOR + uint72 impactOnDelegationBefore72 = uint72(impactOnDelegationBefore / POWER_SCALE_FACTOR); + uint72 impactOnDelegationAfter72 = uint72(impactOnDelegationAfter / POWER_SCALE_FACTOR); + + bool testCondition = (delegationType == GovernancePowerType.VOTING + && + _balances[delegatee].delegatedVotingBalance < impactOnDelegationBefore72) + || ( + delegationType == GovernancePowerType.PROPOSITION + && + _balances[delegatee].delegatedPropositionBalance < impactOnDelegationBefore72 + ); + require(!testCondition); + + if (delegationType == GovernancePowerType.VOTING) { + _balances[delegatee].delegatedVotingBalance = + _balances[delegatee].delegatedVotingBalance - + impactOnDelegationBefore72 + + impactOnDelegationAfter72; + } else { + _balances[delegatee].delegatedPropositionBalance = + _balances[delegatee].delegatedPropositionBalance - + impactOnDelegationBefore72 + + impactOnDelegationAfter72; + } + } + + /** + * @dev performs all state changes related to balance transfer and corresponding delegation changes + * @param from token sender + * @param to token recipient + * @param amount amount of tokens sent + **/ + function _transferWithDelegation( + address from, + address to, + uint256 amount + ) internal override { + if (from == to) { + return; + } + + if (from != address(0)) { + DelegationAwareBalance memory fromUserState = _balances[from]; + require(fromUserState.balance >= amount, 'ERC20: transfer amount exceeds balance'); + + uint104 fromBalanceAfter; + unchecked { + fromBalanceAfter = fromUserState.balance - uint104(amount); + } + _balances[from].balance = fromBalanceAfter; + if (fromUserState.delegationState != DelegationState.NO_DELEGATION) { + _governancePowerTransferByType( + fromUserState.balance, + fromBalanceAfter, + _getDelegateeByType(from, fromUserState, GovernancePowerType.VOTING), + GovernancePowerType.VOTING + ); + _governancePowerTransferByType( + fromUserState.balance, + fromBalanceAfter, + _getDelegateeByType(from, fromUserState, GovernancePowerType.PROPOSITION), + GovernancePowerType.PROPOSITION + ); + } + } + + if (to != address(0)) { + DelegationAwareBalance memory toUserState = _balances[to]; + uint104 toBalanceBefore = toUserState.balance; + toUserState.balance = toBalanceBefore + uint104(amount); + _balances[to] = toUserState; + + if (toUserState.delegationState != DelegationState.NO_DELEGATION) { + _governancePowerTransferByType( + toBalanceBefore, + toUserState.balance, + _getDelegateeByType(to, toUserState, GovernancePowerType.VOTING), + GovernancePowerType.VOTING + ); + _governancePowerTransferByType( + toBalanceBefore, + toUserState.balance, + _getDelegateeByType(to, toUserState, GovernancePowerType.PROPOSITION), + GovernancePowerType.PROPOSITION + ); + } + } + } + + /** + * @dev Extracts from state and returns delegated governance power (Voting, Proposition) + * @param userState the current state of a user + * @param delegationType the type of governance power delegation (VOTING, PROPOSITION) + **/ + function _getDelegatedPowerByType( + DelegationAwareBalance memory userState, + GovernancePowerType delegationType + ) internal pure returns (uint256) { + return + POWER_SCALE_FACTOR * + ( + delegationType == GovernancePowerType.VOTING + ? userState.delegatedVotingBalance + : userState.delegatedPropositionBalance + ); + } + + /** + * @dev Extracts from state and returns the delegatee of a delegator by type of governance power (Voting, Proposition) + * - If the delegator doesn't have any delegatee, returns address(0) + * @param delegator delegator + * @param userState the current state of a user + * @param delegationType the type of governance power delegation (VOTING, PROPOSITION) + **/ + function _getDelegateeByType( + address delegator, + DelegationAwareBalance memory userState, + GovernancePowerType delegationType + ) internal view returns (address) { + if (delegationType == GovernancePowerType.VOTING) { + return + /// With the & operation, we cover both VOTING_DELEGATED delegation and FULL_POWER_DELEGATED + /// as VOTING_DELEGATED is equivalent to 01 in binary and FULL_POWER_DELEGATED is equivalent to 11 + (uint8(userState.delegationState) & uint8(DelegationState.VOTING_DELEGATED)) != 0 + ? _votingDelegateeV2[delegator] + : address(0); + } + return + userState.delegationState >= DelegationState.PROPOSITION_DELEGATED + ? _propositionDelegateeV2[delegator] + : address(0); + } + + /** + * @dev Changes user's delegatee address by type of governance power (Voting, Proposition) + * @param delegator delegator + * @param delegationType the type of governance power delegation (VOTING, PROPOSITION) + * @param _newDelegatee the new delegatee + **/ + function _updateDelegateeByType( + address delegator, + GovernancePowerType delegationType, + address _newDelegatee + ) internal { + address newDelegatee = _newDelegatee == delegator ? address(0) : _newDelegatee; + if (delegationType == GovernancePowerType.VOTING) { + _votingDelegateeV2[delegator] = newDelegatee; + } else { + _propositionDelegateeV2[delegator] = newDelegatee; + } + } + + /** + * @dev Updates the specific flag which signaling about existence of delegation of governance power (Voting, Proposition) + * @param userState a user state to change + * @param delegationType the type of governance power delegation (VOTING, PROPOSITION) + * @param willDelegate next state of delegation + **/ + function _updateDelegationFlagByType( + DelegationAwareBalance memory userState, + GovernancePowerType delegationType, + bool willDelegate + ) internal pure returns (DelegationAwareBalance memory) { + if (willDelegate) { + // Because GovernancePowerType starts from 0, we should add 1 first, then we apply bitwise OR + userState.delegationState = DelegationState( + uint8(userState.delegationState) | (uint8(delegationType) + 1) + ); + } else { + // First bitwise NEGATION, ie was 01, after XOR with 11 will be 10, + // then bitwise AND, which means it will keep only another delegation type if it exists + userState.delegationState = DelegationState( + uint8(userState.delegationState) & + ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED)) + ); + } + return userState; + } + + /** + * @dev This is the equivalent of an ERC20 transfer(), but for a power type: an atomic transfer of a balance (power). + * When needed, it decreases the power of the `delegator` and when needed, it increases the power of the `delegatee` + * @param delegator delegator + * @param _delegatee the user which delegated power will change + * @param delegationType the type of delegation (VOTING, PROPOSITION) + **/ + function _delegateByType( + address delegator, + address _delegatee, + GovernancePowerType delegationType + ) internal { + // Here we unify the property that delegating power to address(0) == delegating power to yourself == no delegation + // So from now on, not being delegating is (exclusively) that delegatee == address(0) + address delegatee = _delegatee == delegator ? address(0) : _delegatee; + + // We read the whole struct before validating delegatee, because in the optimistic case + // (_delegatee != currentDelegatee) we will reuse userState in the rest of the function + DelegationAwareBalance memory delegatorState = _balances[delegator]; + address currentDelegatee = _getDelegateeByType(delegator, delegatorState, delegationType); + if (delegatee == currentDelegatee) return; + + bool delegatingNow = currentDelegatee != address(0); + bool willDelegateAfter = delegatee != address(0); + + if (delegatingNow) { + _governancePowerTransferByType(delegatorState.balance, 0, currentDelegatee, delegationType); + } + + if (willDelegateAfter) { + _governancePowerTransferByType(0, delegatorState.balance, delegatee, delegationType); + } + + _updateDelegateeByType(delegator, delegationType, delegatee); + + if (willDelegateAfter != delegatingNow) { + _balances[delegator] = _updateDelegationFlagByType( + delegatorState, + delegationType, + willDelegateAfter + ); + } + + emit DelegateChanged(delegator, delegatee, delegationType); + } + + /** + Harness section - replace struct reads and writes with function calls + */ + +// struct DelegationAwareBalance { +// uint104 balance; +// uint72 delegatedPropositionBalance; +// uint72 delegatedVotingBalance; +// bool delegatingProposition; +// bool delegatingVoting; +// } + + + function getBalance(address user) view public returns (uint104) { + return _balances[user].balance; + } + + function getDelegatedPropositionBalance(address user) view public returns (uint72) { + return _balances[user].delegatedPropositionBalance; + } + + + function getDelegatedVotingBalance(address user) view public returns (uint72) { + return _balances[user].delegatedVotingBalance; + } + + + function getDelegatingProposition(address user) view public returns (bool) { + return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } + + + function getDelegatingVoting(address user) view public returns (bool) { + return _balances[user].delegationState == DelegationState.VOTING_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } + + function getVotingDelegate(address user) view public returns (address) { + return _votingDelegateeV2[user]; + } + + function getPropositionDelegate(address user) view public returns (address) { + return _propositionDelegateeV2[user]; + } + + function getDelegatedPower(address user, GovernancePowerType delegationType) view external returns (uint256) { + DelegationAwareBalance memory userState = _balances[user]; + return _getDelegatedPowerByType(userState, delegationType); + } + + /** + End of harness section + */ +} diff --git a/certora/harness/BaseAaveTokenHarness.sol b/certora/harness/BaseAaveTokenHarness.sol new file mode 100644 index 0000000..bcc17fa --- /dev/null +++ b/certora/harness/BaseAaveTokenHarness.sol @@ -0,0 +1,161 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import {Context} from '../../lib/openzeppelin-contracts/contracts/utils/Context.sol'; +import {IERC20} from '../../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol'; +import {IERC20Metadata} from '../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol'; + +// Inspired by OpenZeppelin Contracts (last updated v4.5.0) (token/ERC20/ERC20.sol) +abstract contract BaseAaveToken is Context, IERC20Metadata { + enum DelegationState { + NO_DELEGATION, + VOTING_DELEGATED, + PROPOSITION_DELEGATED, + FULL_POWER_DELEGATED + } + + struct DelegationAwareBalance { + uint104 balance; + uint72 delegatedPropositionBalance; + uint72 delegatedVotingBalance; + DelegationState delegationState; + } + + mapping(address => DelegationAwareBalance) public _balances; + + mapping(address => mapping(address => uint256)) public _allowances; + + uint256 internal _totalSupply; + + string internal _name; + string internal _symbol; + + // @dev DEPRECATED + // kept for backwards compatibility with old storage layout + uint8 private ______DEPRECATED_OLD_ERC20_DECIMALS; + + /** + * @dev Returns the name of the token. + */ + function name() public view virtual override returns (string memory) { + return _name; + } + + /** + * @dev Returns the symbol of the token, usually a shorter version of the + * name. + */ + function symbol() public view virtual override returns (string memory) { + return _symbol; + } + + function decimals() public view virtual override returns (uint8) { + return 18; + } + + function totalSupply() public view virtual override returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view virtual override returns (uint256) { + return _balances[account].balance; + } + + function transfer(address to, uint256 amount) public virtual override returns (bool) { + address owner = _msgSender(); + _transfer(owner, to, amount); + return true; + } + + function allowance(address owner, address spender) + public + view + virtual + override + returns (uint256) + { + return _allowances[owner][spender]; + } + + function approve(address spender, uint256 amount) public virtual override returns (bool) { + address owner = _msgSender(); + _approve(owner, spender, amount); + return true; + } + + function transferFrom( + address from, + address to, + uint256 amount + ) public virtual override returns (bool) { + address spender = _msgSender(); + _spendAllowance(from, spender, amount); + _transfer(from, to, amount); + return true; + } + + function increaseAllowance(address spender, uint256 addedValue) public virtual returns (bool) { + address owner = _msgSender(); + _approve(owner, spender, _allowances[owner][spender] + addedValue); + return true; + } + + function decreaseAllowance(address spender, uint256 subtractedValue) + public + virtual + returns (bool) + { + address owner = _msgSender(); + uint256 currentAllowance = _allowances[owner][spender]; + require(currentAllowance >= subtractedValue, 'ERC20: decreased allowance below zero'); + unchecked { + _approve(owner, spender, currentAllowance - subtractedValue); + } + + return true; + } + + function _transfer( + address from, + address to, + uint256 amount + ) internal virtual { + require(from != address(0), 'ERC20: transfer from the zero address'); + require(to != address(0), 'ERC20: transfer to the zero address'); + + _transferWithDelegation(from, to, amount); + emit Transfer(from, to, amount); + } + + function _approve( + address owner, + address spender, + uint256 amount + ) internal virtual { + require(owner != address(0), 'ERC20: approve from the zero address'); + require(spender != address(0), 'ERC20: approve to the zero address'); + + _allowances[owner][spender] = amount; + emit Approval(owner, spender, amount); + } + + function _spendAllowance( + address owner, + address spender, + uint256 amount + ) internal virtual { + uint256 currentAllowance = allowance(owner, spender); + if (currentAllowance != type(uint256).max) { + require(currentAllowance >= amount, 'ERC20: insufficient allowance'); + unchecked { + _approve(owner, spender, currentAllowance - amount); + } + } + } + + function _transferWithDelegation( + address from, + address to, + uint256 amount + ) internal virtual {} +} diff --git a/certora/harness/BaseAaveTokenV2Harness.sol b/certora/harness/BaseAaveTokenV2Harness.sol new file mode 100644 index 0000000..7904063 --- /dev/null +++ b/certora/harness/BaseAaveTokenV2Harness.sol @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import {VersionedInitializable} from '../../src/utils/VersionedInitializable.sol'; +import {BaseAaveToken} from './BaseAaveTokenHarness.sol'; + +abstract contract BaseAaveTokenV2 is BaseAaveToken, VersionedInitializable { + /// @dev owner => next valid nonce to submit with permit() + mapping(address => uint256) public _nonces; + + ///////// @dev DEPRECATED from AaveToken v1 ////////////////////////// + //////// kept for backwards compatibility with old storage layout //// + uint256[3] private ______DEPRECATED_FROM_AAVE_V1; + ///////// @dev END OF DEPRECATED from AaveToken v1 ////////////////////////// + + bytes32 public DOMAIN_SEPARATOR; + + ///////// @dev DEPRECATED from AaveToken v2 ////////////////////////// + //////// kept for backwards compatibility with old storage layout //// + uint256[4] private ______DEPRECATED_FROM_AAVE_V2; + ///////// @dev END OF DEPRECATED from AaveToken v2 ////////////////////////// + + bytes public constant EIP712_REVISION = bytes('1'); + bytes32 internal constant EIP712_DOMAIN = + keccak256('EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)'); + bytes32 public constant PERMIT_TYPEHASH = + keccak256('Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)'); + + uint256 public constant REVISION = 3; + + /** + * @dev initializes the contract upon assignment to the InitializableAdminUpgradeabilityProxy + */ + function initialize() external initializer {} + + /** + * @dev implements the permit function as for https://github.com/ethereum/EIPs/blob/8a34d644aacf0f9f8f00815307fd7dd5da07655f/EIPS/eip-2612.md + * @param owner the owner of the funds + * @param spender the spender + * @param value the amount + * @param deadline the deadline timestamp, type(uint256).max for no deadline + * @param v signature param + * @param s signature param + * @param r signature param + */ + + function permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external { + require(owner != address(0), 'INVALID_OWNER'); + //solium-disable-next-line + require(block.timestamp <= deadline, 'INVALID_EXPIRATION'); + uint256 currentValidNonce = _nonces[owner]; + bytes32 digest = keccak256( + abi.encodePacked( + '\x19\x01', + DOMAIN_SEPARATOR, + keccak256(abi.encode(PERMIT_TYPEHASH, owner, spender, value, currentValidNonce, deadline)) + ) + ); + + require(owner == ecrecover(digest, v, r, s), 'INVALID_SIGNATURE'); + unchecked { + // does not make sense to check because it's not realistic to reach uint256.max in nonce + _nonces[owner] = currentValidNonce + 1; + } + _approve(owner, spender, value); + } + + /** + * @dev returns the revision of the implementation contract + */ + function getRevision() internal pure override returns (uint256) { + return REVISION; + } +} diff --git a/certora/scripts/AaveToken3_fyang1024.sh b/certora/scripts/AaveToken3_fyang1024.sh new file mode 100644 index 0000000..c9066f6 --- /dev/null +++ b/certora/scripts/AaveToken3_fyang1024.sh @@ -0,0 +1,12 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \ + --verify AaveTokenV3:certora/specs/AaveToken3_fyang1024.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --send_only \ + --msg "AaveTokenV3:AaveToken3_fyang1024.spec $1" diff --git a/certora/scripts/AaveToken3_fyang1024_useBitVectorTheory.sh b/certora/scripts/AaveToken3_fyang1024_useBitVectorTheory.sh new file mode 100644 index 0000000..a573427 --- /dev/null +++ b/certora/scripts/AaveToken3_fyang1024_useBitVectorTheory.sh @@ -0,0 +1,12 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \ + --verify AaveTokenV3:certora/specs/AaveToken3_fyang1024_useBitVectorTheory.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --settings -useBitVectorTheory \ + --msg "AaveTokenV3:AaveToken3_fyang1024_useBitVectorTheory.spec $1" diff --git a/certora/scripts/setup.sh b/certora/scripts/setup.sh new file mode 100644 index 0000000..03df365 --- /dev/null +++ b/certora/scripts/setup.sh @@ -0,0 +1,13 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \ + --verify AaveTokenV3:certora/specs/setup.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --send_only \ + --cloud \ + --msg "AaveTokenV3:setup.spec $1" diff --git a/certora/specs/AaveTokenV3_fyang1024.spec b/certora/specs/AaveTokenV3_fyang1024.spec new file mode 100644 index 0000000..f0d8056 --- /dev/null +++ b/certora/specs/AaveTokenV3_fyang1024.spec @@ -0,0 +1,312 @@ +import "./setup.spec" + +methods { + delegateByType(address delegatee, uint8 delegationType) + getDelegatedPower(address user, uint8 delegationType) returns (uint256) envfree + getDelegateeByType(address delegator, uint8 delegationType) returns (address) envfree +} + +/* + @Invariant + + @Description: + A user's total power equals to + its delegated power if the user is delegating, or + its delegated power plus its own token balance if the user is not delegating + +*/ +invariant power_equations(address user) + getDelegatingVoting(user) => getPowerCurrent(user, VOTING_POWER()) == getDelegatedPower(user, VOTING_POWER()) + && + !getDelegatingVoting(user) => getPowerCurrent(user, VOTING_POWER()) == balanceOf(user) + getDelegatedPower(user, VOTING_POWER()) + && + getDelegatingProposition(user) => getPowerCurrent(user, PROPOSITION_POWER()) == getDelegatedPower(user, PROPOSITION_POWER()) + && + !getDelegatingProposition(user) => getPowerCurrent(user, PROPOSITION_POWER()) == balanceOf(user) + getDelegatedPower(user, PROPOSITION_POWER()) + +/* + @Rule + + @Description: + calling + delegate + delegateByType + metaDelegate + metaDelegateByType + functions should have the same effect on involved accounts' + voting power + proposition power + delegate +*/ +rule equivalence_of_delegate_functions(address other) { + env e; + // delegate not to self or to zero + address self = e.msg.sender; + require other != self && other != 0; + uint256 otherDelegatedBalance = getDelegatedVotingBalance(other); + // avoid unrealistic delegated balance + require(otherDelegatedBalance < MAX_DELEGATED_BALANCE()); + // make sure the sender doesn't already delegate to other + address delegateBefore = getVotingDelegate(self); + require delegateBefore != other; + + storage init = lastStorage; + + delegate(e, other); + uint256 _myVotingPower = getPowerCurrent(self, VOTING_POWER()); + uint256 _myPropositionPower = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 _otherVotingPower = getPowerCurrent(other, VOTING_POWER()); + uint256 _otherPropositionPower = getPowerCurrent(other, PROPOSITION_POWER()); + address _myVotingDelegate = getVotingDelegate(self); + address _myPropositionDelegate = getPropositionDelegate(self); + + delegateByType(e, other, VOTING_POWER()) at init; + uint256 myVotingPower_ = getPowerCurrent(self, VOTING_POWER()); + uint256 otherVotingPower_ = getPowerCurrent(other, VOTING_POWER()); + address myVotingDelegate_ = getVotingDelegate(self); + + delegateByType(e, other, PROPOSITION_POWER()) at init; + uint256 myPropositionPower_ = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 otherPropositionPower_ = getPowerCurrent(other, PROPOSITION_POWER()); + address myPropositionDelegate_ = getPropositionDelegate(self); + + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + metaDelegate(e, self, other, deadline, v, r, s) at init; + uint256 myVotingPower_metaDelegate = getPowerCurrent(self, VOTING_POWER()); + uint256 myPropositionPower_metaDelegate = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 otherVotingPower_metaDelegate = getPowerCurrent(other, VOTING_POWER()); + uint256 otherPropositionPower_metaDelegate = getPowerCurrent(other, PROPOSITION_POWER()); + address myVotingDelegate_metaDelegate = getVotingDelegate(self); + address myPropositionDelegate_metaDelegate = getPropositionDelegate(self); + + metaDelegateByType(e, self, other, VOTING_POWER(), deadline, v, r, s) at init; + uint256 myVotingPower_metaDelegateByType = getPowerCurrent(self, VOTING_POWER()); + uint256 otherVotingPower_metaDelegateByType = getPowerCurrent(other, VOTING_POWER()); + address myVotingDelegate_metaDelegateByType = getVotingDelegate(self); + + metaDelegateByType(e, self, other, PROPOSITION_POWER(), deadline, v, r, s) at init; + uint256 myPropositionPower_metaDelegateByType = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 otherPropositionPower_metaDelegateByType = getPowerCurrent(other, PROPOSITION_POWER()); + address myPropositionDelegate_metaDelegateByType = getPropositionDelegate(self); + + assert _myVotingPower == myVotingPower_; + assert _myPropositionPower == myPropositionPower_; + assert _myVotingDelegate == myVotingDelegate_; + assert _myPropositionDelegate == myPropositionDelegate_; + assert _otherVotingPower == otherVotingPower_; + assert _otherPropositionPower == otherPropositionPower_; + + assert _myVotingPower == myVotingPower_metaDelegate; + assert _myPropositionPower == myPropositionPower_metaDelegate; + assert _myVotingDelegate == myVotingDelegate_metaDelegate; + assert _myPropositionDelegate == myPropositionDelegate_metaDelegate; + assert _otherVotingPower == otherVotingPower_metaDelegate; + assert _otherPropositionPower == otherPropositionPower_metaDelegate; + + assert _myVotingPower == myVotingPower_metaDelegateByType; + assert _myPropositionPower == myPropositionPower_metaDelegateByType; + assert _myVotingDelegate == myVotingDelegate_metaDelegateByType; + assert _myPropositionDelegate == myPropositionDelegate_metaDelegateByType; + assert _otherVotingPower == otherVotingPower_metaDelegateByType; + assert _otherPropositionPower == otherPropositionPower_metaDelegateByType; +} + +/* + @Rule + + @Description: + delegate to self and delegate to zero address are equivalent +*/ +rule equivalence_of_self_and_zero_addresses(address other) { + env e; + address self = e.msg.sender; + require self != other; + + storage init = lastStorage; + + delegate(e, self); // delegate to self + + address _myVotingDelegate = getVotingDelegate(self); + address _myPropositionDelegate = getPropositionDelegate(self); + uint256 _myVotingPower = getPowerCurrent(self, VOTING_POWER()); + uint256 _myPropositionPower = getPowerCurrent(self, PROPOSITION_POWER()); + + address _otherVotingDelegate = getVotingDelegate(other); + address _otherPropositionDelegate = getPropositionDelegate(other); + uint256 _otherVotingPower = getPowerCurrent(other, VOTING_POWER()); + uint256 _otherPropositionPower = getPowerCurrent(other, PROPOSITION_POWER()); + + delegate(e, 0) at init; // delegate to 0 + + address myVotingDelegate_ = getVotingDelegate(self); + address myPropositionDelegate_ = getPropositionDelegate(self); + uint256 myVotingPower_ = getPowerCurrent(self, VOTING_POWER()); + uint256 myPropositionPower_ = getPowerCurrent(self, PROPOSITION_POWER()); + + address otherVotingDelegate_ = getVotingDelegate(other); + address otherPropositionDelegate_ = getPropositionDelegate(other); + uint256 otherVotingPower_ = getPowerCurrent(other, VOTING_POWER()); + uint256 otherPropositionPower_ = getPowerCurrent(other, PROPOSITION_POWER()); + + assert _myVotingDelegate == myVotingDelegate_; + assert _myPropositionDelegate == myPropositionDelegate_; + assert _myVotingPower == myVotingPower_; + assert _myPropositionPower == myPropositionPower_; + + assert _otherVotingDelegate == otherVotingDelegate_; + assert _otherPropositionDelegate == otherPropositionDelegate_; + assert _otherVotingPower == otherVotingPower_; + assert _otherPropositionPower == otherPropositionPower_; +} + + +/* + @Rule + + @Description: + If a user has not delegated to anyone and now delegates to self, + it should affect nothing. +*/ +rule self_delegation_affects_nothing(address other) { + env e; + address self = e.msg.sender; + require self != other; + + address _myVotingDelegate = getVotingDelegate(self); + address _myPropositionDelegate = getPropositionDelegate(self); + uint256 _myVotingPower = getPowerCurrent(self, VOTING_POWER()); + uint256 _myPropositionPower = getPowerCurrent(self, PROPOSITION_POWER()); + + require _myVotingDelegate == 0 && _myPropositionDelegate == 0; // not delegating to anyone + + address _otherVotingDelegate = getVotingDelegate(other); + address _otherPropositionDelegate = getPropositionDelegate(other); + uint256 _otherVotingPower = getPowerCurrent(other, VOTING_POWER()); + uint256 _otherPropositionPower = getPowerCurrent(other, PROPOSITION_POWER()); + + delegate(e, self); // delegate to self + + address myVotingDelegate_ = getVotingDelegate(self); + address myPropositionDelegate_ = getPropositionDelegate(self); + uint256 myVotingPower_ = getPowerCurrent(self, VOTING_POWER()); + uint256 myPropositionPower_ = getPowerCurrent(self, PROPOSITION_POWER()); + + address otherVotingDelegate_ = getVotingDelegate(other); + address otherPropositionDelegate_ = getPropositionDelegate(other); + uint256 otherVotingPower_ = getPowerCurrent(other, VOTING_POWER()); + uint256 otherPropositionPower_ = getPowerCurrent(other, PROPOSITION_POWER()); + + assert _myVotingDelegate == myVotingDelegate_; + assert _myPropositionDelegate == myPropositionDelegate_; + assert _myVotingPower == myVotingPower_; + assert _myPropositionPower == myPropositionPower_; + + assert _otherVotingDelegate == otherVotingDelegate_; + assert _otherPropositionDelegate == otherPropositionDelegate_; + assert _otherVotingPower == otherVotingPower_; + assert _otherPropositionPower == otherPropositionPower_; +} + +/* + @Rule + + @Description: + If a user has delegated to someone and now delegate to someone else, + it should only affect delegatees' power, while not affecting self and other's power. +*/ +rule changing_delegatee_affects_delegatees_only(address newDelegatee, uint8 delegationType, address other) { + env e; + address self = e.msg.sender; + require self != other && self != newDelegatee && newDelegatee != other && newDelegatee != 0; + require delegationType == VOTING_POWER() || delegationType == PROPOSITION_POWER(); + if (delegationType == VOTING_POWER()) { + require getDelegatingVoting(self); + } else { + require getDelegatingProposition(self); + } + address delegatee = getDelegateeByType(self, delegationType); + require delegatee != other && delegatee != self && delegatee != newDelegatee && delegatee != 0; + + uint256 selfBalance = balanceOf(self); + uint256 _selfPower = getPowerCurrent(self, delegationType); + uint256 _delegateePower = getPowerCurrent(delegatee, delegationType); + uint256 _newDelegateePower = getPowerCurrent(newDelegatee, delegationType); + uint256 _otherPower = getPowerCurrent(other, delegationType); + + require selfBalance < MAX_DELEGATED_BALANCE(); + require _selfPower < MAX_DELEGATED_BALANCE(); + require _delegateePower < MAX_DELEGATED_BALANCE(); + require _newDelegateePower < MAX_DELEGATED_BALANCE(); + require _selfPower >= selfBalance; + + delegateByType(e, newDelegatee, delegationType); // change delegate + + uint256 selfPower_ = getPowerCurrent(self, delegationType); + uint256 delegateePower_ = getPowerCurrent(delegatee, delegationType); + uint256 newDelegateePower_ = getPowerCurrent(newDelegatee, delegationType); + uint256 otherPower_ = getPowerCurrent(other, delegationType); + + assert getDelegateeByType(self, delegationType) == newDelegatee; + assert _selfPower == selfPower_; // selfPower does not change + assert _delegateePower - normalize(selfBalance) == delegateePower_; // delegateePower decreased by selfBalance + assert _newDelegateePower + normalize(selfBalance) == newDelegateePower_; // newDelegateePower increased by selfBalance + assert _otherPower == otherPower_; // otherPower does not change +} + +/* + @Rule + + @Description: + If a user delegates to the same address more than once, the subsequent delegations do not change anything +*/ +rule idempotency_of_delegation(address delegatee) { + env e; + address self = e.msg.sender; + + delegate(e, delegatee); // first delegation + uint256 _myVotingPower = getPowerCurrent(self, VOTING_POWER()); + uint256 _myPropositionPower = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 _delegateeVotingPower = getPowerCurrent(delegatee, VOTING_POWER()); + uint256 _delegateePropositionPower = getPowerCurrent(delegatee, PROPOSITION_POWER()); + address _myVotingDelegate = getVotingDelegate(self); + address _myPropositionDelegate = getPropositionDelegate(self); + + delegate(e, delegatee); // second delegation + uint256 myVotingPower_ = getPowerCurrent(self, VOTING_POWER()); + uint256 myPropositionPower_ = getPowerCurrent(self, PROPOSITION_POWER()); + uint256 delegateeVotingPower_ = getPowerCurrent(delegatee, VOTING_POWER()); + uint256 delegateePropositionPower_ = getPowerCurrent(delegatee, PROPOSITION_POWER()); + address myVotingDelegate_ = getVotingDelegate(self); + address myPropositionDelegate_ = getPropositionDelegate(self); + + assert _myVotingDelegate == myVotingDelegate_; + assert _myPropositionDelegate == myPropositionDelegate_; + assert _myVotingPower == myVotingPower_; + assert _myPropositionPower == myPropositionPower_; + assert _delegateeVotingPower == delegateeVotingPower_; + assert _delegateePropositionPower == delegateePropositionPower_; +} + +/* + @Rule + + @Description: + only transferring functions affect user's token balance +*/ +rule only_transfer_affect_balance(address user, method f) { + + uint256 _balance = balanceOf(user); + + env e; + calldataarg args; + f(e, args); + + uint256 balance_ = balanceOf(user); + + assert _balance != balance_ => + f.selector == transfer(address, uint256).selector || + f.selector == transferFrom(address, address, uint256).selector; +} \ No newline at end of file diff --git a/certora/specs/AaveTokenV3_fyang1024_useBitVectorTheory.spec b/certora/specs/AaveTokenV3_fyang1024_useBitVectorTheory.spec new file mode 100644 index 0000000..ae81297 --- /dev/null +++ b/certora/specs/AaveTokenV3_fyang1024_useBitVectorTheory.spec @@ -0,0 +1,161 @@ +import "./AaveTokenV3_fyang1024.spec" + +/* + @Rule + + @Description: + If a user has not delegated to anyone and now delegate, + it should decrease self power but increase delegatee power by its balance, while not affecting other's power. + + @Note: + This rule needs to be run with --settings -useBitVectorTheory flag, but the server threw + [java.lang.IllegalStateException: max size of bit vector 256 literals exceeded by + 115792089237316195423570985008687907853269984665640564039457584007913129639936], + hence this rule has not been verified yet. +*/ +rule delegate_affects_self_and_delegatee_only(address delegatee, uint8 delegationType, address other) { + env e; + address self = e.msg.sender; + require self != other && self != delegatee && delegatee != other && delegatee != 0; + require delegationType == VOTING_POWER() || delegationType == PROPOSITION_POWER(); + if (delegationType == VOTING_POWER()) { + require !getDelegatingVoting(self); + } else { + require !getDelegatingProposition(self); + } + require getDelegateeByType(self, delegationType) == 0; // not delegating now + + uint256 selfBalance = balanceOf(self); + uint256 _selfPower = getPowerCurrent(self, delegationType); + uint256 _delegateePower = getPowerCurrent(delegatee, delegationType); + uint256 _otherPower = getPowerCurrent(other, delegationType); + + require selfBalance < MAX_DELEGATED_BALANCE(); + require _selfPower < MAX_DELEGATED_BALANCE(); + require _delegateePower < MAX_DELEGATED_BALANCE(); + require _selfPower >= selfBalance; + + delegateByType(e, delegatee, delegationType); + + uint256 selfPower_ = getPowerCurrent(self, delegationType); + uint256 delegateePower_ = getPowerCurrent(delegatee, delegationType); + uint256 otherPower_ = getPowerCurrent(other, delegationType); + + assert getDelegateeByType(self, delegationType) == delegatee; + assert _selfPower - selfBalance == selfPower_; // selfPower decreased by selfBalance + assert _delegateePower + normalize(selfBalance) == delegateePower_; // delegateePower increased by selfBalance + assert _otherPower == otherPower_; // otherPower does not change +} + +/* + @Rule + + @Description: + If a user has delegated to someone and now undelegates (delegates to self), + it should increase self power but decrease delegatee power, while not affecting other power. + + @Note: + This rule needs to be run with --settings -useBitVectorTheory flag, but the server threw + [java.lang.IllegalStateException: max size of bit vector 256 literals exceeded by + 115792089237316195423570985008687907853269984665640564039457584007913129639936], + hence this rule has not been verified yet. +*/ +rule undelegate_affects_self_and_delegatee_only(uint8 delegationType, address other) { + env e; + address self = e.msg.sender; + require self != other; + require delegationType == VOTING_POWER() || delegationType == PROPOSITION_POWER(); + + if (delegationType == VOTING_POWER()) { + require getDelegatingVoting(self); + } else { + require getDelegatingProposition(self); + } + address delegatee = getDelegateeByType(self, delegationType); + require delegatee != other && delegatee != self && delegatee != 0; + + uint256 selfBalance = balanceOf(self); + uint256 _selfPower = getPowerCurrent(self, delegationType); + uint256 _delegateePower = getPowerCurrent(delegatee, delegationType); + uint256 _otherPower = getPowerCurrent(other, delegationType); + + require selfBalance < MAX_DELEGATED_BALANCE(); + require _selfPower < MAX_DELEGATED_BALANCE(); + require _delegateePower < MAX_DELEGATED_BALANCE(); + require _delegateePower >= selfBalance; + + delegateByType(e, self, delegationType); // undelegate + + uint256 selfPower_ = getPowerCurrent(self, delegationType); + uint256 delegateePower_ = getPowerCurrent(delegatee, delegationType); + uint256 otherPower_ = getPowerCurrent(other, delegationType); + + assert getDelegateeByType(self, delegationType) == 0; // no delegatee anymore + assert _selfPower + selfBalance == selfPower_; // selfPower increased by selfBalance + assert _delegateePower - normalize(selfBalance) == delegateePower_; // delegateePower decreased by selfBalance + assert _otherPower == otherPower_; // otherPower does not change +} + +/* + @Rule + + @Description: + delegation of voting power should not affect proposition power, and vice versa. + + @Note: + This rule needs to be run with --settings -useBitVectorTheory flag, but the server threw + [java.lang.IllegalStateException: max size of bit vector 256 literals exceeded by + 115792089237316195423570985008687907853269984665640564039457584007913129639936], + hence this rule has not been verified yet. +*/ +rule independency_of_delegation_types(uint8 delegationType) { + env e; + address self = e.msg.sender; + address other; + require other != 0 && other != self; + require delegationType == VOTING_POWER() || delegationType == PROPOSITION_POWER(); + + uint8 otherDelegationType; + if (delegationType == VOTING_POWER()) { + otherDelegationType = PROPOSITION_POWER(); + } else { + otherDelegationType = VOTING_POWER(); + } + + uint256 _selfPower = getPowerCurrent(self, otherDelegationType); + uint256 _otherPower = getPowerCurrent(other, otherDelegationType); + address _delegatee; + if (otherDelegationType == VOTING_POWER()) { + _delegatee = getVotingDelegate(self); + } else { + _delegatee = getPropositionDelegate(self); + } + bool _delegating; + if (otherDelegationType == VOTING_POWER()) { + _delegating = getDelegatingVoting(self); + } else { + _delegating = getDelegatingProposition(self); + } + + delegateByType(e, other, delegationType); + + uint256 selfPower_ = getPowerCurrent(self, otherDelegationType); + uint256 otherPower_ = getPowerCurrent(other, otherDelegationType); + address delegatee_; + if (otherDelegationType == VOTING_POWER()) { + delegatee_ = getVotingDelegate(self); + } else { + delegatee_ = getPropositionDelegate(self); + } + bool delegating_; + if (otherDelegationType == VOTING_POWER()) { + delegating_ = getDelegatingVoting(self); + } else { + delegating_ = getDelegatingProposition(self); + } + + assert _selfPower == selfPower_; + assert _otherPower == otherPower_; + assert _delegatee == delegatee_; + assert _delegating == delegating_; +} \ No newline at end of file diff --git a/certora/specs/setup.spec b/certora/specs/setup.spec new file mode 100644 index 0000000..077401f --- /dev/null +++ b/certora/specs/setup.spec @@ -0,0 +1,138 @@ +/** + + Setup for writing rules for Aave Token v3 + +*/ + +/** + Public methods from the AaveTokenV3Harness.sol +*/ + +methods{ + totalSupply() returns (uint256) envfree + balanceOf(address addr) returns (uint256) envfree + transfer(address to, uint256 amount) returns (bool) + transferFrom(address from, address to, uint256 amount) returns (bool) + delegate(address delegatee) + metaDelegate(address, address, uint256, uint8, bytes32, bytes32) + getPowerCurrent(address user, uint8 delegationType) returns (uint256) envfree + getBalance(address user) returns (uint104) envfree + getDelegatedPropositionBalance(address user) returns (uint72) envfree + getDelegatedVotingBalance(address user) returns (uint72) envfree + getDelegatingProposition(address user) returns (bool) envfree + getDelegatingVoting(address user) returns (bool) envfree + getVotingDelegate(address user) returns (address) envfree + getPropositionDelegate(address user) returns (address) envfree +} + +/** + + Constants + +*/ +// GovernancyType enum from the token contract +definition VOTING_POWER() returns uint8 = 0; +definition PROPOSITION_POWER() returns uint8 = 1; + +definition DELEGATED_POWER_DIVIDER() returns uint256 = 10^10; + +// 16000000 * 10^18 is the maximum supply of the AAVE token +definition MAX_DELEGATED_BALANCE() returns uint256 = 16000000 * 10^18 / DELEGATED_POWER_DIVIDER(); + +/** + + Function that normalizes (removes 10 least significant digits) a given param. + It mirrors the way delegated balances are stored in the token contract. Since the delegated + balance is stored as a uint72 variable, delegated amounts (uint256()) are normalized. + +*/ + +function normalize(uint256 amount) returns uint256 { + return to_uint256(amount / DELEGATED_POWER_DIVIDER() * DELEGATED_POWER_DIVIDER()); +} + +/** + + Testing correctness of delegate(). An example of a unit test + +*/ + +rule delegateCorrectness(address bob) { + env e; + // delegate not to self or to zero + require bob != e.msg.sender && bob != 0; + + uint256 bobDelegatedBalance = getDelegatedVotingBalance(bob); + // avoid unrealistic delegated balance + require(bobDelegatedBalance < MAX_DELEGATED_BALANCE()); + + // verify that the sender doesn't already delegate to bob + address delegateBefore = getVotingDelegate(e.msg.sender); + require delegateBefore != bob; + + uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + uint256 delegatorBalance = balanceOf(e.msg.sender); + + delegate(e, bob); + + // test the delegate indeed has changed to bob + address delegateAfter = getVotingDelegate(e.msg.sender); + assert delegateAfter == bob; + + // test the delegate's new voting power + uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + assert bobVotingPowerAfter == bobVotingPowerBefore + normalize(delegatorBalance); +} + +/** + + Verify that only delegate functions can change someone's delegate. + An example for a parametric rule. + +*/ + +rule votingDelegateChanges(address alice, method f) { + env e; + calldataarg args; + + address aliceDelegateBefore = getVotingDelegate(alice); + + f(e, args); + + address aliceDelegateAfter = getVotingDelegate(alice); + + // only these four function may change the delegate of an address + assert aliceDelegateAfter != aliceDelegateBefore => + f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector; +} + +/** + + A ghost variable that tracks the sum of all addresses' balances + +*/ +ghost mathint sumBalances { + init_state axiom sumBalances == 0; +} + +/** + + This hook updates the sumBalances ghost whenever any address balance is updated + +*/ +hook Sstore _balances[KEY address user].balance uint104 balance + (uint104 old_balance) STORAGE { + sumBalances = sumBalances - to_mathint(old_balance) + to_mathint(balance); + } + +/** + + Invariant: + sum of all addresses' balances should be always equal to the total supply of the token + +*/ +invariant totalSupplyEqualsBalances() + sumBalances == totalSupply() \ No newline at end of file diff --git a/properties.md b/properties.md index 0a485ae..501a1a8 100644 --- a/properties.md +++ b/properties.md @@ -30,7 +30,6 @@ $t_1$ → the state of the system after a transaction. ## General rules -- The total power (of one type) of all users in the system is less or equal than the sum of balances of all AAVE holders (totalSupply of AAVE token): $$\sum powerOfAccount_i <= \sum balanceOf(account_i)$$ - If an account is delegating a power to itself or to `address(0)`, that means that account is not delegating that power to anybody: $$powerOfAccountX = (accountXDelegatingPower \ ? \ 0 : balanceOf(accountX)) + diff --git a/resource_errors.json b/resource_errors.json new file mode 100644 index 0000000..d9bd792 --- /dev/null +++ b/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/src/AaveTokenV3.sol b/src/AaveTokenV3.sol index 1806c75..c94d192 100644 --- a/src/AaveTokenV3.sol +++ b/src/AaveTokenV3.sol @@ -6,6 +6,8 @@ import {IGovernancePowerDelegationToken} from './interfaces/IGovernancePowerDele import {BaseAaveTokenV2} from './BaseAaveTokenV2.sol'; contract AaveTokenV3 is BaseAaveTokenV2, IGovernancePowerDelegationToken { + + mapping(address => address) internal _votingDelegateeV2; mapping(address => address) internal _propositionDelegateeV2; diff --git a/src/BaseAaveTokenV3.sol b/src/BaseAaveTokenV3.sol new file mode 100644 index 0000000..9b773a8 --- /dev/null +++ b/src/BaseAaveTokenV3.sol @@ -0,0 +1,84 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import {VersionedInitializable} from './utils/VersionedInitializable.sol'; + +import {BaseAaveToken} from './BaseAaveToken.sol'; + +abstract contract BaseAaveTokenV2 is BaseAaveToken, VersionedInitializable { + /// @dev owner => next valid nonce to submit with permit() + mapping(address => uint256) public _nonces; + + ///////// @dev DEPRECATED from AaveToken v1 ////////////////////////// + //////// kept for backwards compatibility with old storage layout //// + uint256[3] private ______DEPRECATED_FROM_AAVE_V1; + ///////// @dev END OF DEPRECATED from AaveToken v1 ////////////////////////// + + bytes32 public DOMAIN_SEPARATOR; + + ///////// @dev DEPRECATED from AaveToken v2 ////////////////////////// + //////// kept for backwards compatibility with old storage layout //// + uint256[4] private ______DEPRECATED_FROM_AAVE_V2; + ///////// @dev END OF DEPRECATED from AaveToken v2 ////////////////////////// + + bytes public constant EIP712_REVISION = bytes('1'); + bytes32 internal constant EIP712_DOMAIN = + keccak256('EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)'); + bytes32 public constant PERMIT_TYPEHASH = + keccak256('Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)'); + + uint256 public constant REVISION = 3; // TODO: CHECK, but most probably was 2 before + + /** + * @dev initializes the contract upon assignment to the InitializableAdminUpgradeabilityProxy + */ + function initialize() external initializer {} + + /** + * @dev implements the permit function as for https://github.com/ethereum/EIPs/blob/8a34d644aacf0f9f8f00815307fd7dd5da07655f/EIPS/eip-2612.md + * @param owner the owner of the funds + * @param spender the spender + * @param value the amount + * @param deadline the deadline timestamp, type(uint256).max for no deadline + * @param v signature param + * @param s signature param + * @param r signature param + */ + + function permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external { + require(owner != address(0), 'INVALID_OWNER'); + //solium-disable-next-line + require(block.timestamp <= deadline, 'INVALID_EXPIRATION'); + uint256 currentValidNonce = _nonces[owner]; + bytes32 digest = keccak256( + abi.encodePacked( + '\x19\x01', + DOMAIN_SEPARATOR, + keccak256(abi.encode(PERMIT_TYPEHASH, owner, spender, value, currentValidNonce, deadline)) + ) + ); + + require(owner == ecrecover(digest, v, r, s), 'INVALID_SIGNATURE'); + unchecked { + // does not make sense to check because it's not realistic to reach uint256.max in nonce + _nonces[owner] = currentValidNonce + 1; + } + _approve(owner, spender, value); + } + + /** + * @dev returns the revision of the implementation contract + */ + function getRevision() internal pure override returns (uint256) { + return REVISION; + } +}