chore: certora setup for stakemanager and vault

certora/confs/StakeManager.conf

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

certora/confs/StakeVault.conf

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

certora/helpers/ERC20A.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.19;
+
+import { ERC20 } from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+
+contract ERC20A is ERC20 {
+   constructor(string memory name_, string memory symbol_) ERC20(name_, symbol_) {}
+}

certora/specs/StakeManager.spec

@@ -1,4 +1,50 @@
-
-rule shouldPass {
-  assert true;
+using ERC20A as staked;
+methods {
+  function staked.balanceOf(address) external returns (uint256) envfree;
+}
+
+function isMigrationfunction(method f) returns bool {
+  return  f.selector == sig:leave().selector ||
+          f.selector == sig:migrate(address,StakeManager.Account).selector ||
+          f.selector == sig:migrate().selector;
+}
+
+/*  assume that migration is zero, causing the verification to take into account only
+ cases where it is zero. specifically no externall call to the migration contract */
+function simplification() {
+  require currentContract.migration == 0;
+}
+
+
+rule reachability(method f)
+{
+  calldataarg args;
+  env e;
+  f(e,args);
+  satisfy true;
+}
+
+/**
+@title when there is no migration - some functions must revert.
+Other function should have non reverting cases
+**/
+rule revertsWhenNoMigration(method f) {
+  calldataarg args;
+  env e;
+  require currentContract.migration == 0;
+  f@withrevert(e,args);
+  bool reverted = lastReverted;
+  if (!isMigrationfunction(f))
+    satisfy !reverted;
+  assert isMigrationfunction(f) => reverted;
+}
+
+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);
 }

certora/specs/StakeVault.spec

@@ -0,0 +1,28 @@
+using ERC20A as staked;
+using StakeManager as stakeManager;
+methods {
+  function ERC20A.balanceOf(address) external returns (uint256) envfree;
+}
+
+/*  assume that migration is zero, causing to ignore cases where it is not zero */
+function simplification() {
+  require stakeManager.migration == 0;
+}
+
+rule reachability(method f){
+  calldataarg args;
+  env e;
+  f(e,args);
+  satisfy true;
+}
+
+rule whoChangeERC20Balance(method f)
+{
+  simplification();
+  address user;
+  uint256 before = staked.balanceOf(user);
+  calldataarg args;
+  env e;
+  f(e,args);
+  assert before == staked.balanceOf(user);
+}

contracts/StakeVault.sol

@@ -20,7 +20,7 @@ contract StakeVault is Ownable {
 
     StakeManager private stakeManager;
 
-    ERC20 private immutable STAKED_TOKEN;
+    ERC20 public immutable STAKED_TOKEN;
 
     event Staked(address from, address to, uint256 _amount, uint256 time);
 

package.json

@@ -20,9 +20,11 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "verify": "certoraRun certora/certora.conf",
+    "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager",
     "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"
+    "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",
+    "verify:stake_vault": "certoraRun certora/confs/StakeVault.conf",
+    "verify:stake_manager": "certoraRun certora/confs/StakeManager.conf"
   }
 }