Commit Graph

149 Commits

Author SHA1 Message Date
Ricardo Guilherme Schmidt 5d204fee27 refactor: remove restake ability from the same vault 2024-08-31 00:15:06 -03:00
Ricardo Guilherme Schmidt 9e1192dc00 fix: revert line_lenght to 110 2024-08-28 16:36:32 -03:00
Ricardo Guilherme Schmidt 99370f1a23 fix: ran foundryup, reverted to 120 max chars and ran forge fmt 2024-08-28 16:13:53 -03:00
Ricardo Guilherme Schmidt 5af8d35e97 fix: update foundry.toml line_lenght to 110 to fix conflict with prettier 2024-08-27 13:34:54 -03:00
Ricardo Guilherme Schmidt 12f16e300c fix: line lenght (other way) 2024-08-27 13:14:40 -03:00
Ricardo Guilherme Schmidt d2345d21c8 fix: line lenght size 2024-08-27 13:12:34 -03:00
Ricardo Guilherme Schmidt 7bf91d45b2 fix: adorno and workaroud test 2024-08-27 12:56:58 -03:00
Ricardo Guilherme Schmidt 6744ce19ec WIP: add estimatied MPs to migration system 2024-08-15 00:35:10 -03:00
Ricardo Guilherme Schmidt 522e4ae174 fix: shift mps not minted in stake epoch to final epoch of account MP generation 2024-08-09 15:57:49 -03:00
Ricardo Guilherme Schmidt e213629cc5 WIP: improve gas, fix halfway epoch stake estimation, reject too low stake amount, fix doubling totalSupply of epochs, add view to calculate MPs for externally any amount for any delta time 2024-08-07 20:09:34 -03:00
Ricardo Guilherme Schmidt 2f07513931 chore: update .gas-report 2024-08-07 13:51:45 -03:00
Ricardo Guilherme Schmidt ca0fb9a9d9 chore: remove old comments 2024-08-07 11:59:31 -03:00
Ricardo Guilherme Schmidt 99ee39d170 chore: remove console.logs and old comments 2024-08-07 11:58:23 -03:00
Ricardo Guilherme Schmidt 2453e18d69 fix: remove from estimation mps that would not be minted in currentEpoch when account starts staking in middle of epoch 2024-08-05 16:36:32 -03:00
Ricardo Guilherme Schmidt c1f283876c fix: mp estimation to exact correct values 2024-08-01 12:51:03 -03:00
r4bbit de3790e0fc
WIP 2024-07-30 14:54:44 +02:00
r4bbit 60d80bf4b2
WIP: more mp estimation debugging 2024-07-19 17:01:43 +02:00
r4bbit be137c7a9e
WIP: fixing one-off error for MP estimation 2024-07-19 14:23:22 +02:00
r4bbit ec98278081
WIP: continue implementing mp estimation 2024-07-18 14:28:59 +02:00
r4bbit 86c411a2df
WIP: make tests compile again 2024-07-17 16:20:40 +02:00
r4bbit 95f06b4d70
WIP: make code compile again 2024-07-17 16:20:02 +02:00
r4bbit 97e50b2ee1
WIP: custom revert when restaking 2024-07-17 16:19:36 +02:00
Ricardo Guilherme Schmidt 4cca1db698 WIP estimated MP 2024-07-17 09:50:13 -03:00
r4bbit 4a699ef8e6
WIP 2024-07-03 13:36:47 +02:00
Ricardo Guilherme Schmidt e6df0a6587 wip mp estimate 2024-07-02 10:18:26 -03:00
Ricardo Guilherme Schmidt 0aa19d276b WIP mp estimate 2024-07-02 09:37:38 -03: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