Invariants
The properties the code is built to hold, each covered by tests. These are what an auditor should try to break.
Live properties
- beforeSwap and afterSwap never revert for a well-formed swap on any pool state. Every failure degrades to a quoted fee.
- Every quoted fee lies within the advertised range that
feeBounds()reports, so a router reading it before quoting is not misled. - The surcharge nets to exactly zero for the hook.
donatedebits it and the returned delta repays it, leaving the swapper as the sole funder and the hook holding no balance. - Only bound pools may attach — the currencies must match the pair the reference oracle declares.
- A degraded reference degrades upward. Stale, reverting, or out-of-range readings quote the ceiling rather than presenting a wrong price as correct.
- A fresh reference is checked twice. A reading the oracle reports as usable is additionally compared against a smoothed average of the pool's own tick, sampled once per block; one that disagrees by more than the configured cap is treated as stale.
Not applicable
The original design specified a rebate ledger with ERC-6909 accounting, EIP-712 router attestations, and an on-chain logistic classifier. None of it is built, so the invariants covering ledger solvency and attestation replay do not apply. See what is not built.