merge with main

Certora · Mar 14, 2024 · 1860d13 · 1860d13
2 parents 0aef3de + 3b6810c
commit 1860d13
Show file tree

Hide file tree

Showing 75 changed files with 10,682 additions and 8,416 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
@@ -13,7 +13,6 @@ on:
 jobs:
   verify:
     runs-on: ubuntu-latest
-    #   group: larger
 
     steps:
       - uses: actions/checkout@v2
@@ -37,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-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -1,4 +1,4 @@
-name: certora-GSM
+name: certora-gsm
 
 on:
   push:
@@ -15,7 +15,10 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Check key
         env:
@@ -38,11 +41,7 @@ jobs:
           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}
@@ -69,4 +68,3 @@ jobs:
           - 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/.github/workflows/node.js.yml b/.github/workflows/node.js.yml
@@ -6,6 +6,7 @@ jobs:
       group: larger
     env:
       ALCHEMY_KEY: '${{secrets.ALCHEMY_KEY}}'
+      ETH_RPC_URL: 'https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
     strategy:
       matrix:
         node-version:
@@ -18,7 +19,11 @@ jobs:
       - name: Setup node
         uses: actions/setup-node@v3
         with:
-          node-version: 16.x.x
+          node-version: 18.x.x
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
       - name: Install Dependencies
         run: npm ci
       - name: Compilation

diff --git a/sync-issue.yml → .github/workflows/sync-issue.yml b/sync-issue.yml → .github/workflows/sync-issue.yml
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,5 @@
 /cache
+/cache_forge
 /out
 /artifacts
 /.env
@@ -14,9 +15,9 @@
 /src/contracts/hardhat-dependency-compiler
 
 .DS_Store
-forge-cache
+
 /report
 lcov.info
 combined-lcov.info
 
-broadcast/
+/broadcast
diff --git a/.gitmodules b/.gitmodules
@@ -11,3 +11,18 @@
 [submodule "lib/solidity-utils"]
 	path = lib/solidity-utils
 	url = https://github.com/bgd-labs/solidity-utils
+[submodule "lib/aave-v3-core"]
+	path = lib/aave-v3-core
+	url = https://github.com/aave/aave-v3-core
+[submodule "lib/aave-token"]
+	path = lib/aave-token
+	url = https://github.com/aave/aave-token
+[submodule "lib/aave-v3-periphery"]
+	path = lib/aave-v3-periphery
+	url = https://github.com/aave/aave-v3-periphery
+[submodule "lib/safety-module"]
+	path = lib/safety-module
+	url = https://github.com/aave/safety-module
+[submodule "lib/openzeppelin-contracts"]
+	path = lib/openzeppelin-contracts
+	url = https://github.com/OpenZeppelin/openzeppelin-contracts
diff --git a/.prettierignore b/.prettierignore
@@ -4,7 +4,6 @@ node_modules
 types
 out
 deployments
-temp-artifacts
 lib
 coverage
-forge-cache
+cache_forge
diff --git a/.solcover.js b/.solcover.js
@@ -1,5 +1,5 @@
 module.exports = {
-  skipFiles: [],
+  skipFiles: ['./script', './test'],
   mocha: {
     enableTimeouts: false,
   },

diff --git a/README.md b/README.md
@@ -39,19 +39,20 @@ You can find all audit reports under the [audits](./audits/) folder
 - [2022-08-12 - OpenZeppelin](./audits/2022-08-12_Openzeppelin-v1.pdf)
 - [2022-11-10 - OpenZeppelin](./audits/2022-11-10_Openzeppelin-v2.pdf)
 - [2023-03-01 - ABDK](./audits/2023-03-01_ABDK.pdf)
-- [2023-03-07 - Sigma Prime](./audits/2023-03-07_SigmaPrime.pdf)
 - [2023-02-28 - Certora Formal Verification](./certora/reports/Aave_Gho_Formal_Verification_Report.pdf)
 - [2023-07-06 - Sigma Prime](./audits/2023-07-06_SigmaPrime.pdf)
 - [2023-06-13 - Sigma Prime (GhoSteward)](./audits/2023-06-13_GhoSteward_SigmaPrime.pdf)
 - [2023-09-20 - Emanuele Ricci @Stermi (GHO Stability Module)](./audits/2023-09-20_GSM_Stermi.pdf)
 - [2023-10-23 - Sigma Prime (GHO Stability Module)](./audits/2023-10-23_GSM_SigmaPrime.pdf)
+- [2023-12-07 - Certora Formal Verification (GHO Stability Module)](./certora/reports/Formal_Verification_Report_of_GHO_Stability_Module.pdf)
 
 ## Getting Started
 
 Clone the repository and run the following command to install dependencies:
 
 ```sh
 npm i
+forge i
 ```
 
 If you need to interact with GHO in the Goerli testnet, provide your Alchemy API key and mnemonic in the `.env` file:

diff --git a/audits/2023-03-07_SigmaPrime.pdf b/audits/2023-03-07_SigmaPrime.pdf
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",
-        "node_modules/@openzeppelin/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,12 +7,17 @@
         "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",
+        "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-assetToGhoInvertibility.conf b/certora/GSM/conf/non-4626/Dominik-gho-assetToGhoInvertibility.conf
@@ -7,16 +7,18 @@
         "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"
+        "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",
     ],
-//    "rule" : [
-//       "buyAssetInverse_all","sellAssetInverse_all"
-//    ],
     "assert_autofinder_success": true,
     "optimistic_loop":true,
     "loop_iter":"1",

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",
-        "node_modules/@openzeppelin/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",
-        "node_modules/@openzeppelin/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",
-        "node_modules/@openzeppelin/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",
-        "node_modules/@openzeppelin/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",
-        "node_modules/@openzeppelin/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",
-        "node_modules/@openzeppelin/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,
@@ -30,10 +35,5 @@
         "-smt_nonLinearArithmetic true",
     ],
     "verify":
-        "GsmHarness:certora/GSM/specs/gsm/fees-sell.spec",
-//        "GsmHarness:certora/GSM/specs/gsm/fees-sell-R3.spec",
-//    "rule": [
-//        "R3_10",
-//        "R3_11",
-//    ],
+        "GsmHarness:certora/GSM/specs/gsm/fees-sell.spec"
 }