diff --git a/.gas-snapshot b/.gas-snapshot index f2301c5..7cabd3a 100644 --- a/.gas-snapshot +++ b/.gas-snapshot @@ -1,26 +1,32 @@ CreateVaultTest:testDeployment() (gas: 9774) -CreateVaultTest:test_createVault() (gas: 650970) -ExecuteAccountTest:testDeployment() (gas: 26421) -ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 992511) -LeaveTest:testDeployment() (gas: 26193) -LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 678007) -LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10540) -LockTest:testDeployment() (gas: 26421) -LockTest:test_RevertWhen_DecreasingLockTime() (gas: 995651) -LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 815891) +CreateVaultTest:test_createVault() (gas: 678842) +ExecuteAccountTest:testDeployment() (gas: 26378) +ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 1021726) +LeaveTest:testDeployment() (gas: 26150) +LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 711549) +LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10726) +LockTest:testDeployment() (gas: 26378) +LockTest:test_RevertWhen_DecreasingLockTime() (gas: 1025162) +LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 846956) LockTest:test_RevertWhen_SenderIsNotVault() (gas: 10652) -MigrateTest:testDeployment() (gas: 26193) -MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 677868) -MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10629) +MigrateTest:testDeployment() (gas: 26150) +MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 706961) +MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10726) SetStakeManagerTest:testDeployment() (gas: 9774) SetStakeManagerTest:test_RevertWhen_InvalidStakeManagerAddress() (gas: 20481) SetStakeManagerTest:test_SetStakeManager() (gas: 19869) -StakeManagerTest:testDeployment() (gas: 26193) -StakeTest:testDeployment() (gas: 26421) -StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 827181) -StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10672) -StakedTokenTest:testStakeToken() (gas: 7638) -UnstakeTest:testDeployment() (gas: 26376) -UnstakeTest:test_RevertWhen_FundsLocked() (gas: 991901) -UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10609) +StakeManagerTest:testDeployment() (gas: 26150) +StakeTest:testDeployment() (gas: 26378) +StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 860420) +StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10650) +StakeTest:test_RevertWhen_StakeTokenTransferFails() (gas: 175040) +StakeTest:test_StakeWithoutLockUpTimeMintsMultiplierPoints() (gas: 935199) +StakedTokenTest:testStakeToken() (gas: 7616) +UnstakeTest:testDeployment() (gas: 26400) +UnstakeTest:test_RevertWhen_FundsLocked() (gas: 1021273) +UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10631) +UnstakeTest:test_UnstakeShouldReturnFunds() (gas: 933613) +UserFlowsTest:testDeployment() (gas: 26378) +UserFlowsTest:test_StakeWithLockUpTimeLocksStake() (gas: 1001435) +UserFlowsTest:test_StakedSupplyShouldIncreaseAndDecreaseAgain() (gas: 1797181) VaultFactoryTest:testDeployment() (gas: 9774) \ No newline at end of file diff --git a/certora/confs/StakeManagerStartMigration.conf b/certora/confs/StakeManagerStartMigration.conf new file mode 100644 index 0000000..e12c8fb --- /dev/null +++ b/certora/confs/StakeManagerStartMigration.conf @@ -0,0 +1,20 @@ +{ + "files": + [ "contracts/StakeManager.sol", + "certora/harness/StakeManagerNew.sol", + "certora/helpers/ERC20A.sol" + ], + "link" : [ + "StakeManager:stakedToken=ERC20A" + ], + "msg": "Verifying StakeManager.sol", + "rule_sanity": "basic", + "verify": "StakeManager:certora/specs/StakeManagerStartMigration.spec", + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts" + ] +} + + diff --git a/certora/harness/StakeManagerNew.sol b/certora/harness/StakeManagerNew.sol new file mode 100644 index 0000000..1080a26 --- /dev/null +++ b/certora/harness/StakeManagerNew.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.19; + +import {StakeManager} from "../../contracts/StakeManager.sol"; + +contract StakeManagerNew is StakeManager { + constructor(address token, address oldManager) StakeManager(token, oldManager) {} +} diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 8502191..9b3345f 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -5,7 +5,10 @@ methods { function stakeSupply() external returns (uint256) envfree; function multiplierSupply() external returns (uint256) envfree; function oldManager() external returns (address) envfree; - function _.migrate(address, StakeManager.Account) external => NONDET; + function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET; + function _.increaseMPFromMigration(uint256) external => NONDET; + function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET; + function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree; } @@ -24,9 +27,9 @@ function getAccountBalance(address addr) returns uint256 { } function isMigrationfunction(method f) returns bool { - return f.selector == sig:leave().selector || - f.selector == sig:migrate(address,StakeManager.Account).selector || - f.selector == sig:migrate().selector; + return + f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector || + f.selector == sig:migrateTo(bool).selector; } /* assume that migration is zero, causing the verification to take into account only @@ -37,6 +40,11 @@ function simplification(env e) { require currentContract.migration == 0; } +ghost mathint sumOfEpochRewards +{ + init_state axiom sumOfEpochRewards == 0; +} + ghost mathint sumOfBalances { /* sigma account[u].balance forall u */ init_state axiom sumOfBalances == 0; } @@ -46,6 +54,10 @@ ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */ init_state axiom sumOfMultipliers == 0; } +hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE { + sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue; +} + hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE { sumOfBalances = sumOfBalances - oldValue + newValue; } @@ -64,6 +76,17 @@ invariant sumOfMultipliersIsMultiplierSupply() } } +invariant sumOfEpochRewardsIsPendingRewards() + sumOfEpochRewards == to_mathint(currentContract.pendingReward) + { preserved { + requireInvariant highEpochsAreNull(currentContract.currentEpoch); + } +} + +invariant highEpochsAreNull(uint256 epochNumber) + epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0; + + rule reachability(method f) { calldataarg args; @@ -138,3 +161,36 @@ rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked } f(e,args); assert before == staked.balanceOf(user); } + +rule epochOnlyIncreases { + method f; + env e; + calldataarg args; + + uint256 epochBefore = currentContract.currentEpoch; + + f(e, args); + + assert currentContract.currentEpoch >= epochBefore; +} + + +//TODO codehash / isVault +/* +ghost mapping(address => bytes32) codehash; + +hook EXTCODEHASH(address a) bytes32 hash { + require hash == codehash[a]; +} + +rule checksCodeHash(method f) filtered { + f -> requiresVault(f) +} { + env e; + + bool isWhitelisted = isVault(codehash[e.msg.sender]); + f(e); + + assert isWhitelisted; +} +*/ diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec new file mode 100644 index 0000000..73c0fc8 --- /dev/null +++ b/certora/specs/StakeManagerStartMigration.spec @@ -0,0 +1,130 @@ +using ERC20A as staked; +using StakeManagerNew as newStakeManager; + +methods { + function staked.balanceOf(address) external returns (uint256) envfree; + function stakeSupply() external returns (uint256) envfree; + function multiplierSupply() external returns (uint256) envfree; + function oldManager() external returns (address) envfree; + function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree; + + function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true); + function StakeManagerNew.stakeSupply() external returns (uint256) envfree; + //function _.stakeSupply() external => DISPATCHER(true); +} + + +function getAccountMultiplierPoints(address addr) returns uint256 { + uint256 multiplierPoints; + _, _, multiplierPoints, _, _, _ = accounts(addr); + + return multiplierPoints; +} + +function getAccountBalance(address addr) returns uint256 { + uint256 balance; + _, balance, _, _, _, _ = accounts(addr); + + return balance; +} + +definition blockedWhenMigrating(method f) returns bool = ( + f.selector == sig:stake(uint256, uint256).selector || + f.selector == sig:unstake(uint256).selector || + f.selector == sig:lock(uint256).selector || + f.selector == sig:executeEpoch().selector || + f.selector == sig:startMigration(address).selector + ); + +definition blockedWhenNotMigrating(method f) returns bool = ( + f.selector == sig:migrateTo(bool).selector || + f.selector == sig:transferNonPending().selector + ); + +rule rejectWhenMigrating(method f) filtered { + f -> blockedWhenMigrating(f) +} { + calldataarg args; + env e; + + require currentContract.migration != 0; + + f@withrevert(e, args); + + assert lastReverted; +} + +rule allowWhenMigrating(method f) filtered { + f -> !blockedWhenMigrating(f) +} { + calldataarg args; + env e; + + require currentContract.migration != 0; + + f@withrevert(e, args); + + satisfy !lastReverted; +} + + +rule rejectWhenNotMigrating(method f) filtered { + f -> blockedWhenNotMigrating(f) +} { + calldataarg args; + env e; + + require currentContract.migration == 0; + + f@withrevert(e, args); + + assert lastReverted; +} + +rule allowWhenNotMigrating(method f) filtered { + f -> !blockedWhenNotMigrating(f) +} { + calldataarg args; + env e; + + require currentContract.migration == 0; + + f@withrevert(e, args); + + satisfy !lastReverted; +} + +rule startMigrationCorrect { + env e; + address newContract = newStakeManager; + + startMigration(e, newContract); + + assert currentContract.migration == newContract; + assert newStakeManager.stakeSupply() == currentContract.stakeSupply(); +} + +rule migrationLockedIn { + method f; + env e; + calldataarg args; + + require currentContract.migration != 0; + + f(e, args); + + assert currentContract.migration != 0; +} + +rule epochStaysSameOnMigration { + method f; + env e; + calldataarg args; + + uint256 epochBefore = currentContract.currentEpoch; + require currentContract.migration != 0; + + f(e, args); + + assert currentContract.currentEpoch == epochBefore; +} diff --git a/contracts/StakeManager.sol b/contracts/StakeManager.sol index 96533e9..fcb3bd5 100644 --- a/contracts/StakeManager.sol +++ b/contracts/StakeManager.sol @@ -57,6 +57,27 @@ contract StakeManager is Ownable { _; } + modifier noMigration() { + if (address(migration) != address(0)) { + revert StakeManager__PendingMigration(); + } + _; + } + + modifier onlyMigration() { + if (address(migration) == address(0)) { + revert StakeManager__NoPendingMigration(); + } + _; + } + + modifier onlyOldManager() { + if (msg.sender != address(oldManager)) { + revert StakeManager__SenderIsNotPreviousStakeManager(); + } + _; + } + constructor(address _stakedToken, address _oldManager) { epochs[0].startTime = block.timestamp; oldManager = StakeManager(_oldManager); @@ -70,7 +91,7 @@ contract StakeManager is Ownable { * * @dev Reverts when `_time` is not in range of [MIN_LOCKUP_PERIOD, MAX_LOCKUP_PERIOD] */ - function stake(uint256 _amount, uint256 _time) external onlyVault { + function stake(uint256 _amount, uint256 _time) external onlyVault noMigration { if (_time > 0 && (_time < MIN_LOCKUP_PERIOD || _time > MAX_LOCKUP_PERIOD)) { revert StakeManager__InvalidLockupPeriod(); } @@ -86,7 +107,7 @@ contract StakeManager is Ownable { * Decreases balance of msg.sender; * @param _amount Amount of balance to be decreased */ - function unstake(uint256 _amount) external onlyVault { + function unstake(uint256 _amount) external onlyVault noMigration { Account storage account = accounts[msg.sender]; if (account.lockUntil > block.timestamp) { revert StakeManager__FundsLocked(); @@ -106,7 +127,7 @@ contract StakeManager is Ownable { * @dev Reverts when `_time` is bigger than `MAX_LOCKUP_PERIOD` * @dev Reverts when `_time + block.timestamp` is smaller than current lock time. */ - function lock(uint256 _time) external onlyVault { + function lock(uint256 _time) external onlyVault noMigration { if (_time > MAX_LOCKUP_PERIOD) { revert StakeManager__InvalidLockupPeriod(); } @@ -118,23 +139,10 @@ contract StakeManager is Ownable { mintIntialMultiplier(account, _time, account.balance, 0); } - /** - * @notice leave without processing account - */ - function leave() external onlyVault { - if (address(migration) == address(0)) { - revert StakeManager__NoPendingMigration(); - } - Account memory account = accounts[msg.sender]; - delete accounts[msg.sender]; - multiplierSupply -= account.multiplier; - stakeSupply -= account.balance; - } - /** * @notice Release rewards for current epoch and increase epoch. */ - function executeEpoch() external { + function executeEpoch() external noMigration { processEpoch(); } @@ -154,21 +162,59 @@ contract StakeManager is Ownable { function setVault(bytes32 _codehash) external onlyOwner { isVault[_codehash] = true; } + /** - * @notice Migrate account to new manager. + * @notice starts migration to new StakeManager + * @param _migration new StakeManager */ + function startMigration(StakeManager _migration) external onlyOwner noMigration { + processEpoch(); + migration = _migration; + stakedToken.transfer(address(migration), epochReward()); + migration.migrationInitialize(currentEpoch, multiplierSupply, stakeSupply, epochs[currentEpoch].startTime); + } - function migrate() external onlyVault returns (StakeManager newManager) { - if (address(migration) == address(0)) { - revert StakeManager__NoPendingMigration(); - } - Account storage account = accounts[msg.sender]; - stakedToken.approve(address(migration), account.balance); - migration.migrate(msg.sender, account); + /** + * @dev Callable automatically from old StakeManager.startMigration(address) + * @notice Initilizes migration process + * @param _currentEpoch epoch of old manager + * @param _multiplierSupply MP supply on old manager + * @param _stakeSupply stake supply on old manager + * @param _epochStartTime epoch start time of old manager + */ + function migrationInitialize( + uint256 _currentEpoch, + uint256 _multiplierSupply, + uint256 _stakeSupply, + uint256 _epochStartTime + ) + external + onlyOldManager + { + currentEpoch = _currentEpoch; + multiplierSupply = _multiplierSupply; + stakeSupply = _stakeSupply; + epochs[currentEpoch].startTime = _epochStartTime; + } - multiplierSupply -= accounts[msg.sender].multiplier; - delete accounts[msg.sender]; + /** + * @notice Transfer current epoch funds for migrated manager + */ + function transferNonPending() external onlyMigration { + stakedToken.transfer(address(migration), epochReward()); + } + /** + * @notice Migrate account to new manager. + * @param _acceptMigration true if wants to migrate, false if wants to leave + */ + function migrateTo(bool _acceptMigration) external onlyVault onlyMigration returns (StakeManager newManager) { + processAccount(accounts[msg.sender], currentEpoch); + Account memory account = accounts[msg.sender]; + multiplierSupply -= account.multiplier; + stakeSupply -= account.balance; + delete accounts[msg.sender]; + migration.migrateFrom(msg.sender, _acceptMigration, account); return migration; } @@ -177,13 +223,24 @@ contract StakeManager is Ownable { * @notice Migrate account from old manager * @param _vault Account address * @param _account Account data + * @param _acceptMigration If account should be stored or its MP/balance supply reduced */ - function migrate(address _vault, Account memory _account) external { - if (msg.sender != address(oldManager)) { - revert StakeManager__SenderIsNotPreviousStakeManager(); + function migrateFrom(address _vault, bool _acceptMigration, Account memory _account) external onlyOldManager { + if (_acceptMigration) { + accounts[_vault] = _account; + } else { + multiplierSupply -= _account.multiplier; + stakeSupply -= _account.balance; } - stakedToken.transferFrom(address(oldManager), address(this), _account.balance); - accounts[_vault] = _account; + } + /** + * @dev Only callable from old manager. + * @notice Increase total MP from old manager + * @param _increasedMP amount MP increased on account after migration initialized + */ + + function increaseMPFromMigration(uint256 _increasedMP) external onlyOldManager { + multiplierSupply += _increasedMP; } function calcMaxMultiplierIncrease( @@ -207,7 +264,7 @@ contract StakeManager is Ownable { } function processEpoch() private { - if (block.timestamp >= epochEnd()) { + if (block.timestamp >= epochEnd() && address(migration) == address(0)) { //finalize current epoch epochs[currentEpoch].epochReward = epochReward(); epochs[currentEpoch].totalSupply = totalSupply(); @@ -220,38 +277,43 @@ contract StakeManager is Ownable { function processAccount(Account storage account, uint256 _limitEpoch) private { processEpoch(); - if (address(migration) != address(0)) { - revert StakeManager__PendingMigration(); - } if (_limitEpoch > currentEpoch) { revert StakeManager__InvalidLimitEpoch(); } uint256 userReward; uint256 userEpoch = account.epoch; - for (Epoch memory iEpoch = epochs[userEpoch]; userEpoch < _limitEpoch; userEpoch++) { + for (Epoch storage iEpoch = epochs[userEpoch]; userEpoch < _limitEpoch; userEpoch++) { //mint multipliers to that epoch - mintMultiplier(account, iEpoch.startTime + EPOCH_SIZE); + mintMultiplier(account, iEpoch.startTime + EPOCH_SIZE, iEpoch); uint256 userSupply = account.balance + account.multiplier; - uint256 userShare = userSupply / iEpoch.totalSupply; //TODO: might lose precision, multiply by 100 and - // divide back later? - userReward += userShare * iEpoch.epochReward; + uint256 userShare = (userSupply / iEpoch.totalSupply) * 100; + uint256 userEpochReward = (userShare * iEpoch.epochReward) / 100; + userReward += userEpochReward; + iEpoch.epochReward -= userEpochReward; + iEpoch.totalSupply -= userSupply; } account.epoch = userEpoch; if (userReward > 0) { pendingReward -= userReward; stakedToken.transfer(account.rewardAddress, userReward); } - mintMultiplier(account, block.timestamp); + if (userEpoch == currentEpoch && address(migration) == address(0)) { + mintMultiplier(account, block.timestamp, epochs[currentEpoch]); + } } - function mintMultiplier(Account storage account, uint256 processTime) private { + function mintMultiplier(Account storage account, uint256 processTime, Epoch storage epoch) private { uint256 deltaTime = processTime - account.lastMint; account.lastMint = processTime; uint256 increasedMultiplier = calcMaxMultiplierIncrease( - account.balance * (MP_APY / YEAR * deltaTime), account.multiplier, account.lockUntil, account.balance + account.balance * ((MP_APY / YEAR) * deltaTime), account.multiplier, account.lockUntil, account.balance ); account.multiplier += increasedMultiplier; multiplierSupply += increasedMultiplier; + epoch.totalSupply += increasedMultiplier; + if (address(migration) != address(0)) { + migration.increaseMPFromMigration(increasedMultiplier); + } } function mintIntialMultiplier( diff --git a/contracts/StakeVault.sol b/contracts/StakeVault.sol index 63c0b0b..8588d9e 100644 --- a/contracts/StakeVault.sol +++ b/contracts/StakeVault.sol @@ -53,15 +53,15 @@ contract StakeVault is Ownable { } function leave() external onlyOwner { - stakeManager.leave(); + stakeManager.migrateTo(false); STAKED_TOKEN.transferFrom(address(this), msg.sender, STAKED_TOKEN.balanceOf(address(this))); } /** * @notice Opt-in migration to a new StakeManager contract. */ - function updateManager() external onlyOwner { - StakeManager migrated = stakeManager.migrate(); + function acceptMigration() external onlyOwner { + StakeManager migrated = stakeManager.migrateTo(true); if (address(migrated) == address(0)) revert StakeVault__MigrationNotAvailable(); stakeManager = migrated; } diff --git a/test/StakeManager.t.sol b/test/StakeManager.t.sol index d42858f..c9abc7d 100644 --- a/test/StakeManager.t.sol +++ b/test/StakeManager.t.sol @@ -194,13 +194,16 @@ contract LeaveTest is StakeManagerTest { function test_RevertWhen_SenderIsNotVault() public { vm.expectRevert(StakeManager.StakeManager__SenderIsNotVault.selector); - stakeManager.leave(); + stakeManager.migrateTo(false); } function test_RevertWhen_NoPendingMigration() public { StakeVault userVault = _createTestVault(testUser); vm.prank(testUser); vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector); + userVault.acceptMigration(); + vm.prank(testUser); + vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector); userVault.leave(); } } @@ -212,14 +215,14 @@ contract MigrateTest is StakeManagerTest { function test_RevertWhen_SenderIsNotVault() public { vm.expectRevert(StakeManager.StakeManager__SenderIsNotVault.selector); - stakeManager.migrate(); + stakeManager.migrateTo(true); } function test_RevertWhen_NoPendingMigration() public { StakeVault userVault = _createTestVault(testUser); vm.prank(testUser); vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector); - userVault.updateManager(); + userVault.acceptMigration(); } }