Merge pull request #545 from morpho-org/certora/configuration-files

[Certora] Use configuration files

.github/workflows/certora.yml

@@ -22,34 +22,34 @@ jobs:
           python-version: "3.10"
 
       - name: Install certora
-        run: pip install certora-cli-beta
+        run: pip install certora-cli
 
       - name: Install solc
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
+          sudo mv solc-static-linux /usr/local/bin/solc
 
       - name: Verify rule ${{ matrix.script }}
         run: |
           echo "key length" ${#CERTORAKEY}
-          bash certora/scripts/${{ matrix.script }} --solc solc8.19
+          certoraRun certora/configuration/${{ matrix.conf }}.conf
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
     strategy:
       fail-fast: false
 
       matrix:
-        script:
-          - verifyAccrueInterest.sh
-          - verifyConsistentState.sh
-          - verifyExactMath.sh
-          - verifyExitLiquidity.sh
-          - verifyHealth.sh
-          - verifyLibSummary.sh
-          - verifyLiveness.sh
-          - verifyRatioMath.sh
-          - verifyReentrancy.sh
-          - verifyReverts.sh
-          - verifyTransfer.sh
+        conf:
+          - AccrueInterest
+          - ConsistentState
+          - ExactMath
+          - ExitLiquidity
+          - Health
+          - LibSummary
+          - Liveness
+          - RatioMath
+          - Reentrancy
+          - Reverts
+          - Transfer

certora/configuration/AccrueInterest.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity",
+        "-mediumTimeout 30"
+    ],
+    "msg": "Morpho Blue Accrue Interest"
+}

certora/configuration/ConsistentState.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
+    "msg": "Morpho Blue Consistent State"
+}

certora/configuration/ExactMath.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ExactMath.spec",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity",
+        "-mediumTimeout 30"
+    ],
+    "msg": "Morpho Blue Exact Math"
+}

certora/configuration/ExitLiquidity.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec",
+    "msg": "Morpho Blue Exit Liquidity"
+}

certora/configuration/Health.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol",
+        "src/mocks/OracleMock.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Health.spec",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity"
+    ],
+    "msg": "Morpho Blue Health"
+}

certora/configuration/LibSummary.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "msg": "Morpho Blue Lib Summary",
+    "process": "emv",
+    "verify": "MorphoHarness:certora/specs/LibSummary.spec"
+}

certora/configuration/Liveness.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harness/MorphoInternalAccess.sol"
+    ],
+    "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
+    "msg": "Morpho Blue Liveness"
+}

certora/configuration/RatioMath.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/RatioMath.spec",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity"
+    ],
+    "msg": "Morpho Blue Ratio Math"
+}

certora/configuration/Reentrancy.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
+    "prover_args": [
+        "-enableStorageSplitting false"
+    ],
+    "msg": "Morpho Blue Reentrancy"
+}

certora/configuration/Reverts.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Reverts.spec",
+    "msg": "Morpho Blue Reverts"
+}

certora/configuration/Transfer.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harness/TransferHarness.sol",
+        "certora/dispatch/ERC20Standard.sol",
+        "certora/dispatch/ERC20USDT.sol",
+        "certora/dispatch/ERC20NoRevert.sol"
+    ],
+    "verify": "TransferHarness:certora/specs/Transfer.spec",
+    "msg": "Morpho Blue Transfer"
+}