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

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.
This commit is contained in:
r4bbit 2024-03-01 10:42:11 +01:00 committed by Ricardo Guilherme Schmidt
parent 1c52edbbd9
commit 8d09f0b2dc
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
certora/specs/StakeManagerStartMigration.spec
View File

@ -41,7 +41,7 @@ definition blockedWhenNotMigrating(method f) returns bool = (
);
rule rejectWhenMigrating(method f) filtered {
f -> blockedWhenMigrating(f)
f -> blockedWhenMigrating(f) && f.contract == currentContract
} {
calldataarg args;
env e;
@ -68,7 +68,7 @@ rule allowWhenMigrating(method f) filtered {
rule rejectWhenNotMigrating(method f) filtered {
f -> blockedWhenNotMigrating(f)
f -> blockedWhenNotMigrating(f) && f.contract == currentContract
} {
calldataarg args;
env e;
@ -103,8 +103,9 @@ rule startMigrationCorrect {
assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
}
rule migrationLockedIn {
method f;
rule migrationLockedIn(method f) filtered {
f -> !blockedWhenMigrating(f) && f.contract == currentContract
} {
env e;
calldataarg args;