3 Commits

Author	SHA1	Message	Date
r4bbit	450831a613	fix(Certora specs): ensure prover runs rules on currentContract ... 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.	2024-03-01 15:42:09 -03:00
r4bbit	109b684a2c	fix(Certora specs): make specs compile 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.	2024-03-01 13:17:45 +01:00
Ricardo Guilherme Schmidt	03bc6559ae	fix: StakeManager migration fixes and certora rules	2024-02-20 09:08:00 +01:00