Certora GSM Review

Certora · Jan 29, 2024 · 0750d1f · 0750d1f
1 parent afee515
commit 0750d1f
Show file tree

Hide file tree

Showing 122 changed files with 17,048 additions and 137 deletions.
diff --git a/.github/workflows/certora-latest.yml → .github/workflows/certora-gho-505.yml b/.github/workflows/certora-latest.yml → .github/workflows/certora-gho-505.yml
@@ -1,4 +1,4 @@
-name: certora-latest
+name: certora-gho-5.0.5
 
 on:
   push:
@@ -42,12 +42,12 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          cd certora
+          cd certora/gho
           touch applyHarness.patch
           make munged
-          cd ..
+          cd ../..
           echo "key length" ${#CERTORAKEY}
-          certoraRun certora/conf/${{ matrix.rule }}
+          certoraRun certora/gho/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 

diff --git a/.github/workflows/certora.yml → .github/workflows/certora-gho.yml b/.github/workflows/certora.yml → .github/workflows/certora-gho.yml
@@ -1,4 +1,4 @@
-name: certora
+name: certora-gho
 
 on:
   push:
@@ -12,8 +12,8 @@ on:
 
 jobs:
   verify:
-    runs-on:
-      group: larger
+    runs-on: ubuntu-latest
+    #   group: larger
 
     steps:
       - uses: actions/checkout@v2
@@ -43,12 +43,12 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          cd certora
+          cd certora/gho
           touch applyHarness.patch
           make munged
-          cd ..
+          cd ../..
           echo "key length" ${#CERTORAKEY}
-          certoraRun certora/conf/${{ matrix.rule }}
+          certoraRun certora/gho/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 

diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -0,0 +1,72 @@
+name: certora-gsm
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Check key
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+        run: echo "key length" ${#CERTORAKEY}
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: '11', java-package: jre }
+
+      - name: Install certora cli
+        run: pip install certora-cli==6.1.3
+
+      - 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: Install node dependencies
+        run: |
+          npm i
+      
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          echo "key length" ${#CERTORAKEY}
+          certoraRun certora/GSM/conf/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      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 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
+
diff --git a/certora/GSM/conf/non-4626/Alex-gho-gsm.conf b/certora/GSM/conf/non-4626/Alex-gho-gsm.conf
@@ -0,0 +1,33 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/ERC20Helper.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol",
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "parametric_contracts": [ "GsmHarness"],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "optimistic_hashing":true,
+    "rule_sanity" : "basic",
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "GSM properties",
+    "smt_timeout": "7200",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20"
+    ],
+    "verify": 
+        "GsmHarness:certora/GSM/specs/gsm/Alex-gho-gsm.spec",
+}
diff --git a/certora/GSM/conf/non-4626/Alex-gho-gsm_inverse.conf b/certora/GSM/conf/non-4626/Alex-gho-gsm_inverse.conf
@@ -0,0 +1,32 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "certora/GSM/harness/ERC20Helper.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol",
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "rule_sanity" : "basic",
+    "msg": "GSM properties",
+    "smt_timeout": "7200",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20"
+    ],
+    "verify": 
+        "GsmHarness:certora/GSM/specs/gsm/Alex-gho-gsm_inverse.spec",
+}
diff --git a/certora/GSM/conf/non-4626/Dominik-gho-assetToGhoInvertibility.conf b/certora/GSM/conf/non-4626/Dominik-gho-assetToGhoInvertibility.conf
@@ -0,0 +1,33 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/ERC20Helper.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol"
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness"
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "optimistic_hashing":true,
+    "rule_sanity" : "basic",
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "GSM getAsset/GhoAmountForBuy/SellAsset invertibility rules",
+    "smt_timeout": "7200",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20"
+    ],
+    "multi_assert_check": true,
+    "verify": 
+        "GsmHarness:certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec",
+}
diff --git a/certora/GSM/conf/non-4626/Dominik-gho-fixedPriceStrategy.conf b/certora/GSM/conf/non-4626/Dominik-gho-fixedPriceStrategy.conf
@@ -0,0 +1,22 @@
+{
+    "files": [
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol"
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "GSM4626 - getAssetAmountInGho and getGhoAmountInAsset are inverse",
+    "smt_timeout": "7200",
+    "rule_sanity" : "basic",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20"
+    ],
+    "multi_assert_check": true,
+    "verify": 
+        "FixedPriceStrategyHarness:certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec",
+}
diff --git a/certora/GSM/conf/non-4626/Martin-gho-gsm.conf b/certora/GSM/conf/non-4626/Martin-gho-gsm.conf
@@ -0,0 +1,33 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "certora/GSM/harness/ERC20Helper.sol:ERC20Helper",
+        "src/contracts/gho/GhoToken.sol",
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    "GsmHarness:UNDERLYING_ASSET=DummyERC20B"
+    ],
+    "parametric_contracts": [ "GsmHarness"],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "rule_sanity" : "basic",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "GSM properties",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20",
+        "-smt_hashingScheme plainInjectivity"
+    ],
+    "verify": 
+        "GsmHarness:certora/GSM/specs/gsm/Martin-gho-gsm.spec",
+}
diff --git a/certora/GSM/conf/non-4626/antti-optimality.conf b/certora/GSM/conf/non-4626/antti-optimality.conf
@@ -0,0 +1,32 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/ERC20Helper.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol",
+    ],
+    "link": [
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "rule_sanity" : "basic",
+    "loop_iter":"1",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "optimality of buyAsset - multi_assert",
+    "multi_assert_check": true,
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20"
+    ],
+    "verify":
+        "GsmHarness:certora/GSM/specs/gsm/optimality_antti.spec",
+}
diff --git a/certora/GSM/conf/non-4626/balances-buy.conf b/certora/GSM/conf/non-4626/balances-buy.conf
@@ -0,0 +1,31 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "certora/GSM/harness/DiffHelper.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol",
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "rule_sanity" : "basic",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "balances - buy",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20",
+    ],
+    "verify":
+        "GsmHarness:certora/GSM/specs/gsm/balances-buy.spec",
+}
diff --git a/certora/GSM/conf/non-4626/balances-sell.conf b/certora/GSM/conf/non-4626/balances-sell.conf
@@ -0,0 +1,31 @@
+{
+    "files": [
+        "certora/GSM/harness/GsmHarness.sol",
+        "certora/GSM/harness/DummyERC20A.sol",
+        "certora/GSM/harness/DummyERC20B.sol",
+        "certora/GSM/harness/FixedPriceStrategyHarness.sol",
+        "certora/GSM/harness/FixedFeeStrategyHarness.sol",
+        "src/contracts/gho/GhoToken.sol",
+        "certora/GSM/harness/DiffHelper.sol",
+        "node_modules/@openzeppelin/contracts/utils/math/Math.sol",
+    ],
+    "link": [
+    "GsmHarness:GHO_TOKEN=GhoToken",
+    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+    "loop_iter":"1",
+    "rule_sanity" : "basic",
+    "optimistic_hashing":true,
+    "hashing_length_bound":"416",
+    "solc": "solc8.10",
+    "msg": "balances - sell",
+    "prover_args": [
+        "-copyLoopUnroll 6",
+        "-depth 20",
+    ],
+    "verify":
+        "GsmHarness:certora/GSM/specs/gsm/balances-sell.spec",
+}