From 279f14a57bd462ef70bdfa5c4def52322ad1ec00 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:03:56 +0100
Subject: [PATCH 01/31] feat: import distributor verification

---
 .github/workflows/certora.yml                 |  51 +++++++++
 .gitignore                                    |   6 +-
 certora/README.md                             |  60 ++++++++++
 certora/checker/Checker.sol                   |  53 +++++++++
 certora/checker/create_certificate.py         |  78 +++++++++++++
 certora/confs/MerkleTrees.conf                |  12 ++
 .../confs/UniversalRewardsDistributor.conf    |  14 +++
 certora/helpers/MerkleTreeLib.sol             | 108 ++++++++++++++++++
 certora/helpers/MerkleTrees.sol               |  65 +++++++++++
 certora/helpers/Util.sol                      |  10 ++
 certora/specs/MerkleTrees.spec                |  36 ++++++
 .../specs/UniversalRewardsDistributor.spec    |  66 +++++++++++
 12 files changed, 558 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/certora.yml
 create mode 100644 certora/README.md
 create mode 100644 certora/checker/Checker.sol
 create mode 100644 certora/checker/create_certificate.py
 create mode 100644 certora/confs/MerkleTrees.conf
 create mode 100644 certora/confs/UniversalRewardsDistributor.conf
 create mode 100644 certora/helpers/MerkleTreeLib.sol
 create mode 100644 certora/helpers/MerkleTrees.sol
 create mode 100644 certora/helpers/Util.sol
 create mode 100644 certora/specs/MerkleTrees.spec
 create mode 100644 certora/specs/UniversalRewardsDistributor.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..619964b
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,51 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - MerkleTrees
+          - RewardsDistributor
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
+          cache: yarn
+
+      - name: Install dependencies
+        run: yarn install --frozen-lockfile
+        shell: bash
+
+      - name: Install python
+        uses: actions/setup-python@v4
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.13
+
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
index 9aa64ca..1818db5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,4 +15,8 @@ docs/
 
 # npm
 package-lock.json
-node_modules
\ No newline at end of file
+node_modules
+
+# certora
+.certora**
+emv-*-certora*
diff --git a/certora/README.md b/certora/README.md
new file mode 100644
index 0000000..396019f
--- /dev/null
+++ b/certora/README.md
@@ -0,0 +1,60 @@
+This folder contains the verification of the universal rewards distribution mechanism using CVL, Certora's Verification Language.
+
+# Folder and file structure
+
+The [`certora/specs`](specs) folder contains the specification files.
+
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
+
+The [`certora/helpers`](helpers) folder contains files that enable the verification of Morpho Blue.
+
+# Overview of the verification
+
+This work aims at providing a formally verified rewards checker.
+The rewards checker is composed of the [Checker.sol](checker/Checker.sol) file, which takes a certificate as an input.
+The certificate is assumed to contain the submitted root to verify, a total amount of rewards distributed, and a Merkle tree, and it is checked that:
+
+1. the Merkle tree is a well-formed Merkle tree
+2. the total amount of rewards distributed matches the total rewards contained in the Merkle tree
+
+Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants:
+
+- it is checked in [MerkleTrees.spec](specs/MerkleTrees.spec) that those functions lead to creating well-formed trees.
+  Well-formed trees also verify that the value of their internal node is the sum of the rewards it contains.
+- it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.
+
+# Getting started
+
+## Verifying the rewards checker
+
+Install `certora-cli` package with `pip install certora-cli`.
+To verify specification files, pass to `certoraRun` the corresponding configuration file in the [`certora/confs`](confs) folder.
+It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
+You can also pass additional arguments, notably to verify a specific rule.
+For example, at the root of the repository:
+
+```
+certoraRun certora/confs/MerkleTrees.conf --rule wellFormed
+```
+
+## Running the rewards checker
+
+To verify that a given list of proofs corresponds to a valid Merkle tree, you must generate a certificate from it.
+This assumes that the list of proofs is in the expected JSON format.
+For example, at the root of the repository, given a `proofs.json` file:
+
+```
+python certora/checker/create_certificate.py proofs.json
+```
+
+This requires installing the corresponding libraries first:
+
+```
+pip install web3 eth-tester py-evm
+```
+
+Then, verify this certificate:
+
+```
+FOUNDRY_PROFILE=checker forge test
+```
diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
new file mode 100644
index 0000000..e3b7bc0
--- /dev/null
+++ b/certora/checker/Checker.sol
@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import "../../lib/openzeppelin-contracts/contracts/utils/Strings.sol";
+import "../helpers/MerkleTreeLib.sol";
+import "../../lib/forge-std/src/Test.sol";
+import "../../lib/forge-std/src/StdJson.sol";
+
+contract Checker is Test {
+    using MerkleTreeLib for MerkleTreeLib.Tree;
+    using stdJson for string;
+
+    MerkleTreeLib.Tree public tree;
+
+    struct Leaf {
+        address addr;
+        uint256 value;
+    }
+
+    struct InternalNode {
+        address addr;
+        address left;
+        address right;
+    }
+
+    function testVerifyCertificate() public {
+        string memory projectRoot = vm.projectRoot();
+        string memory path = string.concat(projectRoot, "/certificate.json");
+        string memory json = vm.readFile(path);
+
+        uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
+        Leaf memory leaf;
+        for (uint256 i; i < leafLength; i++) {
+            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
+            tree.newLeaf(leaf.addr, leaf.value);
+        }
+
+        uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
+        InternalNode memory node;
+        for (uint256 i; i < nodeLength; i++) {
+            node = abi.decode(json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (InternalNode));
+            tree.newInternalNode(node.addr, node.left, node.right);
+        }
+
+        assertTrue(!tree.isEmpty(node.addr), "empty root");
+
+        uint256 total = abi.decode(json.parseRaw(".total"), (uint256));
+        assertEq(tree.getValue(node.addr), total, "incorrect total rewards");
+
+        bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
+        assertEq(tree.getHash(node.addr), root, "mismatched roots");
+    }
+}
diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
new file mode 100644
index 0000000..67387fd
--- /dev/null
+++ b/certora/checker/create_certificate.py
@@ -0,0 +1,78 @@
+import sys
+import json
+from web3 import Web3, EthereumTesterProvider
+
+w3 = Web3(EthereumTesterProvider())
+
+
+def keccak_node(left_hash, right_hash):
+    return w3.to_hex(
+        w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
+    )
+
+
+def keccak_leaf(address, amount):
+    address = w3.to_checksum_address(address)
+    return w3.to_hex(w3.solidity_keccak(["address", "uint256"], [address, amount]))
+
+
+certificate = {}
+hash_to_address = {}
+hash_to_value = {}
+left = {}
+right = {}
+
+
+def populate(address, amount, proof):
+    amount = int(amount)
+    computedHash = keccak_leaf(address, amount)
+    hash_to_address[computedHash] = address
+    hash_to_value[computedHash] = amount
+    for proofElement in proof:
+        [leftHash, rightHash] = (
+            [computedHash, proofElement]
+            if computedHash <= proofElement
+            else [proofElement, computedHash]
+        )
+        computedHash = keccak_node(leftHash, rightHash)
+        left[computedHash] = leftHash
+        right[computedHash] = rightHash
+        hash_to_address[computedHash] = keccak_node(computedHash, computedHash)[:42]
+
+
+def walk(h):
+    if h in left:
+        walk(left[h])
+        walk(right[h])
+        certificate["node"].append(
+            {
+                "addr": hash_to_address[h],
+                "left": hash_to_address[left[h]],
+                "right": hash_to_address[right[h]],
+            }
+        )
+    else:
+        certificate["leaf"].append(
+            {"addr": hash_to_address[h], "value": hash_to_value[h]}
+        )
+
+
+with open(sys.argv[1]) as input_file:
+    proofs = json.load(input_file)
+    certificate["root"] = proofs["root"]
+    certificate["total"] = int(proofs["total"])
+    certificate["leaf"] = []
+    certificate["node"] = []
+
+    for address, data in proofs["proofs"].items():
+        populate(address, data["amount"], data["proof"])
+
+    walk(proofs["root"])
+
+    certificate["leafLength"] = len(certificate["leaf"])
+    certificate["nodeLength"] = len(certificate["node"])
+
+    json_output = json.dumps(certificate)
+
+with open("certificate.json", "w") as output_file:
+    output_file.write(json_output)
diff --git a/certora/confs/MerkleTrees.conf b/certora/confs/MerkleTrees.conf
new file mode 100644
index 0000000..fcb22ad
--- /dev/null
+++ b/certora/confs/MerkleTrees.conf
@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/helpers/MerkleTrees.sol"
+    ],
+    "solc": "solc8.19",
+    "verify": "MerkleTrees:certora/specs/MerkleTrees.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Merkle Trees",
+}
diff --git a/certora/confs/UniversalRewardsDistributor.conf b/certora/confs/UniversalRewardsDistributor.conf
new file mode 100644
index 0000000..5537996
--- /dev/null
+++ b/certora/confs/UniversalRewardsDistributor.conf
@@ -0,0 +1,14 @@
+{
+    "files": [
+        "src/UniversalRewardsDistributor.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "certora/helpers/MerkleTrees.sol",
+        "certora/helpers/Util.sol",
+    ],
+    "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
+    "optimistic_loop": true,
+    "loop_iter": "2",
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Universal Rewards Distributor",
+}
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
new file mode 100644
index 0000000..f14e954
--- /dev/null
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -0,0 +1,108 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+library MerkleTreeLib {
+    using MerkleTreeLib for Node;
+
+    struct Node {
+        address left;
+        address right;
+        address reward;
+        uint256 value;
+        bytes32 hashNode;
+    }
+
+    function isEmpty(Node memory node) internal pure returns (bool) {
+        return node.left == address(0) && node.right == address(0) && node.reward == address(0) && node.value == 0
+            && node.hashNode == bytes32(0);
+    }
+
+    struct Tree {
+        mapping(address => Node) nodes;
+        address root;
+    }
+
+    function newLeaf(Tree storage tree, address addr, address reward, uint256 value) internal {
+        Node storage node = tree.nodes[addr];
+        require(addr != address(0), "addr is zero address");
+        require(node.isEmpty(), "leaf is not empty");
+        require(value != 0, "value is zero");
+
+        node.reward = reward;
+        node.value = value;
+        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(addr, reward, value))));
+    }
+
+    function newInternalNode(Tree storage tree, address parent, address left, address right) internal {
+        Node storage parentNode = tree.nodes[parent];
+        Node storage leftNode = tree.nodes[left];
+        Node storage rightNode = tree.nodes[right];
+        require(parent != address(0), "parent is zero address");
+        require(parentNode.isEmpty(), "parent is not empty");
+        require(!leftNode.isEmpty(), "left is empty");
+        require(!rightNode.isEmpty(), "right is empty");
+        require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
+
+        parentNode.left = left;
+        parentNode.right = right;
+        // The value of an internal node represents the sum of the values of the leaves underneath.
+        parentNode.value = leftNode.value + rightNode.value;
+        parentNode.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
+    }
+
+    function setRoot(Tree storage tree, address addr) internal {
+        require(!tree.nodes[addr].isEmpty(), "root is empty");
+        tree.root = addr;
+    }
+
+    // The specification of a well-formed tree is the following:
+    //   - empty nodes are well-formed
+    //   - other nodes should have non-zero value, where the leaf node contains the value of the account and internal
+    // nodes contain the sum of the values of its leaf children.
+    //   - correct hashing of leaves and of internal nodes
+    //   - internal nodes have their children pair sorted and not empty
+    function isWellFormed(Tree storage tree, address addr) internal view returns (bool) {
+        Node storage node = tree.nodes[addr];
+
+        if (node.isEmpty()) return true;
+
+        if (node.value == 0) return false;
+
+        if (node.left == address(0) && node.right == address(0)) {
+            return node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(addr, node.reward, node.value))));
+        } else {
+            // Well-formed nodes have exactly 0 or 2 children.
+            if (node.left == address(0) || node.right == address(0)) return false;
+            Node storage left = tree.nodes[node.left];
+            Node storage right = tree.nodes[node.right];
+            // Well-formed nodes should have its children pair-sorted.
+            bool sorted = left.hashNode <= right.hashNode;
+            return !left.isEmpty() && !right.isEmpty() && sorted
+                && node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode));
+        }
+    }
+
+    function isEmpty(Tree storage tree, address addr) internal view returns (bool) {
+        return tree.nodes[addr].isEmpty();
+    }
+
+    function getRoot(Tree storage tree) internal view returns (address) {
+        return tree.root;
+    }
+
+    function getLeft(Tree storage tree, address addr) internal view returns (address) {
+        return tree.nodes[addr].left;
+    }
+
+    function getRight(Tree storage tree, address addr) internal view returns (address) {
+        return tree.nodes[addr].right;
+    }
+
+    function getValue(Tree storage tree, address addr) internal view returns (uint256) {
+        return tree.nodes[addr].value;
+    }
+
+    function getHash(Tree storage tree, address addr) internal view returns (bytes32) {
+        return tree.nodes[addr].hashNode;
+    }
+}
diff --git a/certora/helpers/MerkleTrees.sol b/certora/helpers/MerkleTrees.sol
new file mode 100644
index 0000000..b412c04
--- /dev/null
+++ b/certora/helpers/MerkleTrees.sol
@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import "./MerkleTreeLib.sol";
+
+contract MerkleTrees {
+    using MerkleTreeLib for MerkleTreeLib.Node;
+    using MerkleTreeLib for MerkleTreeLib.Tree;
+
+    mapping(address => MerkleTreeLib.Tree) trees;
+
+    function newLeaf(address treeAddress, address addr, uint256 value) public {
+        trees[treeAddress].newLeaf(addr, value);
+    }
+
+    function newInternalNode(address treeAddress, address parent, address left, address right) public {
+        trees[treeAddress].newInternalNode(parent, left, right);
+    }
+
+    function setRoot(address treeAddress, address addr) public {
+        trees[treeAddress].setRoot(addr);
+    }
+
+    function getRoot(address treeAddress) public view returns (address) {
+        return trees[treeAddress].getRoot();
+    }
+
+    function getLeft(address treeAddress, address addr) public view returns (address) {
+        return trees[treeAddress].getLeft(addr);
+    }
+
+    function getRight(address treeAddress, address addr) public view returns (address) {
+        return trees[treeAddress].getRight(addr);
+    }
+
+    function getValue(address treeAddress, address addr) public view returns (uint256) {
+        return trees[treeAddress].getValue(addr);
+    }
+
+    function getHash(address treeAddress, address addr) public view returns (bytes32) {
+        return trees[treeAddress].getHash(addr);
+    }
+
+    function isEmpty(address treeAddress, address addr) public view returns (bool) {
+        return trees[treeAddress].nodes[addr].isEmpty();
+    }
+
+    function isWellFormed(address treeAddress, address addr) public view returns (bool) {
+        return trees[treeAddress].isWellFormed(addr);
+    }
+
+    // Only go up to a given depth, to avoid CVL recursion protection.
+    function wellFormedUpTo(address treeAddress, address addr, uint256 depth) public view {
+        if (depth == 0) return;
+
+        require(trees[treeAddress].isWellFormed(addr));
+
+        address left = trees[treeAddress].getLeft(addr);
+        address right = trees[treeAddress].getRight(addr);
+        if (left != address(0)) {
+            wellFormedUpTo(treeAddress, left, depth - 1);
+            wellFormedUpTo(treeAddress, right, depth - 1);
+        }
+    }
+}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
new file mode 100644
index 0000000..645633a
--- /dev/null
+++ b/certora/helpers/Util.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import {IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol";
+
+contract Util {
+    function balanceOf(address reward, address user) external view returns (uint256) {
+        return IERC20(reward).balanceOf(user);
+    }
+}
diff --git a/certora/specs/MerkleTrees.spec b/certora/specs/MerkleTrees.spec
new file mode 100644
index 0000000..a9e3895
--- /dev/null
+++ b/certora/specs/MerkleTrees.spec
@@ -0,0 +1,36 @@
+methods {
+    function newInternalNode(address, address, address, address) external envfree;
+
+    function getRoot(address) external returns address envfree;
+    function getValue(address, address) external returns uint256 envfree;
+    function isEmpty(address, address) external returns bool envfree;
+    function isWellFormed(address, address) external returns bool envfree;
+}
+
+invariant zeroIsEmpty(address tree)
+    isEmpty(tree, 0);
+
+invariant nonEmptyHasValue(address tree, address addr)
+    ! isEmpty(tree, addr) => getValue(tree, addr) != 0
+{ preserved newInternalNode(address _, address parent, address left, address right) {
+    requireInvariant nonEmptyHasValue(tree, left);
+    requireInvariant nonEmptyHasValue(tree, right);
+  }
+}
+
+invariant rootIsZeroOrNotEmpty(address tree)
+    getRoot(tree) == 0 || !isEmpty(tree, getRoot(tree));
+
+invariant wellFormed(address tree, address addr)
+    isWellFormed(tree, addr)
+{ preserved {
+    requireInvariant zeroIsEmpty(tree);
+    requireInvariant wellFormed(tree, addr);
+  }
+  preserved newInternalNode(address _, address parent, address left, address right) {
+    requireInvariant zeroIsEmpty(tree);
+    requireInvariant wellFormed(tree, addr);
+    requireInvariant nonEmptyHasValue(tree, left);
+    requireInvariant nonEmptyHasValue(tree, right);
+  }
+}
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
new file mode 100644
index 0000000..d04224b
--- /dev/null
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -0,0 +1,66 @@
+using MerkleTrees as MerkleTrees;
+using Util as Util;
+
+methods {
+    function root() external returns bytes32 envfree;
+    function claimed(address, address) external returns(uint256) envfree;
+    function claim(address, address, uint256, bytes32[]) external returns(uint256) envfree;
+
+    function MerkleTrees.getValue(address, address) external returns(uint256) envfree;
+    function MerkleTrees.getHash(address, address) external returns(bytes32) envfree;
+    function MerkleTrees.wellFormedUpTo(address, address, uint256) external envfree;
+
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+
+    function Util.balanceOf(address, address) external returns(uint256) envfree;
+}
+
+// Check an account can only claim greater rewards each time.
+rule noClaimAgain(address account, address reward, uint256 claimable, bytes32[] proof) {
+    claim(account, reward, claimable, proof);
+
+    assert claimable == claimed(account, reward);
+
+    uint256 _claimable2;
+    // Assume that the second claim is smaller or equal to the previous claimed amount.
+    require (_claimable2 <= claimable);
+    claim@withrevert(account, reward, _claimable2, proof);
+
+    assert lastReverted;
+}
+
+// Check that the transferred amount is equal to the claimed amount minus the previous claimed amount.
+rule transferredTokens(address account, address reward, uint256 claimable, bytes32[] proof) {
+    // Assume that the rewards distributor itself is not receiving the tokens, to simplify this rule.
+    require account != currentContract;
+
+    uint256 balanceBefore = Util.balanceOf(reward, account);
+    uint256 claimedBefore = claimed(account, reward);
+
+    // Safe require because the sum is capped by the total supply.
+    require balanceBefore + Util.balanceOf(reward, currentContract) < 2^256;
+
+    claim(account, reward, claimable, proof);
+
+    uint256 balanceAfter = Util.balanceOf(reward, account);
+
+    assert balanceAfter - balanceBefore == claimable - claimedBefore;
+}
+
+rule claimCorrectness(address account, address reward, uint256 claimable, bytes32[] proof) {
+    address tree; address node;
+
+    // Assume that root is the hash of node in tree.
+    require MerkleTrees.getHash(tree, node) == root();
+
+    // No need to make sure that node is equal to currRoot : one can pass an internal node instead.
+
+    // Assume that tree is well-formed.
+    MerkleTrees.wellFormedUpTo(tree, node, 3);
+
+    claim(account, reward, claimable, proof);
+
+    assert claimable == MerkleTrees.getValue(tree, account);
+}

From db961565e1936684976e680a09db08494d185ee9 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:06:53 +0100
Subject: [PATCH 02/31] chore: bump node version to 18 in CI

---
 .github/workflows/certora.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 619964b..2a9e7f4 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -26,7 +26,7 @@ jobs:
 
       - uses: actions/setup-node@v3
         with:
-          node-version: 16
+          node-version: 18
           cache: yarn
 
       - name: Install dependencies

From 320af1dbdf6d6799309beaaf4684a355b10c079c Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:09:39 +0100
Subject: [PATCH 03/31] chore: use forge instead of yarn

---
 .github/workflows/certora.yml | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 2a9e7f4..d7482f8 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -24,14 +24,8 @@ jobs:
         with:
           submodules: recursive
 
-      - uses: actions/setup-node@v3
-        with:
-          node-version: 18
-          cache: yarn
-
-      - name: Install dependencies
-        run: yarn install --frozen-lockfile
-        shell: bash
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
 
       - name: Install python
         uses: actions/setup-python@v4
@@ -41,9 +35,9 @@ jobs:
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.13
+          sudo mv solc-static-linux /usr/local/bin/solc
 
       - name: Verify ${{ matrix.conf }}
         run: certoraRun certora/confs/${{ matrix.conf }}.conf

From 46abbb257d303e4e79aceedfe50612c49c83839b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:11:22 +0100
Subject: [PATCH 04/31] fix: use solc path directly

---
 certora/confs/MerkleTrees.conf | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/certora/confs/MerkleTrees.conf b/certora/confs/MerkleTrees.conf
index fcb22ad..f583826 100644
--- a/certora/confs/MerkleTrees.conf
+++ b/certora/confs/MerkleTrees.conf
@@ -2,10 +2,9 @@
     "files": [
         "certora/helpers/MerkleTrees.sol"
     ],
-    "solc": "solc8.19",
     "verify": "MerkleTrees:certora/specs/MerkleTrees.spec",
-    "loop_iter": "2",
     "optimistic_loop": true,
+    "loop_iter": "2",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "Merkle Trees",

From b13f9ca505ffb9c1df342099c34e0d10a3399ce7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:12:06 +0100
Subject: [PATCH 05/31] fix: name of job universal rewards distributor

---
 .github/workflows/certora.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index d7482f8..3843f82 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -17,7 +17,7 @@ jobs:
       matrix:
         conf:
           - MerkleTrees
-          - RewardsDistributor
+          - UniversalRewardsDistributor
 
     steps:
       - uses: actions/checkout@v3

From 5ccbfae3b2365e55193deb2b9d3b28e765e06dbc Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 16:13:53 +0100
Subject: [PATCH 06/31] fix: reward in newLeaf wrapper

---
 certora/helpers/MerkleTrees.sol | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/helpers/MerkleTrees.sol b/certora/helpers/MerkleTrees.sol
index b412c04..dc8271c 100644
--- a/certora/helpers/MerkleTrees.sol
+++ b/certora/helpers/MerkleTrees.sol
@@ -9,8 +9,8 @@ contract MerkleTrees {
 
     mapping(address => MerkleTreeLib.Tree) trees;
 
-    function newLeaf(address treeAddress, address addr, uint256 value) public {
-        trees[treeAddress].newLeaf(addr, value);
+    function newLeaf(address treeAddress, address addr, address reward, uint256 value) public {
+        trees[treeAddress].newLeaf(addr, reward, value);
     }
 
     function newInternalNode(address treeAddress, address parent, address left, address right) public {

From b40f15942f55b6e25c43ead5a5f5b4f93c44c8a5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 2 Feb 2024 17:38:20 +0100
Subject: [PATCH 07/31] refactor: primary key as a hash of account and reward

---
 .github/workflows/certora.yml                 |  2 +-
 .../{MerkleTrees.conf => MerkleTree.conf}     |  6 +-
 .../confs/UniversalRewardsDistributor.conf    |  2 +-
 certora/helpers/MerkleTree.sol                | 65 +++++++++++++++++++
 certora/helpers/MerkleTreeLib.sol             | 64 +++++++++---------
 certora/helpers/MerkleTrees.sol               | 65 -------------------
 certora/specs/MerkleTree.spec                 | 20 ++++++
 certora/specs/MerkleTrees.spec                | 36 ----------
 .../specs/UniversalRewardsDistributor.spec    | 20 +++---
 9 files changed, 133 insertions(+), 147 deletions(-)
 rename certora/confs/{MerkleTrees.conf => MerkleTree.conf} (50%)
 create mode 100644 certora/helpers/MerkleTree.sol
 delete mode 100644 certora/helpers/MerkleTrees.sol
 create mode 100644 certora/specs/MerkleTree.spec
 delete mode 100644 certora/specs/MerkleTrees.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 3843f82..8415d87 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -16,7 +16,7 @@ jobs:
 
       matrix:
         conf:
-          - MerkleTrees
+          - MerkleTree
           - UniversalRewardsDistributor
 
     steps:
diff --git a/certora/confs/MerkleTrees.conf b/certora/confs/MerkleTree.conf
similarity index 50%
rename from certora/confs/MerkleTrees.conf
rename to certora/confs/MerkleTree.conf
index f583826..b8079a7 100644
--- a/certora/confs/MerkleTrees.conf
+++ b/certora/confs/MerkleTree.conf
@@ -1,11 +1,11 @@
 {
     "files": [
-        "certora/helpers/MerkleTrees.sol"
+        "certora/helpers/MerkleTree.sol"
     ],
-    "verify": "MerkleTrees:certora/specs/MerkleTrees.spec",
+    "verify": "MerkleTree:certora/specs/MerkleTree.spec",
     "optimistic_loop": true,
     "loop_iter": "2",
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "Merkle Trees",
+    "msg": "Merkle Tree",
 }
diff --git a/certora/confs/UniversalRewardsDistributor.conf b/certora/confs/UniversalRewardsDistributor.conf
index 5537996..34bfd2d 100644
--- a/certora/confs/UniversalRewardsDistributor.conf
+++ b/certora/confs/UniversalRewardsDistributor.conf
@@ -2,7 +2,7 @@
     "files": [
         "src/UniversalRewardsDistributor.sol",
         "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
-        "certora/helpers/MerkleTrees.sol",
+        "certora/helpers/MerkleTree.sol",
         "certora/helpers/Util.sol",
     ],
     "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
new file mode 100644
index 0000000..2855410
--- /dev/null
+++ b/certora/helpers/MerkleTree.sol
@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import "./MerkleTreeLib.sol";
+
+contract MerkleTree {
+    using MerkleTreeLib for MerkleTreeLib.Node;
+    using MerkleTreeLib for MerkleTreeLib.Tree;
+
+    MerkleTreeLib.Tree tree;
+
+    function newLeaf(address addr, address reward, uint256 value) public {
+        tree.newLeaf(addr, reward, value);
+    }
+
+    function newInternalNode(bytes32 parent, bytes32 left, bytes32 right) public {
+        tree.newInternalNode(parent, left, right);
+    }
+
+    function setRoot(bytes32 id) public {
+        tree.setRoot(id);
+    }
+
+    function getRoot() public view returns (bytes32) {
+        return tree.getRoot();
+    }
+
+    function getLeft(bytes32 id) public view returns (bytes32) {
+        return tree.getLeft(id);
+    }
+
+    function getRight(bytes32 id) public view returns (bytes32) {
+        return tree.getRight(id);
+    }
+
+    function getValue(address addr, address reward) public view returns (uint256) {
+        return tree.getValue(addr, reward);
+    }
+
+    function getHash(bytes32 id) public view returns (bytes32) {
+        return tree.getHash(id);
+    }
+
+    function isEmpty(bytes32 id) public view returns (bool) {
+        return tree.nodes[id].isEmpty();
+    }
+
+    function isWellFormed(bytes32 id) public view returns (bool) {
+        return tree.isWellFormed(id);
+    }
+
+    // Only go up to a given depth, to avoid CVL recursion protection.
+    function wellFormedUpTo(bytes32 id, uint256 depth) public view {
+        if (depth == 0) return;
+
+        require(tree.isWellFormed(id));
+
+        bytes32 left = tree.getLeft(id);
+        bytes32 right = tree.getRight(id);
+        if (left != 0) {
+            wellFormedUpTo(left, depth - 1);
+            wellFormedUpTo(right, depth - 1);
+        }
+    }
+}
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index f14e954..4cdcce7 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -5,39 +5,42 @@ library MerkleTreeLib {
     using MerkleTreeLib for Node;
 
     struct Node {
-        address left;
-        address right;
+        bytes32 left;
+        bytes32 right;
+        address addr;
         address reward;
         uint256 value;
         bytes32 hashNode;
     }
 
     function isEmpty(Node memory node) internal pure returns (bool) {
-        return node.left == address(0) && node.right == address(0) && node.reward == address(0) && node.value == 0
-            && node.hashNode == bytes32(0);
+        return node.left == 0 && node.right == 0 && node.addr == address(0) && node.reward == address(0)
+            && node.value == 0 && node.hashNode == 0;
     }
 
     struct Tree {
-        mapping(address => Node) nodes;
-        address root;
+        mapping(bytes32 => Node) nodes;
+        bytes32 root;
     }
 
     function newLeaf(Tree storage tree, address addr, address reward, uint256 value) internal {
-        Node storage node = tree.nodes[addr];
-        require(addr != address(0), "addr is zero address");
+        bytes32 id = keccak256(abi.encode(addr, reward));
+        Node storage node = tree.nodes[id];
+        require(id != 0, "id is the zero bytes");
         require(node.isEmpty(), "leaf is not empty");
         require(value != 0, "value is zero");
 
+        node.addr = addr;
         node.reward = reward;
         node.value = value;
         node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(addr, reward, value))));
     }
 
-    function newInternalNode(Tree storage tree, address parent, address left, address right) internal {
+    function newInternalNode(Tree storage tree, bytes32 parent, bytes32 left, bytes32 right) internal {
         Node storage parentNode = tree.nodes[parent];
         Node storage leftNode = tree.nodes[left];
         Node storage rightNode = tree.nodes[right];
-        require(parent != address(0), "parent is zero address");
+        require(parent != 0, "parent is zero bytes");
         require(parentNode.isEmpty(), "parent is not empty");
         require(!leftNode.isEmpty(), "left is empty");
         require(!rightNode.isEmpty(), "right is empty");
@@ -50,9 +53,9 @@ library MerkleTreeLib {
         parentNode.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 
-    function setRoot(Tree storage tree, address addr) internal {
-        require(!tree.nodes[addr].isEmpty(), "root is empty");
-        tree.root = addr;
+    function setRoot(Tree storage tree, bytes32 id) internal {
+        require(!tree.nodes[id].isEmpty(), "root is empty");
+        tree.root = id;
     }
 
     // The specification of a well-formed tree is the following:
@@ -61,18 +64,16 @@ library MerkleTreeLib {
     // nodes contain the sum of the values of its leaf children.
     //   - correct hashing of leaves and of internal nodes
     //   - internal nodes have their children pair sorted and not empty
-    function isWellFormed(Tree storage tree, address addr) internal view returns (bool) {
-        Node storage node = tree.nodes[addr];
+    function isWellFormed(Tree storage tree, bytes32 id) internal view returns (bool) {
+        Node storage node = tree.nodes[id];
 
         if (node.isEmpty()) return true;
 
-        if (node.value == 0) return false;
-
-        if (node.left == address(0) && node.right == address(0)) {
-            return node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(addr, node.reward, node.value))));
+        if (node.left == 0 && node.right == 0) {
+            return node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
         } else {
             // Well-formed nodes have exactly 0 or 2 children.
-            if (node.left == address(0) || node.right == address(0)) return false;
+            if (node.left == 0 || node.right == 0) return false;
             Node storage left = tree.nodes[node.left];
             Node storage right = tree.nodes[node.right];
             // Well-formed nodes should have its children pair-sorted.
@@ -82,27 +83,28 @@ library MerkleTreeLib {
         }
     }
 
-    function isEmpty(Tree storage tree, address addr) internal view returns (bool) {
-        return tree.nodes[addr].isEmpty();
+    function isEmpty(Tree storage tree, bytes32 id) internal view returns (bool) {
+        return tree.nodes[id].isEmpty();
     }
 
-    function getRoot(Tree storage tree) internal view returns (address) {
+    function getRoot(Tree storage tree) internal view returns (bytes32) {
         return tree.root;
     }
 
-    function getLeft(Tree storage tree, address addr) internal view returns (address) {
-        return tree.nodes[addr].left;
+    function getLeft(Tree storage tree, bytes32 id) internal view returns (bytes32) {
+        return tree.nodes[id].left;
     }
 
-    function getRight(Tree storage tree, address addr) internal view returns (address) {
-        return tree.nodes[addr].right;
+    function getRight(Tree storage tree, bytes32 id) internal view returns (bytes32) {
+        return tree.nodes[id].right;
     }
 
-    function getValue(Tree storage tree, address addr) internal view returns (uint256) {
-        return tree.nodes[addr].value;
+    function getValue(Tree storage tree, address addr, address reward) internal view returns (uint256) {
+        bytes32 id = keccak256(abi.encode(addr, reward));
+        return tree.nodes[id].value;
     }
 
-    function getHash(Tree storage tree, address addr) internal view returns (bytes32) {
-        return tree.nodes[addr].hashNode;
+    function getHash(Tree storage tree, bytes32 id) internal view returns (bytes32) {
+        return tree.nodes[id].hashNode;
     }
 }
diff --git a/certora/helpers/MerkleTrees.sol b/certora/helpers/MerkleTrees.sol
deleted file mode 100644
index dc8271c..0000000
--- a/certora/helpers/MerkleTrees.sol
+++ /dev/null
@@ -1,65 +0,0 @@
-// SPDX-License-Identifier: GNU AGPLv3
-pragma solidity ^0.8.0;
-
-import "./MerkleTreeLib.sol";
-
-contract MerkleTrees {
-    using MerkleTreeLib for MerkleTreeLib.Node;
-    using MerkleTreeLib for MerkleTreeLib.Tree;
-
-    mapping(address => MerkleTreeLib.Tree) trees;
-
-    function newLeaf(address treeAddress, address addr, address reward, uint256 value) public {
-        trees[treeAddress].newLeaf(addr, reward, value);
-    }
-
-    function newInternalNode(address treeAddress, address parent, address left, address right) public {
-        trees[treeAddress].newInternalNode(parent, left, right);
-    }
-
-    function setRoot(address treeAddress, address addr) public {
-        trees[treeAddress].setRoot(addr);
-    }
-
-    function getRoot(address treeAddress) public view returns (address) {
-        return trees[treeAddress].getRoot();
-    }
-
-    function getLeft(address treeAddress, address addr) public view returns (address) {
-        return trees[treeAddress].getLeft(addr);
-    }
-
-    function getRight(address treeAddress, address addr) public view returns (address) {
-        return trees[treeAddress].getRight(addr);
-    }
-
-    function getValue(address treeAddress, address addr) public view returns (uint256) {
-        return trees[treeAddress].getValue(addr);
-    }
-
-    function getHash(address treeAddress, address addr) public view returns (bytes32) {
-        return trees[treeAddress].getHash(addr);
-    }
-
-    function isEmpty(address treeAddress, address addr) public view returns (bool) {
-        return trees[treeAddress].nodes[addr].isEmpty();
-    }
-
-    function isWellFormed(address treeAddress, address addr) public view returns (bool) {
-        return trees[treeAddress].isWellFormed(addr);
-    }
-
-    // Only go up to a given depth, to avoid CVL recursion protection.
-    function wellFormedUpTo(address treeAddress, address addr, uint256 depth) public view {
-        if (depth == 0) return;
-
-        require(trees[treeAddress].isWellFormed(addr));
-
-        address left = trees[treeAddress].getLeft(addr);
-        address right = trees[treeAddress].getRight(addr);
-        if (left != address(0)) {
-            wellFormedUpTo(treeAddress, left, depth - 1);
-            wellFormedUpTo(treeAddress, right, depth - 1);
-        }
-    }
-}
diff --git a/certora/specs/MerkleTree.spec b/certora/specs/MerkleTree.spec
new file mode 100644
index 0000000..d762b8f
--- /dev/null
+++ b/certora/specs/MerkleTree.spec
@@ -0,0 +1,20 @@
+methods {
+    function getRoot() external returns(bytes32) envfree;
+    function getValue(address, address) external returns(uint256) envfree;
+    function isEmpty(bytes32) external returns(bool) envfree;
+    function isWellFormed(bytes32) external returns(bool) envfree;
+}
+
+invariant zeroIsEmpty()
+    isEmpty(to_bytes32(0));
+
+invariant rootIsZeroOrNotEmpty()
+    getRoot() == to_bytes32(0) || !isEmpty(getRoot());
+
+invariant wellFormed(bytes32 id)
+    isWellFormed(id)
+{ preserved {
+    requireInvariant zeroIsEmpty();
+    requireInvariant wellFormed(id);
+  }
+}
diff --git a/certora/specs/MerkleTrees.spec b/certora/specs/MerkleTrees.spec
deleted file mode 100644
index a9e3895..0000000
--- a/certora/specs/MerkleTrees.spec
+++ /dev/null
@@ -1,36 +0,0 @@
-methods {
-    function newInternalNode(address, address, address, address) external envfree;
-
-    function getRoot(address) external returns address envfree;
-    function getValue(address, address) external returns uint256 envfree;
-    function isEmpty(address, address) external returns bool envfree;
-    function isWellFormed(address, address) external returns bool envfree;
-}
-
-invariant zeroIsEmpty(address tree)
-    isEmpty(tree, 0);
-
-invariant nonEmptyHasValue(address tree, address addr)
-    ! isEmpty(tree, addr) => getValue(tree, addr) != 0
-{ preserved newInternalNode(address _, address parent, address left, address right) {
-    requireInvariant nonEmptyHasValue(tree, left);
-    requireInvariant nonEmptyHasValue(tree, right);
-  }
-}
-
-invariant rootIsZeroOrNotEmpty(address tree)
-    getRoot(tree) == 0 || !isEmpty(tree, getRoot(tree));
-
-invariant wellFormed(address tree, address addr)
-    isWellFormed(tree, addr)
-{ preserved {
-    requireInvariant zeroIsEmpty(tree);
-    requireInvariant wellFormed(tree, addr);
-  }
-  preserved newInternalNode(address _, address parent, address left, address right) {
-    requireInvariant zeroIsEmpty(tree);
-    requireInvariant wellFormed(tree, addr);
-    requireInvariant nonEmptyHasValue(tree, left);
-    requireInvariant nonEmptyHasValue(tree, right);
-  }
-}
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index d04224b..64f3ff2 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -1,4 +1,4 @@
-using MerkleTrees as MerkleTrees;
+using MerkleTree as MerkleTree;
 using Util as Util;
 
 methods {
@@ -6,9 +6,9 @@ methods {
     function claimed(address, address) external returns(uint256) envfree;
     function claim(address, address, uint256, bytes32[]) external returns(uint256) envfree;
 
-    function MerkleTrees.getValue(address, address) external returns(uint256) envfree;
-    function MerkleTrees.getHash(address, address) external returns(bytes32) envfree;
-    function MerkleTrees.wellFormedUpTo(address, address, uint256) external envfree;
+    function MerkleTree.getValue(address, address) external returns(uint256) envfree;
+    function MerkleTree.getHash(bytes32) external returns(bytes32) envfree;
+    function MerkleTree.wellFormedUpTo(bytes32, uint256) external envfree;
 
     function _.balanceOf(address) external => DISPATCHER(true);
     function _.transfer(address, uint256) external => DISPATCHER(true);
@@ -50,17 +50,17 @@ rule transferredTokens(address account, address reward, uint256 claimable, bytes
 }
 
 rule claimCorrectness(address account, address reward, uint256 claimable, bytes32[] proof) {
-    address tree; address node;
+    bytes32 node;
 
-    // Assume that root is the hash of node in tree.
-    require MerkleTrees.getHash(tree, node) == root();
+    // Assume that root is the hash of node in the tree.
+    require MerkleTree.getHash(node) == root();
 
     // No need to make sure that node is equal to currRoot : one can pass an internal node instead.
 
-    // Assume that tree is well-formed.
-    MerkleTrees.wellFormedUpTo(tree, node, 3);
+    // Assume that the tree is well-formed.
+    MerkleTree.wellFormedUpTo(node, 3);
 
     claim(account, reward, claimable, proof);
 
-    assert claimable == MerkleTrees.getValue(tree, account);
+    assert claimable == MerkleTree.getValue(account, reward);
 }

From 91f519d4501ced4a05c01f0d501c3bb6385aad0a Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 13 Feb 2024 14:18:15 +0100
Subject: [PATCH 08/31] fix: well-formed leaves

---
 certora/helpers/MerkleTreeLib.sol | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index 4cdcce7..6dabbe7 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -70,7 +70,9 @@ library MerkleTreeLib {
         if (node.isEmpty()) return true;
 
         if (node.left == 0 && node.right == 0) {
-            return node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
+            bytes32 accountHash = keccak256(abi.encode(node.addr, node.reward));
+            return id == accountHash
+                && node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
         } else {
             // Well-formed nodes have exactly 0 or 2 children.
             if (node.left == 0 || node.right == 0) return false;

From a9e0ee16315d6930b8075aa8da9eb3da02c169a7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 13 Feb 2024 14:35:35 +0100
Subject: [PATCH 09/31] docs: broken link in README

---
 certora/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/README.md b/certora/README.md
index 396019f..af6bfbe 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -19,7 +19,7 @@ The certificate is assumed to contain the submitted root to verify, a total amou
 
 Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants:
 
-- it is checked in [MerkleTrees.spec](specs/MerkleTrees.spec) that those functions lead to creating well-formed trees.
+- it is checked in [MerkleTree.spec](specs/MerkleTree.spec) that those functions lead to creating well-formed trees.
   Well-formed trees also verify that the value of their internal node is the sum of the rewards it contains.
 - it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.
 

From 22b7fb53d4e761792f4f71b73753b0eb7044f23a Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Wed, 14 Feb 2024 17:07:30 +0100
Subject: [PATCH 10/31] refactor: remove sum of children value

---
 certora/helpers/MerkleTreeLib.sol | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index 6dabbe7..70aaaa5 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -48,8 +48,6 @@ library MerkleTreeLib {
 
         parentNode.left = left;
         parentNode.right = right;
-        // The value of an internal node represents the sum of the values of the leaves underneath.
-        parentNode.value = leftNode.value + rightNode.value;
         parentNode.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 
@@ -60,8 +58,7 @@ library MerkleTreeLib {
 
     // The specification of a well-formed tree is the following:
     //   - empty nodes are well-formed
-    //   - other nodes should have non-zero value, where the leaf node contains the value of the account and internal
-    // nodes contain the sum of the values of its leaf children.
+    //   - correct identifiers of leaves
     //   - correct hashing of leaves and of internal nodes
     //   - internal nodes have their children pair sorted and not empty
     function isWellFormed(Tree storage tree, bytes32 id) internal view returns (bool) {
@@ -70,8 +67,8 @@ library MerkleTreeLib {
         if (node.isEmpty()) return true;
 
         if (node.left == 0 && node.right == 0) {
-            bytes32 accountHash = keccak256(abi.encode(node.addr, node.reward));
-            return id == accountHash
+            bytes32 idLeaf = keccak256(abi.encode(node.addr, node.reward));
+            return id == idLeaf
                 && node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
         } else {
             // Well-formed nodes have exactly 0 or 2 children.

From f918daa4ec42d11195879b7759673162057d03d8 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 15 Feb 2024 09:56:12 +0100
Subject: [PATCH 11/31] feat: refactor certificate to new json format

---
 certora/checker/Checker.sol           | 21 ++++++-----
 certora/checker/create_certificate.py | 51 ++++++++++++++++++---------
 foundry.toml                          |  5 +++
 3 files changed, 50 insertions(+), 27 deletions(-)

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index e3b7bc0..7859480 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -13,14 +13,16 @@ contract Checker is Test {
     MerkleTreeLib.Tree public tree;
 
     struct Leaf {
-        address addr;
+        bytes32 id;
+        bytes32 addr;
+        bytes32 reward;
         uint256 value;
     }
 
     struct InternalNode {
-        address addr;
-        address left;
-        address right;
+        bytes32 id;
+        bytes32 left;
+        bytes32 right;
     }
 
     function testVerifyCertificate() public {
@@ -32,22 +34,19 @@ contract Checker is Test {
         Leaf memory leaf;
         for (uint256 i; i < leafLength; i++) {
             leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
-            tree.newLeaf(leaf.addr, leaf.value);
+            tree.newLeaf(address(bytes20(leaf.addr)), address(bytes20(leaf.reward)), leaf.value);
         }
 
         uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
         InternalNode memory node;
         for (uint256 i; i < nodeLength; i++) {
             node = abi.decode(json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (InternalNode));
-            tree.newInternalNode(node.addr, node.left, node.right);
+            tree.newInternalNode(node.id, node.left, node.right);
         }
 
-        assertTrue(!tree.isEmpty(node.addr), "empty root");
-
-        uint256 total = abi.decode(json.parseRaw(".total"), (uint256));
-        assertEq(tree.getValue(node.addr), total, "incorrect total rewards");
+        assertTrue(!tree.isEmpty(node.id), "empty root");
 
         bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
-        assertEq(tree.getHash(node.addr), root, "mismatched roots");
+        assertEq(tree.getHash(node.id), root, "mismatched roots");
     }
 }
diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
index 67387fd..9d8edaa 100644
--- a/certora/checker/create_certificate.py
+++ b/certora/checker/create_certificate.py
@@ -1,32 +1,44 @@
 import sys
 import json
+from eth_abi import encode
 from web3 import Web3, EthereumTesterProvider
 
 w3 = Web3(EthereumTesterProvider())
 
 
-def keccak_node(left_hash, right_hash):
+def hash_node(left_hash, right_hash):
     return w3.to_hex(
         w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
     )
 
 
-def keccak_leaf(address, amount):
+def hash_leaf(address, reward, amount):
     address = w3.to_checksum_address(address)
-    return w3.to_hex(w3.solidity_keccak(["address", "uint256"], [address, amount]))
+    reward = w3.to_checksum_address(reward)
+    encoded_args = encode(["address", "address", "uint256"], [address, reward, amount])
+    first_hash = w3.solidity_keccak(
+        ["bytes"],
+        [encoded_args],
+    )
+    second_hash = w3.solidity_keccak(
+        ["bytes"],
+        [first_hash],
+    )
+    return w3.to_hex(second_hash)
 
 
 certificate = {}
 hash_to_address = {}
+hash_to_reward = {}
 hash_to_value = {}
 left = {}
 right = {}
 
 
-def populate(address, amount, proof):
-    amount = int(amount)
-    computedHash = keccak_leaf(address, amount)
-    hash_to_address[computedHash] = address
+def populate(addr, reward, amount, proof):
+    computedHash = hash_leaf(addr, reward, amount)
+    hash_to_address[computedHash] = addr.lower()
+    hash_to_reward[computedHash] = reward.lower()
     hash_to_value[computedHash] = amount
     for proofElement in proof:
         [leftHash, rightHash] = (
@@ -34,10 +46,9 @@ def populate(address, amount, proof):
             if computedHash <= proofElement
             else [proofElement, computedHash]
         )
-        computedHash = keccak_node(leftHash, rightHash)
+        computedHash = hash_node(leftHash, rightHash)
         left[computedHash] = leftHash
         right[computedHash] = rightHash
-        hash_to_address[computedHash] = keccak_node(computedHash, computedHash)[:42]
 
 
 def walk(h):
@@ -46,26 +57,34 @@ def walk(h):
         walk(right[h])
         certificate["node"].append(
             {
-                "addr": hash_to_address[h],
-                "left": hash_to_address[left[h]],
-                "right": hash_to_address[right[h]],
+                "id": h,
+                "left": left[h],
+                "right": right[h],
             }
         )
     else:
         certificate["leaf"].append(
-            {"addr": hash_to_address[h], "value": hash_to_value[h]}
+            {
+                "id": h,
+                "addr": hash_to_address[h],
+                "reward": hash_to_reward[h],
+                "value": hash_to_value[h],
+            }
         )
 
 
 with open(sys.argv[1]) as input_file:
     proofs = json.load(input_file)
+    rewards = proofs["rewards"]
+
     certificate["root"] = proofs["root"]
-    certificate["total"] = int(proofs["total"])
     certificate["leaf"] = []
     certificate["node"] = []
 
-    for address, data in proofs["proofs"].items():
-        populate(address, data["amount"], data["proof"])
+    for addr, rest in rewards.items():
+        for reward, data in rest.items():
+            amount = int(data["amount"])
+            populate(addr, reward, amount, data["proof"])
 
     walk(proofs["root"])
 
diff --git a/foundry.toml b/foundry.toml
index 60c9b35..58ce97c 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -50,3 +50,8 @@ max_test_rejects = 65536
 [profile.test-fast.invariant]
 runs = 16
 depth = 256
+
+[profile.checker]
+test = 'certora/checker'
+fs_permissions = [{access = "read", path= "./"}]
+match_contract = 'Checker'

From b6a5eb0a0d0bc2040b5800b745f5d5416ff6e0c6 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 15 Feb 2024 10:47:07 +0100
Subject: [PATCH 12/31] fix: workaround parsing issue

---
 certora/checker/Checker.sol           | 7 +++----
 certora/checker/create_certificate.py | 1 -
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index 7859480..2d21fb1 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -13,9 +13,8 @@ contract Checker is Test {
     MerkleTreeLib.Tree public tree;
 
     struct Leaf {
-        bytes32 id;
-        bytes32 addr;
-        bytes32 reward;
+        address addr;
+        address reward;
         uint256 value;
     }
 
@@ -34,7 +33,7 @@ contract Checker is Test {
         Leaf memory leaf;
         for (uint256 i; i < leafLength; i++) {
             leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
-            tree.newLeaf(address(bytes20(leaf.addr)), address(bytes20(leaf.reward)), leaf.value);
+            tree.newLeaf(leaf.addr, leaf.reward, leaf.value);
         }
 
         uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
index 9d8edaa..3bf8e3f 100644
--- a/certora/checker/create_certificate.py
+++ b/certora/checker/create_certificate.py
@@ -65,7 +65,6 @@ def walk(h):
     else:
         certificate["leaf"].append(
             {
-                "id": h,
                 "addr": hash_to_address[h],
                 "reward": hash_to_reward[h],
                 "value": hash_to_value[h],

From 07322bcd154c19dbe185a1cd0af495bf18da5d28 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 15 Feb 2024 11:16:46 +0100
Subject: [PATCH 13/31] fix: disambiguate hash and id

---
 certora/checker/create_certificate.py | 24 ++++++++++++++++--------
 certora/helpers/MerkleTreeLib.sol     | 14 +++++++-------
 2 files changed, 23 insertions(+), 15 deletions(-)

diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
index 3bf8e3f..5c07565 100644
--- a/certora/checker/create_certificate.py
+++ b/certora/checker/create_certificate.py
@@ -13,8 +13,6 @@ def hash_node(left_hash, right_hash):
 
 
 def hash_leaf(address, reward, amount):
-    address = w3.to_checksum_address(address)
-    reward = w3.to_checksum_address(reward)
     encoded_args = encode(["address", "address", "uint256"], [address, reward, amount])
     first_hash = w3.solidity_keccak(
         ["bytes"],
@@ -27,7 +25,13 @@ def hash_leaf(address, reward, amount):
     return w3.to_hex(second_hash)
 
 
+def hash_id(addr, reward):
+    encoded_args = encode(["address", "address"], [addr, reward])
+    return w3.to_hex(w3.solidity_keccak(["bytes"], [encoded_args]))
+
+
 certificate = {}
+hash_to_id = {}
 hash_to_address = {}
 hash_to_reward = {}
 hash_to_value = {}
@@ -37,8 +41,9 @@ def hash_leaf(address, reward, amount):
 
 def populate(addr, reward, amount, proof):
     computedHash = hash_leaf(addr, reward, amount)
-    hash_to_address[computedHash] = addr.lower()
-    hash_to_reward[computedHash] = reward.lower()
+    hash_to_id[computedHash] = hash_id(addr, reward)
+    hash_to_address[computedHash] = addr
+    hash_to_reward[computedHash] = reward
     hash_to_value[computedHash] = amount
     for proofElement in proof:
         [leftHash, rightHash] = (
@@ -47,6 +52,7 @@ def populate(addr, reward, amount, proof):
             else [proofElement, computedHash]
         )
         computedHash = hash_node(leftHash, rightHash)
+        hash_to_id[computedHash] = computedHash
         left[computedHash] = leftHash
         right[computedHash] = rightHash
 
@@ -58,8 +64,8 @@ def walk(h):
         certificate["node"].append(
             {
                 "id": h,
-                "left": left[h],
-                "right": right[h],
+                "left": hash_to_id[left[h]],
+                "right": hash_to_id[right[h]],
             }
         )
     else:
@@ -80,8 +86,10 @@ def walk(h):
     certificate["leaf"] = []
     certificate["node"] = []
 
-    for addr, rest in rewards.items():
-        for reward, data in rest.items():
+    for addr, data in rewards.items():
+        address = w3.to_checksum_address(addr)
+        for reward, data in data.items():
+            reward = w3.to_checksum_address(reward)
             amount = int(data["amount"])
             populate(addr, reward, amount, data["proof"])
 
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index 70aaaa5..c204f45 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -36,19 +36,19 @@ library MerkleTreeLib {
         node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(addr, reward, value))));
     }
 
-    function newInternalNode(Tree storage tree, bytes32 parent, bytes32 left, bytes32 right) internal {
-        Node storage parentNode = tree.nodes[parent];
+    function newInternalNode(Tree storage tree, bytes32 id, bytes32 left, bytes32 right) internal {
+        Node storage node = tree.nodes[id];
         Node storage leftNode = tree.nodes[left];
         Node storage rightNode = tree.nodes[right];
-        require(parent != 0, "parent is zero bytes");
-        require(parentNode.isEmpty(), "parent is not empty");
+        require(id != 0, "id is zero bytes");
+        require(node.isEmpty(), "node is not empty");
         require(!leftNode.isEmpty(), "left is empty");
         require(!rightNode.isEmpty(), "right is empty");
         require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
 
-        parentNode.left = left;
-        parentNode.right = right;
-        parentNode.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
+        node.left = left;
+        node.right = right;
+        node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 
     function setRoot(Tree storage tree, bytes32 id) internal {

From dd229009c061750b5a3a1be046bd1a1e611ca64f Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 19 Feb 2024 18:10:41 +0100
Subject: [PATCH 14/31] feat: add Dockerfile for proof verification

---
 Dockerfile | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 Dockerfile

diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..f94749f
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,14 @@
+FROM ubuntu:latest
+WORKDIR /usr/rewards-checker
+
+RUN apt update
+RUN apt install python3-pip git curl -y
+RUN pip install web3 eth-tester py-evm
+
+RUN curl -L https://foundry.paradigm.xyz | bash
+ENV PATH="${PATH}:/root/.foundry/bin/"
+RUN foundryup
+
+COPY . .
+RUN python3 certora/checker/create_certificate.py proofs.json
+RUN FOUNDRY_PROFILE=checker forge test

From 43b781229e5df76bf1cf17b89d49a4c5243bc1fa Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Wed, 6 Mar 2024 15:08:08 +0100
Subject: [PATCH 15/31] chore: import upgrades to the verification

---
 certora/confs/MerkleTree.conf                 |  2 +-
 .../confs/UniversalRewardsDistributor.conf    |  2 +-
 certora/helpers/MerkleTree.sol                | 20 ++++++-----
 .../specs/UniversalRewardsDistributor.spec    | 36 ++++++++++++++-----
 4 files changed, 40 insertions(+), 20 deletions(-)

diff --git a/certora/confs/MerkleTree.conf b/certora/confs/MerkleTree.conf
index b8079a7..4287ba6 100644
--- a/certora/confs/MerkleTree.conf
+++ b/certora/confs/MerkleTree.conf
@@ -4,7 +4,7 @@
     ],
     "verify": "MerkleTree:certora/specs/MerkleTree.spec",
     "optimistic_loop": true,
-    "loop_iter": "2",
+    "loop_iter": "4",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "Merkle Tree",
diff --git a/certora/confs/UniversalRewardsDistributor.conf b/certora/confs/UniversalRewardsDistributor.conf
index 34bfd2d..4689525 100644
--- a/certora/confs/UniversalRewardsDistributor.conf
+++ b/certora/confs/UniversalRewardsDistributor.conf
@@ -7,7 +7,7 @@
     ],
     "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
     "optimistic_loop": true,
-    "loop_iter": "2",
+    "loop_iter": "4",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "Universal Rewards Distributor",
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 2855410..3a074c5 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -49,17 +49,19 @@ contract MerkleTree {
         return tree.isWellFormed(id);
     }
 
-    // Only go up to a given depth, to avoid CVL recursion protection.
-    function wellFormedUpTo(bytes32 id, uint256 depth) public view {
-        if (depth == 0) return;
+    // Check that the nodes are well formed on the path from the root.
+    function wellFormedPath(bytes32 id, bytes32[] memory proof) public view {
+        for (uint256 i = proof.length;;) {
+            require(tree.isWellFormed(id));
 
-        require(tree.isWellFormed(id));
+            if (i == 0) break;
 
-        bytes32 left = tree.getLeft(id);
-        bytes32 right = tree.getRight(id);
-        if (left != 0) {
-            wellFormedUpTo(left, depth - 1);
-            wellFormedUpTo(right, depth - 1);
+            bytes32 otherHash = proof[--i];
+
+            bytes32 left = tree.getLeft(id);
+            bytes32 right = tree.getRight(id);
+
+            id = tree.getHash(left) == otherHash ? right : left;
         }
     }
 }
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index 64f3ff2..da6b43c 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -8,7 +8,7 @@ methods {
 
     function MerkleTree.getValue(address, address) external returns(uint256) envfree;
     function MerkleTree.getHash(bytes32) external returns(bytes32) envfree;
-    function MerkleTree.wellFormedUpTo(bytes32, uint256) external envfree;
+    function MerkleTree.wellFormedPath(bytes32, bytes32[]) external envfree;
 
     function _.balanceOf(address) external => DISPATCHER(true);
     function _.transfer(address, uint256) external => DISPATCHER(true);
@@ -17,18 +17,36 @@ methods {
     function Util.balanceOf(address, address) external returns(uint256) envfree;
 }
 
-// Check an account can only claim greater rewards each time.
-rule noClaimAgain(address account, address reward, uint256 claimable, bytes32[] proof) {
+// 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);
+
+    assert claimable > claimed;
+}
+
+// Check that claiming twice is equivalent to claiming once with the last amount.
+rule claimTwice(address account, address reward, uint256 claim1, uint256 claim2) {
+    storage initStorage = lastStorage;
+
+    bytes32[] proof1; bytes32[] proof2;
+    claim(account, reward, claim1, proof1);
+    claim(account, reward, claim2, proof2);
+
+    storage afterBothStorage = lastStorage;
 
-    uint256 _claimable2;
-    // Assume that the second claim is smaller or equal to the previous claimed amount.
-    require (_claimable2 <= claimable);
-    claim@withrevert(account, reward, _claimable2, proof);
+    bytes32[] proof;
+    claim(account, reward, claim2, proof) at initStorage;
 
-    assert lastReverted;
+    assert lastStorage == afterBothStorage;
 }
 
 // Check that the transferred amount is equal to the claimed amount minus the previous claimed amount.
@@ -58,7 +76,7 @@ rule claimCorrectness(address account, address reward, uint256 claimable, bytes3
     // No need to make sure that node is equal to currRoot : one can pass an internal node instead.
 
     // Assume that the tree is well-formed.
-    MerkleTree.wellFormedUpTo(node, 3);
+    MerkleTree.wellFormedPath(node, proof);
 
     claim(account, reward, claimable, proof);
 

From 2de7d4dc90cbb45986a61a06280d30d12633468c Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 11:14:32 +0100
Subject: [PATCH 16/31] refactor: remove unnecessary require invariant

---
 certora/specs/MerkleTree.spec | 1 -
 1 file changed, 1 deletion(-)

diff --git a/certora/specs/MerkleTree.spec b/certora/specs/MerkleTree.spec
index d762b8f..31942b2 100644
--- a/certora/specs/MerkleTree.spec
+++ b/certora/specs/MerkleTree.spec
@@ -15,6 +15,5 @@ invariant wellFormed(bytes32 id)
     isWellFormed(id)
 { preserved {
     requireInvariant zeroIsEmpty();
-    requireInvariant wellFormed(id);
   }
 }

From c242902275f41e0384c0991957cec9f2a1df9a02 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 11:50:36 +0100
Subject: [PATCH 17/31] docs: add comments

---
 certora/checker/Checker.sol                    | 2 +-
 certora/checker/create_certificate.py          | 5 +++++
 certora/helpers/MerkleTree.sol                 | 2 +-
 certora/helpers/MerkleTreeLib.sol              | 4 +++-
 certora/helpers/Util.sol                       | 2 +-
 certora/specs/MerkleTree.spec                  | 2 ++
 certora/specs/UniversalRewardsDistributor.spec | 2 ++
 7 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index 2d21fb1..0313caa 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GNU AGPLv3
+// SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.0;
 
 import "../../lib/openzeppelin-contracts/contracts/utils/Strings.sol";
diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
index 5c07565..e31b1d1 100644
--- a/certora/checker/create_certificate.py
+++ b/certora/checker/create_certificate.py
@@ -6,12 +6,14 @@
 w3 = Web3(EthereumTesterProvider())
 
 
+# Returns the hash of a node given the hashes of its children.
 def hash_node(left_hash, right_hash):
     return w3.to_hex(
         w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
     )
 
 
+# Returns the hash of a leaf given the rewards details.
 def hash_leaf(address, reward, amount):
     encoded_args = encode(["address", "address", "uint256"], [address, reward, amount])
     first_hash = w3.solidity_keccak(
@@ -25,6 +27,7 @@ def hash_leaf(address, reward, amount):
     return w3.to_hex(second_hash)
 
 
+# Returns the identifier of a leaf.
 def hash_id(addr, reward):
     encoded_args = encode(["address", "address"], [addr, reward])
     return w3.to_hex(w3.solidity_keccak(["bytes"], [encoded_args]))
@@ -39,6 +42,7 @@ def hash_id(addr, reward):
 right = {}
 
 
+# Populates the fields of the tree along the path given by the proof.
 def populate(addr, reward, amount, proof):
     computedHash = hash_leaf(addr, reward, amount)
     hash_to_id[computedHash] = hash_id(addr, reward)
@@ -57,6 +61,7 @@ def populate(addr, reward, amount, proof):
         right[computedHash] = rightHash
 
 
+# Traverse the tree and generate corresponding instruction for each internal node and each leaf.
 def walk(h):
     if h in left:
         walk(left[h])
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 3a074c5..9625bfb 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GNU AGPLv3
+// SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.0;
 
 import "./MerkleTreeLib.sol";
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index c204f45..2108644 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GNU AGPLv3
+// SPDX-License-Identifier: AGPL-3.0-only
 pragma solidity ^0.8.0;
 
 library MerkleTreeLib {
@@ -24,6 +24,8 @@ library MerkleTreeLib {
     }
 
     function newLeaf(Tree storage tree, address addr, address reward, uint256 value) internal {
+        // The following identifier is used as the key to create a new leaf.
+        // This ensures that the same pair of address and reward does not appear twice in the tree.
         bytes32 id = keccak256(abi.encode(addr, reward));
         Node storage node = tree.nodes[id];
         require(id != 0, "id is the zero bytes");
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
index 645633a..386a681 100644
--- a/certora/helpers/Util.sol
+++ b/certora/helpers/Util.sol
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GNU AGPLv3
+// SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.0;
 
 import {IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol";
diff --git a/certora/specs/MerkleTree.spec b/certora/specs/MerkleTree.spec
index 31942b2..85e4d39 100644
--- a/certora/specs/MerkleTree.spec
+++ b/certora/specs/MerkleTree.spec
@@ -1,3 +1,5 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
 methods {
     function getRoot() external returns(bytes32) envfree;
     function getValue(address, address) external returns(uint256) envfree;
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index da6b43c..babf8bf 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -1,3 +1,5 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
 using MerkleTree as MerkleTree;
 using Util as Util;
 

From d612432a986119af89519d7386623c7fb5d57ba0 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 12:03:26 +0100
Subject: [PATCH 18/31] refactor: variable renaming

---
 certora/checker/create_certificate.py | 20 ++++++++++----------
 certora/helpers/MerkleTreeLib.sol     |  6 ++----
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
index e31b1d1..eb0315b 100644
--- a/certora/checker/create_certificate.py
+++ b/certora/checker/create_certificate.py
@@ -62,23 +62,23 @@ def populate(addr, reward, amount, proof):
 
 
 # Traverse the tree and generate corresponding instruction for each internal node and each leaf.
-def walk(h):
-    if h in left:
-        walk(left[h])
-        walk(right[h])
+def walk(node):
+    if node in left:
+        walk(left[node])
+        walk(right[node])
         certificate["node"].append(
             {
-                "id": h,
-                "left": hash_to_id[left[h]],
-                "right": hash_to_id[right[h]],
+                "id": node,
+                "left": hash_to_id[left[node]],
+                "right": hash_to_id[right[node]],
             }
         )
     else:
         certificate["leaf"].append(
             {
-                "addr": hash_to_address[h],
-                "reward": hash_to_reward[h],
-                "value": hash_to_value[h],
+                "addr": hash_to_address[node],
+                "reward": hash_to_reward[node],
+                "value": hash_to_value[node],
             }
         )
 
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index 2108644..fb28ee7 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -54,7 +54,7 @@ library MerkleTreeLib {
     }
 
     function setRoot(Tree storage tree, bytes32 id) internal {
-        require(!tree.nodes[id].isEmpty(), "root is empty");
+        require(!tree.nodes[id].isEmpty(), "node is empty");
         tree.root = id;
     }
 
@@ -77,9 +77,7 @@ library MerkleTreeLib {
             if (node.left == 0 || node.right == 0) return false;
             Node storage left = tree.nodes[node.left];
             Node storage right = tree.nodes[node.right];
-            // Well-formed nodes should have its children pair-sorted.
-            bool sorted = left.hashNode <= right.hashNode;
-            return !left.isEmpty() && !right.isEmpty() && sorted
+            return !left.isEmpty() && !right.isEmpty() && left.hashNode <= right.hashNode
                 && node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode));
         }
     }

From e8296dbd032568caaeeccc551ffb4438e7d62372 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 12:30:01 +0100
Subject: [PATCH 19/31] refactor: use structs in merkle tree lib

---
 certora/checker/Checker.sol       | 26 ++++++--------------
 certora/helpers/MerkleTreeLib.sol | 41 ++++++++++++++++++++-----------
 2 files changed, 35 insertions(+), 32 deletions(-)

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index 0313caa..8367562 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -12,35 +12,25 @@ contract Checker is Test {
 
     MerkleTreeLib.Tree public tree;
 
-    struct Leaf {
-        address addr;
-        address reward;
-        uint256 value;
-    }
-
-    struct InternalNode {
-        bytes32 id;
-        bytes32 left;
-        bytes32 right;
-    }
-
     function testVerifyCertificate() public {
         string memory projectRoot = vm.projectRoot();
         string memory path = string.concat(projectRoot, "/certificate.json");
         string memory json = vm.readFile(path);
 
         uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
-        Leaf memory leaf;
+        MerkleTreeLib.Leaf memory leaf;
         for (uint256 i; i < leafLength; i++) {
-            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
-            tree.newLeaf(leaf.addr, leaf.reward, leaf.value);
+            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (MerkleTreeLib.Leaf));
+            tree.newLeaf(leaf);
         }
 
         uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
-        InternalNode memory node;
+        MerkleTreeLib.InternalNode memory node;
         for (uint256 i; i < nodeLength; i++) {
-            node = abi.decode(json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (InternalNode));
-            tree.newInternalNode(node.id, node.left, node.right);
+            node = abi.decode(
+                json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (MerkleTreeLib.InternalNode)
+            );
+            tree.newInternalNode(node);
         }
 
         assertTrue(!tree.isEmpty(node.id), "empty root");
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index fb28ee7..b45f4db 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -4,12 +4,25 @@ pragma solidity ^0.8.0;
 library MerkleTreeLib {
     using MerkleTreeLib for Node;
 
+    struct Leaf {
+        address addr;
+        address reward;
+        uint256 value;
+    }
+
+    struct InternalNode {
+        bytes32 id;
+        bytes32 left;
+        bytes32 right;
+    }
+
     struct Node {
         bytes32 left;
         bytes32 right;
         address addr;
         address reward;
         uint256 value;
+        // hash of [addr, reward, value] for leaves, and [left.hash, right.hash] for internal nodes.
         bytes32 hashNode;
     }
 
@@ -23,33 +36,33 @@ library MerkleTreeLib {
         bytes32 root;
     }
 
-    function newLeaf(Tree storage tree, address addr, address reward, uint256 value) internal {
+    function newLeaf(Tree storage tree, Leaf memory leaf) internal {
         // The following identifier is used as the key to create a new leaf.
         // This ensures that the same pair of address and reward does not appear twice in the tree.
-        bytes32 id = keccak256(abi.encode(addr, reward));
+        bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
         Node storage node = tree.nodes[id];
         require(id != 0, "id is the zero bytes");
         require(node.isEmpty(), "leaf is not empty");
-        require(value != 0, "value is zero");
+        require(leaf.value != 0, "value is zero");
 
-        node.addr = addr;
-        node.reward = reward;
-        node.value = value;
-        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(addr, reward, value))));
+        node.addr = leaf.addr;
+        node.reward = leaf.reward;
+        node.value = leaf.value;
+        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(leaf.addr, leaf.reward, leaf.value))));
     }
 
-    function newInternalNode(Tree storage tree, bytes32 id, bytes32 left, bytes32 right) internal {
-        Node storage node = tree.nodes[id];
-        Node storage leftNode = tree.nodes[left];
-        Node storage rightNode = tree.nodes[right];
-        require(id != 0, "id is zero bytes");
+    function newInternalNode(Tree storage tree, InternalNode memory internalNode) internal {
+        Node storage node = tree.nodes[internalNode.id];
+        Node storage leftNode = tree.nodes[internalNode.left];
+        Node storage rightNode = tree.nodes[internalNode.right];
+        require(internalNode.id != 0, "id is zero bytes");
         require(node.isEmpty(), "node is not empty");
         require(!leftNode.isEmpty(), "left is empty");
         require(!rightNode.isEmpty(), "right is empty");
         require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
 
-        node.left = left;
-        node.right = right;
+        node.left = internalNode.left;
+        node.right = internalNode.right;
         node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 

From f450ce11095736c53678bbef1b96ffbf16ad0173 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 12:46:49 +0100
Subject: [PATCH 20/31] fix: new interface for node creation

---
 certora/helpers/MerkleTree.sol | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 9625bfb..99d9a28 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-only
 pragma solidity ^0.8.0;
 
 import "./MerkleTreeLib.sol";
@@ -9,12 +9,12 @@ contract MerkleTree {
 
     MerkleTreeLib.Tree tree;
 
-    function newLeaf(address addr, address reward, uint256 value) public {
-        tree.newLeaf(addr, reward, value);
+    function newLeaf(MerkleTreeLib.Leaf memory leaf) public {
+        tree.newLeaf(leaf);
     }
 
-    function newInternalNode(bytes32 parent, bytes32 left, bytes32 right) public {
-        tree.newInternalNode(parent, left, right);
+    function newInternalNode(MerkleTreeLib.InternalNode memory internalNode) public {
+        tree.newInternalNode(internalNode);
     }
 
     function setRoot(bytes32 id) public {

From 0ffa4a54f3d38ba6a4d830b0557a751fcb07c387 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 12:55:18 +0100
Subject: [PATCH 21/31] feat: check increasing claim amounts

---
 certora/specs/UniversalRewardsDistributor.spec | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index babf8bf..626c73d 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -42,11 +42,12 @@ rule claimTwice(address account, address reward, uint256 claim1, uint256 claim2)
     bytes32[] proof1; bytes32[] proof2;
     claim(account, reward, claim1, proof1);
     claim(account, reward, claim2, proof2);
+    assert claim2 >= claim1;
 
     storage afterBothStorage = lastStorage;
 
-    bytes32[] proof;
-    claim(account, reward, claim2, proof) at initStorage;
+    bytes32[] proof3;
+    claim(account, reward, claim2, proof3) at initStorage;
 
     assert lastStorage == afterBothStorage;
 }

From 4facf980484ef08140100aab02b5a97f401d00d0 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 11 Mar 2024 13:17:22 +0100
Subject: [PATCH 22/31] refactor: remove unnecessary root of the Merkle tree

---
 certora/checker/Checker.sol                    |  2 +-
 certora/helpers/MerkleTree.sol                 |  8 --------
 certora/helpers/MerkleTreeLib.sol              | 11 +----------
 certora/specs/MerkleTree.spec                  |  4 ----
 certora/specs/UniversalRewardsDistributor.spec |  2 +-
 5 files changed, 3 insertions(+), 24 deletions(-)

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index 8367562..dffe6f1 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -10,7 +10,7 @@ contract Checker is Test {
     using MerkleTreeLib for MerkleTreeLib.Tree;
     using stdJson for string;
 
-    MerkleTreeLib.Tree public tree;
+    MerkleTreeLib.Tree tree;
 
     function testVerifyCertificate() public {
         string memory projectRoot = vm.projectRoot();
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 99d9a28..bbd2b01 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -17,14 +17,6 @@ contract MerkleTree {
         tree.newInternalNode(internalNode);
     }
 
-    function setRoot(bytes32 id) public {
-        tree.setRoot(id);
-    }
-
-    function getRoot() public view returns (bytes32) {
-        return tree.getRoot();
-    }
-
     function getLeft(bytes32 id) public view returns (bytes32) {
         return tree.getLeft(id);
     }
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
index b45f4db..3abca4f 100644
--- a/certora/helpers/MerkleTreeLib.sol
+++ b/certora/helpers/MerkleTreeLib.sol
@@ -31,9 +31,9 @@ library MerkleTreeLib {
             && node.value == 0 && node.hashNode == 0;
     }
 
+    // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
     struct Tree {
         mapping(bytes32 => Node) nodes;
-        bytes32 root;
     }
 
     function newLeaf(Tree storage tree, Leaf memory leaf) internal {
@@ -66,11 +66,6 @@ library MerkleTreeLib {
         node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 
-    function setRoot(Tree storage tree, bytes32 id) internal {
-        require(!tree.nodes[id].isEmpty(), "node is empty");
-        tree.root = id;
-    }
-
     // The specification of a well-formed tree is the following:
     //   - empty nodes are well-formed
     //   - correct identifiers of leaves
@@ -99,10 +94,6 @@ library MerkleTreeLib {
         return tree.nodes[id].isEmpty();
     }
 
-    function getRoot(Tree storage tree) internal view returns (bytes32) {
-        return tree.root;
-    }
-
     function getLeft(Tree storage tree, bytes32 id) internal view returns (bytes32) {
         return tree.nodes[id].left;
     }
diff --git a/certora/specs/MerkleTree.spec b/certora/specs/MerkleTree.spec
index 85e4d39..0754f38 100644
--- a/certora/specs/MerkleTree.spec
+++ b/certora/specs/MerkleTree.spec
@@ -1,7 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 methods {
-    function getRoot() external returns(bytes32) envfree;
     function getValue(address, address) external returns(uint256) envfree;
     function isEmpty(bytes32) external returns(bool) envfree;
     function isWellFormed(bytes32) external returns(bool) envfree;
@@ -10,9 +9,6 @@ methods {
 invariant zeroIsEmpty()
     isEmpty(to_bytes32(0));
 
-invariant rootIsZeroOrNotEmpty()
-    getRoot() == to_bytes32(0) || !isEmpty(getRoot());
-
 invariant wellFormed(bytes32 id)
     isWellFormed(id)
 { preserved {
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index 626c73d..3f64c4d 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -76,7 +76,7 @@ rule claimCorrectness(address account, address reward, uint256 claimable, bytes3
     // Assume that root is the hash of node in the tree.
     require MerkleTree.getHash(node) == root();
 
-    // No need to make sure that node is equal to currRoot : one can pass an internal node instead.
+    // No need to make sure that node is equal to currRoot: one can pass an internal node instead.
 
     // Assume that the tree is well-formed.
     MerkleTree.wellFormedPath(node, proof);

From a67796792c2743293ee9ca31a2de7a7bdf732398 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 12 Mar 2024 11:18:27 +0100
Subject: [PATCH 23/31] refactor: remove MerkleTreeLib

---
 certora/checker/Checker.sol       |  15 ++--
 certora/helpers/MerkleTree.sol    | 114 ++++++++++++++++++++++++------
 certora/helpers/MerkleTreeLib.sol | 113 -----------------------------
 3 files changed, 99 insertions(+), 143 deletions(-)
 delete mode 100644 certora/helpers/MerkleTreeLib.sol

diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
index dffe6f1..6259862 100644
--- a/certora/checker/Checker.sol
+++ b/certora/checker/Checker.sol
@@ -2,15 +2,14 @@
 pragma solidity ^0.8.0;
 
 import "../../lib/openzeppelin-contracts/contracts/utils/Strings.sol";
-import "../helpers/MerkleTreeLib.sol";
+import "../helpers/MerkleTree.sol";
 import "../../lib/forge-std/src/Test.sol";
 import "../../lib/forge-std/src/StdJson.sol";
 
 contract Checker is Test {
-    using MerkleTreeLib for MerkleTreeLib.Tree;
     using stdJson for string;
 
-    MerkleTreeLib.Tree tree;
+    MerkleTree tree = new MerkleTree();
 
     function testVerifyCertificate() public {
         string memory projectRoot = vm.projectRoot();
@@ -18,18 +17,16 @@ contract Checker is Test {
         string memory json = vm.readFile(path);
 
         uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
-        MerkleTreeLib.Leaf memory leaf;
+        Leaf memory leaf;
         for (uint256 i; i < leafLength; i++) {
-            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (MerkleTreeLib.Leaf));
+            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
             tree.newLeaf(leaf);
         }
 
         uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
-        MerkleTreeLib.InternalNode memory node;
+        InternalNode memory node;
         for (uint256 i; i < nodeLength; i++) {
-            node = abi.decode(
-                json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (MerkleTreeLib.InternalNode)
-            );
+            node = abi.decode(json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (InternalNode));
             tree.newInternalNode(node);
         }
 
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index bbd2b01..75fd19e 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -1,59 +1,131 @@
 // SPDX-License-Identifier: AGPL-3.0-only
 pragma solidity ^0.8.0;
 
-import "./MerkleTreeLib.sol";
+struct Leaf {
+    address addr;
+    address reward;
+    uint256 value;
+}
+
+struct InternalNode {
+    bytes32 id;
+    bytes32 left;
+    bytes32 right;
+}
+
+struct Node {
+    bytes32 left;
+    bytes32 right;
+    address addr;
+    address reward;
+    uint256 value;
+    // hash of [addr, reward, value] for leaves, and [left.hash, right.hash] for internal nodes.
+    bytes32 hashNode;
+}
 
 contract MerkleTree {
-    using MerkleTreeLib for MerkleTreeLib.Node;
-    using MerkleTreeLib for MerkleTreeLib.Tree;
+    /* STORAGE */
+
+    // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
+    mapping(bytes32 => Node) internal tree;
+
+    /* MAIN FUNCTIONS */
+
+    function newLeaf(Leaf memory leaf) public {
+        // The following identifier is used as the key to create a new leaf.
+        // This ensures that the same pair of address and reward does not appear twice in the tree.
+        bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
+        Node storage node = tree[id];
+        require(id != 0, "id is the zero bytes");
+        require(isEmpty(node), "leaf is not empty");
+        require(leaf.value != 0, "value is zero");
+
+        node.addr = leaf.addr;
+        node.reward = leaf.reward;
+        node.value = leaf.value;
+        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(leaf.addr, leaf.reward, leaf.value))));
+    }
 
-    MerkleTreeLib.Tree tree;
+    function newInternalNode(InternalNode memory internalNode) public {
+        Node storage node = tree[internalNode.id];
+        Node storage leftNode = tree[internalNode.left];
+        Node storage rightNode = tree[internalNode.right];
+        require(internalNode.id != 0, "id is zero bytes");
+        require(isEmpty(node), "node is not empty");
+        require(!isEmpty(leftNode), "left is empty");
+        require(!isEmpty(rightNode), "right is empty");
+        require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
+
+        node.left = internalNode.left;
+        node.right = internalNode.right;
+        node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
+    }
 
-    function newLeaf(MerkleTreeLib.Leaf memory leaf) public {
-        tree.newLeaf(leaf);
+    /* GETTERS */
+
+    function isEmpty(Node memory node) public pure returns (bool) {
+        return node.left == 0 && node.right == 0 && node.addr == address(0) && node.reward == address(0)
+            && node.value == 0 && node.hashNode == 0;
     }
 
-    function newInternalNode(MerkleTreeLib.InternalNode memory internalNode) public {
-        tree.newInternalNode(internalNode);
+    function isEmpty(bytes32 id) public view returns (bool) {
+        return isEmpty(tree[id]);
     }
 
     function getLeft(bytes32 id) public view returns (bytes32) {
-        return tree.getLeft(id);
+        return tree[id].left;
     }
 
     function getRight(bytes32 id) public view returns (bytes32) {
-        return tree.getRight(id);
+        return tree[id].right;
     }
 
     function getValue(address addr, address reward) public view returns (uint256) {
-        return tree.getValue(addr, reward);
+        bytes32 id = keccak256(abi.encode(addr, reward));
+        return tree[id].value;
     }
 
     function getHash(bytes32 id) public view returns (bytes32) {
-        return tree.getHash(id);
-    }
-
-    function isEmpty(bytes32 id) public view returns (bool) {
-        return tree.nodes[id].isEmpty();
+        return tree[id].hashNode;
     }
 
+    // The specification of a well-formed tree is the following:
+    //   - empty nodes are well-formed
+    //   - correct identifiers of leaves
+    //   - correct hashing of leaves and of internal nodes
+    //   - internal nodes have their children pair sorted and not empty
     function isWellFormed(bytes32 id) public view returns (bool) {
-        return tree.isWellFormed(id);
+        Node storage node = tree[id];
+
+        if (isEmpty(node)) return true;
+
+        if (node.left == 0 && node.right == 0) {
+            bytes32 idLeaf = keccak256(abi.encode(node.addr, node.reward));
+            return id == idLeaf
+                && node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
+        } else {
+            // Well-formed nodes have exactly 0 or 2 children.
+            if (node.left == 0 || node.right == 0) return false;
+            Node storage left = tree[node.left];
+            Node storage right = tree[node.right];
+            return !isEmpty(left) && !isEmpty(right) && left.hashNode <= right.hashNode
+                && node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode));
+        }
     }
 
     // Check that the nodes are well formed on the path from the root.
     function wellFormedPath(bytes32 id, bytes32[] memory proof) public view {
         for (uint256 i = proof.length;;) {
-            require(tree.isWellFormed(id));
+            require(isWellFormed(id));
 
             if (i == 0) break;
 
             bytes32 otherHash = proof[--i];
 
-            bytes32 left = tree.getLeft(id);
-            bytes32 right = tree.getRight(id);
+            bytes32 left = getLeft(id);
+            bytes32 right = getRight(id);
 
-            id = tree.getHash(left) == otherHash ? right : left;
+            id = getHash(left) == otherHash ? right : left;
         }
     }
 }
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
deleted file mode 100644
index 3abca4f..0000000
--- a/certora/helpers/MerkleTreeLib.sol
+++ /dev/null
@@ -1,113 +0,0 @@
-// SPDX-License-Identifier: AGPL-3.0-only
-pragma solidity ^0.8.0;
-
-library MerkleTreeLib {
-    using MerkleTreeLib for Node;
-
-    struct Leaf {
-        address addr;
-        address reward;
-        uint256 value;
-    }
-
-    struct InternalNode {
-        bytes32 id;
-        bytes32 left;
-        bytes32 right;
-    }
-
-    struct Node {
-        bytes32 left;
-        bytes32 right;
-        address addr;
-        address reward;
-        uint256 value;
-        // hash of [addr, reward, value] for leaves, and [left.hash, right.hash] for internal nodes.
-        bytes32 hashNode;
-    }
-
-    function isEmpty(Node memory node) internal pure returns (bool) {
-        return node.left == 0 && node.right == 0 && node.addr == address(0) && node.reward == address(0)
-            && node.value == 0 && node.hashNode == 0;
-    }
-
-    // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
-    struct Tree {
-        mapping(bytes32 => Node) nodes;
-    }
-
-    function newLeaf(Tree storage tree, Leaf memory leaf) internal {
-        // The following identifier is used as the key to create a new leaf.
-        // This ensures that the same pair of address and reward does not appear twice in the tree.
-        bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
-        Node storage node = tree.nodes[id];
-        require(id != 0, "id is the zero bytes");
-        require(node.isEmpty(), "leaf is not empty");
-        require(leaf.value != 0, "value is zero");
-
-        node.addr = leaf.addr;
-        node.reward = leaf.reward;
-        node.value = leaf.value;
-        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(leaf.addr, leaf.reward, leaf.value))));
-    }
-
-    function newInternalNode(Tree storage tree, InternalNode memory internalNode) internal {
-        Node storage node = tree.nodes[internalNode.id];
-        Node storage leftNode = tree.nodes[internalNode.left];
-        Node storage rightNode = tree.nodes[internalNode.right];
-        require(internalNode.id != 0, "id is zero bytes");
-        require(node.isEmpty(), "node is not empty");
-        require(!leftNode.isEmpty(), "left is empty");
-        require(!rightNode.isEmpty(), "right is empty");
-        require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
-
-        node.left = internalNode.left;
-        node.right = internalNode.right;
-        node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
-    }
-
-    // The specification of a well-formed tree is the following:
-    //   - empty nodes are well-formed
-    //   - correct identifiers of leaves
-    //   - correct hashing of leaves and of internal nodes
-    //   - internal nodes have their children pair sorted and not empty
-    function isWellFormed(Tree storage tree, bytes32 id) internal view returns (bool) {
-        Node storage node = tree.nodes[id];
-
-        if (node.isEmpty()) return true;
-
-        if (node.left == 0 && node.right == 0) {
-            bytes32 idLeaf = keccak256(abi.encode(node.addr, node.reward));
-            return id == idLeaf
-                && node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
-        } else {
-            // Well-formed nodes have exactly 0 or 2 children.
-            if (node.left == 0 || node.right == 0) return false;
-            Node storage left = tree.nodes[node.left];
-            Node storage right = tree.nodes[node.right];
-            return !left.isEmpty() && !right.isEmpty() && left.hashNode <= right.hashNode
-                && node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode));
-        }
-    }
-
-    function isEmpty(Tree storage tree, bytes32 id) internal view returns (bool) {
-        return tree.nodes[id].isEmpty();
-    }
-
-    function getLeft(Tree storage tree, bytes32 id) internal view returns (bytes32) {
-        return tree.nodes[id].left;
-    }
-
-    function getRight(Tree storage tree, bytes32 id) internal view returns (bytes32) {
-        return tree.nodes[id].right;
-    }
-
-    function getValue(Tree storage tree, address addr, address reward) internal view returns (uint256) {
-        bytes32 id = keccak256(abi.encode(addr, reward));
-        return tree.nodes[id].value;
-    }
-
-    function getHash(Tree storage tree, bytes32 id) internal view returns (bytes32) {
-        return tree.nodes[id].hashNode;
-    }
-}

From a588de34adb9dac73ef62a10dcae98ec3338aa89 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 12 Mar 2024 13:25:59 +0100
Subject: [PATCH 24/31] docs: clarify verification

---
 certora/README.md              | 2 +-
 certora/helpers/MerkleTree.sol | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index af6bfbe..dfbb40b 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -53,7 +53,7 @@ This requires installing the corresponding libraries first:
 pip install web3 eth-tester py-evm
 ```
 
-Then, verify this certificate:
+Then, check this certificate:
 
 ```
 FOUNDRY_PROFILE=checker forge test
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 75fd19e..5bca7ed 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -113,7 +113,8 @@ contract MerkleTree {
         }
     }
 
-    // Check that the nodes are well formed on the path from the root.
+    // Check that the nodes are well formed starting from `node` and going down the `tree.
+    // The `proof` is used to choose the path downward.
     function wellFormedPath(bytes32 id, bytes32[] memory proof) public view {
         for (uint256 i = proof.length;;) {
             require(isWellFormed(id));

From fd6cc82c16303cb5837a39e530860f35170eb779 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 12 Mar 2024 15:39:30 +0100
Subject: [PATCH 25/31] docs: pure and view functions

---
 certora/helpers/MerkleTree.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 5bca7ed..806adfd 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -61,7 +61,7 @@ contract MerkleTree {
         node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
     }
 
-    /* GETTERS */
+    /* PURE AND VIEW FUNCTIONS */
 
     function isEmpty(Node memory node) public pure returns (bool) {
         return node.left == 0 && node.right == 0 && node.addr == address(0) && node.reward == address(0)

From 28c6e4b4a064cb1f14f3bbe3da8a17e7562859c3 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 11:37:40 +0100
Subject: [PATCH 26/31] feat: accept root storage change

---
 .github/workflows/certora.yml                  |  2 +-
 certora/confs/MerkleTree.conf                  |  1 +
 certora/confs/UniversalRewardsDistributor.conf |  1 +
 certora/specs/UniversalRewardsDistributor.spec | 13 +++++++++++++
 4 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 8415d87..0ca3fac 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -37,7 +37,7 @@ jobs:
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Verify ${{ matrix.conf }}
         run: certoraRun certora/confs/${{ matrix.conf }}.conf
diff --git a/certora/confs/MerkleTree.conf b/certora/confs/MerkleTree.conf
index 4287ba6..73e698d 100644
--- a/certora/confs/MerkleTree.conf
+++ b/certora/confs/MerkleTree.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MerkleTree.sol"
     ],
+    "solc": "solc-0.8.19",
     "verify": "MerkleTree:certora/specs/MerkleTree.spec",
     "optimistic_loop": true,
     "loop_iter": "4",
diff --git a/certora/confs/UniversalRewardsDistributor.conf b/certora/confs/UniversalRewardsDistributor.conf
index 4689525..4cc7bdc 100644
--- a/certora/confs/UniversalRewardsDistributor.conf
+++ b/certora/confs/UniversalRewardsDistributor.conf
@@ -5,6 +5,7 @@
         "certora/helpers/MerkleTree.sol",
         "certora/helpers/Util.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
     "optimistic_loop": true,
     "loop_iter": "4",
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index 3f64c4d..047b768 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -5,8 +5,10 @@ using Util as Util;
 
 methods {
     function root() external returns bytes32 envfree;
+    function ipfsHash() external returns bytes32 envfree;
     function claimed(address, address) external returns(uint256) envfree;
     function claim(address, address, uint256, bytes32[]) external returns(uint256) envfree;
+    function pendingRoot() external returns(bytes32, bytes32, uint256) envfree;
 
     function MerkleTree.getValue(address, address) external returns(uint256) envfree;
     function MerkleTree.getHash(bytes32) external returns(bytes32) envfree;
@@ -19,6 +21,17 @@ methods {
     function Util.balanceOf(address, address) external returns(uint256) envfree;
 }
 
+// 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);

From 2609c719b9c6f2f5092f398027923549aeb21910 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 11:46:16 +0100
Subject: [PATCH 27/31] docs: comment on claim correctness rule

---
 certora/helpers/MerkleTree.sol                 | 2 +-
 certora/specs/UniversalRewardsDistributor.spec | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 806adfd..5a4298c 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -113,7 +113,7 @@ contract MerkleTree {
         }
     }
 
-    // Check that the nodes are well formed starting from `node` and going down the `tree.
+    // Check that the nodes are well formed starting from `node` and going down the `tree`.
     // The `proof` is used to choose the path downward.
     function wellFormedPath(bytes32 id, bytes32[] memory proof) public view {
         for (uint256 i = proof.length;;) {
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index 047b768..089a33b 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -83,6 +83,8 @@ rule transferredTokens(address account, address reward, uint256 claimable, bytes
     assert balanceAfter - balanceBefore == claimable - claimedBefore;
 }
 
+// The main correctness result of the verification.
+// It ensures that if the root is setup according to a well-formed Merkle tree, then claiming will result in receiving the rewards stored in the tree for that particular pair of account and reward.
 rule claimCorrectness(address account, address reward, uint256 claimable, bytes32[] proof) {
     bytes32 node;
 

From 99fbc6afcb3b9b3fa77abcbb3c36e0ff511ef70b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 11:55:11 +0100
Subject: [PATCH 28/31] refactor: remove getLeft and getRight

---
 certora/helpers/MerkleTree.sol | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index 5a4298c..e429567 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -72,14 +72,6 @@ contract MerkleTree {
         return isEmpty(tree[id]);
     }
 
-    function getLeft(bytes32 id) public view returns (bytes32) {
-        return tree[id].left;
-    }
-
-    function getRight(bytes32 id) public view returns (bytes32) {
-        return tree[id].right;
-    }
-
     function getValue(address addr, address reward) public view returns (uint256) {
         bytes32 id = keccak256(abi.encode(addr, reward));
         return tree[id].value;
@@ -123,8 +115,8 @@ contract MerkleTree {
 
             bytes32 otherHash = proof[--i];
 
-            bytes32 left = getLeft(id);
-            bytes32 right = getRight(id);
+            bytes32 left = tree[id].left;
+            bytes32 right = tree[id].right;
 
             id = getHash(left) == otherHash ? right : left;
         }

From 7ecb32178d4967981c8d2f2d5cc47a3caff47ad7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 12:08:41 +0100
Subject: [PATCH 29/31] docs: update without total rewards

---
 certora/README.md | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index dfbb40b..d20271b 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -12,15 +12,11 @@ The [`certora/helpers`](helpers) folder contains files that enable the verific
 
 This work aims at providing a formally verified rewards checker.
 The rewards checker is composed of the [Checker.sol](checker/Checker.sol) file, which takes a certificate as an input.
-The certificate is assumed to contain the submitted root to verify, a total amount of rewards distributed, and a Merkle tree, and it is checked that:
-
-1. the Merkle tree is a well-formed Merkle tree
-2. the total amount of rewards distributed matches the total rewards contained in the Merkle tree
+The certificate is assumed to contain the submitted root to verify and a Merkle tree, and it is checked that the Merkle tree is well-formed.
 
 Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants:
 
 - it is checked in [MerkleTree.spec](specs/MerkleTree.spec) that those functions lead to creating well-formed trees.
-  Well-formed trees also verify that the value of their internal node is the sum of the rewards it contains.
 - it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.
 
 # Getting started

From 47203a6609be40d23ffb87102fa5a88c0a3fa621 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 18:03:39 +0100
Subject: [PATCH 30/31] refactor: remove claim twice rule as it should not be
 possible

---
 certora/helpers/MerkleTree.sol                 |  5 +++--
 certora/specs/UniversalRewardsDistributor.spec | 17 -----------------
 2 files changed, 3 insertions(+), 19 deletions(-)

diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
index e429567..da051ff 100644
--- a/certora/helpers/MerkleTree.sol
+++ b/certora/helpers/MerkleTree.sol
@@ -27,13 +27,14 @@ contract MerkleTree {
     /* STORAGE */
 
     // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
+    // We use bytes32 as keys of the mapping so that leaves can have an identifier that is the hash of the address and the reward token.
+    // This ensures that the same pair of address and reward token does not appear twice as a leaf in the tree.
+    // For internal nodes the key is left arbitrary, so that the certificate generation can choose freely any bytes32 value (that is not already used).
     mapping(bytes32 => Node) internal tree;
 
     /* MAIN FUNCTIONS */
 
     function newLeaf(Leaf memory leaf) public {
-        // The following identifier is used as the key to create a new leaf.
-        // This ensures that the same pair of address and reward does not appear twice in the tree.
         bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
         Node storage node = tree[id];
         require(id != 0, "id is the zero bytes");
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
index 089a33b..51037c4 100644
--- a/certora/specs/UniversalRewardsDistributor.spec
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -48,23 +48,6 @@ rule increasingClaimedAmounts(address account, address reward, uint256 claimable
     assert claimable > claimed;
 }
 
-// Check that claiming twice is equivalent to claiming once with the last amount.
-rule claimTwice(address account, address reward, uint256 claim1, uint256 claim2) {
-    storage initStorage = lastStorage;
-
-    bytes32[] proof1; bytes32[] proof2;
-    claim(account, reward, claim1, proof1);
-    claim(account, reward, claim2, proof2);
-    assert claim2 >= claim1;
-
-    storage afterBothStorage = lastStorage;
-
-    bytes32[] proof3;
-    claim(account, reward, claim2, proof3) at initStorage;
-
-    assert lastStorage == afterBothStorage;
-}
-
 // Check that the transferred amount is equal to the claimed amount minus the previous claimed amount.
 rule transferredTokens(address account, address reward, uint256 claimable, bytes32[] proof) {
     // Assume that the rewards distributor itself is not receiving the tokens, to simplify this rule.

From 12ae1430e19ad62f2cd753c5a9d94d946edc9bf2 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 25 Mar 2024 10:20:03 +0100
Subject: [PATCH 31/31] chore: remove Dockerfile

---
 Dockerfile | 14 --------------
 1 file changed, 14 deletions(-)
 delete mode 100644 Dockerfile

diff --git a/Dockerfile b/Dockerfile
deleted file mode 100644
index f94749f..0000000
--- a/Dockerfile
+++ /dev/null
@@ -1,14 +0,0 @@
-FROM ubuntu:latest
-WORKDIR /usr/rewards-checker
-
-RUN apt update
-RUN apt install python3-pip git curl -y
-RUN pip install web3 eth-tester py-evm
-
-RUN curl -L https://foundry.paradigm.xyz | bash
-ENV PATH="${PATH}:/root/.foundry/bin/"
-RUN foundryup
-
-COPY . .
-RUN python3 certora/checker/create_certificate.py proofs.json
-RUN FOUNDRY_PROFILE=checker forge test