Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ci test with pr base delegation #31

Open
wants to merge 67 commits into
base: certora-to-main-fork
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
67 commits
Select commit Hold shift + click to select a range
0f582d7
certora folder with complexit check + git ignore
MichaelMorami May 25, 2022
1e657e3
certora folder with complexit check + git ignore
MichaelMorami May 25, 2022
c36fab4
removing unnecessary files and updating contract
MichaelMorami May 25, 2022
9608d99
Merge branch 'certora' of github.com:bgd-labs/aave-token-v3 into certora
MichaelMorami May 25, 2022
5bffdd8
removing unnecessary files
MichaelMorami May 25, 2022
12f9931
starting setup
MichaelMorami Jun 20, 2022
72e3e5d
feat: initial harness and unit test
yuradmt Jun 28, 2022
bf7fe90
splitting certora's gitignore from main gitignore
MichaelMorami Jun 29, 2022
ff4fecc
Merge branch 'certora' of github.com:bgd-labs/aave-token-v3 into certora
MichaelMorami Jun 29, 2022
f5f767a
feat: new rules
yuradmt Jul 12, 2022
c2e0cb4
Merge branch 'certora' of https://github.com/bgd-labs/aave-token-v3 i…
yuradmt Jul 12, 2022
da405d3
fix: upgate gitignore to exclude certora config
yuradmt Jul 12, 2022
0d93d6b
update folders
yuradmt Jul 19, 2022
249a7f2
merge certora folder with complexit check + git ignore
MichaelMorami May 25, 2022
d161df8
removing unnecessary files and updating contract
MichaelMorami May 25, 2022
676fe4a
certora folder with complexit check + git ignore
MichaelMorami May 25, 2022
abe6a90
removing unnecessary files
MichaelMorami May 25, 2022
72013e2
starting setup
MichaelMorami Jun 20, 2022
9cb5293
feat: initial harness and unit test
yuradmt Jun 28, 2022
bb26417
feat: new rules
yuradmt Jul 12, 2022
452e2c5
splitting certora's gitignore from main gitignore
MichaelMorami Jun 29, 2022
75f28eb
fix: upgate gitignore to exclude certora config
yuradmt Jul 12, 2022
1988a65
update folders
yuradmt Jul 19, 2022
f1b94fa
rebase from main
yuradmt Jul 19, 2022
183e803
Merge branch 'certora' of https://github.com/bgd-labs/aave-token-v3 i…
yuradmt Jul 19, 2022
1a71906
rebase from small-loss-precision branch
yuradmt Jul 19, 2022
d2e3e2a
add a setup
yuradmt Jul 20, 2022
e5e039f
add erc20 spec
yuradmt Jul 25, 2022
258e337
finalize delegate.spec
yuradmt Jul 26, 2022
cff0a2f
refactor harness
yuradmt Jul 27, 2022
0fafd34
refactor harness
yuradmt Jul 28, 2022
3f73a32
update AaveTokenV3 from main
yuradmt Jul 28, 2022
b937ed4
gitignore
yuradmt Jul 29, 2022
097b44f
install test
yuradmt Jul 31, 2022
429bcd8
add delegation to zero invariant
yuradmt Jul 31, 2022
77ebc77
update delegate correctness invariant
yuradmt Jul 31, 2022
634118d
invariant for sum of all balances
yuradmt Aug 1, 2022
4ebd9d0
fix invariants
yuradmt Aug 1, 2022
4430e60
update general.spec and invariants
yuradmt Aug 4, 2022
1bee65b
clean up
yuradmt Aug 7, 2022
b54110b
fix cantDelegateTwice rule
yuradmt Aug 7, 2022
dde0954
add README
yuradmt Aug 10, 2022
b228950
update sanity runs
yuradmt Aug 10, 2022
2c80326
fix: bug in transferCorrect rule
yuradmt Aug 10, 2022
2a7e417
clean up comments
yuradmt Aug 11, 2022
1dca850
adding the git ignore
MichaelMorami Aug 14, 2022
bd5474c
Add community spec
yuradmt Sep 11, 2022
fa9f813
Merge branch 'certora' of https://github.com/bgd-labs/aave-token-v3 i…
yuradmt Sep 11, 2022
610fdbf
add comments to the community spec
yuradmt Sep 12, 2022
f181c15
add munged for creating harnesses
yuradmt Sep 21, 2022
8456c34
delete todos
yuradmt Sep 21, 2022
5046629
add markdown report
yuradmt Sep 21, 2022
d4b0cd1
add PDF report
yuradmt Sep 21, 2022
4b69038
updating code according to BGD update
MichaelMorami Oct 2, 2022
f624eda
Create temp.yml
MichaelMorami Oct 6, 2022
04688de
Certora + Community Formal Verification
MichaelMorami Oct 11, 2022
6f08e2e
Sync with upstream
tadeas-kucera Mar 28, 2023
68bccf6
Merge main to this branch after syncing with bgd repo remote origin
tadeas-kucera Mar 28, 2023
65e71ad
Fix applyHarness.patch and Makefile
tadeas-kucera Mar 28, 2023
924cb6f
draft: BaseDelegation
kyzia551 Mar 28, 2023
7f345be
Fix scripts
tadeas-kucera Mar 28, 2023
b5c3f58
Add certora-to-main-fork github action trigger on PRs
tadeas-kucera Mar 28, 2023
7a97d9d
change GovernancePowerType to uint8 on DELEGATE_BY_TYPE_TYPEHASH
kyzia551 Mar 28, 2023
7524631
Delete unused imports from munged BaseAaveToken.sol by applyHarness.p…
tadeas-kucera Mar 28, 2023
b3b97b3
Fix applyHarness.patch
tadeas-kucera Mar 28, 2023
37c7f8a
Harness import contracts from munged/src instead od munged
tadeas-kucera Mar 28, 2023
3cf1ca3
Merge remote-tracking branch 'upstream/feat/base-delegation-isolation…
tadeas-kucera Mar 28, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions .github/workflows/certora.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ on:
pull_request:
branches:
- main
- certora-to-main-fork

workflow_dispatch:

Expand All @@ -32,13 +33,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
Expand All @@ -49,7 +50,7 @@ jobs:
sh certora/scripts/${{ matrix.rule }}
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}

strategy:
fail-fast: false
max-parallel: 16
Expand Down
36 changes: 36 additions & 0 deletions .github/workflows/temp.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
# This is a basic workflow to help you get started with Actions

name: CI

# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the "main" branch
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]

# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:

# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
# This workflow contains a single job called "build"
build:
# The type of runner that the job will run on
runs-on: ubuntu-latest

# Steps represent a sequence of tasks that will be executed as part of the job
steps:
# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
- uses: actions/checkout@v3

# Runs a single command using the runners shell
- name: Run a one-line script
run: echo Hello, world!

# Runs a set of commands using the runners shell
- name: Run a multi-line script
run: |
echo Add other actions to build,
echo test, and deploy your project.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# $AAVE V3

Next iteration of the AAVE token, optimized for its usage on the upcoming new iteration of the Aave Governance.
Nex#t iteration of the AAVE token, optimized for its usage on the upcoming new iteration of the Aave Governance.

More detailed description and specification [HERE](./properties.md)

Expand All @@ -13,4 +13,4 @@ After having installed Foundry:
2. `make test` to run the simulation tests.

## Copyright
2022 BGD Labs
2022 BGD Labs
9 changes: 7 additions & 2 deletions certora/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
43 changes: 15 additions & 28 deletions certora/applyHarness.patch
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
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 @@
Binary files .DS_Store and .DS_Store differ
diff -ruN src/AaveTokenV3.sol src/AaveTokenV3.sol
--- src/AaveTokenV3.sol 2023-03-28 15:10:26
+++ src/AaveTokenV3.sol 2023-03-28 15:05:22
@@ -215,7 +215,7 @@
fromBalanceAfter = fromUserState.balance - uint104(amount);
}
_balances[from].balance = fromBalanceAfter;
Expand All @@ -10,7 +11,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;

Expand All @@ -19,7 +20,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
_governancePowerTransferByType(
toBalanceBefore,
toUserState.balance,
@@ -288,7 +288,7 @@
@@ -293,7 +293,7 @@
: address(0);
}
return
Expand All @@ -28,7 +29,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
Expand All @@ -48,32 +49,18 @@ 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;
diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol
--- src/BaseAaveToken.sol 2023-03-28 15:10:26
+++ src/BaseAaveToken.sol 2023-03-28 15:10:24
@@ -16,10 +16,10 @@

-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 @@
// reorder fields to make hooks syntax simpler
struct DelegationAwareBalance {
- DelegationState delegationState;
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
4 changes: 2 additions & 2 deletions certora/harness/AaveTokenV3HarnessStorage.sol
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@

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";
import {AaveTokenV3} from "../munged/src/AaveTokenV3.sol";

contract AaveTokenV3Harness is AaveTokenV3 {
function getBalance(address user) view public returns (uint104) {
Expand Down
2 changes: 1 addition & 1 deletion certora/scripts/erc20.sh
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
--optimistic_loop \
--cloud \
--msg "AaveTokenV3:erc20.spec $1"

2 changes: 1 addition & 1 deletion certora/scripts/verifyCommunity.sh
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \
--cloud \
--msg "AaveTokenV3HarnessCommunity:community.spec $1"
# --sanity

2 changes: 1 addition & 1 deletion certora/scripts/verifyDelegate.sh
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
--cloud \
--msg "AaveTokenV3Harness:delegate.spec $1"
# --sanity

2 changes: 1 addition & 1 deletion certora/scripts/verifyGeneral.sh
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \
--settings -smt_bitVectorTheory=true \
--cloud \
--msg "AaveTokenV3:general.spec $1"

28 changes: 14 additions & 14 deletions certora/specs/community.spec
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -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))
}
Expand Down Expand Up @@ -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));

Expand All @@ -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));
}
Expand All @@ -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))
}
Expand Down Expand Up @@ -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));
}
Expand All @@ -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
Expand All @@ -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
Expand Down
1 change: 0 additions & 1 deletion lib/aave-token-v2
Submodule aave-token-v2 deleted from 6ebf51
1 change: 0 additions & 1 deletion lib/forge-std
Submodule forge-std deleted from 1680d7
Loading