Skip to content

Commit 859b070

Browse files
miguelmtzinfefecarranzanisnislevi
authored
feat: Add support for Remote GSM (#9)
* feat: initial commit * feat: finish tests * fix: safecast overflow * feat: overflow tests * feat: add entity checks and delete usage * fix: update test * feat: add limit check on remove entity * chore: remove unnecesarry check * chore: remove deletion * feat: add audit * chore: run lint * for PR * chore: lint certora * chore: run ci without if * chore: add all certora ci * chore: explicit certora key --------- Co-authored-by: Fermin 'Piscu' Carranza <[email protected]> Co-authored-by: nisnislevi <[email protected]>
1 parent a4f80fc commit 859b070

File tree

126 files changed

+3543
-2387
lines changed

Some content is hidden

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

126 files changed

+3543
-2387
lines changed

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

Lines changed: 0 additions & 56 deletions
This file was deleted.

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

Lines changed: 40 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
name: certora-gho
22

3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
37
on:
48
pull_request:
59
branches:
6-
- main
7-
- certora
10+
- "*"
811
push:
912
branches:
1013
- main
@@ -14,57 +17,48 @@ on:
1417
jobs:
1518
verify:
1619
runs-on: ubuntu-latest
17-
20+
permissions:
21+
contents: read
22+
statuses: write
23+
pull-requests: write
24+
id-token: write
1825
steps:
19-
- name: Checkout
20-
uses: actions/checkout@v4
26+
- uses: actions/checkout@v4
2127
with:
2228
submodules: recursive
2329

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 }}
30+
- name: Munged
4231
run: |
4332
cd certora/gho
4433
touch applyHarness.patch
4534
make munged
46-
cd ../..
47-
certoraRun certora/gho/conf/${{ matrix.rule }}
35+
36+
- uses: Certora/certora-run-action@v2
37+
with:
38+
cli-version: 7.31.2
39+
configurations: |-
40+
certora/gho/conf/verifyUpgradeableGhoToken.conf
41+
certora/gho/conf/verifyGhoToken.conf
42+
certora/gho/conf/verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
43+
certora/gho/conf/verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
44+
certora/gho/conf/verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
45+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken
46+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint
47+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt
48+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate
49+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance
50+
certora/gho/conf/verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent
51+
certora/gho/conf/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
52+
certora/gho/conf/verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh
53+
certora/gho/conf/verifyGhoVariableDebtTokenInternal.conf
54+
certora/gho/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf
55+
certora/gho/conf/verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease
56+
solc-versions: 0.8.10
57+
comment-fail-only: false
58+
solc-remove-version-prefix: "0."
59+
job-name: "Certora Prover Run"
60+
certora-key: ${{ secrets.CERTORAKEY }}
61+
install-java: true
4862
env:
63+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
4964
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: 42 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
name: certora-gsm-4626
22

3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
37
on:
48
pull_request:
59
branches:
6-
- main
7-
- certora
10+
- "*"
811
push:
912
branches:
1013
- main
@@ -14,56 +17,46 @@ on:
1417
jobs:
1518
verify:
1619
runs-on: ubuntu-latest
17-
20+
permissions:
21+
contents: read
22+
statuses: write
23+
pull-requests: write
24+
id-token: write
1825
steps:
19-
- name: Checkout
20-
uses: actions/checkout@v4
26+
- uses: actions/checkout@v4
2127
with:
2228
submodules: recursive
2329

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 }}
30+
- uses: Certora/certora-run-action@v2
31+
with:
32+
cli-version: 7.31.2
33+
configurations: |-
34+
certora/gsm/conf/gsm4626/gho-gsm4626-1.conf
35+
certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis
36+
certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule accruedFeesNeverDecrease
37+
#certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule systemBalanceStabilitySell waiting for ticket CERT-9408
38+
certora/gsm/conf/gsm4626/gho-gsm4626-inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19
39+
certora/gsm/conf/gsm4626/balances-buy-4626.conf
40+
certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq
41+
certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly
42+
certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange
43+
certora/gsm/conf/gsm4626/fees-buy-4626.conf
44+
certora/gsm/conf/gsm4626/fees-sell-4626.conf --rule R3a_estimatedSellFeeCanBeLowerThanActualSellFee R2_getAssetAmountForSellAssetVsActualSellFee R4a_getSellFeeVsgetAssetAmountForSellAsset R4_getSellFeeVsgetAssetAmountForSellAsset R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee
45+
certora/gsm/conf/gsm4626/optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset
46+
certora/gsm/conf/gsm4626/optimality4626.conf --rule R1_optimalityOfBuyAsset_v1
47+
certora/gsm/conf/gsm4626/optimality4626.conf --rule R3_optimalityOfSellAsset_v1
48+
certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness
49+
certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_optimality
50+
certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_correctness
51+
certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
52+
certora/gsm/conf/gsm4626/finishedRules-4626.conf --rule cantBuyOrSellWhenSeized cantBuyOrSellWhenFrozen sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingAssetKeepsAccruedFees rescuingGhoKeepsAccruedFees giftingGhoDoesntAffectStorageSIMPLE correctnessOfBuyAsset giftingUnderlyingDoesntAffectStorageSIMPLE sellAssetSameAsGetGhoAmountForSellAsset correctnessOfSellAsset giftingGhoDoesntCreateExcessOrDearth backWithGhoDoesntCreateExcess getAssetAmountForSellAsset_correctness collectedSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure
53+
certora/gsm/conf/gsm4626/finishedRules-4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth
54+
solc-versions: 0.8.20
55+
comment-fail-only: false
56+
solc-remove-version-prefix: "0."
57+
job-name: "Certora Prover Run"
58+
certora-key: ${{ secrets.CERTORAKEY }}
59+
install-java: true
4460
env:
61+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
4562
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

0 commit comments

Comments
 (0)