refactor(certora): introduce shared.spec to reuse helper functions

certora/specs/StakeManager.spec

@@ -1,4 +1,7 @@
+import "./shared.spec";
+
 using ERC20A as staked;
+
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
   function totalSupplyBalance() external returns (uint256) envfree;
@@ -17,34 +20,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
   return require_uint256(a*b/c);
 }
 
-function getAccountBalance(address addr) returns uint256 {
-  uint256 balance;
-  _, balance, _, _, _, _, _, _ = accounts(addr);
-
-  return balance;
-}
-
-function getAccountBonusMultiplierPoints(address addr) returns uint256 {
-  uint256 bonusMP;
-  _, _, bonusMP, _, _, _, _, _ = accounts(addr);
-
-  return bonusMP;
-}
-
-function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
-  uint256 totalMP;
-  _, _, _, totalMP, _, _, _, _  = accounts(addr);
-
-  return totalMP;
-}
-
-function getAccountLockUntil(address addr) returns uint256 {
-  uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _, _  = accounts(addr);
-
-  return lockUntil;
-}
-
 function isMigrationfunction(method f) returns bool {
   return
           f.selector == sig:migrateTo(bool).selector ||
@@ -59,17 +34,6 @@ function simplification(env e) {
   require e.msg.sender != 0;
 }
 
-definition requiresPreviousManager(method f) returns bool = (
-  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
-  f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
-  f.selector == sig:increaseTotalMP(uint256).selector
-  );
-
-definition requiresNextManager(method f) returns bool = (
-  f.selector == sig:migrateTo(bool).selector ||
-  f.selector == sig:transferNonPending().selector
-  );
-
 ghost mathint sumOfEpochRewards
 {
   init_state axiom sumOfEpochRewards == 0;

certora/specs/StakeManagerProcessAccount.spec

@@ -1,4 +1,7 @@
+import "./shared.spec";
+
 using ERC20A as staked;
+
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
   function totalSupplyBalance() external returns (uint256) envfree;
@@ -20,28 +23,10 @@ function markAccountProccessed(address account, uint256 _limitEpoch) {
     accountProcessed[account] = to_mathint(_limitEpoch);
 }
 
-function getAccountLockUntil(address addr) returns uint256 {
-  uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _, _ = accounts(addr);
-
-  return lockUntil;
-}
-
 hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) {
     balanceChangedInEpoch[addr] = accountProcessed[addr];
 }
 
-definition requiresPreviousManager(method f) returns bool = (
-  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
-  f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
-  f.selector == sig:increaseTotalMP(uint256).selector
-  );
-
-definition requiresNextManager(method f) returns bool = (
-  f.selector == sig:migrateTo(bool).selector ||
-  f.selector == sig:transferNonPending().selector
-  );
-
 /*
   If a balance of an account has changed, the account should have been processed up to the `currentEpoch`.
   This is filtering out most of migration related functions, as those will be vacuous.

certora/specs/StakeManagerStartMigration.spec

@@ -1,3 +1,5 @@
+import "./shared.spec";
+
 using ERC20A as staked;
 using StakeManagerNew as newStakeManager;
 
@@ -12,21 +14,6 @@ methods {
   function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree;
 }
 
-
-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 ||

certora/specs/StakeVault.spec

@@ -1,3 +1,5 @@
+import "./shared.spec";
+
 using ERC20A as staked;
 using StakeManager as stakeManager;
 
@@ -17,13 +19,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
   return require_uint256(a*b/c);
 }
 
-function getAccountBalance(address addr) returns uint256 {
-  uint256 balance;
-  _, balance, _, _, _, _, _, _ = stakeManager.accounts(addr);
-
-  return balance;
-}
-
 definition isMigrationFunction(method f) returns bool = (
   f.selector == sig:stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:stakeManager.migrateFrom(address,bool,StakeManager.Account).selector ||

certora/specs/shared.spec

@@ -0,0 +1,42 @@
+using StakeManager as _stakeManager;
+
+definition requiresPreviousManager(method f) returns bool = (
+  f.selector == sig:_stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
+  f.selector == sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector ||
+  f.selector == sig:_stakeManager.increaseTotalMP(uint256).selector
+  );
+
+definition requiresNextManager(method f) returns bool = (
+  f.selector == sig:_stakeManager.migrateTo(bool).selector ||
+  f.selector == sig:_stakeManager.transferNonPending().selector
+  );
+
+function getAccountBalance(address addr) returns uint256 {
+  uint256 balance;
+  _, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr);
+
+  return balance;
+}
+
+function getAccountBonusMultiplierPoints(address addr) returns uint256 {
+  uint256 bonusMP;
+  _, _, bonusMP, _, _, _, _, _ = _stakeManager.accounts(addr);
+
+  return bonusMP;
+}
+
+function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
+  uint256 totalMP;
+  _, _, _, totalMP, _, _, _, _  = _stakeManager.accounts(addr);
+
+  return totalMP;
+}
+
+function getAccountLockUntil(address addr) returns uint256 {
+  uint256 lockUntil;
+  _, _, _, _, _, lockUntil, _, _  = _stakeManager.accounts(addr);
+
+  return lockUntil;
+}
+
+