From d21a86f291aad386dc3383ca7e16a790c213d7b6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 22 Nov 2023 19:36:43 +0100 Subject: [PATCH 1/4] test: mutant 13 --- src/Morpho.sol | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index f755904b6..0cf98947a 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -461,7 +461,9 @@ contract Morpho is IMorphoStaticTyping { /// @inheritdoc IMorphoBase function accrueInterest(MarketParams memory marketParams) external { Id id = marketParams.id(); - require(market[id].lastUpdate != 0, ErrorsLib.MARKET_NOT_CREATED); + /// RequireMutation(`market[id].lastUpdate != 0` |==> `false`) of: `require(market[id].lastUpdate != 0, + /// ErrorsLib.MARKET_NOT_CREATED);` + require(false, ErrorsLib.MARKET_NOT_CREATED); _accrueInterest(marketParams, id); } From 04f0c4b3953180aaf1cfdadbf6a170a10f504772 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Nov 2023 12:50:55 +0100 Subject: [PATCH 2/4] refactor: improving mutant to get significant result --- src/Morpho.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 0cf98947a..226386cee 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -463,7 +463,7 @@ contract Morpho is IMorphoStaticTyping { Id id = marketParams.id(); /// RequireMutation(`market[id].lastUpdate != 0` |==> `false`) of: `require(market[id].lastUpdate != 0, /// ErrorsLib.MARKET_NOT_CREATED);` - require(false, ErrorsLib.MARKET_NOT_CREATED); + require(true, ErrorsLib.MARKET_NOT_CREATED); _accrueInterest(marketParams, id); } From c4306f1c72fb981832e1697b85aad8001b39d30d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Nov 2023 13:26:43 +0100 Subject: [PATCH 3/4] feat: accrue interest input validation --- certora/specs/Reverts.spec | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 7ecb5be1c..11bdabddf 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -161,3 +161,10 @@ rule liquidateInputValidation(env e, MorphoHarness.MarketParams marketParams, ad liquidate@withrevert(e, marketParams, borrower, seizedAssets, repaidShares, data); assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted; } + +// Check that accrueInterest reverts when its inputs are not validated. +rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) { + uint256 lastUpdate = lastUpdate(libId(marketParams)); + accrueInterest@withrevert(e, marketParams); + assert lastUpdate == 0 => lastReverted; +} From c25947a795a8fdea18211c0d5642c1b1cf5176bc Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Nov 2023 14:03:12 +0100 Subject: [PATCH 4/4] revert: test mutant 13 --- src/Morpho.sol | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 226386cee..f755904b6 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -461,9 +461,7 @@ contract Morpho is IMorphoStaticTyping { /// @inheritdoc IMorphoBase function accrueInterest(MarketParams memory marketParams) external { Id id = marketParams.id(); - /// RequireMutation(`market[id].lastUpdate != 0` |==> `false`) of: `require(market[id].lastUpdate != 0, - /// ErrorsLib.MARKET_NOT_CREATED);` - require(true, ErrorsLib.MARKET_NOT_CREATED); + require(market[id].lastUpdate != 0, ErrorsLib.MARKET_NOT_CREATED); _accrueInterest(marketParams, id); }