feat: import distributor verification

.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 }}

.gitignore

@@ -15,4 +15,8 @@ docs/
 
 # npm
 package-lock.json
-node_modules
+node_modules
+
+# certora
+.certora**
+emv-*-certora*

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
+```

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");
+    }
+}

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)

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",
+}

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",
+}

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;
+    }
+}