chore: make certora rules passa gain

logos-co · Sep 4, 2024 · e21b333 · e21b333
1 parent 6df329d
commit e21b333
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 16 deletions.
diff --git a/certora/confs/StakeManager.conf b/certora/confs/StakeManager.conf
@@ -1,17 +1,20 @@
 {
-  "files": 
+  "files":
     ["contracts/StakeManager.sol",
+    "certora/helpers/StakeRewardEstimateA.sol",
       "certora/helpers/ERC20A.sol"
     ],
   "link" : [
-    "StakeManager:stakedToken=ERC20A"
+    "StakeManager:stakedToken=ERC20A",
+    "StakeManager:stakeRewardEstimate=StakeRewardEstimateA"
   ],
   "msg": "Verifying StakeManager.sol",
   "rule_sanity": "basic",
   "verify": "StakeManager:certora/specs/StakeManager.spec",
   "optimistic_loop": true,
   "loop_iter": "3",
   "packages": [
+    "forge-std=lib/forge-std/src",
     "@openzeppelin=lib/openzeppelin-contracts"
   ]
 }

diff --git a/certora/confs/StakeManagerProcess.conf b/certora/confs/StakeManagerProcess.conf
@@ -1,17 +1,20 @@
 {
-  "files": 
+  "files":
     ["contracts/StakeManager.sol",
-      "certora/helpers/ERC20A.sol"
+      "certora/helpers/ERC20A.sol",
+      "certora/helpers/StakeRewardEstimateA.sol"
     ],
   "link" : [
-    "StakeManager:stakedToken=ERC20A"
+    "StakeManager:stakedToken=ERC20A",
+    "StakeManager:stakeRewardEstimate=StakeRewardEstimateA"
   ],
   "msg": "Verifying StakeManager ProcessAccount",
   "rule_sanity": "basic",
   "verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec",
   "optimistic_loop": true,
   "loop_iter": "3",
   "packages": [
+    "forge-std=lib/forge-std/src",
     "@openzeppelin=lib/openzeppelin-contracts"
   ]
 }

diff --git a/certora/helpers/StakeRewardEstimateA.sol b/certora/helpers/StakeRewardEstimateA.sol
@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.19;
+
+import { StakeRewardEstimate } from "./../../contracts/StakeManager.sol";
+
+contract StakeRewardEstimateA is StakeRewardEstimate {}
+
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
@@ -6,9 +6,10 @@ methods {
   function previousManager() external returns (address) envfree;
   function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
   function _.increaseTotalMP(uint256) external => NONDET;
-  function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
-  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+  function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
+  function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
   function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
+  function _._ external => DISPATCH [] default NONDET;
 }
 
 function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
@@ -18,28 +19,28 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
 
 function getAccountBalance(address addr) returns uint256 {
   uint256 balance;
-  _, balance, _, _, _, _, _ = accounts(addr);
+  _, balance, _, _, _, _, _, _ = accounts(addr);
 
   return balance;
 }
 
 function getAccountBonusMultiplierPoints(address addr) returns uint256 {
   uint256 bonusMP;
-  _, _, bonusMP, _, _, _, _ = accounts(addr);
+  _, _, bonusMP, _, _, _, _, _ = accounts(addr);
 
   return bonusMP;
 }
 
 function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
   uint256 totalMP;
-  _, _, _, totalMP, _, _, _ = accounts(addr);
+  _, _, _, totalMP, _, _, _, _  = accounts(addr);
 
   return totalMP;
 }
 
 function getAccountLockUntil(address addr) returns uint256 {
   uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _ = accounts(addr);
+  _, _, _, _, _, lockUntil, _, _  = accounts(addr);
 
   return lockUntil;
 }
@@ -59,7 +60,7 @@ function simplification(env e) {
 }
 
 definition requiresPreviousManager(method f) returns bool = (
-  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
+  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
   f.selector == sig:increaseTotalMP(uint256).selector
   );

diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
@@ -2,10 +2,13 @@ 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 totalSupplyMP() external returns (uint256) envfree;
+  function totalMPPerEpoch() external returns (uint256) envfree;
+  function accounts(address) external returns(address, uint256, 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;
+  function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
+  function pendingMPToBeMinted() external returns (uint256) envfree;
 }
 
 // keeps track of the last epoch an account was processed
@@ -19,7 +22,7 @@ function markAccountProccessed(address account, uint256 _limitEpoch) {
 
 function getAccountLockUntil(address addr) returns uint256 {
   uint256 lockUntil;
-  _, _, _, _, _, lockUntil, _ = accounts(addr);
+  _, _, _, _, _, lockUntil, _, _ = accounts(addr);
 
   return lockUntil;
 }
@@ -29,7 +32,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
 }
 
 definition requiresPreviousManager(method f) returns bool = (
-  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
+  f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
   f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
   f.selector == sig:increaseTotalMP(uint256).selector
   );