From 99c73be3c4ff85c5d75604ad1fcd45653c9a5733 Mon Sep 17 00:00:00 2001
From: Ricardo Guilherme Schmidt <3esmit@gmail.com>
Date: Fri, 15 Nov 2024 02:22:56 -0300
Subject: [PATCH] fix(certora/specs): Make rules work again

---
 certora/specs/MaxMPRule.spec                  | 31 +++++++++++++++++--
 certora/specs/StakeManager.spec               |  7 -----
 certora/specs/StakeManagerProcessAccount.spec |  1 -
 certora/specs/StakeManagerStartMigration.spec |  1 -
 certora/specs/StakeVault.spec                 |  7 -----
 certora/specs/shared.spec                     | 15 +++++++++
 6 files changed, 44 insertions(+), 18 deletions(-)

diff --git a/certora/specs/MaxMPRule.spec b/certora/specs/MaxMPRule.spec
index fb26269..6ae51f1 100644
--- a/certora/specs/MaxMPRule.spec
+++ b/certora/specs/MaxMPRule.spec
@@ -1,15 +1,42 @@
 import "./shared.spec";
 
 methods {
-  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+  function startTime() external returns (uint256) envfree;
+  function currentEpoch() external returns (uint256) envfree;
 }
 
+function simplifyEpochProcessing(env e){
+  require e.block.timestamp == _stakeManager.startTime();
+  require _stakeManager.currentEpoch() == 0;
+}
+
+/* TODO: very usage of CONSTANT with Math.mulDiv or simplify mulDiv somehow, and replace simplifyEpochProcessing with reduceEpochProcessing
+
+function reduceEpochProcessing(env e, uint256 maxEpochs) {
+  require e.block.timestamp >= _stakeManager.startTime();
+  uint256 currentEpoch = _stakeManager.currentEpoch();
+  uint256 newEpoch = _stakeManager.newEpoch(e);
+  require currentEpoch <= newEpoch;
+  require currentEpoch - newEpoch <= maxEpochs;
+}
+
+function reduceAccountProcessing(env e, address addr, uint256 maxEpochs) {
+  uint256 currentEpoch = _stakeManager.currentEpoch();
+  uint256 accountEpoch = getAccountEpoch(addr);
+  require accountEpoch <= currentEpoch;
+  require accountEpoch >= currentEpoch - maxEpochs;
+}
+*/
+
 invariant MPcantBeGreaterThanMaxMP(address addr)
   to_mathint(getAccountCurrentMultiplierPoints(addr)) <= to_mathint(getAccountMaxMultiplierPoints(addr))
   filtered {
     f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
   }
-  { preserved {
+  { preserved with (env e) {
+      simplifyEpochProcessing(e);
+      /*reduceEpochProcessing(e, 3);
+      reduceAccountProcessing(e, addr, 3);*/
       requireInvariant MaxMPIsNeverSmallerThanBalance(addr);
       requireInvariant CurrentMPIsNeverSmallerThanBalance(addr);
     }
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 960668f..e6dbfef 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -10,16 +10,9 @@ methods {
   function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
   function _.increaseTotalMP(uint256) external => NONDET;
   function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
-  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);
   function _._ external => DISPATCH [] default NONDET;
 }
 
-function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
-  require c != 0;
-  return require_uint256(a*b/c);
-}
-
 function isMigrationfunction(method f) returns bool {
   return
           f.selector == sig:acceptUpdate().selector ||
diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
index 32b3de5..30bde55 100644
--- a/certora/specs/StakeManagerProcessAccount.spec
+++ b/certora/specs/StakeManagerProcessAccount.spec
@@ -7,7 +7,6 @@ methods {
   function totalStaked() external returns (uint256) envfree;
   function totalMP() external returns (uint256) envfree;
   function totalMPRate() external returns (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,uint256,uint256,uint256) external => NONDET;
diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec
index 0ccb1b1..0a15f02 100644
--- a/certora/specs/StakeManagerStartMigration.spec
+++ b/certora/specs/StakeManagerStartMigration.spec
@@ -8,7 +8,6 @@ methods {
   function totalStaked() external returns (uint256) envfree;
   function totalMP() external returns (uint256) envfree;
   function previousManager() external returns (address) envfree;
-  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
 
   function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => DISPATCHER(true);
   function StakeManagerNew.totalStaked() external returns (uint256) envfree;
diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec
index c1c02b1..446b193 100644
--- a/certora/specs/StakeVault.spec
+++ b/certora/specs/StakeVault.spec
@@ -7,16 +7,9 @@ methods {
   function ERC20A.balanceOf(address) external returns (uint256) envfree;
   function ERC20A.allowance(address, address) external returns(uint256) envfree;
   function ERC20A.totalSupply() external returns(uint256) envfree;
-  function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
   function _.migrateFrom(address, bool, StakeManager.Account) 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);
-}
-
-function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
-  require c != 0;
-  return require_uint256(a*b/c);
 }
 
 definition isMigrationFunction(method f) returns bool = (
diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec
index 7851964..fe39382 100644
--- a/certora/specs/shared.spec
+++ b/certora/specs/shared.spec
@@ -1,5 +1,15 @@
 using StakeManager as _stakeManager;
 
+methods {
+  function StakeManager.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);
+}
+
+function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
+  require c != 0;
+  return require_uint256(a*b/c);
+}
+
 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 ||
@@ -40,6 +50,11 @@ function getAccountLockUntil(address addr) returns uint256 {
   return lockUntil;
 }
 
+function getAccountEpoch(address addr) returns uint256 {
+  uint256 epoch;
+  _, _, _, _, _, _, epoch, _ = _stakeManager.accounts(addr);
+  return epoch;
+}
 
 invariant MaxMPIsNeverSmallerThanBalance(address addr)
   to_mathint(getAccountMaxMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))