diff --git a/certora/README.md b/certora/README.md index 62199d767..b2da4a4f0 100644 --- a/certora/README.md +++ b/certora/README.md @@ -43,6 +43,39 @@ How offers are consumed when taken. - [`EmptyOffer.spec`](specs/EmptyOffer.spec) checks that taking an empty offer always reverts (so the offer tree can be padded with empty offers). - [`Ratification.spec`](specs/Ratification.spec) checks that every successful take requires the maker to have authorized the ratifier. +## Offer trees + +Offers are authorized in batches: a ratifier signs a single Merkle root over an offer tree, and a `take` only succeeds if the offer's hash is proven to be a leaf under that root. +Objective is to show that a successful `take` can only settle an offer that was genuinely committed in the signed tree. +We reason about [`OfferTree`](helpers/OfferTree.sol), a model of the tree built only through the `newLeaf` and `newInternalNode` primitives. Leaves are keyed by `HashLib.hashOffer(offer)` and store a fixed-size pre-image of the offer, so `isWellFormed` re-hashes a leaf with a single bounded keccak instead of looping over the offer's dynamic members, which keeps the proofs bounded regardless of offer size. + +- [`OfferTreeWellFormed.spec`](specs/OfferTreeWellFormed.spec) checks that the primitives only ever build well-formed trees: every node is empty, a leaf carrying a genuine `hashOffer`, or an internal node correctly hashing its two children. In particular, there is no restriction for the left and right children of a parent node to be sorted. +- [`OfferTreeMembership.spec`](specs/OfferTreeMembership.spec) checks the main soundness result: for any well-formed tree, if a Merkle proof verifies an offer's hash against the root, then the offer is registered as a leaf. Equivalently, no valid proof can be forged for an offer that is not in the tree. +- [`Ratification.spec`](specs/Ratification.spec) connects this to the on-chain path: every successful `isRatified` (across all ratifier implementations) and every successful `take` actually invokes `HashLib.isLeaf` and it returns true. + +Combining the three: a successful `take` runs a Merkle membership check against the ratified root (`Ratification`), which for a well-formed root implies the offer is genuinely a leaf of that tree (`OfferTreeMembership`), and the root is well-formed because it is built only from the well-formedness-preserving primitives (`OfferTreeWellFormed`). + +### Checking a concrete root + +The membership result is stated for any well-formed root; the checker in [`checker`](checker) lets anyone confirm what a specific root commits to, by rebuilding the tree through the same verified primitives. + +1. Write a `proofs.json` listing the claimed `root` and the offers (`leaves`), padded to a power of two with empty offers. +2. Generate the certificate, from the repository root: + ``` + python certora/checker/create_certificate.py proofs.json + ``` + This recomputes the tree bottom-up, asserts the computed root equals the claimed `root`, and writes `certificate.json`. +3. Replay it through the verified primitives: + ``` + FOUNDRY_PROFILE=checker forge test --match-test testVerifyCertificate + ``` + [`Checker.sol`](checker/Checker.sol) reads `certificate.json`, rebuilds the tree via `OfferTree.newLeaf`/`newInternalNode`, and asserts the constructed root equals `root`. + +A passing run certifies that the root is the root of a well-formed tree built from exactly those offers, so the membership guarantee applies to it. +This confirms what a root commits to, not that it was signed; verifying the ratifier's signature is a separate step. + +The verification setup and technique is inspired from the Merkle Tree Membership soundness spec in [Universal Rewards Distributor](https://github.com/morpho-org/universal-rewards-distributor/). + ## Fees Continuous-fee accrual and settlement-fee rounding stay within their expected bounds. diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol new file mode 100644 index 000000000..540308c9f --- /dev/null +++ b/certora/checker/Checker.sol @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association +pragma solidity ^0.8.0; + +import {Test} from "../../lib/forge-std/src/Test.sol"; +import {stdJson} from "../../lib/forge-std/src/StdJson.sol"; + +import {OfferTree} from "../helpers/OfferTree.sol"; +import {Offer} from "../../src/interfaces/IMidnight.sol"; +import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; + +contract Checker is Test { + using stdJson for string; + + struct InternalNode { + bytes32 id; + bytes32 left; + bytes32 right; + } + + // Replay the certificate through the verified `newLeaf` and `newInternalNode` + // primitives, then assert that the final certificate item matches `root`. + function testVerifyCertificate() public { + string memory path = string.concat(vm.projectRoot(), "/certificate.json"); + if (!vm.exists(path)) vm.skip(true, "no certificate.json at project root"); + + string memory json = vm.readFile(path); + bytes32 root = json.readBytes32(".root"); + + uint256 leafLength = json.readUint(".leafLength"); + Offer[] memory leaves = new Offer[](leafLength); + for (uint256 i = 0; i < leafLength; i++) { + bytes memory enc = json.readBytes(string.concat(".leaf[", vm.toString(i), "]")); + leaves[i] = abi.decode(enc, (Offer)); + } + + uint256 nodeLength = json.readUint(".nodeLength"); + InternalNode[] memory nodes = new InternalNode[](nodeLength); + for (uint256 i = 0; i < nodeLength; i++) { + bytes memory enc = json.readBytes(string.concat(".node[", vm.toString(i), "]")); + nodes[i] = abi.decode(enc, (InternalNode)); + } + + require(leaves.length > 0, "no leaves"); + require(nodes.length > 0 || leaves.length == 1, "missing internal nodes"); + + OfferTree tree = new OfferTree(); + + for (uint256 i = 0; i < leaves.length; i++) { + tree.newLeaf(leaves[i]); + } + + bytes32 rootId = HashLib.hashOffer(leaves[0]); + for (uint256 i = 0; i < nodes.length; i++) { + InternalNode memory node = nodes[i]; + tree.newInternalNode(node.id, node.left, node.right); + rootId = node.id; + } + + assertEq(tree.getHash(rootId), root, "mismatched roots"); + } +} diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py new file mode 100644 index 000000000..3b281a805 --- /dev/null +++ b/certora/checker/create_certificate.py @@ -0,0 +1,229 @@ +import json +import sys + +from eth_abi import encode +from web3 import Web3 + +w3 = Web3() + +COLLATERAL_PARAMS_TYPEHASH = bytes.fromhex( + "af44a88eb50ebdbbebd980e5a23045c44f61ece5f80ab708a1bbe8718102e6af" +) +MARKET_TYPEHASH = bytes.fromhex( + "358117e98511cc3df97175dca58053b06675b43ad090b0553f8a1eff008b6e2e" +) +OFFER_TYPEHASH = bytes.fromhex( + "980a4cfc9766df84667f316d76e10cefc8caf04fb4cd4a9fca00a8e7b34f619c" +) + +# ABI signature for `Offer` matching src/interfaces/IMidnight.sol field order. +OFFER_ABI_TYPE = ( + "(" + "(address,(address,uint256,uint256,address)[],uint256,uint256,address,address)," + "bool,address,uint256,uint256,uint256,bytes32,address,bytes,address,address,bool,uint256,uint256" + ")" +) +INTERNAL_NODE_ABI_TYPE = "(bytes32,bytes32,bytes32)" + + +# Safety checks use this instead of `assert`, which is stripped under `python -O`. +def _require(cond, msg): + if not cond: + raise ValueError(msg) + + +def _bytes32(v): + raw = bytes.fromhex(v.removeprefix("0x")) + _require(len(raw) == 32, f"expected 32 bytes, got {len(raw)}") + return raw + + +def _hexbytes(v): + return bytes.fromhex(v.removeprefix("0x")) + + +def _keccak_abi(types, values): + return w3.keccak(encode(types, values)) + + +# Returns the abi-encoded form of an Offer, ready for `abi.decode(bytes, (Offer))`. +def abi_encode_offer(o): + m = o["market"] + market = ( + w3.to_checksum_address(m["loanToken"]), + [ + ( + w3.to_checksum_address(cp["token"]), + int(cp["lltv"]), + int(cp["maxLif"]), + w3.to_checksum_address(cp["oracle"]), + ) + for cp in m["collateralParams"] + ], + int(m["maturity"]), + int(m["rcfThreshold"]), + w3.to_checksum_address(m["enterGate"]), + w3.to_checksum_address(m["liquidatorGate"]), + ) + offer = ( + market, + bool(o["buy"]), + w3.to_checksum_address(o["maker"]), + int(o["start"]), + int(o["expiry"]), + int(o["tick"]), + _bytes32(o["group"]), + w3.to_checksum_address(o["callback"]), + _hexbytes(o["callbackData"]), + w3.to_checksum_address(o["receiverIfMakerIsSeller"]), + w3.to_checksum_address(o["ratifier"]), + bool(o["reduceOnly"]), + int(o["maxUnits"]), + int(o["maxAssets"]), + ) + return "0x" + encode([OFFER_ABI_TYPE], [offer]).hex() + + +def abi_encode_node(node_id, left, right): + node = (_bytes32(node_id), _bytes32(left), _bytes32(right)) + return "0x" + encode([INTERNAL_NODE_ABI_TYPE], [node]).hex() + + +def hash_collateral_params(cp): + return _keccak_abi( + ["bytes32", "address", "uint256", "uint256", "address"], + [ + COLLATERAL_PARAMS_TYPEHASH, + w3.to_checksum_address(cp["token"]), + int(cp["lltv"]), + int(cp["maxLif"]), + w3.to_checksum_address(cp["oracle"]), + ], + ) + + +def hash_market(m): + collateral_params_hashes = b"".join( + hash_collateral_params(cp) for cp in m["collateralParams"] + ) + collateral_params_hash = w3.keccak(collateral_params_hashes) + return _keccak_abi( + ["bytes32", "address", "bytes32", "uint256", "uint256", "address", "address"], + [ + MARKET_TYPEHASH, + w3.to_checksum_address(m["loanToken"]), + collateral_params_hash, + int(m["maturity"]), + int(m["rcfThreshold"]), + w3.to_checksum_address(m["enterGate"]), + w3.to_checksum_address(m["liquidatorGate"]), + ], + ) + + +# Returns the hash of an offer (mirrors HashLib.hashOffer). +def hash_offer(o): + return w3.to_hex( + _keccak_abi( + [ + "bytes32", + "bytes32", + "bool", + "address", + "uint256", + "uint256", + "uint256", + "bytes32", + "address", + "bytes32", + "address", + "address", + "bool", + "uint256", + "uint256", + ], + [ + OFFER_TYPEHASH, + hash_market(o["market"]), + bool(o["buy"]), + w3.to_checksum_address(o["maker"]), + int(o["start"]), + int(o["expiry"]), + int(o["tick"]), + _bytes32(o["group"]), + w3.to_checksum_address(o["callback"]), + w3.keccak(_hexbytes(o["callbackData"])), + w3.to_checksum_address(o["receiverIfMakerIsSeller"]), + w3.to_checksum_address(o["ratifier"]), + bool(o["reduceOnly"]), + int(o["maxUnits"]), + int(o["maxAssets"]), + ], + ) + ) + + +# Returns the hash of a node given the hashes of its children. +def hash_node(left, right): + return w3.to_hex(w3.keccak(_bytes32(left) + _bytes32(right))) + + +# Builds a certificate from a power-of-two list of offers, in leftIndex order, by pairing +# leaves level-by-level into a perfect binary tree. +def build_certificate(leaves, claimed_root): + n = len(leaves) + _require(n > 0 and (n & (n - 1)) == 0, "leaves count must be a power of two") + + leaf_instructions = {} + node_instructions = {} + + level = [hash_offer(o) for o in leaves] + for leaf, leaf_hash in zip(leaves, level): + encoded_leaf = abi_encode_offer(leaf) + previous = leaf_instructions.setdefault(leaf_hash, encoded_leaf) + _require(previous == encoded_leaf, "leaf hash collides with a different offer") + + while len(level) > 1: + next_level = [] + for i in range(len(level) // 2): + left = level[2 * i] + right = level[2 * i + 1] + node_hash = hash_node(left, right) + _require(node_hash not in leaf_instructions, "internal node id collides with a leaf id") + encoded_node = abi_encode_node(node_hash, left, right) + previous = node_instructions.setdefault(node_hash, encoded_node) + _require(previous == encoded_node, "internal node id collides with different children") + next_level.append(node_hash) + level = next_level + + _require( + level[0].lower() == claimed_root.lower(), + f"computed root {level[0]} != claimed root {claimed_root}", + ) + + return { + "root": claimed_root, + "leafLength": len(leaf_instructions), + "leaf": list(leaf_instructions.values()), + "nodeLength": len(node_instructions), + "node": list(node_instructions.values()), + } + + +def main(): + if len(sys.argv) != 2: + print("usage: python create_certificate.py ", file=sys.stderr) + sys.exit(2) + + with open(sys.argv[1]) as f: + proofs = json.load(f) + + root = proofs["root"] + certificate = build_certificate([entry["offer"] for entry in proofs["leaves"]], root) + + with open("certificate.json", "w") as f: + json.dump(certificate, f, indent=2) + + +if __name__ == "__main__": + main() diff --git a/certora/confs/OfferTreeMembership.conf b/certora/confs/OfferTreeMembership.conf new file mode 100644 index 000000000..c00b1f1c8 --- /dev/null +++ b/certora/confs/OfferTreeMembership.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/Midnight.sol", + "certora/helpers/OfferTree.sol", + "certora/helpers/Utils.sol" + ], + "verify": "Midnight:certora/specs/OfferTreeMembership.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 3, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "rule_sanity": "basic", + "smt_timeout": 7200, + "prover_args": [ + "-splitParallel true", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" + ], + "msg": "Offer Tree Membership" +} diff --git a/certora/confs/OfferTreeWellFormed.conf b/certora/confs/OfferTreeWellFormed.conf new file mode 100644 index 000000000..d88336857 --- /dev/null +++ b/certora/confs/OfferTreeWellFormed.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "certora/helpers/OfferTree.sol" + ], + "verify": "OfferTree:certora/specs/OfferTreeWellFormed.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 3, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "rule_sanity": "basic", + "smt_timeout": 7200, + "prover_args": [ + "-splitParallel true", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" + ], + "msg": "OfferTreeWellFormed" +} diff --git a/certora/confs/Ratification.conf b/certora/confs/Ratification.conf index a8edd78fd..1a2010582 100644 --- a/certora/confs/Ratification.conf +++ b/certora/confs/Ratification.conf @@ -1,6 +1,13 @@ { "files": [ - "src/Midnight.sol" + "src/Midnight.sol", + "src/ratifiers/EcrecoverRatifier.sol", + "src/ratifiers/SetterRatifier.sol", + "certora/helpers/Utils.sol" + ], + "link": [ + "EcrecoverRatifier:MIDNIGHT=Midnight", + "SetterRatifier:MIDNIGHT=Midnight" ], "verify": "Midnight:certora/specs/Ratification.spec", "solc": "solc-0.8.34", diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol new file mode 100644 index 000000000..f25185128 --- /dev/null +++ b/certora/helpers/OfferTree.sol @@ -0,0 +1,182 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association +pragma solidity ^0.8.0; + +import {Offer} from "../../src/interfaces/IMidnight.sol"; +import {HashLib, OFFER_TYPEHASH} from "../../src/ratifiers/libraries/HashLib.sol"; + +// A leaf's offer reaches HashLib.hashOffer only through fixed-size fields: every dynamic member of Offer +// (market.collateralParams and callbackData) is already reduced to a single bytes32 before the final +// keccak (hashMarket(market) and keccak256(callbackData)). So we store that fixed-size pre-image instead +// of the raw Offer. This keeps every Node fixed-size, so isWellFormed re-hashes a leaf with one bounded +// keccak (no dynamic-array reads, no loops) — the property that lets the wellFormed invariant scale, exactly +// as it does for URD's fixed-size leaves. _hashLeaf mirrors hashOffer's outer keccak field-for-field, so a +// leaf's id is the real hashOffer value; the wellFormed invariant's newLeaf case checks this mirror holds +// (id == hashOffer(offer) and id == _hashLeaf(leaf)), so the correspondence is verified, not assumed. +struct Leaf { + bytes32 marketHash; // = HashLib.hashMarket(offer.market) + bool buy; + address maker; + uint256 start; + uint256 expiry; + uint256 tick; + bytes32 group; + address callback; + bytes32 callbackDataHash; // = keccak256(offer.callbackData) + address receiverIfMakerIsSeller; + address ratifier; + bool reduceOnly; + uint256 maxUnits; + uint256 maxAssets; +} + +contract OfferTree { + struct Node { + bytes32 left; + bytes32 right; + Leaf leaf; + // hash of the offer for leaves, and of [left.hash, right.hash] for internal nodes. + bytes32 hashNode; + } + + /* STORAGE */ + + // The tree has no root because every node (and the nodes underneath) form an offer tree. + // We use bytes32 as keys of the mapping so that leaves have an identifier that is the hash of the offer. + // Identical offers therefore share a single node (referenced by multiple parents). + // For internal nodes the key is left arbitrary, so that the certificate generation can choose freely any bytes32 + // value (that is not already used). + // Leaves keep the fixed-size pre-image of hashOffer (see Leaf) so isWellFormed can recompute a leaf's hash + // and pin its hashNode into the image of hashOffer. hashOffer and hashNode feed keccak distinct + // input shapes, this gives domain separation between leaves and internal nodes. The tree is built only via newLeaf + // and newInternalNode, which preserve well-formedness by construction. + mapping(bytes32 => Node) internal tree; + + /* MAIN FUNCTIONS */ + + function newLeaf(Offer memory offer) public { + bytes32 id = HashLib.hashOffer(offer); + require(id != 0, "id is the zero bytes"); + Node storage n = tree[id]; + require(_isEmpty(n), "leaf is not empty"); + // Store the fixed-size pre-image of hashOffer; the dynamic members are kept only as their sub-hashes. + Leaf storage l = n.leaf; + l.marketHash = HashLib.hashMarket(offer.market); + l.buy = offer.buy; + l.maker = offer.maker; + l.start = offer.start; + l.expiry = offer.expiry; + l.tick = offer.tick; + l.group = offer.group; + l.callback = offer.callback; + l.callbackDataHash = keccak256(offer.callbackData); + l.receiverIfMakerIsSeller = offer.receiverIfMakerIsSeller; + l.ratifier = offer.ratifier; + l.reduceOnly = offer.reduceOnly; + l.maxUnits = offer.maxUnits; + l.maxAssets = offer.maxAssets; + n.hashNode = id; + } + + function newInternalNode(bytes32 id, bytes32 left, bytes32 right) public { + require(id != 0, "zero id"); + Node storage n = tree[id]; + require(_isEmpty(n), "node already populated"); + bytes32 leftHash = tree[left].hashNode; + bytes32 rightHash = tree[right].hashNode; + require(leftHash != 0, "left empty"); + require(rightHash != 0, "right empty"); + n.left = left; + n.right = right; + n.hashNode = HashLib.hashNode(leftHash, rightHash); + } + + /* PURE AND VIEW FUNCTIONS */ + + function _isEmpty(Node storage n) internal view returns (bool) { + return n.left == 0 && n.right == 0 && n.hashNode == 0; + } + + function isEmpty(bytes32 id) public view returns (bool) { + return _isEmpty(tree[id]); + } + + function getHash(bytes32 id) public view returns (bytes32) { + return tree[id].hashNode; + } + + function isLeafNode(bytes32 id) public view returns (bool) { + return tree[id].left == 0 && tree[id].right == 0 && tree[id].hashNode != 0; + } + + function hashOffer(Offer memory offer) public pure returns (bytes32) { + return HashLib.hashOffer(offer); + } + + function hashNode(bytes32 left, bytes32 right) public pure returns (bytes32) { + return HashLib.hashNode(left, right); + } + + function _hashLeaf(bytes32 id) public view returns (bytes32) { + return _hashLeaf(tree[id].leaf); + } + + // Recompute the leaf hash from its stored fixed-size pre-image. Mirrors HashLib.hashOffer's outer keccak + // field-for-field, with marketHash standing in for hashMarket(market) and callbackDataHash for + // keccak256(callbackData). Equals HashLib.hashOffer(offer) whenever the fields were extracted from offer. + function _hashLeaf(Leaf storage l) internal view returns (bytes32) { + return keccak256( + abi.encode( + OFFER_TYPEHASH, + l.marketHash, + l.buy, + l.maker, + l.start, + l.expiry, + l.tick, + l.group, + l.callback, + l.callbackDataHash, + l.receiverIfMakerIsSeller, + l.ratifier, + l.reduceOnly, + l.maxUnits, + l.maxAssets + ) + ); + } + + // The specification of a well-formed tree is the following: + // - empty nodes are well-formed + // - leaves have the correct identifier and hashing + // - internal nodes have the correct hashing + // - internal nodes have exactly two non-empty children + function isWellFormed(bytes32 id) public view returns (bool) { + Node storage n = tree[id]; + if (_isEmpty(n)) return true; + if (n.left == 0 && n.right == 0) { + bytes32 expected = _hashLeaf(n.leaf); + return n.hashNode == expected && id == expected; + } + if (n.left != 0 && n.right != 0) { + bytes32 leftHash = tree[n.left].hashNode; + bytes32 rightHash = tree[n.right].hashNode; + return leftHash != 0 && rightHash != 0 && n.hashNode == HashLib.hashNode(leftHash, rightHash); + } + return false; + } + + // Check that the nodes are well-formed starting from id and going down the tree. + // The bits of leafIndex choose the path downward; the depth is proof.length. + function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view returns (bool) { + for (uint256 i = proof.length;;) { + require(isWellFormed(id)); + + if (i == 0) break; + + --i; + id = ((leafIndex >> i) & 1 == 0) ? tree[id].left : tree[id].right; + } + return true; + } +} diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index d61137ccf..e7014d595 100644 --- a/certora/helpers/Utils.sol +++ b/certora/helpers/Utils.sol @@ -4,6 +4,7 @@ pragma solidity ^0.8.0; import {Offer, Market} from "../../src/interfaces/IMidnight.sol"; import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; +import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; import { CALLBACK_SUCCESS, LIQUIDATION_CURSOR_LOW, @@ -14,7 +15,23 @@ import { contract Utils { function hashMarket(Market memory market) external pure returns (bytes32) { - return keccak256(abi.encode(market)); + return HashLib.hashMarket(market); + } + + // Wraps `HashLib.hashOffer` directly so CVL specs can expose the real EIP-712 offer hash + // envfree. Used by OfferTreeMembership.spec as the leaf id. A `keccak256(abi.encode(offer))` + // reimplementation would be a *different* hash (no typehash prefix, no inner hashing of + // market/callbackData), so we forward to the real library function. + function hashOffer(Offer memory offer) external pure returns (bytes32) { + return HashLib.hashOffer(offer); + } + + function isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) + external + pure + returns (bool) + { + return HashLib.isLeaf(root, leafHash, leafIndex, proof); } function getBit(uint128 bitmap, uint256 bit) external pure returns (bool) { diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec new file mode 100644 index 000000000..7256cdc43 --- /dev/null +++ b/certora/specs/OfferTreeMembership.spec @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +using OfferTree as OfferTree; +using Utils as Utils; + +methods { + function OfferTree.getHash(bytes32) external returns (bytes32) envfree; + function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; + function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bool) envfree; + function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; +} + +// Headline Correctness Rule: +// If the root is setup according to a well-formed offer tree, then a successful Merkle verification of an offer against that root implies the offer is registered as a leaf in the tree. +rule membershipSoundness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { + bytes32 node; + + require OfferTree.getHash(node) == root, "root is the hash of node"; + + require(OfferTree.wellFormedPath(node, leafIndex, proof), "the path from the root to the leaf is well-formed"); + + bytes32 leafId = Utils.hashOffer(offer); + + require Utils.isLeaf(root, leafId, leafIndex, proof), "Merkle proof verifies the offer"; + + assert OfferTree.isLeafNode(leafId); +} diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec new file mode 100644 index 000000000..0c87937e0 --- /dev/null +++ b/certora/specs/OfferTreeWellFormed.spec @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Leaves store the fixed-size pre-image of hashOffer (its static fields plus marketHash and callbackDataHash) +// instead of the raw Offer, so isWellFormed re-hashes a leaf with one bounded keccak (_hashLeaf) and the +// wellFormed proof stays bounded regardless of offer size (no dynamic-array loops, no dynamic-length hashing). +// hashLeafReproducesHashOffer justifies the trick: the stored pre-image re-hashes +// to the real hashOffer. leafHashDisjointFromNodeHash and nodeHashInjective record the two keccak-model +// properties (leaf/internal domain separation, hashNode injectivity) that OfferTreeMembership.spec relies on. + +methods { + function newLeaf(OfferTree.Offer) external envfree; + function _hashLeaf(bytes32) external returns (bytes32) envfree; + function hashOffer(OfferTree.Offer) external returns (bytes32) envfree; + function hashNode(bytes32, bytes32) external returns (bytes32) envfree; + function isEmpty(bytes32) external returns (bool) envfree; + function isWellFormed(bytes32) external returns (bool) envfree; +} + +// The zero node is empty, so it can serve as the canonical empty child of every node in the tree. +strong invariant zeroIsEmpty() + isEmpty(to_bytes32(0)); + +// Every node of the tree is well-formed, which is what makes the membership result in OfferTreeMembership.spec sound. +strong invariant wellFormed(bytes32 id) + isWellFormed(id) + { + preserved { + requireInvariant zeroIsEmpty(); + } + } + +// _hashLeaf reproduces the real hashOffer for the leaf stored by newLeaf. +// newLeaf is called without @withrevert, so its own guards (id != 0, slot empty) hold as assumptions. +rule hashLeafReproducesHashOffer(OfferTree.Offer offer) { + newLeaf(offer); + + bytes32 id = hashOffer(offer); + assert _hashLeaf(id) == id; +} + +// A recomputed leaf hash never equals an internal-node hash: image(_hashLeaf) and image(hashNode) are disjoint. +rule leafHashDisjointFromNodeHash(bytes32 id, bytes32 a, bytes32 b) { + assert _hashLeaf(id) != hashNode(a, b); +} + +// hashNode is injective, which the merkle peeling in OfferTreeMembership.spec relies on. +rule nodeHashInjective(bytes32 a, bytes32 b, bytes32 c, bytes32 d) { + require hashNode(a, b) == hashNode(c, d); + assert a == c && b == d; +} diff --git a/certora/specs/Ratification.spec b/certora/specs/Ratification.spec index 6ec782598..8ea872b2b 100644 --- a/certora/specs/Ratification.spec +++ b/certora/specs/Ratification.spec @@ -1,11 +1,27 @@ // SPDX-License-Identifier: GPL-2.0-or-later +using Utils as Utils; + methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function isAuthorized(address authorizer, address authorized) external returns (bool) envfree; - // Over-approximate view functions. + function Utils.callbackSuccess() external returns (bytes32) envfree; + + function _.isRatified(Midnight.Offer, bytes) external => DISPATCHER(true); + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.transfer(address, uint256) external => NONDET; + + // Capture HashLib.isLeaf's return; needed by `isRatifiedRequiresIsLeaf` to assert isRatified gates on a merkle check. + function HashLib.isLeaf(bytes32, bytes32, uint256, bytes32[] memory) internal returns (bool) => isLeafCapture(); + + function HashLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; + function HashLib.offerTreeTypeHash(uint256) internal returns (bytes32) => NONDET; + + // Summaries for internals irrelevant to ratification properties. function IdLib.toId(Midnight.Market memory, uint256, address) internal returns (bytes32) => NONDET; function UtilsLib.mulDivDown(uint256, uint256, uint256) internal returns (uint256) => NONDET; function UtilsLib.mulDivUp(uint256, uint256, uint256) internal returns (uint256) => NONDET; @@ -16,6 +32,18 @@ methods { function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; } +// Captures whether HashLib.isLeaf was called and returned true during the current rule. +// Used by `isRatifiedRequiresIsLeaf` to assert that every successful isRatified gates on a merkle check. +persistent ghost bool isLeafReturnedTrue; + +function isLeafCapture() returns bool { + bool ret; + if (ret) { + isLeafReturnedTrue = true; + } + return ret; +} + /// Every successful take requires the maker to have authorized the ratifier. rule takeRequiresMakerConsent(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData) { bool makerAuthorizedRatifier = isAuthorized(offer.maker, offer.ratifier); @@ -43,3 +71,22 @@ rule takeRequiresNonZeroMaker(env e, Midnight.Offer offer, bytes ratifierData, u take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); assert offer.maker != 0; } + +/// Every successful isRatified call implies HashLib.isLeaf was invoked and returned true. Verified by dispatch across all linked ratifier implementations. +rule isRatifiedRequiresIsLeaf(env e, address ratifierAddr, Midnight.Offer offer, bytes ratifierData) { + require !isLeafReturnedTrue, "fresh capture state"; + + bytes32 result = ratifierAddr.isRatified(e, offer, ratifierData); + require result == Utils.callbackSuccess(), "isRatified succeeded"; + + assert isLeafReturnedTrue, "ratifier must have called HashLib.isLeaf that returned true"; +} + +/// Every successful Midnight.take implies HashLib.isLeaf was invoked and returned true. +rule takeRequiresIsLeaf(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData) { + require !isLeafReturnedTrue, "fresh capture state"; + + take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + + assert isLeafReturnedTrue, "take must have triggered a ratifier that called HashLib.isLeaf returning true"; +} diff --git a/foundry.toml b/foundry.toml index 1c268f0fd..5785fec1f 100644 --- a/foundry.toml +++ b/foundry.toml @@ -9,6 +9,11 @@ fs_permissions = [{ access = "read", path = "test/ticks_exact.json" }] [profile.default.fmt] wrap_comments = true +[profile.checker] +test = "certora/checker" +match_contract = "Checker" +fs_permissions = [{ access = "read", path = "./" }] + [lint] exclude_lints = [ "asm-keccak256",