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.
This adds two more invariants about multiplier points:
1. Initial multiplier points can never be less than an account's balance
2. Current multiplier points can never be less than initial MP
This commit introduces an invariant that ensures the generated
multiplier points can never be greater than the max boost multiplier
points.
See discussion in #80Closes#80
This refactors the spec to no longer rely on the `simplification()`
but instead filter out the vacuous rules from the get go.
Using the `simplification()` previously was needed so that the prover
will ignore cases that revert by design. This made some invariants
vacuous.
Having vacuous rules or invariants is still considered a failure, so to
make get prover happy, we're using filtered invariants instead which
renders the `simplification` obsolete.
A previous manager can only migrate once, because the migration address
is locked in. A **new** manager is always aware of its previous manager.
This means, when a migration happens and is initialized, we know for
sure it's always the first time this is happening.
We probably don't want a migration to take place if the new manager has
already processed epochs, so we're adding a check that its
`currentEpoch` must be `0`.
This also ensures one of its invariants isn't violated:
`epochsOnlyIncrease` and `highEpochsAreNull`.
`simplification()` is used to have some rules make certain assumptions
so that they can pass. We need an additional simplification, stating
that `oldManager == address(0)`.
This means `oldManager` isn't set, meaning no `migrationInitialize()`
and similar functions have a non-reverting path.
The were changes in the contracts that caused this rule to fail.
Namely `migrateTo` shouldn't be reverting so this as been removed from
the rule and `transferNonPending` has been added as it was missing.
This was failing due to `migrationInitialize()` allowing for resetting
or decreasing a `StakeManager`s `currentEpoch`.
In practice, however, this is not possible because a new manager can
only be called from an old manager and the old manager can only migrate
once. So if `migrationInitialize()` is called from an old manager, we
can safely assume it's the first time this is called, meaning the new
manager's `currentEpoch` must be `0` at this point in time.
This is actually a bug that the certora prover found.
The rule `epochStaysSameOnMigration` failed because a previous
`StakeManager` could call `migrationInitialize` and change
`currentEpoch` on a next `StakeManager`, even though the next `StakeManager`
might be in migration itself (which means the `currentEpoch` is now
allowed to change).
This commit fixes this by ensure `migrationInitialize()` will revert if
the `StakeManager` already has a `migration` on going.
Since we're implementing rules for `StakeManager` migrations, we need
multiple instances inside the certora specs.
This results in the prover trying to run rules on the other
`StakeManager` instance as well, which isn't always desired,
as it causes some rules to fail, even though they'd pass if they'd be
executed only on the `currentContract`.
This commit makes the filter condition for relevant rules stronger, such
that the prover will not run them on the `newStakeManager` contract
instance.
We've introduced a rule that finds counter examples for all functions
that changes balances. This rule will always fail by definition, so
we're commenting it out to get CI green again.
There have been a bunch of breaking changes in the staking contract that
resulted in our specs not compiling.
This commit fixes this, however it does not yet ensure the prover is
satisfied.
Ricardo Guilherme Schmidt
r4bbit
Nurit Dor