Skip to content

Commit 08bdf06

Browse files
sakulstrasendrakyzia551eboadomMichaelMorami
committed
This new version of stataToken most importantly upgrades the architecture to rely on [openzeppelin-contracts-upgradeable](https://github.com/OpenZeppelin/openzeppelin-contracts-upgradeable) instead of solmate.
New features: - stataTokens now implement a permissionless rescuable, allowing to transfer excess funds to the treasury - stataTokens are now pausable. This was done in order to align aToken and stataToken functionality - in the previous version, stataTokens would no longer be redeemable but transferable when paused. - latestAnswer is now exposed directly on the token and exposes the asset price as aave would price it (based on aave-oracle & exchange rate) BREAKING_CHANGES: - meta transactions have been removed as there was no clear usecase. Instead a dedicated `depositWithPermit` was added - `deposit/redeem` are no longer overleaded with a `depositToAave/reddemFromAave` flag, but instead dedicated methods have been added `depositATokens/redeemATokens` For a full description of the changes, check https://github.com/aave-dao/aave-v3-origin/blob/project-a/src/periphery/contracts/static-a-token/README.md#upgrade-notes-statatokenv2 Co-authored-by: sakulstra <lukasstrassel@googlemail.com> Co-authored-by: sendra <sendra@users.noreply.github.com> Co-authored-by: Andrey <kyzia.ru@gmail.com> Co-authored-by: eboado <ebdmrr@gmail.com> Co-authored-by: Michael Morami <91594326+MichaelMorami@users.noreply.github.com>
1 parent 6948864 commit 08bdf06

88 files changed

Lines changed: 5824 additions & 2961 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/certora-stata.yml‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
name: certora-stata
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
pull_request:
8+
branches:
9+
- main
10+
11+
workflow_dispatch:
12+
13+
jobs:
14+
verify:
15+
runs-on: ubuntu-latest
16+
17+
steps:
18+
- uses: actions/checkout@v2
19+
with:
20+
submodules: recursive
21+
22+
- name: Install python
23+
uses: actions/setup-python@v2
24+
with: { python-version: 3.9 }
25+
26+
- name: Install java
27+
uses: actions/setup-java@v1
28+
with: { java-version: "11", java-package: jre }
29+
30+
- name: Install certora cli
31+
run: pip install certora-cli==7.14.2
32+
33+
- name: Install solc
34+
run: |
35+
wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
36+
chmod +x solc-static-linux
37+
sudo mv solc-static-linux /usr/local/bin/solc8.20
38+
39+
- name: Verify rule ${{ matrix.rule }}
40+
run: |
41+
cd certora/stata
42+
touch applyHarness.patch
43+
make munged
44+
cd ../..
45+
certoraRun certora/stata/conf/${{ matrix.rule }}
46+
env:
47+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
48+
49+
strategy:
50+
fail-fast: false
51+
max-parallel: 16
52+
matrix:
53+
rule:
54+
- verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
55+
- verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
56+
# Timeout
57+
# - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
58+
- verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
59+
- verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
60+
- verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
61+
- verifyERC4626Extended.conf --rule maxDepositConstant
62+
- verifyERC4626Extended.conf --rule redeemSum
63+
- verifyERC4626Extended.conf --rule redeemATokensSum
64+
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
65+
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
66+
- verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
67+
- verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
68+
- verifyStataToken.conf --rule totalClaimableRewards_stable
69+
- verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
70+
- verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
71+
- verifyStataToken.conf --rule singleAssetAccruedRewards
72+
- verifyStataToken.conf --rule totalAssets_stable
73+
- verifyStataToken.conf --rule getClaimableRewards_stable
74+
- verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
75+
- verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
76+
- verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
77+
- verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
78+
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
79+
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient

‎Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,4 +35,5 @@ coverage :; forge coverage --report lcov && \
3535
download :; cast etherscan-source --chain ${chain} -d src/etherscan/${chain}_${address} ${address}
3636
git-diff :
3737
@mkdir -p diffs
38+
@npx prettier ${before} ${after} --write
3839
@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --diff-algorithm=patience --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md

‎bun.lockb‎

0 Bytes
Binary file not shown.

‎certora/conf/AToken.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,6 @@
1111
"process": "emv",
1212
"solc": "solc8.19",
1313
"verify": "ATokenHarness:certora/specs/AToken.spec",
14+
// "build_cache": true,
1415
"msg": "aToken spec"
1516
}

‎certora/conf/NEW-pool-no-summarizations.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@
3636
"depositUpdatesUserATokenSuperBalance",
3737
"depositCannotChangeOthersATokenSuperBalance"
3838
],
39+
// "build_cache": true,
3940
"parametric_contracts": ["PoolHarness"],
4041
"msg": "pool-no-summarizations::partial rules",
4142
}

‎certora/conf/NEW-pool-simple-properties.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@
3838
"cannotBorrowOnReserveDisabledForBorrowing",
3939
"cannotBorrowOnFrozenReserve"
4040
],
41+
// "build_cache": true,
4142
"parametric_contracts": ["PoolHarness"],
4243
"msg": "pool-simple-properties::ALL",
4344
}

‎certora/conf/ReserveConfiguration.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,6 @@
1010
],
1111
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
1212
"solc": "solc8.19",
13+
// "build_cache": true,
1314
"verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
1415
}

‎certora/conf/StableDebtToken.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,6 @@
1414
"optimistic_loop": true,
1515
"process": "emv",
1616
"solc": "solc8.19",
17+
// "build_cache": true,
1718
"verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
1819
}

‎certora/conf/UserConfiguration.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,6 @@
1111
"-useBitVectorTheory"
1212
],
1313
"solc": "solc8.19",
14+
// "build_cache": true,
1415
"verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
1516
}

‎certora/conf/VariableDebtToken.conf‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,5 +7,6 @@
77
"optimistic_loop": true,
88
"process": "emv",
99
"solc": "solc8.19",
10+
// "build_cache": true,
1011
"verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
1112
}

0 commit comments

Comments
 (0)