chore(certora): add sumOfBalancesIsTotalStaked invariant

Closes #24

.github/workflows/ci.yml

@@ -139,7 +139,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install Certora CLI
-        run: pip3 install certora-cli==5.0.5
+        run: pip3 install certora-cli==7.17.2
 
       - name: Install Solidity
         run: |

certora/confs/RewardsStreamerMP.conf

@@ -1,9 +1,15 @@
 {
-  "files": ["src/RewardsStreamerMP.sol"],
+  "files": [
+    "src/RewardsStreamerMP.sol",
+    "certora/helpers/ERC20A.sol"
+  ],
+  "link" : [
+    "RewardsStreamerMP:STAKING_TOKEN=ERC20A",
+    "RewardsStreamerMP:REWARD_TOKEN=ERC20A"
+  ],
   "msg": "Verifying RewardsStreamerMP.sol",
   "rule_sanity": "basic",
   "verify": "RewardsStreamerMP:certora/specs/RewardsStreamerMP.spec",
-  "wait_for_results": "all",
   "optimistic_loop": true,
   "loop_iter": "3",
   "packages": [

certora/helpers/ERC20A.sol

@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.26;
+
+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/RewardsStreamerMP.spec

@@ -1,3 +1,16 @@
-rule test {
+using ERC20A as staked;
-    assert true;
+
+methods {
+    function totalStaked() external returns (uint256) envfree;
 }
+
+ghost mathint sumOfBalances {
+	init_state axiom sumOfBalances == 0;
+}
+
+hook Sstore users[KEY address account].stakedBalance uint256 newValue (uint256 oldValue) {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+invariant sumOfBalancesIsTotalStaked()
+  sumOfBalances == to_mathint(totalStaked());