fix: new interface for node creation

morpho-org · Mar 11, 2024 · f5daa10 · f5daa10
1 parent 38276f2
commit f5daa10
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 20 deletions.
diff --git a/certora/helpers/MerkleTrees.sol b/certora/helpers/MerkleTrees.sol
@@ -9,21 +9,14 @@ 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, MerkleTreeLib.Leaf memory leaf) public {
+        trees[treeAddress].newLeaf(leaf);
     }
 
-    function newInternalNode(
-        address treeAddress,
-        address parent,
-        address left,
-        address right
-    ) public {
-        trees[treeAddress].newInternalNode(parent, left, right);
+    function newInternalNode(address treeAddress, MerkleTreeLib.InternalNode memory internalNode)
+        public
+    {
+        trees[treeAddress].newInternalNode(internalNode);
     }
 
     function setRoot(address treeAddress, address addr) public {

diff --git a/certora/specs/MerkleTrees.spec b/certora/specs/MerkleTrees.spec
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: AGPL-3.0-only
 
 methods {
-    function newInternalNode(address, address, address, address) external envfree;
+    function newInternalNode(address, MerkleTreeLib.InternalNode) external envfree;
 
     function getRoot(address) external returns address envfree;
     function getValue(address, address) external returns uint256 envfree;
@@ -14,9 +14,9 @@ invariant zeroIsEmpty(address tree)
 
 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);
+{ preserved newInternalNode(address _, MerkleTreeLib.InternalNode internalNode) {
+    requireInvariant nonEmptyHasValue(tree, internalNode.left);
+    requireInvariant nonEmptyHasValue(tree, internalNode.right);
   }
 }
 
@@ -28,9 +28,9 @@ invariant wellFormed(address tree, address addr)
 { preserved {
     requireInvariant zeroIsEmpty(tree);
   }
-  preserved newInternalNode(address _, address parent, address left, address right) {
+  preserved newInternalNode(address _, MerkleTreeLib.InternalNode internalNode) {
     requireInvariant zeroIsEmpty(tree);
-    requireInvariant nonEmptyHasValue(tree, left);
-    requireInvariant nonEmptyHasValue(tree, right);
+    requireInvariant nonEmptyHasValue(tree, internalNode.left);
+    requireInvariant nonEmptyHasValue(tree, internalNode.right);
   }
 }