chore(StakeManagerProcessAccount.spec): add specs for processAccount

This primarily adds a rule that ensures that, when an account's
`balance` changes, `_processAccount()` must have been called as well.

There's very few exceptions where an account's `balance` can change
without the need of `_processAccount()` but those functions have been
deliberately excluded from the rule.

certora/confs/StakeManagerProcess.conf

@@ -0,0 +1,19 @@
+{
+  "files": 
+    ["contracts/StakeManager.sol",
+      "certora/helpers/ERC20A.sol"
+    ],
+  "link" : [
+    "StakeManager:stakedToken=ERC20A"
+  ],
+  "msg": "Verifying StakeManager ProcessAccount",
+  "rule_sanity": "basic",
+  "verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "packages": [
+    "@openzeppelin=lib/openzeppelin-contracts"
+  ]
+}
+
+

certora/specs/StakeManagerProcessAccount.spec

@@ -0,0 +1,86 @@
+using ERC20A as staked;
+methods {
+  function staked.balanceOf(address) external returns (uint256) envfree;
+  function totalSupplyBalance() external returns (uint256) envfree;
+  function accounts(address) external returns(address, 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) external => NONDET;
+}
+
+// keeps track of the last epoch an account was processed
+ghost mapping (address => mathint) accountProcessed;
+// balance changed in an epoch that was processed
+ghost mapping (address => mathint) balanceChangedInEpoch;
+
+function markAccountProccessed(address account, uint256 _limitEpoch) {
+    accountProcessed[account] = to_mathint(_limitEpoch);
+}
+
+function getAccountLockUntil(address addr) returns uint256 {
+  uint256 lockUntil;
+  _, _, _, _, _, lockUntil, _ = accounts(addr);
+
+  return lockUntil;
+}
+
+hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
+    balanceChangedInEpoch[addr] = accountProcessed[addr];
+}
+
+definition requiresPreviousManager(method f) returns bool = (
+  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
+  f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
+  f.selector == sig:increaseMPFromMigration(uint256).selector
+  );
+
+definition requiresNextManager(method f) returns bool = (
+  f.selector == sig:migrateTo(bool).selector ||
+  f.selector == sig:transferNonPending().selector
+  );
+
+/*
+  If a balance of an account has changed, the account should have been processed up to the `currentEpoch`.
+  This is filtering out most of migration related functions, as those will be vacuous.
+
+  Verified on two mutations:
+  https://prover.certora.com/output/40726/68668bbb7b6e49828da8521c3425a20b/?anonymousKey=015fce76d5d66ef40de8342b75fda4cff1dfdd57
+  https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8
+*/
+rule checkAccountProcessedBeforeStoring(method f) filtered {
+  f -> !requiresPreviousManager(f) && !requiresNextManager(f)
+} {
+  address account;
+
+  mathint lastChanged = balanceChangedInEpoch[account];
+  env e;
+  calldataarg args;
+
+  require currentContract.migration == 0;
+
+  // If the account's `lockUntil` == 0, then the account will be initialized
+  // with the current epoch and no processing is required.
+  require getAccountLockUntil(account) > 0;
+
+  f(e,args);
+
+  assert  balanceChangedInEpoch[account] != lastChanged  =>
+          balanceChangedInEpoch[account] == to_mathint(currentContract.currentEpoch);
+
+}
+
+/*
+Below is a rule that finds all methods that change an account's balance.
+This is just for debugging purposes and not meant to be a production rule.
+Hence it is commented out.
+*/
+/*
+rule whoChangeERC20Balance(  method f ) filtered { f -> f.contract != staked }
+{
+  address user;
+  uint256 before = staked.balanceOf(user);
+  calldataarg args;
+  env e;
+  f(e,args);
+  assert before == staked.balanceOf(user);
+} */

package.json

@@ -21,7 +21,7 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration",
+    "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process",
     "lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol",
     "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
     "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",
@@ -29,6 +29,7 @@
     "verify:stake_vault": "certoraRun certora/confs/StakeVault.conf",
     "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",
     "release": "commit-and-tag-version"
   }
 }