diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol index d0e13c6..6a8a099 100644 --- a/certora/harness/AaveTokenV3Harness.sol +++ b/certora/harness/AaveTokenV3Harness.sol @@ -8,48 +8,50 @@ pragma solidity ^0.8.0; -import {AaveTokenV3} from "../../src/AaveTokenV3.sol"; +import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; contract AaveTokenV3Harness is AaveTokenV3 { - - // returns user's token balance, used in some community rules - function getBalance(address user) view public returns (uint104) { + // returns user's token balance, used in some community rules + function getBalance(address user) public view returns (uint104) { return _balances[user].balance; - } - // returns user's delegated proposition balance - function getDelegatedPropositionBalance(address user) view public returns (uint72) { + } + + // returns user's delegated proposition balance + function getDelegatedPropositionBalance(address user) public view returns (uint72) { return _balances[user].delegatedPropositionBalance; - } + } - // returns user's delegated voting balance - function getDelegatedVotingBalance(address user) view public returns (uint72) { + // returns user's delegated voting balance + function getDelegatedVotingBalance(address user) public view returns (uint72) { return _balances[user].delegatedVotingBalance; - } - - //returns user's delegating proposition status - function getDelegatingProposition(address user) view public returns (bool) { - return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } - - // returns user's delegating voting status - function getDelegatingVoting(address user) view public returns (bool) { - return _balances[user].delegationState == DelegationState.VOTING_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } - - // returns user's voting delegate - function getVotingDelegate(address user) view public returns (address) { + } + + //returns user's delegating proposition status + function getDelegatingProposition(address user) public view returns (bool) { + return + _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } + + // returns user's delegating voting status + function getDelegatingVoting(address user) public view returns (bool) { + return + _balances[user].delegationState == DelegationState.VOTING_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } + + // returns user's voting delegate + function getVotingDelegate(address user) public view returns (address) { return _votingDelegateeV2[user]; - } + } - // returns user's proposition delegate - function getPropositionDelegate(address user) view public returns (address) { + // returns user's proposition delegate + function getPropositionDelegate(address user) public view returns (address) { return _propositionDelegateeV2[user]; - } + } - // returns user's delegation state - function getDelegationState(address user) view public returns (DelegationState) { + // returns user's delegation state + function getDelegationState(address user) public view returns (DelegationState) { return _balances[user].delegationState; - } -} \ No newline at end of file + } +} diff --git a/certora/harness/AaveTokenV3HarnessCommunity.sol b/certora/harness/AaveTokenV3HarnessCommunity.sol index ace06bf..cd1dde1 100644 --- a/certora/harness/AaveTokenV3HarnessCommunity.sol +++ b/certora/harness/AaveTokenV3HarnessCommunity.sol @@ -2,57 +2,56 @@ /** - This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for + This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for community-written rules */ pragma solidity ^0.8.0; -import {AaveTokenV3} from "../../src/AaveTokenV3.sol"; +import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; contract AaveTokenV3Harness is AaveTokenV3 { - function getBalance(address user) view public returns (uint104) { + function getBalance(address user) public view returns (uint104) { return _balances[user].balance; - } + } - function getDelegatedPropositionBalance(address user) view public returns (uint72) { + function getDelegatedPropositionBalance(address user) public view returns (uint72) { return _balances[user].delegatedPropositionBalance; - } - + } - function getDelegatedVotingBalance(address user) view public returns (uint72) { + function getDelegatedVotingBalance(address user) public view 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 getDelegatingProposition(address user) public view 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 getDelegatingVoting(address user) public view returns (bool) { + return + _balances[user].delegationState == DelegationState.VOTING_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } - function getVotingDelegate(address user) view public returns (address) { + function getVotingDelegate(address user) public view returns (address) { return _votingDelegateeV2[user]; - } + } - function getPropositionDelegate(address user) view public returns (address) { + function getPropositionDelegate(address user) public view returns (address) { return _propositionDelegateeV2[user]; - } + } - function getDelegationState(address user) view public returns (DelegationState) { + function getDelegationState(address user) public view returns (DelegationState) { return _balances[user].delegationState; - } + } - function getNonce(address user) view public returns (uint256) { + function getNonce(address user) public view returns (uint256) { return _nonces[user]; - } + } - function ecrecoverWrapper( + function ecrecoverWrapper( bytes32 hash, uint8 v, bytes32 r, @@ -61,7 +60,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { return ecrecover(hash, v, r, s); } - function computeMetaDelegateHash( + function computeMetaDelegateHash( address delegator, address delegatee, uint256 deadline, @@ -77,7 +76,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { return digest; } - function computeMetaDelegateByTypeHash( + function computeMetaDelegateByTypeHash( address delegator, address delegatee, GovernancePowerType delegationType, @@ -102,5 +101,4 @@ contract AaveTokenV3Harness is AaveTokenV3 { ); return digest; } - -} \ No newline at end of file +} diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol index 4c77b29..fa9e764 100644 --- a/certora/harness/AaveTokenV3HarnessStorage.sol +++ b/certora/harness/AaveTokenV3HarnessStorage.sol @@ -4,7 +4,7 @@ This is an extension of the harnessed AaveTokenV3 with added getters on the _balances fields. The imported harnessed AaveTokenV3 contract uses uint8 instead of an enum for delegation state. - + This modification is introduced to bypass a current Certora Prover limitation on accessing enum fields inside CVL hooks @@ -12,45 +12,44 @@ pragma solidity ^0.8.0; -import {AaveTokenV3} from "../munged/AaveTokenV3.sol"; +import {AaveTokenV3} from '../munged/AaveTokenV3.sol'; contract AaveTokenV3Harness is AaveTokenV3 { - function getBalance(address user) view public returns (uint104) { + function getBalance(address user) public view returns (uint104) { return _balances[user].balance; - } + } - function getDelegatedPropositionBalance(address user) view public returns (uint72) { + function getDelegatedPropositionBalance(address user) public view returns (uint72) { return _balances[user].delegatedPropositionBalance; - } - + } - function getDelegatedVotingBalance(address user) view public returns (uint72) { + function getDelegatedVotingBalance(address user) public view returns (uint72) { return _balances[user].delegatedVotingBalance; - } + } - - function getDelegatingProposition(address user) view public returns (bool) { + function getDelegatingProposition(address user) public view returns (bool) { uint8 state = _balances[user].delegationState; - return state == uint8(DelegationState.PROPOSITION_DELEGATED) || - state == uint8(DelegationState.FULL_POWER_DELEGATED); - } - + return + state == uint8(DelegationState.PROPOSITION_DELEGATED) || + state == uint8(DelegationState.FULL_POWER_DELEGATED); + } - function getDelegatingVoting(address user) view public returns (bool) { + function getDelegatingVoting(address user) public view returns (bool) { uint8 state = _balances[user].delegationState; - return state == uint8(DelegationState.VOTING_DELEGATED) || - state == uint8(DelegationState.FULL_POWER_DELEGATED); - } + return + state == uint8(DelegationState.VOTING_DELEGATED) || + state == uint8(DelegationState.FULL_POWER_DELEGATED); + } - function getVotingDelegate(address user) view public returns (address) { + function getVotingDelegate(address user) public view returns (address) { return _votingDelegateeV2[user]; - } + } - function getPropositionDelegate(address user) view public returns (address) { + function getPropositionDelegate(address user) public view returns (address) { return _propositionDelegateeV2[user]; - } + } - function getDelegationState(address user) view public returns (uint8) { + function getDelegationState(address user) public view returns (uint8) { return _balances[user].delegationState; - } -} \ No newline at end of file + } +} diff --git a/certora/harness/README.md b/certora/harness/README.md index e7d1aaa..2338a7d 100644 --- a/certora/harness/README.md +++ b/certora/harness/README.md @@ -3,5 +3,5 @@ We use two harnesses: - AaveTokenV3Harness adds a few simple getters to the original AaveTokenV3 code - AaveTokenV3HarnessStorage is used to verify general.spec. It changes delegationState field in _balances -to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which -patches the original code with `applyHarness.patch` patch. \ No newline at end of file +to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which +patches the original code with `applyHarness.patch` patch.