From da007451a45c141348b5e6b56f111eb608e11f06 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 4 Mar 2024 16:23:47 +0100
Subject: [PATCH] fix(StakeManager): ensure `currentEpoch` is `0` when
 migrating

A previous manager can only migrate once, because the migration address
is locked in. A **new** manager is always aware of its previous manager.

This means, when a migration happens and is initialized, we know for
sure it's always the first time this is happening.

We probably don't want a migration to take place if the new manager has
already processed epochs, so we're adding a check that its
`currentEpoch` must be `0`.

This also ensures one of its invariants isn't violated:

`epochsOnlyIncrease` and `highEpochsAreNull`.
---
 certora/specs/StakeManager.spec | 5 +----
 contracts/StakeManager.sol      | 4 ++++
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 3def074..3026793 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -129,10 +129,7 @@ rule revertsWhenNoMigration(method f) {
 //   assert before == staked.balanceOf(user);
 // }
 
-rule epochOnlyIncreases(method f) filtered {
-  f -> f.selector != sig:migrationInitialize(uint256,uint256,uint256,uint256).selector;
-} {
-  method f;
+rule epochOnlyIncreases(method f) {
   env e;
   calldataarg args;
 
diff --git a/contracts/StakeManager.sol b/contracts/StakeManager.sol
index 42d4abc..486194e 100644
--- a/contracts/StakeManager.sol
+++ b/contracts/StakeManager.sol
@@ -19,6 +19,7 @@ contract StakeManager is Ownable {
     error StakeManager__InvalidLockupPeriod();
     error StakeManager__AccountNotInitialized();
     error StakeManager__InvalidMigration();
+    error StakeManager__AlreadyProcessedEpochs();
 
     struct Account {
         address rewardAddress;
@@ -254,6 +255,9 @@ contract StakeManager is Ownable {
         if (address(migration) != address(0)) {
             revert StakeManager__PendingMigration();
         }
+        if (currentEpoch > 0) {
+            revert StakeManager__AlreadyProcessedEpochs();
+        }
         currentEpoch = _currentEpoch;
         totalSupplyMP = _totalSupplyMP;
         totalSupplyBalance = _totalSupplyBalance;