Merge pull request #24 from Certora/verification_stakingReward

Verification staking reward

.gitignore

@@ -36,4 +36,9 @@ coverage/
 
 # Invariant testing files
 crytic-export/
-_corpus/
+_corpus/
+
+# Certora verrifiction temp files 
+.certora_internal/
+gambit_out/
+collect.json

certora/conf/StakingRewardStream.conf

@@ -0,0 +1,45 @@
+{
+    "files": [
+        "src/StakingRewardStreams.sol",
+        "certora/harness/ERC20Caller.sol"
+    ],
+    "packages": [
+        "evc=lib/ethereum-vault-connector/src",
+        "openzeppelin-contracts=lib/openzeppelin-contracts/contracts",
+        "forge-std=lib/forge-std/src"
+    ],
+    "verify": "StakingRewardStreams:certora/specs/StakingRewardStreams.spec",
+    "solc": "solc8.23",
+    "rule_sanity": "basic",
+    "optimistic_loop": true,
+    "loop_iter": "3",
+    "parametric_contracts" : ["StakingRewardStreams","ERC20Caller"],
+
+    // Gambit config
+    "mutations": {
+        // Automatically generated mutations
+        "gambit": [
+            {
+                "filename": "src/StakingRewardStreams.sol",
+                "num_mutants": 2
+            },
+            {
+                "filename": "src/BaseRewardStreams.sol",
+                "num_mutants": 3
+            }
+        ],
+        // Manual mutations
+        "manual_mutants": [
+            {
+                "file_to_mutate": "src/StakingRewardStreams.sol",
+                "mutants_location": "certora/mutations/staking/"
+            },
+            {
+                "file_to_mutate": "src/BaseRewardStreams.sol",
+                "mutants_location": "certora/mutations/base/"
+            }
+        ],
+
+        "msg": "Mutations example"
+    }
+}

certora/harness/ERC20Caller.sol

@@ -0,0 +1,11 @@
+pragma solidity ^0.8.20;
+
+import {IERC20} from "openzeppelin-contracts/token/ERC20/IERC20.sol";
+
+
+contract ERC20Caller {
+
+    function externalTransfer(IERC20 token, address to, uint256 amount) public {
+        token.transferFrom(msg.sender,to,amount);
+    }
+}