[Certora] Improve require documentation

certora/specs/AccrueInterest.spec

@@ -32,6 +32,7 @@ ghost ghostTransferFrom(address, address, uint256) returns bool;
 // Check that calling accrueInterest first has no effect.
 // This is because supply should call accrueInterest itself.
 rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -49,6 +50,7 @@ rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint2
 // Check that calling accrueInterest first has no effect.
 // This is because withdraw should call accrueInterest itself.
 rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -66,6 +68,7 @@ rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uin
 // Check that calling accrueInterest first has no effect.
 // This is because borrow should call accrueInterest itself.
 rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -83,6 +86,7 @@ rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint2
 // Check that calling accrueInterest first has no effect.
 // This is because repay should call accrueInterest itself.
 rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -111,9 +115,9 @@ filtered {
     env e2;
     MorphoHarness.MarketParams marketParams;
 
-    // Require interactions to happen at the same block.
+    // Assume interactions to happen at the same block.
     require e1.block.timestamp == e2.block.timestamp;
-    // Assumption required to cast a timestamp to uint128.
+    // Safe require because timestamps cannot realistically be that large.
     require e1.block.timestamp < 2^128;
 
     storage init = lastStorage;

certora/specs/ConsistentState.spec

@@ -19,6 +19,7 @@ methods {
     function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
 
     function maxFee() external returns uint256 envfree;
+    function wad() external returns uint256 envfree;
 
     function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value);
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
@@ -79,9 +80,11 @@ hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount
 
 function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
     if (from == currentContract) {
+        // Safe require because the reference implementation would revert.
         myBalances[token] = require_uint256(myBalances[token] - amount);
     }
     if (to == currentContract) {
+        // Safe require because the reference implementation would revert.
         myBalances[token] = require_uint256(myBalances[token] + amount);
     }
 }
@@ -116,6 +119,7 @@ invariant marketInvariant(MorphoHarness.MarketParams marketParams)
 invariant isLiquid(address token)
     sumAmount[token] <= myBalances[token]
 {
+    // Safe requires on the sender because the contract cannot call the function itself.
     preserved supply(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) {
         requireInvariant marketInvariant(marketParams);
         require e.msg.sender != currentContract;
@@ -150,6 +154,9 @@ invariant isLiquid(address token)
 invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
     isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
 
+invariant lltvSmallerThanWad(uint256 lltv)
+    isLltvEnabled(lltv) => lltv < wad();
+
 // Check that a market can only exist if its IRM is enabled.
 invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams)
     isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm);
@@ -159,7 +166,7 @@ rule libIdUnique() {
     MorphoHarness.MarketParams marketParams1;
     MorphoHarness.MarketParams marketParams2;
 
-    // Require the same arguments.
+    // Assume that arguments are the same.
     require libId(marketParams1) == libId(marketParams2);
 
     assert marketParams1.borrowableToken == marketParams2.borrowableToken;
@@ -178,7 +185,7 @@ filtered {
     address user;
     address someone;
 
-    // Require a different user to interact with Morpho.
+    // Assume that it is another user that is interacting with Morpho.
     require user != e.msg.sender;
 
     bool authorizedBefore = isAuthorized(user, someone);
@@ -197,7 +204,7 @@ filtered { f -> !f.isView }
     MorphoHarness.Id id;
     address user;
 
-    // Require that the e.msg.sender is not authorized.
+    // Assume that the e.msg.sender is not authorized.
     require !isAuthorized(user, e.msg.sender);
     require user != e.msg.sender;
 
@@ -217,7 +224,7 @@ filtered { f -> !f.isView }
     MorphoHarness.Id id;
     address user;
 
-    // Require that the e.msg.sender is not authorized.
+    // Assume that the e.msg.sender is not authorized.
     require !isAuthorized(user, e.msg.sender);
     require user != e.msg.sender;
 
@@ -240,7 +247,7 @@ filtered {
     MorphoHarness.Id id;
     address user;
 
-    // Require that the e.msg.sender is not authorized.
+    // Assume that the e.msg.sender is not authorized.
     require !isAuthorized(user, e.msg.sender);
     require user != e.msg.sender;
 
@@ -260,10 +267,10 @@ filtered { f -> !f.isView }
     MorphoHarness.Id id;
     address user;
 
-    // Require that the e.msg.sender is not authorized.
+    // Assume that the e.msg.sender is not authorized.
     require !isAuthorized(user, e.msg.sender);
     require user != e.msg.sender;
-    // Require that the user has no outstanding debt.
+    // Assume that the user has no outstanding debt.
     require borrowShares(id, user) == 0;
 
     mathint collateralBefore = collateral(id, user);
@@ -280,6 +287,7 @@ rule noTimeTravel(method f, env e, calldataarg args)
 filtered { f -> !f.isView }
 {
     MorphoHarness.Id id;
+    // Assume the property before the interaction.
     require lastUpdate(id) <= e.block.timestamp;
     f(e, args);
     assert lastUpdate(id) <= e.block.timestamp;

certora/specs/ExactMath.spec

@@ -19,26 +19,32 @@ methods {
 }
 
 function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
     return require_uint256((x * y + (d - 1)) / d);
 }
 
 function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
     return require_uint256((x * y) / d);
 }
 
 // Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio.
+// More details on the purpose of this rule in RatioMath.spec.
 rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) {
     MorphoHarness.Id id = libId(marketParams);
+    // Safe require because this invariant is checked in ConsistentState.spec
     require fee(id) <= maxFee();
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
     mathint sharesBefore = virtualTotalBorrowShares(id);
 
+    // Assume no interest as it would increase the borrowed assets.
     require lastUpdate(id) == e.block.timestamp;
 
     mathint repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onbehalf, data);
 
+    // Check the case where the market is fully repaid.
     require repaidAssets >= assetsBefore;
 
     mathint assetsAfter = virtualTotalBorrowAssets(id);
@@ -60,9 +66,9 @@ rule supplyWithdraw() {
     env e1;
     env e2;
 
-    // Require interactions to happen at the same block.
+    // Assume that interactions to happen at the same block.
     require e1.block.timestamp == e2.block.timestamp;
-    // Assumption required to cast timestamps to uint128.
+    // Safe require because timestamps cannot realistically be that large.
     require e1.block.timestamp < 2^128;
 
     uint256 suppliedAssets;
@@ -93,9 +99,9 @@ rule withdrawSupply() {
     env e1;
     env e2;
 
-    // Require interactions to happen at the same block.
+    // Assume interactions to happen at the same block.
     require e1.block.timestamp == e2.block.timestamp;
-    // Assumption required to cast timestamps to uint128.
+    // Safe require because timestamps cannot realistically be that large.
     require e1.block.timestamp < 2^128;
 
     uint256 withdrawnAssets;

certora/specs/ExitLiquidity.spec

@@ -21,6 +21,7 @@ rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets,
     env e;
     MorphoHarness.Id id = libId(marketParams);
 
+    // Assume no interest as it would increase the total supply assets.
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = supplyShares(id, onBehalf);
@@ -51,6 +52,7 @@ rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uin
     env e;
     MorphoHarness.Id id = libId(marketParams);
 
+    // Assume no interest as it would increase the total borrowed assets.
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = borrowShares(id, onBehalf);
@@ -61,6 +63,7 @@ rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uin
     uint256 repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);
 
+    // Assume a full repay.
     require borrowShares(id, onBehalf) == 0;
 
     assert repaidAssets >= assetsDue;

certora/specs/Health.spec

@@ -28,11 +28,13 @@ function mockPrice() returns uint256 {
 }
 
 function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe requires because the reference implementation would revert.
     require d != 0;
     return require_uint256((x * y + (d - 1)) / d);
 }
 
 function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe requires because the reference implementation would revert.
     require d != 0;
     return require_uint256((x * y) / d);
 }
@@ -55,12 +57,12 @@ filtered {
     MorphoHarness.Id id = libId(marketParams);
     address user;
 
-    // Require that the position is healthy before the interaction.
+    // Assume that the position is healthy before the interaction.
     require isHealthy(marketParams, user);
-    // Require that the LLTV takes coherent values.
+    // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec.
     require marketParams.lltv < 10^18;
     require marketParams.lltv > 0;
-    // Ensure that no interest is accumulated.
+    // Assumption to ensure that no interest is accumulated.
     require lastUpdate(id) == e.block.timestamp;
 
     priceChanged = false;
@@ -81,12 +83,12 @@ filtered { f -> !f.isView }
     MorphoHarness.Id id = libId(marketParams);
     address user;
 
-    // Require that the e.msg.sender is not authorized.
+    // Assume that the e.msg.sender is not authorized.
     require !isAuthorized(user, e.msg.sender);
     require user != e.msg.sender;
-    // Ensure that no interest is accumulated.
+    // Assumption to ensure that no interest is accumulated.
     require lastUpdate(id) == e.block.timestamp;
-    // Require that the user is healthy.
+    // Assume that the user is healthy.
     require isHealthy(marketParams, user);
 
     mathint collateralBefore = collateral(id, user);