This invariant failed as the prover started making wrong assumptions
about the relationship between anyone's account's `totalMP` and its
`balance`, as well as an account's `bonusMP` and its `balance`.
This commit fixes it by adding the necessary invariants to proof the
property.
change
The rule is failing since we've removed the `lockUntil > 0` check in
`stake` and `processAccount` is no longer used in `stake()`.
The rule requires `lockUntil > 0` so it will always fail there and can't
find a non-reverting cases (which makes the rule pass).
The reason it hasn't happened before was because:
The rule required account.lockUntil > 0
Stake required lockUntil > 0 || account balance == 0
Also this commit adds an invariant:
add invariant that account balance == 0 => accountMP == 0
This invariant failed as the prover started making wrong assumptions
about the relationship between anyone's account's `totalMP` and its
`balance`, as well as an account's `bonusMP` and its `balance`.
This commit fixes it by adding the necessary invariants to proof the
property.
change
The rule is failing since we've removed the `lockUntil > 0` check in
`stake` and `processAccount` is no longer used in `stake()`.
The rule requires `lockUntil > 0` so it will always fail there and can't
find a non-reverting cases (which makes the rule pass).
The reason it hasn't happened before was because:
The rule required account.lockUntil > 0
Stake required lockUntil > 0 || account balance == 0
Also this commit adds an invariant:
add invariant that account balance == 0 => accountMP == 0
As now all epochEnd() are multiples of EPOCH_SIZE, we can drop the startTime from the struct Epoch, and avoid storing an information that can be cheaply calculated on the fly.
- Refactored the StakeManager contract to optimize the finalization of epochs and execution of accounts and epochs.
- Replaced the Epoch.startTime with a new global variable startTime to keep track of the start time of the contract.
- Modified the finalizeEpoch function to use a temporary variable for the current epoch and calculate the epoch reward only for the current epoch.
- Updated the migrationInitialize function to set the start time using the new startTime variable.
- Modified the epochEnd function to calculate the end time of the current epoch using the startTime variable.
- Modified the newEpoch function to calculate the number of the next epoch based on the startTime variable.
refactor(StakeManager): set startTime as immutable, load startTime from previousManager at constructor, verify startTime is correct on initializeMigration
This commit refactors the StakeManager contract to optimize the finalization and execution of epochs. It updates the function finalizeEpoch() to new function finalizeEpoch(uint256 _limitEpoch) that releases rewards for the current epoch and increases the epoch up to the specified limit. This allows for more efficient processing of epochs.
The changes also include updates to the executeEpoch() and executeAccount() functions to utilize the new finalizeEpoch() function. Additionally, a new function newEpoch() is introduced to calculate the last epoch that can be processed based on the current time. Now the executeAccount(account,limit) will also process epochs up to the specified limit.
Added a overload of the executeAccount to process the account up to the newEpoch()
Added a overload of the executeEpoch to allow the process of epochs up to a certain limit.
All methods now that finalizeEpoch will process the epochs up to the newEpoch().
These changes improve the overall performance, user expirience and reliability of the StakeManager contract.
chore(StakeManagerStartMigration.spec): add new function executeEpoch(uint256) to blockedWhenMigrating
fix(StakeManager.sol): Replace the check for pending migration in migrationInitialize with noPendingMigration modifier to avoid code duplication
We have a couple of helper functions redefined in multiple spec files.
This commit introduces a `shared.spec` that provides such functions.
The file is then imported in other spec files, so we can make use of the
functions there.
Closes#87
This commit introduces the internal accounting logic for accrueing
multiplier points, that will later be used to determine how many
experience points an account is eligible to.
The majority of the work here was done by @3esmit.
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.
This primarily adds a rule that ensures that, when an account's
`balance` changes, `_processAccount()` must have been called as well.
There's very few exceptions where an account's `balance` can change
without the need of `_processAccount()` but those functions have been
deliberately excluded from the rule.
Ricardo Guilherme Schmidt
r4bbit