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

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

This commit is contained in:
Ricardo Guilherme Schmidt 2024-09-28 17:51:51 -03:00
parent 41b43621f7
commit fefc4dc4f0
No known key found for this signature in database
GPG Key ID: 54B4454CC123AD17
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; sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
} }
hook Sload uint256 newValue accounts[KEY address addr].totalMP {
require sumOfBalances >= to_mathint(newValue);
}
invariant sumOfBalancesIsTotalSupplyBalance() invariant sumOfBalancesIsTotalSupplyBalance()
sumOfBalances == to_mathint(totalSupplyBalance()) sumOfBalances == to_mathint(totalSupplyBalance())
filtered { filtered {