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

chore(Certora specs): comment out purposefully failing rule 

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

21
certora/specs/StakeManager.spec
View File

@ -107,15 +107,18 @@ rule revertsWhenNoMigration(method f) {
assert isMigrationfunction(f) => reverted; assert isMigrationfunction(f) => reverted;
} }
rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked } // This rule is commented out as it's just a helper rule to easily see which
{ // functions change the balance of the `StakeManager` contract.
address user; //
uint256 before = staked.balanceOf(user); // rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked }
calldataarg args; // {
env e; // address user;
f(e,args); // uint256 before = staked.balanceOf(user);
assert before == staked.balanceOf(user); // calldataarg args;
} // env e;
// f(e,args);
// assert before == staked.balanceOf(user);
// }
rule epochOnlyIncreases { rule epochOnlyIncreases {
method f; method f;