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

fix(specs): make `sumOfMultiplierPointsIsMultiplierpoints` work again 

This invariant failed as the prover started making wrong assumptions
about the relationship between anyone's account's `totalMP` and its
`balance`, as well as an account's `bonusMP` and its `balance`.

This commit fixes it by adding the necessary invariants to proof the
property.
This commit is contained in:
r4bbit 2024-11-07 10:50:13 -03:00 committed by Ricardo Guilherme Schmidt
parent df0257c343
commit feb6dd1530
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
certora/specs/StakeManager.spec
View File

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