# Perp Funding Conservation — Design Doc (M-2)

**Status:** DEFERRED to a dedicated, separately-audited effort (decision 2026-05-30).
**Context:** Combined-surface perp audit finding M-2 on `integration/clean-main`. M-1 was fixed
and landed; M-2 is a product-level fork that should not be committed under time/channel pressure.

---

## 1. The finding (as written)

> Premium funding has no conserving settlement pool. `updateFees` is a pure per-position ledger
> movement with no InsuranceFund/BackstopVault deposit at accrual. Receiver funding credits inflate
> `collateralToReturn` (paid from InsuranceFund at close), while a payer liquidated/ADL'd into bad
> debt has its funding debit socialized → InsuranceFund erodes under sustained one-sided funding +
> payer-side liquidations. Severity: Medium (gradual, market-conditioned; no instant exploit).

## 2. What the code actually does (verified 2026-05-30)

Funding is **already substantially conserved through close settlement** — it is not a "missing pool":

- **Payer debit:** positive `periodFundingFee` reduces `position.collateralAmount`
  (`PositionHandler.updateFees`, `src/perpetual/PositionHandler.sol:620-626`). At close the smaller
  `collateralToReturn` makes `BalanceManagerVault._handleRelease` deposit the locked-minus-returned
  gap **into** the InsuranceFund (`BalanceManagerVault.sol:466-468,634-639` →
  `_depositLockedIntoInsurance` → `InsuranceFund.depositFunding`, which bumps `totalFundingReceived`).
- **Receiver credit:** negative `periodFundingFee` raises `collateralAmount`; at close the surplus is
  paid **from** the InsuranceFund (`_creditProfitFromInsurance`, `BalanceManagerVault.sol:633`).
- **The IF cannot go negative.** `InsuranceFund.withdrawFunding` (`src/perpetual/InsuranceFund.sol:267-299`)
  caps the payout at `insuranceFundBalance`, returns the actual amount, and emits `FundingShortfall`.
  `_creditProfitFromInsurance` credits only what was actually paid and records any shortfall in
  `insuranceProfitDeficit` (never reverts — preserves the "liquidations always succeed" guarantee).
- The IF **already tracks** `totalFundingPaid` and `totalFundingReceived`.

So the real residual risk is **not** unbounded bad debt. It is:

1. **Timing asymmetry** — a receiver that closes *before* its paying counterparty closes is fronted by
   IF capital (the matching payer debit hasn't been deposited yet). Self-limiting: the funding *rate*
   exists precisely to rebalance OI, and `withdrawFunding` caps payouts.
2. **Bankrupt payer** — a payer liquidated/ADL'd into bad debt has the portion of its accrued funding
   debit that exceeded its collateral *socialized* (capped to zero in `updateFees`,
   `PositionHandler.sol:622-623`), so that slice never reaches the IF, while the receiver still claims.

The funding model itself — **OI-imbalance-driven, with the InsuranceFund intentionally the counterparty
for the net imbalance** — is a *deliberate* design choice (see
`docs/PERP_MECHANISM_COMPARISON.md` / memory `project_perp_mechanism_comparison.md`, which flags it as
an intentional outlier vs Hyperliquid/Extended/Pacifica/Lighter).

## 3. Two real targets (they are NOT the same)

### Path A — Rate-level zero-sum funding ("by construction")
Make funding a pure long↔short transfer so `sum(debits) == sum(credits)` at **every accrual step**,
removing the IF as the funding counterparty.

- `MarketHandler.accrueFunding` maintains **two** cumulative indices, `cumLongIndex` and
  `cumShortIndex`. At each `dt` with premium rate `r` and current `longNotional`/`shortNotional`:
  - paying side accrues `r*dt` per notional;
  - receiving side accrues `r*dt * (payNotional / receiveNotional)` per notional (scaled), so the
    total credited equals the total debited for that step.
- Position keeps one `entryFundingIndex` (its own side's index; resets on side flip — already true).
- `pendingFundingFromIndex` (consumed by QRE/BMV health views) updated to the per-side index.
- **PerpEngine (Monad) parity.**
- **Pros:** genuinely conserving by construction; IF no longer fronts funding; cleanest invariant.
- **Cons:** OVERTURNS the deliberate OI-imbalance model — a **product decision**, not a bug fix.
  Largest change; most funding tests rewritten; needs its own audit. Bankruptcy STILL needs ADL
  realization (a bankrupt payer that can't cover its scaled debit breaks conservation regardless).

### Path B — Segregated funding pool + bankrupt-debit realization (recommended if M-2 is treated as a bug)
Keep the intentional model; make the IF's funding sub-ledger sound and auditable.

- Add a per-market funding accumulator (DataStore or InsuranceFund: `fundingCollected[market]` /
  `fundingPaid[market]`), or reuse the existing global `totalFundingReceived`/`totalFundingPaid` with a
  per-market breakdown.
- Receiver credits are drawn from **collected funding** first; only the genuine timing gap is fronted
  by IF capital (current behavior), but the gap is now explicitly measured per market.
- **Bankrupt payer:** in `PositionHandler.liquidatePosition` / `_decreasePositionInternal` and the ADL
  path, realize the position's accrued-but-unpaid funding debit into the funding pool from seized
  collateral **before** socializing the residual deficit (so a bankrupt payer's funding obligation is
  collected up to its collateral, not silently dropped).
- Add an explicit conservation invariant test: `totalFundingReceived >= totalFundingPaid` (or the
  per-market equivalent) across a sustained one-sided-funding + payer-liquidation scenario.
- **PerpEngine (Monad) parity.**
- **Pros:** preserves the documented design; closes the bankruptcy leak; bounded, auditable.
- **Cons:** under lazy/async settlement it is "conserving over position lifetimes," NOT literally "by
  construction" — a receiver closing before its solvent payer is still fronted by IF capital.

## 4. Why deferred

- The IF is **already bounded** (no negative balance, shortfalls tracked) — M-2 is gradual,
  market-conditioned, testnet-only; no instant exploit. Not an emergency.
- Path A is a **product-level mechanism change** contradicting a documented deliberate design; it must
  not be committed implicitly inside an integration merge.
- Both paths require **their own dedicated audit** (Pashov + Nemesis) and will shift many of the
  current funding/liquidation tests. Committing a broken funding merge to `main` is hard to reverse.

## 5. Recommended next step

Spin a dedicated `feat/funding-conservation` branch. First decide A vs B as a **product** question
(does funding stay OI-imbalance-driven, or become long↔short zero-sum?). Then implement, run the full
mandatory workflow (sizes + tests + fuzz + Pashov + Nemesis until clean), and land separately.

## 6. Code map (entry points for whoever picks this up)

- `src/perpetual/PositionHandler.sol` — `updateFees` (funding accrual `:580-587`, debit/credit
  application `:619-639`); `liquidatePosition` / `_decreasePositionInternal` (bankrupt-debit realization site).
- `src/perpetual/MarketHandler.sol` — `accrueFunding` (premium-index advancement),
  `pendingFundingFromIndex`.
- `src/perpetual/storages/PerpStorage.sol` — per-market funding index storage (add second index for Path A).
- `src/perpetual/BalanceManagerVault.sol` — `_handleRelease` `:609-666`, `_creditProfitFromInsurance`,
  `_depositLockedIntoInsurance`, `_settleCrossAccountDeficit` `:774-811`.
- `src/perpetual/InsuranceFund.sol` — `depositFunding` `:232-249`, `withdrawFunding` `:267-299`,
  `totalFundingPaid` / `totalFundingReceived`.
- `src/monad/PerpEngine.sol` — Monad parity for ALL of the above (funding refs ~129).
- ADL path — realize bankrupt funding debit before socializing.