[Certora] Dev

.gitignore

@@ -16,6 +16,9 @@ docs/
 # Node modules
 /node_modules
 
+# Certora
+.certora**
+
 # Hardhat
 /types
 /cache_hardhat

certora/harness/MorphoHarness.sol

@@ -0,0 +1,28 @@
+pragma solidity 0.8.19;
+
+import "../../src/Morpho.sol";
+import "../../src/libraries/SharesMathLib.sol";
+
+contract MorphoHarness is Morpho {
+    constructor(address newOwner) Morpho(newOwner) {}
+
+    function getVirtualTotalSupply(Id id) external view returns (uint256) {
+        return totalSupply[id] + SharesMathLib.VIRTUAL_ASSETS;
+    }
+
+    function getVirtualTotalSupplyShares(Id id) external view returns (uint256) {
+        return totalSupplyShares[id] + SharesMathLib.VIRTUAL_SHARES;
+    }
+
+    function getTotalSupply(Id id) external view returns (uint256) {
+        return totalSupply[id];
+    }
+
+    function getTotalSupplyShares(Id id) external view returns (uint256) {
+        return totalSupplyShares[id];
+    }
+
+    function getTotalBorrowShares(Id id) external view returns (uint256) {
+        return totalBorrowShares[id];
+    }
+}

certora/scripts/verifyBlue.sh

@@ -0,0 +1,11 @@
+#!/bin/sh
+
+certoraRun \
+    certora/harness/MorphoHarness.sol \
+    --verify MorphoHarness:certora/specs/Blue.spec \
+    --solc_allow_path src \
+    --loop_iter 3 \
+    --optimistic_loop \
+    --msg "Morpho Blue" \
+    --send_only \
+    "$@"

certora/specs/Blue.spec

@@ -0,0 +1,70 @@
+methods {
+    function supply(MorphoHarness.Market, uint256, uint256, address, bytes) external;
+    function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
+    function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function getTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
+    function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+
+    function _.borrowRate(MorphoHarness.Market) external => DISPATCHER(true);
+
+    // function _.safeTransfer(address, uint256) internal => DISPATCHER(true);
+    // function _.safeTransferFrom(address, address, uint256) internal => DISPATCHER(true);
+}
+
+ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares
+{
+    init_state axiom (forall MorphoHarness.Id id. sumSupplyShares[id] == 0);
+}
+ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares
+{
+    init_state axiom (forall MorphoHarness.Id id. sumBorrowShares[id] == 0);
+}
+ghost mapping(MorphoHarness.Id => mathint) sumCollateral
+{
+    init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
+}
+
+hook Sstore supplyShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE {
+    sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares;
+}
+
+hook Sstore borrowShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE {
+    sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares;
+}
+
+hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAmount (uint256 oldAmount) STORAGE {
+    sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
+}
+
+invariant sumSupplySharesCorrect(MorphoHarness.Id id)
+    to_mathint(getTotalSupplyShares(id)) == sumSupplyShares[id];
+invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
+    to_mathint(getTotalBorrowShares(id)) == sumBorrowShares[id];
+
+rule whatDoesNotIncreaseRatio(MorphoHarness.Id id) {
+    mathint assetsBefore = getVirtualTotalSupply(id);
+    mathint sharesBefore = getVirtualTotalSupplyShares(id);
+
+    method f;
+    env e;
+    calldataarg args;
+
+    f(e,args);
+
+    mathint assetsAfter = getVirtualTotalSupply(id);
+    mathint sharesAfter = getVirtualTotalSupplyShares(id);
+
+    // check if assetsBefore/shareBefore <= assetsAfter / sharesAfter;
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+}
+
+
+rule supplyRevertZero(MorphoHarness.Market market) {
+    env e;
+    bytes b;
+
+    supply@withrevert(e, market, 0, 0, e.msg.sender, b);
+
+    assert lastReverted;
+}

src/Morpho.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: UNLICENSED
-pragma solidity 0.8.21;
+pragma solidity 0.8.19;
 
 import "./interfaces/IMorpho.sol";
 import "./interfaces/IMorphoCallbacks.sol";