Skip to content

Commit 4090c6b

Browse files
avniculaeavniculae
committed
Initial commit
0 parents  commit 4090c6b

File tree

310 files changed

+41430
-0
lines changed

Some content is hidden

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

310 files changed

+41430
-0
lines changed

‎.editorconfig‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# EditorConfig helps developers define and maintain consistent
2+
# coding styles between different editors and IDEs
3+
# http://editorconfig.org
4+
5+
root = true
6+
7+
[*]
8+
indent_style = space
9+
indent_size = 2
10+
end_of_line = lf
11+
charset = utf-8
12+
trim_trailing_whitespace = true
13+
insert_final_newline = true
14+
15+
[{Makefile,**.mk}]
16+
# Use tabs for indentation (Makefiles require tabs)
17+
indent_style = tab

‎.github/workflows/certora-gho-505.yml‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
name: certora-gho-5.0.5
2+
3+
on:
4+
pull_request:
5+
branches:
6+
- main
7+
- certora
8+
push:
9+
branches:
10+
- main
11+
12+
workflow_dispatch:
13+
14+
jobs:
15+
verify:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- name: Checkout
20+
uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- name: Install python
25+
uses: actions/setup-python@v5
26+
with: { python-version: 3.9 }
27+
28+
- name: Install java
29+
uses: actions/setup-java@v4
30+
with: { distribution: "zulu", java-version: "11", java-package: jre }
31+
32+
- name: Install certora cli
33+
run: pip install certora-cli==5.0.5
34+
35+
- name: Install solc
36+
run: |
37+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
38+
chmod +x solc-static-linux
39+
sudo mv solc-static-linux /usr/local/bin/solc8.10
40+
41+
- name: Verify rule ${{ matrix.rule }}
42+
run: |
43+
cd certora/gho
44+
touch applyHarness.patch
45+
make munged
46+
cd ../..
47+
certoraRun certora/gho/conf/${{ matrix.rule }}
48+
env:
49+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
50+
51+
strategy:
52+
fail-fast: false
53+
max-parallel: 16
54+
matrix:
55+
rule:
56+
- verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease

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

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
name: certora-gho
2+
3+
on:
4+
pull_request:
5+
branches:
6+
- main
7+
- certora
8+
push:
9+
branches:
10+
- main
11+
12+
workflow_dispatch:
13+
14+
jobs:
15+
verify:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- name: Checkout
20+
uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- name: Install python
25+
uses: actions/setup-python@v5
26+
with: { python-version: 3.9 }
27+
28+
- name: Install java
29+
uses: actions/setup-java@v4
30+
with: { distribution: "zulu", java-version: "11", java-package: jre }
31+
32+
- name: Install certora cli
33+
run: pip install certora-cli==4.13.1
34+
35+
- name: Install solc
36+
run: |
37+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
38+
chmod +x solc-static-linux
39+
sudo mv solc-static-linux /usr/local/bin/solc8.10
40+
41+
- name: Verify rule ${{ matrix.rule }}
42+
run: |
43+
cd certora/gho
44+
touch applyHarness.patch
45+
make munged
46+
cd ../..
47+
certoraRun certora/gho/conf/${{ matrix.rule }}
48+
env:
49+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
50+
51+
strategy:
52+
fail-fast: false
53+
max-parallel: 16
54+
matrix:
55+
rule:
56+
- verifyUpgradeableGhoToken.conf
57+
- verifyGhoToken.conf
58+
- verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
59+
- verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
60+
- verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
61+
- verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken
62+
- verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint
63+
- verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt
64+
- verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate
65+
- verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance
66+
- verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent
67+
- verifyGhoVariableDebtToken.conf --rule disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy user_index_up_to_date
68+
- verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh
69+
- verifyGhoVariableDebtTokenInternal.conf
70+
- verifyGhoVariableDebtToken-rayMulDiv-summarization.conf

‎.github/workflows/certora-gsm-4626.yml‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
name: certora-gsm-4626
2+
3+
on:
4+
pull_request:
5+
branches:
6+
- main
7+
- certora
8+
push:
9+
branches:
10+
- main
11+
12+
workflow_dispatch:
13+
14+
jobs:
15+
verify:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- name: Checkout
20+
uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- name: Install python
25+
uses: actions/setup-python@v5
26+
with: { python-version: 3.9 }
27+
28+
- name: Install java
29+
uses: actions/setup-java@v4
30+
with: { distribution: "zulu", java-version: "11", java-package: jre }
31+
32+
- name: Install certora cli
33+
run: pip install certora-cli==7.14.2
34+
35+
- name: Install solc
36+
run: |
37+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
38+
chmod +x solc-static-linux
39+
sudo mv solc-static-linux /usr/local/bin/solc8.10
40+
41+
- name: Verify rule ${{ matrix.rule }}
42+
run: |
43+
certoraRun certora/gsm/conf/gsm4626/${{ matrix.rule }}
44+
env:
45+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
46+
47+
strategy:
48+
fail-fast: false
49+
max-parallel: 16
50+
matrix:
51+
rule:
52+
- gho-gsm_4626_inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19
53+
- gho-gsm4626.conf --rule enoughULtoBackGhoNonBuySell NonZeroFeeCheckSellAsset NonZeroFeeCheckBuyAsset
54+
- balances-buy-4626.conf
55+
- balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq
56+
- balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly
57+
- balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange
58+
- fees-buy-4626.conf
59+
- fees-sell-4626.conf --rule R3a_estimatedSellFeeCanBeLowerThanActualSellFee R2_getAssetAmountForSellAssetVsActualSellFee R4a_getSellFeeVsgetAssetAmountForSellAsset R4_getSellFeeVsgetAssetAmountForSellAsset R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee
60+
- gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis accruedFeesNeverDecrease systemBalanceStabilitySell systemBalanceStabilitySell
61+
- optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset
62+
- optimality4626.conf --rule R1_optimalityOfBuyAsset_v1
63+
- optimality4626.conf --rule R3_optimalityOfSellAsset_v1
64+
- getAmount_4626_properties.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness
65+
- getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_optimality
66+
- getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_correctness
67+
- getAmount_4626_properties.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
68+
- finishedRules4626.conf --rule cantBuyOrSellWhenSeized cantBuyOrSellWhenFrozen sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingAssetKeepsAccruedFees rescuingGhoKeepsAccruedFees giftingGhoDoesntAffectStorageSIMPLE correctnessOfBuyAsset giftingUnderlyingDoesntAffectStorageSIMPLE sellAssetSameAsGetGhoAmountForSellAsset correctnessOfSellAsset giftingGhoDoesntCreateExcessOrDearth backWithGhoDoesntCreateExcess getAssetAmountForSellAsset_correctness collectedSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure
69+
- finishedRules4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth

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

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
name: certora-gsm
2+
3+
on:
4+
pull_request:
5+
branches:
6+
- main
7+
- certora
8+
push:
9+
branches:
10+
- main
11+
12+
workflow_dispatch:
13+
14+
jobs:
15+
verify:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- name: Checkout
20+
uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- name: Install python
25+
uses: actions/setup-python@v5
26+
with: { python-version: 3.9 }
27+
28+
- name: Install java
29+
uses: actions/setup-java@v4
30+
with: { distribution: "zulu", java-version: "11", java-package: jre }
31+
32+
- name: Install certora cli
33+
run: pip install certora-cli==6.1.3
34+
35+
- name: Install solc
36+
run: |
37+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
38+
chmod +x solc-static-linux
39+
sudo mv solc-static-linux /usr/local/bin/solc8.10
40+
41+
- name: Verify rule ${{ matrix.rule }}
42+
run: |
43+
certoraRun certora/gsm/conf/gsm/${{ matrix.rule }}
44+
env:
45+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
46+
47+
strategy:
48+
fail-fast: false
49+
max-parallel: 16
50+
matrix:
51+
rule:
52+
- gho-gsm_inverse.conf
53+
- gho-gsm.conf
54+
- balances-buy.conf
55+
- balances-sell.conf
56+
- gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
57+
- gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
58+
- gho-fixedPriceStrategy.conf
59+
- fees-buy.conf
60+
- fees-sell.conf
61+
- FixedFeeStrategy.conf
62+
- gho-gsm.conf
63+
- optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
64+
- getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
65+
- finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
66+
- OracleSwapFreezer.conf

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

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
name: certora-steward
2+
3+
on:
4+
pull_request:
5+
branches:
6+
- main
7+
- certora
8+
push:
9+
branches:
10+
- main
11+
12+
workflow_dispatch:
13+
14+
jobs:
15+
verify:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- name: Checkout
20+
uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- name: Install python
25+
uses: actions/setup-python@v5
26+
with: { python-version: 3.9 }
27+
28+
- name: Install java
29+
uses: actions/setup-java@v4
30+
with: { distribution: "zulu", java-version: "11", java-package: jre }
31+
32+
- name: Install certora cli
33+
run: pip install certora-cli
34+
35+
- name: Install solc
36+
run: |
37+
cd certora/steward/
38+
touch applyHarness.patch
39+
make munged
40+
cd ../..
41+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
42+
chmod +x solc-static-linux
43+
sudo mv solc-static-linux /usr/local/bin/solc8.10
44+
45+
- name: Verify rule ${{ matrix.rule }}
46+
run: |
47+
certoraRun certora/steward/conf/${{ matrix.rule }}
48+
env:
49+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
50+
51+
strategy:
52+
fail-fast: false
53+
max-parallel: 16
54+
matrix:
55+
rule:
56+
- GhoAaveSteward.conf
57+
- GhoBucketSteward.conf
58+
- GhoCcipSteward.conf
59+
- GhoGsmSteward.conf

‎.github/workflows/test.yml‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
name: CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
env:
9+
FOUNDRY_PROFILE: ci
10+
11+
jobs:
12+
lint:
13+
uses: bgd-labs/github-workflows/.github/workflows/foundry-lint-prettier.yml@main
14+
check:
15+
strategy:
16+
fail-fast: true
17+
18+
name: Foundry project
19+
runs-on: ubuntu-latest
20+
env:
21+
ALCHEMY_KEY: "${{secrets.ALCHEMY_KEY}}"
22+
ETH_RPC_URL: "https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}"
23+
RPC_MAINNET: "https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}"
24+
RPC_ARBITRUM: "https://arb-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}"
25+
steps:
26+
- uses: actions/checkout@v4
27+
with:
28+
submodules: recursive
29+
30+
- name: Install Foundry
31+
uses: foundry-rs/foundry-toolchain@v1
32+
with:
33+
version: nightly
34+
35+
- name: Show Forge version
36+
run: |
37+
forge --version
38+
39+
- name: Run Forge build
40+
run: |
41+
forge build --sizes
42+
id: build
43+
44+
- name: Run Forge tests
45+
run: |
46+
forge test -vvv
47+
id: test

0 commit comments

Comments
 (0)