diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 9ae422c51..059011fde 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -103,14 +103,14 @@ rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newFeeRecipient == oldFeeRecipient; } -// Check the revert condition for the createMarket function. -rule createMarketRevertCondition(env e, MorphoHarness.MarketParams marketParams) { +// Check that createMarket reverts when its input are not validated. +rule createMarketInputValidation(env e, MorphoHarness.MarketParams marketParams) { MorphoHarness.Id id = libId(marketParams); bool irmEnabled = isIrmEnabled(marketParams.irm); bool lltvEnabled = isLltvEnabled(marketParams.lltv); bool wasCreated = isCreated(id); createMarket@withrevert(e, marketParams); - assert lastReverted <=> e.msg.value != 0 || !irmEnabled || !lltvEnabled || wasCreated; + assert e.msg.value != 0 || !irmEnabled || !lltvEnabled || wasCreated => lastReverted; } // Check that supply reverts when its input are not validated. diff --git a/src/Morpho.sol b/src/Morpho.sol index 787013200..7871519af 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -158,6 +158,9 @@ contract Morpho is IMorphoStaticTyping { 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 */ diff --git a/test/forge/integration/CreateMarketIntegrationTest.sol b/test/forge/integration/CreateMarketIntegrationTest.sol index 1fd2eb083..50bfdc38a 100644 --- a/test/forge/integration/CreateMarketIntegrationTest.sol +++ b/test/forge/integration/CreateMarketIntegrationTest.sol @@ -47,6 +47,8 @@ contract CreateMarketIntegrationTest is BaseTest { if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + 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); morpho.createMarket(marketParamsFuzz); @@ -66,6 +68,9 @@ contract CreateMarketIntegrationTest is BaseTest { vm.startPrank(OWNER); if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + + vm.mockCall(marketParamsFuzz.irm, abi.encodeWithSelector(IIrm.borrowRate.selector), abi.encode(0)); + morpho.createMarket(marketParamsFuzz); vm.expectRevert(bytes(ErrorsLib.MARKET_ALREADY_CREATED)); @@ -81,6 +86,8 @@ contract CreateMarketIntegrationTest is BaseTest { if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + vm.mockCall(marketParamsFuzz.irm, abi.encodeWithSelector(IIrm.borrowRate.selector), abi.encode(0)); + morpho.createMarket(marketParamsFuzz); vm.stopPrank();