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

@@ -173,3 +173,4 @@ jobs:
           - verify:stake_manager
           - verify:stake_manager_process
           - verify:stake_manager_start_migration
+          - verify:max_mp_rule

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"
+}
+
+

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);
+    }
+  }
+

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;

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
+  }
 

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"
   },