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;