certora setup for stakemanager and vault

certora/certora.conf → 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.18;
+
+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 @@
+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;
+}
 
-rule shouldPass {
-  assert true;
+/*  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,31 @@
+using ERC20A as staked;
+using StakeManager as stakeManger; 
+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 stakeManger.migration == 0;  
+}
+
+rule reachability(method f){
+  calldataarg args;
+  env e;
+  simplification();
+  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

@@ -17,7 +17,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);