logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-02-02 22:04:25 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(StakeManager.spec): fix spec to don't load totalMP greater than current sumOfMultipliers

Browse Source
This commit is contained in:
Ricardo Guilherme Schmidt 2024-10-03 00:24:12 -03:00
parent 9d7aa39d9b
commit f8d52e27e1
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
certora/specs/StakeManager.spec
View File

@ -60,6 +60,10 @@ hook Sstore accounts[KEY address addr].totalMP uint256 newValue (uint256 oldValu
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
}
hook Sload uint256 newValue accounts[KEY address addr].totalMP {
require sumOfBalances >= to_mathint(newValue);
}
invariant sumOfBalancesIsTotalSupplyBalance()
sumOfBalances == to_mathint(totalSupplyBalance())
filtered {