feat: check update root storage change

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

Hide file tree

Showing 2 changed files with 20 additions and 9 deletions.
diff --git a/certora/specs/MerkleTrees.spec b/certora/specs/MerkleTrees.spec
@@ -3,9 +3,9 @@
 methods {
     function newInternalNode(address, MerkleTreeLib.InternalNode) external envfree;
 
-    function getValue(address, address) external returns uint256 envfree;
-    function isEmpty(address, address) external returns bool envfree;
-    function isWellFormed(address, address) external returns bool envfree;
+    function getValue(address, address) external returns(uint256) envfree;
+    function isEmpty(address, address) external returns(bool) envfree;
+    function isWellFormed(address, address) external returns(bool) envfree;
 }
 
 invariant zeroIsEmpty(address tree)

diff --git a/certora/specs/RewardsDistributor.spec b/certora/specs/RewardsDistributor.spec
@@ -4,16 +4,27 @@ using MerkleTrees as MerkleTrees;
 using MorphoToken as MorphoToken;
 
 methods {
-    function prevRoot() external returns bytes32 envfree;
-    function currRoot() external returns bytes32 envfree;
-    function claimed(address) external returns uint256 envfree;
+    function prevRoot() external returns(bytes32) envfree;
+    function currRoot() external returns(bytes32) envfree;
+    function claimed(address) external returns(uint256) envfree;
+    function updateRoot(bytes32) external envfree;
     function claim(address, uint256, bytes32[]) external envfree;
 
-    function MerkleTrees.getValue(address, address) external returns uint256 envfree;
-    function MerkleTrees.getHash(address, address) external returns bytes32 envfree;
+    function MerkleTrees.getValue(address, address) external returns(uint256) envfree;
+    function MerkleTrees.getHash(address, address) external returns(bytes32) envfree;
     function MerkleTrees.wellFormedPath(address, address, bytes32[]) external envfree;
 
-    function MorphoToken.balanceOf(address) external returns uint256 envfree;
+    function MorphoToken.balanceOf(address) external returns(uint256) envfree;
+}
+
+// Check how updateRoot changes the storage.
+rule updateRootStorageChange(bytes32 _newRoot) {
+    bytes32 rootBefore = currRoot();
+
+    updateRoot(_newRoot);
+
+    assert prevRoot() == rootBefore;
+    assert currRoot() == _newRoot;
 }
 
 // Check an account claimed amount is correctly updated.