Skip to content

[Certora] Split Properties #542

Merged
QGarchery merged 85 commits into
mainfrom
certora/offer-splitting
Jun 5, 2026
Merged

[Certora] Split Properties #542
QGarchery merged 85 commits into
mainfrom
certora/offer-splitting

Conversation

@lilCertora
Copy link
Copy Markdown
Collaborator

@lilCertora lilCertora commented Mar 19, 2026

  • offer can be split : splitPreservesPrincipalAccounting: position-level accounting (creditOf, debtOf, totalUnits, lastLossFactor, lastAccrual, continuousFeeCredit) is bitwise equal across the two paths.
  • Splitting an offer will not punish the maker : splitDoesNotPunishMakerOrFavorTaker: taking A vs taking B then C (with A = B + C) differs by at most 1 wei on buyer/seller assets, fee delta, consumed, and claimableTradingFee (exact for maxUnits mode).

corresponding thread

@lilCertora lilCertora changed the title [Certora] Split Properties [Certora] Split Properties (WIP) Mar 19, 2026
@lilCertora lilCertora mentioned this pull request Mar 19, 2026
70 tasks
@lilCertora lilCertora marked this pull request as ready for review March 25, 2026 15:45
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 28d007e71b

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c623afb74b

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 38bce39a87

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 40391749d0

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/OffersCanBeSplit.spec Outdated
@lilCertora lilCertora changed the title [Certora] Split Properties (WIP) [Certora] Split Properties Mar 30, 2026
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3a371fbb25

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 51b9dbb103

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 624d88598b

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 101dbcadc3

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9b5b941745

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitPreservesPrincipalAccounting.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d9d9db253e

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: e15ace9bec

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2a3fb75464

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 644eaef05a

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitPreservesPrincipalAccounting.spec Outdated
Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 59e7c41bfe

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/OffersCanBeSplit.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b88a934f02

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitPreservesAccounting.spec Outdated
Comment thread certora/specs/SplitPreservesAccounting.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a0d97b19d1

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitPreservesPrincipalAccounting.spec Outdated
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 76cc7bf0b6

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Comment thread certora/specs/SplitPreservesPrincipalAccounting.spec Outdated
Comment thread certora/confs/SplitPreservesPrincipalAccounting.conf Outdated
Comment thread certora/confs/SplitPreservesPrincipalAccounting.conf Outdated
Comment thread certora/confs/SplitPreservesPrincipalAccounting.conf Outdated
Comment thread certora/specs/SplitPreservesAccounting.spec Outdated
Comment thread certora/specs/SplitPreservesPrincipalAccounting.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
Comment thread certora/specs/SplitDoesNotPunishMakerOrFavorTaker.spec Outdated
@lilCertora lilCertora force-pushed the certora/offer-splitting branch from 689e75e to 5d0f63d Compare June 5, 2026 12:36
chatgpt-codex-connector[bot]

This comment was marked as outdated.

@QGarchery QGarchery merged commit 0da2d6f into main Jun 5, 2026
45 checks passed
@QGarchery QGarchery deleted the certora/offer-splitting branch June 5, 2026 13:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants