ci: Fix certora ci config files

aave · Feb 19, 2024 · 5e3e080 · 5e3e080
1 parent ec5bd09
commit 5e3e080
Show file tree

Hide file tree

Showing 17 changed files with 114 additions and 62 deletions.
diff --git a/.github/workflows/certora-gho-505.yml b/.github/workflows/certora-gho-505.yml
@@ -36,10 +36,6 @@ jobs:
           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: |
           cd certora/gho

diff --git a/.github/workflows/certora-gho.yml b/.github/workflows/certora-gho.yml
@@ -37,10 +37,6 @@ jobs:
           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: |
           cd certora/gho

diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -42,10 +42,6 @@ jobs:
           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}

diff --git a/certora/GSM/conf/non-4626/Alex-gho-gsm.conf b/certora/GSM/conf/non-4626/Alex-gho-gsm.conf
@@ -7,12 +7,17 @@
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "parametric_contracts": [ "GsmHarness"],
     "assert_autofinder_success": true,

diff --git a/certora/GSM/conf/non-4626/Alex-gho-gsm_inverse.conf b/certora/GSM/conf/non-4626/Alex-gho-gsm_inverse.conf
@@ -7,17 +7,17 @@
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "certora/GSM/harness/ERC20Helper.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
     ],
     "link": [
         "GsmHarness:GHO_TOKEN=GhoToken",
         "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
         "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
     ],
     "packages": [
-        "@aave/core-v3/=certora/munged/lib/aave-v3-core/",
-        "@aave/periphery-v3/=certora/munged/lib/aave-v3-periphery/",
-        "@openzeppelin/=certora/munged/lib/openzeppelin-contracts/"
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/Dominik-gho-assetToGhoInvertibility.conf b/certora/GSM/conf/non-4626/Dominik-gho-assetToGhoInvertibility.conf
@@ -7,12 +7,17 @@
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol"
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness"
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness"
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/Dominik-gho-fixedPriceStrategy.conf b/certora/GSM/conf/non-4626/Dominik-gho-fixedPriceStrategy.conf
@@ -1,7 +1,12 @@
 {
     "files": [
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol"
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/Martin-gho-gsm.conf b/certora/GSM/conf/non-4626/Martin-gho-gsm.conf
@@ -9,10 +9,16 @@
         "src/contracts/gho/GhoToken.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
-    "GsmHarness:UNDERLYING_ASSET=DummyERC20B"
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:UNDERLYING_ASSET=DummyERC20B"
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "parametric_contracts": [ "GsmHarness"],
     "assert_autofinder_success": true,

diff --git a/certora/GSM/conf/non-4626/antti-optimality.conf b/certora/GSM/conf/non-4626/antti-optimality.conf
@@ -7,13 +7,18 @@
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
     ],
     "link": [
         "GsmHarness:GHO_TOKEN=GhoToken",
         "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
         "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
     ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
+    ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,
     "rule_sanity" : "basic",

diff --git a/certora/GSM/conf/non-4626/balances-buy.conf b/certora/GSM/conf/non-4626/balances-buy.conf
@@ -5,14 +5,19 @@
         "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",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+        "src/contracts/gho/GhoToken.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/balances-sell.conf b/certora/GSM/conf/non-4626/balances-sell.conf
@@ -5,14 +5,19 @@
         "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",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+        "src/contracts/gho/GhoToken.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/fees-buy.conf b/certora/GSM/conf/non-4626/fees-buy.conf
@@ -5,14 +5,19 @@
         "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",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+        "src/contracts/gho/GhoToken.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/fees-sell.conf b/certora/GSM/conf/non-4626/fees-sell.conf
@@ -5,14 +5,19 @@
         "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",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+        "src/contracts/gho/GhoToken.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/otakar-FixedFeeStrategy.conf b/certora/GSM/conf/non-4626/otakar-FixedFeeStrategy.conf
@@ -1,7 +1,12 @@
 {
     "files": [
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/otakar-OracleSwapFreezer.conf b/certora/GSM/conf/non-4626/otakar-OracleSwapFreezer.conf
@@ -2,7 +2,12 @@
     "files": [
         "certora/GSM/harness/OracleSwapFreezerHarness.sol",
         "src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezer.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,

diff --git a/certora/GSM/conf/non-4626/otakar-finishedRules.conf b/certora/GSM/conf/non-4626/otakar-finishedRules.conf
@@ -7,12 +7,17 @@
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,
@@ -27,8 +32,6 @@
     "prover_args": [
         "-copyLoopUnroll 6",
         "-depth 20",
-//        "-newSplitParallel true",
-//        "-smt_hashingScheme plainInjectivity",
     ],
     "verify":
         "GsmHarness:certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec",

diff --git a/certora/GSM/conf/non-4626/otakar-getAmount_properties.conf b/certora/GSM/conf/non-4626/otakar-getAmount_properties.conf
@@ -7,12 +7,17 @@
         "certora/GSM/harness/FixedPriceStrategyHarness.sol",
         "certora/GSM/harness/FixedFeeStrategyHarness.sol",
         "src/contracts/gho/GhoToken.sol",
-        "lib/openzeppelin-contracts/contracts/utils/math/Math.sol",
     ],
     "link": [
-    "GsmHarness:GHO_TOKEN=GhoToken",
-    "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
-    "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+        "GsmHarness:GHO_TOKEN=GhoToken",
+        "GsmHarness:PRICE_STRATEGY=FixedPriceStrategyHarness",
+        "GsmHarness:_feeStrategy=FixedFeeStrategyHarness",
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token"
+        "@openzeppelin/=lib/openzeppelin-contracts"
     ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,