diff --git a/.github/workflows/certora-erc20.yml b/.github/workflows/certora-erc20.yml new file mode 100644 index 0000000..664c381 --- /dev/null +++ b/.github/workflows/certora-erc20.yml @@ -0,0 +1,58 @@ +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 new file mode 100644 index 0000000..7dfd691 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,60 @@ +name: certora + +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: + - verifyGeneral.sh + - verifyDelegate.sh + - verifyCommunity.sh diff --git a/.gitignore b/.gitignore index 71f35f8..f0a2ae5 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,10 @@ out/ node_modules package-lock.json .env + +# Certora +.certora_config/ +.last_confs/ +.certora_* +certora/munged +resource_errors.json diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 0000000..e47c83b --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1,5 @@ +# certora +.certora* +.certora*.json +**.last_conf* +certora-logs diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 0000000..5e6e1bc --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,26 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../src +LIB_DIR = ../lib +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + cp -r $(CONTRACTS_DIR) $@ + cp -r $(LIB_DIR) $@ + patch -p0 -d $@ < $(PATCH) + +record: + diff -uN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+$(CONTRACTS_DIR)/++g' | sed 's+$(MUNGED_DIR)++g' > $(PATCH) + +clean: + git clean -fdX + touch $(PATCH) + diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..5891255 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,42 @@ +## Verification Overview +The current directory contains Certora's formal verification of AAVE's V3 token. +In this directory you will find three subdirectories: + +1. specs - Contains all the specification files that were written by Certora for the token code. We have created two spec files, `base.spec`, `delegate.spec`, `erc20.spec` and `general.spec`. +- `base.spec` contains method declarations, CVL functions and definitions used by the main specification files +- `delegate.spec` contains rules that prove various delegation properties +- `erc20.spec` contains rules that prove ERC20 general rules, e.g. correctness of transfer and others +- `general.spec` contains general delegation invariants, e.g. sum of delegated and undelegated balances equals to +total supply + +2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings. +- `verifyDelegate.sh` is a script for running `delegate.spec` +- `verifyGeneral.sh` is a script for running `general.spec` +- `erc20.sh` is a script for running `erc20.spec` + +3. harness - Contains all the inheriting contracts that add/simplify functionalities to the original contract. +We use two harnesses: +- `AaveTokenV3Harness.sol` used by `erc20.sh` and `delegate.sh`. It inherits from the original AaveV3Token +contract and adds a few getter functions. + +- `AaveTokenV3HarnessStorage.sol` used by `general.sh`. It uses a modified a version of AaveV3Token contract +where the `delegationState` field of the `_balances` struct is refactored to be of type uint8 instead of +`DelegationState` enum. This is done in order to bypass a current limitation of the tool and write a hook +on the `delegationState` field (hooks don't support enum fields at the moment) + + +
+ +--- + +## Running Instructions +To run a verification job: + +1. Open terminal and `cd` your way to the main aave-token-v3 directory + +2. Run the script you'd like to get results for: + ``` + sh certora/scripts/verifyDelegate.sh + sh certora/scripts/verifyGeneral.sh + sh certora/scripts/erc20.sh + ``` diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch new file mode 100644 index 0000000..b074b9f --- /dev/null +++ b/certora/applyHarness.patch @@ -0,0 +1,79 @@ +diff -uN AaveTokenV3.sol /AaveTokenV3.sol +--- AaveTokenV3.sol 2022-10-11 16:03:49.000000000 +0300 ++++ /AaveTokenV3.sol 2022-10-11 16:13:48.000000000 +0300 +@@ -210,7 +210,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, +@@ -232,7 +232,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, +@@ -288,7 +288,7 @@ + : address(0); + } + return +- userState.delegationState >= DelegationState.PROPOSITION_DELEGATED ++ userState.delegationState >= uint8(DelegationState.PROPOSITION_DELEGATED) + ? _propositionDelegateeV2[delegator] + : address(0); + } +@@ -325,16 +325,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 -uN BaseAaveToken.sol /BaseAaveToken.sol +--- BaseAaveToken.sol 2022-10-11 17:36:35.000000000 +0300 ++++ /BaseAaveToken.sol 2022-10-11 16:20:40.000000000 +0300 +@@ -1,9 +1,9 @@ + // 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'; ++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 { +@@ -18,7 +18,7 @@ + uint104 balance; + uint72 delegatedPropositionBalance; + uint72 delegatedVotingBalance; +- DelegationState delegationState; ++ uint8 delegationState; // refactored from enum + } + + mapping(address => DelegationAwareBalance) internal _balances; +Common subdirectories: interfaces and /interfaces +Common subdirectories: lib and /lib +Common subdirectories: test and /test +Common subdirectories: utils and /utils diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol new file mode 100644 index 0000000..d0e13c6 --- /dev/null +++ b/certora/harness/AaveTokenV3Harness.sol @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: MIT + +/** + + This is an extension of the AaveTokenV3 with added getters on the _balances fields + + */ + +pragma solidity ^0.8.0; + +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) { + return _balances[user].balance; + } + // returns user's delegated proposition balance + function getDelegatedPropositionBalance(address user) view public returns (uint72) { + return _balances[user].delegatedPropositionBalance; + } + + // returns user's delegated voting balance + function getDelegatedVotingBalance(address user) view public 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) { + return _votingDelegateeV2[user]; + } + + // returns user's proposition delegate + function getPropositionDelegate(address user) view public returns (address) { + return _propositionDelegateeV2[user]; + } + + // returns user's delegation state + function getDelegationState(address user) view public returns (DelegationState) { + return _balances[user].delegationState; + } +} \ No newline at end of file diff --git a/certora/harness/AaveTokenV3HarnessCommunity.sol b/certora/harness/AaveTokenV3HarnessCommunity.sol new file mode 100644 index 0000000..ace06bf --- /dev/null +++ b/certora/harness/AaveTokenV3HarnessCommunity.sol @@ -0,0 +1,106 @@ +// SPDX-License-Identifier: MIT + +/** + + 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"; + +contract AaveTokenV3Harness is AaveTokenV3 { + 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 getDelegationState(address user) view public returns (DelegationState) { + return _balances[user].delegationState; + } + + function getNonce(address user) view public returns (uint256) { + return _nonces[user]; + } + + function ecrecoverWrapper( + bytes32 hash, + uint8 v, + bytes32 r, + bytes32 s + ) public pure returns (address) { + return ecrecover(hash, v, r, s); + } + + function computeMetaDelegateHash( + address delegator, + address delegatee, + 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)) + ) + ); + return digest; + } + + function computeMetaDelegateByTypeHash( + address delegator, + address delegatee, + GovernancePowerType delegationType, + 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 + ) + ) + ) + ); + return digest; + } + +} \ No newline at end of file diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol new file mode 100644 index 0000000..4c77b29 --- /dev/null +++ b/certora/harness/AaveTokenV3HarnessStorage.sol @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: MIT + +/** + + 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 + + */ + +pragma solidity ^0.8.0; + +import {AaveTokenV3} from "../munged/AaveTokenV3.sol"; + +contract AaveTokenV3Harness is AaveTokenV3 { + 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) { + uint8 state = _balances[user].delegationState; + return state == uint8(DelegationState.PROPOSITION_DELEGATED) || + state == uint8(DelegationState.FULL_POWER_DELEGATED); + } + + + function getDelegatingVoting(address user) view public returns (bool) { + uint8 state = _balances[user].delegationState; + return state == uint8(DelegationState.VOTING_DELEGATED) || + state == uint8(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 getDelegationState(address user) view public returns (uint8) { + return _balances[user].delegationState; + } +} \ No newline at end of file diff --git a/certora/harness/README.md b/certora/harness/README.md new file mode 100644 index 0000000..e7d1aaa --- /dev/null +++ b/certora/harness/README.md @@ -0,0 +1,7 @@ +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 diff --git a/certora/report/Formal Verification Report of AAVE Token V3.md b/certora/report/Formal Verification Report of AAVE Token V3.md new file mode 100644 index 0000000..d96167c --- /dev/null +++ b/certora/report/Formal Verification Report of AAVE Token V3.md @@ -0,0 +1,924 @@ +![Certora logo](https://hackmd.io/_uploads/SkaW6ZXr9.png) + +# Formal Verification Report of AAVE Token V3 + +## Summary + +This document describes the specification and verification of AAVE Token V3 using the Certora Prover. The work was undertaken from July 15th to August 10th, 2022. The latest commit reviewed and run through the Certora Prover was [8bb9f896](https://github.com/bgd-labs/aave-token-v3/commit/8bb9f8966991f8225adbce2b5cd38b5ae3612ecd). + +The scope of this verification is AAVE token V3 code which includes the following contracts: + +* `AaveV3Token.sol` + + +And its parent contracts: + +* `BaseAaveToken.sol` +* `BaseAaveTokenV2.sol` + +This project has been a part of a joint Certora and Aave community program. Contributors from the community have conducted independent formal verification of the code, where Certora has provided an initial setup for writing a specification. + +19 out of the 25 community participants submitted spec files containing formal specifications resulting in 275 properties in total. Out of the 275 correctness rules, 240 quality rules passed our professional review and credited their authors with grants. + +Selected rules written by the community are included in this report in the [_Community_](#Community) section. + +Certora also performed a manual audit of these contracts. + +During this verification process, the Certora Prover discovered issues in the code which are listed in the tables below. + +All the rules and specification files are publicly available and can be found in [AAVE Token V3 repository](https://github.com/bgd-labs/aave-token-v3/tree/certora/certora). + +## List of Main Issues Discovered + +**Severity: **Low**** + +Discovered independently by the following contributors: +https://github.com/Elpacos +https://github.com/himanshu-Bhatt +https://github.com/jessicapointing +and Certora team. + +Discover + +| Issue: | Precision loss during voting power transfer | +| -------- | -------- | +| Description: | When calculating delegated balance on token transfer, the new delegated balance of a delegate was calculated with a small precision loss that violated the property $$delegatee1Power_{t1} = delegatee1Power_{t0} - z / 10^{10} * 10^{10}$$ after a delegator to delegatee1 transfers z amount of tokens. +|Property Violated: | vpTransferWhenOnlyOneIsDelegating (Property #6) and others | +| AAVE Response:| The issue was fixed in commit [a287d134](https://github.com/bgd-labs/aave-token-v3/commit/a287d134903618bed5671d411c66641bfd96002b) and the relevant property was modified to be $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance_{t0} / 10^{10} * 10^{10} + account1Balance_{t1} / 10^{10} * 10^{10}$$ + +## List of Issues Discovered Independently By The Community + +**Severity: **High**** + +Found by the following contributors: +https://github.com/Elpacos + +| Issue: | Wrong parameters order in a `_transferWithDelegation` call | +| -------- | -------- | +| Description: | This issue was present in an intermediary version of the code given to the community to verify, but not in the finalized version that Certora has verified. It was introduced for a short period of time during development, and immediately fixed by the AAVE team. +|Property Violated: | multiple properties | +| AAVE Response:| The issue was fixed in commit [190c03f4](https://github.com/bgd-labs/aave-token-v3/commit/190c03f43208ae85bfcbf7dcb4a0022bb34df169) + + + + + ## Disclaimer + +The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification. + +We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Certora or any of its employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here. + +# Summary of Formal Verification + +## Overview of the AAVE Token V3 + +`AaveV3Token.sol` is the main contract. It inherits from `BaseAaveToken.sol` and `BaseAaveTokenV2.sol`. + +The following description is taken from the token [repository](https://github.com/bgd-labs/aave-token-v3/blob/main/properties.md): + +AAVE is an ERC20 token deployed on Ethereum, which main utility is participating in the Aave governance system via voting on proposals or creating them. + +AAVE is a transparent proxy contract, and its current [implementation](https://etherscan.io/address/0xc13eac3b4f9eed480045113b7af00f7b5655ece8#code) is version 2. + +Together with all the standard ERC20 functionalities, the current implementation includes extra logic mainly for the management and accounting of voting and proposition power. Due to the design/architecture of the Aave governance v2 system, of which AAVE is the main voting asset, the current AAVE implementation makes the token transfers quite gas-consuming, as multiple snapshots of data (voting and proposition power) need to be stored all the time. + +With a new iteration of the Aave governance in the Aave/BGD roadmap down the line, snapshots on the token will not be required anymore for its integration with the governance system. So this new version 3 of AAVE consists mainly of removing the snapshotting, together with adding extra minor meta-transactions capabilities. + +## Assumptions and Simplifications Made During Verification + + + +The invariants in `general.spec` were proven on a slightly modified version of the token code. To bypass a current limitation of the Certora prover, we've refactored the `delegationState` field of the `_balances` struct to be a `uint8` instead of a `DelegationState` enum type. The `AaveV3Token.sol` code was modified to accomodate this change. + +These changes can be seen in the [patch file](https://github.com/bgd-labs/aave-token-v3/blob/certora/certora/applyHarness.patch) in the Certora branch of the token repository. + +To create this harness, we run `make munged` command from the `certora` directory (on the `certora` branch). + +- We unroll loops. Violations that require a loop to execute more than twice will not be detected. + +## Notations + +✔️ indicates the rule is formally verified on the latest reviewed commit. We write ✔️* when the rule was verified on the simplified assumptions described above in "Assumptions and Simplifications Made During Verification". + +❌ indicates the rule was violated under one of the tested versions of the code. + + +🔁 indicates the rule is timing out. + +Our tool uses Hoare triples of the form {p} C {q}, which means that if the execution of program C starts in any state satisfying p, it will end in a state satisfying q. This logical structure is reflected in the included formulae for many of the properties below. Note that p and q here can be thought of as analogous to `require` and `assert` in Solidity. + +The syntax {p} (C1 ～ C2) {q} is a generalization of Hoare rules, called relational properties. {p} is a requirement on the states before C1 and C2, and {q} describes the states after their executions. Notice that C1 and C2 result in different states. As a special case, C1 ～op C2, where op is a getter, indicating that C1 and C2 result in states with the same value for op. + +Our tool consists of a special struct type variable called environment, usually denoted by e. This complex type includes the various block data context accessible by solidity (e.g. block.timestamp, msg.sender, msg.value etc.) +These fields are accessible via the environment variable. + +## Community + +The following properties were written and verified by contributors from the Aave community + +1. **permitIntegrity** +Integrity of permit function - successful permit function increases the nonce of owner by 1 and also changes the allowance of owner to spender. +Contributed by https://github.com/parth-15 +``` + { + nonceBefore = getNonce(owner) + } + < + permit(owner, spender, value, deadline, v, r, s) + > + { + allowance(owner, spender) == value && getNonce(owner) == nonceBefore + 1 + } +``` +2. **addressZeroNoPower** +Address 0 has no voting or proposition power. +Contributed by https://github.com/JayP11 +``` +{ + getPowerCurrent(0, VOTING_POWER) == 0 && getPowerCurrent(0, PROPOSITION_POWER) == && balanceOf(0) == 0 +} +``` + +3. **metaDelegateByTypeOnlyCallableWithProperlySignedArguments** +Verify that `metaDelegateByType` can only be called with a signed request. +Contributed by https://github.com/kustosz +``` + { + ecrecover(v,r,s) != delegator + } + < + metaDelegateByType@withrevert(delegator, delegatee, delegationType, deadline, v, r, s) + > + { + lastReverted == true + } +``` +4. **metaDelegateNonRepeatable** +Verify that it's impossible to use the same arguments to call `metaDalegate` twice. +Contributed by https://github.com/kustosz +``` + { + hash1 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce) + hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce + 1) + ecrecover(hash1, v, r, s) == delegator + } + < + metaDelegate(e1, delegator, delegatee, v, r, s) + metaDelegate@withrevert(e2, delegator, delegatee, delegationType, deadline, v, r, s) + > + { + lastReverted == true + } +``` +5. **delegatingToAnotherUserRemovesPowerFromOldDelegatee** +Power of the previous delegate is removed when the delegatee delegates to another delegate. +Contributed by https://github.com/priyankabhanderi +``` + { + _votingBalance = getDelegatedVotingBalance(alice) + } + < + delegateByType(alice, VOTING_POWER) + delegateByType(bob, VOTING_POWER) + > + { + alice != bob => getDelegatedVotingBalance(alice) == _votingBalance + } +``` +6. **powerChanges** +Voting and proposition power change only as a result of specific functions. +Contributed by https://github.com/top-sekret +``` + { + powerBefore = getPowerCurrent(alice, type) + } + < + f(e, args) + > + { + 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 + } +``` +7. **delegateIndependence** +Changing a delegate of one type doesn't influence the delegate of the other type. +Written by https://github.com/top-sekret +``` + { + delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender) + } + < + delegateByType(e, delegatee, 1 - type) + > + { + delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender) + delegateBefore == delegateAfter + } +``` +8. **votingPowerChangesWhileNotBeingADelegatee** +Verify that voting power increases/decreases while not being a voting delegatee yourself. +Contributed by https://github.com/Zarfsec +``` + { + votingPowerBefore = getPowerCurrent(a, VOTING_POWER) + balanceBefore = balanceOf(a) + isVotingDelegatorBefore = getDelegatingVoting(a) + isVotingDelegateeBefore = getDelegatedVotingBalance(a) != 0 + } + < + f(e, args) + > + { + votingPowerAfter = getPowerCurrent(a, VOTING_POWER() + balanceAfter = getBalance(a) + isVotingDelegatorAfter = getDelegatingVoting(a); + isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0 + + votingPowerBefore < votingPowerAfter <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || + (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)) + && + votingPowerBefore > votingPowerAfter <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || + (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)) + } +``` + +9. **propositionPowerChangesWhileNotBeingADelegatee** +Verify that proposition power increases/decreases while not being a voting delegatee yourself. +Contributed by https://github.com/Zarfsec +``` + { + propositionPowerBefore = getPowerCurrent(a, PROPOSITION_POWER) + balanceBefore = balanceOf(a) + isPropositionDelegatorBefore = getDelegatingProposition(a) + isPropositionDelegateeBefore = getDelegatedPropositionBalance(a) != 0 + } + < + f(e, args) + > + { + propositionPowerAfter = getPowerCurrent(a, PROPOSITION_POWER() + balanceAfter = getBalance(a) + isPropositionDelegatorAfter = getDelegatingProposition(a); + isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0 + + propositionPowerBefore < propositionPowerAfter <=> + (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || + (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)) + && + propositionPowerBefore > propositionPowerAfter <=> + (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) || + (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)) + } +``` +10. **allowanceStateChange** +Allowance only changes as a result of specific subset of functions. +Contributed by https://github.com/oracleorb +``` + { + allowanceBefore = allowance(owner, spender) + } + < + 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 + + } +``` + + +## Formal Properties for AaveTokenV3 +The following properties were written and verified by Certora + +### Delegation Invariants + +1. **delegateCorrectness** ✔️ +User's delegation flag is switched on iff user is delegating to an address other than his own own or 0 +``` + { + (getVotingDelegate(account) == account || getVotingDelegate(account) == 0) <=> !getDelegatingVoting(account) + && + (getPropositionDelegate(account) == account || getPropositionDelegate(account) == 0) <=> !getDelegatingProposition(account) + } +``` + +2. **sumOfVBalancesCorrectness** ✔️ +Sum of delegated voting balances and undelegated voting balances is equal to total supply + +$$\sum balances[u'].delegatedVotingBalance * 10^{10} + \sum balanceOf(u) = totalSupply()$$ + +where getVotingDelegate(u) == 0 + +``` + { + sumDelegatedVotingBalances + sumUndelegatedVotingBalances == totalSupply() + } +``` +3. **sumOfPBalancesCorrectness** ✔️ +Sum of delegated proposition balances and undelegated proposition balances is equal to total supply. +$$\sum balances[u'].delegatedPropositionBalance * 10^{10} + \sum balanceOf(u) = totalSupply()$$ + +where getPropositionDelegate(u) == 0 +``` + { + sumDelegatedPropositionBalances + sumUndelegatedPropositionBalances == totalSupply() + } +``` + +### Delegation Properties + + +4. **powerWhenNotDelegating** ✔️ +If an account is not receiving delegation of power (one type) from anybody, +and that account is not delegating that power to anybody, the power of that account must be equal to its token balance. + +``` + { + dvb = _balances[account].delegatedVotingBalance + votingPower = getPowerCurrent(account, VOTING_POWER) + (dvb == 0 && !isDelegatingVoting(account)) => votingPower == balanceOf(account) + } +``` + +5. **vpTransferWhenBothNotDelegating** ✔️ +When both accounts are not delegating: +On transfer of z amount of tokens from account1 to account2, voting power holds the following properties: +$$account1Power_{t1} = account1Power_{t0} - z$$ $$account2Power_{t1} = account2Power_{t0} + z$$ + +``` + { + !isDelegatingVoting(account1) && !isDelegatingVoting(account2) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account2PowerBefore = getPowerCurrent(account2, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - z + getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + z + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` +6. **ppTransferWhenBothNotDelegating** ✔️ +When both account1 and account2 are not delegating: +On transfer of z amount of tokens from account1 to account2, proposition power holds the following properties: +$$account1Power_{t1} = account1Power_{t0} - z$$ $$account2Power_{t1} = account2Power_{t0} + z$$ + +``` + { + !isDelegatingProposition(account1) && !isDelegatingProposition(account2) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - z + getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + z + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` +7. **vpDelegateWhenBothNotDelegating** ✔️ +When both account1 and account2 are not delegating: +After account1 will delegate his voting power to account2 + + $$account1Power_{t1} = account1Power_{t0} - account1Balance$$ + + $$account2Power_{t1} = account2Power_{t0} + account1Balance / 10^{10} * 10^{10}$$ + + $$account1PowerDelegatee_{t1} = account2$$ +``` + { + account1 = e.msg.sender + !isDelegatingVoting(account1) && !isDelegatingVoting(account2) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account2PowerBefore = getPowerCurrent(account2, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + } + < + delegate(account2) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - balanceOf(account1) + getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` +8. **ppDelegateWhenBothNotDelegating**✔️ + +When both account1 and account2 are not delegating: +After account1 will delegate his proposition power to account2 + $$account1Power_{t1} = account1Power_{t0} - account1Balance$$ + + $$account2Power_{t1} = account2Power_{t0} + account1Balance / 10^{10} * 10^{10}$$ + + $$account1PowerDelegatee_{t1} = account2$$ +``` + { + account1 = e.msg.sender + !isDelegatingProposition(account1) && !isDelegatingProposition(account2) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + } + < + delegate(account2) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - balanceOf(account1) + getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` + +9. **vpTransferWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: +On transfer of z amount of tokens from account1 to account2 +$$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance_{t0} / 10^{10} * 10^{10} + account1Balance_{t1} / 10^{10} * 10^{10}$$ + + $$account2Power_{t1} = account2Power_{t0} + z$$ +``` + { + isDelegatingVoting(account1) && !isDelegatingVoting(account2) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account2PowerBefore = getPowerCurrent(account2, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER) + balanceAccount1Before = balanceOf(account1) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0 + getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + z + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` +10. **ppTransferWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating proposition power to delegatee1 and account2 is not delegating proposition power: +On transfer of z amount of tokens from account1 to account2 + $$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance_{t0} / 10^{10} * 10^{10} + account1Balance_{t1} / 10^{10} * 10^{10}$$ + + $$account2Power_{t1} = account2Power_{t0} + z$$ +``` + { + isDelegatingProposition(account1) && !isDelegatingProposition(account2) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER) + balanceAccount1Before = balanceOf(account1) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0 + getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + z + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` + +11. **vpStopDelegatingWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: +After account will stop delegating voting power to delegatee1 + $$account1Power_{t1} = account1Power_{t0} + account1Balance$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance / 10^{10} * 10^{10}$$ + +``` + { + account1 == msg.sender && isDelegatingVoting(account1) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account2PowerBefore = getPowerCurrent(account2, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER) + balanceAccount1Before = balanceOf(account1) + } + < + delegate(0) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore + balanceOfAccount1Before + getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` + +12. **ppStopDelegatingWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating proposition power to delegatee1 and account2 is not delegating proposition power: +After account will stop delegating proposition power to delegatee1 + $$account1Power_{t1} = account1Power_{t0} + account1Balance$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance / 10^{10} * 10^{10}$$ + +``` + { + account1 == msg.sender && isDelegatingProposition(account1) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER) + balanceAccount1Before = balanceOf(account1) + } + < + delegate(0) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore + balanceOfAccount1Before + getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` + +13. **vpChangeDelegateWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: +After account1 will delegate power to delegatee2 + + $$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance / 10^{10} * 10^{10}$$ + + $$delegatee2Power_{t1} = delegatee2Power_{t0} + account1Balance / 10^{10} * 10^{10}$$ + + $$account1PowerDelegatee_{t1} = delegatee2$$ +``` + { + account1 == msg.sender && isDelegatingVoting(account1) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER) + + } + < + delegate(delegatee2) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0 + getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` + +14. **ppChangeDelegateWhenOnlyOneIsDelegating** ✔️ +When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: +After account1 will delegate power to delegatee2 + + $$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance / 10^{10} * 10^{10}$$ + + $$delegatee2Power_{t1} = delegatee2Power_{t0} + account1Balance / 10^{10} * 10^{10}$$ + + $$account1PowerDelegatee_{t1} = delegatee2$$ + +``` + { + account1 == msg.sender && isDelegatingProposition(account1) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER) + + } + < + delegate(delegatee2) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0 + getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` + +15. **vpOnlyAccount2IsDelegating** ✔️ +Account1 not delegating voting power to anybody, account2 is delegating voting power to delegatee2: +On transfer of z tokens from account1 to account 2 + $$account1Power_{t1} = account1Power_{t0} - z$$ + + $$account2Power_{t1} = account2Power_{t0} = 0$$ + + $$delegatee2Power_{t1}=delegatee2Power_{t0} - account2Balance_{t0} / 10^{10} * 10^{10} + account2Balance_{t1} / 10^{10} * 10^{10}$$ + +``` + { + isDelegatingVoting(account1) && isDelegatingVoting(account2) + delegatee2 == getVotingDelegate(account2) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee2, VOTING_POWER) + account2BalanceBefore == balanceOf(account2) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - z + getPowerCurrent(account2, VOTING_POWER) == 0 + getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 *10^10 + balanceOf(account2) / 10^10 * 10^10 + getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore + } +``` + +16. **ppOnlyAccount2IsDelegating** ✔️ +Account1 not delegating proposition power to anybody, account2 is delegating proposition power to delegatee2: +On transfer of z tokens from account1 to account 2 + $$account1Power_{t1} = account1Power_{t0} - z$$ + + $$account2Power_{t1} = account2Power_{t0} = 0$$ + + $$delegatee2Power_{t1}=delegatee2Power_{t0} - account2Balance_{t0} / 10^{10} * 10^{10} + account2Balance_{t1} / 10^{10} * 10^{10}$$ + +``` + { + isDelegatingProposition(account1) && isDelegatingProposition(account2) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee2, PROPOSITION_POWER) + account2BalanceBefore == balanceOf(account2) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - z + getPowerCurrent(account2, PROPOSITION_POWER) == 0 + getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 *10^10 + balanceOf(account2) / 10^10 * 10^10 + getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore + } +``` + +17. **vpTransferWhenBothAreDelegating** ✔️ +Account1 is delegating voting power to delegatee1, account2 is delegating voting power to delegatee2: +On transfer of z tokens from account1 to account2 + $$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance_{t0} / 10^{10} * 10^{10} + account1Balance_{t1} / 10^{10} * 10^{10}$$ + + $$account2Power_{t1} = account2Power_{t0} = 0$$ + + $$delegatee2Power_{t1}=delegatee2Power_{t0} - account2Balance_{t0} / 10^{10} * 10^{10} + account2Balance_{t1} / 10^{10} * 10^{10}$$ + +``` + { + isDelegatingVoting(account1) && isDelegatingVoting(account2) + account1PowerBefore = getPowerCurrent(account1, VOTING_POWER) + account2PowerBefore = getPowerCurrent(account2, VOTING_POWER) + account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee2, VOTING_POWER) + account1BalanceBefore = balanceOf(account1) + account2BalanceBefore = balanceOf(account2) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0 + getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore == 0 + getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - account1BalanceBefore / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 * 10^10 + balanceOf(account2) / 10^10 * 10^10 + } +``` + +18. **ppTransferWhenBothAreDelegating** ✔️ +Account1 is delegating proposition power to delegatee1, account2 is delegating proposition power to delegatee2: +On transfer of z tokens from account1 to account2 + $$account1Power_{t1} = account1Power_{t0} = 0$$ + + $$delegatee1Power_{t1} = delegatee1Power_{t0} - account1Balance_{t0} / 10^{10} * 10^{10} + account1Balance_{t1} / 10^{10} * 10^{10}$$ + + $$account2Power_{t1} = account2Power_{t0} = 0$$ + + $$delegatee2Power_{t1}=delegatee2Power_{t0} - account2Balance_{t0} / 10^{10} * 10^{10} + account2Balance_{t1} / 10^{10} * 10^{10}$$ + +``` + { + isDelegatingProposition(account1) && isDelegatingProposition(account2) + account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER) + account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER) + account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) + delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER) + delegatee2PowerBefore = getPowerCurrent(delegatee2, PROPOSITION_POWER) + account1BalanceBefore = balanceOf(account1) + account2BalanceBefore = balanceOf(account2) + } + < + transferFrom(account1, account2, z) + > + { + getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0 + getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore == 0 + getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - account1BalanceBefore / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10 + getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 * 10^10 + balanceOf(account2) / 10^10 * 10^10 + } +``` + +19. **delegationTypeIndependence** ✔️ +Only delegate() and metaDelegate() may change both voting and +proposition delegates of an account at once. +``` + { + delegateVBefore = getVotingDelegate(account) + delegatePBefore = getPropositionDelegate(account) + } + < + f(e, args) + > + { + delegateVAfter = getVotingDelegate(account) + delegatePAfter = getPropositionDelegate(account) + (delegateVBefore == delegateVAfter || delegatePBefore == delegatePAfter) || (f.selector == delegate(address).selector || f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector) + } +``` + +20. **cantDelegateTwice** ✔️ +Delegating twice to the same delegate _delegate changes the delegate's voting power only once. + +``` + { + votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER) + propositionPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER) + } + < + delegate(_delegate) + votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER) + propositionPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER) + delegate(_delegate) + > + { + getPowerCurrent(_delegate, VOTING_POWER) == votingPowerAfter + getPowerCurrent(_delegate, PROPOSITION_POWER) == propositionPowerAfter + } +``` + +### ERC20 Properties + +21. **transferCorrect** ✔️ +Token transfer works correctly. Balances are updated if not reverted. +If reverted then the transfer amount was too high, or the recipient is 0. +``` + { + balanceFromBefore = balanceOf(msg.sender) + balanceToBefore = balanceOf(to) + } + < + transfer(to, amount) + > + { + lastReverted => to = 0 || amount > balanceOf(msg.sender) + !lastReverted => balanceOf(to) = balanceToBefore + amount && + balanceOf(msg.sender) = balanceFromBefore - amount + } +``` + +22. **transferFromCorrect** ✔️ +Token transferFrom function works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0, or the allowance was not sufficient +``` + { + balanceFromBefore = balanceOf(from) + balanceToBefore = balanceOf(to) + } + < + transferFrom(from, to, amount) + > + { + lastreverted => to = 0 || amount > balanceOf(from) + !lastreverted => balanceOf(to) = balanceToBefore + amount && + balanceOf(from) = balanceFromBefore - amount + } +``` + +23. **zeroAddressNoBalance** ✔️ +Balance of address 0 is always 0 +``` +{ balanceOf(0) = 0 } +``` + +24. **NoChangeTotalSupply** ✔️ +Contract calls don't change token total supply. +``` + { + supplyBefore = totalSupply() + } + < f(e, args)> + { + supplyAfter = totalSupply() + supplyBefore == supplyAfter + } +``` + +25. **ChangingAllowance** ✔️ +Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance +``` + { + allowanceBefore = allowance(from, spender) + } + < + f(e, args) + > + { + f.selector = approve(spender, amount) => allowance(from, spender) = amount + f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount + f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta + f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta + generic f.selector => allowance(from, spender) == allowanceBefore + } +``` + +26. **TransferSumOfFromAndToBalancesStaySame** ✔️ +Transfer from msg.sender to b doesn't change the sum of their balances +``` + { + balancesBefore = balanceOf(msg.sender) + balanceOf(b) + } + < + transfer(b, amount) + > + { + balancesBefore == balanceOf(msg.sender) + balanceOf(b) + } +``` + +27. **TransferFromSumOfFromAndToBalancesStaySame** ✔️ +transferFrom from a to b doesn't change the sum of their balances +``` + { + balancesBefore = balanceOf(a) + balanceOf(b) + } + < + transferFrom(a, b) + > + { + balancesBefore == balanceOf(a) + balanceOf(b) + } +``` + +28. **TransferDoesntChangeOtherBalance** ✔️ +Transfer from msg.sender to alice doesn't change the balance of other addresses +``` + { + balanceBefore = balanceOf(charlie) + } + < + transfer(alice, amount) + > + { + balanceOf(charlie) == balanceBefore + } +``` + +29. **TransferFromDoesntChangeOtherBalance** ✔️ +``` + { + balanceBefore = balanceOf(charlie) + } + < + transferFrom(alice, bob, amount) + > + { + balanceOf(charlie) = balanceBefore + } +``` + +30. **OtherBalanceOnlyGoesUp** ✔️ +Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls +``` + { + balanceBefore = balanceOf(charlie) + } + < + f(e, args) + > + { + f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore + } +``` + + diff --git a/certora/report/Formal Verification Report of AAVE Token V3.pdf b/certora/report/Formal Verification Report of AAVE Token V3.pdf new file mode 100644 index 0000000..556c81b Binary files /dev/null and b/certora/report/Formal Verification Report of AAVE Token V3.pdf differ diff --git a/certora/scripts/erc20.sh b/certora/scripts/erc20.sh new file mode 100644 index 0000000..29631e5 --- /dev/null +++ b/certora/scripts/erc20.sh @@ -0,0 +1,13 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ + --verify AaveTokenV3Harness:certora/specs/erc20.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --cloud \ + --msg "AaveTokenV3:erc20.spec $1" + \ No newline at end of file diff --git a/certora/scripts/verifyCommunity.sh b/certora/scripts/verifyCommunity.sh new file mode 100644 index 0000000..2925a2d --- /dev/null +++ b/certora/scripts/verifyCommunity.sh @@ -0,0 +1,14 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \ + --verify AaveTokenV3Harness:certora/specs/community.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --cloud \ + --msg "AaveTokenV3HarnessCommunity:community.spec $1" +# --sanity + \ No newline at end of file diff --git a/certora/scripts/verifyDelegate.sh b/certora/scripts/verifyDelegate.sh new file mode 100755 index 0000000..f0869cb --- /dev/null +++ b/certora/scripts/verifyDelegate.sh @@ -0,0 +1,14 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ + --verify AaveTokenV3Harness:certora/specs/delegate.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --cloud \ + --msg "AaveTokenV3Harness:delegate.spec $1" +# --sanity + \ No newline at end of file diff --git a/certora/scripts/verifyGeneral.sh b/certora/scripts/verifyGeneral.sh new file mode 100644 index 0000000..4bd1874 --- /dev/null +++ b/certora/scripts/verifyGeneral.sh @@ -0,0 +1,14 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \ + --verify AaveTokenV3Harness:certora/specs/general.spec \ + $RULE \ + --solc solc8.13 \ + --optimistic_loop \ + --settings -smt_bitVectorTheory=true \ + --cloud \ + --msg "AaveTokenV3:general.spec $1" + \ No newline at end of file diff --git a/certora/specs/base.spec b/certora/specs/base.spec new file mode 100644 index 0000000..9dd2e17 --- /dev/null +++ b/certora/specs/base.spec @@ -0,0 +1,77 @@ +/* + This is a base spec file that includes methods declarations, definitions + and functions to be included in other spec. There are no rules in this file. + For more information, visit: https://www.certora.com/ + +*/ + +/* + + Declaration of methods of the Aave token contract (and harness) + +*/ + +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 +} + +definition VOTING_POWER() returns uint8 = 0; +definition PROPOSITION_POWER() returns uint8 = 1; +definition DELEGATED_POWER_DIVIDER() returns uint256 = 10^10; + +/** + + Definitions of delegation states + +*/ +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 AAVE_MAX_SUPPLY() returns uint256 = 16000000 * 10^18; +definition SCALED_MAX_SUPPLY() returns uint256 = AAVE_MAX_SUPPLY() / DELEGATED_POWER_DIVIDER(); + + +/** + + Functions + +*/ + +function normalize(uint256 amount) returns uint256 { + return to_uint256(amount / DELEGATED_POWER_DIVIDER() * DELEGATED_POWER_DIVIDER()); +} + +function validDelegationState(address user) returns bool { + return getDelegationState(user) < 4; +} + +function validAmount(uint256 amt) returns bool { + return amt < AAVE_MAX_SUPPLY(); +} diff --git a/certora/specs/community.spec b/certora/specs/community.spec new file mode 100644 index 0000000..4145f67 --- /dev/null +++ b/certora/specs/community.spec @@ -0,0 +1,494 @@ +/* + 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. + + For more information, visit: https://www.certora.com/ + + This file is run with scripts/verifyCommunity.sh + On AaveTokenV3Harness.sol + + Run results: https://prover.certora.com/output/67509/d36b2357623beec546c1?anonymousKey=f6fb866df18e6bc9ed880806375e7861cde8274f + +*/ + +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 +} + +definition ZERO_ADDRESS() returns address = 0; + + +/* + @Rule + + @Description: + Integrity of permit function + Successful permit function increases the nonce of owner by 1 and also changes the allowance of owner to spender + + @Formula: + { + nonceBefore = getNonce(owner) + } + < + permit(owner, spender, value, deadline, v, r, s) + > + { + allowance(owner, spender) == value && getNonce(owner) == nonceBefore + 1 + } + + @Note: + Written by https://github.com/parth-15 + + @Link: +*/ +rule permitIntegrity() { + env e; + address owner; + address spender; + uint256 value; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + + uint256 allowanceBefore = allowance(owner, spender); + mathint nonceBefore = getNonce(owner); + + //checking this because function is using unchecked math and such a high nonce is unrealistic + require nonceBefore < max_uint; + + permit(e, owner, spender, value, deadline, v, r, s); + + uint256 allowanceAfter = allowance(owner, spender); + mathint nonceAfter = getNonce(owner); + + assert allowanceAfter == value, "permit increases allowance of owner to spender on success"; + assert nonceAfter == nonceBefore + 1, "successful call to permit function increases nonce of owner by 1"; +} + + +/* + @Rule + + @Description: + Address 0 has no voting or proposition power + + @Formula: + { + getPowerCurrent(0, VOTING_POWER) == 0 && getPowerCurrent(0, PROPOSITION_POWER) == && balanceOf(0) == 0 + } + + @Note: + Written by https://github.com/JayP11 + + @Link: +*/ +invariant addressZeroNoPower() + getPowerCurrent(0, VOTING_POWER()) == 0 && getPowerCurrent(0, PROPOSITION_POWER()) == 0 && balanceOf(0) == 0 + + +/* + @Rule + + @Description: + Verify that `metaDelegateByType` can only be called with a signed request. + + @Formula: + { + ecrecover(v,r,s) != delegator + } + < + metaDelegateByType@withrevert(delegator, delegatee, delegationType, deadline, v, r, s) + > + { + lastReverted == true + } + + @Note: + Written by https://github.com/kustosz + + @Link: +*/ +rule metaDelegateByTypeOnlyCallableWithProperlySignedArguments(env e, address delegator, address delegatee, uint8 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; +} + + /* + @Rule + + @Description: + Verify that it's impossible to use the same arguments to call `metaDalegate` twice. + + @Formula: + { + hash1 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce) + hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce + 1) + ecrecover(hash1, v, r, s) == delegator + } + < + metaDelegate(e1, delegator, delegatee, v, r, s) + metaDelegate@withrevert(e2, delegator, delegatee, delegationType, deadline, v, r, s) + > + { + lastReverted == true + } + + @Note: + Written by https://github.com/kustosz + + @Link: +*/ +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); + // assume no hash collisions + require hash1 != hash2; + // assume first call is properly signed + require ecrecoverWrapper(hash1, v, r, s) == delegator; + // assume ecrecover is sane: cannot sign two different messages with the same (v,r,s) + require ecrecoverWrapper(hash2, v, r, s) != ecrecoverWrapper(hash1, v, r, s); + metaDelegate(e1, delegator, delegatee, deadline, v, r, s); + metaDelegate@withrevert(e2, delegator, delegatee, deadline, v, r, s); + assert lastReverted; +} + + +/* + @Rule + + @Description: + Power of the previous delegate is removed when the delegatee delegates to another delegate + + @Formula: + { + _votingBalance = getDelegatedVotingBalance(alice) + } + < + delegateByType(alice, VOTING_POWER) + delegateByType(bob, VOTING_POWER) + > + { + alice != bob => getDelegatedVotingBalance(alice) == _votingBalance + } + + @Note: + Written by https://github.com/priyankabhanderi + + @Link: +*/ +rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, address bob) { + + require e.msg.sender != ZERO_ADDRESS(); + require e.msg.sender != alice && e.msg.sender != bob; + require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS(); + + require getVotingDelegate(e.msg.sender) != alice; + + uint72 _votingBalance = getDelegatedVotingBalance(alice); + + delegateByType(e, alice, VOTING_POWER()); + + assert getVotingDelegate(e.msg.sender) == alice; + + delegateByType(e, bob, VOTING_POWER()); + + assert getVotingDelegate(e.msg.sender) == bob; + uint72 votingBalance_ = getDelegatedVotingBalance(alice); + assert alice != bob => votingBalance_ == _votingBalance; +} + +/* + @Rule + + @Description: + Voting and proposition power change only as a result of specific functions + + @Formula: + { + powerBefore = getPowerCurrent(alice, type) + } + < + f(e, args) + > + { + 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 + } + + @Note: + Written by https://github.com/top-sekret + + @Link: +*/ + +rule powerChanges(address alice, method f) { + env e; + calldataarg args; + + uint8 type; + require type <= 1; + uint256 powerBefore = getPowerCurrent(alice, type); + + f(e, args); + + 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; +} + + + +/* + @Rule + + @Description: + Changing a delegate of one type doesn't influence the delegate of the other type + + @Formula: + { + delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender) + } + < + delegateByType(e, delegatee, 1 - type) + > + { + delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender) + delegateBefore == delegateAfter + } + + @Note: + Written by https://github.com/top-sekret + + @Link: +*/ +rule delegateIndependence(method f) { + env e; + + uint8 type; + require type <= 1; + + address delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); + + delegateByType(e, _, 1 - type); + + address delegateAfter = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender); + + assert delegateBefore == delegateAfter; +} + +/* + @Rule + + @Description: + Verifying voting power increases/decreases while not being a voting delegatee yourself + + @Formula: + { + votingPowerBefore = getPowerCurrent(a, VOTING_POWER) + balanceBefore = balanceOf(a) + isVotingDelegatorBefore = getDelegatingVoting(a) + isVotingDelegateeBefore = getDelegatedVotingBalance(a) != 0 + } + < + f(e, args) + > + { + votingPowerAfter = getPowerCurrent(a, VOTING_POWER() + balanceAfter = getBalance(a) + isVotingDelegatorAfter = getDelegatingVoting(a); + isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0 + + votingPowerBefore < votingPowerAfter <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || + (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)) + && + votingPowerBefore > votingPowerAfter <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || + (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)) + } + + @Note: + Written by https://github.com/Zarfsec + + @Link: +*/ +rule votingPowerChangesWhileNotBeingADelegatee(address a) { + require a != 0; + + uint256 votingPowerBefore = getPowerCurrent(a, VOTING_POWER()); + uint256 balanceBefore = getBalance(a); + bool isVotingDelegatorBefore = getDelegatingVoting(a); + bool isVotingDelegateeBefore = getDelegatedVotingBalance(a) != 0; + + method f; + env e; + calldataarg args; + f(e, args); + + uint256 votingPowerAfter = getPowerCurrent(a, VOTING_POWER()); + uint256 balanceAfter = getBalance(a); + bool isVotingDelegatorAfter = getDelegatingVoting(a); + bool isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0; + + 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 <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || + (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)); + + /* + If you're not a delegatee, your voting 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 votingPowerBefore > votingPowerAfter <=> + (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || + (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)); +} + +/* + @Rule + + @Description: + Verifying proposition power increases/decreases while not being a proposition delegatee yourself + + @Formula: + { + propositionPowerBefore = getPowerCurrent(a, PROPOSITION_POWER) + balanceBefore = balanceOf(a) + isPropositionDelegatorBefore = getDelegatingProposition(a) + isPropositionDelegateeBefore = getDelegatedPropositionBalance(a) != 0 + } + < + f(e, args) + > + { + propositionPowerAfter = getPowerCurrent(a, PROPOSITION_POWER() + balanceAfter = getBalance(a) + isPropositionDelegatorAfter = getDelegatingProposition(a); + isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0 + + propositionPowerBefore < propositionPowerAfter <=> + (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || + (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)) + && + propositionPowerBefore > propositionPowerAfter <=> + (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) || + (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)) + } + + @Note: + Written by https://github.com/Zarfsec + + @Link: +*/ +rule propositionPowerChangesWhileNotBeingADelegatee(address a) { + require a != 0; + + uint256 propositionPowerBefore = getPowerCurrent(a, PROPOSITION_POWER()); + uint256 balanceBefore = getBalance(a); + bool isPropositionDelegatorBefore = getDelegatingProposition(a); + bool isPropositionDelegateeBefore = getDelegatedPropositionBalance(a) != 0; + + method f; + env e; + calldataarg args; + f(e, args); + + uint256 propositionPowerAfter = getPowerCurrent(a, PROPOSITION_POWER()); + uint256 balanceAfter = getBalance(a); + bool isPropositionDelegatorAfter = getDelegatingProposition(a); + bool isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0; + + require !isPropositionDelegateeBefore && !isPropositionDelegateeAfter; + + /* + If you're not a delegatee, your proposition 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 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 <=> + (!isPropositionDelegatorBefore && !isPropositionDelegatorBefore && (balanceBefore > balanceAfter)) || + (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)); +} + +/* + @Rule + + @Description: + Allowance only changes as a result of specific subset of functions + + @Formula: + { + allowanceBefore = allowance(owner, spender) + } + < + 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 + + } + + @Note: + Written by https://github.com/oracleorb + + @Link: +*/ +rule allowanceStateChange(env e){ + address owner; + address user; + method f; + calldataarg args; + + uint256 allowanceBefore=allowance(owner,user); + 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; +} diff --git a/certora/specs/delegate.spec b/certora/specs/delegate.spec new file mode 100644 index 0000000..e5283c6 --- /dev/null +++ b/certora/specs/delegate.spec @@ -0,0 +1,817 @@ + +/* + This is a specification file for the verification of delegation + features of AaveTokenV3.sol smart contract using the Certora prover. + For more information, visit: https://www.certora.com/ + + This file is run with scripts/verifyDelegate.sh + On AaveTokenV3Harness.sol + + Sanity check results: https://prover.certora.com/output/67509/021f59de6995d82ecf18/?anonymousKey=84f18dc61532a37fabfd59655fe7fe43989f1a8e + +*/ + +import "base.spec" + + +/* + @Rule + + @Description: + If an account is not receiving delegation of power (one type) from anybody, + and that account is not delegating that power to anybody, the power of that account + must be equal to its token balance. + + @Note: + + @Link: +*/ + +rule powerWhenNotDelegating(address account) { + uint256 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()); + + assert dvb == 0 && !isDelegatingVoting => votingPower == balance; + assert dpb == 0 && !isDelegatingProposition => propositionPower == balance; +} + + +/** + Account1 and account2 are not delegating power +*/ + +/* + @Rule + + @Description: + Verify correct voting power on token transfers, when both accounts are not delegating + + @Note: + + @Link: +*/ + +rule vpTransferWhenBothNotDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + bool isBobDelegatingVoting = getDelegatingVoting(bob); + + // 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()); + + transferFrom(e, alice, bob, amount); + + uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER()); + uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + + assert alicePowerAfter == alicePowerBefore - amount; + assert bobPowerAfter == bobPowerBefore + amount; + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct proposition power on token transfers, when both accounts are not delegating + + @Note: + + @Link: +*/ + +rule ppTransferWhenBothNotDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingProposition = getDelegatingProposition(alice); + bool isBobDelegatingProposition = getDelegatingProposition(bob); + + require !isAliceDelegatingProposition && !isBobDelegatingProposition; + + uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + uint256 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()); + + assert alicePowerAfter == alicePowerBefore - amount; + assert bobPowerAfter == bobPowerBefore + amount; + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct voting power after Alice delegates to Bob, when + both accounts were not delegating + + @Note: + + @Link: +*/ + +rule vpDelegateWhenBothNotDelegating(address alice, address bob, address charlie) { + env e; + require alice == e.msg.sender; + require alice != 0 && bob != 0 && charlie != 0; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + bool isBobDelegatingVoting = getDelegatingVoting(bob); + + require !isAliceDelegatingVoting && !isBobDelegatingVoting; + + uint256 aliceBalance = balanceOf(alice); + uint256 bobBalance = balanceOf(bob); + + uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + uint256 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()); + + assert alicePowerAfter == alicePowerBefore - aliceBalance; + assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER(); + assert getVotingDelegate(alice) == bob; + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct proposition power after Alice delegates to Bob, when + both accounts were not delegating + + @Note: + + @Link: +*/ + +rule ppDelegateWhenBothNotDelegating(address alice, address bob, address charlie) { + env e; + require alice == e.msg.sender; + require alice != 0 && bob != 0 && charlie != 0; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingProposition = getDelegatingProposition(alice); + bool isBobDelegatingProposition = getDelegatingProposition(bob); + + require !isAliceDelegatingProposition && !isBobDelegatingProposition; + + uint256 aliceBalance = balanceOf(alice); + uint256 bobBalance = balanceOf(bob); + + uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + uint256 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()); + + assert alicePowerAfter == alicePowerBefore - aliceBalance; + assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER(); + assert getPropositionDelegate(alice) == bob; + assert charliePowerAfter == charliePowerBefore; +} + +/** + Account1 is delegating power to delegatee1, account2 is not delegating power to anybody +*/ + +/* + @Rule + + @Description: + Verify correct voting power after a token transfer from Alice to Bob, when + Alice was delegating and Bob wasn't + + @Note: + + @Link: +*/ + +rule vpTransferWhenOnlyOneIsDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + bool isBobDelegatingVoting = getDelegatingVoting(bob); + address aliceDelegate = getVotingDelegate(alice); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie; + + require isAliceDelegatingVoting && !isBobDelegatingVoting; + + uint256 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()); + 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()); + uint256 aliceBalanceAfter = balanceOf(alice); + + assert alicePowerBefore == alicePowerAfter; + assert aliceDelegatePowerAfter == + aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter); + assert bobPowerAfter == bobPowerBefore + amount; + assert charliePowerBefore == charliePowerAfter; +} + +/* + @Rule + + @Description: + Verify correct proposition power after a token transfer from Alice to Bob, when + Alice was delegating and Bob wasn't + + @Note: + + @Link: +*/ + +rule ppTransferWhenOnlyOneIsDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingProposition = getDelegatingProposition(alice); + bool isBobDelegatingProposition = getDelegatingProposition(bob); + address aliceDelegate = getPropositionDelegate(alice); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie; + + require isAliceDelegatingProposition && !isBobDelegatingProposition; + + uint256 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()); + 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()); + uint256 aliceBalanceAfter = balanceOf(alice); + + // still zero + assert alicePowerBefore == alicePowerAfter; + assert aliceDelegatePowerAfter == + aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter); + assert bobPowerAfter == bobPowerBefore + amount; + assert charliePowerBefore == charliePowerAfter; +} + + +/* + @Rule + + @Description: + Verify correct voting power after Alice stops delegating, when + Alice was delegating and Bob wasn't + + @Note: + + @Link: +*/ +rule vpStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) { + env e; + require alice != charlie; + require alice == e.msg.sender; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + address aliceDelegate = getVotingDelegate(alice); + + 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()); + + delegate(e, 0); + + uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER()); + uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER()); + uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER()); + + assert alicePowerAfter == alicePowerBefore + balanceOf(alice); + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct proposition power after Alice stops delegating, when + Alice was delegating and Bob wasn't + + @Note: + + @Link: +*/ +rule ppStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) { + env e; + require alice != charlie; + require alice == e.msg.sender; + + bool isAliceDelegatingProposition = getDelegatingProposition(alice); + address aliceDelegate = getPropositionDelegate(alice); + + 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()); + + delegate(e, 0); + + uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER()); + uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER()); + + assert alicePowerAfter == alicePowerBefore + balanceOf(alice); + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct voting power after Alice delegates + + @Note: + + @Link: +*/ +rule vpChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, address charlie) { + env e; + require alice != charlie && alice != delegate2 && charlie != delegate2; + require alice == e.msg.sender; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + address aliceDelegate = getVotingDelegate(alice); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != delegate2 && + delegate2 != 0 && delegate2 != charlie && aliceDelegate != charlie; + + 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()); + + 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()); + address aliceDelegateAfter = getVotingDelegate(alice); + + assert alicePowerBefore == alicePowerAfter; + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); + assert delegate2PowerAfter == delegate2PowerBefore + normalize(balanceOf(alice)); + assert aliceDelegateAfter == delegate2; + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct proposition power after Alice delegates + + @Note: + + @Link: +*/ +rule ppChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, address charlie) { + env e; + require alice != charlie && alice != delegate2 && charlie != delegate2; + require alice == e.msg.sender; + + bool isAliceDelegatingVoting = getDelegatingProposition(alice); + address aliceDelegate = getPropositionDelegate(alice); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != delegate2 && + delegate2 != 0 && delegate2 != charlie && aliceDelegate != charlie; + + 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()); + + 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()); + address aliceDelegateAfter = getPropositionDelegate(alice); + + assert alicePowerBefore == alicePowerAfter; + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice)); + assert delegate2PowerAfter == delegate2PowerBefore + normalize(balanceOf(alice)); + assert aliceDelegateAfter == delegate2; + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct voting power after Alice transfers to Bob, when only Bob was delegating + + @Note: + + @Link: +*/ + +rule vpOnlyAccount2IsDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + bool isBobDelegatingVoting = getDelegatingVoting(bob); + address bobDelegate = getVotingDelegate(bob); + require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie; + + require !isAliceDelegatingVoting && isBobDelegatingVoting; + + uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER()); + uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER()); + require bobPowerBefore == 0; + uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER()); + uint256 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()); + uint256 bobBalanceAfter = balanceOf(bob); + + assert alicePowerAfter == alicePowerBefore - amount; + assert bobPowerAfter == 0; + assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalize(bobBalanceBefore) + normalize(bobBalanceAfter); + + assert charliePowerAfter == charliePowerBefore; +} + +/* + @Rule + + @Description: + Verify correct proposition power after Alice transfers to Bob, when only Bob was delegating + + @Note: + + @Link: +*/ + +rule ppOnlyAccount2IsDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegating = getDelegatingProposition(alice); + bool isBobDelegating = getDelegatingProposition(bob); + address bobDelegate = getPropositionDelegate(bob); + require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie; + + require !isAliceDelegating && isBobDelegating; + + uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER()); + require bobPowerBefore == 0; + uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER()); + uint256 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()); + uint256 bobBalanceAfter = balanceOf(bob); + + assert alicePowerAfter == alicePowerBefore - amount; + assert bobPowerAfter == 0; + assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalize(bobBalanceBefore) + normalize(bobBalanceAfter); + + assert charliePowerAfter == charliePowerBefore; +} + + +/* + @Rule + + @Description: + Verify correct voting power after Alice transfers to Bob, when both Alice + and Bob were delegating + + @Note: + + @Link: +*/ +rule vpTransferWhenBothAreDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegatingVoting = getDelegatingVoting(alice); + bool isBobDelegatingVoting = getDelegatingVoting(bob); + require isAliceDelegatingVoting && isBobDelegatingVoting; + address aliceDelegate = getVotingDelegate(alice); + address bobDelegate = getVotingDelegate(bob); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != 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()); + 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()); + uint256 aliceBalanceAfter = balanceOf(alice); + uint256 bobBalanceAfter = balanceOf(bob); + + assert alicePowerAfter == alicePowerBefore; + assert bobPowerAfter == bobPowerBefore; + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + + normalize(aliceBalanceAfter); + + uint256 normalizedBalanceBefore = normalize(bobBalanceBefore); + uint256 normalizedBalanceAfter = normalize(bobBalanceAfter); + assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter; +} + +/* + @Rule + + @Description: + Verify correct proposition power after Alice transfers to Bob, when both Alice + and Bob were delegating + + @Note: + + @Link: +*/ +rule ppTransferWhenBothAreDelegating(address alice, address bob, address charlie, uint256 amount) { + env e; + require alice != bob && bob != charlie && alice != charlie; + + bool isAliceDelegating = getDelegatingProposition(alice); + bool isBobDelegating = getDelegatingProposition(bob); + require isAliceDelegating && isBobDelegating; + address aliceDelegate = getPropositionDelegate(alice); + address bobDelegate = getPropositionDelegate(bob); + require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != 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()); + 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()); + uint256 aliceBalanceAfter = balanceOf(alice); + uint256 bobBalanceAfter = balanceOf(bob); + + assert alicePowerAfter == alicePowerBefore; + assert bobPowerAfter == bobPowerBefore; + assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + + normalize(aliceBalanceAfter); + + uint256 normalizedBalanceBefore = normalize(bobBalanceBefore); + uint256 normalizedBalanceAfter = normalize(bobBalanceAfter); + assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter; +} + +/* + @Rule + + @Description: + Verify that an account's delegate changes only as a result of a call to + the delegation functions + + @Note: + + @Link: +*/ +rule votingDelegateChanges(address alice, method f) { + env e; + calldataarg args; + + address aliceVotingDelegateBefore = getVotingDelegate(alice); + address alicePropDelegateBefore = getPropositionDelegate(alice); + + f(e, args); + + address aliceVotingDelegateAfter = getVotingDelegate(alice); + address alicePropDelegateAfter = getPropositionDelegate(alice); + + // 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; +} + +/* + @Rule + + @Description: + Verify that an account's voting and proposition power changes only as a result of a call to + the delegation and transfer functions + + @Note: + + @Link: +*/ +rule votingPowerChanges(address alice, method f) { + env e; + calldataarg args; + + uint aliceVotingPowerBefore = getPowerCurrent(alice, VOTING_POWER()); + uint alicePropPowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + + f(e, args); + + uint aliceVotingPowerAfter = getPowerCurrent(alice, VOTING_POWER()); + uint alicePropPowerAfter = getPowerCurrent(alice, PROPOSITION_POWER()); + + // 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; +} + +/* + @Rule + + @Description: + Verify that only delegate() and metaDelegate() may change both voting and + proposition delegates of an account at once. + + @Note: + + @Link: +*/ +rule delegationTypeIndependence(address who, method f) filtered { f -> !f.isView } { + address _delegateeV = getVotingDelegate(who); + address _delegateeP = getPropositionDelegate(who); + + env e; + calldataarg arg; + f(e, arg); + + 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), + "one delegatee type stays the same, unless delegate or delegateBySig was called"; +} + +/* + @Rule + + @Description: + Verifies that delegating twice to the same delegate changes the delegate's + voting power only once. + + @Note: + + @Link: +*/ +rule cantDelegateTwice(address _delegate) { + env e; + + address delegateBeforeV = getVotingDelegate(e.msg.sender); + address delegateBeforeP = getPropositionDelegate(e.msg.sender); + 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(); + + uint256 votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER()); + uint256 propPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER()); + + delegate(e, _delegate); + + uint256 votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER()); + uint256 propPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER()); + + delegate(e, _delegate); + + uint256 votingPowerAfter2 = getPowerCurrent(_delegate, VOTING_POWER()); + uint256 propPowerAfter2 = getPowerCurrent(_delegate, PROPOSITION_POWER()); + + assert votingPowerAfter == votingPowerBefore + normalize(balanceOf(e.msg.sender)); + assert propPowerAfter == propPowerBefore + normalize(balanceOf(e.msg.sender)); + assert votingPowerAfter2 == votingPowerAfter && propPowerAfter2 == propPowerAfter; +} + +/* + @Rule + + @Description: + transfer and transferFrom change voting/proposition power identically + + @Note: + + @Link: +*/ +rule transferAndTransferFromPowerEquivalence(address bob, uint amount) { + env e1; + env e2; + storage init = lastStorage; + + address alice; + require alice == e1.msg.sender; + + uint aliceVotingPowerBefore = getPowerCurrent(alice, VOTING_POWER()); + uint alicePropPowerBefore = getPowerCurrent(alice, PROPOSITION_POWER()); + + transfer(e1, bob, amount); + + uint aliceVotingPowerAfterTransfer = getPowerCurrent(alice, VOTING_POWER()); + uint alicePropPowerAfterTransfer = getPowerCurrent(alice, PROPOSITION_POWER()); + + transferFrom(e2, alice, bob, amount) at init; + + uint aliceVotingPowerAfterTransferFrom = getPowerCurrent(alice, VOTING_POWER()); + uint alicePropPowerAfterTransferFrom = getPowerCurrent(alice, PROPOSITION_POWER()); + + assert aliceVotingPowerAfterTransfer == aliceVotingPowerAfterTransferFrom && + alicePropPowerAfterTransfer == alicePropPowerAfterTransferFrom; + +} \ No newline at end of file diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec new file mode 100644 index 0000000..f77eba9 --- /dev/null +++ b/certora/specs/erc20.spec @@ -0,0 +1,559 @@ +/* + This is a specification file for the verification of general ERC20 + features of AaveTokenV3.sol smart contract using the Certora prover. + For more information, visit: https://www.certora.com/ + + This file is run with scripts/erc20.sh + On the token harness AaveTokenV3Harness.sol + + Sanity run: + https://prover.certora.com/output/67509/a5d16a31a49b9c9a7b71/?anonymousKey=bd108549122fd97450428a26c4ed52458793b898 +*/ +import "base.spec" + +function doesntChangeBalance(method f) returns bool { + return f.selector != transfer(address,uint256).selector && + f.selector != transferFrom(address,address,uint256).selector; +} + + + +/* + @Rule + + + @Description: + Verify that there is no fee on transferFrom() (like potentially on USDT) + + @Formula: + { + balances[bob] = y + allowance(alice, msg.sender) >= amount + } + < + transferFrom(alice, bob, amount) + > + { + balances[bob] = y + amount + } + + @Notes: + + + @Link: + +*/ +rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) { + env e; + calldataarg args; + require alice != bob; + require allowance(alice, e.msg.sender) >= amount; + uint256 balanceBefore = balanceOf(bob); + + transferFrom(e, alice, bob, amount); + + uint256 balanceAfter = balanceOf(bob); + assert balanceAfter == balanceBefore + amount; +} + +/* + @Rule + + @Description: + Verify that there is no fee on transfer() (like potentially on USDT) + + @Formula: + { + balances[bob] = y + balances[msg.sender] >= amount + } + < + transfer(bob, amount) + > + { + balances[bob] = y + amount + } + + @Notes: + + @Link: + + +*/ +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); + + transfer(e, bob, amount); + + uint256 balanceAfter = balanceOf(bob); + uint256 balanceSenderAfter = balanceOf(e.msg.sender); + assert balanceAfter == balanceBefore + amount; +} + +/* + @Rule + + + @Description: + Token transfer works correctly. Balances are updated if not reverted. + If reverted then the transfer amount was too high, or the recipient is 0. + + @Formula: + { + balanceFromBefore = balanceOf(msg.sender) + balanceToBefore = balanceOf(to) + } + < + transfer(to, amount) + > + { + lastReverted => to = 0 || amount > balanceOf(msg.sender) + !lastReverted => balanceOf(to) = balanceToBefore + amount && + balanceOf(msg.sender) = balanceFromBefore - amount + } + + @Notes: + This rule fails on tokens with a blacklist function, like USDC and USDT. + The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state. + + @Link: + +*/ + + +rule transferCorrect(address to, uint256 amount) { + env e; + require e.msg.value == 0 && e.msg.sender != 0; + uint256 fromBalanceBefore = balanceOf(e.msg.sender); + uint256 toBalanceBefore = balanceOf(to); + require fromBalanceBefore + toBalanceBefore < AAVE_MAX_SUPPLY() / 100; + + // proven elsewhere + address v_delegateTo = getVotingDelegate(to); + mathint dvbTo = getDelegatedVotingBalance(v_delegateTo); + require dvbTo >= balanceOf(to) / DELEGATED_POWER_DIVIDER() && + dvbTo < SCALED_MAX_SUPPLY() - amount / DELEGATED_POWER_DIVIDER(); + address p_delegateTo = getPropositionDelegate(to); + mathint pvbTo = getDelegatedPropositionBalance(p_delegateTo); + require pvbTo >= balanceOf(to) / DELEGATED_POWER_DIVIDER() && + pvbTo < SCALED_MAX_SUPPLY() - amount / DELEGATED_POWER_DIVIDER(); + + // proven elsewhere + address v_delegateFrom = getVotingDelegate(e.msg.sender); + address p_delegateFrom = getPropositionDelegate(e.msg.sender); + mathint dvbFrom = getDelegatedVotingBalance(v_delegateFrom); + mathint pvbFrom = getDelegatedPropositionBalance(p_delegateFrom); + 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 ! ( (getDelegatingVoting(to) && v_delegateTo == to) || + (getDelegatingProposition(to) && p_delegateTo == to)); + + // to not overcomplicate the constraints on dvbTo and dvbFrom + require v_delegateFrom != v_delegateTo && p_delegateFrom != p_delegateTo; + + transfer@withrevert(e, to, amount); + bool reverted = lastReverted; + if (!reverted) { + if (e.msg.sender == to) { + assert balanceOf(e.msg.sender) == fromBalanceBefore; + } else { + assert balanceOf(e.msg.sender) == fromBalanceBefore - amount; + assert balanceOf(to) == toBalanceBefore + amount; + } + } else { + assert amount > fromBalanceBefore || to == 0; + } +} + +/* + @Rule + + + @Description: + Test that transferFrom works correctly. Balances are updated if not reverted. + If reverted, it means the transfer amount was too high, or the recipient is 0 + + @Formula: + { + balanceFromBefore = balanceOf(from) + balanceToBefore = balanceOf(to) + } + < + transferFrom(from, to, amount) + > + { + lastreverted => to = 0 || amount > balanceOf(from) + !lastreverted => balanceOf(to) = balanceToBefore + amount && + balanceOf(from) = balanceFromBefore - amount + } + + @Notes: + This rule fails on tokens with a blacklist and or pause function, like USDC and USDT. + The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state. + + @Link: + +*/ + +rule transferFromCorrect(address from, address to, uint256 amount) { + env e; + require e.msg.value == 0; + uint256 fromBalanceBefore = balanceOf(from); + uint256 toBalanceBefore = balanceOf(to); + uint256 allowanceBefore = allowance(from, e.msg.sender); + require fromBalanceBefore + toBalanceBefore < 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 || + allowance(from, e.msg.sender) == max_uint256); +} + +/* + @Rule + + @Description: + Balance of address 0 is always 0 + + @Formula: + { balanceOf[0] = 0 } + + @Notes: + + + @Link: + +*/ +invariant ZeroAddressNoBalance() + balanceOf(0) == 0 + + +/* + @Rule + + @Description: + Contract calls don't change token total supply. + + @Formula: + { + supplyBefore = totalSupply() + } + < f(e, args)> + { + supplyAfter = totalSupply() + supplyBefore == supplyAfter + } + + @Notes: + This rule should fail for any token that has functions that change totalSupply(), like mint() and burn(). + It's still important to run the rule and see if it fails in functions that _aren't_ supposed to modify totalSupply() + + @Link: + +*/ +rule NoChangeTotalSupply(method f) { + // require f.selector != burn(uint256).selector && f.selector != mint(address, uint256).selector; + uint256 totalSupplyBefore = totalSupply(); + env e; + calldataarg args; + f(e, args); + assert totalSupply() == totalSupplyBefore; +} + +/* + The two rules cover the same ground as NoChangeTotalSupply. + + The split into two rules is in order to make the burn/mint features of a tested token even more obvious +*/ +rule noBurningTokens(method f) { + uint256 totalSupplyBefore = totalSupply(); + env e; + calldataarg args; + f(e, args); + assert totalSupply() >= totalSupplyBefore; +} + +rule noMintingTokens(method f) { + uint256 totalSupplyBefore = totalSupply(); + env e; + calldataarg args; + f(e, args); + assert totalSupply() <= totalSupplyBefore; +} + +/* + @Rule + + @Description: + Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance + + @Formula: + { + allowanceBefore = allowance(from, spender) + } + < + f(e, args) + > + { + f.selector = approve(spender, amount) => allowance(from, spender) = amount + f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount + f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta + f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta + generic f.selector => allowance(from, spender) == allowanceBefore + } + + @Notes: + Some ERC20 tokens have functions like permit() that change allowance via a signature. + The rule will fail on such functions. + + @Link: + +*/ +rule ChangingAllowance(method f, address from, address spender) { + uint256 allowanceBefore = allowance(from, spender); + env e; + if (f.selector == approve(address, uint256).selector) { + address spender_; + uint256 amount; + approve(e, spender_, amount); + if (from == e.msg.sender && spender == spender_) { + assert allowance(from, spender) == amount; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else if (f.selector == transferFrom(address,address,uint256).selector) { + address from_; + address to; + address amount; + transferFrom(e, from_, to, amount); + uint256 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) { + address spender_; + uint256 amount; + require amount <= allowanceBefore; + decreaseAllowance(e, spender_, amount); + if (from == e.msg.sender && spender == spender_) { + assert allowance(from, spender) == allowanceBefore - amount; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else if (f.selector == 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; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } + else + { + calldataarg args; + f(e, args); + assert allowance(from, spender) == allowanceBefore || + f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; + } +} + +/* + @Rule + + @Description: + Transfer from a to b doesn't change the sum of their balances + + @Formula: + { + balancesBefore = balanceOf(msg.sender) + balanceOf(b) + } + < + transfer(b, amount) + > + { + balancesBefore == balanceOf(msg.sender) + balanceOf(b) + } + + @Notes: + + @Link: + +*/ +rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) { + env e; + mathint sum = balanceOf(e.msg.sender) + balanceOf(to); + require sum < max_uint256; + transfer(e, to, amount); + assert balanceOf(e.msg.sender) + balanceOf(to) == sum; +} + +/* + @Rule + + @Description: + Transfer using transferFrom() from a to b doesn't change the sum of their balances + + @Formula: + { + balancesBefore = balanceOf(a) + balanceOf(b) + } + < + transferFrom(a, b) + > + { + balancesBefore == balanceOf(a) + balanceOf(b) + } + + @Notes: + + @Link: + +*/ +rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) { + env e; + mathint sum = balanceOf(from) + balanceOf(to); + require sum < max_uint256; + transferFrom(e, from, to, amount); + assert balanceOf(from) + balanceOf(to) == sum; +} + +/* + @Rule + + @Description: + Transfer from msg.sender to alice doesn't change the balance of other addresses + + @Formula: + { + balanceBefore = balanceOf(bob) + } + < + transfer(alice, amount) + > + { + balanceOf(bob) == balanceBefore + } + + @Notes: + + @Link: + +*/ +rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) { + env e; + require other != e.msg.sender; + require other != to && other != currentContract; + uint256 balanceBefore = balanceOf(other); + transfer(e, to, amount); + assert balanceBefore == balanceOf(other); +} + +/* + @Rule + + @Description: + Transfer from alice to bob using transferFrom doesn't change the balance of other addresses + + @Formula: + { + balanceBefore = balanceOf(charlie) + } + < + transferFrom(alice, bob, amount) + > + { + balanceOf(charlie) = balanceBefore + } + + @Notes: + + @Link: + +*/ +rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) { + env e; + require other != from; + require other != to; + uint256 balanceBefore = balanceOf(other); + transferFrom(e, from, to, amount); + assert balanceBefore == balanceOf(other); +} + +/* + @Rule + + @Description: + Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease + as a result of contract calls + + @Formula: + { + balanceBefore = balanceOf(charlie) + } + < + f(e, args) + > + { + f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore + } + + @Notes: + USDC token has functions like transferWithAuthorization that use a signed message for allowance. + FTT token has a burnFrom that lets an approved spender to burn owner's token. + Certora prover finds these counterexamples to this rule. + In general, the rule will fail on all functions other than transfer/transferFrom that change a balance of an address. + + @Link: + +*/ +rule OtherBalanceOnlyGoesUp(address other, method f) { + env e; + require other != currentContract; + uint256 balanceBefore = balanceOf(other); + + if (f.selector == 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) { + require other != e.msg.sender; + require balanceOf(e.msg.sender) + balanceBefore < max_uint256; + calldataarg args; + f(e, args); + } else { + require other != e.msg.sender; + calldataarg args; + f(e, args); + } + + assert balanceOf(other) >= balanceBefore; +} + +rule noRebasing(method f, address alice) { + env e; + calldataarg args; + + require doesntChangeBalance(f); + + uint256 balanceBefore = balanceOf(alice); + f(e, args); + uint256 balanceAfter = balanceOf(alice); + assert balanceBefore == balanceAfter; +} diff --git a/certora/specs/general.spec b/certora/specs/general.spec new file mode 100644 index 0000000..45ec69f --- /dev/null +++ b/certora/specs/general.spec @@ -0,0 +1,225 @@ +/* + This is a specification file for the verification of delegation invariants + of AaveTokenV3.sol smart contract using the Certora prover. + For more information, visit: https://www.certora.com/ + + This file is run with scripts/verifyGeneral.sh + On a version with some minimal code modifications + AaveTokenV3HarnessStorage.sol + + Sanity check results: https://prover.certora.com/output/67509/8cee7c95432ede6b3f9f/?anonymousKey=78d297585a2b2edc38f6c513e0ce12df10e47b82 +*/ + +import "base.spec" + + +/** + + Ghosts + +*/ + +// sum of all user balances +ghost mathint sumBalances { + init_state axiom sumBalances == 0; +} + +// tracking voting delegation status for each address +ghost mapping(address => bool) isDelegatingVoting { + init_state axiom forall address a. isDelegatingVoting[a] == false; +} + +// tracking voting delegation status for each address +ghost mapping(address => bool) isDelegatingProposition { + init_state axiom forall address a. isDelegatingProposition[a] == false; +} + +// sum of all voting delegated balances +ghost mathint sumDelegatedBalancesV { + init_state axiom sumDelegatedBalancesV == 0; +} + +// sum of all proposition undelegated balances +ghost mathint sumUndelegatedBalancesV { + init_state axiom sumUndelegatedBalancesV == 0; +} + +// sum of all proposition delegated balances +ghost mathint sumDelegatedBalancesP { + init_state axiom sumDelegatedBalancesP == 0; +} + +// sum of all voting undelegated balances +ghost mathint sumUndelegatedBalancesP { + init_state axiom sumUndelegatedBalancesP == 0; +} + +// token balances of each address +ghost mapping(address => uint104) balances { + init_state axiom forall address a. balances[a] == 0; +} + +/* + + Hooks + +*/ + + +/* + + This hook updates the sum of delegated and undelegated balances on each change of delegation state. + If the user moves from not delegating to delegating, their balance is moved from undelegated to delegating, + and etc. + +*/ +hook Sstore _balances[KEY address user].delegationState uint8 new_state (uint8 old_state) STORAGE { + + bool willDelegateP = !DELEGATING_PROPOSITION(old_state) && DELEGATING_PROPOSITION(new_state); + bool wasDelegatingP = DELEGATING_PROPOSITION(old_state) && !DELEGATING_PROPOSITION(new_state); + + // we cannot use if statements inside hooks, hence the ternary operator + sumUndelegatedBalancesP = willDelegateP ? (sumUndelegatedBalancesP - balances[user]) : sumUndelegatedBalancesP; + sumUndelegatedBalancesP = wasDelegatingP ? (sumUndelegatedBalancesP + balances[user]) : sumUndelegatedBalancesP; + sumDelegatedBalancesP = willDelegateP ? (sumDelegatedBalancesP + balances[user]) : sumDelegatedBalancesP; + sumDelegatedBalancesP = wasDelegatingP ? (sumDelegatedBalancesP - balances[user]) : sumDelegatedBalancesP; + + // change the delegating state only if a change is stored + + isDelegatingProposition[user] = new_state == old_state + ? isDelegatingProposition[user] + : new_state == PROPOSITION_DELEGATED() || new_state == FULL_POWER_DELEGATED(); + + + bool willDelegateV = !DELEGATING_VOTING(old_state) && DELEGATING_VOTING(new_state); + bool wasDelegatingV = DELEGATING_VOTING(old_state) && !DELEGATING_VOTING(new_state); + sumUndelegatedBalancesV = willDelegateV ? (sumUndelegatedBalancesV - balances[user]) : sumUndelegatedBalancesV; + sumUndelegatedBalancesV = wasDelegatingV ? (sumUndelegatedBalancesV + balances[user]) : sumUndelegatedBalancesV; + sumDelegatedBalancesV = willDelegateV ? (sumDelegatedBalancesV + balances[user]) : sumDelegatedBalancesV; + sumDelegatedBalancesV = wasDelegatingV ? (sumDelegatedBalancesV - balances[user]) : sumDelegatedBalancesV; + + // change the delegating state only if a change is stored + + isDelegatingVoting[user] = new_state == old_state + ? isDelegatingVoting[user] + : new_state == VOTING_DELEGATED() || new_state == FULL_POWER_DELEGATED(); +} + + +/* + + This hook updates the sum of delegated and undelegated balances on each change of user balance. + Depending on the delegation state, either the delegated or the undelegated balance get updated. + +*/ +hook Sstore _balances[KEY address user].balance uint104 balance (uint104 old_balance) STORAGE { + balances[user] = balances[user] - old_balance + balance; + // we cannot use if statements inside hooks, hence the ternary operator + sumDelegatedBalancesV = isDelegatingVoting[user] + ? sumDelegatedBalancesV + to_mathint(balance) - to_mathint(old_balance) + : sumDelegatedBalancesV; + sumUndelegatedBalancesV = !isDelegatingVoting[user] + ? sumUndelegatedBalancesV + to_mathint(balance) - to_mathint(old_balance) + : sumUndelegatedBalancesV; + sumDelegatedBalancesP = isDelegatingProposition[user] + ? sumDelegatedBalancesP + to_mathint(balance) - to_mathint(old_balance) + : sumDelegatedBalancesP; + sumUndelegatedBalancesP = !isDelegatingProposition[user] + ? sumUndelegatedBalancesP + to_mathint(balance) - to_mathint(old_balance) + : sumUndelegatedBalancesP; + +} + +// 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 + + @Description: + User's delegation flag is switched on iff user is delegating to an address + other than his own own or 0 + + @Notes: + + + @Link: + +*/ +invariant delegateCorrectness(address user) + ((getVotingDelegate(user) == user || getVotingDelegate(user) == 0) <=> !getDelegatingVoting(user)) + && + ((getPropositionDelegate(user) == user || getPropositionDelegate(user) == 0) <=> !getDelegatingProposition(user)) + { + preserved { + requireInvariant delegationStateValid(user); + } + } + +/* + @Rule + + @Description: + Sum of delegated voting balances and undelegated balances is equal to total supply + + @Notes: + + + @Link: + +*/ +invariant sumOfVBalancesCorrectness() sumDelegatedBalancesV + sumUndelegatedBalancesV == totalSupply() + +/* + @Rule + + @Description: + Sum of delegated proposition balances and undelegated balances is equal to total supply + + @Notes: + + + @Link: + +*/ +invariant sumOfPBalancesCorrectness() sumDelegatedBalancesP + sumUndelegatedBalancesP == totalSupply() + +/* + @Rule + + @Description: + Transfers don't change voting delegation state + + @Notes: + + + @Link: + +*/ +rule transferDoesntChangeDelegationState() { + 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(); + bool testFromBefore = isDelegatingVoting[from]; + bool testToBefore = isDelegatingVoting[to]; + + transferFrom(e, from, to, amount); + + uint8 stateFromAfter = getDelegationState(from); + uint8 stateToAfter = getDelegationState(to); + bool testFromAfter = isDelegatingVoting[from]; + bool testToAfter = isDelegatingVoting[to]; + + assert testFromBefore == testFromAfter && testToBefore == testToAfter; + assert getDelegationState(charlie) == stateCharlieBefore; +}