From d7091f24ecf11842f2a2180e0337ad255af79453 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 12:56:30 +0300 Subject: [PATCH 1/7] fix ConsistentState.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/ConsistentState.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From 4c9aa7f182020cea20b58395cbd996e0833acf6e Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 12:56:57 +0300 Subject: [PATCH 2/7] fix Enabled.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/Enabled.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/Enabled.spec b/certora/specs/Enabled.spec index 65210cfc..4a644e3d 100644 --- a/certora/specs/Enabled.spec +++ b/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); From 2ac43e5934d41ae96acbf10ae7ff0ec93f3d7cb5 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 12:57:36 +0300 Subject: [PATCH 3/7] fix LastUpdated.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/LastUpdated.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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; } From e22a6e8d54ba1addfb5d766813a1fba8874532e5 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 12:59:46 +0300 Subject: [PATCH 4/7] fix Roles.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/Roles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From 95112223334cd5b34663c667a55d2a6e49328602 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 13:00:22 +0300 Subject: [PATCH 5/7] fix Timelock.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/Timelock.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From 050052faf333f3907101f13135994a1d5633a2c9 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 13:00:57 +0300 Subject: [PATCH 6/7] fix README.md Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. From fb7861c3f8616d5f23aaea4e3523a439785ec9d4 Mon Sep 17 00:00:00 2001 From: Elias Rad <146735585+nnsW3@users.noreply.github.com> Date: Wed, 3 Jul 2024 19:21:17 +0300 Subject: [PATCH 7/7] Update Enabled.spec Signed-off-by: Elias Rad <146735585+nnsW3@users.noreply.github.com> --- certora/specs/Enabled.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/Enabled.spec b/certora/specs/Enabled.spec index 4a644e3d..65210cfc 100644 --- a/certora/specs/Enabled.spec +++ b/certora/specs/Enabled.spec @@ -25,7 +25,7 @@ rule inWithdrawQueueIsEnabledPreservedUpdateWithdrawQueue(env e, uint256 i, uint updateWithdrawQueue(e, indexes); MetaMorphoHarness.Id id = withdrawQueue(i); - // Safe is required because j is not otherwise constrained. + // Safe require 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);