From cb81a7609cb2b26c07bd9abc6a182c5fe46d2f72 Mon Sep 17 00:00:00 2001 From: Ricardo Guilherme Schmidt <3esmit@gmail.com> Date: Mon, 25 Nov 2024 12:24:09 -0300 Subject: [PATCH] refactor(certora): Reorganize files, add proper descriptions, fix conf files and add summaries --- certora/confs/MaxMPRule.conf | 4 +- certora/confs/StakeManager.conf | 4 +- certora/confs/StakeManagerProcess.conf | 4 +- certora/confs/StakeManagerStartMigration.conf | 6 +- certora/confs/StakeVault.conf | 4 +- certora/specs/EpochMath.spec | 29 + certora/specs/IStakeManager.spec | 136 ++ certora/specs/MaxMPRule.spec | 51 +- .../specs/MultiplierPointsMathSummarized.spec | 64 + certora/specs/StakeManager.spec | 45 +- certora/specs/StakeManagerProcessAccount.spec | 12 +- certora/specs/StakeManagerStartMigration.spec | 46 +- certora/specs/StakeMath.spec | 95 ++ certora/specs/StakeVault.spec | 23 +- certora/specs/definition/DefinitionEpoch.spec | 6 + certora/specs/definition/DefinitionMath.spec | 17 + .../DefinitionMultiplierPointsMath.spec | 29 + certora/specs/definition/DefinitionTime.spec | 5 + certora/specs/math/OpenZeppelinMath.spec | 44 + certora/specs/shared.spec | 70 -- certora/specs/token/ERC20.spec | 12 + docs/MathSpec.md | 1095 +++++++++++++++++ docs/StakeManager.ipynb | 1095 +++++++++++++++++ package.json | 2 +- 24 files changed, 2725 insertions(+), 173 deletions(-) create mode 100644 certora/specs/EpochMath.spec create mode 100644 certora/specs/IStakeManager.spec create mode 100644 certora/specs/MultiplierPointsMathSummarized.spec create mode 100644 certora/specs/StakeMath.spec create mode 100644 certora/specs/definition/DefinitionEpoch.spec create mode 100644 certora/specs/definition/DefinitionMath.spec create mode 100644 certora/specs/definition/DefinitionMultiplierPointsMath.spec create mode 100644 certora/specs/definition/DefinitionTime.spec create mode 100644 certora/specs/math/OpenZeppelinMath.spec delete mode 100644 certora/specs/shared.spec create mode 100644 certora/specs/token/ERC20.spec create mode 100644 docs/MathSpec.md create mode 100644 docs/StakeManager.ipynb diff --git a/certora/confs/MaxMPRule.conf b/certora/confs/MaxMPRule.conf index 315d95f..960f3b1 100644 --- a/certora/confs/MaxMPRule.conf +++ b/certora/confs/MaxMPRule.conf @@ -6,9 +6,9 @@ ], "link": [ "StakeManager:REWARD_TOKEN=ERC20A", - "StakeManager:expiredStakeStorage=ExpiredStakeStorageA" + "StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA" ], - "msg": "Verifying StakeManager.sol maxMP rule", + "msg": "StakeManager:MaxMP", "rule_sanity": "basic", "verify": "StakeManager:certora/specs/MaxMPRule.spec", "optimistic_loop": true, diff --git a/certora/confs/StakeManager.conf b/certora/confs/StakeManager.conf index 6fc3a00..99d5cfc 100644 --- a/certora/confs/StakeManager.conf +++ b/certora/confs/StakeManager.conf @@ -6,9 +6,9 @@ ], "link": [ "StakeManager:REWARD_TOKEN=ERC20A", - "StakeManager:expiredStakeStorage=ExpiredStakeStorageA" + "StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA" ], - "msg": "Verifying StakeManager.sol", + "msg": "StakeManager", "rule_sanity": "basic", "verify": "StakeManager:certora/specs/StakeManager.spec", "optimistic_loop": true, diff --git a/certora/confs/StakeManagerProcess.conf b/certora/confs/StakeManagerProcess.conf index 1c45e5b..d23eb5c 100644 --- a/certora/confs/StakeManagerProcess.conf +++ b/certora/confs/StakeManagerProcess.conf @@ -6,9 +6,9 @@ ], "link": [ "StakeManager:REWARD_TOKEN=ERC20A", - "StakeManager:expiredStakeStorage=ExpiredStakeStorageA" + "StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA" ], - "msg": "Verifying StakeManager ProcessAccount", + "msg": "StakeManager:ProcessAccount", "rule_sanity": "basic", "verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec", "optimistic_loop": true, diff --git a/certora/confs/StakeManagerStartMigration.conf b/certora/confs/StakeManagerStartMigration.conf index bafb372..6f49e9b 100644 --- a/certora/confs/StakeManagerStartMigration.conf +++ b/certora/confs/StakeManagerStartMigration.conf @@ -1,15 +1,15 @@ { "files": [ "contracts/StakeManager.sol", - "certora/harness/StakeManagerNew.sol", + "contracts/StakeManagerUpdated.sol", "certora/helpers/ExpiredStakeStorageA.sol", "certora/helpers/ERC20A.sol" ], "link": [ "StakeManager:REWARD_TOKEN=ERC20A", - "StakeManager:expiredStakeStorage=ExpiredStakeStorageA" + "StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA" ], - "msg": "Verifying StakeManager.sol", + "msg": "StakeManager:Migration", "rule_sanity": "basic", "verify": "StakeManager:certora/specs/StakeManagerStartMigration.spec", "optimistic_loop": true, diff --git a/certora/confs/StakeVault.conf b/certora/confs/StakeVault.conf index 04b5f84..cc93bf8 100644 --- a/certora/confs/StakeVault.conf +++ b/certora/confs/StakeVault.conf @@ -8,10 +8,10 @@ "link": [ "StakeVault:STAKING_TOKEN=ERC20A", "StakeManager:REWARD_TOKEN=ERC20A", - "StakeManager:expiredStakeStorage=ExpiredStakeStorageA", + "StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA", "StakeVault:stakeManager=StakeManager" ], - "msg": "Verifying StakeVault.sol", + "msg": "StakeVault", "rule_sanity": "basic", "verify": "StakeVault:certora/specs/StakeVault.spec", "optimistic_loop": true, diff --git a/certora/specs/EpochMath.spec b/certora/specs/EpochMath.spec new file mode 100644 index 0000000..56a811a --- /dev/null +++ b/certora/specs/EpochMath.spec @@ -0,0 +1,29 @@ +import "./definition/DefinitionEpoch.spec"; + +methods { + function EpochMath._calculateMPPrediction(uint256 _balance, uint256 _accountEpoch, uint256 _deltaTime) internal returns (uint256, uint256, uint256, uint256) => calculateMPPredictionSummary(_balance, _accountEpoch, _deltaTime); + function EpochMath._calculateNewStartTime(uint256 _balance, uint256 _totalMP,uint256 _maxMP, uint256 _processTime) internal returns (uint256) => calculateNewStartTime( _balance, _totalMP, _maxMP, _processTime); +} + +function calculateMPPredictionSummary(uint256 _balance, uint256 _accountEpoch, uint256 _deltaTime) returns (uint256, uint256, uint256, uint256) { + require _balance >= A_MIN(); + uint256 mpRate = require_uint256(accrueMP(_balance, T_RATE())); + uint256 mpFractional = require_uint256(mpRate - accrueMP(_balance, _deltaTime)); + + mathint mpTarget = maxAccrueMP(_balance) + mpFractional; + mathint deltaEpochTarget1 = mpTarget / mpRate; + + uint256 epochTarget1 = require_uint256(_accountEpoch + deltaEpochTarget1); + uint256 mpRemainder; + if (mpTarget % mpRate > 0) { + mpRemainder = require_uint256((mpRate * (deltaEpochTarget1 + 1)) - mpTarget); + } else { + mpRemainder = 0; + } + return (mpRate, mpFractional, epochTarget1, mpRemainder); +} + + +function calculateNewStartTime(uint256 _balance, uint256 _totalMP,uint256 _maxMP, uint256 _processTime) returns uint256 { + return require_uint256(_processTime - timeToAccrueMP(_balance, retrieveAccruedMP(_balance, _totalMP, _maxMP))); +} diff --git a/certora/specs/IStakeManager.spec b/certora/specs/IStakeManager.spec new file mode 100644 index 0000000..e5e7fed --- /dev/null +++ b/certora/specs/IStakeManager.spec @@ -0,0 +1,136 @@ +import "./definition/DefinitionEpoch.spec"; + +methods { + function potentialMP() external returns (uint256) envfree; + function START_TIME() external returns (uint256) envfree; + function currentEpoch() external returns (uint256) envfree; + function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree; + function totalStaked() external returns (uint256) envfree; + function totalMP() external returns (uint256) envfree; + function getEpochStartTime(uint256) external returns (uint256) envfree; + function totalMPRate() external returns (uint256) envfree; + function getEpoch(uint) external returns (uint256) envfree; + function MIN_LOCKUP_PERIOD() external returns (uint256) envfree; + function MAX_LOCKUP_PERIOD() external returns (uint256) envfree; + function YEAR() external returns (uint256) envfree; + function MAX_MULTIPLIER() external returns (uint256) envfree; + function MP_APY() external returns (uint256) envfree; + function MP_MPY() external returns (uint256) envfree; + function MP_MPY_ABSOLUTE() external returns (uint256) envfree; + function ACCURE_RATE() external returns (uint256) envfree; + function MIN_BALANCE() external returns (uint256) envfree; +} + +definition requiresNextManager(method f) returns bool = ( + f.selector == sig:acceptUpdate().selector || + f.selector == sig:leave().selector || + f.selector == sig:transferNonPending().selector + ); + + +function requireValidSystem(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch, uint256 _maxEpochsToProcess) { + require _globalStartTime > 0; + require _processTime >= START_TIME(); + mathint newEpoch = epoch(_processTime, _globalStartTime); + require _globalEpoch <= newEpoch; + require newEpoch - _globalEpoch <= _maxEpochsToProcess; +} + +function simplifyEpochProcessing(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch) { + require _processTime == _globalStartTime; + require _globalEpoch == 0; +} + +function requireValidAccount(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch, address _addr, uint256 _maxEpochsToProcess) { + address rewardAddress; + uint256 balance; + uint256 maxMP; + uint256 totalMP; + uint256 lastMint; + uint256 lockUntil; + uint256 accountEpoch; + uint256 accountStartTime; + rewardAddress, balance, maxMP, totalMP, lastMint, lockUntil, accountEpoch, accountStartTime = accounts(_addr); + + if(balance > 0){ + require balance >= MIN_BALANCE(); + require lastMint >= _globalStartTime; + require lastMint <= _processTime; + require lastMint < epochStart(accountEpoch+1, _globalStartTime); + require accountStartTime >= _globalStartTime; + require accountStartTime <= lastMint; + require lockUntil >= accountStartTime; + require accountEpoch <= _globalEpoch; + require accountEpoch >= _globalEpoch - _maxEpochsToProcess; + mathint lockTime = lockUntil - accountStartTime; + require maxMP > maxTotalMP(balance, lockTime); + require totalMP <= maxMP; + } else { + require accountStartTime == 0; + require lastMint == 0; + require rewardAddress == 0; + require maxMP == 0; + require totalMP == 0; + require lockUntil == 0; + require accountEpoch == 0; + } +} + +function requireValidState(env e, uint256 _maxEpochsToProcess) { + uint256 processTime = e.block.timestamp; + address addr = e.msg.sender; + uint256 globalEpoch = currentEpoch(); + uint256 globalStartTime = START_TIME(); + requireValidSystem(processTime, globalStartTime, globalEpoch, _maxEpochsToProcess); + requireValidAccount(processTime, globalStartTime, globalEpoch, addr, _maxEpochsToProcess); +} +/** +struct Account { + address rewardAddress; + uint256 balance; + uint256 maxMP; + uint256 totalMP; + uint256 lastMint; + uint256 lockUntil; + uint256 accountEpoch; + uint256 _globalStartTime; + } +**/ + + +function getAccountBalance(address _addr) returns uint256 { + uint256 balance; + _, balance, _, _, _, _, _, _ = accounts(_addr); + return balance; +} + + +function getAccountLastMint(address _addr) returns uint256 { + uint256 lastMint; + _, _, _, _, lastMint, _, _, _ = accounts(_addr); + return lastMint; +} + +function getAccountMaxMPs(address _addr) returns uint256 { + uint256 maxMP; + _, _, maxMP, _, _, _, _, _ = accounts(_addr); + return maxMP; +} + +function getAccountTotalMPs(address _addr) returns uint256 { + uint256 totalMP; + _, _, _, totalMP, _, _, _, _ = accounts(_addr); + return totalMP; +} + +function getAccountLockUntil(address _addr) returns uint256 { + uint256 lockUntil; + _, _, _, _, _, lockUntil, _, _ = accounts(_addr); + return lockUntil; +} + +function getAccountEpoch(address _addr) returns uint256 { + uint256 accountEpoch; + _, _, _, _, _, _, accountEpoch, _ = accounts(_addr); + return accountEpoch; +} \ No newline at end of file diff --git a/certora/specs/MaxMPRule.spec b/certora/specs/MaxMPRule.spec index 6ae51f1..c2414c4 100644 --- a/certora/specs/MaxMPRule.spec +++ b/certora/specs/MaxMPRule.spec @@ -1,42 +1,27 @@ -import "./shared.spec"; +import "./math/OpenZeppelinMath.spec"; +import "./EpochMath.spec"; +import "./IStakeManager.spec"; +import "./MultiplierPointsMathSummarized.spec"; -methods { - function startTime() external returns (uint256) envfree; - function currentEpoch() external returns (uint256) envfree; + +invariant MaxMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr)) + { preserved with (env e) { + requireValidState(e, 2); + } } -function simplifyEpochProcessing(env e){ - require e.block.timestamp == _stakeManager.startTime(); - require _stakeManager.currentEpoch() == 0; -} - -/* TODO: very usage of CONSTANT with Math.mulDiv or simplify mulDiv somehow, and replace simplifyEpochProcessing with reduceEpochProcessing - -function reduceEpochProcessing(env e, uint256 maxEpochs) { - require e.block.timestamp >= _stakeManager.startTime(); - uint256 currentEpoch = _stakeManager.currentEpoch(); - uint256 newEpoch = _stakeManager.newEpoch(e); - require currentEpoch <= newEpoch; - require currentEpoch - newEpoch <= maxEpochs; -} - -function reduceAccountProcessing(env e, address addr, uint256 maxEpochs) { - uint256 currentEpoch = _stakeManager.currentEpoch(); - uint256 accountEpoch = getAccountEpoch(addr); - require accountEpoch <= currentEpoch; - require accountEpoch >= currentEpoch - maxEpochs; -} -*/ +invariant CurrentMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr)) + { preserved with (env e) { + requireValidState(e, 2); + } + } invariant MPcantBeGreaterThanMaxMP(address addr) - to_mathint(getAccountCurrentMultiplierPoints(addr)) <= to_mathint(getAccountMaxMultiplierPoints(addr)) - filtered { - f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector - } + to_mathint(getAccountTotalMPs(addr)) <= to_mathint(getAccountMaxMPs(addr)) { preserved with (env e) { - simplifyEpochProcessing(e); - /*reduceEpochProcessing(e, 3); - reduceAccountProcessing(e, addr, 3);*/ + requireValidState(e, 2); requireInvariant MaxMPIsNeverSmallerThanBalance(addr); requireInvariant CurrentMPIsNeverSmallerThanBalance(addr); } diff --git a/certora/specs/MultiplierPointsMathSummarized.spec b/certora/specs/MultiplierPointsMathSummarized.spec new file mode 100644 index 0000000..558a1db --- /dev/null +++ b/certora/specs/MultiplierPointsMathSummarized.spec @@ -0,0 +1,64 @@ +import "./definition/DefinitionMultiplierPointsMath.spec"; + +methods { + function MultiplierPointMath._accrueMP(uint256 _balance, uint256 _deltaTime) internal returns (uint256) => accrueMPSummary(_balance, _deltaTime) ; + function MultiplierPointMath._bonusMP(uint256 _balance, uint256 _lockedSeconds) internal returns (uint256) => bonusMPSummary(_balance, _lockedSeconds); + function MultiplierPointMath._initialMP(uint256 _balance) internal returns (uint256) => initialMPSummary(_balance); + function MultiplierPointMath._reduceMP(uint256 _balance, uint256 _mp, uint256 _reducedAmount) internal returns (uint256) => reduceMPSummary(_balance, _mp, _reducedAmount); + function MultiplierPointMath._maxAccrueMP(uint256 _balance) internal returns (uint256) => maxAccrueMPSummary(_balance); + function MultiplierPointMath._maxTotalMP(uint256 _balance, uint256 _lockTime) internal returns (uint256) => maxTotalMPSummary(_balance, _lockTime) ; + function MultiplierPointMath._maxAbsoluteMP(uint256 _balance) internal returns (uint256) => maxAbsoluteMPSummary(_balance); + function MultiplierPointMath._lockTimeAvailable(uint256 _balance, uint256 _mpMax) internal returns (uint256) => lockTimeAvailableSummary(_balance, _mpMax); + function MultiplierPointMath._timeToAccrueMP(uint256 _balance, uint256 _mp) internal returns (uint256) => timeToAccrueMPSummary(_balance, _mp); + function MultiplierPointMath._retrieveBonusMP(uint256 _balance, uint256 _maxMP) internal returns (uint256) => retrieveBonusMPSummary(_balance, _maxMP); + function MultiplierPointMath._retrieveAccruedMP(uint256 _balance, uint256 _totalMP, uint256 _maxMP) internal returns (uint256) => retrieveAccruedMPSummary(_balance, _totalMP, _maxMP); +} + +function accrueMPSummary(uint256 _balance, uint256 _deltaTime) returns uint256 { + return require_uint256(accrueMP(_balance, _deltaTime)); +} + +function bonusMPSummary(uint256 _balance, uint256 _lockedSeconds) returns uint256 { + return require_uint256(bonusMP(_balance, _lockedSeconds)); +} + +function initialMPSummary(uint256 _balance) returns uint256 { + return _balance; +} + +function reduceMPSummary( + uint256 _balance, + uint256 _mp, + uint256 _reducedAmount +) returns uint256 { + return require_uint256(reduceMP(_balance,_mp,_reducedAmount)); +} + +function maxAccrueMPSummary(uint256 _balance) returns uint256 { + return require_uint256(maxAccrueMP(_balance)); +} + +function maxTotalMPSummary(uint256 _balance, uint256 _lockTime) returns uint256 { + return require_uint256(maxTotalMP(_balance, _lockTime)); +} + +function maxAbsoluteMPSummary(uint256 _balance) returns uint256 { + return require_uint256(maxAbsoluteMP(_balance)); +} + +function lockTimeAvailableSummary( + uint256 _balance, + uint256 _mpMax +) returns uint256 { + return require_uint256(lockTimeAvailable(_balance, _mpMax)); +} + +function timeToAccrueMPSummary(uint256 _balance, uint256 _mp) returns uint256 { + return require_uint256(timeToAccrueMP(_balance, _mp)); +} +function retrieveBonusMPSummary(uint256 _balance, uint256 _maxMP) returns uint256 { + return require_uint256(retrieveBonusMP(_balance, _maxMP)); +} +function retrieveAccruedMPSummary(uint256 _balance, uint256 _totalMP, uint256 _maxMP) returns uint256 { + return require_uint256(retrieveAccruedMP(_balance, _totalMP, _maxMP)); +} \ No newline at end of file diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index e6dbfef..992def9 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -1,15 +1,15 @@ -import "./shared.spec"; +import "./definition/DefinitionMath.spec"; +import "./definition/DefinitionMultiplierPointsMath.spec"; +import "./math/OpenZeppelinMath.spec"; +import "./IStakeManager.spec"; using ERC20A as staked; +using StakeManager as _stakeManager; methods { function staked.balanceOf(address) external returns (uint256) envfree; function totalStaked() external returns (uint256) envfree; function totalMP() external returns (uint256) envfree; - function previousManager() external returns (address) envfree; - function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET; - function _.increaseTotalMP(uint256) external => NONDET; - function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET; function _._ external => DISPATCH [] default NONDET; } @@ -24,7 +24,6 @@ function isMigrationfunction(method f) returns bool { cases where it is zero. specifically no externall call to the migration contract */ function simplification(env e) { require currentContract.migration == 0; - require currentContract.previousManager() == 0; require e.msg.sender != 0; } @@ -58,16 +57,22 @@ hook Sload uint256 newValue accounts[KEY address addr].totalMP { require sumOfMultipliers >= to_mathint(newValue); } +invariant MaxMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr)); + +invariant CurrentMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr)); + invariant sumOfBalancesIsTotalSupplyBalance() sumOfBalances == to_mathint(totalStaked()) filtered { - m -> !requiresPreviousManager(m) && !requiresNextManager(m) + m -> !requiresNextManager(m) } invariant sumOfMultipliersIsMultiplierSupply() sumOfMultipliers == to_mathint(totalMP()) filtered { - m -> !requiresPreviousManager(m) && !requiresNextManager(m) + m -> !requiresNextManager(m) } { preserved with (env e){ requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); @@ -85,20 +90,14 @@ invariant sumOfEpochRewardsIsPendingRewards() invariant highEpochsAreNull(uint256 epochNumber) epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0 filtered { - m -> !requiresPreviousManager(m) && !requiresNextManager(m) + m -> !requiresNextManager(m) } invariant accountMaxMPIsZeroIfBalanceIsZero(address addr) - to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountMaxMultiplierPoints(addr)) == 0 - filtered { - f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector - } + to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountMaxMPs(addr)) == 0; invariant accountMPIsZeroIfBalanceIsZero(address addr) - to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0 - filtered { - f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector - } + to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountTotalMPs(addr)) == 0; rule reachability(method f) { @@ -122,12 +121,12 @@ rule stakingMintsMultiplierPoints1To1Ratio { require getAccountLockUntil(e.msg.sender) <= e.block.timestamp; - multiplierPointsBefore = getAccountMaxMultiplierPoints(e.msg.sender); + multiplierPointsBefore = getAccountMaxMPs(e.msg.sender); stake(e, amount, lockupTime); - multiplierPointsAfter = getAccountMaxMultiplierPoints(e.msg.sender); -// + multiplierPointsAfter = getAccountMaxMPs(e.msg.sender); + assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == amount * 5; - assert to_mathint(multiplierPointsAfter) == to_mathint(amount + ((amount * 100) * ((4 * 31556925) + lockupTime)) / (31556925 * 100)); + assert to_mathint(multiplierPointsAfter) == maxTotalMP(amount, lockupTime); } rule stakingGreaterLockupTimeMeansGreaterMPs { @@ -142,10 +141,10 @@ rule stakingGreaterLockupTimeMeansGreaterMPs { storage initalStorage = lastStorage; stake(e, amount, lockupTime1); - maxMPAfter1 = getAccountMaxMultiplierPoints(e.msg.sender); + maxMPAfter1 = getAccountMaxMPs(e.msg.sender); stake(e, amount, lockupTime2) at initalStorage; - maxMPAfter2 = getAccountMaxMultiplierPoints(e.msg.sender); + maxMPAfter2 = getAccountMaxMPs(e.msg.sender); assert lockupTime1 >= lockupTime2 => to_mathint(maxMPAfter1) >= to_mathint(maxMPAfter2); satisfy to_mathint(maxMPAfter1) > to_mathint(maxMPAfter2); diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec index 30bde55..4dd23bb 100644 --- a/certora/specs/StakeManagerProcessAccount.spec +++ b/certora/specs/StakeManagerProcessAccount.spec @@ -1,16 +1,10 @@ -import "./shared.spec"; +import "./IStakeManager.spec"; using ERC20A as staked; methods { function staked.balanceOf(address) external returns (uint256) envfree; - function totalStaked() external returns (uint256) envfree; - function totalMP() external returns (uint256) envfree; - function totalMPRate() external returns (uint256) envfree; - - function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch); - function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET; - function potentialMP() external returns (uint256) envfree; + function _processAccount(IStakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch); } // keeps track of the last epoch an account was processed @@ -35,7 +29,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8 */ rule checkAccountProcessedBeforeStoring(method f) filtered { - f -> !requiresPreviousManager(f) && !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector + f -> !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector && f.selector != sig:startMigration(address).selector } { address account; diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec index 0a15f02..d7a24ed 100644 --- a/certora/specs/StakeManagerStartMigration.spec +++ b/certora/specs/StakeManagerStartMigration.spec @@ -1,27 +1,49 @@ -import "./shared.spec"; +import "./IStakeManager.spec"; using ERC20A as staked; -using StakeManagerNew as newStakeManager; +using StakeManagerUpdated as newStakeManager; methods { function staked.balanceOf(address) external returns (uint256) envfree; function totalStaked() external returns (uint256) envfree; function totalMP() external returns (uint256) envfree; - function previousManager() external returns (address) envfree; + function newStakeManager.PREVIOUS_MANAGER() external returns (address) envfree; function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => DISPATCHER(true); - function StakeManagerNew.totalStaked() external returns (uint256) envfree; + function newStakeManager.totalStaked() external returns (uint256) envfree; } + +invariant MaxMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr)) + filtered { + f -> f.selector != sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector + } + +invariant CurrentMPIsNeverSmallerThanBalance(address addr) + to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr)) + filtered { + f -> f.selector != sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector + } + + + +definition requiresPreviousManager(method f) returns bool = ( + f.selector == sig:StakeManagerUpdated.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || + f.selector == sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector || + f.selector == sig:StakeManagerUpdated.increaseTotalMP(uint256).selector +); + + definition blockedWhenMigrating(method f) returns bool = ( - f.selector == sig:stake(uint256, uint256).selector || - f.selector == sig:unstake(uint256).selector || - f.selector == sig:lock(uint256).selector || - f.selector == sig:executeEpoch().selector || - f.selector == sig:executeEpoch(uint256).selector || - f.selector == sig:startMigration(address).selector || - f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector - ); + f.selector == sig:stake(uint256, uint256).selector || + f.selector == sig:unstake(uint256).selector || + f.selector == sig:lock(uint256).selector || + f.selector == sig:executeEpoch().selector || + f.selector == sig:executeEpoch(uint256).selector || + f.selector == sig:startMigration(address).selector || + f.selector == sig:StakeManagerUpdated.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector +); definition blockedWhenNotMigrating(method f) returns bool = ( f.selector == sig:acceptUpdate().selector || diff --git a/certora/specs/StakeMath.spec b/certora/specs/StakeMath.spec new file mode 100644 index 0000000..985fbb0 --- /dev/null +++ b/certora/specs/StakeMath.spec @@ -0,0 +1,95 @@ +import "./definition/DefinitionMath.spec"; +import "./definition/DefinitionEpoch.spec"; +import "./definition/DefinitionMultiplierPointsMath.spec"; +import "./math/OpenZeppelinMath.spec"; +import "./EpochMath.spec"; +import "./IStakeManager.spec"; + +rule check_stake( + uint256 _increasedAmount, + uint256 _increasedLockSeconds +) +{ + env e; + uint256 processTime = e.block.timestamp; + address addr = e.msg.sender; + uint256 globalEpoch = currentEpoch(); + uint256 globalStartTime = START_TIME(); + + requireValidSystem(processTime, globalStartTime, globalEpoch, 2); + requireValidAccount(processTime, globalStartTime, globalEpoch, addr, 2); + + address initial_rewardAddress; + uint256 initial_balance; + uint256 initial_maxMP; + uint256 initial_totalMP; + uint256 initial_lastMint; + uint256 initial_lockUntil; + uint256 initial_accountEpoch; + uint256 initial_accountStartTime; + + initial_rewardAddress, initial_balance, initial_maxMP, initial_totalMP, initial_lastMint, initial_lockUntil, initial_accountEpoch, initial_accountStartTime = accounts(addr); + + + mathint calc_balance = initial_balance + _increasedAmount; + mathint calc_lockUntil = max(initial_lockUntil, processTime) + _increasedLockSeconds; + mathint dt_lock = calc_lockUntil - processTime; + mathint calc_accountEpoch = newEpoch(e); + + require calc_balance >= A_MIN(); + require dt_lock == 0 || dt_lock >= T_MIN(); + require dt_lock <= T_MAX(); + + + + mathint delta_bonusMP_initial_balance = bonusMP(initial_balance, _increasedLockSeconds); + mathint delta_bonusMP_increasedAmount = bonusMP(_increasedAmount, dt_lock); + + mathint delta_bonusMP = delta_bonusMP_initial_balance + delta_bonusMP_increasedAmount; + mathint delta_accountEpoch = calc_accountEpoch - initial_accountEpoch; + + mathint calc_lastMint; + if(initial_lastMint == 0){ + calc_lastMint = processTime; + } else if (delta_accountEpoch == 0) { + calc_lastMint = initial_lastMint; + } else { + calc_lastMint = epochStart(calc_accountEpoch, globalStartTime); + } + + mathint delta_totalMP = initialMP(_increasedAmount) + delta_bonusMP; + mathint currentEpochAccrued = initial_accountEpoch < calc_accountEpoch ? accrueMP(initial_balance, epochStart(initial_accountEpoch+1, globalStartTime) - initial_lastMint) : 0; + mathint calc_accruedMP = initial_accountEpoch < calc_accountEpoch ? min(currentEpochAccrued + (accrueMP(initial_balance, T_RATE()) * (delta_accountEpoch-1)), initial_maxMP - initial_totalMP) : 0; + mathint calc_maxMP = initial_maxMP + delta_totalMP + accrueMP(_increasedAmount, MAX_MULTIPLIER() * YEAR()); + mathint calc_totalMP = initial_totalMP + delta_totalMP + calc_accruedMP; + + mathint calc_accountStartTime ; + if(initial_accountStartTime == 0) { + calc_accountStartTime = processTime; + } else if (_increasedAmount > 0) { + calc_accountStartTime = processTime - timeToAccrueMP(calc_balance, retrieveAccruedMP(calc_balance, calc_totalMP, calc_maxMP)); + } else { + calc_accountStartTime = initial_accountStartTime; + } + + stake(e, _increasedAmount, _increasedLockSeconds); + + address final_rewardAddress; + uint256 final_balance; + uint256 final_maxMP; + uint256 final_totalMP; + uint256 final_lastMint; + uint256 final_lockUntil; + uint256 final_accountEpoch; + uint256 final_accountStartTime; + final_rewardAddress, final_balance, final_maxMP, final_totalMP, final_lastMint, final_lockUntil, final_accountEpoch, final_accountStartTime = accounts(addr); + + //assert(final_rewardAddress == calc_rewardAddress); + assert(to_mathint(final_balance) == calc_balance); + assert(to_mathint(final_maxMP) == calc_maxMP); + assert(to_mathint(final_totalMP) == calc_totalMP); + assert(to_mathint(final_lastMint) == calc_lastMint); + assert(to_mathint(final_lockUntil) == calc_lockUntil); + assert(to_mathint(final_accountEpoch) == calc_accountEpoch); + assert(to_mathint(final_accountStartTime) == calc_accountStartTime); +} \ No newline at end of file diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec index 446b193..bacd9b7 100644 --- a/certora/specs/StakeVault.spec +++ b/certora/specs/StakeVault.spec @@ -1,5 +1,3 @@ -import "./shared.spec"; - using ERC20A as staked; using StakeManager as stakeManager; @@ -7,23 +5,22 @@ methods { function ERC20A.balanceOf(address) external returns (uint256) envfree; function ERC20A.allowance(address, address) external returns(uint256) envfree; function ERC20A.totalSupply() external returns(uint256) envfree; - function _.migrateFrom(address, bool, StakeManager.Account) external => DISPATCHER(true); - function _.increaseTotalMP(uint256) external => DISPATCHER(true); + function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree; + function _.owner() external => DISPATCHER(true); } -definition isMigrationFunction(method f) returns bool = ( - f.selector == sig:stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || - f.selector == sig:stakeManager.migrateFrom(address,bool,StakeManager.Account).selector || - f.selector == sig:stakeManager.increaseTotalMP(uint256).selector || - f.selector == sig:stakeManager.startMigration(address).selector - ); +function getAccountBalance(address _addr) returns uint256 { + uint256 balance; + _, balance, _, _, _, _, _, _ = stakeManager.accounts(_addr); + return balance; +} // check that the ERC20.balanceOf(vault) is >= to StakeManager.accounts[a].balance invariant accountBalanceVsERC20Balance() staked.balanceOf(currentContract) >= getAccountBalance(currentContract) filtered { - m -> m.selector != sig:leave().selector && !isMigrationFunction(m) + m -> m.selector != sig:leave().selector } { preserved with (env e) { // the sender can't be the vault otherwise it can transfer tokens @@ -48,9 +45,7 @@ invariant accountBalanceVsERC20Balance() } preserved stake(uint256 amount, uint256 duration) with (env e) { - require e.msg.sender != currentContract; - require staked.balanceOf(currentContract) + staked.balanceOf(e.msg.sender) + staked.balanceOf(stakeManager) <= to_mathint(staked.totalSupply()); } } @@ -62,7 +57,7 @@ function simplification() { require stakeManager.migration == 0; } -rule reachability(method f) filtered { f -> !isMigrationFunction(f) } +rule reachability(method f) { calldataarg args; env e; diff --git a/certora/specs/definition/DefinitionEpoch.spec b/certora/specs/definition/DefinitionEpoch.spec new file mode 100644 index 0000000..3d9af11 --- /dev/null +++ b/certora/specs/definition/DefinitionEpoch.spec @@ -0,0 +1,6 @@ +import "./DefinitionMultiplierPointsMath.spec"; + +definition epoch(mathint _timestamp, mathint startTime) returns mathint = (_timestamp - startTime) / T_RATE(); +definition epochStart(mathint _epochNum, mathint startTime) returns mathint = startTime + (T_RATE() * _epochNum); + + diff --git a/certora/specs/definition/DefinitionMath.spec b/certora/specs/definition/DefinitionMath.spec new file mode 100644 index 0000000..0b51a0a --- /dev/null +++ b/certora/specs/definition/DefinitionMath.spec @@ -0,0 +1,17 @@ +definition abs(mathint x) returns mathint = + x >= 0 ? x : 0 - x; + +definition min(mathint x, mathint y) returns mathint = + x > y ? y : x; + +definition max(mathint x, mathint y) returns mathint = + x > y ? x : y; + +definition average(mathint a, mathint b) returns mathint = + (a + b) / 2; + +definition mulDiv(mathint x, mathint y, mathint denominator) returns mathint = + (x * y) / denominator; + +definition ceilMulDiv(mathint x, mathint y, mathint denominator) returns mathint = + mulDiv(x, y, denominator) + ((x * y) % denominator > 0 ? 1 : 0); \ No newline at end of file diff --git a/certora/specs/definition/DefinitionMultiplierPointsMath.spec b/certora/specs/definition/DefinitionMultiplierPointsMath.spec new file mode 100644 index 0000000..2f8dc11 --- /dev/null +++ b/certora/specs/definition/DefinitionMultiplierPointsMath.spec @@ -0,0 +1,29 @@ +import "./DefinitionTime.spec"; +definition M_MAX() returns mathint = 4; +definition APY() returns mathint = 100; +definition MPY() returns mathint = M_MAX() * APY(); +definition MPY_ABS() returns mathint = 100 + (2 * (M_MAX() * APY())); +definition T_RATE() returns mathint = 1 * T_WEEK(); +definition A_MIN() returns mathint = (((T_YEAR() * 100) - 1) / (APY() * T_RATE())) + 1; +definition T_MIN() returns mathint = 90 * T_DAY(); +definition T_MAX() returns mathint = M_MAX() * T_YEAR(); + + +definition accrueMP(mathint _balance, mathint _deltaTime) returns mathint = (_balance * _deltaTime * APY()) / (T_YEAR() * 100); +definition bonusMP(mathint _balance, mathint _lockedSeconds) returns mathint = accrueMP(_balance, _lockedSeconds); +definition initialMP(mathint _balance) returns mathint = _balance; +definition reduceMP(mathint _balance, mathint _mp, mathint _reducedAmount) returns mathint = (_mp * _balance) / _reducedAmount; + +definition maxTotalMP(mathint _balance, mathint _lockTime) returns mathint = _balance + ((_balance * APY()) * ((M_MAX() * T_YEAR()) + _lockTime) / (T_YEAR() * 100)); +definition maxAccrueMP(mathint _balance) returns mathint = (_balance * MPY()) / 100; +definition maxAbsoluteMP(mathint _balance) returns mathint = (_balance * MPY_ABS()) / 100; +definition retrieveBonusMP(mathint _balance, mathint _maxMP) returns mathint = _maxMP - (_balance + maxAccrueMP(_balance)); +definition retrieveAccruedMP(mathint _balance, mathint _totalMP, mathint _maxMP) returns mathint = _totalMP - maxAccrueMP(_balance) - _maxMP; +definition timeToAccrueMP(mathint _balance, mathint _targetMP) returns mathint = (_targetMP * 100 * T_YEAR()) / (_balance * APY()); +definition estimateLockTime(mathint _balance, mathint _maxMP) returns mathint = (((_maxMP-_balance) * 100 * T_YEAR())+1) / ((_balance * APY())-1); +definition lockTimeAvailable(mathint _balance, mathint _maxMP) returns mathint = ((maxAbsoluteMP(_balance) - _maxMP) * T_YEAR()) / _balance; + + + + + diff --git a/certora/specs/definition/DefinitionTime.spec b/certora/specs/definition/DefinitionTime.spec new file mode 100644 index 0000000..e26b8b7 --- /dev/null +++ b/certora/specs/definition/DefinitionTime.spec @@ -0,0 +1,5 @@ +definition T_MINUTE() returns mathint = 60; +definition T_HOUR() returns mathint = 60 * T_MINUTE(); +definition T_DAY() returns mathint = 24 * T_HOUR(); +definition T_WEEK() returns mathint = 7 * T_DAY(); +definition T_YEAR() returns mathint = 365 * T_DAY() + 5 * T_HOUR() + 48 * T_MINUTE() + 45; \ No newline at end of file diff --git a/certora/specs/math/OpenZeppelinMath.spec b/certora/specs/math/OpenZeppelinMath.spec new file mode 100644 index 0000000..43a8c74 --- /dev/null +++ b/certora/specs/math/OpenZeppelinMath.spec @@ -0,0 +1,44 @@ +// Summary for OpenZeppelin's Math. +methods +{ + function Math.max(uint256 a, uint256 b) internal returns (uint256) => maxSummary(a, b); + function Math.min(uint256 a, uint256 b) internal returns (uint256) => minSummary(a, b); + function Math.average(uint256 a, uint256 b) internal returns (uint256) => averageSummary(a, b); + function Math.ceilDiv(uint256 a, uint256 b) internal returns (uint256) => ceilDivSummary(a, b); + function Math.mulDiv(uint256 x, uint256 y, uint256 denominator) internal returns (uint256) => mulDivSummary(x, y, denominator); + function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal returns (uint256) => mulDivSummaryRounding(x, y, denominator, rounding); +} + +function maxSummary(uint256 a, uint256 b) returns uint256 +{ + return a > b ? a : b; +} + +function minSummary(uint256 a, uint256 b) returns uint256 +{ + return a < b ? a : b; +} + +function averageSummary(uint256 a, uint256 b) returns uint256 +{ + return require_uint256((a + b) / 2); +} + +function ceilDivSummary(uint256 numerator, uint256 denominator) returns uint256 { + require denominator > 0; + return require_uint256((numerator + denominator - 1) / denominator); +} + +function mulDivSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + require denominator > 0; + return require_uint256((x * y) / denominator); +} + +function mulDivSummaryRounding(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 { + require denominator > 0; + if (rounding == Math.Rounding.Up) { + return require_uint256(((x * y) + denominator - 1) / denominator); + } else { + return require_uint256((x * y) / denominator); + } +} diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec deleted file mode 100644 index fe39382..0000000 --- a/certora/specs/shared.spec +++ /dev/null @@ -1,70 +0,0 @@ -using StakeManager as _stakeManager; - -methods { - function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree; - function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a, b, c); -} - -function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 { - require c != 0; - return require_uint256(a*b/c); -} - -definition requiresPreviousManager(method f) returns bool = ( - f.selector == sig:_stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || - f.selector == sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector || - f.selector == sig:_stakeManager.increaseTotalMP(uint256).selector - ); - -definition requiresNextManager(method f) returns bool = ( - f.selector == sig:_stakeManager.acceptUpdate().selector || - f.selector == sig:_stakeManager.leave().selector || - f.selector == sig:_stakeManager.transferNonPending().selector - ); - -function getAccountBalance(address addr) returns uint256 { - uint256 balance; - _, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr); - - return balance; -} - -function getAccountMaxMultiplierPoints(address addr) returns uint256 { - uint256 maxMP; - _, _, maxMP, _, _, _, _, _ = _stakeManager.accounts(addr); - - return maxMP; -} - -function getAccountCurrentMultiplierPoints(address addr) returns uint256 { - uint256 totalMP; - _, _, _, totalMP, _, _, _, _ = _stakeManager.accounts(addr); - - return totalMP; -} - -function getAccountLockUntil(address addr) returns uint256 { - uint256 lockUntil; - _, _, _, _, _, lockUntil, _, _ = _stakeManager.accounts(addr); - - return lockUntil; -} - -function getAccountEpoch(address addr) returns uint256 { - uint256 epoch; - _, _, _, _, _, _, epoch, _ = _stakeManager.accounts(addr); - return epoch; -} - -invariant MaxMPIsNeverSmallerThanBalance(address addr) - to_mathint(getAccountMaxMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr)) - filtered { - f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector - } - -invariant CurrentMPIsNeverSmallerThanBalance(address addr) - to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr)) - filtered { - f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector - } - diff --git a/certora/specs/token/ERC20.spec b/certora/specs/token/ERC20.spec new file mode 100644 index 0000000..e1cc52e --- /dev/null +++ b/certora/specs/token/ERC20.spec @@ -0,0 +1,12 @@ +// erc20 methods +methods { + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +} \ No newline at end of file diff --git a/docs/MathSpec.md b/docs/MathSpec.md new file mode 100644 index 0000000..784e4d8 --- /dev/null +++ b/docs/MathSpec.md @@ -0,0 +1,1095 @@ +## Table of Contents + +## Mathematical Specification of Staking Protocol + + +> [!IMPORTANT] +> All values in this document are expressed as unsigned integers. + +### Summary + +### Constants + +| Symbol | Source | Value | Unit | Description | +| --------------------------- | ----------------------------------------------------------------------- | ----------------------- | ----------------- | ----------------------------------------------------------------------------------------------------------------- | +| $SCALE_{FACTOR}$ | | $\pu{1 \times 10^{18}}$ | (1) | Scaling factor to maintain precision in calculations. | +| $M_{MAX}$ | | $\pu{4 \mathrm{(1)}}$ | (1) | Maximum multiplier of annual percentage yield. | +| $\mathtt{APY}$ | | 100 | percent | Annual percentage yield for multiplier points. | +| $\mathsf{MPY}$ | $M_{MAX} \times \mathtt{APY}$ | 400 | percent | Multiplier points accrued maximum percentage yield. | +| $\mathsf{MPY}^\mathit{abs}$ | $100 + (2 \times M_{\text{MAX}} \times \mathtt{APY})$ | 900 | percent | Multiplier points absolute maximum percentage yield. | +| $T_{RATE}$ | $ 7 \times T_{DAY} | 604800 | seconds | The accrue rate period of time over which multiplier points are calculated. | +| $T_{DAY}$ | | 86400 | seconds | One day. | +| $T_{YEAR}$ | $\lfloor365.242190 \times T_{DAY}\rfloor$ | 31556925 | seconds | One (mean) tropical year. | +| $A_{MIN}$ | $\lceil\tfrac{T_{YEAR} \times 100}{T_{RATE} \times \mathtt{APY}}\rceil$ | 2629744 | tokens per period | Minimal value to generate 1 multiplier point in the accrue rate period ($T_{RATE}$). ($A_{MIN} \propto T_{RATE}$) | +| $A_{MAX}$ | $\frac{2^{256} - 1}{\text{APY} \times T_{\text{RATE}}}$ | | tokens per period | Maximum value to not overflow unsigned integer of 256 bits. | +| $T_{MIN}$ | $90 \times T_{DAY}$ | 7776000 | seconds | Minimum lockup period, equivalent to 90 days. | +| $T_{MAX}$ | $M_{MAX} \times T_{YEAR}$ | 126227700 | seconds | Maximum of lockup period. | + +### Variables + +#### System and User Parameters + +##### $\Delta a\rightarrow$ Amount Difference + +Difference in amount, can be either reduced or increased depending on context. + +--- + +##### $\Delta t\rightarrow$ Time Difference of Last Accrual + +--- + +The time difference defined as: + +$$ +\Delta t = t_{now} - t_{last}, \quad \text{where} \Delta t > T_{RATE} +$$ + +--- + +##### $t_{lock}\rightarrow$ Time Lock Duration + +A user-defined duration for which $a_{bal}$ remains locked. + +--- + +##### $t_{now}\rightarrow$ Time Now + +The current timestamp seconds since the Unix epoch (January 1, 1970). + +--- + +##### $t_{lock, \Delta}\rightarrow$ Time Lock Remaining Duration + +Seconds $a_{bal}$ remains locked, expressed as: + +$$ +\begin{align} &t_{lock, \Delta} = max(t_{lock,end},t_{now}) - t_{now} \\ +\text{ where: }\quad & t_{lock, \Delta} = 0\text{ or }T_{MIN} \le t_{lock, \Delta} \le (M_{MAX} \times T_{YEAR})\end{align} +$$ + +--- + +#### State Related + +##### $a_{bal}\rightarrow$ Amount of Balance + +Amount of tokens in balance, where $a_{bal} \ge A_{MIN}$. + +--- + +##### $t_{lock,end}\rightarrow$ Time Lock End + +Timestamp marking the end of the lock period, its state can be defined as: + +$$ +t_{lock,end} = \max(t_{now}, t_{lock,end}) + t_{lock} +$$ + +The value of $t_{lock,end}$ can be updated only within the functions: + +- $\mathcal{f}^{stake}(\mathbb{Account}, \Delta a, \Delta t_{lock})$; +- $\mathcal{f}^{lock}(\mathbb{Account}, \Delta t_{lock})$; + +--- + +##### $t_{last}\rightarrow$ Time of Accrual + +Timestamp of the last accrued time, its state can be defined as: + +$$ +t_{last} = t_{now} +$$ + +The value of $t_{last}$ is updated by all functions that change state: + +- $f^{accrue}(\mathbb{Account}, a_{bal},\Delta t)$, +- $\mathcal{f}^{stake}(\mathbb{Account}, \Delta a, \Delta t_{lock})$; +- $\mathcal{f}^{lock}(\mathbb{Account}, \Delta t_{lock})$; +- $\mathcal{f}^{unstake}(\mathbb{Account}, \Delta a)$; + +--- + +##### $mp_\mathcal{M}\rightarrow$ Maximum Multiplier Points + +Maximum value that $mp_\Sigma$ can reach. + +Relates as $mp_\mathcal{M} \propto a_{bal} \cdot (t_{lock} + \mathsf{MPY})$. + +Altered by functions that change the account state: + +- $\mathcal{f}^{stake}(\mathbb{Account}, \Delta a, \Delta t_{lock})$; +- $\mathcal{f}^{lock}(\mathbb{Account}, \Delta t_{lock})$; +- $\mathcal{f}^{unstake}(\mathbb{Account}, \Delta a)$. + +It's state can be expressed as the following state changes: + +###### Increase in Balance and Lock + +$$ +\begin{aligned} +mp_\mathcal{M} &= mp_\mathcal{M} + mp_\mathcal{A}(\Delta a, M_{MAX} \times T_{YEAR}) \\ +&\quad + mp_\mathcal{B}(\Delta a, t_{lock,\Delta} + t_{lock}) \\ +&\quad + mp_\mathcal{B}(a_{bal}, t_{lock}) \\ +&\quad + mp_\mathcal{I}(\Delta a) +\end{aligned} +$$ + +###### Increase in Balance only + +$$ +\begin{aligned} +mp_\mathcal{M} &= mp_\mathcal{M} + mp_\mathcal{A}(\Delta a, M_{MAX} \times T_{YEAR}) \\ +&\quad + mp_\mathcal{B}(\Delta a, t_{lock,\Delta}) \\ +&\quad + mp_\mathcal{I}(\Delta a) +\end{aligned} +$$ + +###### Increase in Lock only + +$$ +mp_\mathcal{M} = mp_\mathcal{M} + mp_\mathcal{B}(a_{bal}, t_{lock}) +$$ + +###### Decrease in Balance + +$$ +mp_\mathcal{M} = mp_\mathcal{M} - mp_\mathcal{R}(mp_\mathcal{M}, a_{bal}, \Delta a) +$$ + +--- + +##### $mp_{\Sigma}\rightarrow$ Total Multiplier Points + +Altered by all functions that change state: + +- [[#$mathcal{f} {stake}( mathbb{Account}, Delta a, t_{lock}) longrightarrow$ Stake Amount With Lock]] +- [[#$ mathcal{f} {lock}( mathbb{Account}, t_{lock}) longrightarrow$ Increase Lock]]; +- [[#$ mathcal{f} {unstake}( mathbb{Account}, Delta a) longrightarrow$ Unstake Amount Unlocked]]; +- [[#$ mathcal{f} {accrue}( mathbb{Account}) longrightarrow$ Accrue Multiplier Points]]. + +The state can be expressed as the following state changes: + +###### For every $T_{RATE}$ + +$$ +mp_{\Sigma} = min(\mathcal{f}mp_\mathcal{A}(a_{bal},\Delta t) ,mp_\mathcal{M} - mp_\Sigma) +$$ + +###### Increase in Balance and Lock + +$$ +\begin{aligned} +mp_{\Sigma} &= mp_{\Sigma} + mp_\mathcal{B}(\Delta a, t_{lock, \Delta} + t_{lock}) \\ +&\quad + mp_\mathcal{B}(a_{bal}, t_{lock}) \\ +&\quad + mp_\mathcal{I}(\Delta a) +\end{aligned} +$$ + +###### Increase in Balance only + +$$ +mp_{\Sigma} = mp_{\Sigma} + mp_\mathcal{B}(\Delta a, t_{lock, \Delta}) + mp_\mathcal{I}(\Delta a) +$$ + +###### Increase in Lock only + +$$ +mp_{\Sigma} = mp_{\Sigma} + mp_\mathcal{B}(a_{bal}, t_{lock}) +$$ + +###### Decrease in Balance + +$$ +mp_{\Sigma} = mp_{\Sigma} - mp_\mathcal{R}(mp_{\Sigma}, a_{bal}, \Delta a) +$$ + +--- + + +##### $\mathbb{Epoch}\rightarrow$ Epoch Storage Schema + +Defined as following: + +$$ +\begin{gather} + \mathbb{Epoch} \\ + \overbrace{ + \begin{align} + R_{pending} & : \text{reward pending}, \\ + S_\Sigma & : \text{total supply}, \\ + mp_\mathcal{p} & : \text{potential MP} + \end{align} + } +\end{gather} +$$ + +--- + +##### $\mathbb{Account}\rightarrow$ Account Storage Schema + +Defined as following: + +$$ +\begin{gather} + \mathbb{Account} \\ + \overbrace{ + \begin{align} + a_{bal} & : \text{balance}, \\ + t_{lock,end} & : \text{lock end}, \\ + t_{last} & : \text{last accrual}, \\ + mp_\Sigma & : \text{total MPs}, \\ + mp_\mathcal{M} & : \text{maximum MPs},\\ + E_\mathcal{current} & : \text{current epoch},\\ + E_\mathcal{target} & : \text{target epoch} + \end{align} + } +\end{gather} +$$ + +--- + +##### $\mathbb{System}\rightarrow$ System Storage Schema + +Defined as following: + +$$ +\begin{gather} + \mathbb{System} \\ + \overbrace{ + \begin{align} + \mathbb{Epoch}\mathrm{[]} & : \text{epochs}, \\ + \mathbb{Account}\mathrm{[]} & : \text{accounts}, \\ + a_{bal} & : \text{total staked}, \\ + mp_\Sigma & : \text{MP supply}, \\ + mp_\mathcal{M} & : \text{MP supply max} \\ + mp_\mathcal{p} & : \text{potential MP} \\ + mp_\mathcal{rate} & : \text{total MP rate} \\ + mp_\mathcal{expired} & : \text{current expired mp} \\ + E_\mathcal{target} (E_{num} \rightarrow mp) & : \text{epochs expired MP map} + \end{align} + } +\end{gather} +$$ + + +--- + +### Pure Mathematical Functions + + +> [!NOTE] +> This function definitions represent direct mathematical input -> output methods, which don't change state. + +#### $\mathcal{f}{mp_\mathcal{I}}(\Delta a) \longrightarrow$ Initial Multiplier Points + +Calculates the initial multiplier points (**MPs**) based on the balance change $\Delta a$. The result is equal to the +amount of balance added. + +$$ +\boxed{ + \begin{equation} + \mathcal{f}{mp_\mathcal{I}}(\Delta a) = \Delta a + \end{equation} +} +$$ + +Where + +- **$\Delta a$**: Represents the change in balance. + +--- + +#### $\mathcal{f}{mp_\mathcal{A}}(a_{bal}, \Delta t) \longrightarrow$ Accrue Multiplier Points + +Calculates the accrued multiplier points (**MPs**) over a time period **$\Delta t$**, based on the account balance +**$a_{bal}$** and the annual percentage yield $\mathtt{APY}$. + +$$ +\boxed{ + \begin{equation} + \mathcal{f}mp_\mathcal{A}(a_{bal}, \Delta t) = \dfrac{a_{bal} \times \Delta t \times \mathtt{APY}}{100 \times T_{YEAR}} + \end{equation} +} +$$ + +Where + +- **$a_{bal}$**: Represents the current account balance. +- **$\Delta t$**: The time difference or the duration over which the multiplier points are accrued, expressed in the + same time units as the year (typically days or months). +- **$T_{YEAR}$**: A constant representing the duration of a full year, used to normalize the time difference + **$\Delta t$**. +- **$\mathtt{APY}$**: The Annual Percentage Yield (APY) expressed as a percentage, which determines how much the balance + grows over a year. + +--- + +#### $\mathcal{f}{mp_\mathcal{B}}(\Delta a, t_{lock}) \longrightarrow$ Bonus Multiplier Points + +Calculates the bonus multiplier points (**MPs**) earned when a balance **$\Delta a$** is locked for a specified duration + **$t_{lock}$**. It is equivalent to the [[#$ mathcal{f}{mp_ mathcal{A}}(a_{bal}, Delta t) longrightarrow$ Accrue Multiplier Points]] but specifically applied in the context of a locked balance, using [[#$ Delta t rightarrow$ Time Difference of Last Accrual|$\Delta t$]] as [[#$t_{lock} rightarrow$ Time Lock Duration|$t_{lock}$]]. + +$$ +\begin{aligned} + &\mathcal{f}mp_\mathcal{B}(\Delta a, t_{lock}) = \mathcal{f}mp_\mathcal{A}(\Delta a, t_{lock}) \\ + &\boxed{ + \begin{equation} + \mathcal{f}mp_\mathcal{B}(\Delta a, t_{lock}) = \dfrac{\Delta a \times t_{lock} \times \mathtt{APY}}{100 \times T_{YEAR}} + \end{equation} + } +\end{aligned} +$$ + +Where: + +- **$\Delta a$**: Represents the amount of the balance that is locked. +- **$t_{lock}$**: The duration for which the balance **$\Delta a$** is locked, measured in units of seconds. +- **$T_{YEAR}$**: A constant representing the length of a year, used to normalize the lock period **$t_{lock}$** as a + fraction of a full year. +- **$\mathtt{APY}$**: The Annual Percentage Yield (APY), expressed as a percentage, which indicates the yearly interest rate + applied to the locked balance. + +--- + +#### $\mathcal{f}{mp_\mathcal{R}}(mp, a_{bal}, \Delta a) \longrightarrow$ Reduce Multiplier Points + +Calculates the reduction in multiplier points (**MPs**) when a portion of the balance **$\Delta a$** is removed from the +total balance **$a_{bal}$**. The reduction is proportional to the ratio of the removed balance to the total balance, +applied to the current multiplier points **$mp$**. + +$$ +\boxed{ + \begin{equation} + \mathcal{f}{mp_\mathcal{R}}(mp, a_{bal}, \Delta a) = \dfrac{mp \times \Delta a}{ a_{bal}} + \end{equation} +} +$$ + +Where: + +- **$mp$**: Represents the current multiplier points. +- **$a_{bal}$**: The total account balance before the removal of **$\Delta a$**. +- **$\Delta a$**: The amount of balance being removed or deducted. + +--- + +### State Functions + +These function definitions represent methods that modify the state of both **$\mathbb{System}$** and +**$\mathbb{Account}$**. They perform various pure mathematical operations to implement the specified state changes, +affecting either the system as a whole and the individual account states. + +#### $\mathcal{f}^{stake}(\mathbb{Account},\Delta a, t_{lock}) \longrightarrow$ Stake Amount With Lock + +_Purpose:_ Allows a user to stake an amount $\Delta a$ with an optional lock duration $t_{lock}$. + +```mermaid +--- +title: Stake Storage Access Flowchart +--- +flowchart LR + BonusMP{{Bonus MP}} + InitialMP{{Initial MP}} + Balance + LockEnd[Lock End] + TotalMP[Total MPs] + MaxMP[Maximum MPs] + FBonusMP{Calc Bonus MP} + FMaxMP{Calc Max Accrue MP} + M_MAX([MAX MULTIPLIER]) + Balance --> InitialMP + Balance --> FMaxMP + M_MAX --> FMaxMP + InitialMP --> TotalMP + InitialMP --> MaxMP + BonusMP --> TotalMP + BonusMP --> MaxMP + FMaxMP --> MaxMP + LockEnd --> FBonusMP + Balance --> FBonusMP + FBonusMP --> BonusMP +``` + +##### Steps + +###### Accrue Existing Multiplier Points (MPs) + +Call the [[#$ mathcal{f} {accrue}( mathbb{Account}) longrightarrow$ Accrue Multiplier Points]] function to update MPs and last accrual time. + +###### Calculate the New Remaining Lock Period ($\Delta t_{lock}$) + +$$ +\Delta t_{lock} = max(\mathbb{Account} \cdot t_{lock,end}, t_{now}) + t_{lock} - t_{now} +$$ +###### Verify Constraints + +Ensure new balance ($a_{bal}$ + $\Delta a$) meets the minimum amount ($A_{MIN}$): + +$$ +\mathbb{Account} \cdot a_{bal} + \Delta a > A_{MIN} +$$ + +Ensure the New Remaining Lock Period ($\Delta t_{lock}$) is within Allowed Limits + +$$ +\Delta t_{lock} = 0 \lor T_{MIN} \le \Delta t_{lock} \le T_{MAX} +$$ + + +###### Calculate Increased Bonus MPs + +For the new amount ($\Delta a$) with the New Remaining Lock Period ($\Delta t_{lock}$): + +$$ +\Delta \hat{mp}^\mathcal{B} = \mathcal{f}mp_\mathcal{B}(\Delta a, \Delta t_{lock}) +$$ + +For extending the lock ($t_{lock}$) on the existing balance ($\mathbb{Account} \cdot a_{bal}$): + +$$ +\Delta \hat{mp}^\mathcal{B} = \Delta \hat{mp}^\mathcal{B} + \mathcal{f}mp_\mathcal{B}(\mathbb{Account} \cdot a_{bal}, t_{lock}) +$$ + +###### Calculate Increased Maximum MPs ($\Delta mp_\mathcal{M}$) + +$$ +\Delta mp_\mathcal{M} = \mathcal{f}mp_\mathcal{I}(\Delta a) + \Delta \hat{mp}^\mathcal{B} + \mathcal{f}mp_\mathcal{A}(\Delta a, M_{MAX} \times T_{YEAR}) +$$ + +###### Calculate Increased Total MPs ($\Delta mp_\Sigma$) + +$$ +\Delta mp_\Sigma = \mathcal{f}mp_\mathcal{I}(\Delta a) + \Delta \hat{mp}^\mathcal{B} +$$ + + +###### Verify Constraints + +Ensure the New Maximum MPs ($\mathbb{Account} \cdot mp_\mathcal{M} + \Delta mp_\mathcal{M}$) is within the Absolute Maximum MPs: + +$$ +\mathbb{Account} \cdot mp_\mathcal{M} + \Delta mp_\mathcal{M} \le \frac{a_{bal} \times \mathsf{MPY}^\mathit{abs}}{100} +$$ + +###### Calculate MP Rate: + +$$ +mp_{\text{rate}} = \frac{\Delta a \times T_{\text{RATE}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ + +###### Calculate Fractional + +$$ +mp_{\text{fractional}} = mp_{\text{rate}} - \frac{\Delta a \times \Delta t_{\text{epoch}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ + +###### Total MP Needed to Reach Maximum MP: + +$$ +mp_{\text{target}}(\Delta a) = \hat{\mathcal{f}}mp_\Sigma^{\text{max}}(\Delta a) + mp_{\text{fractional}} +$$ + +$$ +mp_{\text{target}} = \frac{\Delta a \times \mathsf{MPY}}{100} + mp_{\text{fractional}} +$$ + +###### Determine Full and Partial Epochs: + +$$ +\Delta E_{\text{target,1}} = \left\lfloor \frac{mp_{\text{target}}}{mp_{\text{rate}}} \right\rfloor +$$ +$$ +\Delta E_{\text{target,2}} = \frac{mp_{\text{target}}}{mp_{\text{rate}}} \mod 1 +$$ + +###### Update Target Epochs: + +$$ +E_{\text{target,1}} = E_{\text{current}} + \Delta E_{\text{target,1}} +$$ + +###### System Updates: + +$$ +\mathbb{System}.mp_{\text{rate}} = \mathbb{System}.mp_{\text{rate}} + mp_{\text{rate}} +$$ +$$ +\mathbb{System}.mp_{\text{expired}} = \mathbb{System}.mp_{\text{expired}} + mp_{\text{fractional}} +$$ + +Conditionally: + +If $E_{\text{target,2}} == 1$: +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target,1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target,1}}) + mp_{\text{remainder}} +$$ +$$ +E_{\text{target,2}} = E_{\text{target,1}} + 1 +$$ +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target,2}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target,2}}) + mp_{\text{rate}} - mp_{\text{remainder}} +$$ + +Else: + +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target,1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target,1}}) + mp_{\text{rate}} +$$ + + +###### Update account State + +Maximum MPs: + +$$ +\mathbb{Account} \cdot mp_\mathcal{M} = \mathbb{Account}\cdot mp_\mathcal{M} + \Delta mp_\mathcal{M} +$$ + +Total MPs: + +$$ +\mathbb{Account} \cdot mp_\Sigma = \mathbb{Account} \cdot mp_\Sigma + \Delta mp_\Sigma +$$ + +Balance: + +$$ +\mathbb{Account} \cdot a_{bal} = \mathbb{Account} \cdot a_{bal} + \Delta a +$$ + +Lock end time: + +$$ +\mathbb{Account} \cdot t_{lock,end} = max(\mathbb{Account} \cdot t_{lock,end}, t_{now}) + t_{lock} +$$ + +###### Update System State + +Maximum MPs: + +$$ +\mathbb{System} \cdot mp_\mathcal{M} = \mathbb{System} \cdot mp_\mathcal{M} + \Delta mp_\mathcal{M} +$$ + +Total MPs: + +$$ +\mathbb{System} \cdot mp_\Sigma = \mathbb{System} \cdot mp_\Sigma + \Delta mp_\Sigma +$$ + +Total staked amount: + +$$ +\mathbb{System} \cdot a_{bal} = \mathbb{System} \cdot a_{bal} + \Delta a +$$ + +--- + +#### $\mathcal{f}^{lock}(\mathbb{Account}, t_{lock}) \longrightarrow$ Increase Lock + + +> [!NOTE] +> Equivalent to $\mathcal{f}_{stake}(\mathbb{Account},0, t_{lock})$ + +_Purpose:_ Allows a user to lock the $\mathbb{Account} \cdot a_{bal}$ with a lock duration $t_{lock}$. + +```mermaid +--- +title: Lock Storage Access Flowchart +--- +flowchart LR + BonusMP{{Bonus MP}} + LockEnd[Lock End] + TotalMP[Total MPs] + MaxMP[Maximum MPs] + FBonusMP{Calc Bonus MP} + BonusMP --> TotalMP + BonusMP --> MaxMP + LockEnd --> FBonusMP + Balance --> FBonusMP + FBonusMP --> BonusMP +``` + +##### Steps + +###### Accrue Existing Multiplier Points (MPs) + +Call the [[#$ mathcal{f} {accrue}( mathbb{Account}) longrightarrow$ Accrue Multiplier Points]] function to update MPs and last accrual time. + +###### Calculate the New Remaining Lock Period ($\Delta t_{lock}$) + +$$ +\Delta t_{lock} = max(\mathbb{Account} \cdot t_{lock,end}, t_{now}) + t_{lock} - t_{now} +$$ + +###### Verify Constraints + +Ensure the New Remaining Lock Period ($\Delta t_{lock}$) is within allowed limits: + +$$ +\Delta t_{lock} = 0 \lor T_{MIN} \le \Delta t_{lock} \le T_{MAX} +$$ + +###### Calculate Bonus MPs for the Increased Lock Period + +$$ +\Delta \hat{mp}^\mathcal{B} = mp_\mathcal{B}(\mathbb{Account} \cdot a_{bal}, t_{lock}) +$$ + +###### Verify Constraints + +Ensure the New Maximum MPs ($\mathbb{Account} \cdot mp_\mathcal{M} + \Delta \hat{mp}^\mathcal{B}$) is within the Absolute Maximum MPs: + +$$ +\mathbb{Account} \cdot mp_\mathcal{M} + \Delta \hat{mp}^\mathcal{B} \le \frac{a_{bal} \times \mathsf{MPY}^\mathit{abs}}{100} + +$$ +###### Update account State + +Maximum MPs: + +$$ +\mathbb{Account} \cdot mp_\mathcal{M} = \mathbb{Account} \cdot mp_\mathcal{M} + \Delta \hat{mp}^\mathcal{B} +$$ + +Total MPs: + +$$ +\mathbb{Account} \cdot mp_\Sigma = \mathbb{Account} \cdot mp_\Sigma + \Delta \hat{mp}^\mathcal{B} +$$ + +Lock end time: + +$$ +\mathbb{Account} \cdot t_{lock,end} = max(\mathbb{Account} \cdot t_{lock,end}, t_{now}) + t_{lock} +$$ + +###### Update System State + +Maximum MPs: + +$$ +\mathbb{System} \cdot mp_\mathcal{M} = \mathbb{System} \cdot mp_\mathcal{M} + \Delta mp_\mathcal{B} +$$ + +Total MPs: + +$$ +\mathbb{System} \cdot mp_\Sigma = \mathbb{System} \cdot mp_\Sigma + \Delta mp_\mathcal{B} +$$ + +--- + +#### $\mathcal{f}^{unstake}(\mathbb{Account}, \Delta a) \longrightarrow$ Unstake Amount Unlocked + +Purpose: Allows a user to unstake an amount $\Delta a$. + +```mermaid +--- +title: Unstake Storage Access Flowchart +--- +flowchart LR + Balance + TotalMP[Total MPs] + MaxMP[Maximum MPs] + FReduceMP{Calc Reduced MP} + TotalMP --> FReduceMP + MaxMP --> FReduceMP + Balance --> FReduceMP + FReduceMP --> Balance + FReduceMP --> TotalMP + FReduceMP --> MaxMP +``` + +##### Steps + +###### Accrue Existing Multiplier Points (MPs) + +Call the [[#$ mathcal{f} {accrue}( mathbb{Account}) longrightarrow$ Accrue Multiplier Points]] function to update MPs and last accrual time. + +###### Verify Constraints + +Ensure the account is not locked: + +$$ +\mathbb{Account} \cdot t_{lock,end} < t_{now} +$$ + +Ensure that account have enough balance: + +$$ +\mathbb{Account} \cdot a_{bal} > \Delta a +$$ + +Ensure that new balance ($\mathbb{Account} \cdot a_{bal} - \Delta a$) will be zero or more than minimum allowed: + +$$ +\mathbb{Account} \cdot a_{bal} - \Delta a = 0 \lor \mathbb{Account} \cdot a_{bal} - \Delta a > A_{MIN} +$$ + +###### Calculate Reduced Amounts + +Maximum MPs: + +$$ +\Delta mp_\mathcal{M} =\mathcal{f}mp_\mathcal{R}(\mathbb{Account} \cdot mp_\mathcal{M}, \mathbb{Account} \cdot a_{bal}, \Delta a) +$$ + +Total MPs: + +$$ +\Delta mp_\Sigma = \mathcal{f}mp_\mathcal{R}(\mathbb{Account} \cdot mp_\Sigma, \mathbb{Account} \cdot a_{bal}, \Delta a) +$$ +##### Step 1: Retrieve and Reduce Old Target and System Values + +Using the previous balance $a_{\text{bal}}$ (before unstaking), retrieve and reduce the current values for target epochs and MPs. + +###### Recalculate Old Target Epochs and Values: + +- Calculate the old MP per epoch using the previous balance: + +$$ +mp_{\text{rate, old}} = \mathcal{f}mp_\mathcal{A}(a_{\text{bal}}, T_{\text{RATE}}) = \frac{a_{\text{bal}} \times T_{\text{RATE}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ +- Calculate the old target MP and any fractional MP: + +$$ +mp_{\text{target, old}} = \frac{a_{\text{bal}} \times \mathsf{MPY}}{100} + mp_{\text{fractional, old}} +$$ + +where: + +$$ +mp_{\text{fractional, old}} = mp_{\text{rate, old}} - \frac{a_{\text{bal}} \times \Delta t_{\text{epoch}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ + +###### Determine Old Full and Partial Target Epochs: + +- Full epochs required with the previous balance: +$$ +\Delta E_{\text{target, old, 1}} = \left\lfloor \frac{mp_{\text{target, old}}}{mp_{\text{rate, old}}} \right\rfloor +$$ + +- Fractional epoch, if applicable: +$$ +\Delta E_{\text{target, old, 2}} = \frac{mp_{\text{target, old}}}{mp_{\text{rate, old}}} \mod 1 +$$ + +###### Retrieve and Reduce System Values: + +- Using the calculated old target epochs, retrieve and decrement the corresponding entries in the system storage for `expired MP`. +- Reduce the old values: + +- If $\Delta E_{\text{target, old, 2}}$​ is non-zero: +- Reduce both epochs: +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, old, 1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, old, 1}}) - mp_{\text{remainder, old}} +$$ + +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, old, 2}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, old, 2}}) - (mp_{\text{rate, old}} - mp_{\text{remainder, old}}) +$$ + +- Otherwise: +- Reduce only for the main target epoch: +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, old, 1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, old, 1}}) - mp_{\text{rate, old}} +$$ + +###### Reduce System Totals: + +- Subtract the old maximum and total MPs: +$$ +\mathbb{System} \cdot mp_\mathcal{M} = \mathbb{System} \cdot mp_\mathcal{M} - mp_\mathcal{M, old} +$$ + +$$ +\mathbb{System} \cdot mp_\Sigma = \mathbb{System} \cdot mp_\Sigma - mp_\Sigma^{\text{old}} +$$ + +###### Reduce Account MP Totals: + +- Update the account's maximum and total MPs: +$$ +\mathbb{Account} \cdot mp_\mathcal{M} = \mathbb{Account} \cdot mp_\mathcal{M} - \Delta mp_\mathcal{M} +$$ + +$$ +\mathbb{Account} \cdot mp_\Sigma = \mathbb{Account} \cdot mp_\Sigma - \Delta mp_\Sigma +$$ + + +--- + +##### Step 2: Recalculate New Target Epochs and Add New Values + +With the reduced balance $a_{\text{bal}} - \Delta a$, recalculate the target epochs and update the system and account accordingly. + +###### Calculate New MP Per Epoch: + +$$ +mp_{\text{rate, new}} = \mathcal{f}mp_\mathcal{A}(a_{\text{bal}} - \Delta a, T_{\text{RATE}}) = \frac{(a_{\text{bal}} - \Delta a) \times T_{\text{RATE}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ + +###### Recalculate New Target MP (Including Fractional MP): + +- Calculate the target MP needed to reach maximum MPs with the new balance: +$$ +mp_{\text{target, new}} = \frac{(a_{\text{bal}} - \Delta a) \times \mathsf{MPY}}{100} + mp_{\text{fractional, new}} +$$ + +- Where: +$$ +mp_{\text{fractional, new}} = mp_{\text{rate, new}} - \frac{(a_{\text{bal}} - \Delta a) \times \Delta t_{\text{epoch}} \times \mathtt{APY}}{100 \times T_{\text{YEAR}}} +$$ + +###### Calculate New Full and Partial Target Epochs: + +- Full epochs required with the new balance: +$$ +\Delta E_{\text{target, new, 1}} = \left\lfloor \frac{mp_{\text{target, new}}}{mp_{\text{rate, new}}} \right\rfloor +$$ + +- Fractional epoch, if any: +$$ +\Delta E_{\text{target, new, 2}} = \frac{mp_{\text{target, new}}}{mp_{\text{rate, new}}} \mod 1 +$$ + +###### Update New Target Epochs in System Storage: + +- If $\Delta E_{\text{target, new, 2}}$ is non-zero: +- Update both new target epochs: +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, new, 1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, new, 1}}) + mp_{\text{remainder, new}} +$$ + +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, new, 2}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, new, 2}}) + (mp_{\text{rate, new}} - mp_{\text{remainder, new}}) +$$ + +- Otherwise: +- Update only for the primary target epoch: +$$ +\mathbb{System}.E_{\text{target}}(E_{\text{target, new, 1}}) = \mathbb{System}.E_{\text{target}}(E_{\text{target, new, 1}}) + mp_{\text{rate, new}} +$$ + + +###### Update account State + +Maximum MPs: + +$$ +\mathbb{Account} \cdot mp_\mathcal{M} = \mathbb{Account} \cdot mp_\mathcal{M} - \Delta mp_\mathcal{M} +$$ + +Total MPs: + +$$ +\mathbb{Account} \cdot mp_\Sigma = \mathbb{Account} \cdot mp_\Sigma - \Delta mp_\Sigma +$$ + +Balance: + +$$ +\mathbb{Account} \cdot a_{bal} = \mathbb{Account} \cdot a_{bal} - \Delta a +$$ + +###### Update System State + +Maximum MPs: + +$$ +\mathbb{System} \cdot mp_\mathcal{M} = \mathbb{System} \cdot mp_\mathcal{M} - \Delta mp_\mathcal{M} +$$ + +Total MPs: + +$$ +\mathbb{System} \cdot mp_\Sigma = \mathbb{System} \cdot mp_\Sigma - \Delta mp_\Sigma +$$ + +Total staked amount: + +$$ +\mathbb{System} \cdot a_{bal} = \mathbb{System} \cdot a_{bal} - \Delta a +$$ + +--- + +#### $\mathcal{f}^{accrue}(\mathbb{Account}) \longrightarrow$ Accrue Multiplier Points + +Purpose: Accrue multiplier points (MPs) for the account based on the elapsed time since the last accrual. + +```mermaid +--- +title: Accrue Storage Access Flowchart +--- +flowchart LR + AccruedMP{{Accrued MP}} + Balance + LastMint[Last Mint] + TotalMP[Total MPs] --> MAX{max} + MaxMP[Maximum MPs] --> MAX + FAccruedMP{Calc Accrued MP} + NOW((NOW)) --> FAccruedMP + FAccruedMP --> LastMint + LastMint --> FAccruedMP + Balance --> FAccruedMP + FAccruedMP --> AccruedMP + AccruedMP --> MAX + MAX --> TotalMP +``` + +##### Steps + +###### Calculate the time Period since Last Accrual + +$$ +\Delta t = t_{now} - \mathbb{Account} \cdot t_{last} +$$ + +###### Verify Constraints + +Ensure the accrual period is greater than the minimum rate period: + +$$ +\Delta t > T_{RATE} +$$ + +###### Calculate Accrued MP for the Accrual Period + +$$ +\Delta \hat{mp}^\mathcal{A} = min(\mathcal{f}mp_\mathcal{A}(\mathbb{Account} \cdot a_{bal},\Delta t) ,\mathbb{Account} \cdot mp_\mathcal{M} - \mathbb{Account} \cdot mp_\Sigma) +$$ + +###### Update account State + +Total MPs: + +$$ +\mathbb{Account} \cdot mp_\Sigma = \mathbb{Account} \cdot mp_\Sigma + \Delta \hat{mp}^\mathcal{A} +$$ + +Last accrual time: + +$$ +\mathbb{Account} \cdot t_{last} = t_{now} +$$ + +###### Update System State + +Total MPs: + +$$ +\mathbb{System} \cdot mp_\Sigma = \mathbb{System} \cdot mp_\Sigma + \Delta \hat{mp}^\mathcal{A} +$$ + +--- + +### Support Functions +#### Maximum Total Multiplier Points + +The maximum total multiplier points that can be generated for a determined amount of balance and lock duration. + +$$ +\boxed{ + \begin{equation} + \hat{\mathcal{f}}mp_{\mathcal{M}}(a_{bal}, t_{\text{lock}}) = a_{bal} + \frac{a_{bal} \times \mathtt{APY} \times \left( T_{\text{MAX}} + t_{\text{lock}} \right)}{100 \times T_{\text{YEAR}}} + \end{equation} +} +$$ + + +#### Maximum Accrued Multiplier Points + +The maximum multiplier points that can be accrued over time for a determined amount of balance. +It's [[#$ mathcal{f}{mp_ mathcal{A}}(a_{bal}, Delta t) longrightarrow$ Accrue Multiplier Points]] using [[#$ Delta t rightarrow$ Time Difference of Last Accrual|$\Delta t$]] $= M_{MAX} \times T_{YEAR}$ + +$$ +\boxed{ + \begin{equation} + \hat{\mathcal{f}}mp_{A}^{max}(a_{bal}) = \frac{a_{bal} \times \mathsf{MPY}}{100} + \end{equation} +} +$$ +#### Maximum Absolute Multiplier Points + +The absolute maximum multiplier points that some balance could have, which is the sum of the maximum lockup time bonus and the maximum accrued multiplier points. + +$$ +\boxed{ + \begin{equation} + \hat{\mathcal{f}}mp_\mathcal{M}^\mathit{abs}(a_{bal}) = \frac{a_{bal} \times \mathsf{MPY}^\mathit{abs}}{100} + \end{equation} +} +$$ + + +#### Retrieve Bonus Multiplier Points +Returns the Bonus Multiplier Points from the Maximum Multiplier Points and Balance. + +$$ +\boxed{ +\begin{equation} +\hat{\mathcal{f}}\hat{mp}^\mathcal{B}(mp_\mathcal{M}, a_{bal}) = mp_\mathcal{M} - \left(a_{\text{bal}} + \hat{\mathcal{f}}mp_{A}^{max}(a_{bal}) \right) +\end{equation} +} +$$ + + +#### Retrieve Accrued Multiplier Points +Returns the accrued multiplier points from Total Multiplier Points, Maximum Multiplier Points and Balance. + +$$ +\boxed{ +\begin{equation} +\hat{\mathcal{f}}\hat{mp}^\mathcal{A}(mp_\Sigma, mp_\mathcal{M}, a_{bal}) = mp_\Sigma + \hat{\mathcal{f}}mp_{A}^{max}(a_{bal}) - mp_\mathcal{M} +\end{equation} +} +$$ + +#### Time to Accrue Multiplier Points +Retrieves how much seconds to a certain $a_{bal}$ would reach a certain $mp$ +$$ +\boxed{ + \begin{equation} + t_{rem}(a_{bal},mp_{target}) = \frac{mp_{target} \times 100 \times T_{YEAR}}{a_{bal} \times \mathtt{APY}} + \end{equation} +} +$$ +#### Locked Time ($t_{lock}$) + + +> [!CAUTION] +> Use for reference only. If implemented with integers, for $a_{bal} < T_{YEAR}$, due precision loss, the result may be an approximation. + +Estimates the time an account set as locked time. + +$$ +\boxed{ + \begin{equation} + \hat{\mathcal{f}}\tilde{t}_{lock}(mp_{\mathcal{M}}, a_{bal}) \approx \left\lceil \frac{(mp_{\mathcal{M}} - a_{bal}) \times 100 \times T_{YEAR}}{a_{bal} \times \mathtt{APY}}\right\rceil - T_{\text{MAX}} + \end{equation} +} +$$ + +Where: +- $mp_{\mathcal{M}}$: Maximum multiplier points calculated the $a_{bal}$ +- $a_{bal}$: Account balance used to calculate the $mp_{\mathcal{M}}$ + +#### Remaining Time Lock Available to Increase + + +> [!CAUTION] +> Use for reference only. If implemented with integers, for $a_{bal} < T_{YEAR}$, due precision loss, the result may be an approximation. + +Retrieves how much time lock can be increased for an account. + +$$ +\boxed{ + \begin{equation} + t_{rem}^{lock}(a_{bal},mp_\mathcal{M}) \approx \frac{\left(\hat{\mathcal{f}}mp_\mathcal{M}^\mathit{abs}(a_{bal}) - mp_\mathcal{M}\right)\times T_{YEAR}}{a_{bal}} + \end{equation} +} +$$ diff --git a/docs/StakeManager.ipynb b/docs/StakeManager.ipynb new file mode 100644 index 0000000..119dd1c --- /dev/null +++ b/docs/StakeManager.ipynb @@ -0,0 +1,1095 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 3, + "id": "9bd22324-e97c-4d6e-aade-2cf5c6bcbfbd", + "metadata": {}, + "outputs": [], + "source": [ + "# Define time constants\n", + "T_MINUTE = var('T_MINUTE') #60\n", + "T_HOUR = var('T_HOUR') #60 * T_MINUTE\n", + "T_DAY = var('T_DAY') #24 * T_HOUR\n", + "T_WEEK = var('T_WEEK') #7 * T_DAY\n", + "T_YEAR = var('T_YEAR') #365 * T_DAY + 5 * T_HOUR + 48 * T_MINUTE + 45;\n", + "\n", + "# Define system constants\n", + "SCALE_FACTOR = 10^18\n", + "M_MAX = var('M_MAX') #4\n", + "APY = var('APY') # 100 # Annual Percentage Yield (percent)\n", + "MPY = M_MAX * APY\n", + "MPY_abs = 100 + (2 * M_MAX * APY)\n", + "T_RATE = var('T_RATE') #1 * T_WEEK # seconds\n", + "A_MIN = ceil((T_YEAR * 100) / (T_RATE * APY)) # Minimal tokens balance\n", + "A_MAX = (2^256 - 1) # Maximum token balance \n", + "T_MIN = 90 * T_DAY # Minimum lockup period in seconds\n", + "T_MAX = M_MAX * T_YEAR # Maximum lockup period in seconds\n", + "\n", + "# Define variables\n", + "mp, mp_M, mp_Sigma, mp_target, a_bal = var('mp mp_M mp_Sigma mp_target a_bal')\n", + "t_lock, t_lock_end, t_now = var('t_lock t_lock_end t_now')\n", + "Delta_t, Delta_a = var('Delta_t Delta_a')\n", + "S_start, E_num, E_current = var('S_start E_num E_current')\n", + "\n", + "\n", + "mp_Sigma_acc = min((a_bal * T_RATE * APY) / (100 * T_YEAR), mp_M - mp_Sigma)\n", + "t_lock_rem = max(t_lock_end, t_now) - t_now" + ] + }, + { + "cell_type": "markdown", + "id": "a5da982d-4680-42d4-ba2e-37c1b28ce7aa", + "metadata": {}, + "source": [ + "## Constants" + ] + }, + { + "cell_type": "markdown", + "id": "16083f31-2a05-4c7e-9c99-8ab6aa31d7eb", + "metadata": {}, + "source": [ + "$SCALE_{FACTOR} = \\pu{1 \\times 10^{18}}$" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "98b993ed-a2a8-4b2c-a783-4d2445d9d652", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{MINUTE}} = T_{\\mathit{MINUTE}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{MINUTE}} = T_{\\mathit{MINUTE}}$" + ], + "text/plain": [ + "T_{\\text{MINUTE}} = T_{\\mathit{MINUTE}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{HOUR}} = T_{\\mathit{HOUR}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{HOUR}} = T_{\\mathit{HOUR}}$" + ], + "text/plain": [ + "T_{\\text{HOUR}} = T_{\\mathit{HOUR}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{DAY}} = T_{\\mathit{DAY}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{DAY}} = T_{\\mathit{DAY}}$" + ], + "text/plain": [ + "T_{\\text{DAY}} = T_{\\mathit{DAY}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{WEEK}} = T_{\\mathit{WEEK}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{WEEK}} = T_{\\mathit{WEEK}}$" + ], + "text/plain": [ + "T_{\\text{WEEK}} = T_{\\mathit{WEEK}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{YEAR}} = T_{\\mathit{YEAR}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{YEAR}} = T_{\\mathit{YEAR}}$" + ], + "text/plain": [ + "T_{\\text{YEAR}} = T_{\\mathit{YEAR}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle SCALE_{\\text{FACTOR}} = 1000000000000000000\\)" + ], + "text/latex": [ + "$\\displaystyle SCALE_{\\text{FACTOR}} = 1000000000000000000$" + ], + "text/plain": [ + "SCALE_{\\text{FACTOR}} = 1000000000000000000" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle M_{\\text{MAX}} = M_{\\mathit{MAX}}\\)" + ], + "text/latex": [ + "$\\displaystyle M_{\\text{MAX}} = M_{\\mathit{MAX}}$" + ], + "text/plain": [ + "M_{\\text{MAX}} = M_{\\mathit{MAX}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle \\text{APY} = \\mathit{APY}\\)" + ], + "text/latex": [ + "$\\displaystyle \\text{APY} = \\mathit{APY}$" + ], + "text/plain": [ + "\\text{APY} = \\mathit{APY}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle MPY = \\mathit{APY} M_{\\mathit{MAX}}\\)" + ], + "text/latex": [ + "$\\displaystyle MPY = \\mathit{APY} M_{\\mathit{MAX}}$" + ], + "text/plain": [ + "MPY = \\mathit{APY} M_{\\mathit{MAX}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle MPY_{\\text{abs}} = 2 \\, \\mathit{APY} M_{\\mathit{MAX}} + 100\\)" + ], + "text/latex": [ + "$\\displaystyle MPY_{\\text{abs}} = 2 \\, \\mathit{APY} M_{\\mathit{MAX}} + 100$" + ], + "text/plain": [ + "MPY_{\\text{abs}} = 2 \\, \\mathit{APY} M_{\\mathit{MAX}} + 100" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{RATE}} = T_{\\mathit{RATE}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{RATE}} = T_{\\mathit{RATE}}$" + ], + "text/plain": [ + "T_{\\text{RATE}} = T_{\\mathit{RATE}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle A_{\\text{MIN}} = \\left \\lceil \\frac{100 \\, T_{\\mathit{YEAR}}}{\\mathit{APY} T_{\\mathit{RATE}}} \\right \\rceil\\)" + ], + "text/latex": [ + "$\\displaystyle A_{\\text{MIN}} = \\left \\lceil \\frac{100 \\, T_{\\mathit{YEAR}}}{\\mathit{APY} T_{\\mathit{RATE}}} \\right \\rceil$" + ], + "text/plain": [ + "A_{\\text{MIN}} = \\left \\lceil \\frac{100 \\, T_{\\mathit{YEAR}}}{\\mathit{APY} T_{\\mathit{RATE}}} \\right \\rceil" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle A_{\\text{MAX}} = 115792089237316195423570985008687907853269984665640564039457584007913129639935\\)" + ], + "text/latex": [ + "$\\displaystyle A_{\\text{MAX}} = 115792089237316195423570985008687907853269984665640564039457584007913129639935$" + ], + "text/plain": [ + "A_{\\text{MAX}} = 115792089237316195423570985008687907853269984665640564039457584007913129639935" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{MIN}} = 90 \\, T_{\\mathit{DAY}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{MIN}} = 90 \\, T_{\\mathit{DAY}}$" + ], + "text/plain": [ + "T_{\\text{MIN}} = 90 \\, T_{\\mathit{DAY}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "\\(\\displaystyle T_{\\text{MAX}} = M_{\\mathit{MAX}} T_{\\mathit{YEAR}}\\)" + ], + "text/latex": [ + "$\\displaystyle T_{\\text{MAX}} = M_{\\mathit{MAX}} T_{\\mathit{YEAR}}$" + ], + "text/plain": [ + "T_{\\text{MAX}} = M_{\\mathit{MAX}} T_{\\mathit{YEAR}}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "show(r\"T_{\\text{MINUTE}} = \" + latex(T_MINUTE))\n", + "show(r\"T_{\\text{HOUR}} = \" + latex(T_HOUR))\n", + "show(r\"T_{\\text{DAY}} = \" + latex(T_DAY))\n", + "show(r\"T_{\\text{WEEK}} = \" + latex(T_WEEK))\n", + "show(r\"T_{\\text{YEAR}} = \" + latex(T_YEAR))\n", + "\n", + "show(r\"SCALE_{\\text{FACTOR}} = \" + latex(SCALE_FACTOR))\n", + "show(r\"M_{\\text{MAX}} = \" + latex(M_MAX))\n", + "show(r\"\\text{APY} = \" + latex(APY))\n", + "show(r\"MPY = \" + latex(MPY))\n", + "show(r\"MPY_{\\text{abs}} = \" + latex(MPY_abs))\n", + "show(r\"T_{\\text{RATE}} = \" + latex(T_RATE))\n", + "show(r\"A_{\\text{MIN}} = \" + latex(A_MIN))\n", + "show(r\"A_{\\text{MAX}} = \" + latex(A_MAX))\n", + "show(r\"T_{\\text{MIN}} = \" + latex(T_MIN))\n", + "show(r\"T_{\\text{MAX}} = \" + latex(T_MAX))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "49049f8d-c722-41a1-8880-37e02e21a225", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "markdown", + "id": "f4a7d51c-0eef-46ca-b401-a4182ba5a60b", + "metadata": {}, + "source": [ + "#### Initial Multiplier Points\n", + "\\begin{equation}\n", + " \\mathcal{f}{mp_\\mathcal{I}}(\\Delta a) = \\Delta a\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "512bd9d4-8281-453d-9d3a-7508b53b8749", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle a_{\\mathit{bal}}$" + ], + "text/plain": [ + "a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_I = a_bal\n", + "show(mp_I)" + ] + }, + { + "cell_type": "markdown", + "id": "1bd1957d-a03f-4d9c-a7d5-d4d4fb07a540", + "metadata": {}, + "source": [ + "#### Accrued Multiplier Points\n", + "\\begin{equation}\n", + " \\mathcal{f}mp_\\mathcal{A}(a_{bal}, \\Delta t) = \\dfrac{a_{bal} \\times \\Delta t \\times \\mathtt{APY}}{100 \\times T_{YEAR}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "d29950db-9255-437d-9018-fe5503fb3100", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{\\mathit{APY} \\Delta_{t} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{\\mathit{APY} \\Delta_{t} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}}$" + ], + "text/plain": [ + "1/100*APY*Delta_t*a_bal/T_YEAR" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_A = (a_bal * Delta_t * APY) / (100 * T_YEAR)\n", + "show(mp_A)" + ] + }, + { + "cell_type": "markdown", + "id": "b39c11fd-6435-41c8-baa8-6d711872d292", + "metadata": {}, + "source": [ + "#### Bonus Multiplier Points\n", + "\\begin{equation}\n", + " \\mathcal{f}mp_\\mathcal{B}(\\Delta a, t_{lock}) = \\dfrac{\\Delta a \\times t_{lock} \\times \\mathtt{APY}}{100 \\times T_{YEAR}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "db6b1b41-c130-42aa-a3c2-8c089f3195ed", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{\\mathit{APY} a_{\\mathit{bal}} t_{\\mathit{lock}}}{100 \\, T_{\\mathit{YEAR}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{\\mathit{APY} a_{\\mathit{bal}} t_{\\mathit{lock}}}{100 \\, T_{\\mathit{YEAR}}}$" + ], + "text/plain": [ + "1/100*APY*a_bal*t_lock/T_YEAR" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_B = (a_bal * t_lock * APY) / (100 * T_YEAR)\n", + "show(mp_B)" + ] + }, + { + "cell_type": "markdown", + "id": "98f88584-45ca-46f4-8c61-d2eb6d661788", + "metadata": {}, + "source": [ + "#### Reduce Multiplier Points\n", + "\\begin{equation}\n", + " \\mathcal{f}{mp_\\mathcal{R}}(mp, a_{bal}, \\Delta a) = \\dfrac{mp \\times \\Delta a}{ a_{bal}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "9c88ffea-141c-4005-8f91-1b964cbd4dd8", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{\\Delta_{a} \\mathit{mp}}{a_{\\mathit{bal}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{\\Delta_{a} \\mathit{mp}}{a_{\\mathit{bal}}}$" + ], + "text/plain": [ + "Delta_a*mp/a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_R = (mp * Delta_a) / a_bal\n", + "show(mp_R)" + ] + }, + { + "cell_type": "markdown", + "id": "8d8ecaea-38a9-4f9e-834c-2bd3f207fc4c", + "metadata": {}, + "source": [ + "#### Maximum Total Multiplier Points\n", + "\\begin{equation}\n", + " \\hat{\\mathcal{f}}mp_{\\mathcal{M}}(a_{bal}, t_{\\text{lock}}) = a_{bal} + \\frac{a_{bal} \\times \\mathtt{APY} \\times \\left( M_{\\text{MAX}} \\times T_{\\text{YEAR}} + t_{\\text{lock}} \\right)}{100 \\times T_{\\text{YEAR}}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "0ded6bac-3224-46b9-8f3d-37dc5fbf1a54", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{{\\left(M_{\\mathit{MAX}} T_{\\mathit{YEAR}} + t_{\\mathit{lock}}\\right)} \\mathit{APY} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{{\\left(M_{\\mathit{MAX}} T_{\\mathit{YEAR}} + t_{\\mathit{lock}}\\right)} \\mathit{APY} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + a_{\\mathit{bal}}$" + ], + "text/plain": [ + "1/100*(M_MAX*T_YEAR + t_lock)*APY*a_bal/T_YEAR + a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "f_mp_M = a_bal + (a_bal * APY * (M_MAX * T_YEAR + t_lock)) / (100 * T_YEAR)\n", + "show(f_mp_M)" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "5b7314ac-5d26-4e02-89f7-6d212eade766", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{\\mathit{APY} \\Delta_{t} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + \\frac{\\mathit{APY} a_{\\mathit{bal}} t_{\\mathit{lock}}}{100 \\, T_{\\mathit{YEAR}}} + a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{\\mathit{APY} \\Delta_{t} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + \\frac{\\mathit{APY} a_{\\mathit{bal}} t_{\\mathit{lock}}}{100 \\, T_{\\mathit{YEAR}}} + a_{\\mathit{bal}}$" + ], + "text/plain": [ + "1/100*APY*Delta_t*a_bal/T_YEAR + 1/100*APY*a_bal*t_lock/T_YEAR + a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "f_mp_Sigma = mp_I + mp_B + mp_A\n", + "show(f_mp_Sigma)" + ] + }, + { + "cell_type": "markdown", + "id": "ccdd2472-6605-4916-a3ce-5d3266a8a99a", + "metadata": {}, + "source": [ + "#### Maximum Bonus Multiplier Points\n" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "d6e50410-76d5-43fd-91cb-e3e0efc34cbd", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}}$" + ], + "text/plain": [ + "1/100*APY*M_MAX*a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_B_max = (a_bal * T_MAX * APY) / (100 * T_YEAR)\n", + "show(mp_B_max)" + ] + }, + { + "cell_type": "markdown", + "id": "b5884f56-1f54-4948-8f3e-efab850c47a6", + "metadata": {}, + "source": [ + "#### Maximum Accrued Multiplier Points\n", + "\\begin{equation}\n", + " \\hat{\\mathcal{f}}mp_\\Sigma^{max}(a_{bal}) = \\frac{a_{bal} \\times \\mathsf{MPY}}{100}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "f49cb634-e917-481c-97fe-aec300f27142", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}}$" + ], + "text/plain": [ + "1/100*APY*M_MAX*a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_A_max = (a_bal * MPY) / 100\n", + "show(mp_A_max)" + ] + }, + { + "cell_type": "markdown", + "id": "84668702-26ae-4572-9451-b8513ff76e58", + "metadata": {}, + "source": [ + "#### Maximum Absolute Multiplier Points\n", + "\\begin{equation}\n", + " \\hat{\\mathcal{f}}mp_\\mathcal{M}^\\mathit{abs}(a_{bal}) = \\frac{a_{bal} \\times \\mathsf{MPY}^\\mathit{abs}}{100}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "a68d8911-bbb3-4719-b961-503191fc3921", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{1}{50} \\, {\\left(\\mathit{APY} M_{\\mathit{MAX}} + 50\\right)} a_{\\mathit{bal}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{1}{50} \\, {\\left(\\mathit{APY} M_{\\mathit{MAX}} + 50\\right)} a_{\\mathit{bal}}$" + ], + "text/plain": [ + "1/50*(APY*M_MAX + 50)*a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_M_abs = (a_bal * MPY_abs) / 100\n", + "show(mp_M_abs)" + ] + }, + { + "cell_type": "markdown", + "id": "896be099-b4d8-42f4-968f-fdf2a12234b7", + "metadata": {}, + "source": [ + "#### Time to Accrue Multiplier Points\n", + "\\begin{equation}\n", + " t_{rem}(a_{bal},mp) = \\frac{mp \\times 100 \\times T_{YEAR}}{a_{bal} \\times \\mathtt{APY}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "8ea19bde-0ff0-46e3-9a70-0494bc7b27f1", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} \\mathit{mp}}{\\mathit{APY} a_{\\mathit{bal}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} \\mathit{mp}}{\\mathit{APY} a_{\\mathit{bal}}}$" + ], + "text/plain": [ + "100*T_YEAR*mp/(APY*a_bal)" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "t_rem = (mp * 100 * T_YEAR) / (a_bal * APY)\n", + "show(t_rem)" + ] + }, + { + "cell_type": "markdown", + "id": "88de7fb8-d021-4bb5-bad9-1eb10e910587", + "metadata": {}, + "source": [ + "#### Time to Accrue Maximum Multiplier Points\n", + "\\begin{equation}\n", + "\tt_{rem}^{max}(a_{bal},mp_\\Sigma,mp_\\mathcal{M}) = \\frac{(mp_\\mathcal{M} - mp_\\Sigma) \\times 100 \\times T_{YEAR}}{a_{bal} \\times \\mathtt{APY}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "ca688296-ef21-4f5e-9ae9-cd44c11cb1dc", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} {\\left(\\mathit{mp}_{M} - \\mathit{mp}_{\\Sigma}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} {\\left(\\mathit{mp}_{M} - \\mathit{mp}_{\\Sigma}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}}$" + ], + "text/plain": [ + "100*T_YEAR*(mp_M - mp_Sigma)/(APY*a_bal)" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "t_rem_max = ((mp_M - mp_Sigma) * 100 * T_YEAR) / (a_bal * APY)\n", + "show(t_rem_max)" + ] + }, + { + "cell_type": "markdown", + "id": "f3c3ce0a-f0e7-4d38-8658-4c08cc933cf7", + "metadata": {}, + "source": [ + "#### Locked Time Retrival\n", + "\\begin{equation}\n", + "\t\t\\hat{\\mathcal{f}}\\tilde{t}_{lock}(mp_{\\mathcal{M}}, a_{bal}) \\approx \\left\\lceil \\frac{(mp_{\\mathcal{M}} - a_{bal}) \\times 100 \\times T_{YEAR}}{a_{bal} \\times \\mathtt{APY}}\\right\\rceil - T_{\\text{YEAR}} \\times M_{\\text{MAX}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "6308bc45-3e99-4ccc-95e7-e84a59ce0772", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle -M_{\\mathit{MAX}} T_{\\mathit{YEAR}} + \\left \\lceil -\\frac{100 \\, T_{\\mathit{YEAR}} {\\left(a_{\\mathit{bal}} - \\mathit{mp}_{M}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}} \\right \\rceil\\)" + ], + "text/latex": [ + "$\\displaystyle -M_{\\mathit{MAX}} T_{\\mathit{YEAR}} + \\left \\lceil -\\frac{100 \\, T_{\\mathit{YEAR}} {\\left(a_{\\mathit{bal}} - \\mathit{mp}_{M}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}} \\right \\rceil$" + ], + "text/plain": [ + "-M_MAX*T_YEAR + ceil(-100*T_YEAR*(a_bal - mp_M)/(APY*a_bal))" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "t_lock_est = ceil(((mp_M - a_bal) * 100 * T_YEAR) / (a_bal * APY)) - (M_MAX * T_YEAR)\n", + "show(t_lock_est)" + ] + }, + { + "cell_type": "markdown", + "id": "e49cb102-ffa9-4019-95ef-f943cece31fb", + "metadata": {}, + "source": [ + "#### Remaining Time Lock Allowed to Increase\n", + "\\begin{equation}\n", + " t_{rem}^{lock}(a_{bal},mp_\\mathcal{M}) \\approx \\frac{(\\frac{a_{bal} \\times \\mathsf{MPY}^\\mathit{abs}}{100} - mp_\\mathcal{M})\\times T_{YEAR}}{a_{bal}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "c1e3f1df-263f-46ba-a169-57fe6e8906fe", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{{\\left({\\left(\\mathit{APY} M_{\\mathit{MAX}} + 50\\right)} a_{\\mathit{bal}} - 50 \\, \\mathit{mp}_{M}\\right)} T_{\\mathit{YEAR}}}{50 \\, a_{\\mathit{bal}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{{\\left({\\left(\\mathit{APY} M_{\\mathit{MAX}} + 50\\right)} a_{\\mathit{bal}} - 50 \\, \\mathit{mp}_{M}\\right)} T_{\\mathit{YEAR}}}{50 \\, a_{\\mathit{bal}}}$" + ], + "text/plain": [ + "1/50*((APY*M_MAX + 50)*a_bal - 50*mp_M)*T_YEAR/a_bal" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "t_rem_lock = ((((a_bal * MPY_abs)/100)-mp_M) * T_YEAR) / a_bal\n", + "show(t_rem_lock)" + ] + }, + { + "cell_type": "markdown", + "id": "888ed42f-83e7-4c41-9b88-a53942274566", + "metadata": {}, + "source": [ + "#### MP per Accrual Rate\n", + "\\begin{equation}\n", + "\tmp_{\\text{rate}}(a_{bal}) = \\frac{a_{bal} \\times T_{RATE} \\times \\mathtt{APY}}{100 \\times T_{YEAR}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "id": "76ab5ca5-0ce0-4152-9147-82d0a3e6d6fb", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{\\mathit{APY} T_{\\mathit{RATE}} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{\\mathit{APY} T_{\\mathit{RATE}} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}}$" + ], + "text/plain": [ + "1/100*APY*T_RATE*a_bal/T_YEAR" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_rate = (a_bal * T_RATE * APY) / (100 * T_YEAR)\n", + "show(mp_rate)" + ] + }, + { + "cell_type": "markdown", + "id": "df4f8196-9fc3-4047-8fe2-5a9a870efa9c", + "metadata": {}, + "source": [ + "#### Epoch Start Time\n", + "\\begin{equation}\n", + "\tE_{start}(E_{num}) = S_{start} + (T_{RATE} \\times E_{num})\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "id": "da251249-9344-44b2-a99e-48c3cfe2a7f1", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle E_{\\mathit{num}} T_{\\mathit{RATE}} + S_{\\mathit{start}}\\)" + ], + "text/latex": [ + "$\\displaystyle E_{\\mathit{num}} T_{\\mathit{RATE}} + S_{\\mathit{start}}$" + ], + "text/plain": [ + "E_num*T_RATE + S_start" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "E_start = S_start + (T_RATE * E_num)\n", + "show(E_start)" + ] + }, + { + "cell_type": "markdown", + "id": "dbedfbed-9050-4265-8eda-5d40bd5de5df", + "metadata": {}, + "source": [ + "#### MP Accrued for Remaining Time in Current Epoch\n", + "\\begin{equation}\n", + " \\Delta t_{\\text{epoch}} = E_{start}(E_{current} +1) - t_{now}\n", + "\\end{equation}\n", + "\\begin{equation}\n", + "\tmp_{\\text{fractional}} = mp_{\\text{rate}} - \\frac{a_{bal} \\times \\Delta t_{\\text{epoch}} \\times \\mathtt{APY}}{100 \\times T_{YEAR}}\n", + "\\end{equation}\t" + ] + }, + { + "cell_type": "code", + "execution_count": 39, + "id": "d2db1b0d-e235-4f8e-97b2-f61856264b75", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle -\\frac{{\\left(E_{\\mathit{current}} T_{\\mathit{RATE}} + S_{\\mathit{start}} - t_{\\mathit{now}}\\right)} \\mathit{APY} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + \\mathit{mp}_{\\mathit{rate}}\\)" + ], + "text/latex": [ + "$\\displaystyle -\\frac{{\\left(E_{\\mathit{current}} T_{\\mathit{RATE}} + S_{\\mathit{start}} - t_{\\mathit{now}}\\right)} \\mathit{APY} a_{\\mathit{bal}}}{100 \\, T_{\\mathit{YEAR}}} + \\mathit{mp}_{\\mathit{rate}}$" + ], + "text/plain": [ + "-1/100*(E_current*T_RATE + S_start - t_now)*APY*a_bal/T_YEAR + mp_rate" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "Delta_t_epoch = S_start + (T_RATE * E_current) - t_now\n", + "#show(Delta_t_epoch)\n", + "\n", + "mp_epoch_remaining = ((a_bal * Delta_t_epoch * APY)/(100*T_YEAR))\n", + " #show(mp_epoch_remaining)\n", + "mp_rate = var('mp_rate')\n", + "mp_fractional = mp_rate - mp_epoch_remaining\n", + "show(mp_fractional)" + ] + }, + { + "cell_type": "markdown", + "id": "b4f247d4-a37c-43f9-b6ce-90434e2f1255", + "metadata": {}, + "source": [ + "\\begin{equation}\n", + "\tmp_{\\text{target}}(a_{bal}) = \\frac{a_{bal} \\times \\mathsf{MPY}}{100} + mp_{\\text{fractional}}\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 41, + "id": "40587d2d-c4c3-4be4-9164-70f4c6377b4b", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}} + \\mathit{mp}_{\\mathit{fractional}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{1}{100} \\, \\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}} + \\mathit{mp}_{\\mathit{fractional}}$" + ], + "text/plain": [ + "1/100*APY*M_MAX*a_bal + mp_fractional" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_fractional = var('mp_fractional')\n", + "mp_target = mp_A_max + mp_fractional\n", + "show(mp_target)" + ] + }, + { + "cell_type": "markdown", + "id": "6d1a6768-a664-4261-9ba4-51f43da71939", + "metadata": {}, + "source": [ + "\\begin{equation}\n", + "\t\\Delta E_{\\text{target,1}} = \\left\\lfloor \\frac{mp_{\\text{target}}}{mp_{\\text{rate}}} \\right\\rfloor\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 42, + "id": "5b7dabb9-63c7-4d8a-b248-db9b22169292", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle E_{\\mathit{current}} + \\left \\lfloor \\frac{\\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}} + 100 \\, \\mathit{mp}_{\\mathit{fractional}}}{100 \\, \\mathit{mp}_{\\mathit{rate}}} \\right \\rfloor\\)" + ], + "text/latex": [ + "$\\displaystyle E_{\\mathit{current}} + \\left \\lfloor \\frac{\\mathit{APY} M_{\\mathit{MAX}} a_{\\mathit{bal}} + 100 \\, \\mathit{mp}_{\\mathit{fractional}}}{100 \\, \\mathit{mp}_{\\mathit{rate}}} \\right \\rfloor$" + ], + "text/plain": [ + "E_current + floor(1/100*(APY*M_MAX*a_bal + 100*mp_fractional)/mp_rate)" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "delta_e_target=floor(mp_target / mp_rate)\n", + "#show(delta_e_target)\n", + "\n", + "epoch_target = E_current + delta_e_target\n", + "show(epoch_target)" + ] + }, + { + "cell_type": "markdown", + "id": "01b8607f-41a4-494c-a0a8-7e00eb0472b7", + "metadata": {}, + "source": [ + "\\begin{equation}\n", + "\t\\Delta t_{rem}^{mp_M} = \\frac{(mp_\\mathcal{M} - mp_\\Sigma ) \\times T_{RATE}}{\\frac{a_{bal} \\times T_{RATE} \\times \\mathtt{APY}}{100 \\times T_{YEAR}}}\\\\\n", + "\\end{equation}" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "id": "22da419c-b2bf-41ab-ac56-a00cd0a47e13", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} {\\left(\\mathit{mp}_{M} - \\mathit{mp}_{\\Sigma}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}}\\)" + ], + "text/latex": [ + "$\\displaystyle \\frac{100 \\, T_{\\mathit{YEAR}} {\\left(\\mathit{mp}_{M} - \\mathit{mp}_{\\Sigma}\\right)}}{\\mathit{APY} a_{\\mathit{bal}}}$" + ], + "text/plain": [ + "100*T_YEAR*(mp_M - mp_Sigma)/(APY*a_bal)" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "delta_t_mp_M_rem = ((mp_M - mp_Sigma) * T_RATE) / ((a_bal*T_RATE*APY)/(100*T_YEAR))\n", + "show(delta_t_mp_M_rem)" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "id": "cf65ee67-3cbf-468b-9107-cd8c2291cfe4", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\\(\\displaystyle -\\mathit{mp}_{M} + \\mathit{mp}_{\\Sigma} + \\frac{M_{\\mathit{MAX}} a_{\\mathit{bal}} + \\mathit{APY}}{\\mathit{IOO}}\\)" + ], + "text/latex": [ + "$\\displaystyle -\\mathit{mp}_{M} + \\mathit{mp}_{\\Sigma} + \\frac{M_{\\mathit{MAX}} a_{\\mathit{bal}} + \\mathit{APY}}{\\mathit{IOO}}$" + ], + "text/plain": [ + "-mp_M + mp_Sigma + (M_MAX*a_bal + APY)/IOO" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "mp_B, mp_A = var('mp_B mp_A')\n", + "IOO = var ('IOO')\n", + "mp_Sigma_derived = a_bal + mp_B + mp_A\n", + "mp_B_derived = mp_M - (a_bal + ((a_bal * M_MAX + APY)/IOO))\n", + "mp_A_derived = mp_Sigma - a_bal - (mp_M - (a_bal + ((a_bal * M_MAX + APY)/IOO)))\n", + "\n", + "show(mp_A_derived)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "a112bc63-72c1-41a0-b195-63823316a0e8", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "SageMath 10.4", + "language": "sage", + "name": "sagemath" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.11.10" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/package.json b/package.json index c14fb1f..53aed94 100644 --- a/package.json +++ b/package.json @@ -29,7 +29,7 @@ "scripts": { "clean": "rm -rf cache out", "lint": "pnpm lint:sol && pnpm prettier:check", - "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process", + "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process && pnpm verify:max_mp_rule", "lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol", "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore", "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",