Skip to content

Commit

Permalink
refactor(StakeManager): initialMP -> bonusMP, currentMP -> totalMP
Browse files Browse the repository at this point in the history 
After discussing this offline, we've decided that the naming of these
properties was misleading. This commit performs the following changes:

- `account.initialMP` becomes `account.bonusMP`
- `account.currentMP` becomes `account.totalMP`

Rationale:

`initialMP` indicates that this is an immutable field which is not the
case as in scenarios where accounts increase the `lock()` time, they'll
also increase their bonus multiplier (`initialMP`).

`currentMP` was misleading in combination with `initialMP`. Really what
it reflects is the total multiplier points of an account **including**
its bonus multiplier points.
  • Loading branch information
@0x-r4bbit @3esmit
0x-r4bbit authored and 3esmit committed Jun 25, 2024
1 parent d18df07 commit 4a04b46
Show file tree
Hide file tree
Showing 3 changed files with 107 additions and 111 deletions.
30 changes: 15 additions & 15 deletions certora/specs/StakeManager.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,18 +23,18 @@ function getAccountBalance(address addr) returns uint256 {
return balance;
}

function getAccountInitialMultiplierPoints(address addr) returns uint256 {
uint256 initialMP;
_, _, initialMP, _, _, _, _ = accounts(addr);
function getAccountBonusMultiplierPoints(address addr) returns uint256 {
uint256 bonusMP;
_, _, bonusMP, _, _, _, _ = accounts(addr);

return initialMP;
return bonusMP;
}

function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
uint256 currentMP;
_, _, _, currentMP, _, _, _ = accounts(addr);
uint256 totalMP;
_, _, _, totalMP, _, _, _ = accounts(addr);

return currentMP;
return totalMP;
}

function getAccountLockUntil(address addr) returns uint256 {
Expand Down Expand Up @@ -91,7 +91,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
sumOfBalances = sumOfBalances - oldValue + newValue;
}

hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldValue) {
hook Sstore accounts[KEY address addr].totalMP uint256 newValue (uint256 oldValue) {
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
}

Expand Down Expand Up @@ -121,19 +121,19 @@ invariant highEpochsAreNull(uint256 epochNumber)
}

invariant InitialMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountInitialMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}

invariant CurrentMPIsNeverSmallerThanInitialMP(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountInitialMultiplierPoints(addr))
to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBonusMultiplierPoints(addr))
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}

invariant MPcantBeGreaterThanMaxMP(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountInitialMultiplierPoints(addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountBonusMultiplierPoints(addr)
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
Expand Down Expand Up @@ -164,9 +164,9 @@ rule stakingMintsMultiplierPoints1To1Ratio {

require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;

multiplierPointsBefore = getAccountInitialMultiplierPoints(e.msg.sender);
multiplierPointsBefore = getAccountBonusMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime);
multiplierPointsAfter = getAccountInitialMultiplierPoints(e.msg.sender);
multiplierPointsAfter = getAccountBonusMultiplierPoints(e.msg.sender);

assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == multiplierPointsBefore + amount;
assert to_mathint(multiplierPointsAfter) >= multiplierPointsBefore + amount;
Expand All @@ -184,10 +184,10 @@ rule stakingGreaterLockupTimeMeansGreaterMPs {
storage initalStorage = lastStorage;

stake(e, amount, lockupTime1);
multiplierPointsAfter1 = getAccountInitialMultiplierPoints(e.msg.sender);
multiplierPointsAfter1 = getAccountBonusMultiplierPoints(e.msg.sender);

stake(e, amount, lockupTime2) at initalStorage;
multiplierPointsAfter2 = getAccountInitialMultiplierPoints(e.msg.sender);
multiplierPointsAfter2 = getAccountBonusMultiplierPoints(e.msg.sender);

assert lockupTime1 >= lockupTime2 => to_mathint(multiplierPointsAfter1) >= to_mathint(multiplierPointsAfter2);
satisfy to_mathint(multiplierPointsAfter1) > to_mathint(multiplierPointsAfter2);
Expand Down
54 changes: 27 additions & 27 deletions contracts/StakeManager.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ contract StakeManager is Ownable {
struct Account {
address rewardAddress;
uint256 balance;
uint256 initialMP;
uint256 currentMP;
uint256 bonusMP;
uint256 totalMP;
uint256 lastMint;
uint256 lockUntil;
uint256 epoch;
Expand Down Expand Up @@ -157,7 +157,7 @@ contract StakeManager is Ownable {
revert StakeManager__InvalidLockTime();
}
}
_mintInitialMP(account, deltaTime, _amount);
_mintBonusMP(account, deltaTime, _amount);

//update storage
totalSupplyBalance += _amount;
Expand All @@ -184,13 +184,13 @@ contract StakeManager is Ownable {
}
_processAccount(account, currentEpoch);

uint256 reducedMP = Math.mulDiv(_amount, account.currentMP, account.balance);
uint256 reducedInitialMP = Math.mulDiv(_amount, account.initialMP, account.balance);
uint256 reducedMP = Math.mulDiv(_amount, account.totalMP, account.balance);
uint256 reducedInitialMP = Math.mulDiv(_amount, account.bonusMP, account.balance);

//update storage
account.balance -= _amount;
account.initialMP -= reducedInitialMP;
account.currentMP -= reducedMP;
account.bonusMP -= reducedInitialMP;
account.totalMP -= reducedMP;
totalSupplyBalance -= _amount;
totalSupplyMP -= reducedMP;
}
Expand Down Expand Up @@ -222,7 +222,7 @@ contract StakeManager is Ownable {
if (deltaTime < MIN_LOCKUP_PERIOD || deltaTime > MAX_LOCKUP_PERIOD) {
revert StakeManager__InvalidLockTime();
}
_mintInitialMP(account, _timeToIncrease, 0);
_mintBonusMP(account, _timeToIncrease, 0);
//update account storage
account.lockUntil = lockUntil;
}
Expand Down Expand Up @@ -322,7 +322,7 @@ contract StakeManager is Ownable {
{
_processAccount(accounts[msg.sender], currentEpoch);
Account memory account = accounts[msg.sender];
totalSupplyMP -= account.currentMP;
totalSupplyMP -= account.totalMP;
totalSupplyBalance -= account.balance;
delete accounts[msg.sender];
migration.migrateFrom(msg.sender, _acceptMigration, account);
Expand All @@ -340,7 +340,7 @@ contract StakeManager is Ownable {
if (_acceptMigration) {
accounts[_vault] = _account;
} else {
totalSupplyMP -= _account.currentMP;
totalSupplyMP -= _account.totalMP;
totalSupplyBalance -= _account.balance;
}
}
Expand All @@ -365,11 +365,11 @@ contract StakeManager is Ownable {
}
uint256 userReward;
uint256 userEpoch = account.epoch;
uint256 mpDifference = account.currentMP;
uint256 mpDifference = account.totalMP;
for (Epoch storage iEpoch = epochs[userEpoch]; userEpoch < _limitEpoch; userEpoch++) {
//mint multiplier points to that epoch
_mintMP(account, iEpoch.startTime + EPOCH_SIZE, iEpoch);
uint256 userSupply = account.balance + account.currentMP;
uint256 userSupply = account.balance + account.totalMP;
uint256 userEpochReward = Math.mulDiv(userSupply, iEpoch.epochReward, iEpoch.totalSupply);

userReward += userEpochReward;
Expand All @@ -381,7 +381,7 @@ contract StakeManager is Ownable {
pendingReward -= userReward;
stakedToken.transfer(account.rewardAddress, userReward);
}
mpDifference = account.currentMP - mpDifference;
mpDifference = account.totalMP - mpDifference;
if (address(migration) != address(0)) {
migration.increaseTotalMP(mpDifference);
} else if (userEpoch == currentEpoch) {
Expand All @@ -390,14 +390,14 @@ contract StakeManager is Ownable {
}

/**
* @notice Mint initial multiplier points for given staking amount and time
* @notice Mint bonus multiplier points for given staking amount and time
* @dev if amount is greater 0, it increases difference of amount for current remaining lock time
* @dev if increased lock time, increases difference of total new balance for increased lock time
* @param account Account to mint multiplier points
* @param increasedLockTime increased lock time
* @param amount amount to stake
*/
function _mintInitialMP(Account storage account, uint256 increasedLockTime, uint256 amount) private {
function _mintBonusMP(Account storage account, uint256 increasedLockTime, uint256 amount) private {
uint256 mpToMint;
if (amount > 0) {
mpToMint += amount; //initial multiplier points
Expand All @@ -413,8 +413,8 @@ contract StakeManager is Ownable {
}
//update storage
totalSupplyMP += mpToMint;
account.initialMP += mpToMint;
account.currentMP += mpToMint;
account.bonusMP += mpToMint;
account.totalMP += mpToMint;
account.lastMint = block.timestamp;
}

Expand All @@ -428,13 +428,13 @@ contract StakeManager is Ownable {
uint256 increasedMP = _getMaxMPToMint( //check for MAX_BOOST
_getMPToMint(account.balance, processTime - account.lastMint),
account.balance,
account.initialMP,
account.currentMP
account.bonusMP,
account.totalMP
);

//update storage
account.lastMint = processTime;
account.currentMP += increasedMP;
account.totalMP += increasedMP;
totalSupplyMP += increasedMP;
epoch.totalSupply += increasedMP;
}
Expand All @@ -443,25 +443,25 @@ contract StakeManager is Ownable {
* @notice Calculates maximum multiplier point increase for given balance
* @param _mpToMint tested value
* @param _balance balance of account
* @param _currentMP current multiplier point of the account
* @param _initialMP initial multiplier point of the account
* @param _totalMP total multiplier point of the account
* @param _bonusMP bonus multiplier point of the account
* @return _maxToIncrease maximum multiplier point increase
*/
function _getMaxMPToMint(
uint256 _mpToMint,
uint256 _balance,
uint256 _initialMP,
uint256 _currentMP
uint256 _bonusMP,
uint256 _totalMP
)
private
pure
returns (uint256 _maxToIncrease)
{
// Maximum multiplier point for given balance
_maxToIncrease = _getMPToMint(_balance, MAX_BOOST * YEAR) + _initialMP;
if (_mpToMint + _currentMP > _maxToIncrease) {
_maxToIncrease = _getMPToMint(_balance, MAX_BOOST * YEAR) + _bonusMP;
if (_mpToMint + _totalMP > _maxToIncrease) {
//reached cap when increasing MP
return _maxToIncrease - _currentMP; //how much left to reach cap
return _maxToIncrease - _totalMP; //how much left to reach cap
} else {
//not reached capw hen increasing MP
return _mpToMint; //just return tested value
Expand Down
Loading

0 comments on commit 4a04b46

Please sign in to comment.