From 8afa4f3ac9592315f1ef8381085982ff50dacc9a Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 11 Mar 2024 12:38:54 +0100
Subject: [PATCH] chore(StakeManager.spec): add MPCantBeGreaterThanMaxMP
 invariant

This commit introduces an invariant that ensures the generated
multiplier points can never be greater than the max boost multiplier
points.

See discussion in #80

Closes #80
---
 certora/specs/StakeManager.spec | 35 +++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 79608a9..4c6bd58 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -7,15 +7,13 @@ methods {
   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(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+  function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
 }
 
-function getAccountMultiplierPoints(address addr) returns uint256 {
-  uint256 multiplierPoints;
-  _, _, _, multiplierPoints, _, _, _ = accounts(addr);
-
-  return multiplierPoints;
+function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
+  require c != 0;
+  return require_uint256(a*b/c);
 }
 
 function getAccountBalance(address addr) returns uint256 {
@@ -25,6 +23,20 @@ function getAccountBalance(address addr) returns uint256 {
   return balance;
 }
 
+function getAccountInitialMultiplierPoints(address addr) returns uint256 {
+  uint256 initialMP;
+  _, _, initialMP, _, _, _, _ = accounts(addr);
+
+  return initialMP;
+}
+
+function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
+  uint256 currentMP;
+  _, _, _, currentMP, _, _, _ = accounts(addr);
+
+  return currentMP;
+}
+
 function isMigrationfunction(method f) returns bool {
   return
           f.selector == sig:migrateTo(bool).selector ||
@@ -101,6 +113,17 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
+invariant MPcantBeGreaterThanMaxMP(address addr)
+  to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountInitialMultiplierPoints(addr)
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+  { preserved {
+      require getAccountInitialMultiplierPoints(addr) >= getAccountBalance(addr);
+      require getAccountCurrentMultiplierPoints(addr) >= getAccountInitialMultiplierPoints(addr);
+    }
+  }
+
 rule reachability(method f)
 {
   calldataarg args;