Merge branch 'main' into ci/invariant

.github/workflows/certora.yml

@@ -20,21 +20,24 @@ jobs:
           - AssetsAccounting
           - ConsistentState
           - ExactMath
+          - ExchangeRate
           - Health
           - LibSummary
           - Liveness
-          - RatioMath
           - Reentrancy
           - Reverts
+          - StayHealthy
           - Transfer
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.9"
 
       - name: Install certora
         run: pip install certora-cli
@@ -43,7 +46,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

.github/workflows/halmos.yml

@@ -0,0 +1,31 @@
+name: Halmos
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.9"
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install halmos
+        run: pip install halmos
+
+      - name: Run Halmos
+        run: FOUNDRY_PROFILE=test halmos

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes.git

certora/README.md

@@ -1,6 +1,6 @@
 This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language.
 
-The core concepts of the the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf).
+The core concepts of the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf).
 These concepts have been verified using CVL.
 We first give a [high-level description](#high-level-description) of the verification and then describe the [folder and file structure](#folder-and-file-structure) of the specification files.
 
@@ -11,7 +11,7 @@ The Morpho Blue protocol allows users to take out collateralized loans on ERC20
 ## ERC20 tokens and transfers
 
 For a given market, Morpho Blue relies on the fact that the tokens involved respect the ERC20 standard.
-In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if its the recipient or the sender) of the amount transferred.
+In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if it's the recipient or the sender) of the amount transferred.
 
 The file [Transfer.spec](specs/Transfer.spec) defines a summary of the transfer functions.
 This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected.
@@ -33,7 +33,7 @@ The verification is done for the most common implementations of the ERC20 standa
 
 - [ERC20Standard](dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance.
 - [ERC20NoRevert](dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead).
-- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions.
+- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respect the standard because it omits the return value of the `transfer` and `transferFrom` functions.
 
 Additionally, Morpho Blue always goes through a custom transfer library to handle ERC20 tokens, notably in all the above cases.
 This library reverts when the transfer is not successful, and this is checked for the case of insufficient funds or insufficient allowance.
@@ -69,11 +69,11 @@ Said otherwise, markets are independent: tokens from a given market cannot be im
 
 When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
 Shares increase in value as interest is accrued.
-The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest.
-The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement.
+The share mechanism is implemented symmetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest.
+The rule `accrueInterestIncreasesSupplyExchangeRate` checks this property for the supply side with the following statement.
 
 ```soldidity
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 ```
 
@@ -107,7 +107,7 @@ invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
     borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;
 ```
 
-More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty).
+More generally, this means that the result of liquidating a position multiple times eventually leads to a healthy position (possibly empty).
 
 ## Authorization
 
@@ -205,7 +205,7 @@ As an example, the `withdrawChangesTokensAndShares` rule checks that calling the
 Other liveness properties are verified as well.
 Notably, it's also verified that it is always possible to exit a position without concern for the oracle.
 This is done through the verification of two rules: the `canRepayAll` rule and the `canWithdrawCollateralAll` rule.
-The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any oustanding debt.
+The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any outstanding debt.
 The `canWithdrawCollateralAll` rule ensures that in the case where the account has no outstanding debt, then it is possible to withdraw the full collateral.
 
 ## Protection against common attack vectors
@@ -214,7 +214,7 @@ Other common and known attack vectors are verified to not be possible on the Mor
 
 ### Reentrancy
 
-Reentrancy is a common attack vector that happen when a call to a contract allows, when in a temporary state, to call the same contract again.
+Reentrancy is a common attack vector that happens when a call to a contract allows, when in a temporary state, to call the same contract again.
 The state of the contract usually refers to the storage variables, which can typically hold values that are meant to be used only after the full execution of the current function.
 The Morpho Blue contract is verified to not be vulnerable to this kind of reentrancy attack thanks to the rule `reentrancySafe`.
 
@@ -250,12 +250,13 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division.
   Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start.
 - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions.
-  Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism).
+  Notably, debt positions always have some collateral thanks to the bad debt realization mechanism.
 - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.
 - [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
-- [`RatioMath.spec`](specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time.
+- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
 - [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
+- [`StayHealthy.spec`](specs/Health.spec) checks that functions cannot render an account unhealthy.
 - [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.

certora/confs/AccrueInterest.conf

@@ -1,14 +1,16 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
-    "prover_args": [
-        "-depth 3",
-        "-smt_hashingScheme plaininjectivity",
-        "-mediumTimeout 30",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "Morpho Blue Accrue Interest"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 30",
+    "-smt_hashingScheme plaininjectivity"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Accrue Interest"
 }

certora/confs/AssetsAccounting.conf

@@ -1,9 +1,11 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "Morpho Blue Assets Accounting"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Assets Accounting"
 }

certora/confs/ConsistentState.conf

@@ -1,9 +1,11 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "Morpho Blue Consistent State"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Consistent State"
 }

certora/confs/ExactMath.conf

@@ -1,14 +1,19 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/ExactMath.spec",
-    "rule_sanity": "basic",
-    "prover_args": [
-        "-depth 3",
-        "-smt_hashingScheme plaininjectivity",
-        "-mediumTimeout 30",
-    ],
-    "server": "production",
-    "msg": "Morpho Blue Exact Math"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/ExactMath.spec",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 5",
+    "-timeout 3600",
+    "-adaptiveSolverConfig false",
+    "-smt_nonLinearArithmetic true",
+    "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Exact Math"
 }

certora/confs/ExchangeRate.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/ExchangeRate.spec",
+  "prover_args": [
+    "-smt_hashingScheme plaininjectivity",
+    "-smt_easy_LIA true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Exchange Rate"
+}

certora/confs/Health.conf

@@ -1,13 +1,15 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-        "src/mocks/OracleMock.sol"
-    ],
-    "verify": "MorphoHarness:certora/specs/Health.spec",
-    "rule_sanity": "basic",
-    "prover_args": [
-        "-smt_hashingScheme plaininjectivity",
-    ],
-    "server": "production",
-    "msg": "Morpho Blue Health"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol",
+    "src/mocks/OracleMock.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/Health.spec",
+  "prover_args": [
+    "-smt_hashingScheme plaininjectivity"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Health"
 }

certora/confs/LibSummary.conf

@@ -1,9 +1,14 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/LibSummary.spec",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "Morpho Blue Lib Summary"
+  "files": [
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/LibSummary.spec",
+  "prover_args": [
+    "-smt_bitVectorTheory true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Lib Summary"
 }

certora/confs/Liveness.conf

@@ -1,9 +1,11 @@
 {
-    "files": [
-        "certora/harness/MorphoInternalAccess.sol",
-    ],
-    "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "Morpho Blue Liveness"
+  "files": [
+    "certora/harness/MorphoInternalAccess.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Liveness"
 }

certora/confs/Reentrancy.conf

@@ -1,12 +1,13 @@
 {
-    "files": [
-        "certora/harness/MorphoHarness.sol",
-    ],
-    "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
-    "rule_sanity": "basic",
-    "prover_args": [
-        "-enableStorageSplitting false",
-    ],
-    "server": "production",
-    "msg": "Morpho Blue Reentrancy"
+  "files": [
+    "certora/harness/MorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
+  "prover_args": [
+    "-enableStorageSplitting false"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Reentrancy"
 }