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-10-03 00:24:13 -03:00 committed by Ricardo Guilherme Schmidt
parent fc3578ee48
commit c0bf36d14b
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
certora/specs/StakeManager.spec
View File

@ -75,6 +75,11 @@ invariant sumOfMultipliersIsMultiplierSupply()
filtered { filtered {
m -> !requiresPreviousManager(m) && !requiresNextManager(m) m -> !requiresPreviousManager(m) && !requiresNextManager(m)
} }
{ preserved with (env e){
requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
requireInvariant accountBonusMPIsZeroIfBalanceIsZero(e.msg.sender);
}
}
invariant sumOfEpochRewardsIsPendingRewards() invariant sumOfEpochRewardsIsPendingRewards()
sumOfEpochRewards == to_mathint(currentContract.pendingReward) sumOfEpochRewards == to_mathint(currentContract.pendingReward)