Merge pull request #1668 from morpho-org/certora/rewards-checker

Certora rewards checker

certora/checker/Checker.sol

@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import "../../lib/morpho-utils/lib/openzeppelin-contracts/contracts/utils/Strings.sol";
+import "../helpers/MerkleTreeLib.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 public tree;
+
+    struct Leaf {
+        address addr;
+        uint256 value;
+    }
+
+    struct InternalNode {
+        address addr;
+        address left;
+        address right;
+    }
+
+    function testVerifyCertificate() public {
+        string memory projectRoot = vm.projectRoot();
+        string memory path = string.concat(projectRoot, "/certificate.json");
+        string memory json = vm.readFile(path);
+
+        uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
+        Leaf memory leaf;
+        for (uint256 i; i < leafLength; i++) {
+            leaf = abi.decode(
+                json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")),
+                (Leaf)
+            );
+            tree.newAccount(leaf.addr, leaf.value);
+        }
+
+        uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
+        InternalNode memory node;
+        for (uint256 i; i < nodeLength; i++) {
+            node = abi.decode(
+                json.parseRaw(string.concat(".node[", Strings.toString(i), "]")),
+                (InternalNode)
+            );
+            tree.newNode(node.addr, node.left, node.right);
+        }
+
+        bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
+
+        assertTrue(tree.getCreated(node.addr), "unrecognized node");
+        assertEq(tree.getHash(node.addr), root, "mismatched roots");
+    }
+}

certora/checker/create_certificate.py

@@ -0,0 +1,77 @@
+import sys
+import json
+from web3 import Web3, EthereumTesterProvider
+
+w3 = Web3(EthereumTesterProvider())
+
+
+def keccak_node(left_hash, right_hash):
+    return w3.to_hex(
+        w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
+    )
+
+
+def keccak_leaf(address, amount):
+    address = w3.to_checksum_address(address)
+    return w3.to_hex(w3.solidity_keccak(["address", "uint256"], [address, amount]))
+
+
+certificate = {}
+hash_to_address = {}
+hash_to_value = {}
+left = {}
+right = {}
+
+
+def populate(address, amount, proof):
+    amount = int(amount)
+    computedHash = keccak_leaf(address, amount)
+    hash_to_address[computedHash] = address
+    hash_to_value[computedHash] = amount
+    for proofElement in proof:
+        [leftHash, rightHash] = (
+            [computedHash, proofElement]
+            if computedHash <= proofElement
+            else [proofElement, computedHash]
+        )
+        computedHash = keccak_node(leftHash, rightHash)
+        left[computedHash] = leftHash
+        right[computedHash] = rightHash
+        hash_to_address[computedHash] = keccak_node(computedHash, computedHash)[:42]
+
+
+def walk(h):
+    if h in left:
+        walk(left[h])
+        walk(right[h])
+        certificate["node"].append(
+            {
+                "addr": hash_to_address[h],
+                "left": hash_to_address[left[h]],
+                "right": hash_to_address[right[h]],
+            }
+        )
+    else:
+        certificate["leaf"].append(
+            {"addr": hash_to_address[h], "value": hash_to_value[h]}
+        )
+
+
+with open(sys.argv[1]) as input_file:
+    proofs = json.load(input_file)
+    certificate["root"] = proofs["root"]
+    certificate["leaf"] = []
+    certificate["node"] = []
+
+    for address, data in proofs["proofs"].items():
+        populate(address, data["amount"], data["proof"])
+
+    walk(proofs["root"])
+
+    certificate["leafLength"] = len(certificate["leaf"])
+    certificate["nodeLength"] = len(certificate["node"])
+
+    json_output = json.dumps(certificate)
+
+with open("certificate.json", "w") as output_file:
+    output_file.write(json_output)

certora/helpers/MerkleTreeLib.sol

@@ -29,9 +29,9 @@ library MerkleTreeLib {
         uint256 value
     ) internal {
         Node storage node = tree.nodes[addr];
-        require(addr != address(0));
-        require(!node.created);
-        require(value != 0);
+        require(addr != address(0), "addr is zero address");
+        require(!node.created, "node is already created");
+        require(value != 0, "value is zero");
 
         node.created = true;
         node.value = value;
@@ -48,17 +48,18 @@ library MerkleTreeLib {
         Node storage parentNode = tree.nodes[parent];
         Node storage leftNode = tree.nodes[left];
         Node storage rightNode = tree.nodes[right];
-        require(parent != address(0));
-        require(!parentNode.created);
-        require(leftNode.created && rightNode.created);
-        require(leftNode.hashNode <= rightNode.hashNode);
+        require(parent != address(0), "parent is zero address");
+        require(!parentNode.created, "parent is already created");
+        require(leftNode.created, "left is not created");
+        require(rightNode.created, "right is not created");
+        require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
 
         // Notice that internal nodes have value 0.
         parentNode.created = true;
         parentNode.left = left;
         parentNode.right = right;
         parentNode.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
-        require(parentNode.hashNode << 160 != 0);
+        require(parentNode.hashNode << 160 != 0, "invalid node hash");
     }
 
     function setRoot(Tree storage tree, address addr) internal {

foundry.toml

@@ -19,3 +19,8 @@ fork_block_number = 15_581_371
 
 [profile.aave-v2]
 fork_block_number = 15_581_371 # Block number when the Aave's V2 IRM was updated for the stETH.
+
+[profile.checker]
+test = 'certora/checker'
+fs_permissions = [{access = "read", path= "./"}]
+match_contract = 'Checker'