[REAL DoS] Reserve source capacity for admitted positions

[aeyakovenko]

What changed

Reserve sparse source-domain capacity before admitting each new position. Capacity now accounts for both occupied historical claims and every active leg whose favorable K/F source domain has not been materialized yet.

The focused engine regression covers three boundaries: a full table rejects a missing favorable domain without mutation, a full table permits a domain already represented, and an active leg reserves its still-empty favorable domain.

Root cause and impact

attach_leg_at_slot checked the 16-leg limit but did not reserve one of the portfolio's 32 sparse source slots for the leg's first favorable settlement. A user could publicly accumulate claims in all 32 domains, retain an old claim-bearing exposure, and open a new asset whose favorable domain was absent. After an honest mark move, settlement needed a 33rd source entry and returned LockActive.

The paired public LiteSVM red test shows that auto-crank, source-claim conversion, closing either position through TradeNoCpi, and RebalanceReduce all fail with rollback. The live portfolio has no bounded owner or permissionless keeper continuation; only privileged asset shutdown followed by forfeiture can rescue it.

This is also a concrete gap in the conditional no-DoS proof claim: the selector's refresh witness exists at the kernel level, but the real dispatch body fails at source insertion. The capacity invariant closes that monolithic gate-reachability case for newly admitted positions.

Verification

• cargo test --all-targets -- --test-threads=1
• cargo test --features fuzz --all-targets -- --test-threads=1
• cargo kani -Z function-contracts --features fuzz,contracts --harness composition_attach_body_frame_division_stubbed --output-format terse
  • 6,137 checks, 159 unreachable, 1/1 cover, zero failures
• Paired wrapper test is RED on engine 143e68c4917ed0400a27b952f036a5677047cd84 at the no-continuation assertion.
• Paired wrapper branch passes 6 unit tests and all 566 LiteSVM/CU tests.
• Max-shape wrapper measurements after the O(1) compact-tail fast path:
  • 14-leg BatchTradeNoCpi: 1,308,173 CU
  • 14-leg BatchTradeCpi: 1,339,517 CU
  • 14-leg BatchTradeCpi with four maximum tail accounts: 1,343,687 CU

[aeyakovenko]

Independent clean-room LiteSVM confirmation against the exact binaries, extended to remove the owner-footgun ambiguity.

I changed only a temporary harness at wrapper head cf69b40e095bf4ee6b750af56c68f1c3c05b9c0a. The victim LP fills all 32 source-domain entries and retains the old exposure through public instructions, then authorizes the standard matcher. A separate unaffiliated attacker is the only transaction signer on the final TradeCpi; the full-table victim is the passive LP.

RED, exact Meta pin da64be639168b496833dd4c701607a94fcb06b6c / engine 143e68c4917ed0400a27b952f036a5677047cd84:

• attacker-only TradeCpi admits the unsafe victim leg;
• honest AuthMark 100 -> 101 and losing-side crank succeed;
• victim PermissionlessCrank, ConvertReleasedPnl, a new-leg close with a fresh fully funded rescue counterparty, old-leg close, and RebalanceReduce all fail;
• failed continuations leave market and victim account bytes unchanged.

GREEN, exact wrapper cf69b40e095bf4ee6b750af56c68f1c3c05b9c0a / engine c1a058f3f6057838e78a6ada51509af336fd4ed6:

• the attacker-only admission rejects atomically with market, victim, historical counterparty, attacker, and matcher snapshots unchanged;
• the old exposure still closes and the victim withdraws its full 1,000,000-unit principal.

Command used for both binaries:
cargo test --test v16_cu v16_probe_matcher_cannot_admit_an_unsettleable_lp_leg -- --nocapture --test-threads=1

This is a real public-interface DoS: an unaffiliated taker can trap an already-authorized passive LP; it does not require the victim owner to submit the unsafe trade.

[aeyakovenko]

Added a generalized admission-to-continuation theorem in 8b9456e4.

proof_v16_source_capacity_admission_closes_all_favorable_domains invokes the exact production admission decision and proves, for every bounded partition of occupied domains, latent active-leg domains, and the candidate domain, that:

• over-capacity admission fails closed with LockActive;
• every accepted latent favorable source domain can later materialize in any order without exhausting the source table;
• the reserved union cardinality is preserved through materialization and remains within capacity.

All 5 non-vacuity covers are reachable, including latent-domain rejection before the physical table is full and exact-boundary materialization. Mutation checks showed the theorem fails if either the candidate reservation or existing latent reservations are omitted. Removing the production guard makes the existing attach integration regression fail, tying the theorem to the real transition.

Verification:

• cargo test --quiet: pass
• cargo test --features fuzz --quiet: pass
• generalized theorem: pass, 5/5 covers, 0.23s
• sparse-cap rejection theorem: pass, 22.05s
• active-asset uniqueness theorem: pass, 161.50s
• attach body/frame contract: pass, 115.55s

No layout, wrapper-facing API, or spec change.

[aeyakovenko]

Independent Meta LiteSVM follow-up found the max-source conversion path that this PR explicitly leaves separate.

Public red test: aeyakovenko/percolator-meta@1e1a33f

The fixture creates every claim through signed TradeNoCpi, authenticated mark pushes, and permissionless settlement. No account-state injection is used.

Results at the chain's 1,400,000-CU ceiling:

• This PR's exact fixed pin (cf69b40e / engine c1a058f3): 16 domains convert in 1,017,938 CU; 32 domains on a minimum capacity-17 slab consume exactly 1,400,000 CU and fail at the BPF meter.
• Domain-local conversion head (81dfda28 / engine f0e189a1): 16 domains convert in 1,023,549 CU; the same 32-domain minimum slab also consumes exactly 1,400,000 CU and fails.

The failed conversion rolls market and portfolio bytes back. The owner can withdraw the original 1,000,000-unit principal, but cannot withdraw any of the 32 earned, source-backed units, and the remaining positive-claim portfolio cannot close. There is no domain-selective public conversion wire, so the supported state has no bounded live owner path to recover earned value.

This is a separate real public-interface LoF, not a reason to weaken this admission fix. A fix needs either a transaction-bounded domain-local conversion cursor/chunk or a proven full conversion below the ceiling at all supported source shapes, while preserving the caller cap and PR #267/#140's domain-local burn semantics. I left the Meta branch red and opened no Meta PR pending that upstream fix.