[Certora] OfferTree Soundness#816
Conversation
MathisGD
changed the title
bhargavbh
changed the title
…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>
bhargavbh
changed the title
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 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".
There was a problem hiding this comment.
💡 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".
| "solc_via_ir": true, | ||
| "solc_evm_version": "osaka", | ||
| "optimistic_loop": true, | ||
| "loop_iter": 3, |
There was a problem hiding this comment.
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 👍 / 👎.
| function hashMarket(Market memory market) external pure returns (bytes32) { | ||
| return keccak256(abi.encode(market)); | ||
| return HashLib.hashMarket(market); |
There was a problem hiding this comment.
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 👍 / 👎.
1 participant
Objective is to show that a successful
takecan only settle an offer that was genuinely committed in the signed tree.We reason about
OfferTree, a model of the tree built only through thenewLeafandnewInternalNodeprimitives. Leaves are keyed byHashLib.hashOffer(offer)and store a fixed-size pre-image of the offer, soisWellFormedre-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.specchecks that the primitives only ever build well-formed trees: every node is empty, a leaf carrying a genuinehashOffer, or an internal node correctly hashing its two children.OfferTreeMembership.specchecks the main soundness result: for any well-formed tree, if a Merkle proof verifies an offer's hash against the root viaisLeaf, 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.specconnects this to the on-chain path: every successfulisRatified(across all ratifier implementations) and every successfultakeactually invokesHashLib.isLeafand it returns true.The verification setup and technique is inspired from the Merkle Tree Membership soundness spec in Universal Rewards Distributor