test: spec progress with CI

.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/config/paymentCoordinator.conf

@@ -1,6 +1,7 @@
 {
     "files": [
         "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/presets/ERC20PresetFixedSupply.sol",
         "certora/harnesses/PaymentCoordinatorHarness.sol"
     ],
     "verify": "PaymentCoordinatorHarness:certora/specs/core/PaymentCoordinator.spec",
@@ -14,5 +15,13 @@
     "optimistic_fallback": true,
     "optimistic_loop": true,
     "optimistic_hashing": true,
-    "rule_sanity": "basic"
+    "rule_sanity": "basic",
+    "mutations": {
+        "gambit": [
+            {
+                "filename" : "src/contracts/core/PaymentCoordinator.sol",
+                "num_mutants": 5
+            }
+        ],
+    }
 }

certora/specs/core/PaymentCoordinator.spec

@@ -1,5 +1,6 @@
 
-using ERC20 as token;
+using ERC20 as token1;
+using ERC20PresetFixedSupply as token2;
 
 methods {
 
@@ -17,48 +18,24 @@ methods {
     function _.submitRoot(bytes32 root, uint32 paymentCalculationEndTimestamp) external => DISPATCHER(true);
     function _.processClaim(IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) external => DISPATCHER(true);
 
-    // function PaymentCoordinator._checkClaim(
-    //     IPaymentCoordinator.PaymentMerkleC   laim calldata claim,
-    //     IPaymentCoordinator.DistributionRoot memory root
-    // ) internal => NONDET;
-}
-
-// Do not need
-// paymentCoordinator.submitRoot() adds a merkle root to the contract with a 7 day activationDelay
-
-// // Check how accept root changes the storage.
-// rule acceptRootStorageChange(env e) {
-//     bytes32 pendingRoot; bytes32 pendingIpfsHash;
-//     pendingRoot, pendingIpfsHash, _ = pendingRoot();
-
-//     acceptRoot(e);
-
-//     assert root() == pendingRoot;
-//     assert ipfsHash() == pendingIpfsHash;
-// }
-
-// // Check an account claimed amount is correctly updated.
-// rule updatedClaimedAmount(address account, address reward, uint256 claimable, bytes32[] proof) {
-//     claim(account, reward, claimable, proof);
-
-//     assert claimable == claimed(account, reward);
-// }
-
-// // Check an account can only claim greater amounts each time.
-// rule increasingClaimedAmounts(address account, address reward, uint256 claimable, bytes32[] proof) {
-//     uint256 claimed = claimed(account, reward);
-
-//     claim(account, reward, claimable, proof);
+    function _.verifyInclusionKeccak(bytes memory, bytes32, bytes32, uint256) internal => CONSTANT;
+    function cumulativeClaimed(address, address) external returns(uint256) envfree;
 
-//     assert claimable > claimed;
-// }
+    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;
+}
 
 
-// 2. Given a processClaim passes, second processClaim reverts
-// Rule status: FAILS
+// 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, IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) {
     require claim.tokenLeaves.length == 1;
 
@@ -82,23 +59,47 @@ rule claimWithduplicateTokenLeafs(env e, IPaymentCoordinator.PaymentMerkleClaim
     );
 }
 
+/// status: pending
+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 paymentCoordinator.prcocessClaim() is equal to leaf.cumulativeEarnings - cumulativeClaimed
+/// Check that transfer amount in paymentCoordinator.prcocessClaim() is equal to leaf.cumulativeEarnings - cumulativeClaimed
 /// cumulativeEarnings - cumulativeClaimed == balanceAfter - balanceBefore
-/// status: Fail, havoc from token safeTransfer in the calldata
+/// Initially failed from havoc from token safeTransfer in the calldata. Fixed by having unresolved catch-all calls defined
+/// status: pass
 rule transferredTokensFromClaim(env e, IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) {
-    require claim.tokenLeaves.length >= 1;
-    require token == claim.tokenLeaves[0].token;
+    require claim.tokenLeaves.length == 2;
+    require token1 == claim.tokenLeaves[0].token;
+    require token2 == claim.tokenLeaves[1].token;
+    // if recipient is the PaymentCoordinator, rule breaks since balanceAfter == balanceBefore 
+    require recipient != currentContract;
 
     address earner = claim.earnerLeaf.earner;
-    uint256 balanceBefore = token.balanceOf(e, recipient);
-    uint256 cumulativeClaimed = cumulativeClaimed(e, earner, claim.tokenLeaves[0].token);
+    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 balanceAfter = token.balanceOf(e, recipient);
+    uint256 token1BalanceAfter = token1.balanceOf(e, recipient);
+    uint256 token2BalanceAfter = token2.balanceOf(e, recipient);
 
-    assert claim.tokenLeaves[0].cumulativeEarnings - cumulativeClaimed == balanceAfter - balanceBefore;
+    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;
+    }
 }
 
 /// paymentCoordinator.checkClaim == True => processClaim success