From 21739ee96391488c004995be2599fac4ef10396a Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 7 May 2026 10:46:33 +0200 Subject: [PATCH 01/38] added rules inspired form URD --- certora/confs/OfferTreeWellFormed.conf | 20 +++++ certora/confs/TakeCorrectness.conf | 21 +++++ certora/helpers/OfferTree.sol | 110 +++++++++++++++++++++++++ certora/specs/OfferTreeWellFormed.spec | 24 ++++++ certora/specs/TakeCorrectness.spec | 78 ++++++++++++++++++ 5 files changed, 253 insertions(+) create mode 100644 certora/confs/OfferTreeWellFormed.conf create mode 100644 certora/confs/TakeCorrectness.conf create mode 100644 certora/helpers/OfferTree.sol create mode 100644 certora/specs/OfferTreeWellFormed.spec create mode 100644 certora/specs/TakeCorrectness.spec 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/TakeCorrectness.conf b/certora/confs/TakeCorrectness.conf new file mode 100644 index 000000000..bbb860179 --- /dev/null +++ b/certora/confs/TakeCorrectness.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "src/Midnight.sol", + "certora/helpers/OfferTree.sol" + ], + "verify": "Midnight:certora/specs/TakeCorrectness.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": "TakeCorrectness" +} diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol new file mode 100644 index 000000000..98e2df7d1 --- /dev/null +++ b/certora/helpers/OfferTree.sol @@ -0,0 +1,110 @@ +// 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 {UtilsLib} from "../../src/libraries/UtilsLib.sol"; + +/// @dev Ghost offer-tree helper used by Certora specs. +/// @dev Trees are built only via `newLeaf` and `newInternalNode`, which preserve the +/// well-formedness invariant by construction. The verified invariant is then used +/// to prove that any successful `take` against a Midnight signed root corresponds +/// to a leaf actually present in the maker's tree. +contract OfferTree { + struct Node { + bytes32 left; + bytes32 right; + bytes32 hashNode; + bool isLeaf; + } + + mapping(bytes32 => Node) internal tree; + + function newLeaf(Offer memory offer) public { + bytes32 h = UtilsLib.hashOffer(offer); + require(h != 0, "zero leaf hash"); + Node storage n = tree[h]; + require(_isEmpty(n), "leaf already populated"); + n.hashNode = h; + n.isLeaf = true; + } + + 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"); + Node storage L = tree[left]; + Node storage R = tree[right]; + require(!_isEmpty(L), "left empty"); + require(!_isEmpty(R), "right empty"); + require(L.hashNode <= R.hashNode, "children not pair-sorted"); + n.left = left; + n.right = right; + n.hashNode = UtilsLib.commutativeHash(L.hashNode, R.hashNode); + } + + function _isEmpty(Node storage n) internal view returns (bool) { + return n.left == 0 && n.right == 0 && n.hashNode == 0 && !n.isLeaf; + } + + 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].isLeaf; + } + + function getLeft(bytes32 id) public view returns (bytes32) { + return tree[id].left; + } + + function getRight(bytes32 id) public view returns (bytes32) { + return tree[id].right; + } + + function hashOffer(Offer memory offer) external pure returns (bytes32) { + return UtilsLib.hashOffer(offer); + } + + /// @dev Well-formed predicate. + /// @dev Empty nodes well-formed; leaves have id == hashNode and no children; + /// internal nodes have non-empty children, pair-sorted hashes, and + /// hashNode = commutativeHash(left.hashNode, right.hashNode). + function isWellFormed(bytes32 id) public view returns (bool) { + Node storage n = tree[id]; + if (_isEmpty(n)) return true; + if (n.isLeaf) { + return n.left == 0 && n.right == 0 && n.hashNode == id && n.hashNode != 0; + } else { + if (n.left == 0 || n.right == 0) return false; + Node storage L = tree[n.left]; + Node storage R = tree[n.right]; + return !_isEmpty(L) && !_isEmpty(R) && L.hashNode <= R.hashNode + && n.hashNode == UtilsLib.commutativeHash(L.hashNode, R.hashNode); + } + } + + /// @dev Walks down the tree from `id`, consuming `proof` from end to start, + /// asserting every visited node is well-formed. + /// @dev At each step, descends into the child whose hash differs from the sibling + /// hash supplied in the proof. Mirrors the upward fold in `UtilsLib.isLeaf`. + function wellFormedPath(bytes32 id, bytes32[] memory proof) public view { + for (uint256 i = proof.length;;) { + require(isWellFormed(id)); + + if (i == 0) break; + + bytes32 sibling = proof[--i]; + + bytes32 left = tree[id].left; + bytes32 right = tree[id].right; + + id = getHash(left) == sibling ? right : left; + } + } +} diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec new file mode 100644 index 000000000..f9bcef713 --- /dev/null +++ b/certora/specs/OfferTreeWellFormed.spec @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association + +// Rule A — Well-formed offer-tree invariant. +// +// Verifies that the helper's only mutators (`newLeaf`, `newInternalNode`) +// preserve `isWellFormed` for every node id. This justifies using the helper +// as a ghost tree to reason about Midnight's runtime merkle verification. + +methods { + function isEmpty(bytes32) external returns (bool) envfree; + function isWellFormed(bytes32) external returns (bool) envfree; +} + +invariant zeroIsEmpty() + isEmpty(to_bytes32(0)); + +invariant wellFormed(bytes32 id) + isWellFormed(id) + { + preserved { + requireInvariant zeroIsEmpty(); + } + } diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec new file mode 100644 index 000000000..a17a7d9a8 --- /dev/null +++ b/certora/specs/TakeCorrectness.spec @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association + +// Rule B — Take correctness against the ghost offer-tree. +// +// Statement: if the maker's signed root corresponds to a node `node` of a +// well-formed ghost offer-tree, and the supplied proof descends through +// well-formed nodes from `node`, then any successful `take` against +// `(offer, root, proof)` implies `hashOffer(offer)` is registered as a +// leaf in the ghost tree (i.e. the offer was actually committed by the +// maker, not forged via second-preimage). +// +// The well-formed invariant on the ghost tree is established by Rule A +// (see OfferTreeWellFormed.spec). + +using OfferTree as OfferTree; + +methods { + function OfferTree.getHash(bytes32) external returns (bytes32) envfree; + function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; + function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; + function OfferTree.wellFormedPath(bytes32, bytes32[]) external envfree; + function OfferTree.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + + // Real semantics required for hashOffer / isLeaf / commutativeHash: + // these are the functions whose interaction with the ghost tree we are + // verifying. Do NOT summarize. + + // Summarize internals irrelevant to the merkle/hash linkage. + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function _.price() external => NONDET; + function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; + function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.transfer(address, uint256) external => NONDET; + + function IdLib.toId(Midnight.Obligation 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; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function Midnight.isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; + function Midnight.tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; +} + +/// Marquee rule: a successful take implies the offer's hash is a leaf of the +/// well-formed ghost tree pointed to by `root`. +rule takeCorrectness( + env e, + uint256 units, + address taker, + address takerCallback, + bytes takerCallbackData, + address receiverIfTakerIsSeller, + Midnight.Offer offer, + bytes ratifierData, + bytes32 root, + bytes32[] proof +) { + bytes32 node; + + // Root is the hash of some node in the ghost tree. + require OfferTree.getHash(node) == root; + require root != to_bytes32(0); + + // The proof descends through well-formed nodes from that node. + OfferTree.wellFormedPath(node, proof); + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData, root, proof); + + // The offer's hash is registered as a leaf in the ghost tree. + bytes32 leafId = OfferTree.hashOffer(offer); + assert OfferTree.isLeafNode(leafId); + assert OfferTree.getHash(leafId) == leafId; +} From 030c17544ea2c3642d1b94cad2866a5aad10f601 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 7 May 2026 15:31:01 +0200 Subject: [PATCH 02/38] tuned --- certora/confs/TakeCorrectness.conf | 3 +- certora/helpers/OfferTree.sol | 34 +++++++++++++------ certora/helpers/Utils.sol | 4 +++ certora/specs/TakeCorrectness.spec | 54 +++++++++++++++++++++++++++--- 4 files changed, 78 insertions(+), 17 deletions(-) diff --git a/certora/confs/TakeCorrectness.conf b/certora/confs/TakeCorrectness.conf index bbb860179..13e5f2ff9 100644 --- a/certora/confs/TakeCorrectness.conf +++ b/certora/confs/TakeCorrectness.conf @@ -1,7 +1,8 @@ { "files": [ "src/Midnight.sol", - "certora/helpers/OfferTree.sol" + "certora/helpers/OfferTree.sol", + "certora/helpers/Utils.sol" ], "verify": "Midnight:certora/specs/TakeCorrectness.spec", "solc": "solc-0.8.34", diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 98e2df7d1..1b08014d3 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -2,7 +2,6 @@ // Copyright (c) 2025 Morpho Association pragma solidity ^0.8.0; -import {Offer} from "../../src/interfaces/IMidnight.sol"; import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; /// @dev Ghost offer-tree helper used by Certora specs. @@ -10,6 +9,10 @@ import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; /// well-formedness invariant by construction. The verified invariant is then used /// to prove that any successful `take` against a Midnight signed root corresponds /// to a leaf actually present in the maker's tree. +/// @dev Purely structural: the helper does not encode the Offer struct itself, so it +/// avoids triggering pointer-analysis failures on `Offer.obligation.collateralParams[]`. +/// Specs supply leaf hashes externally (computed via the spec's chosen hashOffer +/// summary) and assert structural well-formedness here. contract OfferTree { struct Node { bytes32 left; @@ -20,12 +23,11 @@ contract OfferTree { mapping(bytes32 => Node) internal tree; - function newLeaf(Offer memory offer) public { - bytes32 h = UtilsLib.hashOffer(offer); - require(h != 0, "zero leaf hash"); - Node storage n = tree[h]; + function newLeaf(bytes32 leafHash) public { + require(leafHash != 0, "zero leaf hash"); + Node storage n = tree[leafHash]; require(_isEmpty(n), "leaf already populated"); - n.hashNode = h; + n.hashNode = leafHash; n.isLeaf = true; } @@ -67,10 +69,6 @@ contract OfferTree { return tree[id].right; } - function hashOffer(Offer memory offer) external pure returns (bytes32) { - return UtilsLib.hashOffer(offer); - } - /// @dev Well-formed predicate. /// @dev Empty nodes well-formed; leaves have id == hashNode and no children; /// internal nodes have non-empty children, pair-sorted hashes, and @@ -90,9 +88,15 @@ contract OfferTree { } /// @dev Walks down the tree from `id`, consuming `proof` from end to start, - /// asserting every visited node is well-formed. + /// asserting every visited node is well-formed AND that the path terminates + /// at a leaf. /// @dev At each step, descends into the child whose hash differs from the sibling /// hash supplied in the proof. Mirrors the upward fold in `UtilsLib.isLeaf`. + /// @dev The leaf-termination requirement encodes the assumption that `proof.length` + /// matches the actual depth from `id` to a leaf. The on-chain `take` does NOT + /// enforce this (it accepts any proof length whose folded hash equals root) — + /// the gap is intentional in the contract and is exposed by `takeCorrectness` + /// failing if this requirement is dropped. function wellFormedPath(bytes32 id, bytes32[] memory proof) public view { for (uint256 i = proof.length;;) { require(isWellFormed(id)); @@ -104,7 +108,15 @@ contract OfferTree { bytes32 left = tree[id].left; bytes32 right = tree[id].right; + // Sibling must equal exactly one of the children's hashes. Without this, + // the downward walk and the upward fold in `UtilsLib.isLeaf` can diverge + // below the root, even though they agree on the root value: the fold + // produces a synthetic intermediate hash unrelated to actual tree nodes, + // and the spec's leaf-membership conclusion would not follow. + require(getHash(left) == sibling || getHash(right) == sibling); + id = getHash(left) == sibling ? right : left; } + require(tree[id].isLeaf); } } diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index 977cccc3d..641afb193 100644 --- a/certora/helpers/Utils.sol +++ b/certora/helpers/Utils.sol @@ -12,6 +12,10 @@ contract Utils { return keccak256(abi.encode(obligation)); } + function hashOffer(Offer memory offer) external pure returns (bytes32) { + return keccak256(abi.encode(offer)); + } + function getBit(uint128 bitmap, uint256 bit) external pure returns (bool) { return bitmap & (1 << bit) != 0; } diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index a17a7d9a8..d8e2b3f54 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -12,19 +12,44 @@ // // The well-formed invariant on the ghost tree is established by Rule A // (see OfferTreeWellFormed.spec). +// +// `UtilsLib.hashOffer` is summarized to `Utils.hashOffer`, which uses +// `keccak256(abi.encode(offer))`. This deviates from the contract's actual +// EIP-712 encoding but is sound for this rule because: +// 1. determinism is preserved across the contract call inside `take` and +// the helper-side leaf hash; +// 2. injectivity assumed via `optimistic_hashing`; +// 3. the rule reasons about the hash purely as an opaque commitment — +// its specific bit pattern doesn't matter, only that it is the same +// function on both sides. 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.isWellFormed(bytes32) external returns (bool) envfree; function OfferTree.wellFormedPath(bytes32, bytes32[]) external envfree; - function OfferTree.hashOffer(Midnight.Offer) external returns (bytes32) envfree; - // Real semantics required for hashOffer / isLeaf / commutativeHash: - // these are the functions whose interaction with the ghost tree we are - // verifying. Do NOT summarize. + function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + + // Deterministic summary of UtilsLib.hashOffer so the contract and the spec + // agree on the leaf-hash function. Unsummarized, the via-ir lowering of the + // nested Offer.obligation.collateralParams[] loop blocks the prover's + // pointer/memory analysis. + function UtilsLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => + summaryHashOffer(offer); + + // Deterministic + symmetric + injective summary of UtilsLib.commutativeHash. + // The function uses inline assembly which the prover treats as a black box + // without injectivity, allowing CEXes where the upward fold (in `take`) + // and the downward walk (in `wellFormedPath`) produce the same root from + // structurally distinct intermediate hashes. The ghost axioms below enforce + // sorted-pair determinism and injectivity, matching keccak256's actual + // behavior on 64-byte inputs. + function UtilsLib.commutativeHash(bytes32 a, bytes32 b) internal returns (bytes32) => + summaryCommutativeHash(a, b); // Summarize internals irrelevant to the merkle/hash linkage. function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -42,10 +67,29 @@ methods { function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function TickLib.wExp(int256) internal returns (uint256) => NONDET; function Midnight.isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; function Midnight.tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; } +function summaryHashOffer(Midnight.Offer offer) returns bytes32 { + return Utils.hashOffer(offer); +} + +persistent ghost ghostCommutativeHash(bytes32, bytes32) returns bytes32 { + // Symmetric in its arguments. + axiom forall bytes32 a. forall bytes32 b. + ghostCommutativeHash(a, b) == ghostCommutativeHash(b, a); + // Injective on unordered pairs: equal hashes imply equal unordered inputs. + axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. + ghostCommutativeHash(a1, b1) == ghostCommutativeHash(a2, b2) + => ((a1 == a2 && b1 == b2) || (a1 == b2 && b1 == a2)); +} + +function summaryCommutativeHash(bytes32 a, bytes32 b) returns bytes32 { + return ghostCommutativeHash(a, b); +} + /// Marquee rule: a successful take implies the offer's hash is a leaf of the /// well-formed ghost tree pointed to by `root`. rule takeCorrectness( @@ -72,7 +116,7 @@ rule takeCorrectness( take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData, root, proof); // The offer's hash is registered as a leaf in the ghost tree. - bytes32 leafId = OfferTree.hashOffer(offer); + bytes32 leafId = Utils.hashOffer(offer); assert OfferTree.isLeafNode(leafId); assert OfferTree.getHash(leafId) == leafId; } From 4898d7200af5c9dbaf3037ed6fc7574b1d5903f1 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 17:10:23 +0200 Subject: [PATCH 03/38] take correctness passes; added some diagnostic tests --- certora/helpers/OfferTree.sol | 65 ++++++---- certora/helpers/Utils.sol | 9 ++ certora/specs/TakeCorrectness.spec | 185 ++++++++++++++++++----------- 3 files changed, 168 insertions(+), 91 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 1b08014d3..25a2b6103 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -2,17 +2,20 @@ // Copyright (c) 2025 Morpho Association pragma solidity ^0.8.0; -import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; +import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; /// @dev Ghost offer-tree helper used by Certora specs. /// @dev Trees are built only via `newLeaf` and `newInternalNode`, which preserve the /// well-formedness invariant by construction. The verified invariant is then used -/// to prove that any successful `take` against a Midnight signed root corresponds -/// to a leaf actually present in the maker's tree. +/// to prove that any successful merkle proof verification against a Midnight +/// ratified root corresponds to a leaf actually present in the maker's tree. /// @dev Purely structural: the helper does not encode the Offer struct itself, so it -/// avoids triggering pointer-analysis failures on `Offer.obligation.collateralParams[]`. +/// avoids triggering pointer-analysis failures on `Offer.market.collateralParams[]`. /// Specs supply leaf hashes externally (computed via the spec's chosen hashOffer /// summary) and assert structural well-formedness here. +/// @dev Mirrors the post-merge `HashLib.isLeaf` proof scheme: internal nodes have +/// directional left/right children combined via `HashLib.hashNode`, and the +/// downward walk in `wellFormedPath` follows the bits of `leafIndex`. contract OfferTree { struct Node { bytes32 left; @@ -39,10 +42,9 @@ contract OfferTree { Node storage R = tree[right]; require(!_isEmpty(L), "left empty"); require(!_isEmpty(R), "right empty"); - require(L.hashNode <= R.hashNode, "children not pair-sorted"); n.left = left; n.right = right; - n.hashNode = UtilsLib.commutativeHash(L.hashNode, R.hashNode); + n.hashNode = HashLib.hashNode(L.hashNode, R.hashNode); } function _isEmpty(Node storage n) internal view returns (bool) { @@ -71,8 +73,7 @@ contract OfferTree { /// @dev Well-formed predicate. /// @dev Empty nodes well-formed; leaves have id == hashNode and no children; - /// internal nodes have non-empty children, pair-sorted hashes, and - /// hashNode = commutativeHash(left.hashNode, right.hashNode). + /// internal nodes have non-empty children and hashNode = hashNode(left.hashNode, right.hashNode). function isWellFormed(bytes32 id) public view returns (bool) { Node storage n = tree[id]; if (_isEmpty(n)) return true; @@ -82,40 +83,58 @@ contract OfferTree { if (n.left == 0 || n.right == 0) return false; Node storage L = tree[n.left]; Node storage R = tree[n.right]; - return !_isEmpty(L) && !_isEmpty(R) && L.hashNode <= R.hashNode - && n.hashNode == UtilsLib.commutativeHash(L.hashNode, R.hashNode); + return !_isEmpty(L) && !_isEmpty(R) + && n.hashNode == HashLib.hashNode(L.hashNode, R.hashNode); } } /// @dev Walks down the tree from `id`, consuming `proof` from end to start, /// asserting every visited node is well-formed AND that the path terminates /// at a leaf. - /// @dev At each step, descends into the child whose hash differs from the sibling - /// hash supplied in the proof. Mirrors the upward fold in `UtilsLib.isLeaf`. + /// @dev At each level, the bit of `leafIndex` decides which side the leaf descends to, + /// mirroring the upward fold in `HashLib.isLeaf`: + /// bit == 0 ⇒ leaf was on the LEFT (sibling is the right child). + /// bit == 1 ⇒ leaf was on the RIGHT (sibling is the left child). /// @dev The leaf-termination requirement encodes the assumption that `proof.length` - /// matches the actual depth from `id` to a leaf. The on-chain `take` does NOT - /// enforce this (it accepts any proof length whose folded hash equals root) — + /// matches the actual depth from `id` to a leaf. The on-chain `HashLib.isLeaf` does + /// NOT enforce this (it accepts any proof length whose folded hash equals root) — /// the gap is intentional in the contract and is exposed by `takeCorrectness` /// failing if this requirement is dropped. - function wellFormedPath(bytes32 id, bytes32[] memory proof) public view { + function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view { + require(leafIndex >> proof.length == 0, "leaf index out of range"); for (uint256 i = proof.length;;) { require(isWellFormed(id)); if (i == 0) break; + // If we still have proof elements to consume, the current node must be an + // internal node, not a leaf. Without this, the prover can pick a leaf as the + // starting node — `isWellFormed` accepts it via the leaf branch, the loop + // walks off the leaf's zero children into the unrelated `tree[0]` entry, and + // the well-formedness chain that should pin `hashOffer(offer)` to a leaf in + // this subtree is never established, since the leaf branch of `isWellFormed` + // generates no `hashNode(L.hashNode, R.hashNode)` equation tying the root + // hash to the merkle fold. + require(!tree[id].isLeaf); + bytes32 sibling = proof[--i]; bytes32 left = tree[id].left; bytes32 right = tree[id].right; - // Sibling must equal exactly one of the children's hashes. Without this, - // the downward walk and the upward fold in `UtilsLib.isLeaf` can diverge - // below the root, even though they agree on the root value: the fold - // produces a synthetic intermediate hash unrelated to actual tree nodes, - // and the spec's leaf-membership conclusion would not follow. - require(getHash(left) == sibling || getHash(right) == sibling); - - id = getHash(left) == sibling ? right : left; + // The sibling supplied by the proof must equal the corresponding child's + // stored hash. Without this, the downward walk and the upward fold in + // `HashLib.isLeaf` can diverge below the root, even though they agree on + // the root value: the fold produces a synthetic intermediate hash unrelated + // to actual tree nodes, and the spec's leaf-membership conclusion would not + // follow. + if ((leafIndex >> i) & 1 == 0) { + require(getHash(right) == sibling); + id = left; + } else { + require(getHash(left) == sibling); + id = right; + } } require(tree[id].isLeaf); } diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index c66abb9c9..c8dabebcf 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, @@ -21,6 +22,14 @@ contract Utils { return keccak256(abi.encode(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) { return bitmap & (1 << bit) != 0; } diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index d8e2b3f54..f5b39d208 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -3,21 +3,30 @@ // Rule B — Take correctness against the ghost offer-tree. // -// Statement: if the maker's signed root corresponds to a node `node` of a -// well-formed ghost offer-tree, and the supplied proof descends through -// well-formed nodes from `node`, then any successful `take` against -// `(offer, root, proof)` implies `hashOffer(offer)` is registered as a -// leaf in the ghost tree (i.e. the offer was actually committed by the -// maker, not forged via second-preimage). +// Statement: if a maker-ratified root corresponds to a node `node` of a +// well-formed ghost offer-tree, and the supplied `(leafIndex, proof)` descends +// through well-formed nodes from `node`, then a successful merkle proof +// verification (`HashLib.isLeaf`) of `hashOffer(offer)` against that root +// implies the offer is registered as a leaf in the ghost tree (i.e. the offer +// was actually committed by the maker, not forged via second-preimage). // // The well-formed invariant on the ghost tree is established by Rule A // (see OfferTreeWellFormed.spec). // -// `UtilsLib.hashOffer` is summarized to `Utils.hashOffer`, which uses +// Architectural note (post-main merge): the merkle proof verification has +// moved out of `Midnight.take` and into the ratifier contracts +// (SetterRatifier / EcrecoverRatifier), which call `HashLib.isLeaf` after +// abi-decoding `(root, leafIndex, proof)` from `ratifierData`. The chain +// `successful take ⇒ successful isRatified` is established by +// Ratification.spec (takeRequiresMakerConsent); this rule covers the remaining +// link `successful isLeaf ⇒ leaf in tree`. Composed, the original +// take-level statement still holds. +// +// `HashLib.hashOffer` is summarized to `Utils.hashOffer`, which uses // `keccak256(abi.encode(offer))`. This deviates from the contract's actual // EIP-712 encoding but is sound for this rule because: -// 1. determinism is preserved across the contract call inside `take` and -// the helper-side leaf hash; +// 1. determinism is preserved across the merkle verification and the +// helper-side leaf hash; // 2. injectivity assumed via `optimistic_hashing`; // 3. the rule reasons about the hash purely as an opaque commitment — // its specific bit pattern doesn't matter, only that it is the same @@ -30,80 +39,107 @@ methods { function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; - function OfferTree.wellFormedPath(bytes32, bytes32[]) external envfree; + function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external envfree; function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - // Deterministic summary of UtilsLib.hashOffer so the contract and the spec - // agree on the leaf-hash function. Unsummarized, the via-ir lowering of the - // nested Offer.obligation.collateralParams[] loop blocks the prover's + // Deterministic summary of HashLib.hashOffer so the merkle verification + // (via Utils.isLeaf → HashLib.isLeaf → HashLib.hashNode) and the helper-side + // leaf hash agree on the leaf-hash function. Unsummarized, the via-ir lowering + // of the nested Offer.market.collateralParams[] loop blocks the prover's // pointer/memory analysis. - function UtilsLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => + function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - // Deterministic + symmetric + injective summary of UtilsLib.commutativeHash. - // The function uses inline assembly which the prover treats as a black box - // without injectivity, allowing CEXes where the upward fold (in `take`) - // and the downward walk (in `wellFormedPath`) produce the same root from - // structurally distinct intermediate hashes. The ghost axioms below enforce - // sorted-pair determinism and injectivity, matching keccak256's actual - // behavior on 64-byte inputs. - function UtilsLib.commutativeHash(bytes32 a, bytes32 b) internal returns (bytes32) => - summaryCommutativeHash(a, b); - - // Summarize internals irrelevant to the merkle/hash linkage. - function multicall(bytes[]) external => HAVOC_ALL DELETE; - - function _.price() external => NONDET; - function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; - function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; - function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; - function _.transferFrom(address, address, uint256) external => NONDET; - function _.transfer(address, uint256) external => NONDET; - - function IdLib.toId(Midnight.Obligation 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; - function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; - function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; - function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; - function TickLib.wExp(int256) internal returns (uint256) => NONDET; - function Midnight.isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET; - function Midnight.tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; + // Deterministic + injective summary of HashLib.hashNode. The function uses + // inline assembly which the prover treats as a black box without injectivity, + // allowing CEXes where the upward fold (in `HashLib.isLeaf`) and the downward + // walk (in `wellFormedPath`) produce the same root from structurally distinct + // intermediate hashes. The ghost axiom below enforces ordered-pair injectivity, + // matching keccak256's actual behavior on 64-byte inputs. + function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => + summaryHashNode(a, b); } function summaryHashOffer(Midnight.Offer offer) returns bytes32 { return Utils.hashOffer(offer); } -persistent ghost ghostCommutativeHash(bytes32, bytes32) returns bytes32 { - // Symmetric in its arguments. - axiom forall bytes32 a. forall bytes32 b. - ghostCommutativeHash(a, b) == ghostCommutativeHash(b, a); - // Injective on unordered pairs: equal hashes imply equal unordered inputs. +persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { + // Injective on ordered pairs: equal hashes imply equal ordered inputs. axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. - ghostCommutativeHash(a1, b1) == ghostCommutativeHash(a2, b2) - => ((a1 == a2 && b1 == b2) || (a1 == b2 && b1 == a2)); + ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); +} + +function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { + return ghostHashNode(a, b); +} + +// --------------------------------------------------------------------------- +// Diagnostic rules — isolate whether Z3 can use the implication-form +// injectivity axiom on `ghostHashNode`. They do not exercise storage, +// `wellFormedPath`, or `hashOffer`; they only put `ghostHashNode` applications +// in front of the solver and ask it to derive the consequent of the axiom. +// +// If `diagInjectivityOneStep` fails: the axiom is unusable even at one level. +// If `diagInjectivityOneStep` passes but `diagInjectivityTwoStep` fails: the +// solver instantiates the axiom for ground arguments but does not chain +// through a compound `ghostHashNode(...)` sub-term — which is the chain +// structure `takeCorrectness` requires. +// --------------------------------------------------------------------------- + +rule diagInjectivityOneStep(bytes32 a1, bytes32 b1, bytes32 a2, bytes32 b2) { + require ghostHashNode(a1, b1) == ghostHashNode(a2, b2); + assert a1 == a2; + assert b1 == b2; } -function summaryCommutativeHash(bytes32 a, bytes32 b) returns bytes32 { - return ghostCommutativeHash(a, b); +rule diagInjectivityTwoStep(bytes32 sib0, bytes32 sib1, bytes32 leaf1, bytes32 leaf2) { + require ghostHashNode(ghostHashNode(sib0, leaf1), sib1) + == ghostHashNode(ghostHashNode(sib0, leaf2), sib1); + assert leaf1 == leaf2; } -/// Marquee rule: a successful take implies the offer's hash is a leaf of the -/// well-formed ghost tree pointed to by `root`. -rule takeCorrectness( - env e, - uint256 units, - address taker, - address takerCallback, - bytes takerCallbackData, - address receiverIfTakerIsSeller, - Midnight.Offer offer, - bytes ratifierData, +// Tests pure EUF substitution: combine an equation about a storage-derived +// `intermediate` with an equation about `ghostHashNode` applications, and ask +// Z3 to apply two-step injectivity through the substitution. If this passes, +// the SMT layer handles the substitution and the `takeCorrectness` bug must +// be in how `wellFormedPath` establishes its constraints (or in storage +// aliasing across the `wellFormedPath`/`Utils.isLeaf` boundary). If it fails, +// the axiom shape itself can't close this chain even when stated as plain +// SMT facts, and the axiom needs strengthening. +rule diagSubstitution( bytes32 root, - bytes32[] proof + bytes32 sib0, + bytes32 sib1, + bytes32 D, + bytes32 leafHash, + bytes32 intermediate ) { + require ghostHashNode(intermediate, sib1) == root; + require intermediate == ghostHashNode(sib0, D); + require ghostHashNode(ghostHashNode(sib0, leafHash), sib1) == root; + assert D == leafHash; +} + +// Mirrors `takeCorrectness` but replaces the `hashOffer`-derived `leafId` with a +// free bytes32. If this passes: `hashOffer` (the offer-encoding side) is part +// of the problem. If it fails with the same shape: the failure lives entirely +// in the `wellFormedPath` + `Utils.isLeaf` composition through OfferTree +// storage, independent of how `leafHash` got there. +rule diagTakeCorrectnessFreeLeaf(bytes32 root, uint256 leafIndex, bytes32[] proof, bytes32 leafHash) { + bytes32 node; + require OfferTree.getHash(node) == root; + require root != to_bytes32(0); + OfferTree.wellFormedPath(node, leafIndex, proof); + require Utils.isLeaf(root, leafHash, leafIndex, proof); + assert OfferTree.isLeafNode(leafHash); +} + +/// Marquee rule: a successful merkle verification implies the offer's hash is a +/// leaf of the well-formed ghost tree pointed to by `root`. +rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; // Root is the hash of some node in the ghost tree. @@ -111,12 +147,25 @@ rule takeCorrectness( require root != to_bytes32(0); // The proof descends through well-formed nodes from that node. - OfferTree.wellFormedPath(node, proof); + OfferTree.wellFormedPath(node, leafIndex, proof); + + // Compute the offer's leaf hash once and reuse the symbolic value below. + // Two syntactic `Utils.hashOffer(offer)` sites would each lower to + // `keccak256(abi.encode(offer))` over freshly-materialized `bytes memory`; + // the prover's hashing model only treats keccak as injective on + // byte-equal inputs, and the `Offer.market.collateralParams[]` nested + // dynamic array (the same pointer/memory analysis limitation that + // motivates the `HashLib.hashOffer` summary above) blocks proving the + // two encoded buffers identical. The merkle-fold side and the + // assertion side could then bind to different symbolic hashes, yielding + // a spurious CEX where the upward fold pins one hash to a leaf in the + // ghost tree but the assertion reads a different hash that isn't. + bytes32 leafId = Utils.hashOffer(offer); - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData, root, proof); + // Successful on-chain merkle verification: leafId folds up to root + // along the supplied (leafIndex, proof). + require Utils.isLeaf(root, leafId, leafIndex, proof); // The offer's hash is registered as a leaf in the ghost tree. - bytes32 leafId = Utils.hashOffer(offer); assert OfferTree.isLeafNode(leafId); - assert OfferTree.getHash(leafId) == leafId; } From 215698bc858baa8e85dda0fa754c899e91857667 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 17:12:48 +0200 Subject: [PATCH 04/38] removed the diagnostic rules --- certora/specs/TakeCorrectness.spec | 61 ------------------------------ 1 file changed, 61 deletions(-) diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index f5b39d208..0be4539a2 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -76,67 +76,6 @@ function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { return ghostHashNode(a, b); } -// --------------------------------------------------------------------------- -// Diagnostic rules — isolate whether Z3 can use the implication-form -// injectivity axiom on `ghostHashNode`. They do not exercise storage, -// `wellFormedPath`, or `hashOffer`; they only put `ghostHashNode` applications -// in front of the solver and ask it to derive the consequent of the axiom. -// -// If `diagInjectivityOneStep` fails: the axiom is unusable even at one level. -// If `diagInjectivityOneStep` passes but `diagInjectivityTwoStep` fails: the -// solver instantiates the axiom for ground arguments but does not chain -// through a compound `ghostHashNode(...)` sub-term — which is the chain -// structure `takeCorrectness` requires. -// --------------------------------------------------------------------------- - -rule diagInjectivityOneStep(bytes32 a1, bytes32 b1, bytes32 a2, bytes32 b2) { - require ghostHashNode(a1, b1) == ghostHashNode(a2, b2); - assert a1 == a2; - assert b1 == b2; -} - -rule diagInjectivityTwoStep(bytes32 sib0, bytes32 sib1, bytes32 leaf1, bytes32 leaf2) { - require ghostHashNode(ghostHashNode(sib0, leaf1), sib1) - == ghostHashNode(ghostHashNode(sib0, leaf2), sib1); - assert leaf1 == leaf2; -} - -// Tests pure EUF substitution: combine an equation about a storage-derived -// `intermediate` with an equation about `ghostHashNode` applications, and ask -// Z3 to apply two-step injectivity through the substitution. If this passes, -// the SMT layer handles the substitution and the `takeCorrectness` bug must -// be in how `wellFormedPath` establishes its constraints (or in storage -// aliasing across the `wellFormedPath`/`Utils.isLeaf` boundary). If it fails, -// the axiom shape itself can't close this chain even when stated as plain -// SMT facts, and the axiom needs strengthening. -rule diagSubstitution( - bytes32 root, - bytes32 sib0, - bytes32 sib1, - bytes32 D, - bytes32 leafHash, - bytes32 intermediate -) { - require ghostHashNode(intermediate, sib1) == root; - require intermediate == ghostHashNode(sib0, D); - require ghostHashNode(ghostHashNode(sib0, leafHash), sib1) == root; - assert D == leafHash; -} - -// Mirrors `takeCorrectness` but replaces the `hashOffer`-derived `leafId` with a -// free bytes32. If this passes: `hashOffer` (the offer-encoding side) is part -// of the problem. If it fails with the same shape: the failure lives entirely -// in the `wellFormedPath` + `Utils.isLeaf` composition through OfferTree -// storage, independent of how `leafHash` got there. -rule diagTakeCorrectnessFreeLeaf(bytes32 root, uint256 leafIndex, bytes32[] proof, bytes32 leafHash) { - bytes32 node; - require OfferTree.getHash(node) == root; - require root != to_bytes32(0); - OfferTree.wellFormedPath(node, leafIndex, proof); - require Utils.isLeaf(root, leafHash, leafIndex, proof); - assert OfferTree.isLeafNode(leafHash); -} - /// Marquee rule: a successful merkle verification implies the offer's hash is a /// leaf of the well-formed ghost tree pointed to by `root`. rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { From b62eae77790c1c3721794568b186dabecb4f562c Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 17:18:27 +0200 Subject: [PATCH 05/38] cleaned up comments --- certora/helpers/OfferTree.sol | 58 ++++++++----------------- certora/specs/TakeCorrectness.spec | 69 ++++-------------------------- 2 files changed, 25 insertions(+), 102 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 25a2b6103..25e768212 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -4,18 +4,9 @@ pragma solidity ^0.8.0; import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; -/// @dev Ghost offer-tree helper used by Certora specs. -/// @dev Trees are built only via `newLeaf` and `newInternalNode`, which preserve the -/// well-formedness invariant by construction. The verified invariant is then used -/// to prove that any successful merkle proof verification against a Midnight -/// ratified root corresponds to a leaf actually present in the maker's tree. -/// @dev Purely structural: the helper does not encode the Offer struct itself, so it -/// avoids triggering pointer-analysis failures on `Offer.market.collateralParams[]`. -/// Specs supply leaf hashes externally (computed via the spec's chosen hashOffer -/// summary) and assert structural well-formedness here. -/// @dev Mirrors the post-merge `HashLib.isLeaf` proof scheme: internal nodes have -/// directional left/right children combined via `HashLib.hashNode`, and the -/// downward walk in `wellFormedPath` follows the bits of `leafIndex`. +// Ghost offer-tree helper used by Certora specs. +// Trees are built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by construction. +// Specs supply leaf hashes externally; the helper does not encode the Offer struct itself. contract OfferTree { struct Node { bytes32 left; @@ -24,8 +15,12 @@ contract OfferTree { bool isLeaf; } + /* STORAGE */ + mapping(bytes32 => Node) internal tree; + /* MAIN FUNCTIONS */ + function newLeaf(bytes32 leafHash) public { require(leafHash != 0, "zero leaf hash"); Node storage n = tree[leafHash]; @@ -47,6 +42,8 @@ contract OfferTree { n.hashNode = HashLib.hashNode(L.hashNode, R.hashNode); } + /* PURE AND VIEW FUNCTIONS */ + function _isEmpty(Node storage n) internal view returns (bool) { return n.left == 0 && n.right == 0 && n.hashNode == 0 && !n.isLeaf; } @@ -71,9 +68,10 @@ contract OfferTree { return tree[id].right; } - /// @dev Well-formed predicate. - /// @dev Empty nodes well-formed; leaves have id == hashNode and no children; - /// internal nodes have non-empty children and hashNode = hashNode(left.hashNode, right.hashNode). + // The specification of a well-formed tree is the following: + // - empty nodes are well-formed + // - leaves have id == hashNode and no children + // - internal nodes have non-empty children and hashNode = hashNode(left.hashNode, right.hashNode) function isWellFormed(bytes32 id) public view returns (bool) { Node storage n = tree[id]; if (_isEmpty(n)) return true; @@ -88,18 +86,9 @@ contract OfferTree { } } - /// @dev Walks down the tree from `id`, consuming `proof` from end to start, - /// asserting every visited node is well-formed AND that the path terminates - /// at a leaf. - /// @dev At each level, the bit of `leafIndex` decides which side the leaf descends to, - /// mirroring the upward fold in `HashLib.isLeaf`: - /// bit == 0 ⇒ leaf was on the LEFT (sibling is the right child). - /// bit == 1 ⇒ leaf was on the RIGHT (sibling is the left child). - /// @dev The leaf-termination requirement encodes the assumption that `proof.length` - /// matches the actual depth from `id` to a leaf. The on-chain `HashLib.isLeaf` does - /// NOT enforce this (it accepts any proof length whose folded hash equals root) — - /// the gap is intentional in the contract and is exposed by `takeCorrectness` - /// failing if this requirement is dropped. + // Check that the nodes are well-formed starting from `id` and going down the `tree`. + // The bits of `leafIndex` choose the path downward; `proof` supplies the sibling hashes consumed from end to start. + // The path must terminate at a leaf, matching the depth implied by `proof.length`. function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view { require(leafIndex >> proof.length == 0, "leaf index out of range"); for (uint256 i = proof.length;;) { @@ -107,14 +96,7 @@ contract OfferTree { if (i == 0) break; - // If we still have proof elements to consume, the current node must be an - // internal node, not a leaf. Without this, the prover can pick a leaf as the - // starting node — `isWellFormed` accepts it via the leaf branch, the loop - // walks off the leaf's zero children into the unrelated `tree[0]` entry, and - // the well-formedness chain that should pin `hashOffer(offer)` to a leaf in - // this subtree is never established, since the leaf branch of `isWellFormed` - // generates no `hashNode(L.hashNode, R.hashNode)` equation tying the root - // hash to the merkle fold. + // If proof elements remain, the current node must be internal; otherwise the path walks off a leaf's zero children into the unrelated `tree[0]` entry. require(!tree[id].isLeaf); bytes32 sibling = proof[--i]; @@ -122,12 +104,6 @@ contract OfferTree { bytes32 left = tree[id].left; bytes32 right = tree[id].right; - // The sibling supplied by the proof must equal the corresponding child's - // stored hash. Without this, the downward walk and the upward fold in - // `HashLib.isLeaf` can diverge below the root, even though they agree on - // the root value: the fold produces a synthetic intermediate hash unrelated - // to actual tree nodes, and the spec's leaf-membership conclusion would not - // follow. if ((leafIndex >> i) & 1 == 0) { require(getHash(right) == sibling); id = left; diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index 0be4539a2..f0c0ce0fe 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -1,37 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Copyright (c) 2025 Morpho Association -// Rule B — Take correctness against the ghost offer-tree. -// -// Statement: if a maker-ratified root corresponds to a node `node` of a -// well-formed ghost offer-tree, and the supplied `(leafIndex, proof)` descends -// through well-formed nodes from `node`, then a successful merkle proof -// verification (`HashLib.isLeaf`) of `hashOffer(offer)` against that root -// implies the offer is registered as a leaf in the ghost tree (i.e. the offer -// was actually committed by the maker, not forged via second-preimage). -// -// The well-formed invariant on the ghost tree is established by Rule A -// (see OfferTreeWellFormed.spec). -// -// Architectural note (post-main merge): the merkle proof verification has -// moved out of `Midnight.take` and into the ratifier contracts -// (SetterRatifier / EcrecoverRatifier), which call `HashLib.isLeaf` after -// abi-decoding `(root, leafIndex, proof)` from `ratifierData`. The chain -// `successful take ⇒ successful isRatified` is established by -// Ratification.spec (takeRequiresMakerConsent); this rule covers the remaining -// link `successful isLeaf ⇒ leaf in tree`. Composed, the original -// take-level statement still holds. -// -// `HashLib.hashOffer` is summarized to `Utils.hashOffer`, which uses -// `keccak256(abi.encode(offer))`. This deviates from the contract's actual -// EIP-712 encoding but is sound for this rule because: -// 1. determinism is preserved across the merkle verification and the -// helper-side leaf hash; -// 2. injectivity assumed via `optimistic_hashing`; -// 3. the rule reasons about the hash purely as an opaque commitment — -// its specific bit pattern doesn't matter, only that it is the same -// function on both sides. - using OfferTree as OfferTree; using Utils as Utils; @@ -44,20 +13,11 @@ methods { function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - // Deterministic summary of HashLib.hashOffer so the merkle verification - // (via Utils.isLeaf → HashLib.isLeaf → HashLib.hashNode) and the helper-side - // leaf hash agree on the leaf-hash function. Unsummarized, the via-ir lowering - // of the nested Offer.market.collateralParams[] loop blocks the prover's - // pointer/memory analysis. + // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - // Deterministic + injective summary of HashLib.hashNode. The function uses - // inline assembly which the prover treats as a black box without injectivity, - // allowing CEXes where the upward fold (in `HashLib.isLeaf`) and the downward - // walk (in `wellFormedPath`) produce the same root from structurally distinct - // intermediate hashes. The ghost axiom below enforces ordered-pair injectivity, - // matching keccak256's actual behavior on 64-byte inputs. + // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); } @@ -66,8 +26,8 @@ function summaryHashOffer(Midnight.Offer offer) returns bytes32 { return Utils.hashOffer(offer); } +// Injective on ordered pairs. persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { - // Injective on ordered pairs: equal hashes imply equal ordered inputs. axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); } @@ -76,35 +36,22 @@ function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { return ghostHashNode(a, b); } -/// Marquee rule: a successful merkle verification implies the offer's hash is a -/// leaf of the well-formed ghost tree pointed to by `root`. +// The main correctness result of the verification. +// It ensures that if a maker-ratified root corresponds to a node of a well-formed offer-tree, then a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; - // Root is the hash of some node in the ghost tree. + // Assume that root is the hash of node in the tree. require OfferTree.getHash(node) == root; require root != to_bytes32(0); - // The proof descends through well-formed nodes from that node. + // Assume that the tree is well-formed along the proof path from node down to a leaf. OfferTree.wellFormedPath(node, leafIndex, proof); - // Compute the offer's leaf hash once and reuse the symbolic value below. - // Two syntactic `Utils.hashOffer(offer)` sites would each lower to - // `keccak256(abi.encode(offer))` over freshly-materialized `bytes memory`; - // the prover's hashing model only treats keccak as injective on - // byte-equal inputs, and the `Offer.market.collateralParams[]` nested - // dynamic array (the same pointer/memory analysis limitation that - // motivates the `HashLib.hashOffer` summary above) blocks proving the - // two encoded buffers identical. The merkle-fold side and the - // assertion side could then bind to different symbolic hashes, yielding - // a spurious CEX where the upward fold pins one hash to a leaf in the - // ghost tree but the assertion reads a different hash that isn't. + // Compute the leaf hash once so both uses below bind to the same symbolic value. bytes32 leafId = Utils.hashOffer(offer); - // Successful on-chain merkle verification: leafId folds up to root - // along the supplied (leafIndex, proof). require Utils.isLeaf(root, leafId, leafIndex, proof); - // The offer's hash is registered as a leaf in the ghost tree. assert OfferTree.isLeafNode(leafId); } From b9d943ea13c628c5a704ac1d9200eec27763f787 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 17:39:54 +0200 Subject: [PATCH 06/38] add completeness rule --- certora/helpers/OfferTree.sol | 4 +++- certora/specs/OfferTreeWellFormed.spec | 4 ++-- certora/specs/TakeCorrectness.spec | 17 +++++++++++++++-- 3 files changed, 20 insertions(+), 5 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 25e768212..d7cfd3e1b 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -89,7 +89,8 @@ contract OfferTree { // Check that the nodes are well-formed starting from `id` and going down the `tree`. // The bits of `leafIndex` choose the path downward; `proof` supplies the sibling hashes consumed from end to start. // The path must terminate at a leaf, matching the depth implied by `proof.length`. - function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view { + // Returns the id of the leaf at the bottom of the path. + function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view returns (bytes32) { require(leafIndex >> proof.length == 0, "leaf index out of range"); for (uint256 i = proof.length;;) { require(isWellFormed(id)); @@ -113,5 +114,6 @@ contract OfferTree { } } require(tree[id].isLeaf); + return id; } } diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index f9bcef713..f9b941425 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -12,10 +12,10 @@ methods { function isWellFormed(bytes32) external returns (bool) envfree; } -invariant zeroIsEmpty() +strong invariant zeroIsEmpty() isEmpty(to_bytes32(0)); -invariant wellFormed(bytes32 id) +strong invariant wellFormed(bytes32 id) isWellFormed(id) { preserved { diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index f0c0ce0fe..aa0665656 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -8,7 +8,7 @@ methods { function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; - function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external envfree; + function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; @@ -37,7 +37,7 @@ function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { } // The main correctness result of the verification. -// It ensures that if a maker-ratified root corresponds to a node of a well-formed offer-tree, then a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. +// If a maker-ratified root corresponds to a node of a well-formed offer-tree, then a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; @@ -55,3 +55,16 @@ rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, byte assert OfferTree.isLeafNode(leafId); } + +// The completeness dual of takeCorrectness. +// Every leaf in a well-formed offer-tree has a verifying merkle proof: folding the path's sibling hashes back up against the leaf reproduces the root. +rule takeCompleteness(bytes32 node, bytes32 root, uint256 leafIndex, bytes32[] proof) { + // Assume that root is the hash of node in the tree. + require OfferTree.getHash(node) == root; + require root != to_bytes32(0); + + // Walk the well-formed path; the call returns the leaf at the bottom. + bytes32 endLeaf = OfferTree.wellFormedPath(node, leafIndex, proof); + + assert Utils.isLeaf(root, endLeaf, leafIndex, proof); +} From 9b92e504657a15673431385a96f5d410660ea825 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 18:05:20 +0200 Subject: [PATCH 07/38] abstract properties instantiated to midnight --- certora/confs/SetterRatification.conf | 23 ++++++++++ certora/specs/SetterRatification.spec | 63 +++++++++++++++++++++++++++ certora/specs/TakeCorrectness.spec | 47 ++++++++++++++++++++ 3 files changed, 133 insertions(+) create mode 100644 certora/confs/SetterRatification.conf create mode 100644 certora/specs/SetterRatification.spec diff --git a/certora/confs/SetterRatification.conf b/certora/confs/SetterRatification.conf new file mode 100644 index 000000000..61dea9691 --- /dev/null +++ b/certora/confs/SetterRatification.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "src/Midnight.sol", + "src/ratifiers/SetterRatifier.sol", + "certora/helpers/OfferTree.sol", + "certora/helpers/Utils.sol" + ], + "verify": "Midnight:certora/specs/SetterRatification.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": "SetterRatification" +} diff --git a/certora/specs/SetterRatification.spec b/certora/specs/SetterRatification.spec new file mode 100644 index 000000000..ade7f3ae4 --- /dev/null +++ b/certora/specs/SetterRatification.spec @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association + +using OfferTree as OfferTree; +using Utils as Utils; +using SetterRatifier as SetterRatifier; + +methods { + function OfferTree.getHash(bytes32) external returns (bytes32) envfree; + function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; + function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; + function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; + + function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; + + function SetterRatifier.isRootRatified(address, bytes32) external returns (bool) envfree; + + // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. + function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => + summaryHashOffer(offer); + + // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. + function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => + summaryHashNode(a, b); +} + +function summaryHashOffer(Midnight.Offer offer) returns bytes32 { + return Utils.hashOffer(offer); +} + +// Injective on ordered pairs. +persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { + axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. + ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); +} + +function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { + return ghostHashNode(a, b); +} + +// SetterRatifier-specific framing of takeCorrectness. +// Premise: the maker has explicitly committed to `root` via SetterRatifier.setIsRootRatified. Conclusion: every offer whose hash verifies against `root` via merkle proof is registered as a leaf in the maker's committed offer-tree. +rule setterRatifiedTakeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { + bytes32 node; + + // Assume that the maker has explicitly committed to root via SetterRatifier. + require SetterRatifier.isRootRatified(offer.maker, root); + + // Assume that root is the hash of node in the maker's tree. + require OfferTree.getHash(node) == root; + require root != to_bytes32(0); + + // Assume that the tree is well-formed along the proof path from node down to a leaf. + OfferTree.wellFormedPath(node, leafIndex, proof); + + // Compute the leaf hash once so both uses below bind to the same symbolic value. + bytes32 leafId = Utils.hashOffer(offer); + + require Utils.isLeaf(root, leafId, leafIndex, proof); + + assert OfferTree.isLeafNode(leafId); +} diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index aa0665656..cb671fa49 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -5,6 +5,8 @@ using OfferTree as OfferTree; using Utils as Utils; methods { + function isAuthorized(address authorizer, address authorized) external returns (bool) envfree; + function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; @@ -20,6 +22,24 @@ methods { // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); + + // Take-side externals summarized as NONDET / havoc — irrelevant to the merkle-membership property. + // `isRatified` is NONDET'd so the rule abstracts over the ratifier choice: the bridge from + // `take ⇒ Utils.isLeaf success` is supplied explicitly in `takeImpliesLeafInTree` below. + function _.isRatified(Midnight.Offer, bytes) external => NONDET; + function _.onBuy(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.transfer(address, uint256) external => NONDET; + function multicall(bytes[]) external => HAVOC_ALL DELETE; + 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; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; + function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; } function summaryHashOffer(Midnight.Offer offer) returns bytes32 { @@ -68,3 +88,30 @@ rule takeCompleteness(bytes32 node, bytes32 root, uint256 leafIndex, bytes32[] p assert Utils.isLeaf(root, endLeaf, leafIndex, proof); } + +// The take-level guarantee: every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. +// The bridge from take's success to the merkle check is supplied by `require Utils.isLeaf(...)` below. It is justified by composition: take's body requires `isRatified(offer, ratifierData) == CALLBACK_SUCCESS`, and both SetterRatifier and EcrecoverRatifier implementations `require(HashLib.isLeaf(root, hashOffer(offer), leafIndex, proof))` for the (root, leafIndex, proof) they decode from ratifierData — regardless of how the maker committed the root (on-chain via `isRootRatified`, or off-chain via EIP-712 signature). +rule takeImpliesLeafInTree( + env e, + uint256 units, address taker, address takerCallback, bytes takerCallbackData, + address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, + bytes32 root, uint256 leafIndex, bytes32[] proof +) { + bytes32 node; + + // Assume that root is the hash of node in the maker's tree. + require OfferTree.getHash(node) == root; + require root != to_bytes32(0); + + // Assume that the tree is well-formed along the proof path from node down to a leaf. + OfferTree.wellFormedPath(node, leafIndex, proof); + + bytes32 leafId = Utils.hashOffer(offer); + + // Bridge: a successful take implies the chosen ratifier's `isRatified` returned CALLBACK_SUCCESS, which implies `HashLib.isLeaf(...)` passed for the (root, leafIndex, proof) it decoded from ratifierData. We model that decoded triple as the rule's (root, leafIndex, proof). + require Utils.isLeaf(root, leafId, leafIndex, proof); + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData); + + assert OfferTree.isLeafNode(leafId); +} From 0cd4f3eebe0d5cf7144a2a8e530e486b0813b253 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 18:07:39 +0200 Subject: [PATCH 08/38] cvl fmt --- certora/specs/SetterRatification.spec | 9 +++------ certora/specs/TakeCorrectness.spec | 16 ++++------------ 2 files changed, 7 insertions(+), 18 deletions(-) diff --git a/certora/specs/SetterRatification.spec b/certora/specs/SetterRatification.spec index ade7f3ae4..673ed887e 100644 --- a/certora/specs/SetterRatification.spec +++ b/certora/specs/SetterRatification.spec @@ -17,12 +17,10 @@ methods { function SetterRatifier.isRootRatified(address, bytes32) external returns (bool) envfree; // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. - function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => - summaryHashOffer(offer); + function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. - function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => - summaryHashNode(a, b); + function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); } function summaryHashOffer(Midnight.Offer offer) returns bytes32 { @@ -31,8 +29,7 @@ function summaryHashOffer(Midnight.Offer offer) returns bytes32 { // Injective on ordered pairs. persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { - axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. - ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); + axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); } function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/TakeCorrectness.spec index cb671fa49..f381cd7c8 100644 --- a/certora/specs/TakeCorrectness.spec +++ b/certora/specs/TakeCorrectness.spec @@ -16,12 +16,10 @@ methods { function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. - function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => - summaryHashOffer(offer); + function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. - function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => - summaryHashNode(a, b); + function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); // Take-side externals summarized as NONDET / havoc — irrelevant to the merkle-membership property. // `isRatified` is NONDET'd so the rule abstracts over the ratifier choice: the bridge from @@ -48,8 +46,7 @@ function summaryHashOffer(Midnight.Offer offer) returns bytes32 { // Injective on ordered pairs. persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { - axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. - ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); + axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); } function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { @@ -91,12 +88,7 @@ rule takeCompleteness(bytes32 node, bytes32 root, uint256 leafIndex, bytes32[] p // The take-level guarantee: every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. // The bridge from take's success to the merkle check is supplied by `require Utils.isLeaf(...)` below. It is justified by composition: take's body requires `isRatified(offer, ratifierData) == CALLBACK_SUCCESS`, and both SetterRatifier and EcrecoverRatifier implementations `require(HashLib.isLeaf(root, hashOffer(offer), leafIndex, proof))` for the (root, leafIndex, proof) they decode from ratifierData — regardless of how the maker committed the root (on-chain via `isRootRatified`, or off-chain via EIP-712 signature). -rule takeImpliesLeafInTree( - env e, - uint256 units, address taker, address takerCallback, bytes takerCallbackData, - address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, - bytes32 root, uint256 leafIndex, bytes32[] proof -) { +rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; // Assume that root is the hash of node in the maker's tree. From 07d95e3ed6aea26a67b7436c3c90ea7a9d116901 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 19 May 2026 18:10:22 +0200 Subject: [PATCH 09/38] fmt --- certora/helpers/OfferTree.sol | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index d7cfd3e1b..221713c90 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -81,8 +81,7 @@ contract OfferTree { if (n.left == 0 || n.right == 0) return false; Node storage L = tree[n.left]; Node storage R = tree[n.right]; - return !_isEmpty(L) && !_isEmpty(R) - && n.hashNode == HashLib.hashNode(L.hashNode, R.hashNode); + return !_isEmpty(L) && !_isEmpty(R) && n.hashNode == HashLib.hashNode(L.hashNode, R.hashNode); } } @@ -97,7 +96,8 @@ contract OfferTree { if (i == 0) break; - // If proof elements remain, the current node must be internal; otherwise the path walks off a leaf's zero children into the unrelated `tree[0]` entry. + // If proof elements remain, the current node must be internal; otherwise the path walks off a leaf's zero + // children into the unrelated `tree[0]` entry. require(!tree[id].isLeaf); bytes32 sibling = proof[--i]; From bcc519888c92e58b144d9877bff4ad920188ec90 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:01:28 +0200 Subject: [PATCH 10/38] renamed spec; minor changes in OfferTree definition --- certora/confs/{TakeCorrectness.conf => OfferTreeMembership.conf} | 0 certora/specs/{TakeCorrectness.spec => OfferTreeMembership.spec} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename certora/confs/{TakeCorrectness.conf => OfferTreeMembership.conf} (100%) rename certora/specs/{TakeCorrectness.spec => OfferTreeMembership.spec} (100%) diff --git a/certora/confs/TakeCorrectness.conf b/certora/confs/OfferTreeMembership.conf similarity index 100% rename from certora/confs/TakeCorrectness.conf rename to certora/confs/OfferTreeMembership.conf diff --git a/certora/specs/TakeCorrectness.spec b/certora/specs/OfferTreeMembership.spec similarity index 100% rename from certora/specs/TakeCorrectness.spec rename to certora/specs/OfferTreeMembership.spec From 38c1875d08f03da3c5e7050d7e6a3492ac1acedd Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:02:19 +0200 Subject: [PATCH 11/38] tuned --- certora/confs/OfferTreeMembership.conf | 4 +-- certora/helpers/OfferTree.sol | 43 +++++++++++++------------- certora/specs/OfferTreeWellFormed.spec | 6 ++-- 3 files changed, 26 insertions(+), 27 deletions(-) diff --git a/certora/confs/OfferTreeMembership.conf b/certora/confs/OfferTreeMembership.conf index 13e5f2ff9..c00b1f1c8 100644 --- a/certora/confs/OfferTreeMembership.conf +++ b/certora/confs/OfferTreeMembership.conf @@ -4,7 +4,7 @@ "certora/helpers/OfferTree.sol", "certora/helpers/Utils.sol" ], - "verify": "Midnight:certora/specs/TakeCorrectness.spec", + "verify": "Midnight:certora/specs/OfferTreeMembership.spec", "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", @@ -18,5 +18,5 @@ "-splitParallel true", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" ], - "msg": "TakeCorrectness" + "msg": "Offer Tree Membership" } diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 221713c90..d68b11794 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -12,7 +12,6 @@ contract OfferTree { bytes32 left; bytes32 right; bytes32 hashNode; - bool isLeaf; } /* STORAGE */ @@ -26,26 +25,25 @@ contract OfferTree { Node storage n = tree[leafHash]; require(_isEmpty(n), "leaf already populated"); n.hashNode = leafHash; - n.isLeaf = true; } 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"); - Node storage L = tree[left]; - Node storage R = tree[right]; - require(!_isEmpty(L), "left empty"); - require(!_isEmpty(R), "right empty"); + 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(L.hashNode, R.hashNode); + 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 && !n.isLeaf; + return n.left == 0 && n.right == 0 && n.hashNode == 0; } function isEmpty(bytes32 id) public view returns (bool) { @@ -57,7 +55,7 @@ contract OfferTree { } function isLeafNode(bytes32 id) public view returns (bool) { - return tree[id].isLeaf; + return tree[id].left == 0 && tree[id].right == 0 && tree[id].hashNode != 0; } function getLeft(bytes32 id) public view returns (bytes32) { @@ -69,20 +67,23 @@ contract OfferTree { } // The specification of a well-formed tree is the following: - // - empty nodes are well-formed - // - leaves have id == hashNode and no children - // - internal nodes have non-empty children and hashNode = hashNode(left.hashNode, right.hashNode) + // - empty nodes (all fields zero) are well-formed + // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == id + // - internal nodes (left != 0 && right != 0) require non-empty children and hashNode = hashNode(left.hashNode, right.hashNode) + // - any other field combination is malformed function isWellFormed(bytes32 id) public view returns (bool) { Node storage n = tree[id]; if (_isEmpty(n)) return true; - if (n.isLeaf) { - return n.left == 0 && n.right == 0 && n.hashNode == id && n.hashNode != 0; - } else { - if (n.left == 0 || n.right == 0) return false; - Node storage L = tree[n.left]; - Node storage R = tree[n.right]; - return !_isEmpty(L) && !_isEmpty(R) && n.hashNode == HashLib.hashNode(L.hashNode, R.hashNode); + if (n.left == 0 && n.right == 0) { + return n.hashNode == id; } + 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`. @@ -98,7 +99,7 @@ contract OfferTree { // If proof elements remain, the current node must be internal; otherwise the path walks off a leaf's zero // children into the unrelated `tree[0]` entry. - require(!tree[id].isLeaf); + require(!isLeafNode(id)); bytes32 sibling = proof[--i]; @@ -113,7 +114,7 @@ contract OfferTree { id = right; } } - require(tree[id].isLeaf); + require(isLeafNode(id)); return id; } } diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index f9b941425..3fa87d390 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -1,10 +1,8 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Copyright (c) 2025 Morpho Association -// Rule A — Well-formed offer-tree invariant. -// -// Verifies that the helper's only mutators (`newLeaf`, `newInternalNode`) -// preserve `isWellFormed` for every node id. This justifies using the helper +// Verifies that the tree construction via `newLeaf` and `newInternalNode` +// preserves `isWellFormed` for every node id. This justifies using the helper // as a ghost tree to reason about Midnight's runtime merkle verification. methods { From 8208a49ca589f5cf1ea4ee49aaa25c917c15654a Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:07:31 +0200 Subject: [PATCH 12/38] fmt --- certora/specs/OfferTreeMembership.spec | 57 +++++++++++--------------- certora/specs/OfferTreeWellFormed.spec | 5 --- 2 files changed, 23 insertions(+), 39 deletions(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index f381cd7c8..6095dbbf7 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -1,11 +1,10 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// Copyright (c) 2025 Morpho Association using OfferTree as OfferTree; using Utils as Utils; methods { - function isAuthorized(address authorizer, address authorized) external returns (bool) envfree; + function isAuthorized(address, address) external returns (bool) envfree; function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; @@ -15,15 +14,12 @@ methods { function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. + // Align the merkle verification and the helper's well-formedness on the same injective hash functions. function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - - // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); - // Take-side externals summarized as NONDET / havoc — irrelevant to the merkle-membership property. - // `isRatified` is NONDET'd so the rule abstracts over the ratifier choice: the bridge from - // `take ⇒ Utils.isLeaf success` is supplied explicitly in `takeImpliesLeafInTree` below. + // Take-side externals are irrelevant to merkle membership. `isRatified` is NONDET'd so the rule + // abstracts over the ratifier choice; the bridge to `Utils.isLeaf` is supplied in the rule body. function _.isRatified(Midnight.Offer, bytes) external => NONDET; function _.onBuy(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; function _.onSell(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; @@ -53,55 +49,48 @@ function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { return ghostHashNode(a, b); } -// The main correctness result of the verification. -// If a maker-ratified root corresponds to a node of a well-formed offer-tree, then a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. +/// SOUNDNESS /// + +/// If a root corresponds to a node of a well-formed offer-tree, a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; + require OfferTree.getHash(node) == root, "root is the hash of node"; + require root != to_bytes32(0), "root is non-zero"; - // Assume that root is the hash of node in the tree. - require OfferTree.getHash(node) == root; - require root != to_bytes32(0); - - // Assume that the tree is well-formed along the proof path from node down to a leaf. OfferTree.wellFormedPath(node, leafIndex, proof); - // Compute the leaf hash once so both uses below bind to the same symbolic value. + // Compute leafId once so both uses below bind to the same symbolic hash. bytes32 leafId = Utils.hashOffer(offer); - - require Utils.isLeaf(root, leafId, leafIndex, proof); + require Utils.isLeaf(root, leafId, leafIndex, proof), "merkle proof verifies"; assert OfferTree.isLeafNode(leafId); } -// The completeness dual of takeCorrectness. -// Every leaf in a well-formed offer-tree has a verifying merkle proof: folding the path's sibling hashes back up against the leaf reproduces the root. +/// COMPLETENESS /// + +/// Every leaf in a well-formed offer-tree has a verifying merkle proof: folding the path's sibling hashes back up against the leaf reproduces the root. rule takeCompleteness(bytes32 node, bytes32 root, uint256 leafIndex, bytes32[] proof) { - // Assume that root is the hash of node in the tree. - require OfferTree.getHash(node) == root; - require root != to_bytes32(0); + require OfferTree.getHash(node) == root, "root is the hash of node"; + require root != to_bytes32(0), "root is non-zero"; - // Walk the well-formed path; the call returns the leaf at the bottom. bytes32 endLeaf = OfferTree.wellFormedPath(node, leafIndex, proof); assert Utils.isLeaf(root, endLeaf, leafIndex, proof); } -// The take-level guarantee: every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. -// The bridge from take's success to the merkle check is supplied by `require Utils.isLeaf(...)` below. It is justified by composition: take's body requires `isRatified(offer, ratifierData) == CALLBACK_SUCCESS`, and both SetterRatifier and EcrecoverRatifier implementations `require(HashLib.isLeaf(root, hashOffer(offer), leafIndex, proof))` for the (root, leafIndex, proof) they decode from ratifierData — regardless of how the maker committed the root (on-chain via `isRootRatified`, or off-chain via EIP-712 signature). +/// TAKE-LEVEL LIFT /// + +/// Every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. +/// The `require Utils.isLeaf(...)` below is the bridge from take to the merkle check, justified by composition: take requires `isRatified(...) == CALLBACK_SUCCESS`, and both SetterRatifier and EcrecoverRatifier require HashLib.isLeaf to pass. rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; + require OfferTree.getHash(node) == root, "root is the hash of node"; + require root != to_bytes32(0), "root is non-zero"; - // Assume that root is the hash of node in the maker's tree. - require OfferTree.getHash(node) == root; - require root != to_bytes32(0); - - // Assume that the tree is well-formed along the proof path from node down to a leaf. OfferTree.wellFormedPath(node, leafIndex, proof); bytes32 leafId = Utils.hashOffer(offer); - - // Bridge: a successful take implies the chosen ratifier's `isRatified` returned CALLBACK_SUCCESS, which implies `HashLib.isLeaf(...)` passed for the (root, leafIndex, proof) it decoded from ratifierData. We model that decoded triple as the rule's (root, leafIndex, proof). - require Utils.isLeaf(root, leafId, leafIndex, proof); + require Utils.isLeaf(root, leafId, leafIndex, proof), "ratifier bridge: matches the merkle check inside isRatified"; take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData); diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index 3fa87d390..c584c5cd6 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -1,9 +1,4 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// Copyright (c) 2025 Morpho Association - -// Verifies that the tree construction via `newLeaf` and `newInternalNode` -// preserves `isWellFormed` for every node id. This justifies using the helper -// as a ghost tree to reason about Midnight's runtime merkle verification. methods { function isEmpty(bytes32) external returns (bool) envfree; From 80d2ad2697f303234b8463c8a8fe04d7ad96dca8 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:10:46 +0200 Subject: [PATCH 13/38] forge fmt --- certora/helpers/OfferTree.sol | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index d68b11794..d371eeaff 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -69,8 +69,8 @@ contract OfferTree { // The specification of a well-formed tree is the following: // - empty nodes (all fields zero) are well-formed // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == id - // - internal nodes (left != 0 && right != 0) require non-empty children and hashNode = hashNode(left.hashNode, right.hashNode) - // - any other field combination is malformed + // - internal nodes (left != 0 && right != 0) require non-empty children and hashNode = hashNode(left.hashNode, + // right.hashNode) - any other field combination is malformed function isWellFormed(bytes32 id) public view returns (bool) { Node storage n = tree[id]; if (_isEmpty(n)) return true; @@ -80,8 +80,7 @@ contract OfferTree { 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 leftHash != 0 && rightHash != 0 && n.hashNode == HashLib.hashNode(leftHash, rightHash); } return false; } From 03ba8cdd4201e054622c7fac95079c56f7d503e6 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:36:02 +0200 Subject: [PATCH 14/38] resolved errors from merge --- certora/specs/OfferTreeMembership.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index 6095dbbf7..e8d2764a3 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -92,7 +92,7 @@ rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCal bytes32 leafId = Utils.hashOffer(offer); require Utils.isLeaf(root, leafId, leafIndex, proof), "ratifier bridge: matches the merkle check inside isRatified"; - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, ratifierData); + take(e, offer, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData, ratifierData); assert OfferTree.isLeafNode(leafId); } From dd415d017dc728a9ab8a49dcd456869f2ab9910c Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 10:42:07 +0200 Subject: [PATCH 15/38] updated callback summary signatures --- certora/specs/OfferTreeMembership.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index e8d2764a3..f408be60e 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -21,8 +21,8 @@ methods { // Take-side externals are irrelevant to merkle membership. `isRatified` is NONDET'd so the rule // abstracts over the ratifier choice; the bridge to `Utils.isLeaf` is supplied in the rule body. function _.isRatified(Midnight.Offer, bytes) external => NONDET; - function _.onBuy(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; - function _.onSell(bytes32, Midnight.Market, address, uint256, uint256, bytes) external => NONDET; + 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; function multicall(bytes[]) external => HAVOC_ALL DELETE; From 24140f4b77a2c77d4dae34dd2fc3d7a7bfb31ab6 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 11:23:04 +0200 Subject: [PATCH 16/38] new rule in Ratification.spec: isRatified always calls isLeaf --- certora/confs/Ratification.conf | 7 ++++-- certora/helpers/Utils.sol | 4 ++++ certora/specs/Ratification.spec | 40 +++++++++++++++++++++++++++++++-- 3 files changed, 47 insertions(+), 4 deletions(-) diff --git a/certora/confs/Ratification.conf b/certora/confs/Ratification.conf index ee35ddd4c..1a2010582 100644 --- a/certora/confs/Ratification.conf +++ b/certora/confs/Ratification.conf @@ -1,10 +1,13 @@ { "files": [ "src/Midnight.sol", - "src/ratifiers/EcrecoverRatifier.sol" + "src/ratifiers/EcrecoverRatifier.sol", + "src/ratifiers/SetterRatifier.sol", + "certora/helpers/Utils.sol" ], "link": [ - "EcrecoverRatifier:MIDNIGHT=Midnight" + "EcrecoverRatifier:MIDNIGHT=Midnight", + "SetterRatifier:MIDNIGHT=Midnight" ], "verify": "Midnight:certora/specs/Ratification.spec", "solc": "solc-0.8.34", diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index c8dabebcf..1f8aa03d0 100644 --- a/certora/helpers/Utils.sol +++ b/certora/helpers/Utils.sol @@ -22,6 +22,10 @@ contract Utils { return keccak256(abi.encode(offer)); } + function hashNode(bytes32 a, bytes32 b) external pure returns (bytes32) { + return keccak256(abi.encode(a, b)); + } + function isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) external pure diff --git a/certora/specs/Ratification.spec b/certora/specs/Ratification.spec index c99cd04b6..8a02fc2b7 100644 --- a/certora/specs/Ratification.spec +++ b/certora/specs/Ratification.spec @@ -1,18 +1,28 @@ // 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; + function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + 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; - function HashLib.isLeaf(bytes32, bytes32, uint256, bytes32[] memory) internal returns (bool) => NONDET; + + // Capture HashLib.isLeaf's args + return; needed by `isRatifiedRequiresIsLeaf`. + function HashLib.isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) internal returns (bool) => isLeafCapture(root, leafHash, leafIndex, proof); + + // Route hashOffer through Utils so the rule can equate the captured leafHash to hashOffer(offer). + function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); + function HashLib.offerTreeTypeHash(uint256) internal returns (bytes32) => NONDET; - function HashLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; // Summaries for internals irrelevant to ratification properties. function IdLib.toId(Midnight.Market memory, uint256, address) internal returns (bytes32) => NONDET; @@ -25,6 +35,22 @@ methods { function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; } +function summaryHashOffer(Midnight.Offer offer) returns bytes32 { + return Utils.hashOffer(offer); +} + +// 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(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] proof) 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, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData, bytes ratifierData) { bool makerAuthorizedRatifier = isAuthorized(offer.maker, offer.ratifier); @@ -52,3 +78,13 @@ rule takeRequiresNonZeroMaker(env e, Midnight.Offer offer, uint256 units, addres take(e, offer, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData, ratifierData); 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"; +} From cfb723f7d15d4af477a0496aab0cc3b7c781f34c Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 20 May 2026 11:23:46 +0200 Subject: [PATCH 17/38] rhashNode summarised similar to hashOffer --- certora/specs/OfferTreeMembership.spec | 10 +++------- certora/specs/SetterRatification.spec | 14 +++++--------- 2 files changed, 8 insertions(+), 16 deletions(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index f408be60e..bd614c40c 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -12,9 +12,10 @@ methods { function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + function Utils.hashNode(bytes32, bytes32) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - // Align the merkle verification and the helper's well-formedness on the same injective hash functions. + // Align the merkle verification and the helper's well-formedness on the same hash functions. function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); @@ -40,13 +41,8 @@ function summaryHashOffer(Midnight.Offer offer) returns bytes32 { return Utils.hashOffer(offer); } -// Injective on ordered pairs. -persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { - axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); -} - function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { - return ghostHashNode(a, b); + return Utils.hashNode(a, b); } /// SOUNDNESS /// diff --git a/certora/specs/SetterRatification.spec b/certora/specs/SetterRatification.spec index 673ed887e..06c4b7c72 100644 --- a/certora/specs/SetterRatification.spec +++ b/certora/specs/SetterRatification.spec @@ -12,14 +12,15 @@ methods { function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; + function Utils.hashNode(bytes32, bytes32) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; function SetterRatifier.isRootRatified(address, bytes32) external returns (bool) envfree; - // Summarized so the merkle verification and the helper-side leaf hash agree on the leaf-hash function. + // Align the merkle verification and the helper's well-formedness on the same hash functions. + // Routing through Utils (`keccak256(abi.encode(...))`) lets Certora's bounded-hash recognition + // supply injectivity automatically, instead of needing a ghost + axiom. function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - - // Summarized to a ghost so the upward fold and the downward walk see the same injective hash function. function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); } @@ -27,13 +28,8 @@ function summaryHashOffer(Midnight.Offer offer) returns bytes32 { return Utils.hashOffer(offer); } -// Injective on ordered pairs. -persistent ghost ghostHashNode(bytes32, bytes32) returns bytes32 { - axiom forall bytes32 a1. forall bytes32 b1. forall bytes32 a2. forall bytes32 b2. ghostHashNode(a1, b1) == ghostHashNode(a2, b2) => (a1 == a2 && b1 == b2); -} - function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { - return ghostHashNode(a, b); + return Utils.hashNode(a, b); } // SetterRatifier-specific framing of takeCorrectness. From 8187c247889fab11f4168312662d715c99b90aec Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 21 May 2026 14:18:49 +0200 Subject: [PATCH 18/38] revamped soundness: Offer included in the node --- certora/helpers/OfferTree.sol | 52 ++++++++++---------------- certora/specs/OfferTreeMembership.spec | 17 ++------- certora/specs/Ratification.spec | 6 +-- 3 files changed, 25 insertions(+), 50 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index d371eeaff..8c8e45ede 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -2,15 +2,18 @@ // Copyright (c) 2025 Morpho Association pragma solidity ^0.8.0; +import {Offer} from "../../src/interfaces/IMidnight.sol"; import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; -// Ghost offer-tree helper used by Certora specs. // Trees are built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by construction. -// Specs supply leaf hashes externally; the helper does not encode the Offer struct itself. +// Leaves carry the offer payload so `isWellFormed` can pin a leaf's `hashNode` into the image of +// `hashOffer` (distinct keccak input shape from `hashNode`), giving domain separation against internal-node +// hashes for free under Certora's keccak model. contract OfferTree { struct Node { bytes32 left; bytes32 right; + Offer offer; bytes32 hashNode; } @@ -20,11 +23,13 @@ contract OfferTree { /* MAIN FUNCTIONS */ - function newLeaf(bytes32 leafHash) public { - require(leafHash != 0, "zero leaf hash"); - Node storage n = tree[leafHash]; + function newLeaf(Offer memory offer) public { + bytes32 id = HashLib.hashOffer(offer); + require(id != 0, "zero offer hash"); + Node storage n = tree[id]; require(_isEmpty(n), "leaf already populated"); - n.hashNode = leafHash; + n.offer = offer; + n.hashNode = id; } function newInternalNode(bytes32 id, bytes32 left, bytes32 right) public { @@ -67,15 +72,16 @@ contract OfferTree { } // The specification of a well-formed tree is the following: - // - empty nodes (all fields zero) are well-formed - // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == id + // - empty nodes (left == 0 && right == 0 && hashNode == 0) are well-formed + // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == hashOffer(offer) and id == hashNode // - internal nodes (left != 0 && right != 0) require non-empty children and hashNode = hashNode(left.hashNode, // right.hashNode) - any other field combination is malformed 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) { - return n.hashNode == id; + bytes32 expected = HashLib.hashOffer(n.offer); + return n.hashNode == expected && id == expected; } if (n.left != 0 && n.right != 0) { bytes32 leftHash = tree[n.left].hashNode; @@ -86,34 +92,16 @@ contract OfferTree { } // Check that the nodes are well-formed starting from `id` and going down the `tree`. - // The bits of `leafIndex` choose the path downward; `proof` supplies the sibling hashes consumed from end to start. - // The path must terminate at a leaf, matching the depth implied by `proof.length`. - // Returns the id of the leaf at the bottom of the path. - function wellFormedPath(bytes32 id, uint256 leafIndex, bytes32[] memory proof) public view returns (bytes32) { - require(leafIndex >> proof.length == 0, "leaf index out of range"); + // 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; - // If proof elements remain, the current node must be internal; otherwise the path walks off a leaf's zero - // children into the unrelated `tree[0]` entry. - require(!isLeafNode(id)); - - bytes32 sibling = proof[--i]; - - bytes32 left = tree[id].left; - bytes32 right = tree[id].right; - - if ((leafIndex >> i) & 1 == 0) { - require(getHash(right) == sibling); - id = left; - } else { - require(getHash(left) == sibling); - id = right; - } + --i; + id = ((leafIndex >> i) & 1 == 0) ? tree[id].left : tree[id].right; } - require(isLeafNode(id)); - return id; + return true; } } diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index bd614c40c..dd1e00c45 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -9,7 +9,7 @@ methods { function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; - function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; + function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bool) envfree; function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.hashNode(bytes32, bytes32) external returns (bytes32) envfree; @@ -57,23 +57,12 @@ rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, byte // Compute leafId once so both uses below bind to the same symbolic hash. bytes32 leafId = Utils.hashOffer(offer); + require leafId != to_bytes32(0), "leafId is non-zero"; require Utils.isLeaf(root, leafId, leafIndex, proof), "merkle proof verifies"; assert OfferTree.isLeafNode(leafId); } -/// COMPLETENESS /// - -/// Every leaf in a well-formed offer-tree has a verifying merkle proof: folding the path's sibling hashes back up against the leaf reproduces the root. -rule takeCompleteness(bytes32 node, bytes32 root, uint256 leafIndex, bytes32[] proof) { - require OfferTree.getHash(node) == root, "root is the hash of node"; - require root != to_bytes32(0), "root is non-zero"; - - bytes32 endLeaf = OfferTree.wellFormedPath(node, leafIndex, proof); - - assert Utils.isLeaf(root, endLeaf, leafIndex, proof); -} - /// TAKE-LEVEL LIFT /// /// Every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. @@ -86,7 +75,7 @@ rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCal OfferTree.wellFormedPath(node, leafIndex, proof); bytes32 leafId = Utils.hashOffer(offer); - require Utils.isLeaf(root, leafId, leafIndex, proof), "ratifier bridge: matches the merkle check inside isRatified"; + require Utils.isLeaf(root, leafId, leafIndex, proof); take(e, offer, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData, ratifierData); diff --git a/certora/specs/Ratification.spec b/certora/specs/Ratification.spec index 8a02fc2b7..9430ad465 100644 --- a/certora/specs/Ratification.spec +++ b/certora/specs/Ratification.spec @@ -16,12 +16,10 @@ methods { function _.transferFrom(address, address, uint256) external => NONDET; function _.transfer(address, uint256) external => NONDET; - // Capture HashLib.isLeaf's args + return; needed by `isRatifiedRequiresIsLeaf`. + // Capture HashLib.isLeaf's return; needed by `isRatifiedRequiresIsLeaf` to assert isRatified gates on a merkle check. function HashLib.isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) internal returns (bool) => isLeafCapture(root, leafHash, leafIndex, proof); - // Route hashOffer through Utils so the rule can equate the captured leafHash to hashOffer(offer). - function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - + 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. From 2d1eb8747367acf9d6004d1c3d2daf18493ace97 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 21 May 2026 16:17:57 +0200 Subject: [PATCH 19/38] tuned comment --- certora/helpers/OfferTree.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 8c8e45ede..4024829d4 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -25,9 +25,9 @@ contract OfferTree { function newLeaf(Offer memory offer) public { bytes32 id = HashLib.hashOffer(offer); - require(id != 0, "zero offer hash"); + require(id != 0, "id is the zero bytes"); Node storage n = tree[id]; - require(_isEmpty(n), "leaf already populated"); + require(_isEmpty(n), "leaf is not empty"); n.offer = offer; n.hashNode = id; } From d77d0b3994c91d764acfdc3038135dd29cae1220 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 26 May 2026 00:37:47 +0200 Subject: [PATCH 20/38] add checker --- certora/checker/Checker.sol | 371 ++++++++++++++++++++++++++ certora/checker/create_certificate.py | 275 +++++++++++++++++++ 2 files changed, 646 insertions(+) create mode 100644 certora/checker/Checker.sol create mode 100644 certora/checker/create_certificate.py diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol new file mode 100644 index 000000000..fe41dff06 --- /dev/null +++ b/certora/checker/Checker.sol @@ -0,0 +1,371 @@ +// 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, Market, CollateralParams} from "../../src/interfaces/IMidnight.sol"; +import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; +import {EIP712_DOMAIN_TYPEHASH} from "../../src/ratifiers/interfaces/IEcrecoverRatifier.sol"; + +contract Checker is Test { + using stdJson for string; + + struct Eip712Envelope { + address ratifier; + uint256 chainId; + uint256 height; + address signer; + uint8 v; + bytes32 r; + bytes32 s; + } + + // Rebuild a dense tree level-by-level via the verified `newLeaf` and + // `newInternalNode` primitives and assert the top hash matches `root`. + // Inserts are skipped when the target slot is already populated, so duplicate + // leaves (e.g. an `emptyOffer` repeated across padding slots) collapse into a + // single helper slot. + function _verifyDense(Offer[] memory leaves, bytes32 root) internal { + require(leaves.length > 0, "no leaves"); + require((leaves.length & (leaves.length - 1)) == 0, "leaves length not power of two"); + + OfferTree tree = new OfferTree(); + + bytes32[] memory level = new bytes32[](leaves.length); + for (uint256 i = 0; i < leaves.length; i++) { + bytes32 leafHash = HashLib.hashOffer(leaves[i]); + if (tree.isEmpty(leafHash)) tree.newLeaf(leaves[i]); + level[i] = leafHash; + } + + while (level.length > 1) { + uint256 half = level.length / 2; + bytes32[] memory next = new bytes32[](half); + for (uint256 i = 0; i < half; i++) { + bytes32 leftHash = level[2 * i]; + bytes32 rightHash = level[2 * i + 1]; + bytes32 nodeHash = HashLib.hashNode(leftHash, rightHash); + if (tree.isEmpty(nodeHash)) tree.newInternalNode(nodeHash, leftHash, rightHash); + next[i] = nodeHash; + } + level = next; + } + + assertEq(level[0], root, "dense: root mismatch"); + } + + // Internal nodes must be supplied in topological order (children before parents). + // The last id is taken as the root. + function _verifySparse( + Offer[] memory leaves, + bytes32[] memory nodeIds, + bytes32[] memory nodeLefts, + bytes32[] memory nodeRights, + bytes32 root + ) internal { + require(nodeIds.length == nodeLefts.length, "node arrays length mismatch"); + require(nodeIds.length == nodeRights.length, "node arrays length mismatch"); + require(nodeIds.length > 0, "no internal nodes"); + + OfferTree tree = new OfferTree(); + + for (uint256 i = 0; i < leaves.length; i++) { + bytes32 leafHash = HashLib.hashOffer(leaves[i]); + if (tree.isEmpty(leafHash)) tree.newLeaf(leaves[i]); + } + for (uint256 i = 0; i < nodeIds.length; i++) { + if (tree.isEmpty(nodeIds[i])) { + tree.newInternalNode(nodeIds[i], nodeLefts[i], nodeRights[i]); + } + } + + bytes32 rootId = nodeIds[nodeIds.length - 1]; + assertEq(tree.getHash(rootId), root, "sparse: root mismatch"); + } + + // Mirrors EcrecoverRatifier.isRatified: structHash wraps the offer-tree typehash + // and root, the domain separator binds (chainId, ratifier), and the digest is the + // standard EIP-712 form. + function _verifyEip712(bytes32 root, Eip712Envelope memory env) internal { + bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(env.height), root)); + bytes32 domainSeparator = + keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, env.chainId, env.ratifier)); + bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); + address recovered = ecrecover(digest, env.v, env.r, env.s); + require(recovered != address(0), "eip712: invalid signature"); + assertEq(recovered, env.signer, "eip712: signer mismatch"); + } + + function _maybeVerifyEip712(string memory json, bytes32 root, uint256 leafLength) internal { + if (!json.keyExists(".eip712")) return; + + Eip712Envelope memory env; + env.ratifier = json.readAddress(".eip712.ratifier"); + env.chainId = json.readUint(".eip712.chainId"); + env.height = json.readUint(".eip712.height"); + env.signer = json.readAddress(".eip712.signer"); + env.v = uint8(json.readUint(".eip712.v")); + env.r = json.readBytes32(".eip712.r"); + env.s = json.readBytes32(".eip712.s"); + + require(1 << env.height == leafLength, "eip712: height does not match leaf count"); + _verifyEip712(root, env); + } + + 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); + string memory mode = json.readString(".mode"); + 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)); + } + + bytes32 modeHash = keccak256(bytes(mode)); + if (modeHash == keccak256("dense")) { + _verifyDense(leaves, root); + _maybeVerifyEip712(json, root, leafLength); + } else if (modeHash == keccak256("sparse")) { + uint256 nodeLength = json.readUint(".nodeLength"); + bytes32[] memory ids = new bytes32[](nodeLength); + bytes32[] memory lefts = new bytes32[](nodeLength); + bytes32[] memory rights = new bytes32[](nodeLength); + for (uint256 i = 0; i < nodeLength; i++) { + string memory base = string.concat(".node[", vm.toString(i), "]"); + ids[i] = json.readBytes32(string.concat(base, ".id")); + lefts[i] = json.readBytes32(string.concat(base, ".left")); + rights[i] = json.readBytes32(string.concat(base, ".right")); + } + _verifySparse(leaves, ids, lefts, rights, root); + } else { + revert("unknown certificate mode"); + } + } + + function testSyntheticDenseHeight2() public { + Offer[] memory leaves = new Offer[](4); + for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); + + bytes32 h0 = HashLib.hashOffer(leaves[0]); + bytes32 h1 = HashLib.hashOffer(leaves[1]); + bytes32 h2 = HashLib.hashOffer(leaves[2]); + bytes32 h3 = HashLib.hashOffer(leaves[3]); + bytes32 leftBranch = HashLib.hashNode(h0, h1); + bytes32 rightBranch = HashLib.hashNode(h2, h3); + bytes32 root = HashLib.hashNode(leftBranch, rightBranch); + + _verifyDense(leaves, root); + } + + function testSyntheticDenseHeight2DetectsRootMismatch() public { + Offer[] memory leaves = new Offer[](4); + for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); + + vm.expectRevert(); + this.externalVerifyDense(leaves, bytes32(uint256(0xdeadbeef))); + } + + function testSyntheticDenseHeight2WithEmptyPadding() public { + Offer memory emptyOffer; + Offer memory real = _dummyOffer(42); + + Offer[] memory leaves = new Offer[](4); + leaves[0] = real; + leaves[1] = emptyOffer; + leaves[2] = emptyOffer; + leaves[3] = emptyOffer; + + bytes32 hReal = HashLib.hashOffer(real); + bytes32 hEmpty = HashLib.hashOffer(emptyOffer); + bytes32 leftBranch = HashLib.hashNode(hReal, hEmpty); + bytes32 rightBranch = HashLib.hashNode(hEmpty, hEmpty); + bytes32 root = HashLib.hashNode(leftBranch, rightBranch); + + _verifyDense(leaves, root); + } + + function testSyntheticDenseHeight2AllEmpty() public { + Offer memory emptyOffer; + + Offer[] memory leaves = new Offer[](4); + leaves[0] = emptyOffer; + leaves[1] = emptyOffer; + leaves[2] = emptyOffer; + leaves[3] = emptyOffer; + + bytes32 hEmpty = HashLib.hashOffer(emptyOffer); + bytes32 inner = HashLib.hashNode(hEmpty, hEmpty); + bytes32 root = HashLib.hashNode(inner, inner); + + _verifyDense(leaves, root); + } + + function testSyntheticEip712Height2() public { + Offer[] memory leaves = new Offer[](4); + for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); + + bytes32 h0 = HashLib.hashOffer(leaves[0]); + bytes32 h1 = HashLib.hashOffer(leaves[1]); + bytes32 h2 = HashLib.hashOffer(leaves[2]); + bytes32 h3 = HashLib.hashOffer(leaves[3]); + bytes32 root = HashLib.hashNode(HashLib.hashNode(h0, h1), HashLib.hashNode(h2, h3)); + + address ratifier = address(uint160(0xA17F1E7)); + uint256 chainId = 1; + uint256 height = 2; + uint256 privateKey = 0xA11CE; + + bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); + bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); + bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + _verifyDense(leaves, root); + _verifyEip712( + root, + Eip712Envelope({ + ratifier: ratifier, + chainId: chainId, + height: height, + signer: vm.addr(privateKey), + v: v, + r: r, + s: s + }) + ); + } + + function testSyntheticEip712DetectsSignerMismatch() public { + Offer[] memory leaves = new Offer[](2); + leaves[0] = _dummyOffer(300); + leaves[1] = _dummyOffer(301); + + bytes32 root = HashLib.hashNode(HashLib.hashOffer(leaves[0]), HashLib.hashOffer(leaves[1])); + + address ratifier = address(uint160(0xA17F1E7)); + uint256 chainId = 1; + uint256 height = 1; + + bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); + bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); + bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(uint256(0xB0B), digest); + + Eip712Envelope memory env = Eip712Envelope({ + ratifier: ratifier, + chainId: chainId, + height: height, + signer: vm.addr(uint256(0xDEADBEEF)), + v: v, + r: r, + s: s + }); + + vm.expectRevert(); + this.externalVerifyEip712(root, env); + } + + function testSyntheticEip712DetectsWrongRoot() public { + Offer[] memory leaves = new Offer[](2); + leaves[0] = _dummyOffer(400); + leaves[1] = _dummyOffer(401); + + bytes32 root = HashLib.hashNode(HashLib.hashOffer(leaves[0]), HashLib.hashOffer(leaves[1])); + + address ratifier = address(uint160(0xA17F1E7)); + uint256 chainId = 1; + uint256 height = 1; + uint256 privateKey = 0xC0FFEE; + + bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); + bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); + bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + Eip712Envelope memory env = Eip712Envelope({ + ratifier: ratifier, + chainId: chainId, + height: height, + signer: vm.addr(privateKey), + v: v, + r: r, + s: s + }); + + vm.expectRevert(); + this.externalVerifyEip712(keccak256(abi.encode(root, "tamper")), env); + } + + function testSyntheticSparseTwoLeaves() public { + Offer[] memory leaves = new Offer[](2); + leaves[0] = _dummyOffer(100); + leaves[1] = _dummyOffer(101); + + bytes32 leftHash = HashLib.hashOffer(leaves[0]); + bytes32 rightHash = HashLib.hashOffer(leaves[1]); + bytes32 root = HashLib.hashNode(leftHash, rightHash); + + bytes32[] memory ids = new bytes32[](1); + bytes32[] memory lefts = new bytes32[](1); + bytes32[] memory rights = new bytes32[](1); + ids[0] = root; + lefts[0] = leftHash; + rights[0] = rightHash; + + _verifySparse(leaves, ids, lefts, rights, root); + } + + function testSyntheticSparseDepth2OneActivePath() public { + Offer[] memory leaves = new Offer[](3); + leaves[0] = _dummyOffer(200); + leaves[1] = _dummyOffer(201); + leaves[2] = _dummyOffer(202); + + bytes32 h0 = HashLib.hashOffer(leaves[0]); + bytes32 h1 = HashLib.hashOffer(leaves[1]); + bytes32 hUncle = HashLib.hashOffer(leaves[2]); + bytes32 leftBranch = HashLib.hashNode(h0, h1); + bytes32 root = HashLib.hashNode(leftBranch, hUncle); + + bytes32[] memory ids = new bytes32[](2); + bytes32[] memory lefts = new bytes32[](2); + bytes32[] memory rights = new bytes32[](2); + + ids[0] = leftBranch; + lefts[0] = h0; + rights[0] = h1; + ids[1] = root; + lefts[1] = leftBranch; + rights[1] = hUncle; + + _verifySparse(leaves, ids, lefts, rights, root); + } + + // External wrappers so `vm.expectRevert` can catch internal-call reverts. + function externalVerifyDense(Offer[] memory leaves, bytes32 root) external { + _verifyDense(leaves, root); + } + + function externalVerifyEip712(bytes32 root, Eip712Envelope memory env) external { + _verifyEip712(root, env); + } + + // Distinct dummy offers, distinguished by `tick`. + function _dummyOffer(uint256 nonce) internal pure returns (Offer memory o) { + o.market.loanToken = address(uint160(0x1000 + nonce)); + o.market.collateralParams = new CollateralParams[](0); + o.maker = address(uint160(0x2000 + nonce)); + o.tick = nonce; + o.maxUnits = 1; + o.maxAssets = 1; + } +} diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py new file mode 100644 index 000000000..5982af4d7 --- /dev/null +++ b/certora/checker/create_certificate.py @@ -0,0 +1,275 @@ +import json +import sys + +from eth_abi import encode +from eth_account import Account +from web3 import EthereumTesterProvider, Web3 + +w3 = Web3(EthereumTesterProvider()) + +# keccak256("EIP712Domain(uint256 chainId,address verifyingContract)"). +EIP712_DOMAIN_TYPEHASH = bytes.fromhex( + "47e79534a245952e8b16893a336b85a3d9ea9fa8c573f3d803afb92a79469218" +) + +# Precomputed offerTreeTypeHash(h) for h in 0..20; mirrors HashLib.offerTreeTypeHash. +OFFER_TREE_TYPE_HASHES = [ + "2b9ee710e1977dfc5778fe18c905ccc1d9e144baf3ba83be732d4da65ecb73e3", + "3cc16189b92a85898f1d5c6e87282c8ded7c1c93b2323d5e85ae10c5f4b2b220", + "6de37d3e570afa293a8107d4b6b1d9547616c04f42164d009c89194787b2ffa6", + "ba3ea2ddfbf40a906fcd1b9506dbd344c062e8dcba8b5c902ceb13339f45a358", + "e5faa865e93bc1b7b8fdf91980f54682d649683b014edd6c54b642f5a0c96977", + "eda50f61dd2a827c6ff9fbfcd54335628dcaa78aaa4f2d118c60886219cdce2b", + "54e2c9cc40cdc0e9ad530cf2be298f952f57af2b18b02f88274a9bbab359d23a", + "c9d81859d60d6b21c688f4be93ca83e3be222728bb156ef5f4cf497f879f1e29", + "d59b0c4544e0c60c8611eab0aaa402575f14ee784d22289c5d57f48c422a62d6", + "ccad21701f34f08bb8398a3dbc77e20e4c9c424930f3a8b31485bf059e2bdb20", + "8a42dfb49807647bfc49c906aef322aa0239d40e4cb675761e141bc7bfa530da", + "2adc0d948b2e3ecb642661590d2eec36d4e71e9acf382deb6574371800caf198", + "f5845dfaed016de272342f346346a49d4b1694f622144d420558a38e46ac9dad", + "3d7df854e6294bf433b64bbb8d0a82fa875a87b45b0016db27fc5752e54126ad", + "72a991a101708716ff427c524404ab44f4d4d1f4e7e76c0ae8b967222164b348", + "762c88fc52cf78a54401d247790f1bdb619d51d3458d1415c20d1422197cecc4", + "8ede2209e94c8d5f8379d733dc8712b71a3888c1c4b70f3d6b22285f70bf4286", + "425b18f07b3ac2f641977d2c294590565dd40b5d8414610568dca64628399975", + "7e7d98718c0180e882e5963b9bd49810096912c273dfa38d8afdd6d39fde86ec", + "8d35d491a29d846489e19688efff3c4cc7dbd54458058d49b30294074539f0b9", + "824e385eea1953bcbc783bf900b18aa6fba129b6908765e986cf0968b491ec4f", +] + +# 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" + ")" +) + + +def offer_tree_typehash(height): + if not 0 <= height <= 20: + raise ValueError(f"offer-tree height out of range: {height}") + return bytes.fromhex(OFFER_TREE_TYPE_HASHES[height]) + + +def _bytes32(v): + raw = bytes.fromhex(v.removeprefix("0x")) + assert len(raw) == 32, f"expected 32 bytes, got {len(raw)}" + return raw + + +def _hexbytes(v): + return bytes.fromhex(v.removeprefix("0x")) + + +# 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() + + +# Returns the hash of an offer (mirrors HashLib.hashOffer). +def hash_offer(o): + raw = bytes.fromhex(abi_encode_offer(o)[2:]) + return w3.to_hex(w3.solidity_keccak(["bytes"], [raw])) + + +# Returns the hash of a node given the hashes of its children. +def hash_node(left, right): + return w3.to_hex( + w3.solidity_keccak(["bytes32", "bytes32"], [_bytes32(left), _bytes32(right)]) + ) + + +# Builds a dense certificate from a power-of-two list of offers, in leftIndex order. +def build_dense(leaves, claimed_root): + n = len(leaves) + assert n > 0 and (n & (n - 1)) == 0, "dense leaves count must be a power of two" + + level = [hash_offer(o) for o in leaves] + while len(level) > 1: + level = [hash_node(level[2 * i], level[2 * i + 1]) for i in range(len(level) // 2)] + assert level[0].lower() == claimed_root.lower(), ( + f"dense: computed root {level[0]} != claimed root {claimed_root}" + ) + + return { + "mode": "dense", + "root": claimed_root, + "leafLength": n, + "leaf": [abi_encode_offer(o) for o in leaves], + } + + +# Builds a sparse certificate by walking each leaf's proof up to the root. +# Every sibling must resolve to another supplied leaf or a derivable internal node. +def build_sparse(entries, claimed_root): + nodes = {} + leaf_payloads = [] + + for entry in entries: + offer = entry["offer"] + idx = int(entry["leafIndex"]) + proof = entry["proof"] + leaf_hash = hash_offer(offer) + leaf_payloads.append((leaf_hash, offer)) + + current = leaf_hash + for i, sibling in enumerate(proof): + bit = (idx >> i) & 1 + left_id, right_id = (current, sibling) if bit == 0 else (sibling, current) + parent = hash_node(left_id, right_id) + nodes.setdefault(parent, (left_id, right_id)) + current = parent + assert current.lower() == claimed_root.lower(), ( + f"sparse: proof for leafIndex={idx} ends at {current}, not claimed root {claimed_root}" + ) + + leaf_ids = {h.lower() for (h, _) in leaf_payloads} + node_ids_lc = {n.lower() for n in nodes} + + for nid, (left_id, right_id) in nodes.items(): + for child_id, side in ((left_id, "left"), (right_id, "right")): + if child_id.lower() not in leaf_ids and child_id.lower() not in node_ids_lc: + raise ValueError( + f"sparse: {side} child {child_id} of internal node {nid} is neither a " + f"supplied leaf nor a derivable internal node." + ) + + emitted = set(leaf_ids) + pending = list(nodes.keys()) + ordered = [] + while pending: + next_pending = [] + progressed = False + for nid in pending: + left_id, right_id = nodes[nid] + if left_id.lower() in emitted and right_id.lower() in emitted: + ordered.append(nid) + emitted.add(nid.lower()) + progressed = True + else: + next_pending.append(nid) + if not progressed: + raise RuntimeError("topological sort failed; cycles or unresolved siblings") + pending = next_pending + + assert ordered[-1].lower() == claimed_root.lower(), ( + f"sparse: last emitted node {ordered[-1]} is not claimed root {claimed_root}" + ) + + return { + "mode": "sparse", + "root": claimed_root, + "leafLength": len(leaf_payloads), + "leaf": [abi_encode_offer(offer) for (_, offer) in leaf_payloads], + "nodeLength": len(ordered), + "node": [ + {"id": nid, "left": nodes[nid][0], "right": nodes[nid][1]} for nid in ordered + ], + } + + +# Reconstructs the EIP-712 digest for an OfferTree and either signs it locally +# (`signerKey`) or accepts a precomputed (signer, v, r, s). +def build_eip712(eip712_in, root, leaf_length): + ratifier = w3.to_checksum_address(eip712_in["ratifier"]) + chain_id = int(eip712_in["chainId"]) + height = (leaf_length - 1).bit_length() + if 1 << height != leaf_length: + raise ValueError( + f"eip712 requires a balanced tree; leafLength {leaf_length} is not a power of two" + ) + + struct_hash = w3.solidity_keccak( + ["bytes32", "bytes32"], [offer_tree_typehash(height), _bytes32(root)] + ) + domain_separator = w3.solidity_keccak( + ["bytes32", "uint256", "address"], [EIP712_DOMAIN_TYPEHASH, chain_id, ratifier] + ) + digest = w3.solidity_keccak( + ["bytes1", "bytes1", "bytes32", "bytes32"], + [b"\x19", b"\x01", domain_separator, struct_hash], + ) + + if "signerKey" in eip712_in: + signed = Account._sign_hash(digest, eip712_in["signerKey"]) + signer = Account.from_key(eip712_in["signerKey"]).address + v, r, s = signed.v, signed.r.to_bytes(32, "big"), signed.s.to_bytes(32, "big") + else: + signer = w3.to_checksum_address(eip712_in["signer"]) + v = int(eip712_in["v"]) + r = _bytes32(eip712_in["r"]) + s = _bytes32(eip712_in["s"]) + + return { + "ratifier": ratifier, + "chainId": chain_id, + "height": height, + "signer": signer, + "v": v, + "r": "0x" + r.hex(), + "s": "0x" + s.hex(), + } + + +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) + + mode = proofs["mode"] + root = proofs["root"] + if mode == "dense": + certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], root) + elif mode == "sparse": + certificate = build_sparse(proofs["leaves"], root) + else: + raise ValueError(f"unknown mode: {mode}") + + if "eip712" in proofs: + if mode != "dense": + raise ValueError("eip712 envelope is only supported for dense (balanced) trees") + certificate["eip712"] = build_eip712(proofs["eip712"], root, certificate["leafLength"]) + + with open("certificate.json", "w") as f: + json.dump(certificate, f, indent=2) + + +if __name__ == "__main__": + main() From 939a570f4af022b685b24594826c6438689be41e Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 26 May 2026 00:38:18 +0200 Subject: [PATCH 21/38] add checker --- foundry.toml | 5 +++++ 1 file changed, 5 insertions(+) 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", From d9f174e5fd54d1119eb19206eafe52daccdc17b9 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 26 May 2026 00:38:50 +0200 Subject: [PATCH 22/38] summarise isRatify --- certora/specs/OfferTreeMembership.spec | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index dd1e00c45..b0548ce3b 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -14,14 +14,16 @@ methods { function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.hashNode(bytes32, bytes32) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; + function Utils.callbackSuccess() external returns (bytes32) envfree; // Align the merkle verification and the helper's well-formedness on the same hash functions. function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); - // Take-side externals are irrelevant to merkle membership. `isRatified` is NONDET'd so the rule - // abstracts over the ratifier choice; the bridge to `Utils.isLeaf` is supplied in the rule body. - function _.isRatified(Midnight.Offer, bytes) external => NONDET; + // A successful ratifier must witness a merkle proof for the offer's hash. The + // obligation is discharged in Ratification.spec/isRatifiedRequiresIsLeaf, which + // dispatches across all linked ratifier implementations. + function _.isRatified(Midnight.Offer offer, bytes) external => isRatifiedSummary(offer) expect bytes32; 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; @@ -45,6 +47,15 @@ function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { return Utils.hashNode(a, b); } +function isRatifiedSummary(Midnight.Offer offer) returns bytes32 { + bytes32 result; + bytes32 root; + uint256 leafIndex; + bytes32[] proof; + require result == Utils.callbackSuccess() => Utils.isLeaf(root, Utils.hashOffer(offer), leafIndex, proof); + return result; +} + /// SOUNDNESS /// /// If a root corresponds to a node of a well-formed offer-tree, a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. @@ -66,7 +77,7 @@ rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, byte /// TAKE-LEVEL LIFT /// /// Every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. -/// The `require Utils.isLeaf(...)` below is the bridge from take to the merkle check, justified by composition: take requires `isRatified(...) == CALLBACK_SUCCESS`, and both SetterRatifier and EcrecoverRatifier require HashLib.isLeaf to pass. +/// `require Utils.isLeaf(...)` binds the merkle witness to the specific (root, leafIndex, proof) used in the well-formedness premise; the take->ratifier->merkle composition is mechanised via the `isRatifiedSummary` above (obligation discharged in Ratification.spec/isRatifiedRequiresIsLeaf). rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, uint256 leafIndex, bytes32[] proof) { bytes32 node; require OfferTree.getHash(node) == root, "root is the hash of node"; From fc758a3686c0332700e2165d5253eb0d9e240aec Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 26 May 2026 14:41:18 +0200 Subject: [PATCH 23/38] trimmed down to core properties --- certora/checker/Checker.sol | 179 +------------------------ certora/checker/create_certificate.py | 80 +---------- certora/confs/SetterRatification.conf | 23 ---- certora/helpers/OfferTree.sol | 8 -- certora/specs/OfferTreeMembership.spec | 19 --- certora/specs/SetterRatification.spec | 56 -------- 6 files changed, 4 insertions(+), 361 deletions(-) delete mode 100644 certora/confs/SetterRatification.conf delete mode 100644 certora/specs/SetterRatification.spec diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol index fe41dff06..c57021782 100644 --- a/certora/checker/Checker.sol +++ b/certora/checker/Checker.sol @@ -57,35 +57,6 @@ contract Checker is Test { assertEq(level[0], root, "dense: root mismatch"); } - // Internal nodes must be supplied in topological order (children before parents). - // The last id is taken as the root. - function _verifySparse( - Offer[] memory leaves, - bytes32[] memory nodeIds, - bytes32[] memory nodeLefts, - bytes32[] memory nodeRights, - bytes32 root - ) internal { - require(nodeIds.length == nodeLefts.length, "node arrays length mismatch"); - require(nodeIds.length == nodeRights.length, "node arrays length mismatch"); - require(nodeIds.length > 0, "no internal nodes"); - - OfferTree tree = new OfferTree(); - - for (uint256 i = 0; i < leaves.length; i++) { - bytes32 leafHash = HashLib.hashOffer(leaves[i]); - if (tree.isEmpty(leafHash)) tree.newLeaf(leaves[i]); - } - for (uint256 i = 0; i < nodeIds.length; i++) { - if (tree.isEmpty(nodeIds[i])) { - tree.newInternalNode(nodeIds[i], nodeLefts[i], nodeRights[i]); - } - } - - bytes32 rootId = nodeIds[nodeIds.length - 1]; - assertEq(tree.getHash(rootId), root, "sparse: root mismatch"); - } - // Mirrors EcrecoverRatifier.isRatified: structHash wraps the offer-tree typehash // and root, the domain separator binds (chainId, ratifier), and the digest is the // standard EIP-712 form. @@ -120,7 +91,6 @@ contract Checker is Test { if (!vm.exists(path)) vm.skip(true, "no certificate.json at project root"); string memory json = vm.readFile(path); - string memory mode = json.readString(".mode"); bytes32 root = json.readBytes32(".root"); uint256 leafLength = json.readUint(".leafLength"); @@ -130,25 +100,8 @@ contract Checker is Test { leaves[i] = abi.decode(enc, (Offer)); } - bytes32 modeHash = keccak256(bytes(mode)); - if (modeHash == keccak256("dense")) { - _verifyDense(leaves, root); - _maybeVerifyEip712(json, root, leafLength); - } else if (modeHash == keccak256("sparse")) { - uint256 nodeLength = json.readUint(".nodeLength"); - bytes32[] memory ids = new bytes32[](nodeLength); - bytes32[] memory lefts = new bytes32[](nodeLength); - bytes32[] memory rights = new bytes32[](nodeLength); - for (uint256 i = 0; i < nodeLength; i++) { - string memory base = string.concat(".node[", vm.toString(i), "]"); - ids[i] = json.readBytes32(string.concat(base, ".id")); - lefts[i] = json.readBytes32(string.concat(base, ".left")); - rights[i] = json.readBytes32(string.concat(base, ".right")); - } - _verifySparse(leaves, ids, lefts, rights, root); - } else { - revert("unknown certificate mode"); - } + _verifyDense(leaves, root); + _maybeVerifyEip712(json, root, leafLength); } function testSyntheticDenseHeight2() public { @@ -193,22 +146,6 @@ contract Checker is Test { _verifyDense(leaves, root); } - function testSyntheticDenseHeight2AllEmpty() public { - Offer memory emptyOffer; - - Offer[] memory leaves = new Offer[](4); - leaves[0] = emptyOffer; - leaves[1] = emptyOffer; - leaves[2] = emptyOffer; - leaves[3] = emptyOffer; - - bytes32 hEmpty = HashLib.hashOffer(emptyOffer); - bytes32 inner = HashLib.hashNode(hEmpty, hEmpty); - bytes32 root = HashLib.hashNode(inner, inner); - - _verifyDense(leaves, root); - } - function testSyntheticEip712Height2() public { Offer[] memory leaves = new Offer[](4); for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); @@ -244,121 +181,11 @@ contract Checker is Test { ); } - function testSyntheticEip712DetectsSignerMismatch() public { - Offer[] memory leaves = new Offer[](2); - leaves[0] = _dummyOffer(300); - leaves[1] = _dummyOffer(301); - - bytes32 root = HashLib.hashNode(HashLib.hashOffer(leaves[0]), HashLib.hashOffer(leaves[1])); - - address ratifier = address(uint160(0xA17F1E7)); - uint256 chainId = 1; - uint256 height = 1; - - bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); - bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); - bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); - (uint8 v, bytes32 r, bytes32 s) = vm.sign(uint256(0xB0B), digest); - - Eip712Envelope memory env = Eip712Envelope({ - ratifier: ratifier, - chainId: chainId, - height: height, - signer: vm.addr(uint256(0xDEADBEEF)), - v: v, - r: r, - s: s - }); - - vm.expectRevert(); - this.externalVerifyEip712(root, env); - } - - function testSyntheticEip712DetectsWrongRoot() public { - Offer[] memory leaves = new Offer[](2); - leaves[0] = _dummyOffer(400); - leaves[1] = _dummyOffer(401); - - bytes32 root = HashLib.hashNode(HashLib.hashOffer(leaves[0]), HashLib.hashOffer(leaves[1])); - - address ratifier = address(uint160(0xA17F1E7)); - uint256 chainId = 1; - uint256 height = 1; - uint256 privateKey = 0xC0FFEE; - - bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); - bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); - bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); - (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); - - Eip712Envelope memory env = Eip712Envelope({ - ratifier: ratifier, - chainId: chainId, - height: height, - signer: vm.addr(privateKey), - v: v, - r: r, - s: s - }); - - vm.expectRevert(); - this.externalVerifyEip712(keccak256(abi.encode(root, "tamper")), env); - } - - function testSyntheticSparseTwoLeaves() public { - Offer[] memory leaves = new Offer[](2); - leaves[0] = _dummyOffer(100); - leaves[1] = _dummyOffer(101); - - bytes32 leftHash = HashLib.hashOffer(leaves[0]); - bytes32 rightHash = HashLib.hashOffer(leaves[1]); - bytes32 root = HashLib.hashNode(leftHash, rightHash); - - bytes32[] memory ids = new bytes32[](1); - bytes32[] memory lefts = new bytes32[](1); - bytes32[] memory rights = new bytes32[](1); - ids[0] = root; - lefts[0] = leftHash; - rights[0] = rightHash; - - _verifySparse(leaves, ids, lefts, rights, root); - } - - function testSyntheticSparseDepth2OneActivePath() public { - Offer[] memory leaves = new Offer[](3); - leaves[0] = _dummyOffer(200); - leaves[1] = _dummyOffer(201); - leaves[2] = _dummyOffer(202); - - bytes32 h0 = HashLib.hashOffer(leaves[0]); - bytes32 h1 = HashLib.hashOffer(leaves[1]); - bytes32 hUncle = HashLib.hashOffer(leaves[2]); - bytes32 leftBranch = HashLib.hashNode(h0, h1); - bytes32 root = HashLib.hashNode(leftBranch, hUncle); - - bytes32[] memory ids = new bytes32[](2); - bytes32[] memory lefts = new bytes32[](2); - bytes32[] memory rights = new bytes32[](2); - - ids[0] = leftBranch; - lefts[0] = h0; - rights[0] = h1; - ids[1] = root; - lefts[1] = leftBranch; - rights[1] = hUncle; - - _verifySparse(leaves, ids, lefts, rights, root); - } - - // External wrappers so `vm.expectRevert` can catch internal-call reverts. + // External wrapper so `vm.expectRevert` can catch internal-call reverts. function externalVerifyDense(Offer[] memory leaves, bytes32 root) external { _verifyDense(leaves, root); } - function externalVerifyEip712(bytes32 root, Eip712Envelope memory env) external { - _verifyEip712(root, env); - } - // Distinct dummy offers, distinguished by `tick`. function _dummyOffer(uint256 nonce) internal pure returns (Offer memory o) { o.market.loanToken = address(uint160(0x1000 + nonce)); diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py index 5982af4d7..0766ef8a9 100644 --- a/certora/checker/create_certificate.py +++ b/certora/checker/create_certificate.py @@ -126,82 +126,12 @@ def build_dense(leaves, claimed_root): ) return { - "mode": "dense", "root": claimed_root, "leafLength": n, "leaf": [abi_encode_offer(o) for o in leaves], } -# Builds a sparse certificate by walking each leaf's proof up to the root. -# Every sibling must resolve to another supplied leaf or a derivable internal node. -def build_sparse(entries, claimed_root): - nodes = {} - leaf_payloads = [] - - for entry in entries: - offer = entry["offer"] - idx = int(entry["leafIndex"]) - proof = entry["proof"] - leaf_hash = hash_offer(offer) - leaf_payloads.append((leaf_hash, offer)) - - current = leaf_hash - for i, sibling in enumerate(proof): - bit = (idx >> i) & 1 - left_id, right_id = (current, sibling) if bit == 0 else (sibling, current) - parent = hash_node(left_id, right_id) - nodes.setdefault(parent, (left_id, right_id)) - current = parent - assert current.lower() == claimed_root.lower(), ( - f"sparse: proof for leafIndex={idx} ends at {current}, not claimed root {claimed_root}" - ) - - leaf_ids = {h.lower() for (h, _) in leaf_payloads} - node_ids_lc = {n.lower() for n in nodes} - - for nid, (left_id, right_id) in nodes.items(): - for child_id, side in ((left_id, "left"), (right_id, "right")): - if child_id.lower() not in leaf_ids and child_id.lower() not in node_ids_lc: - raise ValueError( - f"sparse: {side} child {child_id} of internal node {nid} is neither a " - f"supplied leaf nor a derivable internal node." - ) - - emitted = set(leaf_ids) - pending = list(nodes.keys()) - ordered = [] - while pending: - next_pending = [] - progressed = False - for nid in pending: - left_id, right_id = nodes[nid] - if left_id.lower() in emitted and right_id.lower() in emitted: - ordered.append(nid) - emitted.add(nid.lower()) - progressed = True - else: - next_pending.append(nid) - if not progressed: - raise RuntimeError("topological sort failed; cycles or unresolved siblings") - pending = next_pending - - assert ordered[-1].lower() == claimed_root.lower(), ( - f"sparse: last emitted node {ordered[-1]} is not claimed root {claimed_root}" - ) - - return { - "mode": "sparse", - "root": claimed_root, - "leafLength": len(leaf_payloads), - "leaf": [abi_encode_offer(offer) for (_, offer) in leaf_payloads], - "nodeLength": len(ordered), - "node": [ - {"id": nid, "left": nodes[nid][0], "right": nodes[nid][1]} for nid in ordered - ], - } - - # Reconstructs the EIP-712 digest for an OfferTree and either signs it locally # (`signerKey`) or accepts a precomputed (signer, v, r, s). def build_eip712(eip712_in, root, leaf_length): @@ -253,18 +183,10 @@ def main(): with open(sys.argv[1]) as f: proofs = json.load(f) - mode = proofs["mode"] root = proofs["root"] - if mode == "dense": - certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], root) - elif mode == "sparse": - certificate = build_sparse(proofs["leaves"], root) - else: - raise ValueError(f"unknown mode: {mode}") + certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], root) if "eip712" in proofs: - if mode != "dense": - raise ValueError("eip712 envelope is only supported for dense (balanced) trees") certificate["eip712"] = build_eip712(proofs["eip712"], root, certificate["leafLength"]) with open("certificate.json", "w") as f: diff --git a/certora/confs/SetterRatification.conf b/certora/confs/SetterRatification.conf deleted file mode 100644 index 61dea9691..000000000 --- a/certora/confs/SetterRatification.conf +++ /dev/null @@ -1,23 +0,0 @@ -{ - "files": [ - "src/Midnight.sol", - "src/ratifiers/SetterRatifier.sol", - "certora/helpers/OfferTree.sol", - "certora/helpers/Utils.sol" - ], - "verify": "Midnight:certora/specs/SetterRatification.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": "SetterRatification" -} diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 4024829d4..03f329363 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -63,14 +63,6 @@ contract OfferTree { return tree[id].left == 0 && tree[id].right == 0 && tree[id].hashNode != 0; } - function getLeft(bytes32 id) public view returns (bytes32) { - return tree[id].left; - } - - function getRight(bytes32 id) public view returns (bytes32) { - return tree[id].right; - } - // The specification of a well-formed tree is the following: // - empty nodes (left == 0 && right == 0 && hashNode == 0) are well-formed // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == hashOffer(offer) and id == hashNode diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index b0548ce3b..fdebf2b1b 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -73,22 +73,3 @@ rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, byte assert OfferTree.isLeafNode(leafId); } - -/// TAKE-LEVEL LIFT /// - -/// Every successful Midnight.take is for an offer registered as a leaf in the maker's offer-tree. -/// `require Utils.isLeaf(...)` binds the merkle witness to the specific (root, leafIndex, proof) used in the well-formedness premise; the take->ratifier->merkle composition is mechanised via the `isRatifiedSummary` above (obligation discharged in Ratification.spec/isRatifiedRequiresIsLeaf). -rule takeImpliesLeafInTree(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, uint256 leafIndex, bytes32[] proof) { - bytes32 node; - require OfferTree.getHash(node) == root, "root is the hash of node"; - require root != to_bytes32(0), "root is non-zero"; - - OfferTree.wellFormedPath(node, leafIndex, proof); - - bytes32 leafId = Utils.hashOffer(offer); - require Utils.isLeaf(root, leafId, leafIndex, proof); - - take(e, offer, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData, ratifierData); - - assert OfferTree.isLeafNode(leafId); -} diff --git a/certora/specs/SetterRatification.spec b/certora/specs/SetterRatification.spec deleted file mode 100644 index 06c4b7c72..000000000 --- a/certora/specs/SetterRatification.spec +++ /dev/null @@ -1,56 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0-or-later -// Copyright (c) 2025 Morpho Association - -using OfferTree as OfferTree; -using Utils as Utils; -using SetterRatifier as SetterRatifier; - -methods { - function OfferTree.getHash(bytes32) external returns (bytes32) envfree; - function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; - function OfferTree.isWellFormed(bytes32) external returns (bool) envfree; - function OfferTree.wellFormedPath(bytes32, uint256, bytes32[]) external returns (bytes32) envfree; - - function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; - function Utils.hashNode(bytes32, bytes32) external returns (bytes32) envfree; - function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - - function SetterRatifier.isRootRatified(address, bytes32) external returns (bool) envfree; - - // Align the merkle verification and the helper's well-formedness on the same hash functions. - // Routing through Utils (`keccak256(abi.encode(...))`) lets Certora's bounded-hash recognition - // supply injectivity automatically, instead of needing a ghost + axiom. - function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); -} - -function summaryHashOffer(Midnight.Offer offer) returns bytes32 { - return Utils.hashOffer(offer); -} - -function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { - return Utils.hashNode(a, b); -} - -// SetterRatifier-specific framing of takeCorrectness. -// Premise: the maker has explicitly committed to `root` via SetterRatifier.setIsRootRatified. Conclusion: every offer whose hash verifies against `root` via merkle proof is registered as a leaf in the maker's committed offer-tree. -rule setterRatifiedTakeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { - bytes32 node; - - // Assume that the maker has explicitly committed to root via SetterRatifier. - require SetterRatifier.isRootRatified(offer.maker, root); - - // Assume that root is the hash of node in the maker's tree. - require OfferTree.getHash(node) == root; - require root != to_bytes32(0); - - // Assume that the tree is well-formed along the proof path from node down to a leaf. - OfferTree.wellFormedPath(node, leafIndex, proof); - - // Compute the leaf hash once so both uses below bind to the same symbolic value. - bytes32 leafId = Utils.hashOffer(offer); - - require Utils.isLeaf(root, leafId, leafIndex, proof); - - assert OfferTree.isLeafNode(leafId); -} From 253e37e14cbc19ba8b4a1bf4686634e5d44a8e1d Mon Sep 17 00:00:00 2001 From: Bhargav Date: Fri, 29 May 2026 16:23:18 +0200 Subject: [PATCH 24/38] removed completeness --- certora/helpers/Utils.sol | 11 +++++-- certora/specs/OfferTreeMembership.spec | 45 +------------------------- certora/specs/Ratification.spec | 9 ++++++ 3 files changed, 18 insertions(+), 47 deletions(-) diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index 1f8aa03d0..fa557338d 100644 --- a/certora/helpers/Utils.sol +++ b/certora/helpers/Utils.sol @@ -15,15 +15,20 @@ 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. Avoids the prior `keccak256(abi.encode(offer))` reimplementation, which is a + // *different* hash than `HashLib.hashOffer` (no typehash prefix, no inner hashing of + // market/callbackData) and broke keccak unification across summary boundaries when the + // prover had to forward-compute the merkle chain (completeness direction). function hashOffer(Offer memory offer) external pure returns (bytes32) { - return keccak256(abi.encode(offer)); + return HashLib.hashOffer(offer); } function hashNode(bytes32 a, bytes32 b) external pure returns (bytes32) { - return keccak256(abi.encode(a, b)); + return HashLib.hashNode(a, b); } function isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index fdebf2b1b..9c3cf014b 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -4,62 +4,19 @@ using OfferTree as OfferTree; using Utils as Utils; methods { - function isAuthorized(address, address) external returns (bool) envfree; - function OfferTree.getHash(bytes32) external returns (bytes32) envfree; function OfferTree.isLeafNode(bytes32) external returns (bool) envfree; - function OfferTree.isWellFormed(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.hashNode(bytes32, bytes32) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - function Utils.callbackSuccess() external returns (bytes32) envfree; - - // Align the merkle verification and the helper's well-formedness on the same hash functions. - function HashLib.hashOffer(Midnight.Offer memory offer) internal returns (bytes32) => summaryHashOffer(offer); - function HashLib.hashNode(bytes32 a, bytes32 b) internal returns (bytes32) => summaryHashNode(a, b); - - // A successful ratifier must witness a merkle proof for the offer's hash. The - // obligation is discharged in Ratification.spec/isRatifiedRequiresIsLeaf, which - // dispatches across all linked ratifier implementations. - function _.isRatified(Midnight.Offer offer, bytes) external => isRatifiedSummary(offer) expect bytes32; - 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; - function multicall(bytes[]) external => HAVOC_ALL DELETE; - 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; - function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; - function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; - function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; - function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; - function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; -} - -function summaryHashOffer(Midnight.Offer offer) returns bytes32 { - return Utils.hashOffer(offer); -} - -function summaryHashNode(bytes32 a, bytes32 b) returns bytes32 { - return Utils.hashNode(a, b); -} -function isRatifiedSummary(Midnight.Offer offer) returns bytes32 { - bytes32 result; - bytes32 root; - uint256 leafIndex; - bytes32[] proof; - require result == Utils.callbackSuccess() => Utils.isLeaf(root, Utils.hashOffer(offer), leafIndex, proof); - return result; } /// SOUNDNESS /// /// If a root corresponds to a node of a well-formed offer-tree, a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. -rule takeCorrectness(Midnight.Offer offer, bytes32 root, uint256 leafIndex, bytes32[] proof) { +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 root != to_bytes32(0), "root is non-zero"; diff --git a/certora/specs/Ratification.spec b/certora/specs/Ratification.spec index 9430ad465..fe3e27fa4 100644 --- a/certora/specs/Ratification.spec +++ b/certora/specs/Ratification.spec @@ -86,3 +86,12 @@ rule isRatifiedRequiresIsLeaf(env e, address ratifierAddr, Midnight.Offer offer, 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, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData, bytes ratifierData) { + require !isLeafReturnedTrue, "fresh capture state"; + + take(e, offer, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData, ratifierData); + + assert isLeafReturnedTrue, "take must have triggered a ratifier that called HashLib.isLeaf returning true"; +} From 89c39d69c92cebd54fddeea356850372accfa424 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 1 Jun 2026 10:00:18 +0200 Subject: [PATCH 25/38] comment style adapted to URD --- certora/helpers/OfferTree.sol | 23 +++++++++++++++-------- certora/specs/OfferTreeMembership.spec | 26 +++++++++++++++++--------- certora/specs/OfferTreeWellFormed.spec | 11 ++++++----- 3 files changed, 38 insertions(+), 22 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 03f329363..a3bd4ea33 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -5,20 +5,26 @@ pragma solidity ^0.8.0; import {Offer} from "../../src/interfaces/IMidnight.sol"; import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; -// Trees are built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by construction. -// Leaves carry the offer payload so `isWellFormed` can pin a leaf's `hashNode` into the image of -// `hashOffer` (distinct keccak input shape from `hashNode`), giving domain separation against internal-node -// hashes for free under Certora's keccak model. contract OfferTree { struct Node { bytes32 left; bytes32 right; Offer offer; + // 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 can have an identifier that is the hash of the offer. + // This ensures that the same offer does not appear twice as a leaf in the tree. + // 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 their offer payload so that `isWellFormed` can recompute `hashOffer` and pin a leaf's `hashNode` into + // the image of `hashOffer`. Because `hashOffer` and `hashNode` feed keccak distinct input shapes, this gives domain + // separation between leaves and internal nodes for free under Certora's keccak model. + // The tree is built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by construction. mapping(bytes32 => Node) internal tree; /* MAIN FUNCTIONS */ @@ -63,11 +69,12 @@ contract OfferTree { return tree[id].left == 0 && tree[id].right == 0 && tree[id].hashNode != 0; } + // The specification of a well-formed tree is the following: - // - empty nodes (left == 0 && right == 0 && hashNode == 0) are well-formed - // - leaves (left == 0 && right == 0 && hashNode != 0) require hashNode == hashOffer(offer) and id == hashNode - // - internal nodes (left != 0 && right != 0) require non-empty children and hashNode = hashNode(left.hashNode, - // right.hashNode) - any other field combination is malformed + // - 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; diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index 9c3cf014b..b8d1abcda 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -10,23 +10,31 @@ methods { function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; - } -/// SOUNDNESS /// - -/// If a root corresponds to a node of a well-formed offer-tree, a successful merkle verification of the offer's hash against that root implies the offer is registered as a leaf in the tree. +// The main correctness result of the verification. +// It ensures that 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 root != to_bytes32(0), "root is non-zero"; + // Assume that root is the hash of node in the tree. + require OfferTree.getHash(node) == root; + + // Assume that the root is non-zero, otherwise empty nodes would hash-match it. + require root != to_bytes32(0); + + // No need to make sure that node is equal to the root: one can pass an internal node instead. + // Assume that the tree is well-formed along the path down to the leaf. OfferTree.wellFormedPath(node, leafIndex, proof); - // Compute leafId once so both uses below bind to the same symbolic hash. + // Compute the leaf identifier once so both uses below bind to the same hash. bytes32 leafId = Utils.hashOffer(offer); - require leafId != to_bytes32(0), "leafId is non-zero"; - require Utils.isLeaf(root, leafId, leafIndex, proof), "merkle proof verifies"; + + // Assume that the leaf identifier is non-zero, matching the constraint enforced by newLeaf. + require leafId != to_bytes32(0); + + // Assume that the Merkle proof verifies the offer's hash against the root. + require Utils.isLeaf(root, leafId, leafIndex, proof); assert OfferTree.isLeafNode(leafId); } diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index c584c5cd6..50b0f4380 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -5,13 +5,14 @@ methods { 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(); - } - } +{ preserved { + requireInvariant zeroIsEmpty(); + } +} From a43f97de4060be479262b758929fd626303610f4 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 1 Jun 2026 14:44:09 +0200 Subject: [PATCH 26/38] retained only testVerifyCertificate in Checker; split offer into static and dynamic part --- certora/checker/Checker.sol | 155 ++++++------------------- certora/checker/create_certificate.py | 140 +++++++++++++++++++--- certora/helpers/OfferTree.sol | 89 ++++++++++++-- certora/specs/OfferTreeWellFormed.spec | 29 ++++- 4 files changed, 263 insertions(+), 150 deletions(-) diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol index c57021782..57dd646a0 100644 --- a/certora/checker/Checker.sol +++ b/certora/checker/Checker.sol @@ -6,7 +6,7 @@ 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, Market, CollateralParams} from "../../src/interfaces/IMidnight.sol"; +import {Offer} from "../../src/interfaces/IMidnight.sol"; import {HashLib} from "../../src/ratifiers/libraries/HashLib.sol"; import {EIP712_DOMAIN_TYPEHASH} from "../../src/ratifiers/interfaces/IEcrecoverRatifier.sol"; @@ -23,54 +23,48 @@ contract Checker is Test { bytes32 s; } - // Rebuild a dense tree level-by-level via the verified `newLeaf` and - // `newInternalNode` primitives and assert the top hash matches `root`. - // Inserts are skipped when the target slot is already populated, so duplicate - // leaves (e.g. an `emptyOffer` repeated across padding slots) collapse into a - // single helper slot. - function _verifyDense(Offer[] memory leaves, bytes32 root) internal { + 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 _verifyCertificate(Offer[] memory leaves, InternalNode[] memory nodes, bytes32 root) internal { require(leaves.length > 0, "no leaves"); - require((leaves.length & (leaves.length - 1)) == 0, "leaves length not power of two"); + require(nodes.length > 0 || leaves.length == 1, "missing internal nodes"); OfferTree tree = new OfferTree(); - bytes32[] memory level = new bytes32[](leaves.length); for (uint256 i = 0; i < leaves.length; i++) { - bytes32 leafHash = HashLib.hashOffer(leaves[i]); - if (tree.isEmpty(leafHash)) tree.newLeaf(leaves[i]); - level[i] = leafHash; + tree.newLeaf(leaves[i]); } - while (level.length > 1) { - uint256 half = level.length / 2; - bytes32[] memory next = new bytes32[](half); - for (uint256 i = 0; i < half; i++) { - bytes32 leftHash = level[2 * i]; - bytes32 rightHash = level[2 * i + 1]; - bytes32 nodeHash = HashLib.hashNode(leftHash, rightHash); - if (tree.isEmpty(nodeHash)) tree.newInternalNode(nodeHash, leftHash, rightHash); - next[i] = nodeHash; - } - level = next; + 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(level[0], root, "dense: root mismatch"); + assertTrue(!tree.isEmpty(rootId), "empty root"); + assertEq(tree.getHash(rootId), root, "mismatched roots"); } // Mirrors EcrecoverRatifier.isRatified: structHash wraps the offer-tree typehash // and root, the domain separator binds (chainId, ratifier), and the digest is the // standard EIP-712 form. - function _verifyEip712(bytes32 root, Eip712Envelope memory env) internal { + function _verifyEip712(bytes32 root, Eip712Envelope memory env) internal pure { bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(env.height), root)); - bytes32 domainSeparator = - keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, env.chainId, env.ratifier)); + bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, env.chainId, env.ratifier)); bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); address recovered = ecrecover(digest, env.v, env.r, env.s); require(recovered != address(0), "eip712: invalid signature"); assertEq(recovered, env.signer, "eip712: signer mismatch"); } - function _maybeVerifyEip712(string memory json, bytes32 root, uint256 leafLength) internal { + function _maybeVerifyEip712(string memory json, bytes32 root) internal view { if (!json.keyExists(".eip712")) return; Eip712Envelope memory env; @@ -82,7 +76,9 @@ contract Checker is Test { env.r = json.readBytes32(".eip712.r"); env.s = json.readBytes32(".eip712.s"); - require(1 << env.height == leafLength, "eip712: height does not match leaf count"); + if (json.keyExists(".treeLeafLength")) { + require(1 << env.height == json.readUint(".treeLeafLength"), "eip712: height does not match leaf count"); + } _verifyEip712(root, env); } @@ -100,99 +96,14 @@ contract Checker is Test { leaves[i] = abi.decode(enc, (Offer)); } - _verifyDense(leaves, root); - _maybeVerifyEip712(json, root, leafLength); - } - - function testSyntheticDenseHeight2() public { - Offer[] memory leaves = new Offer[](4); - for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); - - bytes32 h0 = HashLib.hashOffer(leaves[0]); - bytes32 h1 = HashLib.hashOffer(leaves[1]); - bytes32 h2 = HashLib.hashOffer(leaves[2]); - bytes32 h3 = HashLib.hashOffer(leaves[3]); - bytes32 leftBranch = HashLib.hashNode(h0, h1); - bytes32 rightBranch = HashLib.hashNode(h2, h3); - bytes32 root = HashLib.hashNode(leftBranch, rightBranch); - - _verifyDense(leaves, root); - } - - function testSyntheticDenseHeight2DetectsRootMismatch() public { - Offer[] memory leaves = new Offer[](4); - for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); - - vm.expectRevert(); - this.externalVerifyDense(leaves, bytes32(uint256(0xdeadbeef))); - } - - function testSyntheticDenseHeight2WithEmptyPadding() public { - Offer memory emptyOffer; - Offer memory real = _dummyOffer(42); - - Offer[] memory leaves = new Offer[](4); - leaves[0] = real; - leaves[1] = emptyOffer; - leaves[2] = emptyOffer; - leaves[3] = emptyOffer; - - bytes32 hReal = HashLib.hashOffer(real); - bytes32 hEmpty = HashLib.hashOffer(emptyOffer); - bytes32 leftBranch = HashLib.hashNode(hReal, hEmpty); - bytes32 rightBranch = HashLib.hashNode(hEmpty, hEmpty); - bytes32 root = HashLib.hashNode(leftBranch, rightBranch); - - _verifyDense(leaves, root); - } - - function testSyntheticEip712Height2() public { - Offer[] memory leaves = new Offer[](4); - for (uint256 i = 0; i < 4; i++) leaves[i] = _dummyOffer(i); - - bytes32 h0 = HashLib.hashOffer(leaves[0]); - bytes32 h1 = HashLib.hashOffer(leaves[1]); - bytes32 h2 = HashLib.hashOffer(leaves[2]); - bytes32 h3 = HashLib.hashOffer(leaves[3]); - bytes32 root = HashLib.hashNode(HashLib.hashNode(h0, h1), HashLib.hashNode(h2, h3)); - - address ratifier = address(uint160(0xA17F1E7)); - uint256 chainId = 1; - uint256 height = 2; - uint256 privateKey = 0xA11CE; - - bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(height), root)); - bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, chainId, ratifier)); - bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); - (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); - - _verifyDense(leaves, root); - _verifyEip712( - root, - Eip712Envelope({ - ratifier: ratifier, - chainId: chainId, - height: height, - signer: vm.addr(privateKey), - v: v, - r: r, - s: s - }) - ); - } - - // External wrapper so `vm.expectRevert` can catch internal-call reverts. - function externalVerifyDense(Offer[] memory leaves, bytes32 root) external { - _verifyDense(leaves, root); - } + 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)); + } - // Distinct dummy offers, distinguished by `tick`. - function _dummyOffer(uint256 nonce) internal pure returns (Offer memory o) { - o.market.loanToken = address(uint160(0x1000 + nonce)); - o.market.collateralParams = new CollateralParams[](0); - o.maker = address(uint160(0x2000 + nonce)); - o.tick = nonce; - o.maxUnits = 1; - o.maxAssets = 1; + _verifyCertificate(leaves, nodes, root); + _maybeVerifyEip712(json, root); } } diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py index 0766ef8a9..a920cccd4 100644 --- a/certora/checker/create_certificate.py +++ b/certora/checker/create_certificate.py @@ -3,14 +3,23 @@ from eth_abi import encode from eth_account import Account -from web3 import EthereumTesterProvider, Web3 +from web3 import Web3 -w3 = Web3(EthereumTesterProvider()) +w3 = Web3() # keccak256("EIP712Domain(uint256 chainId,address verifyingContract)"). EIP712_DOMAIN_TYPEHASH = bytes.fromhex( "47e79534a245952e8b16893a336b85a3d9ea9fa8c573f3d803afb92a79469218" ) +COLLATERAL_PARAMS_TYPEHASH = bytes.fromhex( + "af44a88eb50ebdbbebd980e5a23045c44f61ece5f80ab708a1bbe8718102e6af" +) +MARKET_TYPEHASH = bytes.fromhex( + "358117e98511cc3df97175dca58053b06675b43ad090b0553f8a1eff008b6e2e" +) +OFFER_TYPEHASH = bytes.fromhex( + "980a4cfc9766df84667f316d76e10cefc8caf04fb4cd4a9fca00a8e7b34f619c" +) # Precomputed offerTreeTypeHash(h) for h in 0..20; mirrors HashLib.offerTreeTypeHash. OFFER_TREE_TYPE_HASHES = [ @@ -44,6 +53,7 @@ "bool,address,uint256,uint256,uint256,bytes32,address,bytes,address,address,bool,uint256,uint256" ")" ) +INTERNAL_NODE_ABI_TYPE = "(bytes32,bytes32,bytes32)" def offer_tree_typehash(height): @@ -62,6 +72,10 @@ 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"] @@ -100,17 +114,88 @@ def abi_encode_offer(o): 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): - raw = bytes.fromhex(abi_encode_offer(o)[2:]) - return w3.to_hex(w3.solidity_keccak(["bytes"], [raw])) + 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.solidity_keccak(["bytes32", "bytes32"], [_bytes32(left), _bytes32(right)]) - ) + return w3.to_hex(w3.keccak(_bytes32(left) + _bytes32(right))) # Builds a dense certificate from a power-of-two list of offers, in leftIndex order. @@ -118,17 +203,41 @@ def build_dense(leaves, claimed_root): n = len(leaves) assert n > 0 and (n & (n - 1)) == 0, "dense 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) + assert previous == encoded_leaf, "leaf hash collides with a different offer" + while len(level) > 1: - level = [hash_node(level[2 * i], level[2 * i + 1]) for i in range(len(level) // 2)] + next_level = [] + for i in range(len(level) // 2): + left = level[2 * i] + right = level[2 * i + 1] + node_hash = hash_node(left, right) + assert ( + 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) + assert previous == encoded_node, "internal node id collides with different children" + next_level.append(node_hash) + level = next_level + assert level[0].lower() == claimed_root.lower(), ( f"dense: computed root {level[0]} != claimed root {claimed_root}" ) return { "root": claimed_root, - "leafLength": n, - "leaf": [abi_encode_offer(o) for o in leaves], + "treeLeafLength": n, + "leafLength": len(leaf_instructions), + "leaf": list(leaf_instructions.values()), + "nodeLength": len(node_instructions), + "node": list(node_instructions.values()), } @@ -143,16 +252,13 @@ def build_eip712(eip712_in, root, leaf_length): f"eip712 requires a balanced tree; leafLength {leaf_length} is not a power of two" ) - struct_hash = w3.solidity_keccak( + struct_hash = _keccak_abi( ["bytes32", "bytes32"], [offer_tree_typehash(height), _bytes32(root)] ) - domain_separator = w3.solidity_keccak( + domain_separator = _keccak_abi( ["bytes32", "uint256", "address"], [EIP712_DOMAIN_TYPEHASH, chain_id, ratifier] ) - digest = w3.solidity_keccak( - ["bytes1", "bytes1", "bytes32", "bytes32"], - [b"\x19", b"\x01", domain_separator, struct_hash], - ) + digest = w3.keccak(b"\x19\x01" + domain_separator + struct_hash) if "signerKey" in eip712_in: signed = Account._sign_hash(digest, eip712_in["signerKey"]) @@ -187,7 +293,7 @@ def main(): certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], root) if "eip712" in proofs: - certificate["eip712"] = build_eip712(proofs["eip712"], root, certificate["leafLength"]) + certificate["eip712"] = build_eip712(proofs["eip712"], root, certificate["treeLeafLength"]) with open("certificate.json", "w") as f: json.dump(certificate, f, indent=2) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index a3bd4ea33..939a89a73 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -3,13 +3,38 @@ pragma solidity ^0.8.0; import {Offer} from "../../src/interfaces/IMidnight.sol"; -import {HashLib} from "../../src/ratifiers/libraries/HashLib.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; - Offer offer; + Leaf leaf; // hash of the offer for leaves, and of [left.hash, right.hash] for internal nodes. bytes32 hashNode; } @@ -21,10 +46,11 @@ contract OfferTree { // This ensures that the same offer does not appear twice as a leaf in the tree. // 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 their offer payload so that `isWellFormed` can recompute `hashOffer` and pin a leaf's `hashNode` into - // the image of `hashOffer`. Because `hashOffer` and `hashNode` feed keccak distinct input shapes, this gives domain - // separation between leaves and internal nodes for free under Certora's keccak model. - // The tree is built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by construction. + // 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`. Because `hashOffer` and `hashNode` feed keccak distinct + // input shapes, this gives domain separation between leaves and internal nodes for free under Certora's keccak + // model. The tree is built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by + // construction. mapping(bytes32 => Node) internal tree; /* MAIN FUNCTIONS */ @@ -34,7 +60,22 @@ contract OfferTree { require(id != 0, "id is the zero bytes"); Node storage n = tree[id]; require(_isEmpty(n), "leaf is not empty"); - n.offer = offer; + // 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; } @@ -69,6 +110,38 @@ contract OfferTree { 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 _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 @@ -79,7 +152,7 @@ contract OfferTree { Node storage n = tree[id]; if (_isEmpty(n)) return true; if (n.left == 0 && n.right == 0) { - bytes32 expected = HashLib.hashOffer(n.offer); + bytes32 expected = _hashLeaf(n.leaf); return n.hashNode == expected && id == expected; } if (n.left != 0 && n.right != 0) { diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index 50b0f4380..92c5cd575 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -1,6 +1,13 @@ // SPDX-License-Identifier: GPL-2.0-or-later +// No hashing summaries are needed: `Node` stores only the fixed-size pre-image of `hashOffer` (see OfferTree.sol), +// so `isWellFormed` re-hashes a leaf with a single bounded keccak over fixed-size storage — no dynamic-array reads, +// no loops. The only dynamic hashing is `newLeaf` hashing its offer argument once, which is cheap. + methods { + function newLeaf(OfferTree.Offer) external envfree; + function _hashLeaf(bytes32) external returns (bytes32) envfree; + function hashOffer(OfferTree.Offer) external returns (bytes32) envfree; function isEmpty(bytes32) external returns (bool) envfree; function isWellFormed(bytes32) external returns (bool) envfree; } @@ -12,7 +19,23 @@ strong invariant zeroIsEmpty() // 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(); - } + { + preserved { + requireInvariant zeroIsEmpty(); + } + } + +// Focused bridge check: `newLeaf` keys the node by `HashLib.hashOffer(offer)` and stores the fixed-size +// pre-image that `_hashLeaf` re-hashes. This rule catches drift between `_hashLeaf` and the real offer hash +// construction. +rule newLeafConnectsHashLeafToHashOffer(OfferTree.Offer offer) { + bytes32 id = hashOffer(offer); + + require id != to_bytes32(0); + require isEmpty(id); + + newLeaf(offer); + + assert _hashLeaf(id) == id; + assert _hashLeaf(id) == hashOffer(offer); } From 65e69d19b7186d4235671004e06b1ccd2bb275b5 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 1 Jun 2026 15:11:19 +0200 Subject: [PATCH 27/38] removed ratifier --- certora/checker/Checker.sol | 42 -------------- certora/checker/create_certificate.py | 79 --------------------------- 2 files changed, 121 deletions(-) diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol index 57dd646a0..1a5e4445f 100644 --- a/certora/checker/Checker.sol +++ b/certora/checker/Checker.sol @@ -8,21 +8,10 @@ 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"; -import {EIP712_DOMAIN_TYPEHASH} from "../../src/ratifiers/interfaces/IEcrecoverRatifier.sol"; contract Checker is Test { using stdJson for string; - struct Eip712Envelope { - address ratifier; - uint256 chainId; - uint256 height; - address signer; - uint8 v; - bytes32 r; - bytes32 s; - } - struct InternalNode { bytes32 id; bytes32 left; @@ -52,36 +41,6 @@ contract Checker is Test { assertEq(tree.getHash(rootId), root, "mismatched roots"); } - // Mirrors EcrecoverRatifier.isRatified: structHash wraps the offer-tree typehash - // and root, the domain separator binds (chainId, ratifier), and the digest is the - // standard EIP-712 form. - function _verifyEip712(bytes32 root, Eip712Envelope memory env) internal pure { - bytes32 structHash = keccak256(abi.encode(HashLib.offerTreeTypeHash(env.height), root)); - bytes32 domainSeparator = keccak256(abi.encode(EIP712_DOMAIN_TYPEHASH, env.chainId, env.ratifier)); - bytes32 digest = keccak256(bytes.concat(hex"1901", domainSeparator, structHash)); - address recovered = ecrecover(digest, env.v, env.r, env.s); - require(recovered != address(0), "eip712: invalid signature"); - assertEq(recovered, env.signer, "eip712: signer mismatch"); - } - - function _maybeVerifyEip712(string memory json, bytes32 root) internal view { - if (!json.keyExists(".eip712")) return; - - Eip712Envelope memory env; - env.ratifier = json.readAddress(".eip712.ratifier"); - env.chainId = json.readUint(".eip712.chainId"); - env.height = json.readUint(".eip712.height"); - env.signer = json.readAddress(".eip712.signer"); - env.v = uint8(json.readUint(".eip712.v")); - env.r = json.readBytes32(".eip712.r"); - env.s = json.readBytes32(".eip712.s"); - - if (json.keyExists(".treeLeafLength")) { - require(1 << env.height == json.readUint(".treeLeafLength"), "eip712: height does not match leaf count"); - } - _verifyEip712(root, env); - } - 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"); @@ -104,6 +63,5 @@ contract Checker is Test { } _verifyCertificate(leaves, nodes, root); - _maybeVerifyEip712(json, root); } } diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py index a920cccd4..34a99eb30 100644 --- a/certora/checker/create_certificate.py +++ b/certora/checker/create_certificate.py @@ -2,15 +2,10 @@ import sys from eth_abi import encode -from eth_account import Account from web3 import Web3 w3 = Web3() -# keccak256("EIP712Domain(uint256 chainId,address verifyingContract)"). -EIP712_DOMAIN_TYPEHASH = bytes.fromhex( - "47e79534a245952e8b16893a336b85a3d9ea9fa8c573f3d803afb92a79469218" -) COLLATERAL_PARAMS_TYPEHASH = bytes.fromhex( "af44a88eb50ebdbbebd980e5a23045c44f61ece5f80ab708a1bbe8718102e6af" ) @@ -21,31 +16,6 @@ "980a4cfc9766df84667f316d76e10cefc8caf04fb4cd4a9fca00a8e7b34f619c" ) -# Precomputed offerTreeTypeHash(h) for h in 0..20; mirrors HashLib.offerTreeTypeHash. -OFFER_TREE_TYPE_HASHES = [ - "2b9ee710e1977dfc5778fe18c905ccc1d9e144baf3ba83be732d4da65ecb73e3", - "3cc16189b92a85898f1d5c6e87282c8ded7c1c93b2323d5e85ae10c5f4b2b220", - "6de37d3e570afa293a8107d4b6b1d9547616c04f42164d009c89194787b2ffa6", - "ba3ea2ddfbf40a906fcd1b9506dbd344c062e8dcba8b5c902ceb13339f45a358", - "e5faa865e93bc1b7b8fdf91980f54682d649683b014edd6c54b642f5a0c96977", - "eda50f61dd2a827c6ff9fbfcd54335628dcaa78aaa4f2d118c60886219cdce2b", - "54e2c9cc40cdc0e9ad530cf2be298f952f57af2b18b02f88274a9bbab359d23a", - "c9d81859d60d6b21c688f4be93ca83e3be222728bb156ef5f4cf497f879f1e29", - "d59b0c4544e0c60c8611eab0aaa402575f14ee784d22289c5d57f48c422a62d6", - "ccad21701f34f08bb8398a3dbc77e20e4c9c424930f3a8b31485bf059e2bdb20", - "8a42dfb49807647bfc49c906aef322aa0239d40e4cb675761e141bc7bfa530da", - "2adc0d948b2e3ecb642661590d2eec36d4e71e9acf382deb6574371800caf198", - "f5845dfaed016de272342f346346a49d4b1694f622144d420558a38e46ac9dad", - "3d7df854e6294bf433b64bbb8d0a82fa875a87b45b0016db27fc5752e54126ad", - "72a991a101708716ff427c524404ab44f4d4d1f4e7e76c0ae8b967222164b348", - "762c88fc52cf78a54401d247790f1bdb619d51d3458d1415c20d1422197cecc4", - "8ede2209e94c8d5f8379d733dc8712b71a3888c1c4b70f3d6b22285f70bf4286", - "425b18f07b3ac2f641977d2c294590565dd40b5d8414610568dca64628399975", - "7e7d98718c0180e882e5963b9bd49810096912c273dfa38d8afdd6d39fde86ec", - "8d35d491a29d846489e19688efff3c4cc7dbd54458058d49b30294074539f0b9", - "824e385eea1953bcbc783bf900b18aa6fba129b6908765e986cf0968b491ec4f", -] - # ABI signature for `Offer` matching src/interfaces/IMidnight.sol field order. OFFER_ABI_TYPE = ( "(" @@ -56,12 +26,6 @@ INTERNAL_NODE_ABI_TYPE = "(bytes32,bytes32,bytes32)" -def offer_tree_typehash(height): - if not 0 <= height <= 20: - raise ValueError(f"offer-tree height out of range: {height}") - return bytes.fromhex(OFFER_TREE_TYPE_HASHES[height]) - - def _bytes32(v): raw = bytes.fromhex(v.removeprefix("0x")) assert len(raw) == 32, f"expected 32 bytes, got {len(raw)}" @@ -241,46 +205,6 @@ def build_dense(leaves, claimed_root): } -# Reconstructs the EIP-712 digest for an OfferTree and either signs it locally -# (`signerKey`) or accepts a precomputed (signer, v, r, s). -def build_eip712(eip712_in, root, leaf_length): - ratifier = w3.to_checksum_address(eip712_in["ratifier"]) - chain_id = int(eip712_in["chainId"]) - height = (leaf_length - 1).bit_length() - if 1 << height != leaf_length: - raise ValueError( - f"eip712 requires a balanced tree; leafLength {leaf_length} is not a power of two" - ) - - struct_hash = _keccak_abi( - ["bytes32", "bytes32"], [offer_tree_typehash(height), _bytes32(root)] - ) - domain_separator = _keccak_abi( - ["bytes32", "uint256", "address"], [EIP712_DOMAIN_TYPEHASH, chain_id, ratifier] - ) - digest = w3.keccak(b"\x19\x01" + domain_separator + struct_hash) - - if "signerKey" in eip712_in: - signed = Account._sign_hash(digest, eip712_in["signerKey"]) - signer = Account.from_key(eip712_in["signerKey"]).address - v, r, s = signed.v, signed.r.to_bytes(32, "big"), signed.s.to_bytes(32, "big") - else: - signer = w3.to_checksum_address(eip712_in["signer"]) - v = int(eip712_in["v"]) - r = _bytes32(eip712_in["r"]) - s = _bytes32(eip712_in["s"]) - - return { - "ratifier": ratifier, - "chainId": chain_id, - "height": height, - "signer": signer, - "v": v, - "r": "0x" + r.hex(), - "s": "0x" + s.hex(), - } - - def main(): if len(sys.argv) != 2: print("usage: python create_certificate.py ", file=sys.stderr) @@ -292,9 +216,6 @@ def main(): root = proofs["root"] certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], root) - if "eip712" in proofs: - certificate["eip712"] = build_eip712(proofs["eip712"], root, certificate["treeLeafLength"]) - with open("certificate.json", "w") as f: json.dump(certificate, f, indent=2) From 7091ed9ba5cff426d2e6456bb3fd3157d51eafd1 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 1 Jun 2026 18:13:09 +0200 Subject: [PATCH 28/38] added justification rules for the hashLeaf trick --- certora/helpers/OfferTree.sol | 4 ++++ certora/specs/OfferTreeWellFormed.spec | 24 ++++++++++++++++++------ 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 939a89a73..115044ffa 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -114,6 +114,10 @@ contract OfferTree { 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); } diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index 92c5cd575..3b62b908c 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -1,13 +1,16 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// No hashing summaries are needed: `Node` stores only the fixed-size pre-image of `hashOffer` (see OfferTree.sol), -// so `isWellFormed` re-hashes a leaf with a single bounded keccak over fixed-size storage — no dynamic-array reads, -// no loops. The only dynamic hashing is `newLeaf` hashing its offer argument once, which is cheap. +// Leaves store the fixed-size pre-image of `hashOffer` (its scalar fields plus `marketHash` and `callbackDataHash`) +// instead of the raw `Offer`, so `isWellFormed` re-hashes a leaf with one bounded keccak (`_hashLeaf`) and the +// invariant scales. The rules below justify the trick: `newLeafConnectsHashLeafToHashOffer` checks `_hashLeaf` +// faithfully reproduces `hashOffer`, `leafHashDisjointFromNodeHash` checks leaf and internal hashes never collide, +// and `nodeHashInjective` underpins the merkle reasoning in OfferTreeMembership.spec. 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; } @@ -25,9 +28,7 @@ strong invariant wellFormed(bytes32 id) } } -// Focused bridge check: `newLeaf` keys the node by `HashLib.hashOffer(offer)` and stores the fixed-size -// pre-image that `_hashLeaf` re-hashes. This rule catches drift between `_hashLeaf` and the real offer hash -// construction. +// `_hashLeaf` reproduces the real `hashOffer` for the pre-image stored by `newLeaf`. rule newLeafConnectsHashLeafToHashOffer(OfferTree.Offer offer) { bytes32 id = hashOffer(offer); @@ -39,3 +40,14 @@ rule newLeafConnectsHashLeafToHashOffer(OfferTree.Offer offer) { assert _hashLeaf(id) == id; assert _hashLeaf(id) == hashOffer(offer); } + +// 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; +} From 9d0635b90bf8b5ac2b38caccb7f8562c966135ef Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 16:55:55 +0200 Subject: [PATCH 29/38] removed assumptions from soundness rule --- certora/specs/OfferTreeMembership.spec | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index b8d1abcda..b5f3fb418 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -12,29 +12,18 @@ methods { function Utils.isLeaf(bytes32, bytes32, uint256, bytes32[]) external returns (bool) envfree; } -// The main correctness result of the verification. -// It ensures that 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. +// 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; - // Assume that root is the hash of node in the tree. - require OfferTree.getHash(node) == root; + require OfferTree.getHash(node) == root, "root is the hash of node"; - // Assume that the root is non-zero, otherwise empty nodes would hash-match it. - require root != to_bytes32(0); + require(OfferTree.wellFormedPath(node, leafIndex, proof), "the path from the root to the leaf is well-formed"); - // No need to make sure that node is equal to the root: one can pass an internal node instead. - // Assume that the tree is well-formed along the path down to the leaf. - OfferTree.wellFormedPath(node, leafIndex, proof); - - // Compute the leaf identifier once so both uses below bind to the same hash. bytes32 leafId = Utils.hashOffer(offer); - // Assume that the leaf identifier is non-zero, matching the constraint enforced by newLeaf. - require leafId != to_bytes32(0); - - // Assume that the Merkle proof verifies the offer's hash against the root. - require Utils.isLeaf(root, leafId, leafIndex, proof); + require Utils.isLeaf(root, leafId, leafIndex, proof), "Merkle proof verifies the offer"; assert OfferTree.isLeafNode(leafId); } From 4a3f12168b02593e848dd7f5058ee699ae0a51cd Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 16:56:31 +0200 Subject: [PATCH 30/38] tuned --- certora/specs/OfferTreeMembership.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/specs/OfferTreeMembership.spec b/certora/specs/OfferTreeMembership.spec index b5f3fb418..7256cdc43 100644 --- a/certora/specs/OfferTreeMembership.spec +++ b/certora/specs/OfferTreeMembership.spec @@ -7,7 +7,6 @@ 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; } From 5dec1247d6d2fc3614e8f31947e010eccfde97d9 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 19:21:55 +0200 Subject: [PATCH 31/38] tuned; retained market-level hashLeaf --- certora/helpers/OfferTree.sol | 37 +++++++++++++------------- certora/specs/OfferTreeWellFormed.spec | 23 +++++++--------- 2 files changed, 28 insertions(+), 32 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 115044ffa..2b09a6a18 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -5,14 +5,14 @@ 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 +// 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. +// 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; @@ -42,14 +42,13 @@ contract OfferTree { /* 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 can have an identifier that is the hash of the offer. - // This ensures that the same offer does not appear twice as a leaf in the 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`. Because `hashOffer` and `hashNode` feed keccak distinct - // input shapes, this gives domain separation between leaves and internal nodes for free under Certora's keccak - // model. The tree is built only via `newLeaf` and `newInternalNode`, which preserve well-formedness by + // 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; @@ -60,7 +59,7 @@ contract OfferTree { 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. + // 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; @@ -122,9 +121,9 @@ contract OfferTree { 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`. + // 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( @@ -167,8 +166,8 @@ contract OfferTree { 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`. + // 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)); diff --git a/certora/specs/OfferTreeWellFormed.spec b/certora/specs/OfferTreeWellFormed.spec index 3b62b908c..0c87937e0 100644 --- a/certora/specs/OfferTreeWellFormed.spec +++ b/certora/specs/OfferTreeWellFormed.spec @@ -1,10 +1,11 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// Leaves store the fixed-size pre-image of `hashOffer` (its scalar fields plus `marketHash` and `callbackDataHash`) -// instead of the raw `Offer`, so `isWellFormed` re-hashes a leaf with one bounded keccak (`_hashLeaf`) and the -// invariant scales. The rules below justify the trick: `newLeafConnectsHashLeafToHashOffer` checks `_hashLeaf` -// faithfully reproduces `hashOffer`, `leafHashDisjointFromNodeHash` checks leaf and internal hashes never collide, -// and `nodeHashInjective` underpins the merkle reasoning in OfferTreeMembership.spec. +// 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; @@ -28,17 +29,13 @@ strong invariant wellFormed(bytes32 id) } } -// `_hashLeaf` reproduces the real `hashOffer` for the pre-image stored by `newLeaf`. -rule newLeafConnectsHashLeafToHashOffer(OfferTree.Offer offer) { - bytes32 id = hashOffer(offer); - - require id != to_bytes32(0); - require isEmpty(id); - +// _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; - assert _hashLeaf(id) == hashOffer(offer); } // A recomputed leaf hash never equals an internal-node hash: image(_hashLeaf) and image(hashNode) are disjoint. From 956a11f9c60e2b100e3218c3d8fa616a7e6148aa Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 20:42:48 +0200 Subject: [PATCH 32/38] cleanup ratification spec --- certora/specs/Ratification.spec | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/certora/specs/Ratification.spec b/certora/specs/Ratification.spec index fe3e27fa4..ecc3499ec 100644 --- a/certora/specs/Ratification.spec +++ b/certora/specs/Ratification.spec @@ -7,7 +7,6 @@ methods { function isAuthorized(address authorizer, address authorized) external returns (bool) envfree; - function Utils.hashOffer(Midnight.Offer) external returns (bytes32) envfree; function Utils.callbackSuccess() external returns (bytes32) envfree; function _.isRatified(Midnight.Offer, bytes) external => DISPATCHER(true); @@ -17,7 +16,7 @@ methods { 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 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) internal returns (bool) => isLeafCapture(root, leafHash, leafIndex, proof); + 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; @@ -33,15 +32,11 @@ methods { function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; } -function summaryHashOffer(Midnight.Offer offer) returns bytes32 { - return Utils.hashOffer(offer); -} - // 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(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] proof) returns bool { +function isLeafCapture() returns bool { bool ret; if (ret) { isLeafReturnedTrue = true; From ea946969253c9fe0694f0e36e73796c9a2867555 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 20:44:42 +0200 Subject: [PATCH 33/38] varibale renaming in create_certificate.py; tuned checker --- certora/checker/Checker.sol | 39 ++++++++++++--------------- certora/checker/create_certificate.py | 12 ++++----- certora/helpers/Utils.sol | 11 +++----- 3 files changed, 26 insertions(+), 36 deletions(-) diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol index 1a5e4445f..540308c9f 100644 --- a/certora/checker/Checker.sol +++ b/certora/checker/Checker.sol @@ -20,27 +20,6 @@ contract Checker is Test { // Replay the certificate through the verified `newLeaf` and `newInternalNode` // primitives, then assert that the final certificate item matches `root`. - function _verifyCertificate(Offer[] memory leaves, InternalNode[] memory nodes, bytes32 root) internal { - 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; - } - - assertTrue(!tree.isEmpty(rootId), "empty root"); - assertEq(tree.getHash(rootId), root, "mismatched roots"); - } - 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"); @@ -62,6 +41,22 @@ contract Checker is Test { nodes[i] = abi.decode(enc, (InternalNode)); } - _verifyCertificate(leaves, nodes, root); + 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 index 34a99eb30..566b37b33 100644 --- a/certora/checker/create_certificate.py +++ b/certora/checker/create_certificate.py @@ -162,10 +162,11 @@ def hash_node(left, right): return w3.to_hex(w3.keccak(_bytes32(left) + _bytes32(right))) -# Builds a dense certificate from a power-of-two list of offers, in leftIndex order. -def build_dense(leaves, claimed_root): +# 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) - assert n > 0 and (n & (n - 1)) == 0, "dense leaves count must be a power of two" + assert n > 0 and (n & (n - 1)) == 0, "leaves count must be a power of two" leaf_instructions = {} node_instructions = {} @@ -192,12 +193,11 @@ def build_dense(leaves, claimed_root): level = next_level assert level[0].lower() == claimed_root.lower(), ( - f"dense: computed root {level[0]} != claimed root {claimed_root}" + f"computed root {level[0]} != claimed root {claimed_root}" ) return { "root": claimed_root, - "treeLeafLength": n, "leafLength": len(leaf_instructions), "leaf": list(leaf_instructions.values()), "nodeLength": len(node_instructions), @@ -214,7 +214,7 @@ def main(): proofs = json.load(f) root = proofs["root"] - certificate = build_dense([entry["offer"] for entry in proofs["leaves"]], 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) diff --git a/certora/helpers/Utils.sol b/certora/helpers/Utils.sol index fa557338d..aa1ff6552 100644 --- a/certora/helpers/Utils.sol +++ b/certora/helpers/Utils.sol @@ -19,18 +19,13 @@ contract Utils { } // Wraps `HashLib.hashOffer` directly so CVL specs can expose the real EIP-712 offer hash - // envfree. Avoids the prior `keccak256(abi.encode(offer))` reimplementation, which is a - // *different* hash than `HashLib.hashOffer` (no typehash prefix, no inner hashing of - // market/callbackData) and broke keccak unification across summary boundaries when the - // prover had to forward-compute the merkle chain (completeness direction). + // 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 hashNode(bytes32 a, bytes32 b) external pure returns (bytes32) { - return HashLib.hashNode(a, b); - } - function isLeaf(bytes32 root, bytes32 leafHash, uint256 leafIndex, bytes32[] memory proof) external pure From fa88df5df8c60be82c680f46a73d30f832798e15 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 21:24:23 +0200 Subject: [PATCH 34/38] added high-level verification approach in README --- certora/README.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/certora/README.md b/certora/README.md index 62199d767..007980423 100644 --- a/certora/README.md +++ b/certora/README.md @@ -43,6 +43,37 @@ 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. +- [`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. + ## Fees Continuous-fee accrual and settlement-fee rounding stay within their expected bounds. From a1b4b8ecabf4e126d40b2e295a800c659cc61b08 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 21:27:33 +0200 Subject: [PATCH 35/38] fmt --- certora/helpers/OfferTree.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/helpers/OfferTree.sol b/certora/helpers/OfferTree.sol index 2b09a6a18..f25185128 100644 --- a/certora/helpers/OfferTree.sol +++ b/certora/helpers/OfferTree.sol @@ -48,8 +48,8 @@ contract OfferTree { // 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. + // 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 */ From be2a5635c1f47a5944d16bfed63e9e74943f9626 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 21:45:22 +0200 Subject: [PATCH 36/38] acknowledge URD spec in README --- certora/README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/README.md b/certora/README.md index 007980423..01e2d01c6 100644 --- a/certora/README.md +++ b/certora/README.md @@ -74,6 +74,8 @@ The membership result is stated for any well-formed root; the checker in [`check 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. From 6aaa42049a8aa36b1c852ddc894323b25a788ae9 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Tue, 2 Jun 2026 21:59:58 +0200 Subject: [PATCH 37/38] asserts replaced with raising exceptions --- certora/checker/create_certificate.py | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py index 566b37b33..3b281a805 100644 --- a/certora/checker/create_certificate.py +++ b/certora/checker/create_certificate.py @@ -26,9 +26,15 @@ 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")) - assert len(raw) == 32, f"expected 32 bytes, got {len(raw)}" + _require(len(raw) == 32, f"expected 32 bytes, got {len(raw)}") return raw @@ -166,7 +172,7 @@ def hash_node(left, right): # leaves level-by-level into a perfect binary tree. def build_certificate(leaves, claimed_root): n = len(leaves) - assert n > 0 and (n & (n - 1)) == 0, "leaves count must be a power of two" + _require(n > 0 and (n & (n - 1)) == 0, "leaves count must be a power of two") leaf_instructions = {} node_instructions = {} @@ -175,7 +181,7 @@ def build_certificate(leaves, claimed_root): for leaf, leaf_hash in zip(leaves, level): encoded_leaf = abi_encode_offer(leaf) previous = leaf_instructions.setdefault(leaf_hash, encoded_leaf) - assert previous == encoded_leaf, "leaf hash collides with a different offer" + _require(previous == encoded_leaf, "leaf hash collides with a different offer") while len(level) > 1: next_level = [] @@ -183,17 +189,16 @@ def build_certificate(leaves, claimed_root): left = level[2 * i] right = level[2 * i + 1] node_hash = hash_node(left, right) - assert ( - node_hash not in leaf_instructions - ), "internal node id collides with a leaf id" + _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) - assert previous == encoded_node, "internal node id collides with different children" + _require(previous == encoded_node, "internal node id collides with different children") next_level.append(node_hash) level = next_level - assert level[0].lower() == claimed_root.lower(), ( - f"computed root {level[0]} != claimed root {claimed_root}" + _require( + level[0].lower() == claimed_root.lower(), + f"computed root {level[0]} != claimed root {claimed_root}", ) return { From bec4e8f256f249a37e50f55c9547af34d484805d Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 3 Jun 2026 08:54:46 +0200 Subject: [PATCH 38/38] tuned --- certora/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/README.md b/certora/README.md index 01e2d01c6..b2da4a4f0 100644 --- a/certora/README.md +++ b/certora/README.md @@ -49,7 +49,7 @@ Offers are authorized in batches: a ratifier signs a single Merkle root over an 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. +- [`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.