Docs improvements

certora/README.md

@@ -90,7 +90,7 @@ Note also that these properties are ensured to always hold, because the contract
 
 ### Consistent asset
 
-For deposit and withdraw, it is checked that markets have a the same loan token as the loan token of the vault.
+For deposit and withdraw, it is checked that markets have the same loan token as the loan token of the vault.
 We say that such market has a consistent asset.
 The following function defined in [`ConsistentState.spec`](specs/ConsistentState.spec) is verified to always return `true` and contributes to verifying the property above.
 

certora/specs/ConsistentState.spec

@@ -11,7 +11,7 @@ methods {
     function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
 }
 
-// Check that fee cannot accrue to an unset fee recipient.
+// Check that the fee cannot accrue to an unset fee recipient.
 invariant noFeeToUnsetFeeRecipient()
     feeRecipient() == 0 => fee() == 0;
 

certora/specs/Enabled.spec

@@ -25,7 +25,7 @@ rule inWithdrawQueueIsEnabledPreservedUpdateWithdrawQueue(env e, uint256 i, uint
     updateWithdrawQueue(e, indexes);
 
     MetaMorphoHarness.Id id = withdrawQueue(i);
-    // Safe require because j is not otherwise constrained.
+    // Safe is required because j is not otherwise constrained.
     // The ghost variable deletedAt is useful to make sure that markets are not permuted and deleted at the same time in updateWithdrawQueue.
     require j == deletedAt(id);
 

certora/specs/LastUpdated.spec

@@ -19,10 +19,10 @@ function hasGuardianRole(address user) returns bool {
     return user == owner() || user == guardian();
 }
 
-// Check that any market with positive cap is created on Morpho Blue.
+// Check that any market with a positive cap is created on Morpho Blue.
 // The corresponding invariant is difficult to verify because it requires to check properties on MetaMorpho and on Blue at the same time:
 // - on MetaMorpho, that it holds when the cap is positive for the first time
-// - on Blue, that a created market always has positive last update
+// - on Blue, that a created market always has a positive last update
 function hasPositiveSupplyCapIsUpdated(MetaMorphoHarness.Id id) returns bool {
     return config_(id).cap > 0 => Morpho.lastUpdate(id) > 0;
 }

certora/specs/Roles.spec

@@ -13,7 +13,7 @@ methods {
     function guardian() external returns(address) envfree;
     function isAllocator(address target) external returns(bool) envfree;
 
-    // Sumarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
+    // Summarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
     function _.idToMarketParams(MetaMorphoHarness.Id) external => CONSTANT;
     function _.supplyShares(MetaMorphoHarness.Id, address) external => CONSTANT;
     function _.accrueInterest(MetaMorphoHarness.MarketParams) external => CONSTANT;

certora/specs/Timelock.spec

@@ -97,7 +97,7 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) {
     f(e_next, args);
 
     if (e_next.block.timestamp < nextTime)  {
-        // Check that cap cannot increase.
+        // Check that the cap cannot increase.
         assert config_(id).cap <= prevCap;
         // Increasing nextCapIncreaseTime with an interaction;
         assert nextCapIncreaseTime(e_next, id) >= nextCapIncreaseTimeBeforeInteraction;