[Certora] OfferTree Soundness

[bhargavbh]

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.

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

corresponding thread
motivation

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c0e2d9281b

ℹ️ 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".

[jhoenicke]

Looks good. I also tried it with a broken hash function that allows collision of node and leaf and at least that found a counterexample.

[bhargavbh]

All good suggestions. Incorporated the following changes which simplifies the model quite a bit without impacting the claim:

• Hash IDs: Internal-node IDs equal their hashes.
• Idempotent creation: Constructors return hash IDs and reuse existing nodes.
• Simpler membership: Use root directly; remove the separate node variable and getHash.
• Generator does not inherit OfferTree: Compute roots in memory, independently of OfferTree.
• Cleaner configs: Remove explicit sanity and timeout settings.
• Regression tests: Cover root agreement, idempotency, missing children, duplicates, membership proofs, and storage isolation.
  cc @QGarchery

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 4b669c0ade

ℹ️ 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".