From 7581c2a079561820608711abc4609469bbda7794 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Tue, 8 Oct 2024 10:19:43 +0200
Subject: [PATCH] refactor(certora): move rule about MP not greater than max MP
 into own spec

This is necessary because we need to run this rule on a custom config to
avoid timeouts.
---
 .github/workflows/ci.yml        |  1 +
 certora/confs/MaxMPRule.conf    | 33 +++++++++++++++++++++++++++++++++
 certora/specs/MaxMPRule.spec    | 17 +++++++++++++++++
 certora/specs/StakeManager.spec | 19 ++++---------------
 certora/specs/shared.spec       | 11 +++++++++++
 package.json                    |  1 +
 6 files changed, 67 insertions(+), 15 deletions(-)
 create mode 100644 certora/confs/MaxMPRule.conf
 create mode 100644 certora/specs/MaxMPRule.spec

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7481794..d874ba2 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -173,3 +173,4 @@ jobs:
           - verify:stake_manager
           - verify:stake_manager_process
           - verify:stake_manager_start_migration
+          - verify:max_mp_rule
diff --git a/certora/confs/MaxMPRule.conf b/certora/confs/MaxMPRule.conf
new file mode 100644
index 0000000..22470c3
--- /dev/null
+++ b/certora/confs/MaxMPRule.conf
@@ -0,0 +1,33 @@
+{
+	"files": [
+		"contracts/StakeManager.sol",
+    "certora/helpers/ExpiredStakeStorageA.sol",
+		"certora/helpers/ERC20A.sol"
+	],
+	"global_timeout": "7200",
+	"link": [
+		"StakeManager:stakedToken=ERC20A",
+    "StakeManager:expiredStakeStorage=ExpiredStakeStorageA",
+	],
+	"loop_iter": "3",
+	"msg": "Z3 random seeds",
+	"optimistic_loop": true,
+	"packages": [
+		"forge-std=lib/forge-std/src",
+		"@openzeppelin=lib/openzeppelin-contracts"
+	],
+	"process": "emv",
+	"prover_args": [
+		" -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+	],
+	"prover_version": "master",
+	"rule": [
+		"MPcantBeGreaterThanMaxMP"
+	],
+  "rule_sanity": "none",
+	"smt_timeout": "7200",
+  "server": "staging",
+	"verify": "StakeManager:certora/specs/MaxMPRule.spec"
+}
+
+
diff --git a/certora/specs/MaxMPRule.spec b/certora/specs/MaxMPRule.spec
new file mode 100644
index 0000000..b13b890
--- /dev/null
+++ b/certora/specs/MaxMPRule.spec
@@ -0,0 +1,17 @@
+import "./shared.spec";
+
+methods {
+  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+}
+
+invariant MPcantBeGreaterThanMaxMP(address addr)
+  to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountBonusMultiplierPoints(addr)
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+  { preserved {
+      requireInvariant InitialMPIsNeverSmallerThanBalance(addr);
+      requireInvariant CurrentMPIsNeverSmallerThanInitialMP(addr);
+    }
+  }
+
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 28b6c06..f964f85 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -85,29 +85,18 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
-invariant InitialMPIsNeverSmallerThanBalance(address addr)
-  to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
+invariant accountBonusMPIsZeroIfBalanceIsZero(address addr)
+  to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0
   filtered {
     f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
   }
 
-invariant CurrentMPIsNeverSmallerThanInitialMP(address addr)
-  to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBonusMultiplierPoints(addr))
+invariant accountMPIsZeroIfBalanceIsZero(address addr)
+  to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0
   filtered {
     f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
   }
 
-invariant MPcantBeGreaterThanMaxMP(address addr)
-  to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountBonusMultiplierPoints(addr)
-  filtered {
-    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
-  }
-  { preserved {
-      requireInvariant InitialMPIsNeverSmallerThanBalance(addr);
-      requireInvariant CurrentMPIsNeverSmallerThanInitialMP(addr);
-    }
-  }
-
 rule reachability(method f)
 {
   calldataarg args;
diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec
index a4731e2..053e710 100644
--- a/certora/specs/shared.spec
+++ b/certora/specs/shared.spec
@@ -39,4 +39,15 @@ function getAccountLockUntil(address addr) returns uint256 {
   return lockUntil;
 }
 
+invariant InitialMPIsNeverSmallerThanBalance(address addr)
+  to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
+  filtered {
+    f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
+  }
+
+invariant CurrentMPIsNeverSmallerThanInitialMP(address addr)
+  to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBonusMultiplierPoints(addr))
+  filtered {
+    f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
+  }
 
diff --git a/package.json b/package.json
index a996c58..c14fb1f 100644
--- a/package.json
+++ b/package.json
@@ -38,6 +38,7 @@
     "verify:stake_manager": "certoraRun certora/confs/StakeManager.conf",
     "verify:stake_manager_start_migration": "certoraRun certora/confs/StakeManagerStartMigration.conf",
     "verify:stake_manager_process": "certoraRun certora/confs/StakeManagerProcess.conf",
+    "verify:max_mp_rule": "certoraRun certora/confs/MaxMPRule.conf",
     "release": "commit-and-tag-version",
     "adorno": "pnpm prettier:write && forge fmt && pnpm gas-report"
   },