From 109b684a2c7ad28c719aed278a987fdce817b287 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 1 Mar 2024 10:35:19 +0100
Subject: [PATCH] fix(Certora specs): make specs compile again

There have been a bunch of breaking changes in the staking contract that
resulted in our specs not compiling.

This commit fixes this, however it does not yet ensure the prover is
satisfied.
---
 certora/specs/StakeManager.spec               | 20 +++++++++----------
 certora/specs/StakeManagerStartMigration.spec | 15 +++++++-------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index b4742b2..caf0c7e 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -1,26 +1,26 @@
 using ERC20A as staked;
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
-  function stakeSupply() external returns (uint256) envfree;
-  function multiplierSupply() external returns (uint256) envfree;
+  function totalSupplyBalance() external returns (uint256) envfree;
+  function totalSupplyMP() external returns (uint256) envfree;
   function oldManager() external returns (address) envfree;
   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;
+  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
 }
 
 function getAccountMultiplierPoints(address addr) returns uint256 {
   uint256 multiplierPoints;
-  _, _, multiplierPoints, _, _, _ = accounts(addr);
+  _, _, _, multiplierPoints, _, _, _ = accounts(addr);
 
   return multiplierPoints;
 }
 
 function getAccountBalance(address addr) returns uint256 {
   uint256 balance;
-  _, balance, _, _, _, _ = accounts(addr);
+  _, balance, _, _, _, _, _ = accounts(addr);
 
   return balance;
 }
@@ -59,17 +59,17 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
     sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 
-hook Sstore accounts[KEY address addr].multiplier uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldValue) STORAGE {
     sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
 }
 
 invariant sumOfBalancesIsStakeSupply()
-      sumOfBalances == to_mathint(stakeSupply());
+      sumOfBalances == to_mathint(totalSupplyBalance());
 
 invariant sumOfMultipliersIsMultiplierSupply()
-      sumOfMultipliers == to_mathint(multiplierSupply())
-      { preserved with (env e) {
-          simplification(e);
+      sumOfMultipliers == to_mathint(totalSupplyMP())
+      { preserved with () {
+          simplification();
         }
       }
 
diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec
index 73c0fc8..8cbfdc3 100644
--- a/certora/specs/StakeManagerStartMigration.spec
+++ b/certora/specs/StakeManagerStartMigration.spec
@@ -3,27 +3,26 @@ 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 totalSupplyBalance() external returns (uint256) envfree;
+  function totalSupplyMP() external returns (uint256) envfree;
   function oldManager() external returns (address) envfree;
-  function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
+  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
 
   function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true);
-  function StakeManagerNew.stakeSupply() external returns (uint256) envfree;
-  //function _.stakeSupply() external => DISPATCHER(true);
+  function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree;
 }
 
 
 function getAccountMultiplierPoints(address addr) returns uint256 {
   uint256 multiplierPoints;
-  _, _, multiplierPoints, _, _, _ = accounts(addr);
+  _, _, _, multiplierPoints, _, _, _ = accounts(addr);
 
   return multiplierPoints;
 }
 
 function getAccountBalance(address addr) returns uint256 {
   uint256 balance;
-  _, balance, _, _, _, _ = accounts(addr);
+  _, balance, _, _, _, _, _ = accounts(addr);
 
   return balance;
 }
@@ -101,7 +100,7 @@ rule startMigrationCorrect {
   startMigration(e, newContract);
 
   assert currentContract.migration == newContract;
-  assert newStakeManager.stakeSupply() == currentContract.stakeSupply();
+  assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
 }
 
 rule migrationLockedIn {