test: halmost irm and ltv can't be disabled

test/forge/HalmosTest.sol

@@ -28,6 +28,7 @@ contract HalmosTest is SymTest, Test {
     ERC20Mock internal collateralToken;
     OracleMock internal oracle;
     IrmMock internal irm;
+    uint256 internal lltv;
 
     MarketParams internal marketParams;
     Id internal id;
@@ -51,7 +52,7 @@ contract HalmosTest is SymTest, Test {
         morpho.setFeeRecipient(FEE_RECIPIENT);
         vm.stopPrank();
 
-        uint256 lltv = svm.createUint256("lltv");
+        lltv = svm.createUint256("lltv");
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
@@ -141,11 +142,26 @@ contract HalmosTest is SymTest, Test {
     }
 
     // Check that enabled LLTVs are necessarily less than 1.
-    function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 lltv) public {
-        vm.assume(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+    function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 _lltv) public {
+        vm.assume(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18);
 
         _callMorpho(selector, caller);
 
-        assert(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+        assert(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18);
+    }
+
+    // Check that LLTVs can't be disabled.
+    function check_lltvCannotBeDisabled(bytes4 selector, address caller) public {
+        _callMorpho(selector, caller);
+
+        assert(morpho.isLltvEnabled(lltv));
+    }
+
+    // Check that IRMs can't be disabled.
+    // Note: IRM is not symbolic, that is not ideal.
+    function check_irmCannotBeDisabled(bytes4 selector, address caller) public {
+        _callMorpho(selector, caller);
+
+        assert(morpho.isIrmEnabled(address(irm)));
     }
 }