test: rewards certora spec

.github/workflows/certora-prover-conf.yml

@@ -0,0 +1,60 @@
+name: Certora Prover
+
+on:
+  push:
+    branches:
+      - dev
+      - payments-spec
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  list-scripts:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - uses: actions/checkout@v2
+      - id: set-matrix
+        run: echo ::set-output name=matrix::$(ls certora/config/*.conf | jq -Rsc 'split("\n")[:-1]')
+  verify:
+    runs-on: ubuntu-latest
+    needs: list-scripts
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+      - name: Install forge dependencies
+        run: forge install
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+          cache: 'pip'
+      - name: Install java
+        uses: actions/setup-java@v2
+        with:
+          distribution: temurin
+          java-version: '17'
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify rule ${{ matrix.params }}
+        run: |
+          certoraRun ${{ matrix.params }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params: ${{ fromJson(needs.list-scripts.outputs.matrix) }}

certora/conf/rewardsCoordinator.conf

@@ -0,0 +1,28 @@
+{
+    "files": [
+        "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/presets/ERC20PresetFixedSupply.sol",
+        "certora/harnesses/RewardsCoordinatorHarness.sol"
+    ],
+    "verify": "RewardsCoordinatorHarness:certora/specs/core/RewardsCoordinator.spec",
+    "loop_iter": "2",
+    "parametric_contracts": ["RewardsCoordinatorHarness"],
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts",
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable"
+    ],
+    "link": [],
+    "optimistic_fallback": true,
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "rule_sanity": "basic",
+    "exclude_rule": ["checkClaimNeverFalse"],
+    "mutations": {
+        "gambit": [
+            {
+                "filename" : "src/contracts/core/RewardsCoordinator.sol",
+                "num_mutants": 20
+            }
+        ],
+    }
+}

certora/harnesses/RewardsCoordinatorHarness.sol

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.12;
+
+import "../../src/contracts/core/RewardsCoordinator.sol";
+
+contract RewardsCoordinatorHarness is RewardsCoordinator {
+    constructor(
+        IDelegationManager _delegationManager,
+        IStrategyManager _strategyManager,
+        uint32 _CALCULATION_INTERVAL_SECONDS,
+        uint32 _MAX_PAYMENT_DURATION,
+        uint32 _MAX_RETROACTIVE_LENGTH,
+        uint32 _MAX_FUTURE_LENGTH,
+        uint32 _GENESIS_PAYMENT_TIMESTAMP
+    ) RewardsCoordinator(
+        _delegationManager,
+        _strategyManager,
+        _CALCULATION_INTERVAL_SECONDS,
+        _MAX_PAYMENT_DURATION,
+        _MAX_RETROACTIVE_LENGTH,
+        _MAX_FUTURE_LENGTH,
+        _GENESIS_PAYMENT_TIMESTAMP
+    ) {}
+}

certora/specs/core/RewardsCoordinator.spec

@@ -0,0 +1,113 @@
+
+using ERC20 as token1;
+using ERC20PresetFixedSupply as token2;
+
+methods {
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+
+    function _.createAVSRewardsSubmission(IRewardsCoordinator.RewardsSubmission[]) external => DISPATCHER(true);
+    function _.createRewardsForAllSubmission(IRewardsCoordinator.RewardsSubmission[]) external => DISPATCHER(true);
+    function _.submitRoot(bytes32 root, uint32 rewardsCalculationEndTimestamp) external => DISPATCHER(true);
+    function _.processClaim(IRewardsCoordinator.RewardsMerkleClaim claim, address recipient) external => DISPATCHER(true);
+
+    function _.verifyInclusionKeccak(bytes memory, bytes32, bytes32, uint256) internal => CONSTANT;
+    function cumulativeClaimed(address, address) external returns(uint256) envfree;
+
+    function _.strategyIsWhitelistedForDeposit(address) external => NONDET;
+    function _.isPauser(address) external => NONDET;
+    function _.unpauser() external => NONDET;
+    function _._ external => DISPATCH [
+        _.transferFrom(address, address, uint256),
+        _.transfer(address, uint256)
+    ] default NONDET;
+}
+
+
+// Given a processClaim passes, second processClaim reverts
+// Assumptions
+// - checkClaim(claim) == true and does not revert
+// - claim has non-empty tokenLeaves
+/// status: pass
+rule claimWithduplicateTokenLeafs(env e, IRewardsCoordinator.RewardsMerkleClaim claim, address recipient) {
+    require claim.tokenLeaves.length == 1;
+
+    checkClaim(e, claim);
+
+    if ((claimerFor(e, claim.earnerLeaf.earner)) != 0) {
+        require e.msg.sender == claimerFor(e, claim.earnerLeaf.earner);
+    } else {
+        require e.msg.sender == claim.earnerLeaf.earner;
+    }
+
+    processClaim(e, claim, recipient);
+    processClaim@withrevert(e, claim, recipient);
+
+	assert (
+        lastReverted,
+        "First claim passing with token claims means second claim should revert"
+    );
+}
+
+/// status: pass
+rule cumulativeClaimedStrictlyIncreasing(env e, address claimToken, address earner) {
+    uint256 cumulativeClaimedBefore = cumulativeClaimed(earner, claimToken);
+    calldataarg args;
+    method f;
+    f(e, args);
+    uint256 cumulativeClaimedAfter = cumulativeClaimed(earner, claimToken);
+
+    assert(cumulativeClaimedAfter >= cumulativeClaimedBefore);
+}
+
+
+/// Check that transfer amount in RewardsCoordinator.prcocessClaim() is equal to leaf.cumulativeEarnings - cumulativeClaimed
+/// cumulativeEarnings - cumulativeClaimed == balanceAfter - balanceBefore
+/// Initially failed from havoc from token safeTransfer in the calldata. Fixed by having unresolved catch-all calls defined
+/// status: pass
+rule transferredTokensFromClaim(env e, IRewardsCoordinator.RewardsMerkleClaim claim, address recipient) {
+    require claim.tokenLeaves.length == 2;
+    require token1 == claim.tokenLeaves[0].token;
+    require token2 == claim.tokenLeaves[1].token;
+    // if recipient is the RewardsCoordinator, rule breaks since balanceAfter == balanceBefore 
+    require recipient != currentContract;
+
+    address earner = claim.earnerLeaf.earner;
+    uint256 token1BalanceBefore = token1.balanceOf(e, recipient);
+    uint256 token2BalanceBefore = token2.balanceOf(e, recipient);
+    uint256 token1CumulativeClaimed = cumulativeClaimed(earner, claim.tokenLeaves[0].token);
+    uint256 token2CumulativeClaimed = cumulativeClaimed(earner, claim.tokenLeaves[1].token);
+
+    processClaim(e, claim, recipient);
+
+    uint256 token1BalanceAfter = token1.balanceOf(e, recipient);
+    uint256 token2BalanceAfter = token2.balanceOf(e, recipient);
+
+    if (token1 == token2) {
+        // In practice this shouldn't occur as we will not construct leaves with multiple tokenLeaves with the same token address
+        assert claim.tokenLeaves[1].cumulativeEarnings - token1CumulativeClaimed == token2BalanceAfter - token2BalanceBefore;
+    } else {
+        assert claim.tokenLeaves[0].cumulativeEarnings - token1CumulativeClaimed == token1BalanceAfter - token1BalanceBefore;
+        assert claim.tokenLeaves[1].cumulativeEarnings - token2CumulativeClaimed == token2BalanceAfter - token2BalanceBefore;
+    }
+}
+
+/// RewardsCoordinator.checkClaim == True => processClaim success 
+/// status: pass
+rule claimCorrectness(env e, IRewardsCoordinator.RewardsMerkleClaim claim, address recipient) {
+    // Call checkClaim to ensure it does not revert in rule since it never returns false
+    checkClaim(e, claim);
+
+    bool canWork = claimerFor(e, claim.earnerLeaf.earner) != 0 ? 
+        e.msg.sender == claimerFor(e, claim.earnerLeaf.earner) :
+        e.msg.sender == claim.earnerLeaf.earner;
+
+    processClaim@withrevert(e, claim, recipient);
+
+    assert !lastReverted => canWork;
+}
+
+/// checkClaim either returns True or reverts otherwise
+invariant checkClaimNeverFalse(env e, IRewardsCoordinator.RewardsMerkleClaim claim)
+    !checkClaim(e, claim);