test: more tests

.github/workflows/certora.yml

@@ -30,7 +30,8 @@ jobs:
           - Roles
           - Timelock
           - Tokens
-          - Hole
+          - HoleNoLink
+          - HoleLink
 
     steps:
       - uses: actions/checkout@v4

certora/confs/HoleLink.conf

@@ -0,0 +1,26 @@
+{
+    "files": [
+        "certora/helpers/MetaMorphoHarness.sol",
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    ],
+    "solc_map": {
+        "MetaMorphoHarness": "solc-0.8.21",
+        "MorphoHarness": "solc-0.8.19"
+    },
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "verify": "MetaMorphoHarness:certora/specs/HoleLink.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+        "-superOptimisticReturnsize true",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Hole Link",
+}
+

certora/confs/Hole.conf → certora/confs/HoleNoLink.conf

@@ -5,7 +5,7 @@
     "solc_map": {
         "MetaMorphoHarness": "solc-0.8.21",
     },
-    "verify": "MetaMorphoHarness:certora/specs/Hole.spec",
+    "verify": "MetaMorphoHarness:certora/specs/HoleNoLink.spec",
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
@@ -16,5 +16,5 @@
     ],
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "MetaMorpho Hole",
+    "msg": "MetaMorpho Hole No Link",
 }

certora/specs/HoleLink.spec

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    // TODO: why do we need to do this?
+    function multicall(bytes[]) external returns(bytes[]) => NONDET DELETE;
+
+    // We assume that the following functions are envfree, meaning don't depend on 
+    // tx, sender and block.
+    function hole() external returns(uint256) envfree;
+    function totalAssets() external returns(uint256) envfree;
+    function totalSupply() external returns(uint256) envfree;
+    function lastTotalAssets() external returns(uint256) envfree;
+
+    // Assume that it's a constant.
+    function DECIMALS_OFFSET() external returns(uint8) => CONSTANT;
+
+    // We assume that the erc20 is view. It's ok as we don't care about what happens in the token.
+    function _.transfer(address, uint256) external => NONDET;
+    function _.transferFrom(address, address, uint256) external => NONDET;
+    function _.balanceOf(address) external => NONDET;
+
+    // We assume that the borrow rate is view.
+    function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => NONDET;
+
+    // We deactivate callbacks. 
+    // Ideally we can assume that they can't change arbitrarily the storage of Morpho 
+    // and Metamorpho, but can only reenter through public entry-points, but I don't 
+    // know how to do this.
+    function _.onMorphoSupply(uint256, bytes) external => NONDET;
+    function _.onMorphoRepay(uint256, bytes) external => NONDET;
+    function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET;
+    function _.onMorphoLiquidate(uint256, bytes) external => NONDET;
+    function _.onMorphoFlashLoan(uint256, bytes) external => NONDET;
+}
+
+// TODO: this rule is timing out
+invariant holeSmallerThanLastTotalAssets()
+    hole() <= lastTotalAssets();

certora/specs/HoleNoLink.spec

@@ -0,0 +1,113 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    // TODO: why do we need to do this?
+    function multicall(bytes[]) external returns(bytes[]) => NONDET DELETE;
+
+    // We assume that the following functions are envfree, meaning don't depend on 
+    // tx, sender and block.
+    function hole() external returns(uint256) envfree;
+    function totalAssets() external returns(uint256) envfree;
+    function totalSupply() external returns(uint256) envfree;
+    function lastTotalAssets() external returns(uint256) envfree;
+
+    // Assume that it's a constant.
+    function DECIMALS_OFFSET() external returns(uint8) => CONSTANT;
+
+    // We assume that the erc20 is view. It's ok as we don't care about what happens in the token.
+    function _.transfer(address, uint256) external => NONDET;
+    function _.transferFrom(address, address, uint256) external => NONDET;
+    function _.balanceOf(address) external => NONDET;
+
+    // We deactivate callbacks. 
+    // Ideally we can assume that they can't change arbitrarily the storage of Morpho 
+    // and Metamorpho, but can only reenter through public entry-points, but I don't 
+    // know how to do this.
+    function _.onMorphoSupply(uint256, bytes) external => NONDET;
+    function _.onMorphoRepay(uint256, bytes) external => NONDET;
+    function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET;
+    function _.onMorphoLiquidate(uint256, bytes) external => NONDET;
+    function _.onMorphoFlashLoan(uint256, bytes) external => NONDET;
+}
+
+rule holeIncreases(method f, env e, calldataarg args) {
+    uint256 holeBefore = hole();
+
+    f(e, args);
+
+    uint256 holeAfter = hole();
+
+    assert holeBefore <= holeAfter;
+}
+
+rule lastTotalAssetsSmallerThanTotalAssets() {
+    assert lastTotalAssets() <= totalAssets();
+}
+
+rule lastTotalAssetsIncreases(method f, env e, calldataarg args) 
+filtered {
+    f -> f.selector != sig:withdraw(uint256, address, address).selector && 
+        f.selector != sig:redeem(uint256, address, address).selector && 
+        f.selector != sig:updateWithdrawQueue(uint256[]).selector
+}
+{
+    uint256 lastTotalAssetsBefore = lastTotalAssets();
+
+    f(e, args);
+
+    uint256 lastTotalAssetsAfter = lastTotalAssets();
+
+    assert lastTotalAssetsBefore <= lastTotalAssetsAfter;
+}
+
+// this rule's vacuity check is timing out
+rule lastTotalAssetsDecreasesCorrectlyOnWithdraw(env e, uint256 assets, address receiver, address owner) {
+    uint256 lastTotalAssetsBefore = lastTotalAssets();
+
+    withdraw(e, assets, receiver, owner);
+
+    uint256 lastTotalAssetsAfter = lastTotalAssets();
+
+    assert to_mathint(lastTotalAssetsAfter) >= lastTotalAssetsBefore - assets;
+}
+
+// this rule's vacuity check is timing out
+rule lastTotalAssetsDecreasesCorrectlyOnRedeem(env e, uint256 shares, address receiver, address owner) {
+    uint256 lastTotalAssetsBefore = lastTotalAssets();
+
+    uint256 assets = redeem(e, shares, receiver, owner);
+
+    uint256 lastTotalAssetsAfter = lastTotalAssets();
+
+    assert to_mathint(lastTotalAssetsAfter) >= lastTotalAssetsBefore - assets;
+}
+
+ghost mathint sumBalances {
+    init_state axiom sumBalances == 0;
+}
+
+hook Sstore _balances[KEY address user] uint256 newBalance (uint256 oldBalance) {
+    sumBalances = sumBalances + newBalance - oldBalance;
+}
+
+invariant totalIsSumBalances()
+    to_mathint(totalSupply()) == sumBalances;
+
+// More precisely: share price does not decrease lower than the one at the last interaction.
+// TODO: not passing yet.
+rule sharePriceIncreases(method f, env e, calldataarg args) {
+    requireInvariant totalIsSumBalances();
+
+    // We query them in a state in which the vault is sync.
+    uint256 lastTotalAssetsBefore = lastTotalAssets();
+    uint256 totalSupplyBefore = totalSupply();
+
+    f(e, args);
+
+    uint256 totalAssetsAfter = totalAssets();
+    uint256 totalSupplyAfter = totalSupply();
+    require totalSupplyAfter > 0;
+
+    assert lastTotalAssetsBefore * totalSupplyAfter <= totalAssetsAfter * totalSupplyBefore;
+}
+

test/forge/HoleTest.sol

@@ -39,27 +39,40 @@ contract HoleTest is IntegrationTest {
         _sortSupplyQueueIdleLast();
     }
 
-    function test_totalAssetsCannotDecrease(uint256 assets, uint128 totalSupplyAssets) public {
+    function test_totalAssetsDecrease(uint256 assets, uint128 expectedHole) public {
         assets = bound(assets, MIN_TEST_ASSETS, MAX_TEST_ASSETS);
 
         loanToken.setBalance(SUPPLIER, assets);
 
         vm.prank(SUPPLIER);
         vault.deposit(assets, ONBEHALF);
 
+        uint128 totalSupplyAssetsBefore = morpho.market(allMarkets[0].id()).totalSupplyAssets;
+        expectedHole = uint128(bound(expectedHole, 0, totalSupplyAssetsBefore));
+
         uint256 totalAssetsBefore = vault.totalAssets();
-        _writeTotalSupplyAssets(Id.unwrap(allMarkets[0].id()), totalSupplyAssets);
+        _writeTotalSupplyAssets(Id.unwrap(allMarkets[0].id()), totalSupplyAssetsBefore - expectedHole);
         uint256 totalAssetsAfter = vault.totalAssets();
 
-        assertGe(totalAssetsAfter, totalAssetsBefore, "totalAssets decreased");
+        assertLe(totalAssetsAfter, totalAssetsBefore, "totalAssets did not decreased");
     }
 
-    function invariant_totalAssetsCannotDecrease() public {
-        uint256 totalAssetsBefore = vault.totalAssets();
-        _writeTotalSupplyAssets(Id.unwrap(allMarkets[0].id()), 0);
-        uint256 totalAssetsAfter = vault.totalAssets();
+    function test_lastTotalAssetsNoDecrease(uint256 assets, uint128 expectedHole) public {
+        assets = bound(assets, MIN_TEST_ASSETS, MAX_TEST_ASSETS);
 
-        assertGe(totalAssetsAfter, totalAssetsBefore, "totalAssets decreased");
+        loanToken.setBalance(SUPPLIER, assets);
+
+        vm.prank(SUPPLIER);
+        vault.deposit(assets, ONBEHALF);
+
+        uint128 totalSupplyAssetsBefore = morpho.market(allMarkets[0].id()).totalSupplyAssets;
+        expectedHole = uint128(bound(expectedHole, 0, totalSupplyAssetsBefore));
+
+        uint256 lastTotalAssetsBefore = vault.totalAssets();
+        _writeTotalSupplyAssets(Id.unwrap(allMarkets[0].id()), totalSupplyAssetsBefore - expectedHole);
+        uint256 lastTotalAssetsAfter = vault.totalAssets();
+
+        assertLe(totalAssetsAfter, totalAssetsBefore, "totalAssets did not decreased");
     }
 
     function test_HoleValue() public {
@@ -72,10 +85,10 @@ contract HoleTest is IntegrationTest {
 
         vault.deposit(0, ONBEHALF); // update hole.
 
-        assertEq(vault.hole(), 0.5 ether, "totalAssets decreased");
+        assertEq(vault.hole(), 0.5 ether, "hole");
     }
 
-    function test_HoleValue(uint256 assets, uint128 expectedHole) public {
+    function test_HoleValue(uint256 assets, uint128 expectedHole) public returns (uint128) {
         assets = bound(assets, MIN_TEST_ASSETS, MAX_TEST_ASSETS);
 
         loanToken.setBalance(SUPPLIER, assets);
@@ -90,7 +103,44 @@ contract HoleTest is IntegrationTest {
 
         vault.deposit(0, ONBEHALF); // update hole.
 
-        assertEq(vault.hole(), expectedHole, "totalAssets decreased");
+        assertEq(vault.hole(), expectedHole, "hole");
+
+        return expectedHole;
+    }
+
+    function test_resupplyOnHole(uint256 assets, uint128 expectedHole, uint256 assets2) public {
+        expectedHole = test_HoleValue(assets, expectedHole);
+
+        assets2 = bound(assets2, MIN_TEST_ASSETS, MAX_TEST_ASSETS);
+
+        loanToken.setBalance(SUPPLIER, assets2);
+
+        vm.prank(SUPPLIER);
+        vault.deposit(assets2, ONBEHALF);
+
+        assertEq(vault.hole(), expectedHole, "hole");
+    }
+
+    function test_newHoleOnHole(uint256 firstSupply, uint128 firstHole, uint256 secondSupply, uint128 secondHole)
+        public
+    {
+        firstHole = test_HoleValue(firstSupply, firstHole);
+
+        secondSupply = bound(secondSupply, MIN_TEST_ASSETS, MAX_TEST_ASSETS);
+
+        loanToken.setBalance(SUPPLIER, secondSupply);
+
+        vm.prank(SUPPLIER);
+        vault.deposit(secondSupply, ONBEHALF);
+
+        uint128 totalSupplyAssetsBefore = morpho.market(allMarkets[0].id()).totalSupplyAssets;
+        secondHole = uint128(bound(secondHole, 0, totalSupplyAssetsBefore));
+
+        _writeTotalSupplyAssets(Id.unwrap(allMarkets[0].id()), totalSupplyAssetsBefore - secondHole);
+
+        vault.deposit(0, ONBEHALF); // update hole.
+
+        assertEq(vault.hole(), firstHole + secondHole, "hole");
     }
 
     function test_HoleEvent(uint256 assets, uint128 expectedHole) public {