refactor: require well formed on the path only

certora/helpers/MerkleTrees.sol

@@ -58,21 +58,28 @@ contract MerkleTrees {
         return trees[treeAddress].isWellFormed(addr);
     }
 
-    // Only go up to a given depth, to avoid CVL recursion protection.
-    function wellFormedUpTo(
+    // Check that the nodes are well formed on the path from the root.
+    // Stops early if the proof is incorrect.
+    function wellFormedPath(
         address treeAddress,
         address addr,
-        uint256 depth
+        bytes32[] memory proof,
+        uint256 length
     ) public view {
-        if (depth == 0) return;
+        MerkleTreeLib.Tree storage tree = trees[treeAddress];
 
-        require(trees[treeAddress].isWellFormed(addr));
+        require(tree.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);
+        if (length == 0) return;
+
+        bytes32 otherHash = proof[length - 1];
+
+        address left = tree.getLeft(addr);
+        address right = tree.getRight(addr);
+        if (tree.getHash(left) == otherHash) {
+            wellFormedPath(treeAddress, right, proof, length - 1);
+        } else if (tree.getHash(right) == otherHash) {
+            wellFormedPath(treeAddress, left, proof, length - 1);
         }
     }
 }

certora/specs/RewardsDistributor.spec

@@ -9,7 +9,7 @@ methods {
 
     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 MerkleTrees.wellFormedPath(address, address, bytes32[], uint256) external envfree;
 
     function MorphoToken.balanceOf(address) external returns uint256 envfree;
 }
@@ -75,8 +75,8 @@ rule claimCorrectness(address _account, uint256 _claimable, bytes32[] _proof) {
     // No need to make sure that currNode (resp prevNode) is equal to currRoot (resp prevRoot): one can pass an internal node instead.
 
     // Assume that prevTree and currTree are well-formed.
-    MerkleTrees.wellFormedUpTo(prevTree, prevNode, 3);
-    MerkleTrees.wellFormedUpTo(currTree, currNode, 3);
+    MerkleTrees.wellFormedPath(prevTree, prevNode, _proof, _proof.length);
+    MerkleTrees.wellFormedPath(currTree, currNode, _proof, _proof.length);
 
     claim(_account, _claimable, _proof);