refactor(StakeManager): make function names more descriptive

Some of the functions on our contracts were confusing. This commit changes them so they describe what they actually do.
logos-co · Jun 19, 2024 · 3c4c463 · 3c4c463
1 parent d953391
commit 3c4c463
Show file tree

Hide file tree

Showing 6 changed files with 86 additions and 87 deletions.
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
@@ -3,9 +3,9 @@ methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
   function totalSupplyBalance() external returns (uint256) envfree;
   function totalSupplyMP() external returns (uint256) envfree;
-  function oldManager() external returns (address) envfree;
+  function previousManager() external returns (address) envfree;
   function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
-  function _.increaseMPFromMigration(uint256) external => NONDET;
+  function _.increaseTotalMP(uint256) external => NONDET;
   function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
   function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
   function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
@@ -54,14 +54,14 @@ function isMigrationfunction(method f) returns bool {
  cases where it is zero. specifically no externall call to the migration contract */
 function simplification(env e) {
   require currentContract.migration == 0;
-  require currentContract.oldManager() == 0;
+  require currentContract.previousManager() == 0;
   require e.msg.sender != 0;
 }
 
 definition requiresPreviousManager(method f) returns bool = (
   f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
-  f.selector == sig:increaseMPFromMigration(uint256).selector
+  f.selector == sig:increaseTotalMP(uint256).selector
   );
 
 definition requiresNextManager(method f) returns bool = (

diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
@@ -31,7 +31,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
 definition requiresPreviousManager(method f) returns bool = (
   f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
-  f.selector == sig:increaseMPFromMigration(uint256).selector
+  f.selector == sig:increaseTotalMP(uint256).selector
   );
 
 definition requiresNextManager(method f) returns bool = (

diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec
@@ -5,7 +5,7 @@ methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
   function totalSupplyBalance() external returns (uint256) envfree;
   function totalSupplyMP() external returns (uint256) envfree;
-  function oldManager() external returns (address) envfree;
+  function previousManager() external returns (address) envfree;
   function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
 
   function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true);

diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec
@@ -7,7 +7,7 @@ methods {
   function ERC20A.totalSupply() external returns(uint256) envfree;
   function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
   function _.migrateFrom(address, bool, StakeManager.Account) external => DISPATCHER(true);
-  function _.increaseMPFromMigration(uint256) external => DISPATCHER(true);
+  function _.increaseTotalMP(uint256) external => DISPATCHER(true);
   function _.owner() external => DISPATCHER(true);
   function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
 }
@@ -27,7 +27,7 @@ function getAccountBalance(address addr) returns uint256 {
 definition isMigrationFunction(method f) returns bool = (
   f.selector == sig:stakeManager.migrationInitialize(uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:stakeManager.migrateFrom(address,bool,StakeManager.Account).selector ||
-  f.selector == sig:stakeManager.increaseMPFromMigration(uint256).selector ||
+  f.selector == sig:stakeManager.increaseTotalMP(uint256).selector ||
   f.selector == sig:stakeManager.startMigration(address).selector
   );