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
parent 109b684a2c
commit bb31a4c80d
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
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;