Remote GSM

.github/workflows/certora-gho.yml

@@ -1,10 +1,13 @@
 name: certora-gho
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
   pull_request:
     branches:
-      - main
-      - certora
+      - "*"
   push:
     branches:
       - main
@@ -14,57 +17,48 @@ on:
 jobs:
   verify:
     runs-on: ubuntu-latest
-
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
     steps:
-      - name: Checkout
-        uses: actions/checkout@v4
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
-      - name: Install python
-        uses: actions/setup-python@v5
-        with: { python-version: 3.9 }
-
-      - name: Install java
-        uses: actions/setup-java@v4
-        with: { distribution: "zulu", java-version: "11", java-package: jre }
-
-      - name: Install certora cli
-        run: pip install certora-cli==4.13.1
-
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
-          chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.10
-
-      - name: Verify rule ${{ matrix.rule }}
+      - name: Munged
         run: |
           cd certora/gho
           touch applyHarness.patch
           make munged
-          cd ../..
-          certoraRun certora/gho/conf/${{ matrix.rule }}
+
+      - uses: Certora/certora-run-action@v2
+        with:
+          cli-version: 7.31.2
+          configurations: |-
+            certora/gho/conf/verifyUpgradeableGhoToken.conf
+            certora/gho/conf/verifyGhoToken.conf
+            certora/gho/conf/verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
+            certora/gho/conf/verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
+            certora/gho/conf/verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance
+            certora/gho/conf/verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent
+            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
+            certora/gho/conf/verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh
+            certora/gho/conf/verifyGhoVariableDebtTokenInternal.conf
+            certora/gho/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf
+            certora/gho/conf/verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease
+          solc-versions: 0.8.10
+          comment-fail-only: false
+          solc-remove-version-prefix: "0."
+          job-name: "Certora Prover Run"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          install-java: true
         env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
-
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - verifyUpgradeableGhoToken.conf
-          - verifyGhoToken.conf
-          - verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
-          - verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
-          - verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
-          - verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken
-          - verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint
-          - verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt
-          - verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate
-          - verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance
-          - verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent
-          - 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
-          - verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh
-          - verifyGhoVariableDebtTokenInternal.conf
-          - verifyGhoVariableDebtToken-rayMulDiv-summarization.conf

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

@@ -1,10 +1,13 @@
 name: certora-gsm-4626
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
   pull_request:
     branches:
-      - main
-      - certora
+      - "*"
   push:
     branches:
       - main
@@ -14,56 +17,46 @@ on:
 jobs:
   verify:
     runs-on: ubuntu-latest
-
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
     steps:
-      - name: Checkout
-        uses: actions/checkout@v4
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
-      - name: Install python
-        uses: actions/setup-python@v5
-        with: { python-version: 3.9 }
-
-      - name: Install java
-        uses: actions/setup-java@v4
-        with: { distribution: "zulu", java-version: "11", java-package: jre }
-
-      - name: Install certora cli
-        run: pip install certora-cli==7.14.2
-
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
-          chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.10
-
-      - name: Verify rule ${{ matrix.rule }}
-        run: |
-          certoraRun certora/gsm/conf/gsm4626/${{ matrix.rule }}
+      - uses: Certora/certora-run-action@v2
+        with:
+          cli-version: 7.31.2
+          configurations: |-
+            certora/gsm/conf/gsm4626/gho-gsm4626-1.conf
+            certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis 
+            certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule accruedFeesNeverDecrease  
+            #certora/gsm/conf/gsm4626/gho-gsm4626-2.conf --rule systemBalanceStabilitySell waiting for ticket CERT-9408
+            certora/gsm/conf/gsm4626/gho-gsm4626-inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19
+            certora/gsm/conf/gsm4626/balances-buy-4626.conf
+            certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq
+            certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly
+            certora/gsm/conf/gsm4626/balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange
+            certora/gsm/conf/gsm4626/fees-buy-4626.conf
+            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
+            certora/gsm/conf/gsm4626/optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset
+            certora/gsm/conf/gsm4626/optimality4626.conf --rule R1_optimalityOfBuyAsset_v1
+            certora/gsm/conf/gsm4626/optimality4626.conf --rule R3_optimalityOfSellAsset_v1
+            certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness
+            certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_optimality
+            certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_correctness
+            certora/gsm/conf/gsm4626/getAmount-properties-4626.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
+            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
+            certora/gsm/conf/gsm4626/finishedRules-4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth
+          solc-versions: 0.8.20
+          comment-fail-only: false
+          solc-remove-version-prefix: "0."
+          job-name: "Certora Prover Run"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          install-java: true
         env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
-
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - gho-gsm_4626_inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19
-          - gho-gsm4626.conf --rule enoughULtoBackGhoNonBuySell NonZeroFeeCheckSellAsset NonZeroFeeCheckBuyAsset
-          - balances-buy-4626.conf
-          - balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq
-          - balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly
-          - balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange
-          - fees-buy-4626.conf
-          - fees-sell-4626.conf --rule R3a_estimatedSellFeeCanBeLowerThanActualSellFee R2_getAssetAmountForSellAssetVsActualSellFee R4a_getSellFeeVsgetAssetAmountForSellAsset R4_getSellFeeVsgetAssetAmountForSellAsset R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee
-          - gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis accruedFeesNeverDecrease systemBalanceStabilitySell systemBalanceStabilitySell
-          - optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset
-          - optimality4626.conf --rule R1_optimalityOfBuyAsset_v1
-          - optimality4626.conf --rule R3_optimalityOfSellAsset_v1
-          - getAmount_4626_properties.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness
-          - getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_optimality
-          - getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_correctness
-          - getAmount_4626_properties.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
-          - 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
-          - finishedRules4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth