[Certora] OfferTree Soundness by bhargavbh · Pull Request #816 · morpho-org/midnight

bhargavbh · 2026-05-07T13:05:45Z

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, 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 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 checks the main soundness result: for any well-formed tree, if a Merkle proof verifies an offer's hash against the root via isLeaf, 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 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.

The verification setup and technique is inspired from the Merkle Tree Membership soundness spec in Universal Rewards Distributor

…ic and dynamic part

Conflicts resolved: - certora/specs/Ratification.spec: kept the offer-tree additions (isLeaf capture, isRatified dispatcher, isRatifiedRequiresIsLeaf/takeRequiresIsLeaf) and adopted main's take() parameter reorder (ratifierData 2nd) in the new takeRequiresIsLeaf rule; kept main's tradingFee->settlementFee rename. - certora/confs/Ratification.conf: kept the ratifier files + links needed for the cross-ratifier dispatch claim. - certora/helpers/Utils.sol: auto-merged (our hashOffer reword + removed hashNode wrapper, plus main's maxTradingFee->maxSettlementFee rename). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: be2a5635c1

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 6aaa42049a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-06-02T20:03:13Z

+  "solc_via_ir": true,
+  "solc_evm_version": "osaka",
+  "optimistic_loop": true,
+  "loop_iter": 3,


Raise the proof loop bound to cover supported trees

With optimistic_loop enabled, this loop_iter only unrolls the proof.length loops in OfferTree.wellFormedPath and HashLib.isLeaf for three levels, while the ratifiers accept signed offer trees up to height 20 via offerTreeTypeHash. For any concrete root/proof of height 4–20, the headline membership soundness proof is therefore only checking a truncated Merkle path, so it does not justify the README claim for the supported tree sizes. Set the loop bound to 20 (or otherwise require proof.length <= 3 in the property and docs).

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-06-02T20:03:13Z

    function hashMarket(Market memory market) external pure returns (bytes32) {
-        return keccak256(abi.encode(market));
+        return HashLib.hashMarket(market);


Keep the CVL market-id summary loop-free

Several existing specs summarize IdLib.toId as Utils.hashMarket(market), and their configs use small loop bounds such as loop_iter: 2; replacing the previous single keccak256(abi.encode(market)) helper with HashLib.hashMarket adds a loop over market.collateralParams, even though markets may contain up to 128 collaterals. For markets with more entries than the spec loop bound, those unrelated accounting/created-market proofs now reason under optimistic loop truncation for their market IDs, which can make them prove properties about the wrong or colliding IDs. Keep this helper loop-free for ID summaries and add a separate EIP-712 helper for offer-tree hashing.

Useful? React with 👍 / 👎.

jhoenicke · 2026-06-08T09:24:39Z

+        n.hashNode = id;
+    }
+
+    function newInternalNode(bytes32 id, bytes32 left, bytes32 right) public {


For a leafnode, the id equals the hash (tree[i].hashNode == id). But for internal nodes you allow the id to be different from the hashNode. Is there a reason for it?

Initially this constraint was there to prevent having the same address multiple times in the tree.

We don't have this requirement, but it's weirdly useful here. Assume that the id of the leaves was not necessarily the same as the hash, and you remove the corresponding check in isWellFormed (the check id == expected). Now you could have a function that would change marketHash and adapt hashNode accordingly (as the hashLeaf of the new params with the changed marketHash). This would not break the invariant isWellFormed, but it would allow to forge another root.

Another more straightforward way to avoid the above scenario, is to check that the tree is immutable.

QGarchery · 2026-06-08T07:42:58Z

Let's keep the following convention: one sentence per line

QGarchery · 2026-06-08T07:47:14Z

+
+- [`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.


Suggested change

- [`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.

- [`Ratification.spec`](specs/Ratification.spec) connects this to the on-chain path: every successful `isRatified` (across all ratifier implementations) and every successful `take` actually verifies the Merkle tree membership of an offer, taking as input the offer's hash and checking it against the root.

Because isLeaf is an implementation detail that is not mentioned before

QGarchery · 2026-06-08T08:19:57Z

+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


In the URD the proofs.json was obtained as an artifact of the creation of the rewards distribution program (see the proofs.json files under this folder). Since here it doesn't work the same it makes less sense to take a proofs.json file. I'm thinking that we may prefer the full offer tree, which is what is produced when doing clear signing (see test/frontend/README.md)

QGarchery · 2026-06-08T09:23:53Z

+    function hashOffer(Offer memory offer) public pure returns (bytes32) {
+        return HashLib.hashOffer(offer);
+    }
+
+    function hashNode(bytes32 left, bytes32 right) public pure returns (bytes32) {
+        return HashLib.hashNode(left, right);
+    }
+
+    function _hashLeaf(bytes32 id) public view returns (bytes32) {
+        return _hashLeaf(tree[id].leaf);
+    }
+


Suggested change

function hashOffer(Offer memory offer) public pure returns (bytes32) {

return HashLib.hashOffer(offer);

}

function hashNode(bytes32 left, bytes32 right) public pure returns (bytes32) {

return HashLib.hashNode(left, right);

}

function _hashLeaf(bytes32 id) public view returns (bytes32) {

return _hashLeaf(tree[id].leaf);

}

QGarchery · 2026-06-08T09:24:06Z

+    function _isEmpty(Node storage n) internal view returns (bool) {
+        return n.left == 0 && n.right == 0 && n.hashNode == 0;
+    }
+
+    function isEmpty(bytes32 id) public view returns (bool) {
+        return _isEmpty(tree[id]);
+    }


Suggested change

function _isEmpty(Node storage n) internal view returns (bool) {

return n.left == 0 && n.right == 0 && n.hashNode == 0;

}

function isEmpty(bytes32 id) public view returns (bool) {

return _isEmpty(tree[id]);

}

function isEmpty(Node storage n) internal view returns (bool) {

return n.left == 0 && n.right == 0 && n.hashNode == 0;

}

(and change _isEmpty occurrences to isEmpty)

QGarchery · 2026-06-08T09:29:06Z

+// 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.


It really checks: hashNode == _hashLeaf(leaf) and id == _hashLeaf(leaf). But it doesn't verify that hashNode == hashOffer(offer) (which it can't do because it doesn't have the offer), so this part is really assumed

actually it does verify it with the rule hashLeafReproducesHashOffer. Maybe it deserves a longer explanation though

QGarchery · 2026-06-08T09:31:30Z

+        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);


Here we are verifying that the hashes are not zero, which is not exactly the definition of isEmpty. Should we simplify isEmpty to only hashNode == 0 ?

QGarchery · 2026-06-08T09:33:43Z

+    //   - leaves have the correct identifier and hashing
+    //   - internal nodes have the correct hashing


Let's avoid using the word "correct", it hides the meaning

Suggested change

// - leaves have the correct identifier and hashing

// - internal nodes have the correct hashing

// - leaves have the hash of the leaf data as identifier, which is also their stored hash

// - internal nodes have the hash of their children has their stored hash

QGarchery · 2026-06-08T14:02:21Z

this is too many changes to Ratification.spec IMO (the new assumptions we make are impacting other rules).
We could either:

try to reduce the number of assumptions (do we need all of them ?)

move it to a separate spec

remove those changes, the added rules are almost trivial, even though it is an important property

I would favor option 3, if we cannot do option 1 and remove a lot of those assumptions

bhargavbh added 2 commits May 7, 2026 10:46

added rules inspired form URD

21739ee

tuned

030c175

MathisGD changed the title ~~added rules inspired form URD~~ [Certora] added rules inspired form URD May 11, 2026

bhargavbh added 6 commits May 19, 2026 15:04

merged main

8e2e5ee

take correctness passes; added some diagnostic tests

4898d72

removed the diagnostic rules

215698b

cleaned up comments

b62eae7

add completeness rule

b9d943e

abstract properties instantiated to midnight

9b92e50

bhargavbh self-assigned this May 19, 2026

bhargavbh added 2 commits May 19, 2026 18:07

cvl fmt

0cd4f3e

fmt

07d95e3

bhargavbh changed the title ~~[Certora] added rules inspired form URD~~ [Certora] OfferTree soundness and completeness May 20, 2026

bhargavbh added 17 commits May 20, 2026 10:01

renamed spec; minor changes in OfferTree definition

bcc5198

tuned

38c1875

fmt

8208a49

forge fmt

80d2ad2

Merge remote-tracking branch 'origin/main' into certora/offer-tree

7a3e019

resolved errors from merge

03ba8cd

updated callback summary signatures

dd415d0

new rule in Ratification.spec: isRatified always calls isLeaf

24140f4

rhashNode summarised similar to hashOffer

cfb723f

revamped soundness: Offer included in the node

8187c24

tuned comment

2d1eb87

add checker

d77d0b3

add checker

939a570

summarise isRatify

d9f174e

trimmed down to core properties

fc758a3

removed completeness

253e37e

comment style adapted to URD

89c39d6

bhargavbh and others added 12 commits June 1, 2026 14:44

retained only testVerifyCertificate in Checker; split offer into stat…

a43f97d

…ic and dynamic part

removed ratifier

65e69d1

added justification rules for the hashLeaf trick

7091ed9

removed assumptions from soundness rule

9d0635b

tuned

4a3f121

tuned; retained market-level hashLeaf

5dec124

cleanup ratification spec

956a11f

varibale renaming in create_certificate.py; tuned checker

ea94696

added high-level verification approach in README

fa88df5

fmt

a1b4b8e

acknowledge URD spec in README

be2a563

bhargavbh changed the title ~~[Certora] OfferTree soundness and completeness~~ [Certora] OfferTree Soundness Jun 2, 2026

bhargavbh marked this pull request as ready for review June 2, 2026 19:50

chatgpt-codex-connector Bot reviewed Jun 2, 2026

View reviewed changes

Comment thread certora/specs/Ratification.spec

asserts replaced with raising exceptions

6aaa420

chatgpt-codex-connector Bot reviewed Jun 2, 2026

View reviewed changes

bhargavbh requested review from MathisGD, QGarchery and lilCertora June 2, 2026 20:26

bhargavbh added the verif-review label Jun 2, 2026

tuned

bec4e8f

jhoenicke reviewed Jun 8, 2026

View reviewed changes

QGarchery reviewed Jun 8, 2026

View reviewed changes

	- [`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.
	- [`Ratification.spec`](specs/Ratification.spec) connects this to the on-chain path: every successful `isRatified` (across all ratifier implementations) and every successful `take` actually verifies the Merkle tree membership of an offer, taking as input the offer's hash and checking it against the root.

		// - leaves have the correct identifier and hashing
		// - internal nodes have the correct hashing

Conversation

bhargavbh commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

bhargavbh commented May 7, 2026 •

edited

Loading