Commit Graph

121 Commits

Author SHA1 Message Date
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
Ricardo Guilherme Schmidt c356954302 fix(StakeManager): check for valid migration address 2024-02-23 10:57:17 -03:00
Ricardo Guilherme Schmidt f06168c8ce fix(StakeManager): properly init accs and checks init 2024-02-23 10:57:17 -03:00
Ricardo Guilherme Schmidt c9ed9dd833 refactor(StakeManager): refactor multiplier points logic 2024-02-23 10:57:17 -03:00
r4bbit 5c564a8050 chore(workflows): add-pr-to-project-board only trigger on `opened`
This is to avoid getting these failing CI tasks where adding a PR to the
board fails when it was already added before (happens when pushing into
an existing PR).
2024-02-22 17:17:28 -03:00
Ricardo Guilherme Schmidt 03bc6559ae fix: StakeManager migration fixes and certora rules 2024-02-20 09:08:00 +01:00
Nurit Dor 14248a285b chore: certora setup for stakemanager and vault 2024-02-20 09:04:23 +01:00
r4bbit 119b8de037 chore: add project board automations 2024-02-16 08:28:23 +01:00
r4bbit dd14d2e9fc cleanup(VaultFactoryTest): remove unused import 2024-01-23 15:11:10 +01:00
r4bbit 300a296137 test(StakeManager): honor lockup period when unstaking
This adds a test to check that the lockup period is considered when a
user tries to unstake their funds through their vault.
2024-01-22 07:34:56 +01:00
r4bbit 4e411f2b37 test(StakeManager): add test to check that inital MPs are minted
This adds a test that ensures multiplier points are minted with a 1:1
ratio to the stake token amount.

This scenario covers the case where no lock up time is set during
staking.
2024-01-19 11:44:25 +01:00