Skip to content

[Certora] Fee Boundaries#449

Merged
QGarchery merged 48 commits into
mainfrom
certora/fee-boundaries
Mar 18, 2026
Merged

[Certora] Fee Boundaries#449
QGarchery merged 48 commits into
mainfrom
certora/fee-boundaries

Conversation

@lilCertora

Copy link
Copy Markdown
Collaborator

Verifies that trading fees computed by piecewise linear interpolation are always bounded by the per-index maxTradingFee caps, and that zero fee parameters produce zero fees. Specifically:

  • Each stored fee breakpoint (both per-obligation and per-default) never exceeds its maxTradingFee(index) cap
  • The interpolated tradingFee(id, ttm) is globally bounded by maxTradingFee(6) (50 bps)
  • The interpolation is a convex combination: it never overshoots or undershoots the enclosing breakpoint values
  • All fee breakpoints zero implies tradingFee == 0 for any time to maturity

@lilCertora lilCertora changed the title Fee Boundaries [Certora] Fee Boundaries Mar 4, 2026
@lilCertora lilCertora marked this pull request as ready for review March 10, 2026 17:09
Comment thread certora/confs/FeeBoundaries.conf Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated

@jhoenicke jhoenicke left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Added some comments

Comment thread certora/specs/FeeBoundaries.spec
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec Outdated
Comment thread certora/specs/FeeBoundaries.spec
Comment thread certora/specs/FeeBoundaries.spec Outdated
lilCertora and others added 5 commits March 16, 2026 16:43
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com>
Signed-off-by: lilCertora <lilian@certora.com>
@QGarchery QGarchery mentioned this pull request Mar 17, 2026
73 tasks
Comment thread certora/specs/FeeBoundaries.spec
Comment thread certora/specs/FeeBoundaries.spec Outdated
@QGarchery QGarchery merged commit e42acac into main Mar 18, 2026
15 checks passed
@QGarchery QGarchery deleted the certora/fee-boundaries branch March 18, 2026 09:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants