From 33e2ff048b06e9f0a3810de001452da6349777c9 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Tue, 17 Sep 2024 13:28:57 +0200
Subject: [PATCH] refactor(certora): introduce shared.spec to reuse helper
 functions

We have a couple of helper functions redefined in multiple spec files.
This commit introduces a `shared.spec` that provides such functions.

The file is then imported in other spec files, so we can make use of the
functions there.

Closes #87
---
 certora/specs/StakeManager.spec               | 42 ++-----------------
 certora/specs/StakeManagerProcessAccount.spec | 21 ++--------
 certora/specs/StakeManagerStartMigration.spec | 17 +-------
 certora/specs/StakeVault.spec                 |  9 +---
 certora/specs/shared.spec                     | 42 +++++++++++++++++++
 5 files changed, 52 insertions(+), 79 deletions(-)
 create mode 100644 certora/specs/shared.spec

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 81cce58..8b49a56 100644
--- a/certora/specs/StakeManager.spec
+++ b/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;
diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
index c121520..e964acb 100644
--- a/certora/specs/StakeManagerProcessAccount.spec
+++ b/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.
diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec
index c469914..c1f36f9 100644
--- a/certora/specs/StakeManagerStartMigration.spec
+++ b/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 ||
diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec
index cadb9c4..c1c02b1 100644
--- a/certora/specs/StakeVault.spec
+++ b/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 ||
diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec
new file mode 100644
index 0000000..a4731e2
--- /dev/null
+++ b/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;
+}
+
+