FORMAL SPECIFICATION
The full mathematical specification of the risk engine that powers Perconaries. Two mechanisms. One invariant. Auditable end to end.
Version 0.4 · Apache-2.0 · Educational research
"No user can ever withdraw more value than actually exists on the exchange balance sheet."
This single property is what the entire spec exists to enforce. Everything below derives from it.
A perp exchange has two distinct fairness problems. Exit fairness — when the vault is stressed, who gets paid and how much. Overhang clearing — when positions go bankrupt, how the opposing side absorbs the residual without deadlock. Percolator solves them with two independent mechanisms that compose cleanly: H for exit fairness, A/K for overhang clearing.
| Mechanism | Solves | Math | Triggered by |
|---|---|---|---|
| H | Exit fairness | Pro-rata profit scaling | Withdrawal or conversion |
| A/K | Overhang clearing | Pro-rata position and deficit scaling | Bankrupt liquidation |
Capital is senior. Profit is junior. A single global ratio determines how much profit is real.
Residual = max(0, V - C_tot - I)
min(Residual, PNL_matured_pos_tot)
H = ──────────────────────────────────
PNL_matured_pos_totIf fully backed, H = 1. If stressed, H < 1. Every profitable account sees the same fraction of its released profit.
ReleasedPos_i = max(PNL_i, 0) - R_i effective_pnl_i = floor(ReleasedPos_i × H)
Fresh profit sits in a per-account reserve R_i and converts to released profit through a warmup period. Only matured profit enters the haircut denominator. This is the core oracle-manipulation defense — an attacker who spikes a price sees their unrealized gain locked in R_i, excluded from both the ratio and their withdrawable amount, until the warmup window passes.
No rankings. No queue priority. No first-come advantage. The floor rounding is conservative — the sum of all effective PnL never exceeds what exists in the vault. Flat accounts are always protected; H only gates profit extraction.
When a leveraged account goes bankrupt, two things must happen — remove the position quantity from open interest, and distribute any uncovered deficit across the opposing side. Traditional ADL queues pick specific counterparties and force-close them. Percolator replaces the queue with two global coefficients per side.
A — scales every account's effective position equally.K — accumulates all PnL events (mark, funding, deficit socialization) into one index.effective_pos(i) = floor(basis_i × A / a_basis_i)
pnl_delta(i) = floor(|basis_i| × (K - k_snap_i)
/ (a_basis_i × POS_SCALE))When a liquidation reduces OI, A decreases — every account on that side shrinks by the same ratio. When a deficit is socialized, K shifts — every account absorbs the same per-unit loss. No account is ever singled out. Settlement is O(1) per account and order-independent.
A/K guarantees forward progress through a deterministic state machine. No admin intervention. No governance vote. The state machine always makes progress.
When A drops below a precision threshold, no new OI can be added. Positions can only close.
When OI reaches zero, the engine snapshots K, increments the epoch, and resets A back to 1. Remaining accounts settle their residual PnL exactly once when next touched.
Once all stale accounts have settled and OI is confirmed zero, the side reopens for trading with full precision.
The two mechanisms are independent. H acts at withdrawal time on the profit-claim set. A/K acts at liquidation time on open positions. They share no state, but together they satisfy the full invariant: no user can withdraw more than exists, no user is singled out for forced closure, markets always recover, flat accounts keep their deposits.
A/K fairness is exact for open-position economics. H fairness is exact for the currently stored realized claim set.