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 delegate by type typehash #29

Open
wants to merge 68 commits into
base: certora-to-main-fork
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
68 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
40d940f
fix DELEGATE_BY_TYPE_TYPEHASH
kyzia551 Mar 17, 2023
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
7f345be
Fix scripts
tadeas-kucera Mar 28, 2023
b5c3f58
Add certora-to-main-fork github action trigger on PRs
tadeas-kucera Mar 28, 2023
7524631
Delete unused imports from munged BaseAaveToken.sol by applyHarness.p…
tadeas-kucera Mar 28, 2023
33ab90a
Merge remote-tracking branch 'remotes/upstream/fix/delegate-by-type-t…
tadeas-kucera Mar 28, 2023
b3b97b3
Fix applyHarness.patch
tadeas-kucera Mar 28, 2023
c9cf956
Merge branch 'certora-to-main-fork' into CI-test-with-PR-delegate-by-…
tadeas-kucera Mar 28, 2023
37c7f8a
Harness import contracts from munged/src instead od munged
tadeas-kucera Mar 28, 2023
39ce981
Merge branch 'certora-to-main-fork' into CI-test-with-PR-delegate-by-…
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
Prev Previous commit
Next Next commit
update folders
yuradmt committed Jul 19, 2022
commit 0d93d6b3fe7b80a46e9c7060e2fcad6412015a68
Original file line number Diff line number Diff line change
@@ -2,11 +2,11 @@

pragma solidity ^0.8.0;

import {VersionedInitializable} from '../utils/VersionedInitializable.sol';
import {VersionedInitializable} from '../../src/utils/VersionedInitializable.sol';

import {IGovernancePowerDelegationToken} from '../interfaces/IGovernancePowerDelegationToken.sol';
import {IGovernancePowerDelegationToken} from '../../src/interfaces/IGovernancePowerDelegationToken.sol';
import {BaseAaveTokenV2} from './BaseAaveTokenV2Harness.sol';
import {MathUtils} from '../utils/MathUtils.sol';
import {MathUtils} from '../../src/utils/MathUtils.sol';

contract AaveTokenV3 is BaseAaveTokenV2, IGovernancePowerDelegationToken {

@@ -106,10 +106,13 @@ contract AaveTokenV3 is BaseAaveTokenV2, IGovernancePowerDelegationToken {
) internal {
if (delegatee == address(0)) return;

// FIXING A PRECISION ISSUE HERE

// @dev to make delegated balance fit into uin72 we're decreasing precision of delegated balance by DELEGATED_POWER_DIVIDER
uint72 delegationDelta = uint72(
(userBalanceBefore / DELEGATED_POWER_DIVIDER) - (userBalanceAfter / DELEGATED_POWER_DIVIDER)
);
// uint72 delegationDelta = uint72(
// (userBalanceBefore / DELEGATED_POWER_DIVIDER) - (userBalanceAfter / DELEGATED_POWER_DIVIDER)
// );
uint72 delegationDelta = uint72((userBalanceBefore - userBalanceAfter) / DELEGATED_POWER_DIVIDER);
if (delegationDelta == 0) return;

if (delegationType == GovernancePowerType.VOTING) {
File renamed without changes.
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@ pragma solidity ^0.8.0;

// harness: import BaseAaveToken from harness file

import {VersionedInitializable} from '../utils/VersionedInitializable.sol';
import {VersionedInitializable} from '../../src/utils/VersionedInitializable.sol';

import {BaseAaveToken} from './BaseAaveTokenHarness.sol';

2 changes: 1 addition & 1 deletion certora/scripts/verifyBgdSpec.sh
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@ then
RULE="--rule $1"
fi

certoraRun src/harness/AaveTokenV3Harness.sol:AaveTokenV3 \
certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \
--verify AaveTokenV3:certora/specs/bgdSpec.spec \
--rule $1 \
--solc solc8.13 \
364 changes: 354 additions & 10 deletions certora/specs/bgdSpec.spec

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions certora/specs/setup.spec
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
// unit test, invariant, parametric test, ghost + hook, documentation
84 changes: 84 additions & 0 deletions src/BaseAaveTokenV3.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
// SPDX-License-Identifier: MIT

pragma solidity ^0.8.0;

import {VersionedInitializable} from './utils/VersionedInitializable.sol';

import {BaseAaveToken} from './BaseAaveToken.sol';

abstract contract BaseAaveTokenV2 is BaseAaveToken, VersionedInitializable {
/// @dev owner => next valid nonce to submit with permit()
mapping(address => uint256) public _nonces;

///////// @dev DEPRECATED from AaveToken v1 //////////////////////////
//////// kept for backwards compatibility with old storage layout ////
uint256[3] private ______DEPRECATED_FROM_AAVE_V1;
///////// @dev END OF DEPRECATED from AaveToken v1 //////////////////////////

bytes32 public DOMAIN_SEPARATOR;

///////// @dev DEPRECATED from AaveToken v2 //////////////////////////
//////// kept for backwards compatibility with old storage layout ////
uint256[4] private ______DEPRECATED_FROM_AAVE_V2;
///////// @dev END OF DEPRECATED from AaveToken v2 //////////////////////////

bytes public constant EIP712_REVISION = bytes('1');
bytes32 internal constant EIP712_DOMAIN =
keccak256('EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)');
bytes32 public constant PERMIT_TYPEHASH =
keccak256('Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)');

uint256 public constant REVISION = 3; // TODO: CHECK, but most probably was 2 before

/**
* @dev initializes the contract upon assignment to the InitializableAdminUpgradeabilityProxy
*/
function initialize() external initializer {}

/**
* @dev implements the permit function as for https://github.com/ethereum/EIPs/blob/8a34d644aacf0f9f8f00815307fd7dd5da07655f/EIPS/eip-2612.md
* @param owner the owner of the funds
* @param spender the spender
* @param value the amount
* @param deadline the deadline timestamp, type(uint256).max for no deadline
* @param v signature param
* @param s signature param
* @param r signature param
*/

function permit(
address owner,
address spender,
uint256 value,
uint256 deadline,
uint8 v,
bytes32 r,
bytes32 s
) external {
require(owner != address(0), 'INVALID_OWNER');
//solium-disable-next-line
require(block.timestamp <= deadline, 'INVALID_EXPIRATION');
uint256 currentValidNonce = _nonces[owner];
bytes32 digest = keccak256(
abi.encodePacked(
'\x19\x01',
DOMAIN_SEPARATOR,
keccak256(abi.encode(PERMIT_TYPEHASH, owner, spender, value, currentValidNonce, deadline))
)
);

require(owner == ecrecover(digest, v, r, s), 'INVALID_SIGNATURE');
unchecked {
// does not make sense to check because it's not realistic to reach uint256.max in nonce
_nonces[owner] = currentValidNonce + 1;
}
_approve(owner, spender, value);
}

/**
* @dev returns the revision of the implementation contract
*/
function getRevision() internal pure override returns (uint256) {
return REVISION;
}
}