refactor: checker is now based on the contract instead of the lib

morpho-org · Mar 11, 2024 · 223f718 · 223f718
1 parent ef54f35
commit 223f718
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 55 deletions.
diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
@@ -2,15 +2,15 @@
 pragma solidity ^0.8.0;
 
 import "../../lib/morpho-utils/lib/openzeppelin-contracts/contracts/utils/Strings.sol";
-import "../helpers/MerkleTreeLib.sol";
+import "../helpers/MerkleTrees.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 internal tree;
+    MerkleTrees trees = new MerkleTrees();
+    address constant tree = address(0);
 
     function testVerifyCertificate() public {
         string memory projectRoot = vm.projectRoot();
@@ -24,7 +24,7 @@ contract Checker is Test {
                 json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")),
                 (MerkleTreeLib.Leaf)
             );
-            tree.newLeaf(leaf);
+            trees.newLeaf(tree, leaf);
         }
 
         uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
@@ -34,15 +34,15 @@ contract Checker is Test {
                 json.parseRaw(string.concat(".node[", Strings.toString(i), "]")),
                 (MerkleTreeLib.InternalNode)
             );
-            tree.newInternalNode(node);
+            trees.newInternalNode(tree, node);
         }
 
-        assertTrue(!tree.isEmpty(node.addr), "empty root");
+        assertTrue(!trees.isEmpty(tree, node.addr), "empty root");
 
         uint256 total = abi.decode(json.parseRaw(".total"), (uint256));
-        assertEq(tree.getValue(node.addr), total, "incorrect total rewards");
+        assertEq(trees.getValue(tree, node.addr), total, "incorrect total rewards");
 
         bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
-        assertEq(tree.getHash(node.addr), root, "mismatched roots");
+        assertEq(trees.getHash(tree, node.addr), root, "mismatched roots");
     }
 }
diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol
@@ -93,24 +93,4 @@ library MerkleTreeLib {
                 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 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
@@ -7,61 +7,57 @@ contract MerkleTrees {
     using MerkleTreeLib for MerkleTreeLib.Node;
     using MerkleTreeLib for MerkleTreeLib.Tree;
 
-    mapping(address => MerkleTreeLib.Tree) trees;
+    mapping(address => MerkleTreeLib.Tree) internal trees;
 
-    function newLeaf(address treeAddress, MerkleTreeLib.Leaf memory leaf) public {
-        trees[treeAddress].newLeaf(leaf);
+    function newLeaf(address tree, MerkleTreeLib.Leaf memory leaf) public {
+        trees[tree].newLeaf(leaf);
     }
 
-    function newInternalNode(address treeAddress, MerkleTreeLib.InternalNode memory internalNode)
-        public
-    {
-        trees[treeAddress].newInternalNode(internalNode);
+    function newInternalNode(address tree, MerkleTreeLib.InternalNode memory internalNode) public {
+        trees[tree].newInternalNode(internalNode);
     }
 
-    function getLeft(address treeAddress, address addr) public view returns (address) {
-        return trees[treeAddress].getLeft(addr);
+    function getLeft(address tree, address node) public view returns (address) {
+        return trees[tree].nodes[node].left;
     }
 
-    function getRight(address treeAddress, address addr) public view returns (address) {
-        return trees[treeAddress].getRight(addr);
+    function getRight(address tree, address node) public view returns (address) {
+        return trees[tree].nodes[node].right;
     }
 
-    function getValue(address treeAddress, address addr) public view returns (uint256) {
-        return trees[treeAddress].getValue(addr);
+    function getValue(address tree, address node) public view returns (uint256) {
+        return trees[tree].nodes[node].value;
     }
 
-    function getHash(address treeAddress, address addr) public view returns (bytes32) {
-        return trees[treeAddress].getHash(addr);
+    function getHash(address tree, address node) public view returns (bytes32) {
+        return trees[tree].nodes[node].hashNode;
     }
 
-    function isEmpty(address treeAddress, address addr) public view returns (bool) {
-        return trees[treeAddress].nodes[addr].isEmpty();
+    function isEmpty(address tree, address node) public view returns (bool) {
+        return trees[tree].nodes[node].isEmpty();
     }
 
-    function isWellFormed(address treeAddress, address addr) public view returns (bool) {
-        return trees[treeAddress].isWellFormed(addr);
+    function isWellFormed(address tree, address node) public view returns (bool) {
+        return trees[tree].isWellFormed(node);
     }
 
     // Check that the nodes are well formed on the path from the root.
     function wellFormedPath(
-        address treeAddress,
-        address addr,
+        address tree,
+        address node,
         bytes32[] memory proof
     ) public view {
-        MerkleTreeLib.Tree storage tree = trees[treeAddress];
-
         for (uint256 i = proof.length; ; ) {
-            require(tree.isWellFormed(addr));
+            require(isWellFormed(tree, node));
 
             if (i == 0) break;
 
             bytes32 otherHash = proof[--i];
 
-            address left = tree.getLeft(addr);
-            address right = tree.getRight(addr);
+            address left = getLeft(tree, node);
+            address right = getRight(tree, node);
 
-            addr = tree.getHash(left) == otherHash ? right : left;
+            node = getHash(tree, left) == otherHash ? right : left;
         }
     }
 }