staking/certora/specs
r4bbit 4a04b46e14 refactor(StakeManager): initialMP -> bonusMP, currentMP -> totalMP
After discussing this offline, we've decided that the naming of these
properties was misleading. This commit performs the following changes:

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

Rationale:

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

`currentMP` was misleading in combination with `initialMP`. Really what
it reflects is the total multiplier points of an account **including**
its bonus multiplier points.
2024-06-25 13:13:02 -03:00
..
StakeManager.spec refactor(StakeManager): initialMP -> bonusMP, currentMP -> totalMP 2024-06-25 13:13:02 -03:00
StakeManagerProcessAccount.spec refactor(StakeManager): make function names more descriptive 2024-06-20 15:48:27 -03:00
StakeManagerStartMigration.spec refactor(StakeManager): make function names more descriptive 2024-06-20 15:48:27 -03:00
StakeVault.spec refactor(StakeManager): make function names more descriptive 2024-06-20 15:48:27 -03:00