logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-01-25 18:09:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix(StakeManager.spec): make epochOnlyIncreases rule pass

Browse Source 
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.
This commit is contained in:
r4bbit 2024-03-04 11:45:57 +01:00
parent 50c8a11d5d
commit 9bfcb0710e
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
certora/specs/StakeManager.spec
View File

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