Merge pull request #673 from morpho-org/certora/update-cvl-7.0.7

[Certora] Update CVL version 7.0.7
morpho-org · Mar 22, 2024 · e262e84 · e262e84
2 parents 8fd9262 + 34c7194
commit e262e84
Show file tree

Hide file tree

Showing 14 changed files with 21 additions and 17 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -43,7 +43,7 @@ jobs:
         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/solc
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Verify ${{ matrix.conf }}
         run: certoraRun certora/confs/${{ matrix.conf }}.conf

diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
     "prover_args": [
         "-depth 3",

diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf
@@ -2,12 +2,14 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/ExactMath.spec",
     "rule_sanity": "basic",
     "prover_args": [
         "-depth 3",
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30",
+        "-timeout 3600",
     ],
     "server": "production",
     "msg": "Morpho Blue Exact Math"

diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf
@@ -3,6 +3,7 @@
         "certora/harness/MorphoHarness.sol",
         "src/mocks/OracleMock.sol"
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Health.spec",
     "rule_sanity": "basic",
     "prover_args": [

diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoInternalAccess.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/RatioMath.spec",
     "rule_sanity": "basic",
     "prover_args": [

diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
     "rule_sanity": "basic",
     "prover_args": [

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Reverts.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf
@@ -5,6 +5,7 @@
         "certora/dispatch/ERC20USDT.sol",
         "certora/dispatch/ERC20NoRevert.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "TransferHarness:certora/specs/Transfer.spec",
     "rule_sanity": "basic",
     "server": "production",

diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -46,24 +46,24 @@ persistent ghost mapping(address => mathint) idleAmount {
     init_state axiom (forall address token. idleAmount[token] == 0);
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) {
     sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares;
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) {
     sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares;
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
     idleAmount[toMarketParams(id).collateralToken] = idleAmount[toMarketParams(id).collateralToken] - oldAmount + newAmount;
 }
 
-hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) {
     idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] - oldAmount + newAmount;
 }
 
-hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) {
     idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] + oldAmount - newAmount;
 }
 
@@ -107,11 +107,7 @@ invariant hashOfMarketParamsOf(MorphoHarness.Id id)
 // This invariant is useful in the following rule, to link an id back to a market.
 invariant marketParamsOfHashOf(MorphoHarness.MarketParams marketParams)
     isCreated(libId(marketParams)) =>
-    toMarketParams(libId(marketParams)).loanToken == marketParams.loanToken &&
-    toMarketParams(libId(marketParams)).collateralToken == marketParams.collateralToken &&
-    toMarketParams(libId(marketParams)).oracle == marketParams.oracle &&
-    toMarketParams(libId(marketParams)).lltv == marketParams.lltv &&
-    toMarketParams(libId(marketParams)).irm == marketParams.irm;
+    toMarketParams(libId(marketParams)) == marketParams;
 
 // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow.
 invariant idleAmountLessThanBalance(address token)
@@ -167,11 +163,7 @@ rule libIdUnique() {
     // Assume that arguments are the same.
     require libId(marketParams1) == libId(marketParams2);
 
-    assert marketParams1.loanToken == marketParams2.loanToken;
-    assert marketParams1.collateralToken == marketParams2.collateralToken;
-    assert marketParams1.oracle == marketParams2.oracle;
-    assert marketParams1.irm == marketParams2.irm;
-    assert marketParams1.lltv == marketParams2.lltv;
+    assert marketParams1 == marketParams2;
 }
 
 // Check that only the user is able to change who is authorized to manage his position.

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
@@ -27,7 +27,7 @@ persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral
 {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
 }