logos-co
/
staking
mirror of https://github.com/logos-co/staking.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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`.
This commit is contained in:
r4bbit 2024-03-04 16:23:47 +01:00
parent c5d44380e7
commit 0d28141a98
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
certora/specs/StakeManager.spec
View File

@ -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;

4
contracts/StakeManager.sol
View File

@ -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;