Wave 11d: bankrupt-close setter integration (Phase 1)

[dcccrypto]

Summary

Wave 11d — wires the Wave 11a-ii-A bankrupt-close setters into the production hot paths that surface a Live-market deficit. Mirrors toly engine v12.20.6 patterns at toly:4980-4982, 7103-7112, 7138-7144, 7210, 7214, 7869-7870, 8364, 8402.

• settle_losses / resolve_flat_negative refactored to _with_context(Option<&mut InstructionContext>) variants. The Some(ctx) path threads the bankruptcy h_max lock through trigger_bankruptcy_hmax_lock(ctx); the None path uses _without_context.
• enqueue_adl Step 2: arms the lock when d > 0, BEFORE use_insurance_buffer.
• ctx threaded into the 4 ctx-having call sites: touch_account_live_local (settle + resolve), execute_trade_not_atomic post-trade pair settle, liquidate_at_oracle_internal ExactPartial step 9, liquidate_at_oracle_internal FullClose step.

Deferred to Wave 11e candidate

The toly:5057 wiring of book_or_start_active_close_residual_to_side into enqueue_adl Step 7 (d_social branch when uncertified_potential == 0) requires replacing fork's K-adjust algorithm with toly's v12.20.6 certified/potential/B-residual algorithm. That replacement breaks the t11_54_worked_example_regression Kani proof which pins fork's K-adjust post-condition (adl_coeff_long != 0 after ADL with d > 0).

Per Wave 11d STOP CONDITION ("If integration breaks existing Kani proof → STOP, redesign, surface") the algorithm migration is surfaced as a follow-up wave. The bankrupt-close setter remains wired into the recovery dispatcher (Wave 11a-ii-C); Phase 1 of Wave 11d adds the lock setter into every Live deficit settle path that mirrors toly.

Verification

• cargo build --release: clean
• cargo test --features test --release: 283 passed, 0 failed
• scripts/verify-engine-preservation.sh: silent
• scripts/verify-engine-deferred-absent.sh: silent
• Kani harness count: 356 → 360 (+4)

Schema impact

None. No new RiskEngine / Account / InstructionContext fields. Pure behavior wiring on top of Wave 11a-i (B-tracking schema) + Wave 11a-ii-A (setter helpers) + Wave 11a-ii-C (recovery dispatcher). No NFT or wrapper follow-up required.

KEEP_LIST

KL-FORK-ENGINE-BANKRUPT-CLOSE-1: state-machine setters now have production callers in every Live deficit path (settle / enqueue_adl Step 2). Residual booking integration (Step 7 d_social branch) deferred to Wave 11e per STOP CONDITION. KL stays partially revoked one notch closer to full closure.

Test plan

• Local cargo build --release clean
• cargo test --features test --release 283 / 283 pass
• verify-engine-* scripts silent
• 4 new Kani harnesses compile
• CI Kani run (will verify 360 harnesses)

🤖 Generated with Claude Code

Summary by CodeRabbit

• Tests

  • Added formal verification proofs for bankruptcy lock arming during ADL and loss settlement scenarios, ensuring robust handling during account liquidation.

• Refactor

  • Enhanced settlement processes with context-aware bankruptcy lock mechanisms, improving consistency across deficit coverage and loss resolution flows.

[coderabbitai]

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 5f84ef13-d47b-407d-9b5a-9e26508f739c

📥 Commits

Reviewing files that changed from the base of the PR and between aea9a58 and d0fae02.

📒 Files selected for processing (2)

• src/percolator.rs
• tests/proofs_invariants.rs

---

📝 Walkthrough

Walkthrough

This PR extends bankruptcy h-max-lock arming to loss settlement and flat-negative resolution by introducing context-aware variants of settle_losses and resolve_flat_negative, threading an InstructionContext through entry points (ADL) and wiring sites (live-touch, liquidation, trade settlement) to conditionally arm the lock for Live accounts that exhaust capital while negative-PnL.

Changes

Bankruptcy H-Max Lock Arming and Context Threading

Layer / File(s)	Summary
Core Settlement Helpers src/percolator.rs	Introduced settle_losses_with_context(idx, ctx) and resolve_flat_negative_with_context(idx, ctx) that conditionally arm trigger_bankruptcy_hmax_lock(ctx) for Live accounts exhausting capital with negative-PnL or resolving flat-negative. Original non-context variants remain as thin wrappers.
ADL Deficit Entry Point src/percolator.rs	enqueue_adl now calls trigger_bankruptcy_hmax_lock(ctx) when deficit parameter d > 0 before insurance-first coverage.
Live Touch Pipeline Wiring src/percolator.rs	touch_account_live_local updated to pass Some(ctx) into both context-aware settlement helpers, enabling lock arming during the full live-touch pipeline.
Settlement Call Sites src/percolator.rs	execute_trade_not_atomic and both liquidation paths in liquidate_at_oracle_internal (partial and full close) updated to call settle_losses_with_context(..., Some(&mut ctx)), enabling bankruptcy h-max-lock arming during trade and liquidation loss realization.
Verification Proofs tests/proofs_invariants.rs	Added four Wave 11d Kani proofs: proof_enqueue_adl_arms_bankruptcy_lock_when_d_positive, proof_enqueue_adl_leaves_bankruptcy_lock_when_d_zero, proof_settle_losses_with_context_arms_lock_when_capital_exhausted, and proof_resolve_flat_negative_with_context_arms_lock_before_absorb verify lock arming behavior and context stamping across ADL and settlement paths.

Possibly related PRs

• dcccrypto/percolator#88: Foundational v12.19 sync introducing InstructionContext threading and live-settlement path refactors that this PR builds upon.
• dcccrypto/percolator#68: Earlier settlement path modifications to settle_losses and resolve_flat_negative that this PR extends with context-aware variants.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

Poem

🐰 A rabbit bounds through bankrupt gates,
With locks that arm at loss-sealed fates,
Context threads through settlement flows,
Where capital exhausts, the bright guard glows!
Four proofs stand sentinel, true and bright—
The chaos calmed, the ledger right. ✨

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/eng-bankrupt-close-integration-wave11d

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}