Merge pull request #114 from morpho-org/certora/hash-key

[Certora] Hash key

.github/workflows/certora.yml

@@ -16,7 +16,7 @@ jobs:
 
       matrix:
         conf:
-          - MerkleTrees
+          - MerkleTree
           - UniversalRewardsDistributor
 
     steps:

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.
 

certora/confs/MerkleTrees.conf → 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",
 }

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

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

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,18 @@ 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) {
+            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 == 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 +85,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;
     }
 }

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