From 5617ec0c8afabc18a67f791490c087f1d80fb049 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 21:34:41 +0300 Subject: [PATCH] docs: minor improvements (#423) * fix ConsistentState.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * fix Enabled.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * fix LastUpdated.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * fix Roles.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * fix Timelock.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * fix README.md Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> * Update Enabled.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --------- Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/README.md | 2 +- certora/specs/ConsistentState.spec | 2 +- certora/specs/LastUpdated.spec | 4 ++-- certora/specs/Roles.spec | 2 +- certora/specs/Timelock.spec | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/README.md b/certora/README.md index c2156b68..7d7a94cb 100644 --- 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 index 7e825094..fd2a7c15 100644 --- 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 index 4fee4e59..8e36b3b9 100644 --- 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 index e04fb8d3..0d1f8fec 100644 --- 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 index 734e93e3..f2435d5d 100644 --- 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;