From e723464245c3450ad707ba0deb9dd3514a10e24c Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 4 Mar 2024 11:45:57 +0100
Subject: [PATCH] fix(StakeManager.spec): make `epochOnlyIncreases` rule pass

This was failing due to `migrationInitialize()` allowing for resetting
or decreasing a `StakeManager`s `currentEpoch`.

In practice, however, this is not possible because a new manager can
only be called from an old manager and the old manager can only migrate
once. So if `migrationInitialize()` is called from an old manager, we
can safely assume it's the first time this is called, meaning the new
manager's `currentEpoch` must be `0` at this point in time.
---
 certora/specs/StakeManager.spec | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index c1ab2b3..bd02388 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -119,7 +119,9 @@ rule revertsWhenNoMigration(method f) {
 //   assert before == staked.balanceOf(user);
 // }
 
-rule epochOnlyIncreases {
+rule epochOnlyIncreases(method f) filtered {
+  f -> f.selector != sig:migrationInitialize(uint256,uint256,uint256,uint256).selector;
+} {
   method f;
   env e;
   calldataarg args;