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
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.
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.
r4bbit