This is actually a bug that the certora prover found.
The rule `epochStaysSameOnMigration` failed because a previous
`StakeManager` could call `migrationInitialize` and change
`currentEpoch` on a next `StakeManager`, even though the next `StakeManager`
might be in migration itself (which means the `currentEpoch` is now
allowed to change).
This commit fixes this by ensure `migrationInitialize()` will revert if
the `StakeManager` already has a `migration` on going.
Since we're implementing rules for `StakeManager` migrations, we need
multiple instances inside the certora specs.
This results in the prover trying to run rules on the other
`StakeManager` instance as well, which isn't always desired,
as it causes some rules to fail, even though they'd pass if they'd be
executed only on the `currentContract`.
This commit makes the filter condition for relevant rules stronger, such
that the prover will not run them on the `newStakeManager` contract
instance.
We've introduced a rule that finds counter examples for all functions
that changes balances. This rule will always fail by definition, so
we're commenting it out to get CI green again.
There have been a bunch of breaking changes in the staking contract that
resulted in our specs not compiling.
This commit fixes this, however it does not yet ensure the prover is
satisfied.
r4bbit
Ricardo Guilherme Schmidt
Nurit Dor