AIMM invariants

This page is the register of properties AIMM claims to hold on every path, at every depth, in every pool. Several are conditional (they hold only while a specific construction is preserved) and those conditions are stated here rather than assumed. Read §1 first: the status labels separate what deployed code enforces from what is merely decided, and one entry is a live defect.

1. How to read this page

Each entry states the constraint formally, its enforcement site, and the consequence of violation. A claim with no enforcement site is an aspiration, not an invariant, and is labeled as such.

Every invariant below is enforced by deployed contract code. Where one holds only under a stated condition, the condition is named with it; nothing here describes intent that the contracts do not already implement.

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: Oracles §5).

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 + q.protoFee);

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 (Pricing._walkLegs, Pricing.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 says nothing about 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 merely asserts I-2.

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

Enforced: Pricing.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: PoolIOLib.settle credits the full amtIn to reserves (PoolIOLib.sol). An input-side skim would be an LP-reserve drain, since the gross output is already priced off the full amtIn.

S <= 65,535 PBPS by the saturating narrowing in _pathSpread: the raw spread is a uint256 sum, so the single cast into SwapQuote.spreadPbps clamps rather than wraps. That is the only upper bound on S and it is a field width, 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: PoolLiquidity.sol (withdrawValue = lpAmount * liquidityIndexWad / WAD), PoolLiquidity.sol (liabIn). liquidityIndexWad is uint96 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: at the shipped haircutSuppressorBps = 0 a same-asset exit is coverage-neutral, not coverage-raising (I-6, I-32). The paths that do 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 hookWriteDown is the only index-lowering writer.

idx == 0 is not a lazy-init sentinel: it means the leg was written down to total loss, every share is worth 0, and the leg accepts no further deposits (PoolConstantsLib.sol).

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; it appears only in an external Compound interface. 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, Pricing.sol).

Deposit of a at c <= 1:

A donation raises both sides by the same a and additionally scales the index (PoolLiquidity.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 (PoolLiquidity.sol), so total outstanding claim can never exceed liabilities.

A same-asset withdrawal is coverage-neutral at c = 1 ((R-a)/(L-a) = 1) and, at the shipped haircutSuppressorBps = 0, at every coverage below it as well: the haircut ratio is the deficit itself, so the payout is y = x·R/L against a full-face x liability burn and (R - xR/L)/(L - x) = R/L exactly, up to the ceil-div dust the pool keeps. The exiting LP takes its pro-rata share of the deficit and moves the ratio nowhere. haircutSuppressorBps >= HAIRCUT_SUPPRESSOR_FULL_BPS = 20,000 would disable the haircut entirely, and config caps strictly below that so a deficit is always at least partially socialized (HAIRCUT_SUPPRESSOR_FULL_BPS, PoolConstantsLib.sol); a walled leg is pinned at exactly 0, so the neutral case is the only reachable one.

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)

This is not free. 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: Pricing._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 (Pricing.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 holding by construction plus the fuzz suite, not on a runtime check. Status: DESIGN. See 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 actually 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 perfectly throughout. Nothing about the reserve ledger is wrong.
3. Any price transform applied per direction, rather than derived from one shared integer, reopens exactly this class.

4. Pricing bounds

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

with c_0 = R_0/L and c_1 = (R_0 - y_gross)/L.

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

• Charge-only: dQ <= 0 => return 0 (Pricing.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 (Pricing.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 (Pricing.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) (Pricing.sol).
• Every listed asset including the hub is walled: kappaCovBps > 0 on the base is allowed (requireWallOk; test test_base_kappa_accepted_at_addAsset). Old P3 “base never walled” is void. _covToll is output-only, so hub κ prices taking the hub out. κ=0 is forbidden.

Tests: test_fuzz_toll_bounds, test_fuzz_toll_charge_only_overcovered, test_fuzz_toll_monotone_in_size, invariant_coverage_floor.

DEFECT (D-2): the wall’s saturation branch returns grossOut and silently produces amountOut == 0 rather than reverting.

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, Pricing.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 (Pricing._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 Pricing.dispersionCap(curve) = INTERIOR_SWING_CAP_PBPS · dispRefPbps · Q / span, the widest dispersion whose interior mid swing still fits the 1% structural swing cap - a σ-driven κ past that cap reverts fail-closed on the swing rather than mispricing.
• One floor. Pricing._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: PoolConfig.validatePresetAssign refuses to list an asset without a curve, so every leg carries one and presetId = 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, deliberately. $S$ is bounded below, never above: a spread that a $\sigma$, confidence or staleness term drives wide is the honest price of that risk, and quoting a capped number instead would sell an underpriced quote on exactly 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: Pricing._pathSpread. The spread is symmetric; there is no directional term. Every risk aggregate composes over legs and none is a max:

• S_v = Σ minFee_i + σ_path·max(vega_in, vega_out)/(100·BPS), with σ_path = sqrt(Σ σ_i²) in quadrature (_walkLegs, rooted at _pathSpread). Σ minFee_i is the additive base, not a clamp, which is why the lower bound needs no comparison at all.
• U_stale = Σ_i STALE_Z·σ_i·√(τ_i)/BPS, per leg off that leg’s own age and σ, zero inside the keeper grace min(ttl/2, STALE_GRACE_CAP_SECS = 30 s) (_staleTerm, _staleExcessOf, summed in _walkLegs). STALE_Z = 100.
• U_conf = (Σ_i confidence_i) · (PBPS/BPS). It shares the riskPath accumulator with U_stale, exactly: the two were only ever consumed as a sum and the scale is an integer constant.
• The interior fence folds into $\underset{\_}{f_i}$ at its one consumer (_priceInteriorLeg sets r.minFee = max(minFee, fence)). It is not a separate accumulator: the fence and the leg’s own floor are the same quantity by the time the path sums them.
• Saturation into uint16 cannot eat the fence. The composed interior fence is bounded by construction and the raw spread is bounded below by it, so what saturates away is the σ/CI/staleness surcharge, never the security floor. Arithmetic: Spread & Fees §9. SwapQuote.spreadPbps is a field width, not a fee policy.

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, setAssetParams). 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 grandfather into an extortionate 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 constraint: vegaBps should stay uniform across assets. Nothing in the contract enforces it, and the untimelocked tighten path can introduce heterogeneity one asset at a time because a vega raise classifies as defensive. Inert while vega stays uniform; live the moment anyone tunes it per asset. Derivation: Spread & Fees §11.2.

I-12. Price impact is monotone in size

Enforced by construction. The execution price is the exact analytic integral of the quartic I-spline over [lo, hi] divided by the width (_priceEdgeHop, Pricing.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 and is the only per-asset one. There is no stored absolute price bound: it would raise a denomination question (base-per-asset or anchor-per-asset, and what holds when the base itself depegs) that 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 Pricing._readBasePriceOrHalt, which reverts BaseDepegged past BASE_DEPEG_HALT_BPS = 500 bps from 1e18 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 the star always transits.

The comparison is in the primary’s own catalog unit, in numeric 1e18 space (both marks arrive as mark1e18 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 corpse price.

The reference is read from oc.refPrimary, a separate oracle instance, never oc.primary. PoolConfig.validateOracleConfig enforces refPrimary != primary and reachability whenever refBandBps != 0. Address inequality is the on-chain floor, not proof of operational independence; the deploy-time preflight checks operational disjointness. See Oracle Price-Push Security §4.6.

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 (PoolConfig.requireExternalSpokeBound).

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). A parent-depeg breaker would need a new field on Asset; it is roadmap rather than deployed, so nothing in the shipped contracts bounds a parent’s peg directly.

Tests: test_refBand_stale_reference_feed_fails_closed, test_refPrimary_independent_reference_bounds_walked_mark, test_refPrimary_zero_failClosed, 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 setAssetParams.

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;
• NX Rates 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 nothing to search and nothing to choose, 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 worth to the pool is depressed, and pricing the hop at the undepressed mark hands the trader the pivot’s depeg risk for free. 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 (NUQuartic._centre, NUQuartic.sol), so no read path re-centers; a swing past INTERIOR_SWING_CAP_PBPS = 10,000 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 five earlier fence shapes (§3.4).
• The dispersion band is bound at the write to Pricing.dispersionCap of the asset’s preset, so a live 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 in any field. OracleConfig.refFeedId is a same-unit agreement check between two independent attestations of the same pair, not a peg test: PoolIOLib.sol computes dev = |pRaw - refP| and reverts past refP * refBandBps / BPS, and PoolConfig.sol requires refPrimary != primary. Pointing it at the absolute leg would brick the pool: a stETH/ETH primary near 1.15 against a stETH/USD reference near 4000 gives dev/refP ~= 99.97%, past any band, so the first swap reverts and so does every one after it. Making a parent depeg visible needs a NEW field (absFeedId plus absBandBps) or a split of refFeedId into an agreement band and an absolute-depeg band. Neither is built. See Anchor Path Pricing §7.1.
• Re-anchoring is a re-rooting and is timelocked at the CRITICAL base-migration tier, atomic with the oracle config in one payload (requestOp(..., UPDATE_ANCHOR, ...) → executeAnchorUpdate): 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 Oracles §8.3 and Price-Push Security §5.

The live oracle is ExternalOracleV4. The read-side invariants below (I-18, I-19) hold on every generation. The write-side ones are stated against V1 and differ on V4 in three ways, each noted in place: a failing lane is skipped, not reverted; the replay guard is one accepted write per slot per source second, not one per feed per block; and the σ floor runs only where the σ word is already loaded.

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

FeedMathLib.gate reverts on:

observedAt = min(sourceTs/1000, updatedAt) when signed, else updatedAt (FeedMathLib.observedAt). Taking the minimum is what closes withheld-blob relabeling: a relay stamping updatedAt = now on an old signed quote does not refresh it. Signed-path clock skew is deliberately not capped to block.timestamp, which would push the observation forward every block and extend TTL.

On V4 the minimum is an identity: the contract stores one reconstructed source time per slot and no landing time, so updatedAt == sourceTs/1000. Relabeling is closed by the acceptance window instead — a reconstruction outside [now − MAX_RECON_AGE, now + 5] is rejected on the push and read as now − 21601 on the read, which is stale under every deployed ttl.

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

A mark landed in the current block is deliberately not gated: withholding it would hand any address a pool-wide outage switch, since the signed push path takes authority from signatures rather than msg.sender.

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). V1 validates the decoded mark; V4 enforces it structurally — a lane whose mantissa MSB is clear is the STALE sentinel, and a write of one is refused (the lane is skipped), so no accepted lane decodes to zero.

I-20. Stored σ is bounded and floored

with $\hat{\sigma }$ the stored value, $m$ the mark, $m_{-}$ its previous value, and both sides in PBPS.

Enforced: cap at PoolConstantsLib.sol, applied on the signed sample and again on the realized-move floor; floor via the push path, which itself caps at MAX_SIGMA_PBPS.

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, so the round trip is spread-negative.

The floor is spread-side only. It cannot ratchet the deviation band, because the band caps its σ term at 9·maxDeviation independently.

V4 weakens the floor to a conditional. σ/confidence elision is total: a push carrying no σ entry for a slot never loads that slot’s σ word, and the floor is applied only where the word is already in memory — the deviation-band slow path (a move past maxDeviation), or a slot the blob carries σ entries for. A sub-band move in a σ-less blob leaves the stored σ untouched, so the equality above is a bound the floor reaches, not one it holds on every push. V4 stores σ at 16-pbps granularity, rounded up, so the stored value never understates the attested one.

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

V1: Δt = block.timestamp − updatedAt = 0 ⇒ revert CooldownActive, with a duplicate idx inside one batch failing closed on the second record.

V4 replaces both the rule and its failure mode. The guard is per-slot strictly increasing reconstructed source seconds: a slot whose incoming source second is not strictly newer than its stored one is skipped in silence — the whole slot, no event. Several pushes may therefore land in one block if their source seconds differ, and none may land across blocks that share a source second. A repeated or descending gi inside one blob section still fails the blob closed with BadBlobHeader. Intra-transaction read consistency does not rest on this rule at all: Pricing._primePath pins every feed a path touches into transient storage 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: Oracles §8.3. Kept facts: $\beta ={\delta }_{\max }+\min (6\sigma \sqrt{\mathrm{\Delta }{t}_{src}/1800}/100,9{\delta }_{\max })\le 10{\delta }_{\max }$; $Z=6$, $T=1800$ s, $X=9$; $\sigma$ = stored prior in PBPS (never the incoming push’s own); ${\delta }_{\max }$ mandatory non-zero, capped at MAX_DEV_THRESHOLD $=2,000$ bps; V1 fallback $\mathrm{\Delta }t=t-t_{upd}$ on never-pushed feeds, V4 fallback MAX_RECON_AGE $=6$ h on out-of-window predecessors (both stored-state-derived).

Three V4 qualifications on this invariant:

• A breach skips the lane, it does not revert the push. The lane keeps its previous value, its bit is cleared in acceptedMask and set in LanesSkipped, and every other lane in the blob lands.
• The band is conditional on a previous mark. It runs only when EXPRESS is false — it is false on every deploy path — and the lane already holds one. registerFeed seeds no mark, so a newly registered feed’s first push is unbanded: there is nothing to compare it to.
• Past the ceiling the band does not release itself. updateFeed is tighten-or-equal for the owner as well as the guardian, and narrowMaxDeviation does not exist on V4. Shipping in the next release, a feed wedged past 10·maxDeviation is released by the owner’s requestFeedWiden → BASE delay → executeFeedWiden, which clears the lane and the rebias band anchor so the next push is unbanded — the same exemption the bullet above describes for a newly registered feed, reached deliberately. Until it ships, recovery is redeploying the oracle and repointing each leg through a BASE-tier UPDATE_ORACLE.

The claim “the first signed push collapses the band to the bare maxDeviation floor” is false against HEAD on both generations. It describes pre-fallback V1 code and would reintroduce the seeded-feed deadlock the fallback exists to prevent.

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 at exactly four sites: PoolIOLib.pull, the reserve-crediting chokepoint shared by deposit, donate and swap; PoolLiquidity.withdrawTo; PoolLiquidity.swapLiability; and the hook writers on Pool. 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 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 deliberately does not skip the to == address(0) case: burn is the redeem path and is exactly what the lock gates. Withdrawal sizing reads it back through PoolLiquidity.maxRedeem / _unlockedShares; there is no PoolView contract. τ = $.flowCooldownSecs, default DEFAULT_FLOW_COOLDOWN = 15 s, hard-capped at MAX_FLOW_COOLDOWN = 300 s (PoolConstantsLib.sol, PoolConfig.setFlowCooldown).

The cap is the invariant that matters: 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

NUQuartic._validate (NUQuartic.sol); segments capped at MAX_SEGS = 14 (NUQuartic.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 by construction, with no value discontinuity at any knot.

I-28. Dispersion scaling preserves both

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

I-29. Normalized utilization

0 <= u <= 1, held by the explicit clamps at Pricing.sol (volumeFraction) and Pricing.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 (per leg)

Coverage is per leg, so solvency is per leg: L_i <= R_i whenever c_i >= 1, which is the definition of c_i. The pool-wide value form Σ L_i·p_i <= Σ R_i·p_i follows only if every leg is at or above full coverage, which is not guaranteed and is not enforced anywhere. Do not cite the aggregate form as an invariant.

I-32. Haircut effectiveness (bounded)

The haircut socializes a deficit on withdrawal below full coverage, so reserves cannot be driven negative by an exit sequence. haircutSuppressorBps is capped strictly below HAIRCUT_SUPPRESSOR_FULL_BPS = 20,000 (PoolConstantsLib.sol, checked at PoolConfig.sol), so it can dampen but never disable the socialization. Cross-path exits do not escape it: tests test_cross_withdraw_cannot_escape_coverage_haircut, test_swapLiability_cannot_escape_coverage_haircut, test_haircutSuppressor_cap_rejected, test_walled_asset_rejects_nonzero_haircut_suppressor.

10. Open gaps

Documented as behavior, not as intent.

D-2. Full-drain toll yields an amountOut == 0 view quote (exec-side fixed)

_covToll returns grossOut when grossOut >= r0 (Pricing.sol). _settleQuote then subtracts it (Pricing.sol), leaving acc.currentAmount == 0, so feeOut == 0 and quote.amountOut == 0 (Pricing.sol).

On the executing path this is closed: Pricing.swap reverts Err.ZeroValue on out == 0 before settlement (Pricing.sol; see Slippage & Price Impact §4.1), so a fully-tolled drain can no longer consume its input and deliver nothing.

What remains is the view-quote shape: getSwapQuote still returns a fully populated SwapQuote with amountOut == 0 instead of surfacing the failure. A caller that skips an explicit amountOut > 0 check sees an executable-looking quote that can never fill.

Remaining fix: surface the zero at the quote boundary rather than leaving callers to discover the wall by inspecting amountOut.

D-5. Cycle safety has no runtime assertion (live)

See I-7. C0, C1 and C2 hold by construction 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

D-2 (zero-output view quote): the exec-side fix is shipped - Pricing.swap reverts Err.ZeroValue on out == 0 before settlement. Still open: no test pins the revert, and the view quote still returns a populated SwapQuote with amountOut == 0.

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 Admin._enforceHard, 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.setAssetParams checks only minFeeHardMinPbps. No deploy script calls setRiskFences, so on Arc the fences are unseeded and $\nu \ne 0$ is the whole bound.

RiskConfig is the whole of { uint16 flags; uint16 kappaCovBps; }, 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, presetId, minFeePbps, vegaBps, haircutSuppressorBps, decimals, deadSeedPow10, flags, kappaCovBps. The last two are the RiskConfig pair, 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 (refFeedId / refBandBps, plus the base parity halt, 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
• Oracles: feed struct, gates, deviation band
• Depeg Halt: base and spoke circuit breakers
• Oracle Price-Push Security: quorum, ceremony, cumulative bound
• Flow Guards: reentrancy and JIT