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.
logos-co · Oct 8, 2024 · 44be126 · 44be126
1 parent da6cac4
commit 44be126
Show file tree

Hide file tree

Showing 6 changed files with 64 additions and 15 deletions.
diff --git 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
@@ -0,0 +1,30 @@
+{
+	"files": [
+		"contracts/StakeManager.sol",
+		"certora/helpers/StakeRewardEstimateA.sol",
+		"certora/helpers/ERC20A.sol"
+	],
+	"global_timeout": "7200",
+	"link": [
+		"StakeManager:stakedToken=ERC20A",
+		"StakeManager:stakeRewardEstimate=StakeRewardEstimateA"
+	],
+	"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}]"
+	],
+	"rule": [
+		"MPcantBeGreaterThanMaxMP"
+	],
+	"smt_timeout": "7200",
+	"verify": "StakeManager:certora/specs/MaxMPRule.spec"
+}
+
+
diff --git a/certora/specs/MaxMPRule.spec 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
@@ -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
@@ -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
@@ -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"
   },