From 9f99f114655e329183c7927a1be9d2090aee84ec Mon Sep 17 00:00:00 2001 From: nisnislevi Date: Thu, 29 Jun 2023 19:02:07 +0300 Subject: [PATCH] Certora Review CVL2 --- .github/workflows/certora-erc20.yml | 58 ---- .github/workflows/certora.yml | 19 +- certora/Makefile | 2 - certora/applyHarness.patch | 66 +---- certora/conf/community.conf | 14 + certora/conf/delegate.conf | 14 + certora/conf/erc20.conf | 14 + certora/conf/general.conf | 15 + certora/harness/AaveTokenV3Harness.sol | 13 +- .../harness/AaveTokenV3HarnessCommunity.sol | 74 +++-- certora/harness/AaveTokenV3HarnessStorage.sol | 19 +- certora/scripts/erc20.sh | 4 +- certora/scripts/verifyCommunity.sh | 2 + certora/scripts/verifyDelegate.sh | 2 + certora/scripts/verifyGeneral.sh | 4 +- certora/specs/base.spec | 80 +++--- certora/specs/community.spec | 99 ++++--- certora/specs/delegate.spec | 272 +++++++++--------- certora/specs/erc20.spec | 62 ++-- certora/specs/general.spec | 40 +-- src/BaseAaveToken.sol | 2 +- 21 files changed, 416 insertions(+), 459 deletions(-) delete mode 100644 .github/workflows/certora-erc20.yml create mode 100644 certora/conf/community.conf create mode 100644 certora/conf/delegate.conf create mode 100644 certora/conf/erc20.conf create mode 100644 certora/conf/general.conf diff --git a/.github/workflows/certora-erc20.yml b/.github/workflows/certora-erc20.yml deleted file mode 100644 index 664c381..0000000 --- a/.github/workflows/certora-erc20.yml +++ /dev/null @@ -1,58 +0,0 @@ -name: certora-erc20 - -on: - push: - branches: - - main - pull_request: - branches: - - main - - workflow_dispatch: - -jobs: - verify: - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v2 - - - name: Check key - env: - CERTORAKEY: ${{ secrets.CERTORAKEY }} - run: echo "key length" ${#CERTORAKEY} - - - name: Install python - uses: actions/setup-python@v2 - with: { python-version: 3.9 } - - - name: Install java - uses: actions/setup-java@v1 - with: { java-version: "11", java-package: jre } - - - name: Install certora cli - run: pip install certora-cli - - - name: Install solc - run: | - wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux - chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc8.13 - - - name: Verify rule ${{ matrix.rule }} - run: | - cd certora - touch applyHarness.patch - make munged - cd .. - echo "key length" ${#CERTORAKEY} - sh certora/scripts/${{ matrix.rule }} - env: - CERTORAKEY: ${{ secrets.CERTORAKEY }} - - strategy: - fail-fast: false - max-parallel: 16 - matrix: - rule: - - erc20.sh diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 31c092d..0fcae6d 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -16,11 +16,8 @@ jobs: steps: - uses: actions/checkout@v2 - - - name: Check key - env: - CERTORAKEY: ${{ secrets.CERTORAKEY }} - run: echo "key length" ${#CERTORAKEY} + with: + submodules: recursive - name: Install python uses: actions/setup-python@v2 @@ -31,7 +28,7 @@ jobs: with: { java-version: "11", java-package: jre } - name: Install certora cli - run: pip install certora-cli + run: pip3 install certora-cli-beta - name: Install solc run: | @@ -46,7 +43,7 @@ jobs: make munged cd .. echo "key length" ${#CERTORAKEY} - sh certora/scripts/${{ matrix.rule }} + certoraRun certora/conf/${{ matrix.rule }} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} @@ -55,6 +52,8 @@ jobs: max-parallel: 16 matrix: rule: - - verifyGeneral.sh - - verifyDelegate.sh - - verifyCommunity.sh + - general.conf + - delegate.conf + - community.conf + - erc20.conf + diff --git a/certora/Makefile b/certora/Makefile index a4c6cec..ed01e55 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -14,8 +14,6 @@ help: munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) rm -rf $@ mkdir $@ - cp -r $(LIB_DIR) $@ - cp -r $(CONTRACTS_DIR) $@ patch -p0 -d $@ < $(PATCH) record: diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 3ae58b3..8174481 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,69 +1,7 @@ diff -ruN .gitignore .gitignore ---- .gitignore 1970-01-01 02:00:00 -+++ .gitignore 2023-03-29 13:05:55 +--- .gitignore 1970-01-01 02:00:00.000000000 +0200 ++++ .gitignore 2023-06-29 18:12:58.710152977 +0300 @@ -0,0 +1,2 @@ +* +!.gitignore \ No newline at end of file -diff -ruN src/AaveTokenV3.sol src/AaveTokenV3.sol ---- src/AaveTokenV3.sol 2023-03-29 13:12:02 -+++ src/AaveTokenV3.sol 2023-03-29 13:07:15 -@@ -215,7 +215,7 @@ - fromBalanceAfter = fromUserState.balance - uint104(amount); - } - _balances[from].balance = fromBalanceAfter; -- if (fromUserState.delegationState != DelegationState.NO_DELEGATION) { -+ if (fromUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) { - _governancePowerTransferByType( - fromUserState.balance, - fromBalanceAfter, -@@ -237,7 +237,7 @@ - toUserState.balance = toBalanceBefore + uint104(amount); - _balances[to] = toUserState; - -- if (toUserState.delegationState != DelegationState.NO_DELEGATION) { -+ if (toUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) { - _governancePowerTransferByType( - toBalanceBefore, - toUserState.balance, -@@ -293,7 +293,7 @@ - : address(0); - } - return -- userState.delegationState >= DelegationState.PROPOSITION_DELEGATED -+ userState.delegationState >= uint8(DelegationState.PROPOSITION_DELEGATED) - ? _propositionDelegateeV2[delegator] - : address(0); - } -@@ -330,16 +330,12 @@ - ) 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) -- ); -+ userState.delegationState = 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)) -- ); -+ userState.delegationState = userState.delegationState & -+ ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED)); - } - return userState; - } -diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol ---- src/BaseAaveToken.sol 2023-03-29 13:12:02 -+++ src/BaseAaveToken.sol 2023-03-29 13:07:15 -@@ -18,7 +18,7 @@ - uint104 balance; - uint72 delegatedPropositionBalance; - uint72 delegatedVotingBalance; -- DelegationState delegationState; -+ uint8 delegationState; // refactored from enum - } - - mapping(address => DelegationAwareBalance) internal _balances; diff --git a/certora/conf/community.conf b/certora/conf/community.conf new file mode 100644 index 0000000..fbe67d4 --- /dev/null +++ b/certora/conf/community.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness" + ], + "optimistic_loop": true, + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "cloud": "", + "process": "emv", + "solc": "solc8.13", + "verify": "AaveTokenV3Harness:certora/specs/community.spec", + "msg": "AaveTokenV3HarnessCommunity:community.spec " +} \ No newline at end of file diff --git a/certora/conf/delegate.conf b/certora/conf/delegate.conf new file mode 100644 index 0000000..f677073 --- /dev/null +++ b/certora/conf/delegate.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness" + ], + "cloud": "", + "optimistic_loop": true, + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "process": "emv", + "solc": "solc8.13", + "verify": "AaveTokenV3Harness:certora/specs/delegate.spec", + "msg": "AaveTokenV3Harness:delegate.spec " +} \ No newline at end of file diff --git a/certora/conf/erc20.conf b/certora/conf/erc20.conf new file mode 100644 index 0000000..706b639 --- /dev/null +++ b/certora/conf/erc20.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness" + ], + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "cloud": "", + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.13", + "verify": "AaveTokenV3Harness:certora/specs/erc20.spec", + "msg": "AaveTokenV3:erc20.spec " +} \ No newline at end of file diff --git a/certora/conf/general.conf b/certora/conf/general.conf new file mode 100644 index 0000000..9af48ba --- /dev/null +++ b/certora/conf/general.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness" + ], + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "cloud": "", + "optimistic_loop": true, + "process": "emv", + "prover_args": [" -smt_bitVectorTheory true"], + "solc": "solc8.13", + "verify": "AaveTokenV3Harness:certora/specs/general.spec", + "msg": "AaveTokenV3:general.spec " +} \ No newline at end of file diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol index c712ed3..8529d29 100644 --- a/certora/harness/AaveTokenV3Harness.sol +++ b/certora/harness/AaveTokenV3Harness.sol @@ -9,6 +9,7 @@ pragma solidity ^0.8.0; import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; +import {DelegationMode} from '../../src/DelegationAwareBalance.sol'; contract AaveTokenV3Harness is AaveTokenV3 { // returns user's token balance, used in some community rules @@ -29,15 +30,15 @@ contract AaveTokenV3Harness is AaveTokenV3 { //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; + _balances[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED || + _balances[user].delegationMode == DelegationMode.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; + _balances[user].delegationMode == DelegationMode.VOTING_DELEGATED || + _balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED; } // returns user's voting delegate @@ -51,7 +52,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { } // returns user's delegation state - function getDelegationState(address user) public view returns (DelegationMode) { - return _balances[user].delegationState; + function getDelegationMode(address user) public view returns (DelegationMode) { + return _balances[user].delegationMode; } } diff --git a/certora/harness/AaveTokenV3HarnessCommunity.sol b/certora/harness/AaveTokenV3HarnessCommunity.sol index aa3e8ad..318e0bc 100644 --- a/certora/harness/AaveTokenV3HarnessCommunity.sol +++ b/certora/harness/AaveTokenV3HarnessCommunity.sol @@ -9,6 +9,8 @@ pragma solidity ^0.8.0; import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; +import {DelegationMode} from '../../src/DelegationAwareBalance.sol'; +import {ECDSA} from 'openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol'; contract AaveTokenV3Harness is AaveTokenV3 { function getBalance(address user) public view returns (uint104) { @@ -25,14 +27,14 @@ contract AaveTokenV3Harness is AaveTokenV3 { function getDelegatingProposition(address user) public view returns (bool) { return - _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + _balances[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED || + _balances[user].delegationMode == DelegationMode.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; + _balances[user].delegationMode == DelegationMode.VOTING_DELEGATED || + _balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED; } function getVotingDelegate(address user) public view returns (address) { @@ -43,8 +45,8 @@ contract AaveTokenV3Harness is AaveTokenV3 { return _propositionDelegatee[user]; } - function getDelegationState(address user) public view returns (DelegationMode) { - return _balances[user].delegationState; + function getDelegationMode(address user) public view returns (DelegationMode) { + return _balances[user].delegationMode; } function getNonce(address user) public view returns (uint256) { @@ -66,12 +68,16 @@ contract AaveTokenV3Harness is AaveTokenV3 { uint256 deadline, uint256 nonce ) public view returns (bytes32) { - bytes32 digest = keccak256( - abi.encodePacked( - '\x19\x01', - DOMAIN_SEPARATOR, - keccak256(abi.encode(DELEGATE_TYPEHASH, delegator, delegatee, nonce, deadline)) - ) + //bytes32 digest = keccak256( + //abi.encodePacked( + //'\x19\x01', + // DOMAIN_SEPARATOR, + // keccak256(abi.encode(DELEGATE_TYPEHASH, delegator, delegatee, nonce, deadline)) + //) + //); + bytes32 digest = ECDSA.toTypedDataHash( + _getDomainSeparator(), + keccak256(abi.encode(DELEGATE_TYPEHASH, delegator, delegatee, nonce, deadline)) ); return digest; } @@ -83,22 +89,36 @@ contract AaveTokenV3Harness is AaveTokenV3 { uint256 deadline, uint256 nonce ) public view returns (bytes32) { - bytes32 digest = keccak256( - abi.encodePacked( - '\x19\x01', - DOMAIN_SEPARATOR, - keccak256( - abi.encode( - DELEGATE_BY_TYPE_TYPEHASH, - delegator, - delegatee, - delegationType, - nonce, - deadline - ) - ) - ) + // bytes32 digest = keccak256( + //abi.encodePacked( + // '\x19\x01', + // DOMAIN_SEPARATOR, + // keccak256( + // abi.encode( + // DELEGATE_BY_TYPE_TYPEHASH, + // delegator, + // delegatee, + // delegationType, + // nonce, + // deadline + // ) + //) + //) + //); + bytes32 digest = ECDSA.toTypedDataHash( + _getDomainSeparator(), + keccak256( + abi.encode( + DELEGATE_BY_TYPE_TYPEHASH, + delegator, + delegatee, + delegationType, + nonce, + deadline + ) + ) ); + return digest; } } diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol index f37631d..573749c 100644 --- a/certora/harness/AaveTokenV3HarnessStorage.sol +++ b/certora/harness/AaveTokenV3HarnessStorage.sol @@ -12,7 +12,8 @@ pragma solidity ^0.8.0; -import {AaveTokenV3} from '../munged/src/AaveTokenV3.sol'; +import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; +import {DelegationMode} from '../../src/DelegationAwareBalance.sol'; contract AaveTokenV3Harness is AaveTokenV3 { function getBalance(address user) public view returns (uint104) { @@ -28,17 +29,17 @@ contract AaveTokenV3Harness is AaveTokenV3 { } function getDelegatingProposition(address user) public view returns (bool) { - uint8 state = _balances[user].delegationState; + uint8 state = uint8(_balances[user].delegationMode); return - state == uint8(DelegationState.PROPOSITION_DELEGATED) || - state == uint8(DelegationState.FULL_POWER_DELEGATED); + state == uint8(DelegationMode.PROPOSITION_DELEGATED) || + state == uint8(DelegationMode.FULL_POWER_DELEGATED); } function getDelegatingVoting(address user) public view returns (bool) { - uint8 state = _balances[user].delegationState; + uint8 state = uint8(_balances[user].delegationMode); return - state == uint8(DelegationState.VOTING_DELEGATED) || - state == uint8(DelegationState.FULL_POWER_DELEGATED); + state == uint8(DelegationMode.VOTING_DELEGATED) || + state == uint8(DelegationMode.FULL_POWER_DELEGATED); } function getVotingDelegate(address user) public view returns (address) { @@ -49,7 +50,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { return _propositionDelegatee[user]; } - function getDelegationState(address user) public view returns (uint8) { - return _balances[user].delegationState; + function getDelegationMode(address user) public view returns (DelegationMode) { + return _balances[user].delegationMode; } } diff --git a/certora/scripts/erc20.sh b/certora/scripts/erc20.sh index 4b28024..a8b11f6 100644 --- a/certora/scripts/erc20.sh +++ b/certora/scripts/erc20.sh @@ -5,9 +5,11 @@ fi certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ --verify AaveTokenV3Harness:certora/specs/erc20.spec \ + --packages openzeppelin-contracts=lib/openzeppelin-contracts \ $RULE \ --solc solc8.13 \ --optimistic_loop \ + --send_only \ --cloud \ - --msg "AaveTokenV3:erc20.spec $1" + --msg "AaveTokenV3:erc20.spec $1" \ diff --git a/certora/scripts/verifyCommunity.sh b/certora/scripts/verifyCommunity.sh index 46947f9..8947b93 100644 --- a/certora/scripts/verifyCommunity.sh +++ b/certora/scripts/verifyCommunity.sh @@ -5,8 +5,10 @@ fi certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \ --verify AaveTokenV3Harness:certora/specs/community.spec \ + --packages openzeppelin-contracts=lib/openzeppelin-contracts \ $RULE \ --solc solc8.13 \ + --send_only \ --optimistic_loop \ --cloud \ --msg "AaveTokenV3HarnessCommunity:community.spec $1" diff --git a/certora/scripts/verifyDelegate.sh b/certora/scripts/verifyDelegate.sh index 527014c..c484e0a 100755 --- a/certora/scripts/verifyDelegate.sh +++ b/certora/scripts/verifyDelegate.sh @@ -5,8 +5,10 @@ fi certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ --verify AaveTokenV3Harness:certora/specs/delegate.spec \ + --packages openzeppelin-contracts=lib/openzeppelin-contracts \ $RULE \ --solc solc8.13 \ + --send_only \ --optimistic_loop \ --cloud \ --msg "AaveTokenV3Harness:delegate.spec $1" diff --git a/certora/scripts/verifyGeneral.sh b/certora/scripts/verifyGeneral.sh index 6655c1c..caa648c 100644 --- a/certora/scripts/verifyGeneral.sh +++ b/certora/scripts/verifyGeneral.sh @@ -5,10 +5,12 @@ fi certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \ --verify AaveTokenV3Harness:certora/specs/general.spec \ + --packages openzeppelin-contracts=lib/openzeppelin-contracts \ $RULE \ --solc solc8.13 \ --optimistic_loop \ - --settings -smt_bitVectorTheory=true \ + --send_only \ + --prover_args "-smt_bitVectorTheory true" \ --cloud \ --msg "AaveTokenV3:general.spec $1" diff --git a/certora/specs/base.spec b/certora/specs/base.spec index 9dd2e17..fb140fb 100644 --- a/certora/specs/base.spec +++ b/certora/specs/base.spec @@ -12,50 +12,50 @@ */ methods { - totalSupply() returns (uint256) envfree - balanceOf(address) returns (uint256) envfree - allowance(address,address) returns (uint256) envfree - increaseAllowance(address, uint256) - decreaseAllowance(address, uint256) - transfer(address,uint256) - transferFrom(address,address,uint256) - permit(address,address,uint256,uint256,uint8,bytes32,bytes32) - - delegate(address delegatee) - metaDelegate(address,address,uint256,uint8,bytes32,bytes32) - metaDelegateByType(address,address,uint8,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 - getDelegationState(address user) returns (uint8) envfree + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address,address) external returns (uint256) envfree; + function increaseAllowance(address, uint256) external; + function decreaseAllowance(address, uint256) external; + function transfer(address,uint256) external; + function transferFrom(address,address,uint256) external; + function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; + + function delegate(address delegatee) external; + function metaDelegate(address,address,uint256,uint8,bytes32,bytes32) external; + function metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32) external; + function getPowerCurrent(address, IGovernancePowerDelegationToken.GovernancePowerType) external returns (uint256) envfree; + + function getBalance(address user) external returns (uint104) envfree; + function getDelegatedPropositionBalance(address user) external returns (uint72) envfree; + function getDelegatedVotingBalance(address user) external returns (uint72) envfree; + function getDelegatingProposition(address user) external returns (bool) envfree; + function getDelegatingVoting(address user) external returns (bool) envfree; + function getVotingDelegate(address user) external returns (address) envfree; + function getPropositionDelegate(address user) external returns (address) envfree; + function getDelegationMode(address user) external returns (AaveTokenV3Harness.DelegationMode) envfree; } -definition VOTING_POWER() returns uint8 = 0; -definition PROPOSITION_POWER() returns uint8 = 1; +definition VOTING_POWER() returns IGovernancePowerDelegationToken.GovernancePowerType = IGovernancePowerDelegationToken.GovernancePowerType.VOTING; +definition PROPOSITION_POWER() returns IGovernancePowerDelegationToken.GovernancePowerType = IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION; definition DELEGATED_POWER_DIVIDER() returns uint256 = 10^10; /** - Definitions of delegation states + Definitions of delegation modes */ -definition NO_DELEGATION() returns uint8 = 0; -definition VOTING_DELEGATED() returns uint8 = 1; -definition PROPOSITION_DELEGATED() returns uint8 = 2; -definition FULL_POWER_DELEGATED() returns uint8 = 3; -definition DELEGATING_VOTING(uint8 state) returns bool = - state == VOTING_DELEGATED() || state == FULL_POWER_DELEGATED(); -definition DELEGATING_PROPOSITION(uint8 state) returns bool = - state == PROPOSITION_DELEGATED() || state == FULL_POWER_DELEGATED(); +definition NO_DELEGATION() returns AaveTokenV3Harness.DelegationMode = AaveTokenV3Harness.DelegationMode.NO_DELEGATION; +definition VOTING_DELEGATED() returns AaveTokenV3Harness.DelegationMode = AaveTokenV3Harness.DelegationMode.VOTING_DELEGATED; +definition PROPOSITION_DELEGATED() returns AaveTokenV3Harness.DelegationMode = AaveTokenV3Harness.DelegationMode.PROPOSITION_DELEGATED; +definition FULL_POWER_DELEGATED() returns AaveTokenV3Harness.DelegationMode = AaveTokenV3Harness.DelegationMode.FULL_POWER_DELEGATED; +definition DELEGATING_VOTING(AaveTokenV3Harness.DelegationMode mode) returns bool = + mode == VOTING_DELEGATED() || mode == FULL_POWER_DELEGATED(); +definition DELEGATING_PROPOSITION(AaveTokenV3Harness.DelegationMode mode) returns bool = + mode == PROPOSITION_DELEGATED() || mode == FULL_POWER_DELEGATED(); definition AAVE_MAX_SUPPLY() returns uint256 = 16000000 * 10^18; -definition SCALED_MAX_SUPPLY() returns uint256 = AAVE_MAX_SUPPLY() / DELEGATED_POWER_DIVIDER(); +definition SCALED_MAX_SUPPLY() returns mathint = AAVE_MAX_SUPPLY() / DELEGATED_POWER_DIVIDER(); /** @@ -64,12 +64,16 @@ definition SCALED_MAX_SUPPLY() returns uint256 = AAVE_MAX_SUPPLY() / DELEGATED_P */ -function normalize(uint256 amount) returns uint256 { - return to_uint256(amount / DELEGATED_POWER_DIVIDER() * DELEGATED_POWER_DIVIDER()); +function normalize(uint256 amount) returns mathint { + return amount / DELEGATED_POWER_DIVIDER() * DELEGATED_POWER_DIVIDER(); } -function validDelegationState(address user) returns bool { - return getDelegationState(user) < 4; +function validDelegationMode(address user) returns bool { + AaveTokenV3Harness.DelegationMode state = getDelegationMode(user); + return state == AaveTokenV3Harness.DelegationMode.NO_DELEGATION || + state == AaveTokenV3Harness.DelegationMode.VOTING_DELEGATED || + state == AaveTokenV3Harness.DelegationMode.PROPOSITION_DELEGATED || + state == AaveTokenV3Harness.DelegationMode.FULL_POWER_DELEGATED; } function validAmount(uint256 amt) returns bool { diff --git a/certora/specs/community.spec b/certora/specs/community.spec index 85e0432..bf21e9e 100644 --- a/certora/specs/community.spec +++ b/certora/specs/community.spec @@ -1,5 +1,5 @@ /* - This is a specification file for the verification of AaveTokenV3.sol + This is a specification file for the verification of AaveTokenV3.sol smart contract using the Certora prover. The rules in this spec have been contributed by the community. Individual attribution is given in the comments to each rule. @@ -13,14 +13,14 @@ */ -import "base.spec" +import "base.spec"; methods { - ecrecoverWrapper(bytes32 digest, uint8 v, bytes32 r, bytes32 s) returns (address) envfree - computeMetaDelegateHash(address delegator, address delegatee, uint256 deadline, uint256 nonce) returns (bytes32) envfree - computeMetaDelegateByTypeHash(address delegator, address delegatee, uint8 delegationType, uint256 deadline, uint256 nonce) returns (bytes32) envfree - _nonces(address addr) returns (uint256) envfree - getNonce(address addr) returns (uint256) envfree + function ecrecoverWrapper(bytes32, uint8, bytes32, bytes32) external returns (address) envfree; + function computeMetaDelegateHash(address delegator, address delegatee, uint256 deadline, uint256 nonce) external returns (bytes32) envfree; + function computeMetaDelegateByTypeHash(address delegator, address delegatee, IGovernancePowerDelegationToken.GovernancePowerType delegationType, uint256 deadline, uint256 nonce) external returns (bytes32) envfree; + function _nonces(address addr) external returns (uint256) envfree; + function getNonce(address) external returns (uint256) envfree; } definition ZERO_ADDRESS() returns address = 0; @@ -92,7 +92,7 @@ rule permitIntegrity() { @Link: */ invariant addressZeroNoPower() - getPowerCurrent(0, VOTING_POWER()) == 0 && getPowerCurrent(0, PROPOSITION_POWER()) == 0 && balanceOf(0) == 0 + getPowerCurrent(0, VOTING_POWER()) == 0 && getPowerCurrent(0, PROPOSITION_POWER()) == 0 && balanceOf(0) == 0; /* @@ -117,7 +117,7 @@ invariant addressZeroNoPower() @Link: */ -rule metaDelegateByTypeOnlyCallableWithProperlySignedArguments(env e, address delegator, address delegatee, uint8 delegationType, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { +rule metaDelegateByTypeOnlyCallableWithProperlySignedArguments(env e, address delegator, address delegatee, IGovernancePowerDelegationToken.GovernancePowerType delegationType, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { require ecrecoverWrapper(computeMetaDelegateByTypeHash(delegator, delegatee, delegationType, deadline, _nonces(delegator)), v, r, s) != delegator; metaDelegateByType@withrevert(e, delegator, delegatee, delegationType, deadline, v, r, s); assert lastReverted; @@ -151,7 +151,7 @@ rule metaDelegateByTypeOnlyCallableWithProperlySignedArguments(env e, address de rule metaDelegateNonRepeatable(env e1, env e2, address delegator, address delegatee, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { uint256 nonce = _nonces(delegator); bytes32 hash1 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce); - bytes32 hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce+1); + bytes32 hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, require_uint256(nonce+1)); // assume no hash collisions require hash1 != hash2; // assume first call is properly signed @@ -189,7 +189,7 @@ rule metaDelegateNonRepeatable(env e1, env e2, address delegator, address delega */ rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, address bob) { - require e.msg.sender != ZERO_ADDRESS(); + require e.msg.sender != ZERO_ADDRESS(); require e.msg.sender != alice && e.msg.sender != bob; require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS(); @@ -224,12 +224,12 @@ rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, a { powerAfter = getPowerCurrent(alice, type) powerAfter != powerBefore => - 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 || - f.selector == transfer(address, uint256).selector || - f.selector == transferFrom(address, address, uint256).selector + f.selector == sig:delegate(address).selector || + f.selector == sig:delegateByType(address, uint8).selector || + f.selector == sig:metaDelegate(address, address, uint256, uint8, bytes32, bytes32).selector || + f.selector == sig:metaDelegateByType(address, address, uint8, uint256, uint8, bytes32, bytes32).selector || + f.selector == sig:transfer(address, uint256).selector || + f.selector == sig:transferFrom(address, address, uint256).selector } @Note: @@ -242,8 +242,7 @@ rule powerChanges(address alice, method f) { env e; calldataarg args; - uint8 type; - require type <= 1; + IGovernancePowerDelegationToken.GovernancePowerType type; uint256 powerBefore = getPowerCurrent(alice, type); f(e, args); @@ -251,12 +250,12 @@ rule powerChanges(address alice, method f) { uint256 powerAfter = getPowerCurrent(alice, type); assert powerBefore != powerAfter => - 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 || - f.selector == transfer(address, uint256).selector || - f.selector == transferFrom(address, address, uint256).selector; + f.selector == sig:delegate(address).selector || + f.selector == sig:delegateByType(address, IGovernancePowerDelegationToken.GovernancePowerType).selector || + f.selector == sig:metaDelegate(address, address, uint256, uint8, bytes32, bytes32).selector || + f.selector == sig:metaDelegateByType(address, address, IGovernancePowerDelegationToken.GovernancePowerType, uint256, uint8, bytes32, bytes32).selector || + f.selector == sig:transfer(address, uint256).selector || + f.selector == sig:transferFrom(address, address, uint256).selector; } @@ -287,14 +286,14 @@ rule powerChanges(address alice, method f) { rule delegateIndependence(method f) { env e; - uint8 type; - require type <= 1; + IGovernancePowerDelegationToken.GovernancePowerType type; - address delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); + address delegateBefore = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); - delegateByType(e, _, 1 - type); + IGovernancePowerDelegationToken.GovernancePowerType otherType = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? IGovernancePowerDelegationToken.GovernancePowerType.VOTING : IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION; + delegateByType(e, _, otherType); - address delegateAfter = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); + address delegateAfter = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); assert delegateBefore == delegateAfter; } @@ -321,11 +320,11 @@ rule delegateIndependence(method f) { isVotingDelegatorAfter = getDelegatingVoting(a); isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0 - votingPowerBefore < votingPowerAfter <=> + votingPowerBefore < votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)) && - votingPowerBefore > votingPowerAfter <=> + votingPowerBefore > votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)) } @@ -355,12 +354,12 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { require !isVotingDelegateeBefore && !isVotingDelegateeAfter; - /* + /* If you're not a delegatee, your voting power only increases when 1. You're not delegating and your balance increases 2. You're delegating and stop delegating and your balanceBefore != 0 */ - assert votingPowerBefore < votingPowerAfter <=> + assert votingPowerBefore < votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)); @@ -369,7 +368,7 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { 1. You're not delegating and your balance decreases 2. You're not delegating and start delegating and your balanceBefore != 0 */ - assert votingPowerBefore > votingPowerAfter <=> + assert votingPowerBefore > votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)); } @@ -396,11 +395,11 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { isPropositionDelegatorAfter = getDelegatingProposition(a); isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0 - propositionPowerBefore < propositionPowerAfter <=> + propositionPowerBefore < propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)) && - propositionPowerBefore > propositionPowerAfter <=> + propositionPowerBefore > propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) || (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)) } @@ -435,16 +434,16 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) { 1. You're not delegating and your balance increases 2. You're delegating and stop delegating and your balanceBefore != 0 */ - assert propositionPowerBefore < propositionPowerAfter <=> + assert propositionPowerBefore < propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)); - + /* If you're not a delegatee, your proposition power only decreases when 1. You're not delegating and your balance decreases 2. You're not delegating and start delegating and your balanceBefore != 0 */ - assert propositionPowerBefore > propositionPowerAfter <=> + assert propositionPowerBefore > propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorBefore && (balanceBefore > balanceAfter)) || (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)); } @@ -463,11 +462,11 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) { f(e, args) > { - allowance(owner, spender) != allowanceBefore =>f.selector==approve(address,uint256).selector - || f.selector==increaseAllowance(address,uint256).selector - || f.selector==decreaseAllowance(address,uint256).selector - || f.selector==transferFrom(address,address,uint256).selector - || f.selector==permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector + allowance(owner, spender) != allowanceBefore =>f.selector==sig:approve(address,uint256).selector + || f.selector==sig:increaseAllowance(address,uint256).selector + || f.selector==sig:decreaseAllowance(address,uint256).selector + || f.selector==sig:transferFrom(address,address,uint256).selector + || f.selector==sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector } @@ -486,9 +485,9 @@ rule allowanceStateChange(env e){ f(e, args); uint256 allowanceAfter=allowance(owner,user); - assert allowanceBefore!=allowanceAfter => f.selector==approve(address,uint256).selector - || f.selector==increaseAllowance(address,uint256).selector - || f.selector==decreaseAllowance(address,uint256).selector - || f.selector==transferFrom(address,address,uint256).selector - || f.selector==permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; + assert allowanceBefore!=allowanceAfter => f.selector==sig:approve(address,uint256).selector + || f.selector==sig:increaseAllowance(address,uint256).selector + || f.selector==sig:decreaseAllowance(address,uint256).selector + || f.selector==sig:transferFrom(address,address,uint256).selector + || f.selector==sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; } diff --git a/certora/specs/delegate.spec b/certora/specs/delegate.spec index e5283c6..3f08934 100644 --- a/certora/specs/delegate.spec +++ b/certora/specs/delegate.spec @@ -11,7 +11,7 @@ */ -import "base.spec" +import "base.spec"; /* @@ -28,14 +28,14 @@ import "base.spec" */ rule powerWhenNotDelegating(address account) { - uint256 balance = balanceOf(account); + mathint balance = balanceOf(account); bool isDelegatingVoting = getDelegatingVoting(account); bool isDelegatingProposition = getDelegatingProposition(account); uint72 dvb = getDelegatedVotingBalance(account); uint72 dpb = getDelegatedPropositionBalance(account); - uint256 votingPower = getPowerCurrent(account, VOTING_POWER()); - uint256 propositionPower = getPowerCurrent(account, PROPOSITION_POWER()); + mathint votingPower = getPowerCurrent(account, VOTING_POWER()); + mathint propositionPower = getPowerCurrent(account, PROPOSITION_POWER()); assert dvb == 0 && !isDelegatingVoting => votingPower == balance; assert dpb == 0 && !isDelegatingProposition => propositionPower == balance; @@ -67,15 +67,15 @@ rule vpTransferWhenBothNotDelegating(address alice, address bob, address charlie // both accounts are not delegating require !isAliceDelegatingVoting && !isBobDelegatingVoting; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); assert alicePowerAfter == alicePowerBefore - amount; assert bobPowerAfter == bobPowerBefore + amount; @@ -102,15 +102,15 @@ rule ppTransferWhenBothNotDelegating(address alice, address bob, address charlie require !isAliceDelegatingProposition && !isBobDelegatingProposition; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); assert alicePowerAfter == alicePowerBefore - amount; assert bobPowerAfter == bobPowerBefore + amount; @@ -140,18 +140,18 @@ rule vpDelegateWhenBothNotDelegating(address alice, address bob, address charlie require !isAliceDelegatingVoting && !isBobDelegatingVoting; - uint256 aliceBalance = balanceOf(alice); - uint256 bobBalance = balanceOf(bob); + mathint aliceBalance = balanceOf(alice); + mathint bobBalance = balanceOf(bob); - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); delegate(e, bob); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); assert alicePowerAfter == alicePowerBefore - aliceBalance; assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER(); @@ -182,18 +182,18 @@ rule ppDelegateWhenBothNotDelegating(address alice, address bob, address charlie require !isAliceDelegatingProposition && !isBobDelegatingProposition; - uint256 aliceBalance = balanceOf(alice); - uint256 bobBalance = balanceOf(bob); + mathint aliceBalance = balanceOf(alice); + mathint bobBalance = balanceOf(bob); - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); delegate(e, bob); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); assert alicePowerAfter == alicePowerBefore - aliceBalance; assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER(); @@ -228,21 +228,21 @@ rule vpTransferWhenOnlyOneIsDelegating(address alice, address bob, address charl require isAliceDelegatingVoting && !isBobDelegatingVoting; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); // no delegation of anyone to Alice require alicePowerBefore == 0; - uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); uint256 aliceBalanceBefore = balanceOf(alice); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); uint256 aliceBalanceAfter = balanceOf(alice); assert alicePowerBefore == alicePowerAfter; @@ -275,21 +275,21 @@ rule ppTransferWhenOnlyOneIsDelegating(address alice, address bob, address charl require isAliceDelegatingProposition && !isBobDelegatingProposition; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); // no delegation of anyone to Alice require alicePowerBefore == 0; - uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); uint256 aliceBalanceBefore = balanceOf(alice); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); uint256 aliceBalanceAfter = balanceOf(alice); // still zero @@ -322,15 +322,15 @@ rule vpStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) { require isAliceDelegatingVoting && aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != charlie; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); delegate(e, 0); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); assert alicePowerAfter == alicePowerBefore + balanceOf(alice); assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); @@ -358,15 +358,15 @@ rule ppStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) { require isAliceDelegatingProposition && aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != charlie; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); delegate(e, 0); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); assert alicePowerAfter == alicePowerBefore + balanceOf(alice); assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); @@ -395,17 +395,17 @@ rule vpChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, a require isAliceDelegatingVoting; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); - uint256 delegate2PowerBefore = getPowerCurrent(delegate2, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint delegate2PowerBefore = getPowerCurrent(delegate2, VOTING_POWER()); delegate(e, delegate2); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); - uint256 delegate2PowerAfter = getPowerCurrent(delegate2, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint delegate2PowerAfter = getPowerCurrent(delegate2, VOTING_POWER()); address aliceDelegateAfter = getVotingDelegate(alice); assert alicePowerBefore == alicePowerAfter; @@ -437,17 +437,17 @@ rule ppChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, a require isAliceDelegatingVoting; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); - uint256 delegate2PowerBefore = getPowerCurrent(delegate2, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint delegate2PowerBefore = getPowerCurrent(delegate2, PROPOSITION_POWER()); delegate(e, delegate2); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); - uint256 delegate2PowerAfter = getPowerCurrent(delegate2, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint delegate2PowerAfter = getPowerCurrent(delegate2, PROPOSITION_POWER()); address aliceDelegateAfter = getPropositionDelegate(alice); assert alicePowerBefore == alicePowerAfter; @@ -479,19 +479,19 @@ rule vpOnlyAccount2IsDelegating(address alice, address bob, address charlie, uin require !isAliceDelegatingVoting && isBobDelegatingVoting; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); require bobPowerBefore == 0; - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); - uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER()); uint256 bobBalanceBefore = balanceOf(bob); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); - uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER()); uint256 bobBalanceAfter = balanceOf(bob); assert alicePowerAfter == alicePowerBefore - amount; @@ -523,19 +523,19 @@ rule ppOnlyAccount2IsDelegating(address alice, address bob, address charlie, uin require !isAliceDelegating && isBobDelegating; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); require bobPowerBefore == 0; - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); uint256 bobBalanceBefore = balanceOf(bob); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); uint256 bobBalanceAfter = balanceOf(bob); assert alicePowerAfter == alicePowerBefore - amount; @@ -570,21 +570,21 @@ rule vpTransferWhenBothAreDelegating(address alice, address bob, address charlie require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie; require aliceDelegate != bobDelegate; - uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); - uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER()); uint256 aliceBalanceBefore = balanceOf(alice); uint256 bobBalanceBefore = balanceOf(bob); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); - uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); + mathint bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER()); uint256 aliceBalanceAfter = balanceOf(alice); uint256 bobBalanceAfter = balanceOf(bob); @@ -593,8 +593,8 @@ rule vpTransferWhenBothAreDelegating(address alice, address bob, address charlie assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter); - uint256 normalizedBalanceBefore = normalize(bobBalanceBefore); - uint256 normalizedBalanceAfter = normalize(bobBalanceAfter); + mathint normalizedBalanceBefore = normalize(bobBalanceBefore); + mathint normalizedBalanceAfter = normalize(bobBalanceAfter); assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter; } @@ -622,21 +622,21 @@ rule ppTransferWhenBothAreDelegating(address alice, address bob, address charlie require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie; require aliceDelegate != bobDelegate; - uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); - uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); + mathint alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); uint256 aliceBalanceBefore = balanceOf(alice); uint256 bobBalanceBefore = balanceOf(bob); transferFrom(e, alice, bob, amount); - uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); - uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); - uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); - uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); - uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); + mathint alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + mathint bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER()); + mathint charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + mathint aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + mathint bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER()); uint256 aliceBalanceAfter = balanceOf(alice); uint256 bobBalanceAfter = balanceOf(bob); @@ -645,8 +645,8 @@ rule ppTransferWhenBothAreDelegating(address alice, address bob, address charlie assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter); - uint256 normalizedBalanceBefore = normalize(bobBalanceBefore); - uint256 normalizedBalanceAfter = normalize(bobBalanceAfter); + mathint normalizedBalanceBefore = normalize(bobBalanceBefore); + mathint normalizedBalanceAfter = normalize(bobBalanceAfter); assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter; } @@ -675,10 +675,10 @@ rule votingDelegateChanges(address alice, method f) { // only these four function may change the delegate of an address assert aliceVotingDelegateAfter != aliceVotingDelegateBefore || alicePropDelegateBefore != alicePropDelegateAfter => - 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; + f.selector == sig:delegate(address).selector || + f.selector == sig:delegateByType(address,IGovernancePowerDelegationToken.GovernancePowerType).selector || + f.selector == sig:metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == sig:metaDelegateByType(address,address,IGovernancePowerDelegationToken.GovernancePowerType,uint256,uint8,bytes32,bytes32).selector; } /* @@ -706,12 +706,12 @@ rule votingPowerChanges(address alice, method f) { // only these four function may change the power of an address assert aliceVotingPowerAfter != aliceVotingPowerBefore || alicePropPowerAfter != alicePropPowerBefore => - 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 || - f.selector == transfer(address,uint256).selector || - f.selector == transferFrom(address,address,uint256).selector; + f.selector == sig:delegate(address).selector || + f.selector == sig:delegateByType(address,IGovernancePowerDelegationToken.GovernancePowerType).selector || + f.selector == sig:metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == sig:metaDelegateByType(address,address,IGovernancePowerDelegationToken.GovernancePowerType,uint256,uint8,bytes32,bytes32).selector || + f.selector == sig:transfer(address,uint256).selector || + f.selector == sig:transferFrom(address,address,uint256).selector; } /* @@ -736,8 +736,8 @@ rule delegationTypeIndependence(address who, method f) filtered { f -> !f.isView address delegateeV_ = getVotingDelegate(who); address delegateeP_ = getPropositionDelegate(who); assert _delegateeV != delegateeV_ && _delegateeP != delegateeP_ => - (f.selector == delegate(address).selector || - f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector), + (f.selector == sig:delegate(address).selector || + f.selector == sig:metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector), "one delegatee type stays the same, unless delegate or delegateBySig was called"; } @@ -760,20 +760,20 @@ rule cantDelegateTwice(address _delegate) { require delegateBeforeV != _delegate && delegateBeforeV != e.msg.sender && delegateBeforeV != 0; require delegateBeforeP != _delegate && delegateBeforeP != e.msg.sender && delegateBeforeP != 0; require _delegate != e.msg.sender && _delegate != 0 && e.msg.sender != 0; - require getDelegationState(e.msg.sender) == FULL_POWER_DELEGATED(); + require getDelegationMode(e.msg.sender) == FULL_POWER_DELEGATED(); - uint256 votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER()); - uint256 propPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER()); + mathint votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER()); + mathint propPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER()); delegate(e, _delegate); - uint256 votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER()); - uint256 propPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER()); + mathint votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER()); + mathint propPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER()); delegate(e, _delegate); - uint256 votingPowerAfter2 = getPowerCurrent(_delegate, VOTING_POWER()); - uint256 propPowerAfter2 = getPowerCurrent(_delegate, PROPOSITION_POWER()); + mathint votingPowerAfter2 = getPowerCurrent(_delegate, VOTING_POWER()); + mathint propPowerAfter2 = getPowerCurrent(_delegate, PROPOSITION_POWER()); assert votingPowerAfter == votingPowerBefore + normalize(balanceOf(e.msg.sender)); assert propPowerAfter == propPowerBefore + normalize(balanceOf(e.msg.sender)); @@ -814,4 +814,4 @@ rule transferAndTransferFromPowerEquivalence(address bob, uint amount) { assert aliceVotingPowerAfterTransfer == aliceVotingPowerAfterTransferFrom && alicePropPowerAfterTransfer == alicePropPowerAfterTransferFrom; -} \ No newline at end of file +} diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec index f77eba9..b542438 100644 --- a/certora/specs/erc20.spec +++ b/certora/specs/erc20.spec @@ -9,11 +9,11 @@ Sanity run: https://prover.certora.com/output/67509/a5d16a31a49b9c9a7b71/?anonymousKey=bd108549122fd97450428a26c4ed52458793b898 */ -import "base.spec" +import "base.spec"; function doesntChangeBalance(method f) returns bool { - return f.selector != transfer(address,uint256).selector && - f.selector != transferFrom(address,address,uint256).selector; + return f.selector != sig:transfer(address,uint256).selector && + f.selector != sig:transferFrom(address,address,uint256).selector; } @@ -48,11 +48,11 @@ rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) { calldataarg args; require alice != bob; require allowance(alice, e.msg.sender) >= amount; - uint256 balanceBefore = balanceOf(bob); + mathint balanceBefore = balanceOf(bob); transferFrom(e, alice, bob, amount); - uint256 balanceAfter = balanceOf(bob); + mathint balanceAfter = balanceOf(bob); assert balanceAfter == balanceBefore + amount; } @@ -84,13 +84,13 @@ rule noFeeOnTransfer(address bob, uint256 amount) { env e; calldataarg args; require bob != e.msg.sender; - uint256 balanceSenderBefore = balanceOf(e.msg.sender); - uint256 balanceBefore = balanceOf(bob); + mathint balanceSenderBefore = balanceOf(e.msg.sender); + mathint balanceBefore = balanceOf(bob); transfer(e, bob, amount); - uint256 balanceAfter = balanceOf(bob); - uint256 balanceSenderAfter = balanceOf(e.msg.sender); + mathint balanceAfter = balanceOf(bob); + mathint balanceSenderAfter = balanceOf(e.msg.sender); assert balanceAfter == balanceBefore + amount; } @@ -150,10 +150,12 @@ rule transferCorrect(address to, uint256 amount) { require dvbFrom >= balanceOf(e.msg.sender) / DELEGATED_POWER_DIVIDER(); require pvbFrom >= balanceOf(e.msg.sender) / DELEGATED_POWER_DIVIDER(); - require validDelegationState(e.msg.sender) && validDelegationState(to); + require validDelegationMode(e.msg.sender) && validDelegationMode(to); require ! ( (getDelegatingVoting(to) && v_delegateTo == to) || (getDelegatingProposition(to) && p_delegateTo == to)); - + require validDelegationMode(p_delegateFrom) && validDelegationMode(p_delegateTo); + require validDelegationMode(v_delegateFrom) && validDelegationMode(v_delegateTo); + // to not overcomplicate the constraints on dvbTo and dvbFrom require v_delegateFrom != v_delegateTo && p_delegateFrom != p_delegateTo; @@ -163,8 +165,8 @@ rule transferCorrect(address to, uint256 amount) { if (e.msg.sender == to) { assert balanceOf(e.msg.sender) == fromBalanceBefore; } else { - assert balanceOf(e.msg.sender) == fromBalanceBefore - amount; - assert balanceOf(to) == toBalanceBefore + amount; + assert to_mathint(balanceOf(e.msg.sender)) == fromBalanceBefore - amount; + assert to_mathint(balanceOf(to)) == toBalanceBefore + amount; } } else { assert amount > fromBalanceBefore || to == 0; @@ -207,14 +209,14 @@ rule transferFromCorrect(address from, address to, uint256 amount) { uint256 fromBalanceBefore = balanceOf(from); uint256 toBalanceBefore = balanceOf(to); uint256 allowanceBefore = allowance(from, e.msg.sender); - require fromBalanceBefore + toBalanceBefore < AAVE_MAX_SUPPLY(); + require fromBalanceBefore + toBalanceBefore < to_mathint(AAVE_MAX_SUPPLY()); transferFrom(e, from, to, amount); assert from != to => - balanceOf(from) == fromBalanceBefore - amount && - balanceOf(to) == toBalanceBefore + amount && - (allowance(from, e.msg.sender) == allowanceBefore - amount || + to_mathint(balanceOf(from)) == fromBalanceBefore - amount && + to_mathint(balanceOf(to)) == toBalanceBefore + amount && + (to_mathint(allowance(from, e.msg.sender)) == allowanceBefore - amount || allowance(from, e.msg.sender) == max_uint256); } @@ -234,7 +236,7 @@ rule transferFromCorrect(address from, address to, uint256 amount) { */ invariant ZeroAddressNoBalance() - balanceOf(0) == 0 + balanceOf(0) == 0; /* @@ -261,7 +263,7 @@ invariant ZeroAddressNoBalance() */ rule NoChangeTotalSupply(method f) { - // require f.selector != burn(uint256).selector && f.selector != mint(address, uint256).selector; + // require f.selector != sig:burn(uint256).selector && f.selector != sig:mint(address, uint256).selector; uint256 totalSupplyBefore = totalSupply(); env e; calldataarg args; @@ -321,7 +323,7 @@ rule noMintingTokens(method f) { rule ChangingAllowance(method f, address from, address spender) { uint256 allowanceBefore = allowance(from, spender); env e; - if (f.selector == approve(address, uint256).selector) { + if (f.selector == sig:approve(address, uint256).selector) { address spender_; uint256 amount; approve(e, spender_, amount); @@ -330,34 +332,34 @@ rule ChangingAllowance(method f, address from, address spender) { } else { assert allowance(from, spender) == allowanceBefore; } - } else if (f.selector == transferFrom(address,address,uint256).selector) { + } else if (f.selector == sig:transferFrom(address,address,uint256).selector) { address from_; address to; - address amount; + uint256 amount; transferFrom(e, from_, to, amount); - uint256 allowanceAfter = allowance(from, spender); + mathint allowanceAfter = allowance(from, spender); if (from == from_ && spender == e.msg.sender) { assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount; } else { assert allowance(from, spender) == allowanceBefore; } - } else if (f.selector == decreaseAllowance(address, uint256).selector) { + } else if (f.selector == sig:decreaseAllowance(address, uint256).selector) { address spender_; uint256 amount; require amount <= allowanceBefore; decreaseAllowance(e, spender_, amount); if (from == e.msg.sender && spender == spender_) { - assert allowance(from, spender) == allowanceBefore - amount; + assert to_mathint(allowance(from, spender)) == allowanceBefore - amount; } else { assert allowance(from, spender) == allowanceBefore; } - } else if (f.selector == increaseAllowance(address, uint256).selector) { + } else if (f.selector == sig:increaseAllowance(address, uint256).selector) { address spender_; uint256 amount; require amount + allowanceBefore < max_uint256; increaseAllowance(e, spender_, amount); if (from == e.msg.sender && spender == spender_) { - assert allowance(from, spender) == allowanceBefore + amount; + assert to_mathint(allowance(from, spender)) == allowanceBefore + amount; } else { assert allowance(from, spender) == allowanceBefore; } @@ -367,7 +369,7 @@ rule ChangingAllowance(method f, address from, address spender) { calldataarg args; f(e, args); assert allowance(from, spender) == allowanceBefore || - f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; + f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; } } @@ -525,14 +527,14 @@ rule OtherBalanceOnlyGoesUp(address other, method f) { require other != currentContract; uint256 balanceBefore = balanceOf(other); - if (f.selector == transferFrom(address, address, uint256).selector) { + if (f.selector == sig:transferFrom(address, address, uint256).selector) { address from; address to; uint256 amount; require(other != from); require balanceOf(from) + balanceBefore < max_uint256; transferFrom(e, from, to, amount); - } else if (f.selector == transfer(address, uint256).selector) { + } else if (f.selector == sig:transfer(address, uint256).selector) { require other != e.msg.sender; require balanceOf(e.msg.sender) + balanceBefore < max_uint256; calldataarg args; diff --git a/certora/specs/general.spec b/certora/specs/general.spec index 45ec69f..2a5aecf 100644 --- a/certora/specs/general.spec +++ b/certora/specs/general.spec @@ -10,7 +10,7 @@ Sanity check results: https://prover.certora.com/output/67509/8cee7c95432ede6b3f9f/?anonymousKey=78d297585a2b2edc38f6c513e0ce12df10e47b82 */ -import "base.spec" +import "base.spec"; /** @@ -55,7 +55,7 @@ ghost mathint sumUndelegatedBalancesP { } // token balances of each address -ghost mapping(address => uint104) balances { +ghost mapping(address => mathint) balances { init_state axiom forall address a. balances[a] == 0; } @@ -73,7 +73,7 @@ ghost mapping(address => uint104) balances { and etc. */ -hook Sstore _balances[KEY address user].delegationState uint8 new_state (uint8 old_state) STORAGE { +hook Sstore _balances[KEY address user].delegationMode AaveTokenV3Harness.DelegationMode new_state (AaveTokenV3Harness.DelegationMode old_state) STORAGE { bool willDelegateP = !DELEGATING_PROPOSITION(old_state) && DELEGATING_PROPOSITION(new_state); bool wasDelegatingP = DELEGATING_PROPOSITION(old_state) && !DELEGATING_PROPOSITION(new_state); @@ -130,13 +130,6 @@ hook Sstore _balances[KEY address user].balance uint104 balance (uint104 old_bal } -// user's delegation state is always valid, i.e. one of the 4 legitimate states -// (NO_DELEGATION, VOTING_DELEGATED, PROPOSITION_DELEGATED, FULL_POWER_DELEGATED) -// passes -invariant delegationStateValid(address user) - validDelegationState(user) - - /* @Rule @@ -153,12 +146,7 @@ invariant delegationStateValid(address user) invariant delegateCorrectness(address user) ((getVotingDelegate(user) == user || getVotingDelegate(user) == 0) <=> !getDelegatingVoting(user)) && - ((getPropositionDelegate(user) == user || getPropositionDelegate(user) == 0) <=> !getDelegatingProposition(user)) - { - preserved { - requireInvariant delegationStateValid(user); - } - } + ((getPropositionDelegate(user) == user || getPropositionDelegate(user) == 0) <=> !getDelegatingProposition(user)); /* @Rule @@ -172,7 +160,7 @@ invariant delegateCorrectness(address user) @Link: */ -invariant sumOfVBalancesCorrectness() sumDelegatedBalancesV + sumUndelegatedBalancesV == totalSupply() +invariant sumOfVBalancesCorrectness() sumDelegatedBalancesV + sumUndelegatedBalancesV == to_mathint(totalSupply()); /* @Rule @@ -186,7 +174,7 @@ invariant sumOfVBalancesCorrectness() sumDelegatedBalancesV + sumUndelegatedBala @Link: */ -invariant sumOfPBalancesCorrectness() sumDelegatedBalancesP + sumUndelegatedBalancesP == totalSupply() +invariant sumOfPBalancesCorrectness() sumDelegatedBalancesP + sumUndelegatedBalancesP == to_mathint(totalSupply()); /* @Rule @@ -200,26 +188,26 @@ invariant sumOfPBalancesCorrectness() sumDelegatedBalancesP + sumUndelegatedBala @Link: */ -rule transferDoesntChangeDelegationState() { +rule transferDoesntChangeDelegationMode() { env e; address from; address to; address charlie; require (charlie != from && charlie != to); uint amount; - uint8 stateFromBefore = getDelegationState(from); - uint8 stateToBefore = getDelegationState(to); - uint8 stateCharlieBefore = getDelegationState(charlie); - require stateFromBefore <= FULL_POWER_DELEGATED() && stateToBefore <= FULL_POWER_DELEGATED(); + AaveTokenV3Harness.DelegationMode stateFromBefore = getDelegationMode(from); + AaveTokenV3Harness.DelegationMode stateToBefore = getDelegationMode(to); + AaveTokenV3Harness.DelegationMode stateCharlieBefore = getDelegationMode(charlie); + bool testFromBefore = isDelegatingVoting[from]; bool testToBefore = isDelegatingVoting[to]; transferFrom(e, from, to, amount); - uint8 stateFromAfter = getDelegationState(from); - uint8 stateToAfter = getDelegationState(to); + AaveTokenV3Harness.DelegationMode stateFromAfter = getDelegationMode(from); + AaveTokenV3Harness.DelegationMode stateToAfter = getDelegationMode(to); bool testFromAfter = isDelegatingVoting[from]; bool testToAfter = isDelegatingVoting[to]; assert testFromBefore == testFromAfter && testToBefore == testToAfter; - assert getDelegationState(charlie) == stateCharlieBefore; + assert getDelegationMode(charlie) == stateCharlieBefore; } diff --git a/src/BaseAaveToken.sol b/src/BaseAaveToken.sol index 4f4c3d3..e6df24a 100644 --- a/src/BaseAaveToken.sol +++ b/src/BaseAaveToken.sol @@ -126,7 +126,7 @@ abstract contract BaseAaveToken is Context, IERC20Metadata { _balances[from].balance = fromBalanceBefore - uint104(amount); } - _balances[to].balance += toBalanceBefore + uint104(amount); + _balances[to].balance = toBalanceBefore + uint104(amount); _afterTokenTransfer(from, to, fromBalanceBefore, toBalanceBefore, amount); }