docs: minor improvements (#423)

* fix ConsistentState.spec Signed-off-by: Elias Rad <[email protected]> * fix Enabled.spec Signed-off-by: Elias Rad <[email protected]> * fix LastUpdated.spec Signed-off-by: Elias Rad <[email protected]> * fix Roles.spec Signed-off-by: Elias Rad <[email protected]> * fix Timelock.spec Signed-off-by: Elias Rad <[email protected]> * fix README.md Signed-off-by: Elias Rad <[email protected]> * Update Enabled.spec Signed-off-by: Elias Rad <[email protected]> --------- Signed-off-by: Elias Rad <[email protected]>
morpho-org · Jul 3, 2024 · 5617ec0 · 5617ec0
1 parent 3527aff
commit 5617ec0
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/certora/README.md b/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.
 

diff --git a/certora/specs/ConsistentState.spec b/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;
 

diff --git a/certora/specs/LastUpdated.spec b/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;
 }

diff --git a/certora/specs/Roles.spec b/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;

diff --git a/certora/specs/Timelock.spec b/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;