adding 4626

Certora · Jan 13, 2025 · 95d2000 · 95d2000
1 parent bd4fab0
commit 95d2000
Show file tree

Hide file tree

Showing 128 changed files with 5,788 additions and 14,356 deletions.
diff --git a/.github/workflows/certora-GSM-4626.yml b/.github/workflows/certora-GSM-4626.yml
@@ -0,0 +1,71 @@
+name: certora-GSM-4626
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        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 }}
+        env:
+          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 R3a_sellAssetUpdatesAssetBalanceCorrectly 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
+
+
+
+
+
diff --git a/.github/workflows/certora-gho-505.yml b/.github/workflows/certora-gho-505.yml
@@ -15,17 +15,18 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - name: Checkout
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v5
         with: { python-version: 3.9 }
 
       - name: Install java
-        uses: actions/setup-java@v1
-        with: { java-version: '11', java-package: jre }
+        uses: actions/setup-java@v4
+        with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
         run: pip install certora-cli==5.0.5
@@ -42,7 +43,6 @@ jobs:
           touch applyHarness.patch
           make munged
           cd ../..
-          echo "key length" ${#CERTORAKEY}
           certoraRun certora/gho/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}

diff --git a/.github/workflows/certora-gho.yml b/.github/workflows/certora-gho.yml
@@ -15,17 +15,18 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - name: Checkout
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v5
         with: { python-version: 3.9 }
 
       - name: Install java
-        uses: actions/setup-java@v1
-        with: { java-version: '11', java-package: jre }
+        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
@@ -42,7 +43,6 @@ jobs:
           touch applyHarness.patch
           make munged
           cd ../..
-          echo "key length" ${#CERTORAKEY}
           certoraRun certora/gho/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}

diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -16,22 +16,17 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
-      - name: Check key
-        env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
-        run: echo "key length" ${#CERTORAKEY}
-
       - name: Install python
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v5
         with: { python-version: 3.9 }
 
       - name: Install java
-        uses: actions/setup-java@v1
-        with: { java-version: '11', java-package: jre }
+        uses: actions/setup-java@v4
+        with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
         run: pip install certora-cli==6.1.3
@@ -44,8 +39,7 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          echo "key length" ${#CERTORAKEY}
-          certoraRun certora/GSM/conf/${{ matrix.rule }}
+          certoraRun certora/gsm/conf/gsm/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -54,18 +48,18 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - non-4626/Alex-gho-gsm_inverse.conf
-          - non-4626/Alex-gho-gsm.conf
-          - non-4626/balances-buy.conf
-          - non-4626/balances-sell.conf
-          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
-          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
-          - non-4626/Dominik-gho-fixedPriceStrategy.conf
-          - non-4626/fees-buy.conf
-          - non-4626/fees-sell.conf
-          - non-4626/otakar-FixedFeeStrategy.conf
-          - non-4626/Martin-gho-gsm.conf
-          - non-4626/antti-optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
-          - non-4626/otakar-getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
-          - non-4626/otakar-finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
-          - non-4626/otakar-OracleSwapFreezer.conf
+          - gho-gsm_inverse.conf
+          - gho-gsm.conf
+          - balances-buy.conf
+          - balances-sell.conf
+          - gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
+          - gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
+          - gho-fixedPriceStrategy.conf
+          - fees-buy.conf
+          - fees-sell.conf
+          - FixedFeeStrategy.conf
+          - gho-gsm.conf
+          - optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
+          - getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
+          - finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
+          - OracleSwapFreezer.conf
diff --git a/.github/workflows/certora-steward.yml b/.github/workflows/certora-steward.yml
@@ -15,17 +15,18 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - name: Checkout
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v5
         with: { python-version: 3.9 }
 
       - name: Install java
-        uses: actions/setup-java@v1
-        with: { java-version: '11', java-package: jre }
+        uses: actions/setup-java@v4
+        with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
         run: pip install certora-cli
@@ -42,7 +43,6 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          echo "key length" ${#CERTORAKEY}
           certoraRun certora/steward/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}

diff --git a/certora/GSM/conf/non-4626/otakar-getAmount_properties.conf b/certora/GSM/conf/non-4626/otakar-getAmount_properties.conf