From 017b74e3c364655ba56f663c1b1c8ee3194b9a1d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 2 Apr 2024 11:29:45 +0200 Subject: [PATCH 1/6] feat: use timestamp hook --- certora/specs/Timelock.spec | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec index 3b880965..7b471076 100644 --- a/certora/specs/Timelock.spec +++ b/certora/specs/Timelock.spec @@ -13,13 +13,21 @@ function summarySupplyshares(MetaMorphoHarness.Id id, address user) returns uint return res; } +ghost uint256 lastTimestamp; + +hook TIMESTAMP uint v { + // Safe require because timestamps are guaranteed to be increasing. + require v >= lastTimestamp; + // Safe require as it corresponds to some time very far into the future. + require v < 2^63; + lastTimestamp = v; +} + // Show that nextGuardianUpdateTime does not revert. rule nextGuardianUpdateTimeDoesNotRevert() { // The environment e yields the current time. env e; require e.msg.value == 0; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -35,8 +43,6 @@ rule nextGuardianUpdateTimeDoesNotRevert() { rule guardianUpdateTime(env e_next, method f, calldataarg args) { // The environment e yields the current time. env e; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -46,8 +52,6 @@ rule guardianUpdateTime(env e_next, method f, calldataarg args) { // Assume that the guardian is already set. require prevGuardian != 0; - // Sane assumption on the current time, as any following transaction should happen after it. - require e_next.block.timestamp >= e.block.timestamp; uint256 nextGuardianUpdateTimeBeforeInteraction = nextGuardianUpdateTime(e); // Increasing nextGuardianUpdateTime with no interaction; assert nextGuardianUpdateTimeBeforeInteraction >= nextTime; @@ -68,8 +72,6 @@ rule nextCapIncreaseTimeDoesNotRevert(MetaMorphoHarness.Id id) { // The environment e yields the current time. env e; require e.msg.value == 0; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -85,8 +87,6 @@ rule nextCapIncreaseTimeDoesNotRevert(MetaMorphoHarness.Id id) { rule capIncreaseTime(env e_next, method f, calldataarg args) { // The environment e yields the current time. env e; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; MetaMorphoHarness.Id id; @@ -96,8 +96,6 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) { uint256 nextTime = nextCapIncreaseTime(e, id); uint184 prevCap = config_(id).cap; - // Sane assumption on the current time, as any following transaction should happen after it. - require e_next.block.timestamp >= e.block.timestamp; uint256 nextCapIncreaseTimeBeforeInteraction = nextCapIncreaseTime(e_next, id); // Increasing nextCapIncreaseTime with no interaction; assert nextCapIncreaseTimeBeforeInteraction >= nextTime; @@ -118,8 +116,6 @@ rule nextTimelockDecreaseTimeDoesNotRevert() { // The environment e yields the current time. env e; require e.msg.value == 0; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -135,8 +131,6 @@ rule nextTimelockDecreaseTimeDoesNotRevert() { rule timelockDecreaseTime(env e_next, method f, calldataarg args) { // The environment e yields the current time. env e; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -144,8 +138,6 @@ rule timelockDecreaseTime(env e_next, method f, calldataarg args) { uint256 nextTime = nextTimelockDecreaseTime(e); uint256 prevTimelock = timelock(); - // Sane assumption on the current time, as any following transaction should happen after it. - require e_next.block.timestamp >= e.block.timestamp; uint256 nextTimelockDecreaseTimeBeforeInteraction = nextTimelockDecreaseTime(e_next); // Increasing nextTimelockDecreaseTime with no interaction; assert nextTimelockDecreaseTimeBeforeInteraction >= nextTime; @@ -166,8 +158,6 @@ rule nextRemovableTimeDoesNotRevert(MetaMorphoHarness.Id id) { // The environment e yields the current time. env e; require e.msg.value == 0; - // Safe require as it corresponds to some time very far into the future. - require e.block.timestamp < 2^63; // Safe require because it is a verified invariant. require isTimelockInRange(); @@ -195,8 +185,6 @@ rule removableTime(env e_next, method f, calldataarg args) { // Assume that the market is enabled. require config_(id).enabled; - // Sane assumption on the current time, as any following transaction should happen after it. - require e_next.block.timestamp >= e.block.timestamp; uint256 nextRemovableTimeBeforeInteraction = nextRemovableTime(e_next, id); // Increasing nextRemovableTime with no interaction; assert nextRemovableTimeBeforeInteraction >= nextTime; From 70c44402b5cc79af5f6e14815e27705b20182c36 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 2 Apr 2024 12:06:11 +0200 Subject: [PATCH 2/6] feat: add not marked for removal on non enabled markets --- certora/specs/ConsistentState.spec | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index c9a20a75..be81fb49 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -61,6 +61,16 @@ function hasSupplyCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool invariant supplyCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) hasSupplyCapIsNotMarkedForRemoval(id); +function isNotEnabledIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool { + MetaMorphoHarness.MarketConfig config = config_(id); + + return !config.enabled => config.removableAt == 0; +} + +// Check that a non-enabled market cannot be marked for removal. +invariant notEnabledIsNotMarkedForRemoval(MetaMorphoHarness.Id id) + isNotEnabledIsNotMarkedForRemoval(id); + function hasPendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool { return pendingCap_(id).validAt > 0 => config_(id).removableAt == 0; } From 6a59f0e513dfbce16e503d33a78abf35bbccf624 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 2 Apr 2024 15:02:19 +0200 Subject: [PATCH 3/6] fix: persistent ghost lastTimestamp --- 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 7b471076..6c860d10 100644 --- a/certora/specs/Timelock.spec +++ b/certora/specs/Timelock.spec @@ -13,7 +13,7 @@ function summarySupplyshares(MetaMorphoHarness.Id id, address user) returns uint return res; } -ghost uint256 lastTimestamp; +persistent ghost uint256 lastTimestamp; hook TIMESTAMP uint v { // Safe require because timestamps are guaranteed to be increasing. From d43b5471be6904a0f0d6345a9b3d0c9f59329adb Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 2 Apr 2024 15:03:19 +0200 Subject: [PATCH 4/6] refactor: naming timestamp hook --- certora/specs/Timelock.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec index 6c860d10..e5d38c9b 100644 --- a/certora/specs/Timelock.spec +++ b/certora/specs/Timelock.spec @@ -15,12 +15,12 @@ function summarySupplyshares(MetaMorphoHarness.Id id, address user) returns uint persistent ghost uint256 lastTimestamp; -hook TIMESTAMP uint v { +hook TIMESTAMP uint newTimestamp { // Safe require because timestamps are guaranteed to be increasing. - require v >= lastTimestamp; + require newTimestamp >= lastTimestamp; // Safe require as it corresponds to some time very far into the future. - require v < 2^63; - lastTimestamp = v; + require newTimestamp < 2^63; + lastTimestamp = newTimestamp; } // Show that nextGuardianUpdateTime does not revert. From 9b2099f48efdefd6c8ba7fadddbeebeae7fb05c1 Mon Sep 17 00:00:00 2001 From: Jean-Grimal <83286814+Jean-Grimal@users.noreply.github.com> Date: Wed, 10 Apr 2024 16:08:14 +0200 Subject: [PATCH 5/6] fix: add SPDX identifier to ERC1820Registry.sol --- src/mocks/ERC1820Registry.sol | 1 + 1 file changed, 1 insertion(+) diff --git a/src/mocks/ERC1820Registry.sol b/src/mocks/ERC1820Registry.sol index 7b092e17..e73a6089 100644 --- a/src/mocks/ERC1820Registry.sol +++ b/src/mocks/ERC1820Registry.sol @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: GPL-2.0-or-later /** * Submitted for verification at Etherscan.io on 2019-04-03 */ From 7bbd846058c5eb0c8b044af12733f150c09aa6a8 Mon Sep 17 00:00:00 2001 From: Jean-Grimal <83286814+Jean-Grimal@users.noreply.github.com> Date: Thu, 11 Apr 2024 16:29:04 +0200 Subject: [PATCH 6/6] fix: remove CC0 line in EERC1820 registry.sol --- src/mocks/ERC1820Registry.sol | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/mocks/ERC1820Registry.sol b/src/mocks/ERC1820Registry.sol index e73a6089..4d69b106 100644 --- a/src/mocks/ERC1820Registry.sol +++ b/src/mocks/ERC1820Registry.sol @@ -12,9 +12,6 @@ * To the extent possible under law, the author(s) have dedicated all copyright and related and neighboring rights to * this software to the public domain worldwide. This software is distributed without any warranty. * - * You should have received a copy of the CC0 Public Domain Dedication along with this software. If not, see - * . - * * ███████╗██████╗ ██████╗ ██╗ █████╗ ██████╗ ██████╗ * ██╔════╝██╔══██╗██╔════╝███║██╔══██╗╚════██╗██╔═████╗ * █████╗ ██████╔╝██║ ╚██║╚█████╔╝ █████╔╝██║██╔██║