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 bb31a4c80d
commit 450831a613
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 { rule rejectWhenMigrating(method f) filtered {
f -> blockedWhenMigrating(f) f -> blockedWhenMigrating(f) && f.contract == currentContract
} { } {
calldataarg args; calldataarg args;
env e; env e;
@ -68,7 +68,7 @@ rule allowWhenMigrating(method f) filtered {
rule rejectWhenNotMigrating(method f) filtered { rule rejectWhenNotMigrating(method f) filtered {
f -> blockedWhenNotMigrating(f) f -> blockedWhenNotMigrating(f) && f.contract == currentContract
} { } {
calldataarg args; calldataarg args;
env e; env e;
@ -103,8 +103,9 @@ rule startMigrationCorrect {
assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance(); assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
} }
rule migrationLockedIn { rule migrationLockedIn(method f) filtered {
method f; f -> !blockedWhenMigrating(f) && f.contract == currentContract
} {
env e; env e;
calldataarg args; calldataarg args;