AIMM invariants

Register of the properties AIMM claims to hold on every path, at every depth, in every pool. Several are conditional: they hold only while a stated construction is preserved. Status labels: §1. Open gaps: §10.

1. How to read this page

Each entry states the constraint, its enforcement site and the consequence of violation. An unlabeled entry is enforced by the deployed source. CONDITIONAL holds only under a stated construction (I-7, I-30). NOT AN INVARIANT is a withdrawn claim, kept so it is not restated (I-5). A D-entry (§10) is a decided property with no runtime check.

Units throughout: WAD = 1e18, BPS = 1e4 (1 bp = 0.01%), PBPS = 1e6 (1 PBPS = 0.01 bp). The oracle returns the mark as a 1e18 WAD (mark1e18), so pricing comparisons are plain numeric ones (PoolIOLib.sol). Any internal mark packing is an oracle detail (V1: Mark Relayer).

Citations name the enforcing contract function; that function name is the stable reference.

Topology is the general bounded tree: any asset may anchor to a non-base parent within the depth bound, and nothing in the contracts prefers the base. Depth is configuration, per pool; see Anchor Path Pricing §1 and §1.1. Invariants below are stated against the bound, not against any one roster’s shape.

2. Settlement and accounting

I-1. Endpoint-only settlement

A swap mutates exactly two reserve slots: the input leg and the output leg. No intermediate hop moves any reserve, at any path length.

Enforced: PoolIOLib.sol is the whole of the reserve mutation:

aIn.reserves  += uint128(amtIn);
aOut.reserves -= uint128(q.amountOut);

PoolIOLib.settle receives only aIn and aOut, and it is the whole settlement path: there is no separate exec, and the comment at the function records that the split was considered and rejected. There is no loop over path.hops, so no interior slot is reachable from it. The pricing walk (PricingLib._walkLegs, PricingLib.sol) is a pure view computation over the route and writes nothing.

Why it matters: this is the premise that makes an interior leg priceable at mid with no impact charge. Impact compensates a reserve displacement; on an interior leg the displacement is identically zero, so charging impact invents a cost for an event that did not occur.

Failure mode if violated: interior reserves would drift on every cross-swap, path choice would become extractable, and the coverage toll (I-9) would need a per-leg formulation.

I-2. Value conservation is NOT reserve conservation (a distinction)

I-1 does not constrain value. The two are independent, and one has already failed while the other held.

• Reserve conservation (I-1): no interior reserve moves. Structural.
• Value conservation: a closed cycle returns no more than it consumed. Behavioral, dependent on the arithmetic of every leg.

A pricing law can satisfy I-1 exactly and still leak on a stable round trip: see I-8. Any argument of the shape “no reserves move on the interior, so no harm can come from it” proves I-1 and only asserts I-2.

I-3. Fee is charged once, on the output, post-toll

Enforced: PricingLib.sol. The toll is subtracted from acc.currentAmount before the fee is computed, so the fee base is post-toll. The trader pays approximately S/2 because S is a round-trip spread and one swap crosses half of it.

There is no input-side fee (Spread & Fees §5.2).

S <= 65,535 PBPS by the saturating narrowing in _pathSpread, a field width and not a fee policy (I-11).

I-4. LP shares and liabilities relate through the index, not one-to-one

The frequently repeated form LP_i = L_i is FALSE whenever liquidityIndexWad != WAD. The true relation is:

Enforced: every share/value conversion goes through the index: PoolLiquidityLib.sol (withdrawValue = lpAmount * liquidityIndexWad / WAD), PoolLiquidityLib.sol (liabIn). liquidityIndexWad is uint72 on a WAD base (IPool.sol), so the first deposit mints 1:1 and the index only diverges afterwards through raiseIndex (fee, donation, hook yield) and Pool.hookWriteDown. Nothing writes liabilities down on a schedule, and nothing self-heals coverage either. The paths that raise a leg’s c are the coverage toll, a deposit below parity, and a cross exit out of the leg (withdrawTo to a different token, or swapLiability), which burns the full face from this leg’s liabilities and debits the payout from the destination leg. IPool.IndexUpdated.reason is 0 DONATE, 1 YIELD, 3 WRITEDOWN, 4 FEE, and PoolLiquidityLib.writeDown (reached by hookWriteDown and the owner’s write-down) is the only index-lowering writer.

idx == 0 is unreachable: PoolLiquidityLib.writeDown, the only index-lowering writer, floors the leg’s residual liabilities so the new index stays at or above min(idx, MIN_WRITEDOWN_INDEX = 1e9), through a total loss too (test_total_loss_leaves_the_leg_live_and_depositable). mintIndex still reverts InvalidState at 0, fail-closed. Near the floor a write-down can no longer cut the face a venue loss needs, so no invest lands below MIN_INVEST_INDEX = 1e12 (Pool.hookInvest, and YieldHook.rebalance skips the leg): a floored leg takes on no new venue exposure its own write-down could not cut.

Failure mode if the one-to-one form were assumed: every fee accrual would appear as unbacked LP inflation, and an integrator sizing a redemption off share count alone would misprice by the whole accrued yield.

I-5. Aggregate reserve identity (NOT AN INVARIANT)

There is no totalReserves field on PoolStorage, nor anywhere in the deployed contract set. The claim Σ R_i = R_t referred to state that does not exist, and is removed rather than restated: the per-leg reserves fields are the whole ledger.

I-6. Deposits do not worsen coverage, donations do not change it

Coverage is c_i = R_i / L_i, defined for L_i > 0 and type(uint256).max otherwise (calculateCoverage, PricingLib.sol).

A deposit of a credits a to reserves and a/C to liabilities (mint at the pool rate, I-31). At C = 1 and c <= 1:

A donation raises both sides by the same a and additionally scales the index (PoolLiquidityLib.sol):

so c' = c exactly at c = 1 and moves monotonically toward 1 otherwise. The dead-share seed is carved out of a and joins the raise denominator, never the numerator (PoolLiquidityLib.sol), so total outstanding claim can never exceed liabilities.

In general a deposit raises the leg’s coverage iff c <= C: $(R+a)/(L+a/C)\ge R/L⟺C\ge c$. It leaves C itself unchanged (testFuzz_deposit_preserves_the_rate).

A same-asset withdrawal pays x · μ with μ = min(c, C) and burns the full face x. At μ = c it leaves the leg’s coverage unchanged, (R - x·c)/(L - x) = c; at μ = C < c it raises it. Either way it never lowers C (testFuzz_same_asset_exit_never_lowers_the_rate).

Tests: test_deposit_restores_coverage, test_withdraw_coverage_neutral_when_suppressor_zero, test_donate_liquidityIndex_overflow_clamps.

3. Cycle safety

I-7. A closed cycle returns less than it consumed (CONDITIONAL)

It holds iff all of the following hold jointly:

The residual C4 leaves open. A second, independent source of non-conservation survives, bounded by the impact-conservation tests rather than fixed: PricingLib._priceEdgeHop sizes the buy leg’s traverse with estChild = amountIn / midPrice, the fill estimated at the mid and not the fill delivered at the exec price, so the buy leg walks a slightly wrong x-interval. From $c>1$ the mid carries the inventory discount and the error lands trader-side. It is roughly 2 to 4 PBPS and size-independent (a fixed relative error, not a leak that scales), covered many times over by any shipped minFee, and not closed by bounding a slope: closing it needs the buy leg solved as a fixed point. Tightening the test’s tolerance to 0 is the acceptance criterion for that work.

Why per-edge safety suffices. Routes are unique tree paths (I-16), so any closed trading cycle is a closed walk in a tree, which crosses every edge equally often upward and downward. There is no cycle in the graph itself to accumulate a residue. Per-edge safety therefore gives cycle safety at any length and any depth, with no separate argument per path shape.

Integer exactness. Double flooring gives, for every x and every M:

with no hypothesis on rounding direction, because each direction floors independently against the same M. This needs no fuzz evidence: floor is monotone and the two maps compose to the identity, so the sign result is unconditional. It bounds the sign, not the magnitude; the residual in wei depends on M, on the decimal pair and on the sampling domain, so no single number characterizes it. Any bias in M cancels, since both directions consume the same integer. Only a direction-dependent construction of M can leak.

Round trip strictly loses. Beyond exactness, three independent terms each make the loss strict:

1. s_up <= 1 <= s_dn from spline monotonicity (C2): a sell traverses downward in depth, a buy upward, so the sell VWAP is at or below and the buy VWAP at or above the mid (PricingLib.sol). Tests test_bug2_sell_never_premium, test_buy_never_discount.
2. The fee is charged on both legs (I-3).
3. The coverage toll is charge-only (I-9).

Test: test_fuzz_roundtrip_never_profits.

Not enforced in code. The design mandates a per-leg assertion:

require(isUpward ? out * WAD <= in * M : out * M <= in * WAD);

No such require exists in the shipped code: a source scan finds isUpward only inside _executeLeg and _priceEdgeHop. Cycle safety rests on C0 through C4 plus the fuzz suite, not on a runtime check: D-5.

I-8. The m² counterexample

The cautionary case for C1, and the reason C1 is stated as “one integer, direction as multiply versus divide” rather than “invert the price”.

Suppose an interior downward leg inverts the rate but not the skew multiplier m: upward applies m, downward applies m again instead of 1/m. A closed cycle then returns m² rather than 1.

The leak per cycle is m^2 - 1, so it scales with the skew loaded and with the cycle length: extractable, repeatable and size-unbounded, and a function of configuration rather than a constant.

Three things to take from it:

1. It is a basis defect, not a topology defect. Restricting depth neither prevents nor closes it. What closes it is not re-applying skew after inverting.
2. It violates I-2 (value conservation) while I-1 (reserve conservation) holds throughout. Nothing about the reserve ledger is wrong.
3. Any price transform applied per direction, rather than derived from one shared integer, reopens this class.

4. Pricing bounds

I-9. Coverage toll is charge-only and terminal-only

Toll definition and the potential $Q\left(c\right)=\ln c-c+1$: Spread & Fees §6.1.

Enforced: PricingLib.sol. Properties, each with its site:

• Charge-only: dQ <= 0 => return 0 (PricingLib.sol). Never rebated. A coverage-restoring trade pays nothing, so no rebate ledger exists and a round trip strictly loses.
• Clamped to the increasing branch: Q is non-monotonic (maximum 0 at c = 1, decreasing on both sides), so both coverages are clamped to min(c, 1) before differencing (PricingLib.sol). Without the clamp a drain starting over-covered could cross the peg with dQ <= 0 and pay zero toll.
• Terminal-only: charged once, on cOut, in _settleQuote (PricingLib.sol). Never per-leg. Correct at any depth: dQ = 0 on an interior by I-1 and no path can drain an interior, so per-leg tolling would charge a displacement of zero.
• Telescoping: finite differences of Q telescope to 0 over any closed reserve loop at constant L. LP fee accrual raises L mid-loop, so the telescoping is only approximate; the residual is pool-favorable (higher L gives lower c gives more toll) (PricingLib.sol).
• Every listed asset including the hub is walled: kappaCovBps is required on every listed asset, base/hub included, and bounded on-chain to [MIN_KAPPA_COV_BPS = 50, SC.BPS = 10,000] (requireNeverDepletable; tests test_base_kappa_accepted_at_addAsset, test_kappa_below_floor_rejected_and_floor_accepted). The floor equals MAX_STABLE_DEPEG_BAND_BPS, so the resting coverage c_eq = kappa/(kappa+e) stays ≥ 1/2 at the tightest depeg band the pool enforces; kappa in [1,49] is refused because it is zero in substance. _covToll is output-only, so hub κ prices taking the hub out. Off-chain the emitter additionally gates spoke κ ≥ max(refBandBps, maxDev) and hub κ ≥ max spoke κ.
• Capped fill: the quote clamps gross output at the coverage argmax and refuses a size more than 2% of liabilities past it, view and swap alike, so a paid input never returns amountOut == 0 from the wall (Inventory Management §6.2). Tests: test_a_leg_at_its_floor_names_the_reason, test_view_and_exec_agree_at_the_boundary.

Tests: test_fuzz_toll_bounds, test_fuzz_toll_charge_only_overcovered, test_fuzz_toll_monotone_in_size, invariant_coverage_floor.

I-10. Mid-price bounds and the two floors

with $\psi$ the int8 skew index and $\kappa$ the leg’s live dispersion in PBPS.

• skew is the int8 from computeInventorySkew, hard-clamped at both ends (computeInventorySkew, PricingLib.sol). The bound above is the swing envelope, not the shipped law: the mid is mark·(PBPS + scaleY(evalQ(x0)))/PBPS at x0 = clamp(median + skew·BPS/200, 0, BPS). skew = 0 gives p_m = p_o exactly, for any curve shape, because the anchor is the curve’s density median (§I-7 C4).
• dispersion is per-asset in PBPS, so the mid shift is ±dispersion/1e6, not ±100%. It rises with σ one-for-one (at $\nu =10000$) off the leg’s fitted minDispersionPbps floor (PricingLib._calculateDispersion) and is clamped above only by the protocol-wide MAX_DISPERSION_PBPS = 900,000; there is no per-asset ceiling field. The write path checks the floor under PricingLib.dispersionCap(curve) = MAX_INTERIOR_SWING_PBPS · dispRefPbps · Q / span, the widest dispersion whose interior mid swing still fits the 1.0862% structural swing cap - a σ-driven κ past that cap reverts fail-closed on the swing rather than mispricing.
• One floor. PricingLib._flooredOffsetPrice clamps at SPLINE_MIN_OFFSET_PBPS = -0.9 * PBPS, i.e. the price never falls below 10% of mark. It is the single clamp on the quote’s downside, asserted by test_flooredOffsetPrice_clamps_at_ten_pct_mark, and every quote pays exactly one compare for it.

Therefore p_m = 0 is unreachable on every path: curve, dust (width == 0) and buy-sizing mid all route through that one clamp. There is no fourth path and no shapeless fallback: PoolConfigLib.validateCurveAssign refuses to list an asset without a curve, so every leg carries one and curveId = 0 is a refused-at-config sentinel rather than a routing branch.

I-11. Path spread is bounded below by the path fee floor

with $\underset{\_}{f_i}$ the leg’s floor, $f_{\min ,i}$ its stored minFeePbps, and $F_i$ its interior fence, which is 0 on an endpoint leg. $S$ is the round-trip spread: a swap pays $S/2$ once, on the output. minFeePbps is a floor on this spread, not on the fee.

The bound is one-sided. $S$ is bounded below, never above: a spread that a $\sigma$, confidence or staleness term drives wide is the price of that risk; a capped number would under-quote on the stale or high-CI tape an attacker times. Trader protection is minAmountOut: exact, caller-set, per trade, and composable. Bounding each leg’s contribution instead would make a 2-leg quote cost more than the same legs traded separately. See Spread & Fees §3.1.

Enforced: PricingLib._pathSpread. The spread is symmetric; there is no directional term. Every risk aggregate composes over legs and none is a max (Spread & Fees §3.2). Σ minFee_i is the additive base of $S_v$, not a clamp, which is why the lower bound needs no comparison at all. The interior fence folds into $\underset{\_}{f_i}$ at its one consumer (_priceInteriorLeg sets r.minFee = max(minFee, fence)), and saturation into uint16 cannot remove it: arithmetic at Spread & Fees §9.

Lower bound proof. S >= Σ floor_i because U_stale, U_conf >= 0 and S_v = Σ floor_i + (a non-negative σ term). Every term in the sum is non-negative and no term is clamped, so nothing can invert it. $\mathrm{\square }$

MIN_FEE_PBPS = 1 (0.01 bp) is the protocol floor on minFeePbps and ONE_PCT_PBPS = 10,000 (1%) is the ceiling on that floor, applied at every write path (initAsset, requestAssetParams). The two-sided bound sits on minFeePbps because that is the rate billed unconditionally on every swap, so it is the parameter an owner could otherwise set to an excessive charge; the quoted spread above it is a risk premium, not a policy number. Tests test_MIN_FEE_PBPS_setAssetParams_reverts_below_floor, test_MIN_FEE_PBPS_floor_spread_collects_fee, plus PathSpreadCompositionTest for the composition itself.

Deploy-config hazard: heterogeneous vegaBps. _pathSpread prices the path’s σ at the endpoint maximum, and nothing relates two assets’ vegaBps. The hazard needs only unequal vegaBps across a pool’s assets; fee floor and dispersion are per leg and unaffected. Bound and derivation: Spread & Fees §11.2.

I-12. Price impact is monotone in size

Enforced by the curve law. The execution price is the exact analytic integral of the quartic I-spline over [lo, hi] divided by the width (_priceEdgeHop, PricingLib.sol). hi - lo grows with amountIn, and the integrand is monotone by C2, so the VWAP moves monotonically against the trader in both directions. volumeFraction saturates at SC.BPS and endDepth clamps to [0, SC.BPS], so the property is preserved at the domain edges.

I-13. Depeg price bands on every priced node

A leg’s price bound is feed-relative, plus a per-asset USD depeg band that binds only where the mark is USD-attested (the base, a UOA leg, an INTERNAL leg’s gate mark). There is no absolute bound on an anchor-attested mark: it would raise a denomination question no static number answers. A discretionary “stop quoting this leg” call is the guardian halt.

The invariant is the feed-relative agreement band:

Enforced: PoolIOLib.priceBandGuard, called on tkOut then tkIn after the reserve mutation, plus PoolIOLib.priceBandGuardPath over every interior node of the route. refBandBps == 0 disarms it, and only the base is allowed to leave it disarmed: what the base carries instead is the parity halt in PricingLib._readBasePriceOrHalt, which reverts BaseDepegged past its per-asset band (code·250 bps; code 0 = 2,500 bps) and runs on every hop of every leg. That is why the path guard skips the base rather than double-charging a cold ref-feed round trip on the one node every path transits.

The comparison is in the primary’s own catalog unit, in numeric 1e18 space (both marks decode from one mark word to 1e18 WAD). Both sides fail closed: FeedMathLib.gate runs on the primary and on the reference, so a stale, dead or over-uncertain reference halts rather than anchoring the band to a dead price.

The reference is the same lane’s R tier in the mark store: a second attestation under its own roster and EIP-712 domain, never the primary tier. PoolConfigLib.validateOracleConfig requires a registered lane. A distinct domain is the on-chain floor, not proof of operational independence; disjoint rosters are a deployment obligation. See Mark Relayer.

Cumulative-bound mandate. An armed ref band is the only way to bound an EXTERNAL spoke, so refBandBps != 0 is required on every external spoke (PoolConfigLib.requireExternalSpokeBound). Per route, the sum of the nodes’ refBandBps is capped at MAX_ROUTE_REF_BAND_BPS = 600 (PoolIOLib.priceBandGuardAll, ThresholdViolation past it).

What this band is not. It is an agreement check between two independent attestations of the same pair, not a peg test, and it cannot be turned into one by pointing it at the absolute leg (see I-17). No parent-depeg breaker exists for an anchor-attested child (it would need a new field on Asset), so nothing in the contracts bounds a parent’s peg directly.

Tests: test_refBand_stale_reference_feed_fails_closed, test_refPrimary_independent_reference_bounds_walked_mark, plus the base-depeg parity tests.

I-14. Executable liquidity floor, not raw reserves

The enforced quantity is R_liq = R - R_inv (reserves minus the amount invested through a yield hook), checked pre-outflow:

Enforced: PoolIOLib.settle (PoolIOLib.sol), one function end to end: it computes need, calls PoolHooksLib.preOutflow to force a recall, then re-reads reserves and invested fresh, post-recall and reverts InsufficientAmount on shortfall before touching the ledger. Flash.maxFlashLoan uses the identical dual-ledger form (Flash.sol).

A fully invested asset can satisfy R >= L_min and still revert every swap. Pricing sees full R; only outflow sees R_liq.

minLiquidity is uint96, not uint128 (IPool.sol), in raw token units, bounded below 2^96 at requestAssetParams.

5. Anchor topology

I-15. Tree structure (bounded tree, MAX_DEPTH = 4)

The anchor graph is a tree rooted at the base: every asset has exactly one parent, which need not be the base, and every chain reaches the root within MAX_DEPTH = 4 edges.

Enforced: AnchorTreeLib.validateAnchor (AnchorTreeLib.sol):

• asset == anchor reverts.
• anchor == 0 is legal only for the base.
• The base may never be given a parent.
• An unlisted anchor reverts NotFound.

The walk to the root runs under two independent terminators, and neither is redundant: an explicit cur == asset check, which catches the cycle this assignment would close, and an unconditional step cap, which catches a chain that is cyclic or detached elsewhere. Neither subsumes the other: a disconnected 2-cycle has finite walk length and never reaches the root, so a depth counter keyed on reaching the root never fires. Depth past 4 reverts DepthExceeded (AnchorTreeLib.sol).

A per-node check at write time is not a global invariant: re-parenting an interior node silently lengthens every chain beneath it and no descendant is revalidated. findRoutingPath therefore re-walks under its own bound, so a malformed tree cannot price a swap whatever order the admin writes ran.

Pinned by the anchor-validation tests:

• depths 2, 3 and 4 accepted;
• depth 5 rejected;
• the detached 2-cycle;
• the spliced depth-5 chain caught at routing time;
• the 8-leg / 9-node worst case.

Topology is configuration, and there is no feature flag. The anchor column in a pool’s risk-param file is the sole expression of that pool’s topology: filling one cell deepens that pool’s tree and puts the interior fence in the path of every route through it. A first fill is gated on:

• an independent audit of the interior-leg law;
• the mark provider serving the cross pair as a first-class series (registration alone leaves no live mark and no sigma);
• the indexer reading quoteUnit instead of re-deriving denomination off chain.

None of those is a contract gap: MAX_DEPTH = 4 and everything under it is enforced.

I-16. Route uniqueness and length

The route is the unique tree path: up from tokenIn to the LCA, then down to tokenOut. There is no route selection, so a quote cannot depend on a routing choice.

MAX_DEPTH = 4 bounds one walk; a path is two walks meeting at the LCA, so MAX_PATH_LENGTH = 2 * MAX_DEPTH + 1 = 9 nodes and 8 legs. The worst case is two depth-4 leaves whose LCA is the root. Any “5 nodes, 4 legs” statement is wrong and mis-sizes every summed path budget. Anything that cannot be resolved reverts InvalidPath.

On a flat roster this degenerates to the two familiar shapes, [in, out] and [in, base, out], and the base hub supplies no leg profile: _executeLeg sets profileAsset = isUpward ? from : to, so an edge always prices off the child.

I-17. Interior legs

• Interior legs price off mid (skew included) and charge no spline impact. Skew belongs there because it is pricing, not a charge for inventory change: if the pivot is under-covered its value to the pool is depressed, and pricing the hop at the unskewed mark gives the trader the pivot’s depeg risk at no charge. Impact must not be charged: dR_interior = 0 by I-1, so charging it would monetize path-dependence and replace an exact identity with a size coincidence.
• One law per edge (C3 in I-7): the interior mid is _legMid, byte for byte the expression the terminal leg quotes that same edge with. The curve is centered at the write (NUQuarticLib._centre, NUQuarticLib.sol), so no read path re-centers; a swing past MAX_INTERIOR_SWING_PBPS = 10,862 reverts, because a clamp is a law fork that bites on the interior leg only.
• Interior skew cancels on a round trip only against unchanged interior coverage. An interposed trade that moves an interior node’s coverage between the two crossings breaks the cancellation (+2.96 bp measured under max aggregation, +1.01 bp under sum). The fence that prices it is max(minFee_i, fence_i) in the path floor, fence_i = ⌈swing_i·PBPS/(PBPS - cap/2)⌉ off the leg’s own live swing, computed per quote and folded straight into the leg’s fee floor (Anchor Path Pricing §3.2). Rejected alternatives, recorded so they are not retried: an interior reserve clamp (-9900 bp, destroys the tree), kappa on interiors (no-op, the toll is terminal-only), freezing the edge rate for a path (no-op, the manipulation is cross-transaction), and four earlier fence shapes (§3.4).
• On an interior-capable leg the dispersion band is bound at the write to PricingLib.dispersionCap of the asset’s curve, so a live interior asset never reaches the interior revert; the floor is checked, never clamped.
• Marks are attested in units of assets[X].anchor (parent-per-child) and the pool re-denominates nothing, except the QUOTE_UNIT_UOA bridge, which config restricts to assets anchored directly to the base. OracleConfig.quoteUnit (uint8): 0 = QUOTE_UNIT_ANCHOR (the norm, no re-denomination), 1 = QUOTE_UNIT_UOA (divide out the base’s USD price). No stored per-asset price bound exists to raise the same denomination question (I-13).
• The coverage toll stays terminal-only at any depth (I-9). A walled asset may be a parent. Hub κ is not keyed off; _covToll fires when that token is the output.
• The ref band is what runs on every priced node: PoolIOLib.priceBandGuardPath guards every interior hop except the base, and priceBandGuard guards both endpoints (I-13). The base parity halt does not generalize: _readBasePriceOrHalt is gated on hop == $.baseToken, so it tests the base mark against 1e18 and nothing else, at any depth. Neither expresses a peg test for a parent (next bullet).
• A parent-depeg breaker does not exist for an anchor-attested child. The reference band is a same-unit agreement check between two attestations of the same pair on one lane, not a peg test: PoolIOLib.sol computes dev = |pRaw - refP| and reverts past refP * refBandBps / BPS. The per-asset USD depeg band is absolute but reads only a USD-attested mark, so it does not see a stETH/ETH child’s parent depeg either. Making it visible needs a new absolute-depeg field for anchored legs. It is not built. See Anchor Path Pricing §7.1.
• Re-anchoring is a re-rooting and is timelocked at the GOVERNANCE base-migration tier, atomic with the oracle config in one payload (requestOp(..., UPDATE_ANCHOR, ...) → executeUpdateAnchor): re-anchoring X to P while X’s feed is still attested in base units mis-prices the leg by the parent’s price and drains the reserve in one block.

6. Oracle invariants

Formulas and gate mechanics are specified once, in Mark Relayer.

Generation. The launch store is MarkStoreP8, run by the Pool implementation (Mark Relayer §8). Three write-side properties hold throughout: a failing lane is skipped, not reverted; the replay guard is one accepted write per lane per source second; σ and confidence floor at the realized move on every accepted mark.

I-18. Every priced or gating feed clears the same triad

FeedMathLib.gate reverts on:

Each lane holds one observation second (its word’s clock minus its 12-bit age), served as both updatedAtSecs and sourceTsMs. Relabeling is closed at the push: a source second outside [now − 120 s, now + 5 s] is rejected (StaleData, FutureTimestamp), and the per-lane clock is strictly increasing, so a withheld segment cannot be replayed forward. A lane whose age saturates at 4,095 s reads stale under every class (class ttl at most 4,089 s).

The same gate covers the primary mark, the base mark, the INTERNAL-mode gate mark and the reference mark. An uncertain safety feed must never silently permit execution.

A mark landed in the current block is not gated: that would let any listed relayer revert every priced call by relaying one signed segment per block. One pool call loads each leg’s mark word once at its start (PricingLib._loadMarks), so every leg of the call reads one mark (Mark Relayer §5.3).

I-19. Marks are strictly positive

p_o > 0 for every feed that reaches a quote. Enforced twice: at write and at read (FeedMathLib.gate). P8 enforces it structurally: the lane float carries a hidden leading bit and an exponent code of at least 1, a mark with an exponent outside the lane range is not accepted, and a dark or halted lane reads markless and fails the gate.

I-20. Stored σ is bounded and floored

with $\hat{\sigma }$ the stored value, $m$ the mark, $m_{-}$ its previous value, both in PBPS. The upper bound is the σ8 code’s range; every read clamps to the lane class’s minSigma, including a σ stored before a class retune raised the floor.

The floor is the compromised-signer backstop. A signer signing σ = 0 would collapse the spread to the minFee floor and make a mark-then-self-swap round trip spread-free. Flooring at the realized move forces a proportional spread. It runs on every accepted mark, whether or not the segment carried a σ byte; confidence floors the same way. A σ byte on a lane that did not advance only raises a dark, anchored lane’s σ.

I-21. One accepted write per lane per source second

The guard is per lane, not per word, and the clock is the absolute source second the segment carries. A lane whose observation second is not strictly older than srcSecs is skipped in silence: that lane only, no event. Equal fails closed because a retry landing in the same source second is the replay this guard exists to close. Several pushes may therefore land in one block if their source seconds differ, and a lane accepts nothing twice at one source second. Intra-transaction read consistency does not rest on this rule at all: a pool call loads each leg’s mark word once before the first leg runs.

There is no on-chain EMA to freeze: mark and σ are overwritten directly on each accepted push.

I-22. Per-push deviation band

Canonical statement: Mark Relayer §5.4. Kept facts: $\beta ={\delta }_{\max }+\min (6\sigma \sqrt{\mathrm{\Delta }{t}_{src}/1800}/100,9{\delta }_{\max })\le 10{\delta }_{\max }$; $\sigma$ = the lane’s stored σ clamped to its class floor, never the incoming segment’s own; ${\delta }_{\max }$ the class maxDev, 1 to 2,000 bps; $\mathrm{\Delta }t$ runs from the lane’s own observation second, so a dark lane’s heal band grows from its last accept.

Three qualifications on this invariant:

• A breach darkens the lane, it does not revert the push. The lane keeps its mark as the anchor and reads markless; every other lane in the segment lands. No event is emitted.
• The band is conditional on a previous mark. It compares against the live mark, or on a dark lane against its anchor. A newly registered lane, or one the owner reanchored, has no mark, so its first push is unbanded.
• Past the ceiling the band does not release itself. A lane dark past $10{\delta }_{\max }$ is released by the owner’s reanchor(lane, tierMask) at TUNING, which drops the anchor so the next push lands unbanded. The band binds per segment, not per transaction: one relayer transaction can chain about 125 advancing segments; the cumulative bound is the reference tier.

7. Flow guards

I-23. No reentrancy

Pool inherits solady ReentrancyGuardTransient through @btr-shared/base/TransientGuard.sol, which overrides _useTransientReentrancyGuardOnlyOnMainnet() to false so the guard TSTOREs on every chain, and marks every value-moving entrypoint nonReentrant (Pool.sol). Separately, a second transient slot (FLASH_INFLIGHT_SLOT, PoolIOLib.sol) is set for the duration of a flash callback and is checked by PoolIOLib.requireNoFlash on every path that credits reserves or moves liabilities, hook books or pool balances: PoolIOLib.pull (deposit, donate, swap), withdrawTo (both exits), swapLiability, the hook writers (Pool._hookAuth), both hook clears, claimTreasury and the sweep (Pool.adminSweep). So a borrower cannot “repay” by crediting reserves and double-count the principal, and cannot move liabilities mid-callback either. There is no batchSwap and no on-chain multi-swap call. ERC-3156 repayment is a plain transfer and is unaffected.

I-24. Anti-JIT lock is a frozen quantity, not a per-user timestamp

The commonly stated JIT form t - t_last[user][asset] >= τ is wrong. The lock is per holder, per LP receipt, over a quantity:

with $M\left(h\right)$ the movable balance of holder $h$, $b_h$ its LP balance, $s_h$ the mint stamp, ${\phi }_h$ the frozen quantity, $\tau$ the cooldown and $t$ = block.timestamp.

Enforced: LPToken.locks[owner] = {stamp, frozen} armed on mint and checked in LPToken._beforeTokenTransfer, which does not skip the to == address(0) case: burn is the redeem path and is what the lock gates. Withdrawal sizing reads it back through PoolLiquidityLib.maxRedeem / _unlockedShares; there is no PoolView contract. τ = $.flowCooldownSecs, default DEFAULT_FLOW_COOLDOWN_SECS = 15 s, hard-capped at MAX_FLOW_COOLDOWN_SECS = 300 s (PoolConstantsLib.sol, PoolConfigLib.setFlowCooldown).

The cap is the key invariant: the setter is untimelocked and the receipt is transferable, so 300 s is the worst-case unavailability one compromised admin key can impose on every holder of every leg. Shares held from before the lock window are unaffected, so an ERC-4626 wrapper locks its dust rather than its whole pooled balance.

Test: test_swapLiability_respects_flow_cooldown, plus the LP flow-guard suite.

8. Curve invariants (quartic I-spline)

I-25. Knot ordering

NUQuarticLib._validate (NUQuarticLib.sol); segments capped at MAX_SEGS = 14 (NUQuarticLib.sol), and a degenerate all-flat weight vector is rejected.

I-26. Monotone curve

Nondecreasing control weights give a nondecreasing depth curve, so marginal liquidity is never negative, at any spline degree. This is C2 of I-7 and the source of s_up <= 1 <= s_dn.

I-27. C2 density

Simple interior knots at degree 4 make the density y'(x) C2, smooth at every knot, with no value discontinuity at any knot.

I-28. Dispersion scaling preserves both

Quotes y-scale the fitted curve by dispersion/dispRefPbps (PricingLib._scaleY, PricingLib.sol). A linear y-scale preserves monotonicity and C2 exactly. dispRefPbps == 0 is rejected at write, because _scaleY divides by it (NUQuarticLib.sol).

I-29. Normalized utilization

0 <= u <= 1, held by the explicit clamps at PricingLib.sol (volumeFraction) and PricingLib.sol (endDepth).

9. Economic claims

I-30. No free lunch (CONDITIONAL, see I-7)

“No sequence of swaps within AIMM yields profit absent an external price difference” is not an independent invariant. It is exactly Π_cycle < 1, and it holds only under C0, C1 and C2. I-8 gives a construction that breaks it. State it as a conclusion of I-7, never as an axiom.

I-31. LP solvency (pool level)

Coverage is per leg; LP solvency is pool-level. Every mint, credit and exit settles at C = Σ R̂_k·m_k / Σ L_k·m_k over the leg roster (PoolSolvencyLib.solvency), uncapped, with each leg’s reserves capped at physical backing. A deposit, a donation and a hook yield credit book face at C; a same-asset exit pays face · min(c_leg, C), less the exit toll (Inventory Management §5.2); a cross exit and a liability swap convert face · C; a hook write-down cuts face at C. None of them lowers C except by the lag of the cached lastGoodC the exit’s LP fee credit is booked at (PoolLiquidityLib._credit). With any roster mark unusable every credit path refuses (FeedUnavailable) and only the same-asset exit settles, at min(c_leg, C_lower): C is a mediant of the usable-leg rate and each dark leg’s backed r/l, so the minimum of those bounds it whatever the dark marks are (PoolSolvencyLib._sweep). A dark leg with no backed reserves sets C_lower = 0 and closes the hatch until it is halted and written down. A write-down booked while a leg is dark cuts face at the same bound, clamped into [C_lower, C_upper]. lastGoodC is a stamp for reporting and for booking swap and exit fee credits, never an exit or mint settlement rate. C >= 1 is neither guaranteed nor enforced: a real NAV loss lands in C and every LP in the pool shares it. Derivation and test roster: Inventory Management §5.

I-32. The exit rate cannot be escaped

No exit reads a rate the exiter can move. A cross exit and a liability swap price off C, never off the source leg’s coverage, which rises as its liabilities burn, so slicing gains nothing; neither pays or credits above face · C. A same-asset exit is allocated min(c_leg, C) pro-rata, so amt <= R holds and reserves cannot be driven negative by an exit sequence. Self-drain round trips stay unprofitable against the pooled rate. Tests: §11.

10. Open gaps

Documented as behavior, not as intent.

D-5. Cycle safety has no runtime assertion

See I-7. C0, C1 and C2 hold structurally and are covered by fuzz, but no require enforces the per-edge inequality. A future refactor that reintroduces a direction-dependent price transform would reproduce I-8, and no test outside the dedicated round-trip fuzz would catch it.

11. Verification

11.1. Compile-time

Solidity type widths carry the parameter bounds in section 12. They are not documentation: a uint16 fee field is the ceiling.

11.2. Shipped invariant tests

11.3. Gaps

Invariant gaps: §10. Parameter-level gaps: Parametrization §14.

12. Parameter bounds

12.1. Fee

minFeePbps is a floor on the path spread, per leg, not on the fee. The fee is half the spread, charged once on the output.

RiskFences.vegaHardMinBps / vegaHardMaxBps are not the write-path bound on $\nu$. They are enforced only inside AdminParamsLib.setBounded, reached from Admin.setAssetParamsBounded (the risk-steward lane), which refuses to run at all on an unseeded fence (maxDeltaBps == 0 reverts NotConfigured); the owner lane Admin.requestAssetParams checks only minFeeHardMinPbps and the coop fences. A per-leg window is not a relation across assets, so the bound on $\nu$ is $\nu \ne 0$, plus the dispersion cap at live σ on a raise (Parametrization §2).

RiskConfig is the whole of { uint16 flags; uint16 kappaCovBps; uint16 depositCapCode; uint16 maxLiabWeightBps; }, and the inventory skew is a fixed law with no per-asset dial (I-7 C4). The bound above is the only two-sided bound on a fee rate anywhere in the pool.

12.2. Liquidity and coverage

Asset is 3 slots and carries nothing else: reserves, liabilities, anchor, minLiquidity, liquidityIndexWad, minDispersionPbps, curveId, minFeePbps, vegaBps, depositCapCode, decimals, deadSeedPow10, flags, kappaCovBps, maxLiabWeightBps, oracleBits, refBandBps. flags, kappaCovBps, depositCapCode and maxLiabWeightBps are the RiskConfig quartet, which is an ABI and memory type only and is stored here, in slot 2, not in a mapping of its own. (maxDispersion is not among them: the σ-driven band ceilings at the protocol constant, not a stored field.) A leg’s price bound lives on OracleConfig (lane / refBandBps, plus the per-asset USD depeg band, I-13), and the traverse denominator is the leg’s raw reserves with a zero-guard, taking no coverage adjustment and no per-asset field.

12.3. Oracle

13. Related

• Inventory Management: coverage formulas
• Liquidity Shaping: spline construction
• Anchor Path Pricing: routing and leg composition
• Spread & Fees: fee terms
• Parametrization: parameter ranges
• Mark Relayer: feed struct, gates, deviation band
• Flow Guards: base and spoke circuit breakers
• Mark Relayer: quorum, ceremony, cumulative bound
• Flow Guards: reentrancy and JIT