diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 7dfd691..31c092d 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -32,13 +32,13 @@ jobs: - 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 @@ -49,7 +49,7 @@ jobs: sh certora/scripts/${{ matrix.rule }} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} - + strategy: fail-fast: false max-parallel: 16 diff --git a/.gitignore b/.gitignore index f0a2ae5..5b49ddb 100644 --- a/.gitignore +++ b/.gitignore @@ -9,5 +9,4 @@ package-lock.json .certora_config/ .last_confs/ .certora_* -certora/munged resource_errors.json diff --git a/certora/Makefile b/certora/Makefile index 5e6e1bc..a4c6cec 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -13,12 +13,17 @@ help: munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) rm -rf $@ - cp -r $(CONTRACTS_DIR) $@ + mkdir $@ cp -r $(LIB_DIR) $@ + cp -r $(CONTRACTS_DIR) $@ patch -p0 -d $@ < $(PATCH) record: - diff -uN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+$(CONTRACTS_DIR)/++g' | sed 's+$(MUNGED_DIR)++g' > $(PATCH) + mkdir tmp_make_r + cp -r $(LIB_DIR) tmp_make_r + cp -r $(CONTRACTS_DIR) tmp_make_r + diff -ruN tmp_make_r $(MUNGED_DIR) | sed 's+tmp_make_r/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH) + rm -rf tmp_make_r clean: git clean -fdX diff --git a/certora/README.md b/certora/README.md index 5891255..4496d02 100644 --- a/certora/README.md +++ b/certora/README.md @@ -6,17 +6,17 @@ In this directory you will find three subdirectories: - `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 +- `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. +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 +- `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 diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index b074b9f..3ae58b3 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,7 +1,14 @@ -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 @@ +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00 ++++ .gitignore 2023-03-29 13:05:55 +@@ -0,0 +1,2 @@ ++* ++!.gitignore +\ No newline at end of file +diff -ruN src/AaveTokenV3.sol src/AaveTokenV3.sol +--- src/AaveTokenV3.sol 2023-03-29 13:12:02 ++++ src/AaveTokenV3.sol 2023-03-29 13:07:15 +@@ -215,7 +215,7 @@ fromBalanceAfter = fromUserState.balance - uint104(amount); } _balances[from].balance = fromBalanceAfter; @@ -10,7 +17,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol _governancePowerTransferByType( fromUserState.balance, fromBalanceAfter, -@@ -232,7 +232,7 @@ +@@ -237,7 +237,7 @@ toUserState.balance = toBalanceBefore + uint104(amount); _balances[to] = toUserState; @@ -19,7 +26,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol _governancePowerTransferByType( toBalanceBefore, toUserState.balance, -@@ -288,7 +288,7 @@ +@@ -293,7 +293,7 @@ : address(0); } return @@ -28,7 +35,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol ? _propositionDelegateeV2[delegator] : address(0); } -@@ -325,16 +325,12 @@ +@@ -330,16 +330,12 @@ ) internal pure returns (DelegationAwareBalance memory) { if (willDelegate) { // Because GovernancePowerType starts from 0, we should add 1 first, then we apply bitwise OR @@ -48,22 +55,9 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol } 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 { +diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol +--- src/BaseAaveToken.sol 2023-03-29 13:12:02 ++++ src/BaseAaveToken.sol 2023-03-29 13:07:15 @@ -18,7 +18,7 @@ uint104 balance; uint72 delegatedPropositionBalance; @@ -73,7 +67,3 @@ diff -uN BaseAaveToken.sol /BaseAaveToken.sol } 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/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol index fa9e764..a5978fd 100644 --- a/certora/harness/AaveTokenV3HarnessStorage.sol +++ b/certora/harness/AaveTokenV3HarnessStorage.sol @@ -12,7 +12,7 @@ pragma solidity ^0.8.0; -import {AaveTokenV3} from '../munged/AaveTokenV3.sol'; +import {AaveTokenV3} from '../munged/src/AaveTokenV3.sol'; contract AaveTokenV3Harness is AaveTokenV3 { function getBalance(address user) public view returns (uint104) { diff --git a/certora/harness/README.md b/certora/harness/README.md index 2338a7d..efbc65d 100644 --- a/certora/harness/README.md +++ b/certora/harness/README.md @@ -4,4 +4,4 @@ We use two harnesses: - 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. +patches the original code with `applyHarness.patch` patch. \ No newline at end of file diff --git a/certora/munged/.gitignore b/certora/munged/.gitignore new file mode 100644 index 0000000..c96a04f --- /dev/null +++ b/certora/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore \ No newline at end of file diff --git a/certora/scripts/erc20.sh b/certora/scripts/erc20.sh index 29631e5..4b28024 100644 --- a/certora/scripts/erc20.sh +++ b/certora/scripts/erc20.sh @@ -10,4 +10,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ --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 index 2925a2d..46947f9 100644 --- a/certora/scripts/verifyCommunity.sh +++ b/certora/scripts/verifyCommunity.sh @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \ --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 index f0869cb..527014c 100755 --- a/certora/scripts/verifyDelegate.sh +++ b/certora/scripts/verifyDelegate.sh @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \ --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 index 4bd1874..6655c1c 100644 --- a/certora/scripts/verifyGeneral.sh +++ b/certora/scripts/verifyGeneral.sh @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \ --settings -smt_bitVectorTheory=true \ --cloud \ --msg "AaveTokenV3:general.spec $1" - \ No newline at end of file + diff --git a/certora/specs/community.spec b/certora/specs/community.spec index 4145f67..85e0432 100644 --- a/certora/specs/community.spec +++ b/certora/specs/community.spec @@ -1,5 +1,5 @@ /* - This is a specification file for the verification of AaveTokenV3.sol + This is a specification file for the verification of AaveTokenV3.sol smart contract using the Certora prover. The rules in this spec have been contributed by the community. Individual attribution is given in the comments to each rule. @@ -189,7 +189,7 @@ rule metaDelegateNonRepeatable(env e1, env e2, address delegator, address delega */ rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, address bob) { - require e.msg.sender != ZERO_ADDRESS(); + require e.msg.sender != ZERO_ADDRESS(); require e.msg.sender != alice && e.msg.sender != bob; require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS(); @@ -321,11 +321,11 @@ rule delegateIndependence(method f) { isVotingDelegatorAfter = getDelegatingVoting(a); isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0 - votingPowerBefore < votingPowerAfter <=> + votingPowerBefore < votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)) && - votingPowerBefore > votingPowerAfter <=> + votingPowerBefore > votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)) } @@ -355,12 +355,12 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { require !isVotingDelegateeBefore && !isVotingDelegateeAfter; - /* + /* If you're not a delegatee, your voting power only increases when 1. You're not delegating and your balance increases 2. You're delegating and stop delegating and your balanceBefore != 0 */ - assert votingPowerBefore < votingPowerAfter <=> + assert votingPowerBefore < votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) || (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0)); @@ -369,7 +369,7 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { 1. You're not delegating and your balance decreases 2. You're not delegating and start delegating and your balanceBefore != 0 */ - assert votingPowerBefore > votingPowerAfter <=> + assert votingPowerBefore > votingPowerAfter <=> (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) || (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0)); } @@ -396,11 +396,11 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) { isPropositionDelegatorAfter = getDelegatingProposition(a); isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0 - propositionPowerBefore < propositionPowerAfter <=> + propositionPowerBefore < propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)) && - propositionPowerBefore > propositionPowerAfter <=> + propositionPowerBefore > propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) || (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)) } @@ -435,16 +435,16 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) { 1. You're not delegating and your balance increases 2. You're delegating and stop delegating and your balanceBefore != 0 */ - assert propositionPowerBefore < propositionPowerAfter <=> + assert propositionPowerBefore < propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) || (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0)); - + /* If you're not a delegatee, your proposition power only decreases when 1. You're not delegating and your balance decreases 2. You're not delegating and start delegating and your balanceBefore != 0 */ - assert propositionPowerBefore > propositionPowerAfter <=> + assert propositionPowerBefore > propositionPowerAfter <=> (!isPropositionDelegatorBefore && !isPropositionDelegatorBefore && (balanceBefore > balanceAfter)) || (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0)); } @@ -463,7 +463,7 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) { f(e, args) > { - allowance(owner, spender) != allowanceBefore =>f.selector==approve(address,uint256).selector + 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 @@ -486,7 +486,7 @@ rule allowanceStateChange(env e){ f(e, args); uint256 allowanceAfter=allowance(owner,user); - assert allowanceBefore!=allowanceAfter => f.selector==approve(address,uint256).selector + 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