Commit Graph

145 Commits

Author SHA1 Message Date
Ricardo Guilherme Schmidt 142137dee7 fix(StakeManager): fix finalizeEpoch to use last epoch epochEnd and add tests to catch error 2024-09-26 15:41:35 -03:00
Ricardo Guilherme Schmidt 4a545a0ed4 chore(test): fix fuzzing function to properly test whats suppoused to and make it deterministic in amount of calls 2024-09-25 12:41:23 -03:00
Ricardo Guilherme Schmidt 85b88fa757 chore: improve comments and documentation in README.md 2024-09-25 07:00:02 -03:00
Ricardo Guilherme Schmidt 097bd05665 chore: update pull request template and README.md 2024-09-25 11:29:22 +02:00
Ricardo Guilherme Schmidt 653fe5a542 chore: update project description and author information, update README.md 2024-09-25 11:29:22 +02:00
Ricardo Guilherme Schmidt 474e7cacf5 chore(foundry.toml): update fuzzing settings 2024-09-23 06:10:17 -03:00
Ricardo Guilherme Schmidt 2a90b3e6ad chore(.gas-report, .gas-snapshot): update reports 2024-09-19 17:26:17 +02:00
r4bbit 40c5be49bc refactor(certora): introduce shared.spec to reuse helper functions
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
2024-09-19 14:35:08 +02:00
Ricardo Guilherme Schmidt 3e5361f9be fix(StakeManager): change order of call of mintBonusMP to fix intended behavior. 2024-09-12 11:44:48 +02:00
Ricardo Guilherme Schmidt 0c58dfe241 test(StakeManager): add test to catch bug in minting more bonus MPs when stake with lock 2024-09-12 11:44:48 +02:00
Ricardo Guilherme Schmidt 8683376160 feat(StakeManager): optimizations on processAccount 2024-09-11 20:09:08 +02:00
Ricardo Guilherme Schmidt b19182ad20 chore(StakeManager): remove unnecessary `finalizeEpoch` modifier from `migrateTo`
Fixes #109
2024-09-11 16:43:59 +02:00
Ricardo Guilherme Schmidt 58ca65120f chore(StakeManager: remove irrelevant code from `_mintBonusMP` function
Fixes #108
2024-09-11 16:17:17 +02:00
Ricardo Guilherme Schmidt b2a0d0cf25 fix(StakeManager): use while loop instead of hacky for loop in process account
chore: lint again with foundry updated
2024-09-11 15:18:24 +02:00
Ricardo Guilherme Schmidt 3123df83d9 feat(StakeManager): add test for executing account with limit
chore: lint
2024-09-11 15:18:24 +02:00
Ricardo Guilherme Schmidt 0dd04a179e chore(package.json): fix gas-report command 2024-09-11 15:18:24 +02:00
Ricardo Guilherme Schmidt b312c59177 chore: add adorno command to package.json 2024-09-10 13:05:06 +02:00
r4bbit 5dec595a20 feat(StakeManager): implement multiplier points estimation
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.
2024-09-10 08:51:35 +02:00
r4bbit 2465618007 chore: update pnpm lock 2024-09-10 08:51:35 +02:00
r4bbit f90a3ce365 chore(StakeManager): formatting as foundry changed its mind 2024-08-27 14:46:22 +02:00
r4bbit b62ac5233e chore(CI): update certora-cli to 7.10.2
This should fix a bug in the CLI that causes CI tasks to pass even
though prover runs are emitting errors.
2024-08-27 14:46:22 +02:00
r4bbit ead8db634c chore(ci): update certora CLI in CI
This update the certora cli to the latest version 7.10.1 in CI tasks.
2024-08-05 08:35:47 +02:00
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
r4bbit d18df07b28 refactor(StakeManager): make function names more descriptive
Some of the functions on our contracts were confusing.
This commit changes them so they describe what they actually do.
2024-06-20 15:48:27 -03:00
r4bbit d9533912c2 refactor(certora): use CI matrix for verification jobs 2024-03-28 16:42:44 +01:00
r4bbit 6182d9508c chore(certora): upgrade certora-cli to 7.0.7
This upgrade certora-cli on CI to version 7.0.7 which no longer requires
the `STORAGE` keyword in storage hooks.
2024-03-20 10:59:35 +01:00
r4bbit 70b092ab00 chore(StakeManagerProcessAccount.spec): add specs for processAccount
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.
2024-03-18 11:44:51 +01:00
Ricardo Guilherme Schmidt f1548e56fa chore(StakeManager.t): tests for restake and relock
chore: lint
2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt cd3f238a08 chore(StakeManager.t): add test for unstake more than balance 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt 6c4f5d16f2 chore(StakeManager.t): move migration related tests to migration scope 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt acf5f41bc7 chore: rename DeployMigrationStakeManagerTest to MigrationStakeManagerTest 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt 53e30591f2 chore(StakeManager.t): add test for MP cap 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt 6c3fefd510 chore: add tests for restake 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt ef00a9e205 chore: add tests for migration, unstake and execute epoch 2024-03-15 13:21:59 +01:00
Ricardo Guilherme Schmidt f6a2b682c4 chore: fix warnings on BrokenERC20 mock 2024-03-15 13:21:59 +01:00
r4bbit f946e55759 chore(StakeManager.spec): add rule to ensure MP 1to1 ratio 2024-03-12 17:18:58 +01:00
r4bbit 7e2f675115 chore(StakeManager.spec): add invariant greater lock time -> more MPs 2024-03-12 17:14:30 +01:00
r4bbit f1c1de7993 chore(StakeManager.spec): add two more MP related invariants
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
2024-03-12 16:56:50 +01:00
r4bbit decd8a281d chore(StakeManager.spec): add MPCantBeGreaterThanMaxMP invariant
This commit introduces an invariant that ensures the generated
multiplier points can never be greater than the max boost multiplier
points.

See discussion in #80

Closes #80
2024-03-12 16:30:23 +01:00
Ricardo Guilherme Schmidt cbd40aef8a fix(StakeManager): lock function checks for MIN_LOCKUP_PERIOD 2024-03-12 11:41:41 -03:00
Ricardo Guilherme Schmidt 694608a629 chore(StakeManager): removed duplicate error type 2024-03-12 11:41:41 -03:00
Ricardo Guilherme Schmidt c764142909 chore(StakeManager): change revert to use custom error 2024-03-12 11:41:41 -03:00
r4bbit 4f590049d4 chore(StakeVault.spec): add rule to verify account and vault balance 2024-03-07 19:40:21 +01:00
r4bbit 544cc42f34 fix(StakeManager.spec): use filtered invariants for vacuous rules
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.
2024-03-05 10:21:26 -03:00
r4bbit da007451a4 fix(StakeManager): ensure `currentEpoch` is `0` when migrating
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`.
2024-03-05 10:21:26 -03:00
r4bbit 0708bdd846 fix(StakeManager.spec): change `simplification()` to assume no prev manager
`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.
2024-03-05 10:21:26 -03:00
r4bbit e9f0077488 fix(StakeManager.spec): ensure `revertsWhenNoMigration` passes
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.
2024-03-05 10:21:26 -03:00
r4bbit e723464245 fix(StakeManager.spec): make `epochOnlyIncreases` rule pass
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.
2024-03-05 10:21:26 -03:00
r4bbit 2343213e0d chore(StakeVault.spec): comment out purposefully failing rule
This rule is only used for debugging purposes and serves no function for
production formal verification. Hence we're commenting it out.
2024-03-05 10:21:26 -03:00
Nurit Dor e1bd0f31f8 chore: add cerora rules for `totalSupplyBalance` ghost rule 2024-03-05 10:21:26 -03:00