[Certora] Responsive guardian strategy

certora/README.md

@@ -75,6 +75,19 @@ function isSmallerPendingTimelock() returns bool {
 Notice how increasing the timelock is itself not subject to a timelock, as it does not increase the risk for the user.
 Indeed, a greater timelock means that the user would have more time to react to the vault's management operations that would not align with the user risk profile.
 
+### Responsive guardian
+
+Together, the verified rules entail the following property: if the guardian is responsive, then the curator cannot enact a change that is under timelock.
+It follows by induction on the sequence of transactions from the verified lemmas, given here for the example of a cap increase, but it also applies to the forced removal of a market.
+
+1. **Notice period.** The rule `capIncreaseTime` in [`Timelock.spec`](specs/Timelock.spec) shows that the cap cannot increase before `nextCapIncreaseTime`, and that no interaction can decrease this bound.
+2. **The guardian can always revoke.** The rule `revokePendingCapRevertCondition` in [`Reverts.spec`](specs/Reverts.spec) shows that `revokePendingCap` never reverts when called by the guardian.
+3. **Revocation resets the notice period.** The rule `capIncreaseTimeAfterRevoke` in [`Timelock.spec`](specs/Timelock.spec) shows that right after a revocation the cap cannot increase for one full timelock.
+
+Thus a guardian that checks the pending values at least once every timelock period and revokes the unwanted ones ensures that the cap never increases.
+
+The assumptions that the guardian stays in charge, and that a meaningful notice period is kept are self-sustaining: changing the guardian and the timelock are themselves under timelock and revocable, with the same lemmas verified (`guardianUpdateTime` and `timelockDecreaseTime` with their `AfterRevoke` and revert condition counterparts).
+
 ## Interactions with other contracts
 
 This section details how externals calls are checked to be scoped, which ensures the safety of MetaMorpho.

certora/specs/Timelock.spec

@@ -64,6 +64,16 @@ rule guardianUpdateTime(env e_next, method f, calldataarg args) {
     assert true;
 }
 
+// Show that revoking the pending guardian restarts a full timelock before any guardian change.
+rule guardianUpdateTimeAfterRevoke(env e) {
+    // Assume that there is no pending timelock, which the guardian can ensure by revoking it.
+    require pendingTimelock_().validAt == 0;
+
+    revokePendingGuardian(e);
+
+    assert nextGuardianUpdateTime(e) == e.block.timestamp + timelock();
+}
+
 // Show that nextCapIncreaseTime does not revert.
 rule nextCapIncreaseTimeDoesNotRevert(MetaMorphoHarness.Id id) {
     // The environment e yields the current time.
@@ -105,6 +115,16 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) {
     assert true;
 }
 
+// Show that revoking a pending cap restarts a full timelock before any cap increase.
+rule capIncreaseTimeAfterRevoke(env e, MetaMorphoHarness.Id id) {
+    // Assume that there is no pending timelock, which the guardian can ensure by revoking it.
+    require pendingTimelock_().validAt == 0;
+
+    revokePendingCap(e, id);
+
+    assert nextCapIncreaseTime(e, id) == e.block.timestamp + timelock();
+}
+
 // Show that nextTimelockDecreaseTime does not revert.
 rule nextTimelockDecreaseTimeDoesNotRevert() {
     // The environment e yields the current time.
@@ -144,6 +164,13 @@ rule timelockDecreaseTime(env e_next, method f, calldataarg args) {
     assert true;
 }
 
+// Show that revoking the pending timelock restarts a full timelock before any timelock decrease.
+rule timelockDecreaseTimeAfterRevoke(env e) {
+    revokePendingTimelock(e);
+
+    assert nextTimelockDecreaseTime(e) == e.block.timestamp + timelock();
+}
+
 // Show that nextRemovableTime does not revert.
 rule nextRemovableTimeDoesNotRevert(MetaMorphoHarness.Id id) {
     // The environment e yields the current time.
@@ -187,3 +214,13 @@ rule removableTime(env e_next, method f, calldataarg args) {
     }
     assert true;
 }
+
+// Show that revoking a pending market removal restarts a full timelock before any forced removal.
+rule removableTimeAfterRevoke(env e, MetaMorphoHarness.Id id) {
+    // Assume that there is no pending timelock, which the guardian can ensure by revoking it.
+    require pendingTimelock_().validAt == 0;
+
+    revokePendingMarketRemoval(e, id);
+
+    assert nextRemovableTime(e, id) == e.block.timestamp + timelock();
+}