Commit Graph

131 Commits

Author SHA1 Message Date
Ricardo Guilherme Schmidt fcb620743b refactor(StakeManager): Remove debug code and optimize epoch finalization
This is a work in progress. This commit will be split in many other PRs to address each one of the changes.

Remove debug code and optimize the epoch finalization process in the StakeManager contract. The debug code related to the `nextEpoch` variable has been removed. The `finalizeEpoch` modifier has been optimized to process epochs more efficiently . The `executeEpoch` function has been updated to execute epochs up to a specified limit. The `_processAccount` function has been modified to use a `while` loop instead of a `for` loop to fix a problem with the code.
2024-09-11 06:35:33 -03:00
Ricardo Guilherme Schmidt d3b4e95ab3 DEBUG WIP: possible bug in solidity 2024-09-11 04:44:05 -03: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
r4bbit 5cdd54a884 fix(StakeManager): don't allow migration initialization while migrating
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.
2024-03-05 10:21:26 -03:00
r4bbit 8d09f0b2dc fix(Certora specs): ensure prover runs rules on `currentContract`
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.
2024-03-05 10:21:26 -03:00
r4bbit 1c52edbbd9 chore(Certora specs): comment out purposefully failing rule
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.
2024-03-05 10:21:26 -03:00
r4bbit d7ab130d30 fix(Certora specs): make specs compile 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.
2024-03-01 15:31:14 -03:00
r4bbit d733cc3fd3 chore: update certora-cli in ci 2024-03-01 15:31:14 -03:00
r4bbit a76603e408 chore: add release command
This adds the `pnpm release` command to cut releases and generate
changelogs automatically from commit histories.

It also sets the `package.json` version to `0.1.0` as we haven't
actually put out a `1.0.0` release yet.
2024-02-29 15:36:04 +01:00
r4bbit d397466f75 feat(script): add deployment script for new `StakeManager`s
This is needed to deploy individual new `StakeManager` instances in
both, production environment and testing.

The script can be used as follows:

Within tests, to get a new `StakeManager` instance that has a reference
to an older `StakeManager` instance, run:

```solidity
function setUp() public virtual override {
    super.setUp();
    DeployMigrationStakeManager deployment = new DeployMigrationStakeManager(address(stakeManager), stakeToken);
    newStakeManager = deployment.run();
}
```

Where `address(stakeManager)` is the address of the current
`StakeManager` and `stakeToken` is the address of the stake token.

To deploy a new instance from the CLI using `forge`, one can make use of
the `PREV_STAKE_MANAGER` and `STAKE_TOKEN_ADDRESS` environment variables
like this:

```sh
$ PREV_STAKE_MANAGER=0x123 STAKE_TOKEN_ADDRES=0x456 forge script script/DeployMigrationStakeManager.s.sol
```

The script will revert when `STAKE_TOKEN_ADDRESS` is `address(0)`.

Closes #71
2024-02-29 11:19:18 -03:00
Ricardo Guilherme Schmidt 6c358dab9e fix(StakeManager): use OpenZeppelin Math to avoid precision loss in int divisions 2024-02-26 10:07:54 -03:00
Ricardo Guilherme Schmidt 47d7555c27 chore(StakeManager): add test for process account and unstake 2024-02-26 10:07:54 -03:00
Ricardo Guilherme Schmidt 92ff9bff21 refactor(StakeManager): account initialize in currentEpoch 2024-02-26 10:07:54 -03:00
Ricardo Guilherme Schmidt 6082399e83 chore: add gas-report for all contracts 2024-02-26 10:07:54 -03:00
Ricardo Guilherme Schmidt 17f859577a refactor(StakeManager): change MIN_LOCKUP_PERIOD to 2 weeks 2024-02-23 11:56:03 -03:00
Ricardo Guilherme Schmidt 294c691d1a chore(StakeManager): mark TODOs on division precision loss 2024-02-23 10:57:17 -03:00
Ricardo Guilherme Schmidt 2a762d6a41 fix(StakeManager): use a correct MP formula 2024-02-23 10:57:17 -03:00