logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-02-03 06:13:43 +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-11-07 10:50:13 -03:00 committed by Ricardo Guilherme Schmidt
parent c0bf36d14b
commit df0257c343
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
certora/specs/StakeManager.spec
View File

@ -94,8 +94,14 @@ invariant highEpochsAreNull(uint256 epochNumber)
m -> !requiresPreviousManager(m) && !requiresNextManager(m) m -> !requiresPreviousManager(m) && !requiresNextManager(m)
} }
invariant accountBonusMPIsZeroIfBalanceIsZero(address addr) invariant accountMPIsZeroIfBalanceIsZero(address addr)
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0 to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
invariant InitialMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
filtered { filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
} }