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.
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`.
`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.
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.
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.
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.
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.
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.
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.
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.
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
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).
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.
Unstaking didn't actually work because it was using `transferFrom()` on the
`StakeVault` with the `from` address being the vault itself.
This would result in an approval error because the vault isn't creating
any approvals to spend its own funds.
The solution is to use `transfer` instead and ensuring the return value
is checked.
This commit introduces `MIN_LOCKUP_PERIOD` and `MAX_LOCKUP_PERIOD` and
makes use of them within `StakeManager.stake()` and
`StakeManager.lock()` accordingly.
When users deposit tokens into their vault via `stake()`, they can
provide an optional lockup time. If the value is `0` it implies users do
not want to lock their stake.
If the value is `> 0` it has to be within the range of
`MIN_LOCKUP_PERIOD` and `MAX_LOCKUP_PERIOD`.
Properly addresses #15
This commit introduces a first version of a `VaultFactory` that later
will be extended to be capable of instantiating reward vaults and
possible keep track of vault instances per owner.
As a first step, this implementation comes with a `createVault()`
function which takes care of creating vaults.
Because `VaultFactory` also knows about `StakeManager` it can derive the
manager's address and stake token from it when creating vaults, allowing
the API to be without arguments.
Partially addresses #37
Because the `stakedToken` property is `immutable`, solhint recommends to
make it in all caps. This commit changes the property to adhere to that
rule and also makes the property private.
To access the `stakedToken` there's now a `stakedToken()` function on
the contract.
This was kept around as I wasn't sure if this was still needed but now
that we've removed the legacy folder and are aiming for adding SNT as a
vendor dependency it's most likely no longer needed.
If we still need something like that, we'd implement it as foundry
script.
Ricardo Guilherme Schmidt
r4bbit
Nurit Dor