From 2aa92c962d59050e27c6126e6de3fc7116c6ef69 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Tue, 30 Jul 2024 14:54:44 +0200
Subject: [PATCH] WIP

---
 certora/confs/StakeManager.conf               |  3 ++-
 certora/specs/StakeManager.spec               | 10 ++++----
 certora/specs/StakeManagerProcessAccount.spec | 25 +++++++++++++++++--
 3 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/certora/confs/StakeManager.conf b/certora/confs/StakeManager.conf
index 3291acf..7080431 100644
--- a/certora/confs/StakeManager.conf
+++ b/certora/confs/StakeManager.conf
@@ -1,5 +1,5 @@
 {
-  "files": 
+  "files":
     ["contracts/StakeManager.sol",
       "certora/helpers/ERC20A.sol"
     ],
@@ -12,6 +12,7 @@
   "optimistic_loop": true,
   "loop_iter": "3",
   "packages": [
+    "forge-std=lib/forge-std/src",
     "@openzeppelin=lib/openzeppelin-contracts"
   ]
 }
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 6d24226..1023adc 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -7,7 +7,7 @@ methods {
   function _.migrateFrom(address, bool, StakeManager.Account) 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 accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
   function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
 }
 
@@ -18,28 +18,28 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
 
 function getAccountBalance(address addr) returns uint256 {
   uint256 balance;
-  _, balance, _, _, _, _, _ = accounts(addr);
+  _, balance, _, _, _, _, _, _ = accounts(addr);
 
   return balance;
 }
 
 function getAccountBonusMultiplierPoints(address addr) returns uint256 {
   uint256 bonusMP;
-  _, _, bonusMP, _, _, _, _ = accounts(addr);
+  _, _, bonusMP, _, _, _, _, _ = accounts(addr);
 
   return bonusMP;
 }
 
 function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
   uint256 totalMP;
-  _, _, _, totalMP, _, _, _ = accounts(addr);
+  _, _, _, totalMP, _, _, _, _  = accounts(addr);
 
   return totalMP;
 }
 
 function getAccountLockUntil(address addr) returns uint256 {
   uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _ = accounts(addr);
+  _, _, _, _, _, lockUntil, _, _  = accounts(addr);
 
   return lockUntil;
 }
diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
index a9c7ae7..1876203 100644
--- a/certora/specs/StakeManagerProcessAccount.spec
+++ b/certora/specs/StakeManagerProcessAccount.spec
@@ -2,10 +2,11 @@ using ERC20A as staked;
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
   function totalSupplyBalance() external returns (uint256) envfree;
-  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
 
   function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch);
   function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
+  function pendingMPToBeMinted() external returns (uint256) envfree;
 }
 
 // keeps track of the last epoch an account was processed
@@ -19,7 +20,7 @@ function markAccountProccessed(address account, uint256 _limitEpoch) {
 
 function getAccountLockUntil(address addr) returns uint256 {
   uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _ = accounts(addr);
+  _, _, _, _, _, lockUntil, _, _ = accounts(addr);
 
   return lockUntil;
 }
@@ -69,6 +70,26 @@ rule checkAccountProcessedBeforeStoring(method f) filtered {
 
 }
 
+rule pendingMPToMintShouldNotBeBiggerTotalSupplyMP(method f) filtered {
+  f -> !requiresPreviousManager(f) && !requiresNextManager(f)
+} {
+
+  calldataarg args;
+  env e;
+  address account;
+  address account2;
+  mathint amount;
+
+  uint256 pendingMPBefore = currentContract.pendingMPToBeMinted();
+  currentContract.stake(e, amount, 0);
+  uint256 pendingMPAfter = currentContract.pendingMPToBeMinted();
+
+  require e.block.timestamp > currentContract.currentEpoch()
+  currentContract.executeAccount(account1)
+  assert pendingMPAfter > pendingMPBefore;
+}
+
+
 /*
 Below is a rule that finds all methods that change an account's balance.
 This is just for debugging purposes and not meant to be a production rule.