Skip to content

Commit

Permalink
fix(certora): exclude stake() from rule that checks account balance
Browse files Browse the repository at this point in the history
change

The rule is failing since we've removed the `lockUntil > 0` check in
`stake` and `processAccount` is no longer used in `stake()`.
The rule requires `lockUntil > 0` so it will always fail there and can't
find a non-reverting cases (which makes the rule pass).

The reason it hasn't happened before was because:

The rule required account.lockUntil > 0
Stake required lockUntil > 0 || account balance == 0
  • Loading branch information
0x-r4bbit committed Sep 27, 2024
1 parent ad6328d commit 28881ec
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion certora/specs/StakeManagerProcessAccount.spec
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8
*/
rule checkAccountProcessedBeforeStoring(method f) filtered {
f -> !requiresPreviousManager(f) && !requiresNextManager(f)
f -> !requiresPreviousManager(f) && !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector
} {
address account;

Expand Down

0 comments on commit 28881ec

Please sign in to comment.