Relayer: Implement prover rules

.github/workflows/prover-relayer.yml

@@ -0,0 +1,23 @@
+name: Prover Relayer
+
+env:
+  CI: true
+
+on:
+  pull_request:
+    branches: "*"
+    paths:
+      - packages/relayer/**
+
+jobs:
+  prove:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Prove
+        uses: ./.github/actions/certora
+        with:
+          workspace: '@mimic-fi/v3-relayer'
+          certora-key: ${{ secrets.CERTORA_KEY }}
+          github-token: ${{ secrets.GITHUB_TOKEN }}

packages/relayer/certora/conf/relayer.conf

@@ -0,0 +1,26 @@
+{
+  "files": [
+    "certora/harnesses/RelayerHarness.sol",
+    "certora/helpers/Helpers.sol",
+    "certora/helpers/Depositor.sol"
+  ],
+  "verify": "RelayerHarness:certora/specs/Relayer.spec",
+  "loop_iter": "3",
+  "rule_sanity": "basic",
+  "send_only": true,
+  "optimistic_hashing": true,
+  "prover_args": [
+    "-copyLoopUnroll 8",
+    "-optimisticFallback true"
+  ],
+  "optimistic_loop": true,
+  "packages": [
+    "@mimic-fi/v3-authorizer=../../node_modules/@mimic-fi/v3-authorizer",
+    "@mimic-fi/v3-smart-vault=../../node_modules/@mimic-fi/v3-smart-vault",
+    "@mimic-fi/v3-tasks=../../node_modules/@mimic-fi/v3-tasks",
+    "@openzeppelin=../../node_modules/@openzeppelin"
+  ],
+  "solc_allow_path": ".",
+  "process": "emv",
+  "msg": "RelayerHarness"
+}

packages/relayer/certora/harnesses/RelayerHarness.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+pragma solidity ^0.8.17;
+
+import '../../contracts/Relayer.sol';
+
+contract RelayerHarness is Relayer {
+    constructor(address executor, address collector, address owner) Relayer(executor, collector, owner) {
+        // solhint-disable-previous-line no-empty-blocks
+    }
+
+    function payTransactionGasToRelayer(address smartVault, uint256 amount) external {
+        _payTransactionGasToRelayer(smartVault, amount);
+    }
+}

packages/relayer/certora/helpers/Depositor.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+pragma solidity ^0.8.0;
+
+contract Depositor {
+    fallback() external payable {
+        // solhint-disable-previous-line no-empty-blocks
+    }
+}

packages/relayer/certora/helpers/Helpers.sol

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+pragma solidity ^0.8.0;
+
+import '@mimic-fi/v3-smart-vault/contracts/interfaces/ISmartVault.sol';
+import '@mimic-fi/v3-tasks/contracts/interfaces/ITask.sol';
+
+contract Helpers {
+    function balanceOf(address account) external view returns (uint256) {
+        return address(account).balance;
+    }
+
+    function areValidTasks(address[] memory tasks) external view returns (bool) {
+        if (tasks.length == 0) return false;
+
+        address smartVault = ITask(tasks[0]).smartVault();
+
+        for (uint256 i = 0; i < tasks.length; i++) {
+            address taskSmartVault = ITask(tasks[i]).smartVault();
+            if (taskSmartVault != smartVault) return false;
+
+            bool hasPermissions = ISmartVault(smartVault).hasPermissions(tasks[i]);
+            if (!hasPermissions) return false;
+        }
+
+        return true;
+    }
+}

packages/relayer/certora/specs/General.spec

@@ -0,0 +1,6 @@
+rule sanity(method f) good_description "Sanity" {
+    env e;
+    calldataarg args;
+    f(e, args);
+    assert false;
+}