logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-01-09 10:22:18 +00:00
Code Issues Packages Projects Releases Wiki Activity
staking/docs/MathSpec.md

1096 lines
32 KiB
Markdown
Raw Permalink Normal View History

refactor(certora): Reorganize files, add proper descriptions, fix conf files and add summaries
2024-11-25 12:24:09 -03:00
## Table of Contents
## Mathematical Specification of Staking Protocol
<!-- prettier-ignore -->
> [!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
<!-- prettier-ignore -->
> [!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
<!-- prettier-ignore -->
> [!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}$)
<!-- prettier-ignore -->
> [!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
<!-- prettier-ignore -->
> [!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}
}
$$
Reference in New Issue Copy Permalink