Closed 0x-r4bbit closed 1 month ago
We have a certoral rule in the making that currently looks like this:
rule stakingMintsMultiplierPoints1To1Ratio {
env e;
uint256 amount;
uint256 lockupTime;
uint256 multiplierPointsBefore;
uint256 multiplierPointsAfter;
requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender);
requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender);
multiplierPointsBefore = getAccountInitialMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime);
multiplierPointsAfter = getAccountInitialMultiplierPoints(e.msg.sender);
assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == multiplierPointsBefore + amount;
assert to_mathint(multiplierPointsAfter) >= multiplierPointsBefore + amount;
}
This relies on getAccountInitialMultiplier
to really always reflect the initial multiplier points (which is == stakeAmount
)
With the current implementation, this breaks. This increasingly seems to ask for initialMP
reflecting indeed the initalMP
without the increasedMP
.
Turns out there was a different issue with the rule above, so please ignore the comment.
The reason it was done that like in the current code is because if a lockup time is high enough, an account would immediately hit the max boost sealing.
This is a scenario we need to avoid - one should never hit the max boost by locking. I think we can work with the current approach, i.e. initialMP shifts the values by a fixed number and the varying part and limit is taken care of via the bonusMP counter.
However, we need to make sure the following logic is not distorted:
We're now always adding the bonusMP (the amount of MP for locking) to the max limit MP (without bonusMP). In other words, `maxPossibleMP = bonusMP + SNT staked * max MP multiplier
Currently, the maximum possible multiplier points amount for any account is calculated based on:
https://github.com/logos-co/staking/blob/4f590049d4cf79706dca86df20f3c0903c92ac95/contracts/StakeManager.sol#L416-L435
Specifically this line:
https://github.com/logos-co/staking/blob/4f590049d4cf79706dca86df20f3c0903c92ac95/contracts/StakeManager.sol#L427
_initialMP
is always going to be the initial multiplier points minted via the balance amount when staking, in addition to the bonus multiplier points for the stake lockup time.This results in the maximum multiplier points to be more than what's currently described in the docs
The reason it was done that like in the current code is because if a lockup time is high enough, an account would immediately hit the max boost sealing.
We can normalize this again by subtracking the account's
balance
from the implemented formula. We just need to decide./cc @3esmit @mart1n-xyz