logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-01-10 18:56:00 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix(certora): exclude stake() from rule that checks account balance

Browse Source 
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

Also this commit adds an invariant:

add invariant that account balance == 0 => accountMP == 0
This commit is contained in:
r4bbit 2024-10-03 00:24:12 -03:00 committed by Ricardo Guilherme Schmidt
parent a34ae066a3
commit 9d7aa39d9b
2 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
certora/specs/StakeManager.spec
View File

@ -115,6 +115,7 @@ rule stakingMintsMultiplierPoints1To1Ratio {
requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender);
requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender);
requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;

2
certora/specs/StakeManagerProcessAccount.spec
View File

@ -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;