Skip to content

audit: engine critical bundle (closes C-5/6/7/8/9) #89

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
dcccrypto wants to merge 9 commits into from
Closed

audit: engine critical bundle (closes C-5/6/7/8/9) #89

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
1a949bf
Document price movement bound invariant
aeyakovenko Apr 25, 2026
5940285
Rewrite README around three invariants
aeyakovenko Apr 25, 2026
a559c76
Support sparse keeper stress sweeps
aeyakovenko Apr 27, 2026
a911643
fix(audit): port resolve_market_not_atomic pre-snapshots + zero-OI K-…
dcccrypto May 9, 2026
f460a2a
fix(audit): port empty-market gate on withdraw_live_insurance_not_ato…
dcccrypto May 9, 2026
099ad75
fix(audit): port loss-safe fee anchor + ensure_fee_draw_does_not_prec…
dcccrypto May 9, 2026
9b51dd0
fix(audit): port account_has_unsettled_live_effects post-touch guard …
dcccrypto May 9, 2026
ba3f41a
fix(audit): port per-account side-mode gate (ENG-PORT-4, CRITICAL-8)
dcccrypto May 9, 2026
38b551e
test(audit): update enforce_side_mode_oi_gate callsites for new 6-arg…
dcccrypto May 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
129 changes: 100 additions & 29 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,33 @@

**EDUCATIONAL RESEARCH PROJECT — NOT PRODUCTION READY. NOT AUDITED. Do NOT use with real funds.**

A predictable alternative to ADL queues.
A predictable perpetual-futures risk engine built around backed exits, lazy
overhang clearing, and bounded cranks.

If you want the `xy = k` of perpetual futures risk engines -- something you can reason about, audit, and run without human intervention -- the cleanest move is simple: stop treating profit like money. Treat it like what it really is in a stressed exchange: a junior claim on a shared balance sheet.

> No user can ever withdraw more value than actually exists on the exchange balance sheet.

## Two Problems, Two Mechanisms
## Three Invariants

A perp exchange has two fairness problems:
A stressed perp exchange has three jobs:

1. **Exit fairness:** when the vault is stressed, who gets paid and how much?
2. **Overhang clearing:** when positions go bankrupt, how does the opposing side absorb the residual without deadlocking the market?
1. **Backed exits:** when the vault is stressed, nobody can extract more value than the balance sheet can pay.
2. **Fair overhang clearing:** when positions go bankrupt, the residual is absorbed pro rata instead of by a discretionary ADL queue.
3. **Bounded cranks:** when the oracle moves, the live book is repriced only inside the configured one-step risk budget.

Percolator solves them with two independent mechanisms that compose cleanly:
Percolator composes three mechanisms:

- **H** (the haircut ratio) keeps all exits fair.
- **A/K** (the lazy side indices) keeps all residual overhang clearing fair, and guarantees markets always return to healthy.
- **H** (the haircut ratio) makes positive PnL a junior claim on residual value.
- **A/K/F** (lazy side indices) settles mark moves, funding, and ADL overhang without selecting individual losers.
- **The price/funding envelope** bounds every exposed accrual step before K/F/price/slot state can mutate.

---

## H: Fair Exits
## H: Backed Exits

Capital is senior. Profit is junior. A single global ratio determines how much profit is real.
Capital is senior. Profit is junior. A single global ratio determines how much
released positive PnL is actually backed.

```
Residual = max(0, V - C_tot - I)
Expand All @@ -34,44 +38,62 @@ Residual = max(0, V - C_tot - I)
PNL_matured_pos_tot
```

If fully backed, `h = 1`. If stressed, `h < 1`. Every profitable account sees the same fraction of its *released* profit:
If fully backed, `h = 1`. If stressed, `h < 1`. Every profitable account sees
the same fraction of its *released* positive PnL:

```
ReleasedPos_i = max(PNL_i, 0) - R_i
effective_pnl_i = floor(ReleasedPos_i * h)
```
Comment on lines 44 to 47

@coderabbitai coderabbitai Bot May 9, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Add fence languages to satisfy markdown linting

Line 44, Line 80, and Line 116 use unlabeled fenced blocks. Add a language (e.g., text) to avoid MD040 lint failures in docs checks.

Proposed doc-lint fix 
-```
+```text
 ReleasedPos_i   = max(PNL_i, 0) - R_i
 effective_pnl_i = floor(ReleasedPos_i * h)

```diff
-```
+```text
 effective_pos(i) = floor(basis_i * A / a_basis_i)
 pnl_delta(i)     =
     floor(|basis_i| * ((K - k_snap_i) * FUNDING_DEN + (F - f_snap_i))
           / (a_basis_i * POS_SCALE * FUNDING_DEN))


```diff
-```
+```text
 abs(P_new - P_last) * 10_000
     <= max_price_move_bps_per_slot * dt * P_last

</details>


Also applies to: 80-85, 116-119

<details>
<summary>🧰 Tools</summary>

<details>
<summary>🪛 markdownlint-cli2 (0.22.1)</summary>

[warning] 44-44: Fenced code blocks should have a language specified

(MD040, fenced-code-language)

</details>

</details>

<details>
<summary>🤖 Prompt for AI Agents</summary>

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In @README.md around lines 44 - 47, Markdown fenced code blocks are unlabeled
and cause MD040 lint failures; update the three unlabeled fences containing the
formulas for ReleasedPos_i/effective_pnl_i, effective_pos(i)/pnl_delta(i), and
the price-move inequality (P_new, P_last, max_price_move_bps_per_slot) to
include a language label (e.g., add "text" after the opening ). Edit the blocks that include the symbols ReleasedPos_i, effective_pnl_i, effective_pos(i), pnl_delta(i), P_new, P_last, and max_price_move_bps_per_slot to start with text so the linter accepts them.


</details>

<!-- fingerprinting:phantom:poseidon:hawk -->

<!-- d98c2f50 -->

<!-- This is an auto-generated comment by CodeRabbit -->


Fresh profit sits in a per-account reserve `R_i` and converts to released (matured) profit through a warmup period. Only matured profit enters the haircut denominator (`PNL_matured_pos_tot`) and the per-account effective PnL. 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.
Fresh profit sits in a per-account reserve `R_i` and converts to released
(matured) profit through admission and warmup. Only admitted matured profit
enters the haircut denominator (`PNL_matured_pos_tot`) and per-account effective
PnL.

This is the core anti-oracle-manipulation defense. An attacker who spikes a
price sees live gain locked in reserve, excluded from both the ratio and their
withdrawable amount, until the instruction policy admits it. Public wrappers
using untrusted live oracle or execution-price PnL must use nonzero admission
warmup; stress-threshold gating is not a substitute.

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.

When the system is stressed, `h` falls and less converts. When losses settle or buffers recover, `h` rises. Self-healing.
When the system is stressed, `h` falls and less profit converts. When losses
settle or buffers recover, `h` rises. Self-healing.

Flat accounts are always protected — `h` only gates profit extraction, never touches deposited capital.

---

## A/K: Fair Overhang Clearing
## A/K/F: Fair Overhang Clearing

When a leveraged account goes bankrupt, two things need to 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:
Traditional ADL queues pick specific counterparties and force-close them.
Percolator replaces the queue with lazy side indices:

- **A** scales everyone's effective position equally.
- **K** accumulates all PnL events (mark, funding, deficit socialization) into one index.
- **K** accumulates mark and ADL overhang effects.
- **F** accumulates funding effects.

```
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))
pnl_delta(i) =
floor(|basis_i| * ((K - k_snap_i) * FUNDING_DEN + (F - f_snap_i))
/ (a_basis_i * POS_SCALE * FUNDING_DEN))
```

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.
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. Funding moves through `F` the same way:
accounts settle against their snapshots when touched.

No account is singled out. Settlement is O(1) per account and order-independent.

### Markets Always Return to Healthy
### Markets Return to Healthy

A/K guarantees forward progress through a deterministic cycle:
A/K/F guarantees forward progress through a deterministic cycle:

**DrainOnly** — when `A` drops below a precision threshold, no new OI can be added. Positions can only close.

Expand All @@ -83,22 +105,71 @@ No admin intervention. No governance vote. The state machine always makes progre

---

## Price/Funding Envelope

The third invariant is a system bound: an exposed market cannot be cranked
through an arbitrary oracle or funding jump in one step.

For any crank that advances the engine price while open interest exists, the
allowed price move is capped by elapsed slots:

```
abs(P_new - P_last) * 10_000
<= max_price_move_bps_per_slot * dt * P_last
```

Equivalently, the normalized move is bounded by
`max_price_move_bps_per_slot * dt / 10_000`.

At a high level, the maximum price movement between exposed cranks is bounded by
the system's risk budget. If the market is configured around `L` times leverage,
the safe one-step move is roughly on the order of `1 / L`, with room reserved
for funding, liquidation fees, integer rounding, and fee floors/caps.

This turns "crank often enough" into a hard solvency boundary rather than an
operator preference. A stale or fast-moving oracle target must be fed into the
engine as a capped staircase of effective prices. Same-slot exposed cranks use
the previous price; they cannot mark live OI through a zero-time jump.

Active price or funding accrual also has a maximum elapsed-slot window; beyond
that, ordinary live catch-up fails closed and the wrapper must use recovery or
resolution.

Initialization proves a per-risk-notional envelope for the worst allowed
price/funding step plus liquidation fees. At runtime, before any K/F/price/slot
mutation, the engine checks that the next effective step stays inside that
envelope. If it does not fit, the crank fails closed instead of moving the
market into an unbudgeted state.

---

## How They Compose

| | H | A/K |
|---|---|---|
| **Solves** | Exit fairness | Overhang clearing |
| **Math** | Pro-rata profit scaling | Pro-rata position/deficit scaling |
| **Triggered by** | Withdrawal or conversion | Bankrupt liquidation |
| **Recovery** | Automatic as Residual improves | Deterministic three-phase reset |
| | H | A/K/F | Price/funding envelope |
|---|---|---|---|
| **Solves** | Backed exits | Bankrupt overhang clearing | Bounded live repricing |
| **Math** | Pro-rata profit scaling | Pro-rata position, mark, funding, and deficit scaling | Exact per-risk-notional loss budget |
| **Triggered by** | Withdrawal, conversion, settlement | Mark, funding, liquidation, reset | Live accrual/crank |
| **Failure mode** | Less profit is released | Side drains and resets | Crank fails closed or wrapper stair-steps |

Together:
- 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 only for the currently stored realized claim set, not for the economically "true" claim set you would get after globally cranking everyone.
- Risk-increasing trades cannot count their own favorable execution slippage as margin.
- Markets recover through deterministic side resets.
- Exposed cranks are bounded to the configured price/funding budget.
- Raw oracle targets are wrapper-owned; the engine only sees capped effective prices.

A/K/F fairness is exact for open-position economics. H fairness is exact for the
currently stored realized claim set, not for the economically "true" claim set
you would get after globally touching every account.

The engine is not the whole public protocol by itself. A compliant wrapper must
enforce authorization, source and clamp oracle/funding inputs, use nonzero live
PnL admission for untrusted public flows, sync recurring fees when enabled, and
reject extraction-sensitive actions while raw oracle target and effective engine
price diverge.

---

Expand Down
8 changes: 6 additions & 2 deletions kani-list.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,11 @@
"v19_admit_gate_stress_lane_forces_h_max",
"v19_consumption_floor_below_one_bp",
"v19_consumption_monotone_within_generation",
"v19_rr_window_zero_no_cursor_advance"
"v19_generation_advances_at_most_once_per_slot",
"v19_greedy_phase2_model_respects_touch_budget_and_bounds",
"v19_pending_stress_reset_requires_later_wrap",
"v19_rr_touch_zero_no_cursor_advance",
"v19_same_slot_stress_wrap_defers_generation_reset"
],
"tests/proofs_arithmetic.rs": [
"proof_ceil_div_positive_checked",
Expand Down Expand Up @@ -331,7 +335,7 @@
"contract-harnesses": {},
"contracts": [],
"totals": {
"standard-harnesses": 305,
"standard-harnesses": 309,
"contract-harnesses": 0,
"functions-under-contract": 0
}
Expand Down
33 changes: 27 additions & 6 deletions scripts/proof-strength-audit-results.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
# Kani Proof Strength Audit Results

Generated: 2026-04-24
Generated: 2026-04-27

Source prompt: `scripts/audit-proof-strength.md`.

Execution note: `scripts/audit proof strength` is not an executable in this checkout. This audit applies the prompt directly to the current `tests/proofs_*.rs` harnesses and uses `cargo kani list --format json` for the harness inventory.

Kani version: `0.66.0`. Kani-listed standard harnesses: `305`. Parsed proof harnesses: `305`.
Kani version: `0.66.0`. Kani-listed standard harnesses: `309`. Parsed proof harnesses: `309`.

This is a proof-strength audit, not the overnight full CBMC verification run. It classifies harness shape, symbolic breadth, non-vacuity risk, and inductive strength.

Expand All @@ -15,7 +15,7 @@ This is a proof-strength audit, not the overnight full CBMC verification run. It
| Classification | Count | Audit meaning |
|---|---:|---|
| **INDUCTIVE** | 0 | Fully symbolic initial state plus assumed decomposed invariant and loop-free modular preservation proof. |
| **STRONG** | 170 | Symbolic proof harness with meaningful assertions and no observed vacuity risk, but not inductive. |
| **STRONG** | 174 | Symbolic proof harness with meaningful assertions and no observed vacuity risk, but not inductive. |
| **WEAK** | 0 | Symbolic harness with a proof-strength issue that should be tightened. |
| **UNIT TEST** | 135 | Concrete or deterministic scenario harness with no `kani::any()` input. |
| **VACUOUS** | 0 | Confirmed contradictory assumptions or unreachable assertions. |
Expand All @@ -29,6 +29,7 @@ This is a proof-strength audit, not the overnight full CBMC verification run. It
- No trivially false `kani::assume(false)` or `assert!(true)` proof patterns were found.
- No harness is INDUCTIVE under the prompt definition. The suite still uses constructed engine states rather than a fully symbolic `RiskEngine` with decomposed invariant assumptions.
- Concrete regression harnesses are retained as UNIT TEST by the audit rubric. They are useful scenario coverage, but they are not counted as symbolic proofs.
- The new sparse-sweep/stress-reset harnesses are not weak implementation snapshots: they check spec-level properties for zero touch limits, greedy touch-budget bounds, no same-slot stress clearing, pending reset clearing only on a later eligible wrap, and at-most-once-per-slot generation advancement.

## Strengthened Harnesses

Expand All @@ -52,12 +53,32 @@ cargo kani --tests --exact --harness proof_audit3_compute_trade_pnl_no_panic_at_

All four completed successfully.

The new/changed sparse-sweep and stress-reset harnesses were also run one by one:

```text
cargo kani --tests --exact --harness v19_rr_touch_zero_no_cursor_advance --output-format terse
cargo kani --tests --exact --harness v19_greedy_phase2_model_respects_touch_budget_and_bounds --output-format terse
cargo kani --tests --exact --harness v19_same_slot_stress_wrap_defers_generation_reset --output-format terse
cargo kani --tests --exact --harness v19_pending_stress_reset_requires_later_wrap --output-format terse
cargo kani --tests --exact --harness v19_generation_advances_at_most_once_per_slot --output-format terse
```

All five completed successfully. Reported verification times:

| Harness | Time |
|---|---:|
| `v19_rr_touch_zero_no_cursor_advance` | 3.0102103s |
| `v19_greedy_phase2_model_respects_touch_budget_and_bounds` | 0.050476182s |
| `v19_same_slot_stress_wrap_defers_generation_reset` | 2.8122225s |
| `v19_pending_stress_reset_requires_later_wrap` | 6.8237686s |
| `v19_generation_advances_at_most_once_per_slot` | 5.687566s |

## Validation Commands

The audit update and strengthened harnesses were validated with:

```text
cargo fmt -- --check
cargo fmt --all -- --check
git diff --check
cargo test
cargo test --features small
Expand All @@ -83,7 +104,7 @@ All commands completed successfully. The fuzz profile ran 10 tests with 1 config

| File | Total | STRONG | WEAK | UNIT TEST |
|---|---:|---:|---:|---:|
| `tests/proofs_admission.rs` | 34 | 27 | 0 | 7 |
| `tests/proofs_admission.rs` | 38 | 31 | 0 | 7 |
| `tests/proofs_arithmetic.rs` | 19 | 19 | 0 | 0 |
| `tests/proofs_audit.rs` | 33 | 11 | 0 | 22 |
| `tests/proofs_checklist.rs` | 16 | 12 | 0 | 4 |
Expand All @@ -96,4 +117,4 @@ All commands completed successfully. The fuzz profile ran 10 tests with 1 config

## Remaining Audit Boundary

This audit verifies harness strength and checks the strengthened harnesses with Kani. It does not replace the full overnight `scripts/run_kani_full_audit.sh` run across all 305 harnesses.
This audit verifies harness strength and checks the strengthened harnesses with Kani. It does not replace the full overnight `scripts/run_kani_full_audit.sh` run across all 309 harnesses.
Loading