From 8f0a1c682ae2bbd3a27dbbcf374df9c1af1f5e90 Mon Sep 17 00:00:00 2001 From: Michael M Date: Wed, 29 Mar 2023 13:16:37 +0300 Subject: [PATCH] fixing patch for CI --- .github/workflows/certora.yml | 6 +- .gitignore | 1 - certora/Makefile | 9 ++- certora/README.md | 8 +-- certora/applyHarness.patch | 44 +++++------- certora/harness/AaveTokenV3Harness.sol | 70 +++++++++---------- .../harness/AaveTokenV3HarnessCommunity.sol | 62 ++++++++-------- certora/harness/AaveTokenV3HarnessStorage.sol | 49 ++++++------- certora/harness/README.md | 4 +- certora/munged/.gitignore | 2 + certora/scripts/erc20.sh | 2 +- certora/scripts/verifyCommunity.sh | 2 +- certora/scripts/verifyDelegate.sh | 2 +- certora/scripts/verifyGeneral.sh | 2 +- certora/specs/community.spec | 28 ++++---- 15 files changed, 144 insertions(+), 147 deletions(-) create mode 100644 certora/munged/.gitignore 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/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol index 6a8a099..d0e13c6 100644 --- a/certora/harness/AaveTokenV3Harness.sol +++ b/certora/harness/AaveTokenV3Harness.sol @@ -8,50 +8,48 @@ pragma solidity ^0.8.0; -import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; +import {AaveTokenV3} from "../../src/AaveTokenV3.sol"; contract AaveTokenV3Harness is AaveTokenV3 { - // returns user's token balance, used in some community rules - function getBalance(address user) public view returns (uint104) { - return _balances[user].balance; - } - // returns user's delegated proposition balance - function getDelegatedPropositionBalance(address user) public view returns (uint72) { + // 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) public view returns (uint72) { + // 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) public view returns (bool) { - return - _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } - - // returns user's delegating voting status - function getDelegatingVoting(address user) public view returns (bool) { - return - _balances[user].delegationState == DelegationState.VOTING_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } - - // returns user's voting delegate - function getVotingDelegate(address user) public view returns (address) { + } + + //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) public view returns (address) { + // 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) public view returns (DelegationState) { + // 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 index cd1dde1..ace06bf 100644 --- a/certora/harness/AaveTokenV3HarnessCommunity.sol +++ b/certora/harness/AaveTokenV3HarnessCommunity.sol @@ -2,56 +2,57 @@ /** - This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for + This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for community-written rules */ pragma solidity ^0.8.0; -import {AaveTokenV3} from '../../src/AaveTokenV3.sol'; +import {AaveTokenV3} from "../../src/AaveTokenV3.sol"; contract AaveTokenV3Harness is AaveTokenV3 { - function getBalance(address user) public view returns (uint104) { + function getBalance(address user) view public returns (uint104) { return _balances[user].balance; - } + } - function getDelegatedPropositionBalance(address user) public view returns (uint72) { + function getDelegatedPropositionBalance(address user) view public returns (uint72) { return _balances[user].delegatedPropositionBalance; - } + } - function getDelegatedVotingBalance(address user) public view returns (uint72) { + + function getDelegatedVotingBalance(address user) view public returns (uint72) { return _balances[user].delegatedVotingBalance; - } + } - function getDelegatingProposition(address user) public view returns (bool) { - return - _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } - function getDelegatingVoting(address user) public view returns (bool) { - return - _balances[user].delegationState == DelegationState.VOTING_DELEGATED || - _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; - } + function getDelegatingProposition(address user) view public returns (bool) { + return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED || + _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED; + } + - function getVotingDelegate(address user) public view returns (address) { + 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) public view returns (address) { + function getPropositionDelegate(address user) view public returns (address) { return _propositionDelegateeV2[user]; - } + } - function getDelegationState(address user) public view returns (DelegationState) { + function getDelegationState(address user) view public returns (DelegationState) { return _balances[user].delegationState; - } + } - function getNonce(address user) public view returns (uint256) { + function getNonce(address user) view public returns (uint256) { return _nonces[user]; - } + } - function ecrecoverWrapper( + function ecrecoverWrapper( bytes32 hash, uint8 v, bytes32 r, @@ -60,7 +61,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { return ecrecover(hash, v, r, s); } - function computeMetaDelegateHash( + function computeMetaDelegateHash( address delegator, address delegatee, uint256 deadline, @@ -76,7 +77,7 @@ contract AaveTokenV3Harness is AaveTokenV3 { return digest; } - function computeMetaDelegateByTypeHash( + function computeMetaDelegateByTypeHash( address delegator, address delegatee, GovernancePowerType delegationType, @@ -101,4 +102,5 @@ contract AaveTokenV3Harness is AaveTokenV3 { ); return digest; } -} + +} \ No newline at end of file diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol index fa9e764..d9b746c 100644 --- a/certora/harness/AaveTokenV3HarnessStorage.sol +++ b/certora/harness/AaveTokenV3HarnessStorage.sol @@ -12,44 +12,45 @@ 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) { + function getBalance(address user) view public returns (uint104) { return _balances[user].balance; - } + } - function getDelegatedPropositionBalance(address user) public view returns (uint72) { + function getDelegatedPropositionBalance(address user) view public returns (uint72) { return _balances[user].delegatedPropositionBalance; - } + } - function getDelegatedVotingBalance(address user) public view returns (uint72) { + + function getDelegatedVotingBalance(address user) view public returns (uint72) { return _balances[user].delegatedVotingBalance; - } + } + - function getDelegatingProposition(address user) public view returns (bool) { + 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); - } + return state == uint8(DelegationState.PROPOSITION_DELEGATED) || + state == uint8(DelegationState.FULL_POWER_DELEGATED); + } + - function getDelegatingVoting(address user) public view returns (bool) { + 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); - } + return state == uint8(DelegationState.VOTING_DELEGATED) || + state == uint8(DelegationState.FULL_POWER_DELEGATED); + } - function getVotingDelegate(address user) public view returns (address) { + function getVotingDelegate(address user) view public returns (address) { return _votingDelegateeV2[user]; - } + } - function getPropositionDelegate(address user) public view returns (address) { + function getPropositionDelegate(address user) view public returns (address) { return _propositionDelegateeV2[user]; - } + } - function getDelegationState(address user) public view returns (uint8) { + 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 index 2338a7d..e7d1aaa 100644 --- a/certora/harness/README.md +++ b/certora/harness/README.md @@ -3,5 +3,5 @@ We use two harnesses: - AaveTokenV3Harness adds a few simple getters to the original AaveTokenV3 code - AaveTokenV3HarnessStorage is used to verify general.spec. It changes delegationState field in _balances -to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which -patches the original code with `applyHarness.patch` patch. +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/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