LP capital drains to zero: settlement destroys accumulated positive PnL (both sites) — fixed in d448e1c9

[dcccrypto]

Summary

Two sites in the K/F settlement path destroy an account's accumulated positive PnL far beyond what the arriving loss justifies. On a market whose liquidity provider is settled on a keeper cadence, this converts price volatility into permanent capital loss: the LP's capital becomes monotonically non-increasing and drains to zero regardless of price direction.

Fixed in d448e1c. This issue records the full investigation, because the conclusion reversed twice before landing and the reasoning matters.

The defect

Site 1 — apply_haircut_bounded_close_loss_to_pnl

if remaining_loss != 0 { junior_face_burned = old_positive_face; }

Any under-supported loss, however small, burned the account's entire positive face — and the loss was still charged to capital. A double charge.

Site 2 — apply_signed_kf_delta_to_pnl

junior_face_burned = new_face_support;

A gain arriving at a negative-PnL account was burned in full whenever any of the pre-existing loss stayed uncovered. source_credit_state_realizable_support_for_face returns 0 whenever positive_claim_bound_num == 0, and an underwater account has no positive claims by definition — so support was structurally always 0. An account that went underwater could never recover, no matter how far the price moved back in its favour, and no matter how much backing existed.

Evidence it is real (measured, not modelled)

1. Live on the deployed program. 25 minutes, 935 reads, zero errors. Price moved +391 units in the LP's favour; its equity fell $24.23 (should have risen $14.24). Four discrete destruction events:

profit held	loss that arrived	profit destroyed
$13.078319	$0.072860	$13.005459
$8.451720	$0.036430	$8.415290
$10.309645	$0.072860	$10.236785

A control inside the same recording: a genuine 111-unit adverse move with PnL already at 0 was charged $4.043716 — the honest amount, to the atom. The arithmetic is fine; the defect is confined to what happens to profit at a direction change.

2. On-chain ledger identity, 3/3 markets, to the cent. loss-domain fresh_reserved = $100.000000 seed + residual_crystallized_loss.

3. An accidental control. Two LPs, same keeper, same cadence, same hour — one with an exhausted backing pot, one funded. Error vs honest: −$38.47 versus −$0.000005.

4. Site 2, isolated. Drive an account underwater, then move the price $1,242 in its favour across 150 settlements → $0.00 credited. Identical with a $50,000 funded pot. Post-fix the same probe recovers to +$1,207.25.

Why the fix is the correct semantics

A gain that merely nets against an outstanding loss is not a new claim — it is the counterparty's loss being realized against a debt the account already owes — so it requires no source backing. Only the excess above zero becomes a new claim, and that stays gated by realizable support, preserving the realizable-limited thesis.

spec.md v16.9.0 supports this directly. §2.2 says a round-trip that recovers the mark "settles as fresh positive PnL … so the recovered value returns to the account through realization", and that there is "no unrealized-drawdown ratchet and no double-charge". The realization-extent rule burns "the CONSUMED face". Both sites contradicted that.

Verification

• tests/lp_burn_repro.rs — 28/28. Drives the real crank entry point (permissionless_crank_not_atomic / Refresh) with risk parameters read off a live market, emulates SVM rollback around the _not_atomic calls, and asserts honesty against the price the LP's own leg was settled to on every run, so no test can pass vacuously.
• Adversarial battery: nonzero trading fees, 3 traders, mid-run position changes, real liquidation, multi-asset cross-domain, nonzero funding, Resolved/Recovery mode, and the exact site-2 boundary (gain == debt).
• Mutation tested: reverting both fixes fails 16 tests; reverting either alone fails a disjoint set; restoring passes 28/28.
• Engine suites: v16_spec 49, v16_fork_lp_vault 29, backing_double_claim 6, resolved_insolvent 2 — 0 failures.
• Kani: 139-proof value-safety sweep → 138 pass. The single failure (proof_v16_public_backing_fee_charges_only_selected_domain) is pre-existing and fails identically with both fixes reverted. Both new asymmetric-A accrual proofs pass.

Conservation is preserved: unbacked positive PnL stays non-convertible and non-withdrawable while exposure is open, and the vault never exceeds deposits — including when the counterparty is bankrupted.

Corrections made during the investigation

Recording these because two earlier write-ups were wrong in opposite directions:

• An earlier harness "settled" via sync_account_fee_to_slot_not_atomic — a fee routine that never settles a leg, with the slot number passed as the fee rate. Its original finding and its later retraction were both artifacts of it.
• A reported "$0–$242 residual at high volatility" was my own measurement error, not the engine. The per-slot price clamp rejects steps, so the engine never reaches the path endpoint. Measured per settlement, the engine diverges ≤1 atom. The correct reference is the price the LP's leg was actually settled to, derived from k_snap.
• A claim that the LP "cannot cash out" was wrong. Conversion is blocked only while exposure is open, by design. After closing, the LP is paid in full — measured $1,003.00 out on a $1,000 deposit, with an empty backing pot.

What this does NOT fix

1. The wrapper path is unexercised. Every test drives the engine library directly; account plumbing, matcher, CPI and CU limits are untested. This should be closed before any deployment.
2. A structural backing issue remains. An account's gains draw support from the opposite-side domain, but the LP vault is bound to a single domain at creation. An LP that ends up on the wrong side has a gain domain that no instruction can fund. The engine fix stops the destruction of profit; it does not create the backing.
3. Still unexercised: ADL/socialization, B-settlement (SettleB, b_stale), insurance-backed liens, epoch resets, overflow magnitudes.

[0x-SquidSol]

Independent verification against upstream aeyakovenko/percolator@master

Both defects reproduce on upstream master (143e68c4), which does not contain d448e1c9. This fork branched at 3969c31a and is 724 commits behind upstream, so the fix was developed on a stale base — worth confirming separately. Both lines are present verbatim: site 1 at src/v16.rs:10199, site 2 at src/v16.rs:10309. The blob served by the GitHub contents API at 143e68c4 hashes to d8cd983b, byte-identical to the tree under test.

Summary: both defects are real, and d448e1c9 as merged introduces a value-creation bug. A revised form of site 2 is proposed below, validated against 188 tests including this repo's own 28.

1. Both defects confirmed

Reproduced with no source modification, public API only (accrue_asset_to_not_atomic + full_account_refresh_not_atomic, which reaches settle_leg_kf_effects_at_slot_with_asset). Two accounts, fee_bps: 0, funding disabled, all backing fee rates zero, no counterparty backing seeded so realizable support is zero and site 1's override is the only thing that can burn face. Price returns exactly to its starting value (40000 → 41200 → 40000, four cycles). Measuring capital, which does not depend on how one values an unbacked face claim:

                    LP capital          counterparty capital
upstream HEAD       1000.00 -> 995.20   1000.00 -> 1000.00
both lines fixed    1000.00 -> 998.80   1000.00 -> 1000.00

998.80 is correct (one leg's settled loss). On HEAD the LP gives up an additional 3.60 the counterparty never receives.

Mutation control, porting tests/lp_burn_repro.rs onto upstream: HEAD 16 failed / 12 passed (matching the count reported here); both lines changed 28/28; site 1 reverted alone 13 failed; site 2 reverted alone 3 failed. Disjoint and additive, so each site is independently causal. Site 2 isolated: a 1242.553685 favourable move credited 0.000000, PnL −13.151235 → −28.925370.

On the certified proof. proof_v16_live_positive_kf_delta_without_source_rejects (tests/proofs_v16.rs:8181, certified PASS) asserts Ok((0, delta)) and pnl == -loss for a positive delta at a negative-PnL account. That does not legitimise site 2: the proof passes source_domain = None, whereas settlement always passes Some(..) for a gain —

// src/v16.rs:10585-10590
if net > 0 {
    let source_domain = Some(self.insurance_domain_index(asset_index, opposite_side(leg.side))?);
    self.apply_signed_kf_delta_to_pnl(account, net, source_domain)?;
} else {
    self.apply_signed_kf_delta_to_pnl(account, net, None)?;
}

The proof covers a guard settlement never exercises. Site 2's defect fires through the remaining_loss != 0 disjunct, which the proof does not constrain.

2. d448e1c9 creates value where source support is non-zero

Site 2's premise — that support is "structurally always 0" because an underwater account has no positive claims — does not hold. source_credit_state_realizable_support_for_face reads the domain's aggregate positive_claim_bound_num (src/v16.rs:2761), not the account's, so any other account holding claims on that domain makes it non-zero.

When it is non-zero, support_consumed has already reduced remaining_loss; retaining the full gain as face then applies the same event twice. Measured on this fork's main with a clean tree — an account with exhausted capital at −88.80, another account holding claims on the source domain, backing available:

                      gain 22.40 credited    gain 24.00 credited
upstream HEAD (no fix)        22.40                  24.00     correct
d448e1c9 / fork main          44.80                  48.00     2x

The account ends at +4.00 PnL with zero capital after being 88.80 underwater. Note the direction: unfixed upstream is correct here, so this is a regression introduced by the fix, not a pre-existing issue.

Two further consequences of the same line. d448e1c9 sets junior_face_burned = 0 whenever new_face_support <= old_loss, including when support_consumed > 0; the close ledger rejects support_consumed > junior_face_burned outright (src/v16.rs:4306). And in the no-source Live case it changes the branch the certified proof pins — replaying that proof's assertions over concrete values, pristine upstream holds 6/6 while d448e1c9 violates 6/6.

3. Proposed revision to site 2

Site 1's deletion is unchanged from d448e1c9. Site 2 becomes:

if source_support_domain.is_none()
    && decode_market_mode(self.header.mode)? == MarketModeV16::Live
{
    // No source attribution in Live: nothing can be consumed, so the face
    // cannot cure anything. Unchanged (req 15; certified by
    // proof_v16_live_positive_kf_delta_without_source_rejects).
    junior_face_burned = new_face_support;
} else if remaining_loss != 0 {
    // Source-attributed gain not fully covering the outstanding loss. Burn the
    // face actually consumed as support, plus any excess above the debt (that
    // excess would be a NEW positive claim and stays gated). The part that
    // merely nets against the debt is not a new claim and needs no backing.
    junior_face_burned = support_consumed
        .saturating_add(new_face_support.saturating_sub(old_loss))
        .min(new_face_support);
}

Splitting the disjunct preserves the proven no-source branch, burn >= support_consumed always holds so the ledger check cannot trip, and both regimes land on new_pnl = gain - old_loss.

Results, upstream + this revision: 188 passed, 0 failed, comprising this repo's lp_burn_repro 28/28, v16_spec_tests 72, reference_model_conformance 15, backing_double_claim_fuzz 9, rounding_residue_fuzz 9, resolved_insolvent_fuzz 2, v16_fuzzing 1, lib 50, plus the double-count probe and the certified-proof replay. Seed-0 destruction goes to 0.000000, the double-count probe credits exactly the gain, and the certified proof's assertions hold 6/6.

4. Scope and limits

Deliberately excluded as evidence: partially-backed configurations also show equity loss, but it is essentially unchanged by the fix (at a $0.10 seed, 3.500001 before vs 3.499998 after). That is the structural backing asymmetry already listed under "What This Does NOT Fix", not a defect in either site. Separately, the face-burn accounting in the has_source_claims branch is correct — source_credit_lien_amounts_for_effective yields face = effective / credit_rate and the burned face matches that identity at every observed rate, so there is no additional double-charge there.

Not established: Kani could not be run (no native Windows support; proofs_v16.rs executes 0 tests without it), so the proof result above is a concrete-value replay of that harness's assertions, not exhaustive verification — the revision should be run through the real proof sweep before it is relied on. On-chain exposure of any deployed program and the live devnet figures in the original report were also not checked. Finally, site 1's deletion interacts with the dead-leg forfeit path (settle_forfeited_leg_kf_effects), which spec.md §12 governs with "values positive PnL at zero unless source-domain backing is consumed"; that interaction deserves review independently of anything above.