> For the complete documentation index, see [llms.txt](https://docs.jaawle.xyz/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.jaawle.xyz/security/invariants.md). # Invariants The properties worth asserting in tests, and the one reason each exists. They follow the sections of [Design](/security/design.md); the contract test suite (`test/*.t.sol`) and the backend's fakes-based tests are where they live. ## NAV and shares * [ ] `totalAssets() == (usdcBalance + usdPlusBalance + pendingUsdc) × 1e12 + (stockBalance + pendingStock) × bid − poolExposure`. NAV is built from internal counters only; a wrong term mints or burns against a wrong price. * [ ] Sending USDC or shares directly to a pool does not change `totalAssets()` or `sharePrice()`. Donations must not move NAV. * [ ] `sharePrice()` never decreases from a deposit or a redemption alone. Rounding goes against the requester, never the pool. * [ ] Shares minted on a deposit round down; shares burned on a redemption round up. Dust stays with the pool. * [ ] A deposit below `minDepositUsd` is refused at request time. Dust requests are not queued. * [ ] Placing an issuer order leaves `totalAssets()` unchanged. Escrow in flight is still NAV. * [ ] Settling an issuer order with `filled = 0` refunds the full escrow; `refundStaleOrder` after `maxPendingAge` does the same. A lost order cannot freeze accounting. * [ ] `settleIssuerOrder` reverts when the average fill is further than `maxFillDeviationBps` from the oracle mid. A bad fill cannot be booked. * [ ] `sweepDividends` with only longs open leaves NAV unchanged after `applyDividend`. The pool keeps exactly the credit it owes. * [ ] `sweepDividends` and `syncInventory` revert while orders are in flight. `balanceOf` is only read when the counters and the balance can be reconciled. ## Pricing and session * [ ] `getPrice` reverts on a stale print, on `conf × 10 000 > mid × maxConfBps`, and on a jump above `maxDeviationBps`. No caller ever sees a fallback price. * [ ] `depositPrice ≤ mid ≤ redeemPrice` on a live print. Deposits are valued at bid, redemptions at ask. * [ ] A session older than `sessionMaxAge` reads as `Closed`. A dead keeper cannot leave the exchange open. * [ ] While `Closed` and stale, a market-hours asset returns its last accepted price with `bid == ask == mid` and `session == Closed`, and reverts once the mark is older than `maxMarkAge`. The mark is bounded. * [ ] A live print while `Closed` is preferred over the mark, and reading the mark never refreshes `lastAccepted`. Otherwise the mark would renew itself every refresh. * [ ] At the mark, USDC deposits and redemptions stay queued, stock legs and issuer orders revert, opens, closes, liquidations and triggers revert. Nothing moves value at a stale price. * [ ] A queued USDC request executes at the first live print after the open. The gap belongs to the pool, not to whoever saw it coming. ## Positions and open interest * [ ] `reservedStock ≤ stockBalance` after every position change. Every long is backed by inventory the pool holds. * [ ] `shortOiUsd ≤ usdcBalance × shortCapBps / BPS` after every position change. Shorts are paid from USDC the pool has. * [ ] Synthetic pools cap both sides at `shortCapBps` of USDC. No token, so no inventory to lend. * [ ] Opens revert outside the regular session; closes and liquidations in extended hours pay `offHoursFeeMult` and are tested against `offHoursMaintenanceMult`. Off-hours prices are thinner. * [ ] A position reported liquidatable by `getPosition` is liquidatable by `liquidate`, and one that is not reverts `NotLiquidatable`. The keeper and the contract agree. * [ ] Liquidation shortfall beyond insurance cover is added to `badDebtUsd` and emitted. Bad debt is visible. * [ ] Protocol and insurance cuts are taken from the taker fee and the borrow + funding leg only; the pool receives the remainder; with `protocolFeeBps > 0` and no treasury, settlement reverts `TreasuryUnset`. Revenue never comes from collateral. * [ ] After `applyDividend(perShare)`, a long's `dividendAdj` rises by `perShare × tokens` and a short's falls by the same. The ex-date gap is compensated symmetrically. ## Parent and child * [ ] `IndexVault.totalAssets() == Σ parentLpBalance(child) × child.sharePrice() + free USDC`. The parent values its own claim, never child TVL. * [ ] The parent pulls at most a child's `idleUsdc()`. The reserve floor and queued redemptions come first. * [ ] A paused child is skipped when routing, and deposits and redemptions routed to other children still execute. One paused child cannot stop the parent. * [ ] `shift` reverts before `minRebalanceInterval` and above `maxShiftBps` of NAV. Drift correction is bounded. ## Keeper envelope * [ ] `placeIssuerOrder` reverts above `maxOrderUsd`, above `maxDeployRatioBps`, below the reserve floor and above free inventory. The keeper cannot over-deploy. * [ ] `executeRequests(n)` with one failing item still executes the others. A batch never reverts as a whole. * [ ] No `KEEPER`-gated function changes config, weights, wiring or an implementation. The keeper key is not an admin. ## Insurance * [ ] `cover` pays at most `min(amount, maxCoverPerTx, maxCoverPerDay − coveredToday, balance)` and is callable only by `POSITION_MANAGER`. Caps hold, and nobody else can drain it. * [ ] With both caps at zero, `cover` pays nothing. An unconfigured vault is off. * [ ] Only `ADMIN` can `withdraw`. The vault has no LP shares to front-run. ## Router and triggers * [ ] Every `…For(account)` payout goes to `account`; a subaccount never receives USDC, shares or LP tokens. A stolen session key cannot exfiltrate funds. * [ ] `execute` reverts on an expired grant, an exhausted `maxActions`, a notional above `maxNotionalUsd`, a replayed nonce, a passed deadline, a wrong signer, a fee above `relayFeeUsdc` and an unknown pool. Damage from a stolen key is bounded. * [ ] A grant signature cannot be replayed or forged for another subaccount; a zero-budget grant revokes. Revocation costs one signature. * [ ] `…For` entry points revert for callers without `ROUTER`. Only the router and the trigger book act for accounts. * [ ] The plain `msg.sender` path behaves the same with and without a router deployed. The escape hatch stays open. * [ ] A trigger fires only when a long's bid or a short's ask crosses it, executes as a decrease paid to the account, and never fires on a position opened after it was set. Triggers close at the price a close would fill at, and only the position they were set on. * [ ] Before `flaggedAt + priorityWindow`, only `KEEPER` can execute a trigger. Public execution is a fallback, not a race. ## Access and upgrades * [ ] Every external entry point and settlement callback is `nonReentrant`. Ordering alone is not relied on. * [ ] `GUARDIAN` can pause and cannot unpause. Pausing is a one-way emergency action. * [ ] Implementations cannot be initialised; proxies cannot be re-initialised. `_disableInitializers` and `initializer` hold. * [ ] Upgrading a beacon or a UUPS proxy from any address but the timelock reverts. `ADMIN` is the timelock. * [ ] After bootstrap, the broadcaster no longer holds `ADMIN` (unless it is the declared `devAdmin` of a local fork). No deployer backdoor. * [ ] `skim` reverts for USDC, USD+, the shares and the LP token. Rescue can never touch accounting. ## Keeper and backend (off-chain) * [ ] A replayed chain event or a retried activity never produces a second issuer order: `client_order_id` is the pool's `bytes32` id and `dinari_orders.order_id` is the primary key. Idempotency is on-chain data, not randomness. * [ ] A replayed fulfillment never double-counts inventory: `dinari_fulfillments.dinari_fulfillment_id` is the primary key. * [ ] A relayed action is idempotent on its EIP-712 digest (`relay_actions`). Resubmitting the same signature does not double-charge. * [ ] Rewinding the `ingestion` bookmark and replaying a block range starts no duplicate reaction. Workflow ids are stable per target. * [ ] While the session is `Closed`, the keeper pushes no stock price on-chain, and a print wider than `maxConfBps` is never pushed. The mark stays at the close. * [ ] Every keeper action leaves a `job_runs` row. Nothing runs unrecorded. --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://docs.jaawle.xyz/security/invariants.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.