fix: StakeManager migration fixes and certora rules

.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)

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"
+  ]
+}
+
+

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) {}
+}

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;
+}
+*/

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;
+}