From 28fc36c994853d34292acc570e2ac0754ee49aa8 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sat, 9 Dec 2023 23:15:42 +0100 Subject: [PATCH 01/13] refactor: accrue interest --- src/Morpho.sol | 53 +++++++++++++++++++++++++------------------------- 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 16fd75c80..b98cba9d5 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -153,14 +153,10 @@ contract Morpho is IMorphoStaticTyping { require(isLltvEnabled[marketParams.lltv], ErrorsLib.LLTV_NOT_ENABLED); require(market[id].lastUpdate == 0, ErrorsLib.MARKET_ALREADY_CREATED); - // Safe "unchecked" cast. - market[id].lastUpdate = uint128(block.timestamp); + _accrueInterest(marketParams, id); idToMarketParams[id] = marketParams; emit EventsLib.CreateMarket(id, marketParams); - - // Call to initialize the IRM in case it is stateful. - IIrm(marketParams.irm).borrowRate(marketParams, market[id]); } /* SUPPLY MANAGEMENT */ @@ -472,29 +468,33 @@ contract Morpho is IMorphoStaticTyping { /// @dev Accrues interest for the given market `marketParams`. /// @dev Assumes that the inputs `marketParams` and `id` match. function _accrueInterest(MarketParams memory marketParams, Id id) internal { - uint256 elapsed = block.timestamp - market[id].lastUpdate; - - if (elapsed == 0) return; - + // The IRM is always called, useful for stateful IRMs. uint256 borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); - uint256 interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed)); - market[id].totalBorrowAssets += interest.toUint128(); - market[id].totalSupplyAssets += interest.toUint128(); + // At market creation, elapsed==block.timestamp but totalBorrowAssets==0 so no interest is accrued, as expected. + uint256 elapsed = block.timestamp - market[id].lastUpdate; + uint256 interest; uint256 feeShares; - if (market[id].fee != 0) { - uint256 feeAmount = interest.wMulDown(market[id].fee); - // The fee amount is subtracted from the total supply in this calculation to compensate for the fact - // that total supply is already increased by the full interest (including the fee amount). - feeShares = feeAmount.toSharesDown(market[id].totalSupplyAssets - feeAmount, market[id].totalSupplyShares); - position[id][feeRecipient].supplyShares += feeShares; - market[id].totalSupplyShares += feeShares.toUint128(); + if (elapsed != 0) { + interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed)); + market[id].totalBorrowAssets += interest.toUint128(); + market[id].totalSupplyAssets += interest.toUint128(); + + if (market[id].fee != 0) { + uint256 feeAmount = interest.wMulDown(market[id].fee); + // The fee amount is subtracted from the total supply in this calculation to compensate for the fact + // that total supply is already increased by the full interest (including the fee amount). + feeShares = + feeAmount.toSharesDown(market[id].totalSupplyAssets - feeAmount, market[id].totalSupplyShares); + position[id][feeRecipient].supplyShares += feeShares; + market[id].totalSupplyShares += feeShares.toUint128(); + } } - emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares); - // Safe "unchecked" cast. market[id].lastUpdate = uint128(block.timestamp); + + emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares); } /* HEALTH CHECK */ @@ -502,11 +502,12 @@ contract Morpho is IMorphoStaticTyping { /// @dev Returns whether the position of `borrower` in the given market `marketParams` is healthy. /// @dev Assumes that the inputs `marketParams` and `id` match. function _isHealthy(MarketParams memory marketParams, Id id, address borrower) internal view returns (bool) { - if (position[id][borrower].borrowShares == 0) return true; - - uint256 collateralPrice = IOracle(marketParams.oracle).price(); - - return _isHealthy(marketParams, id, borrower, collateralPrice); + if (position[id][borrower].borrowShares == 0) { + return true; + } else { + uint256 collateralPrice = IOracle(marketParams.oracle).price(); + return _isHealthy(marketParams, id, borrower, collateralPrice); + } } /// @dev Returns whether the position of `borrower` in the given market `marketParams` with the given From cee545a6ce11b2d19f714af66fa16a8921e193e8 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sat, 9 Dec 2023 23:26:46 +0100 Subject: [PATCH 02/13] test: add rule of market creation --- certora/specs/ConsistentState.spec | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 97083a02d..b158be3dc 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -176,6 +176,13 @@ rule libIdUnique() { assert marketParams1.lltv == marketParams2.lltv; } +rule createdMarketIsEmpty(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id = libId(marketParams); + createMarket(e, marketParams); + assert totalBorrowAssets(id) == 0; + assert totalSupplyAssets(id) == 0; +} + // Check that only the user is able to change who is authorized to manage his position. rule onlyUserCanAuthorizeWithoutSig(env e, method f, calldataarg data) filtered { From 65bd84ce7f1448e3ffbb43b25b90dcf2e92a4f37 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sun, 10 Dec 2023 12:01:58 +0100 Subject: [PATCH 03/13] test: improve verif --- certora/specs/ConsistentState.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index b158be3dc..5688d9dc6 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -176,9 +176,11 @@ rule libIdUnique() { assert marketParams1.lltv == marketParams2.lltv; } -rule createdMarketIsEmpty(env e, MorphoHarness.MarketParams marketParams) { +// Check that just after a market is created, its state is consistent. +rule createdMarketConsistentState(env e, MorphoHarness.MarketParams marketParams) { MorphoHarness.Id id = libId(marketParams); createMarket(e, marketParams); + assert lastUpdate(id) == e.block.timestamp; assert totalBorrowAssets(id) == 0; assert totalSupplyAssets(id) == 0; } From 922cd3f450cc00712736f90545e117004d7715b2 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sun, 10 Dec 2023 12:09:08 +0100 Subject: [PATCH 04/13] refactor: revert _isHealthy change --- src/Morpho.sol | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index b98cba9d5..63788754d 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -502,12 +502,11 @@ contract Morpho is IMorphoStaticTyping { /// @dev Returns whether the position of `borrower` in the given market `marketParams` is healthy. /// @dev Assumes that the inputs `marketParams` and `id` match. function _isHealthy(MarketParams memory marketParams, Id id, address borrower) internal view returns (bool) { - if (position[id][borrower].borrowShares == 0) { - return true; - } else { - uint256 collateralPrice = IOracle(marketParams.oracle).price(); - return _isHealthy(marketParams, id, borrower, collateralPrice); - } + if (position[id][borrower].borrowShares == 0) return true; + + uint256 collateralPrice = IOracle(marketParams.oracle).price(); + + return _isHealthy(marketParams, id, borrower, collateralPrice); } /// @dev Returns whether the position of `borrower` in the given market `marketParams` with the given From b556df66f95882b63be4d0fba5000196d3d79858 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sun, 10 Dec 2023 13:04:37 +0100 Subject: [PATCH 05/13] refactor: write lastUpdate before accrueInterest --- src/Morpho.sol | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 63788754d..8d95d12b8 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -153,9 +153,12 @@ contract Morpho is IMorphoStaticTyping { require(isLltvEnabled[marketParams.lltv], ErrorsLib.LLTV_NOT_ENABLED); require(market[id].lastUpdate == 0, ErrorsLib.MARKET_ALREADY_CREATED); - _accrueInterest(marketParams, id); + // Safe "unchecked" cast. + market[id].lastUpdate = uint128(block.timestamp); idToMarketParams[id] = marketParams; + _accrueInterest(marketParams, id); + emit EventsLib.CreateMarket(id, marketParams); } @@ -468,9 +471,8 @@ contract Morpho is IMorphoStaticTyping { /// @dev Accrues interest for the given market `marketParams`. /// @dev Assumes that the inputs `marketParams` and `id` match. function _accrueInterest(MarketParams memory marketParams, Id id) internal { - // The IRM is always called, useful for stateful IRMs. + // The IRM is called even when elapsed=0. It can be useful for stateful IRMs. uint256 borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); - // At market creation, elapsed==block.timestamp but totalBorrowAssets==0 so no interest is accrued, as expected. uint256 elapsed = block.timestamp - market[id].lastUpdate; uint256 interest; From c17b57e414a3d66f0a06f21190c33a6b0747f235 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Sun, 10 Dec 2023 13:12:37 +0100 Subject: [PATCH 06/13] test: remove rule --- certora/specs/ConsistentState.spec | 9 --------- 1 file changed, 9 deletions(-) diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 5688d9dc6..97083a02d 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -176,15 +176,6 @@ rule libIdUnique() { assert marketParams1.lltv == marketParams2.lltv; } -// Check that just after a market is created, its state is consistent. -rule createdMarketConsistentState(env e, MorphoHarness.MarketParams marketParams) { - MorphoHarness.Id id = libId(marketParams); - createMarket(e, marketParams); - assert lastUpdate(id) == e.block.timestamp; - assert totalBorrowAssets(id) == 0; - assert totalSupplyAssets(id) == 0; -} - // Check that only the user is able to change who is authorized to manage his position. rule onlyUserCanAuthorizeWithoutSig(env e, method f, calldataarg data) filtered { From 774b3e564650a717b499db9760f84f2f2ff2d7bc Mon Sep 17 00:00:00 2001 From: MathisGD Date: Mon, 11 Dec 2023 15:06:31 +0100 Subject: [PATCH 07/13] refactor: emit createMarket before interest accrual --- src/Morpho.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 3eee98fe7..1e3147488 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -157,9 +157,9 @@ contract Morpho is IMorphoStaticTyping { market[id].lastUpdate = uint128(block.timestamp); idToMarketParams[id] = marketParams; - _accrueInterest(marketParams, id); - emit EventsLib.CreateMarket(id, marketParams); + + _accrueInterest(marketParams, id); } /* SUPPLY MANAGEMENT */ From fd2c00f5ab1f2e3d677ab791fa30927ed8ddeb30 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Thu, 14 Dec 2023 16:46:54 +0100 Subject: [PATCH 08/13] test: skip certora time-out --- certora/specs/AccrueInterest.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 7babf38de..a57c36a8d 100644 --- a/certora/specs/AccrueInterest.spec +++ b/certora/specs/AccrueInterest.spec @@ -108,7 +108,9 @@ rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint25 // We also exclude setFeeRecipient, as it is known to be not commutative. rule accrueInterestCommutesExceptForSetFeeRecipient(method f, calldataarg args) filtered { - f -> !f.isView && f.selector != sig:setFeeRecipient(address).selector + f -> !f.isView + && f.selector != sig:setFeeRecipient(address).selector + && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector } { env e1; From 8a18826e4b0b3f66ae7776120fa7cff9128eab93 Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Fri, 15 Dec 2023 10:42:18 +0100 Subject: [PATCH 09/13] refactor: don't set zero Co-authored-by: Merlin Egalite <44097430+MerlinEgalite@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- src/Morpho.sol | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index d5b8972b0..9e0dc01a7 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -483,8 +483,7 @@ contract Morpho is IMorphoStaticTyping { function _accrueInterest(MarketParams memory marketParams, Id id) internal { // The IRM is called even when elapsed=0. It can be useful for stateful IRMs. uint256 borrowRate; - if (marketParams.irm == address(0)) borrowRate = 0; - else borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); + if (marketParams.irm != address(0)) borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); uint256 elapsed = block.timestamp - market[id].lastUpdate; From 94e39c0dad37507fa5e8a27d10f1799fd66cab64 Mon Sep 17 00:00:00 2001 From: MathisGD Date: Mon, 18 Dec 2023 10:05:02 +0100 Subject: [PATCH 10/13] test: fix create market test --- test/forge/integration/CreateMarketIntegrationTest.sol | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/test/forge/integration/CreateMarketIntegrationTest.sol b/test/forge/integration/CreateMarketIntegrationTest.sol index cbf23393a..0a72c33d8 100644 --- a/test/forge/integration/CreateMarketIntegrationTest.sol +++ b/test/forge/integration/CreateMarketIntegrationTest.sol @@ -44,6 +44,7 @@ contract CreateMarketIntegrationTest is BaseTest { function testCreateMarketWithEnabledIrmAndLltv(MarketParams memory marketParamsFuzz) public { marketParamsFuzz.lltv = _boundValidLltv(marketParamsFuzz.lltv); + marketParamsFuzz.irm = address(irm); Id marketParamsFuzzId = marketParamsFuzz.id(); vm.startPrank(OWNER); @@ -51,10 +52,6 @@ contract CreateMarketIntegrationTest is BaseTest { if (!morpho.isLltvEnabled(marketParamsFuzz.lltv)) morpho.enableLltv(marketParamsFuzz.lltv); vm.stopPrank(); - if (marketParamsFuzz.irm != address(0)) { - vm.mockCall(marketParamsFuzz.irm, abi.encodeWithSelector(IIrm.borrowRate.selector), abi.encode(0)); - } - vm.expectEmit(true, true, true, true, address(morpho)); emit EventsLib.CreateMarket(marketParamsFuzz.id(), marketParamsFuzz); vm.prank(OWNER); From a0f70079900cf4be228af262ca1b96a30cc7b413 Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Mon, 18 Dec 2023 11:27:02 +0100 Subject: [PATCH 11/13] test: minor improvement Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- test/forge/integration/CreateMarketIntegrationTest.sol | 1 - 1 file changed, 1 deletion(-) diff --git a/test/forge/integration/CreateMarketIntegrationTest.sol b/test/forge/integration/CreateMarketIntegrationTest.sol index 0a72c33d8..59b3831a9 100644 --- a/test/forge/integration/CreateMarketIntegrationTest.sol +++ b/test/forge/integration/CreateMarketIntegrationTest.sol @@ -48,7 +48,6 @@ contract CreateMarketIntegrationTest is BaseTest { Id marketParamsFuzzId = marketParamsFuzz.id(); vm.startPrank(OWNER); - if (!morpho.isIrmEnabled(marketParamsFuzz.irm)) morpho.enableIrm(marketParamsFuzz.irm); if (!morpho.isLltvEnabled(marketParamsFuzz.lltv)) morpho.enableLltv(marketParamsFuzz.lltv); vm.stopPrank(); From 713a4a97117dce079e7994aa6d598a0735e1c46a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 18 Dec 2023 11:49:20 +0100 Subject: [PATCH 12/13] fix: skip update timestamp --- certora/specs/AccrueInterest.spec | 5 ++--- src/Morpho.sol | 6 +++--- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index a57c36a8d..ad0d3b055 100644 --- a/certora/specs/AccrueInterest.spec +++ b/certora/specs/AccrueInterest.spec @@ -108,9 +108,8 @@ rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint25 // We also exclude setFeeRecipient, as it is known to be not commutative. rule accrueInterestCommutesExceptForSetFeeRecipient(method f, calldataarg args) filtered { - f -> !f.isView - && f.selector != sig:setFeeRecipient(address).selector - && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector + f -> !f.isView + && f.selector != sig:setFeeRecipient(address).selector } { env e1; diff --git a/src/Morpho.sol b/src/Morpho.sol index 9e0dc01a7..950a58e8c 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -503,10 +503,10 @@ contract Morpho is IMorphoStaticTyping { position[id][feeRecipient].supplyShares += feeShares; market[id].totalSupplyShares += feeShares.toUint128(); } - } - // Safe "unchecked" cast. - market[id].lastUpdate = uint128(block.timestamp); + // Safe "unchecked" cast. + market[id].lastUpdate = uint128(block.timestamp); + } emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares); } From 91ceb113084a2c6cc099bdbe443635794ac73a15 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 18 Dec 2023 16:03:45 +0100 Subject: [PATCH 13/13] fix: limit depth 3 AccrueInterest --- certora/confs/AccrueInterest.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index a923c628e..a5df41486 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -4,6 +4,7 @@ ], "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_args": [ + "-depth 3", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ],