Wave 11e — v12.20.6 enqueue_adl B-residual algorithm - #103
Merged
Conversation
Replaces fork's K-adjust ADL (`delta_K_abs = ceil(D_rem * A_old * POS_SCALE / OI)`
written to `adl_coeff_<opp>`) with toly's v12.20.6 certified/potential/B-residual
routing. K is no longer modified for bankruptcy residual on any path.
Changes
-------
* `enqueue_adl` Step 7: `D_rem` now splits into `d_phantom` (proportional to
`phantom_dust_certified_<opp> / oi`, routed to
`record_uninsured_protocol_loss`) and `d_social = D_rem - d_phantom`.
`d_social` routes to `book_or_start_active_close_residual_to_side` when
`uncertified_potential == 0`, else to `record_uninsured_protocol_loss`.
Mirrors toly:5034-5069.
* `enqueue_adl` Step 8/10/11: `phantom_dust_certified_<side>` +
`phantom_dust_potential_<side>` maintained via `represented_after` /
`aggregate_gap` arithmetic. Full-drain / terminal-drain / Step 5 paths
zero both accumulators. Mirrors toly:5074-5135.
* Helper `ceil_mul_div_u128_or_wide` ported (toly:3398-3424). Kani-visible
Result-returning ceil(a*b/d) with U256 fallback (cfg(not(kani))) and Err
shortcut (cfg(kani)) on u128 overflow.
* Removed fork-only `inc_phantom_dust_potential_by` (its only call site
was the pre-v12.20.6 Step 10 dust write; toly inlines `aggregate_gap +
account_floor_bound` instead). `wide_mul_div_ceil_u128_or_over_i128max`
+ `OverI128Magnitude` imports dropped (only enqueue_adl used them).
Kani harnesses
--------------
* 3 rewritten — old K-adjust post-state assertions replaced with strictly
stronger v12.20.6 invariants:
- `t11_54_worked_example_regression` — replaces `adl_coeff_long != 0i128`
with `bankruptcy_hmax_lock_active` + `explicit_unallocated_loss_long == 500`.
- `t11_49_pure_pnl_bankruptcy_path` — replaces `adl_coeff_long != k_before`
with `bankruptcy_hmax_lock_active` + `explicit_unallocated_loss_long == 1000`.
- `proof_adl_pipeline_trade_liquidate_reopen` — replaces
`adl_coeff_short < k_short_before` with `bankruptcy_hmax_lock_active` +
`explicit_unallocated_loss_short == 1000`.
* 3 new harnesses pin the three observable D_rem routes:
- `proof_d_phantom_routes_to_uninsured_protocol_loss`
(`old_certified >= oi` shortcut).
- `proof_d_social_routes_to_uninsured_when_uncertified_gap_nonzero`
(`uncertified_potential != 0`).
- `proof_d_social_books_residual_when_uncertified_gap_zero`
(`uncertified_potential == 0` → residual booking; with
`loss_weight_sum_<opp> == 0` records explicit).
* Adjacent harnesses verified non-regressing:
`proof_enqueue_adl_arms_bankruptcy_lock_when_d_positive`,
`proof_enqueue_adl_leaves_bankruptcy_lock_when_d_zero`,
`t11_48_bankruptcy_liquidation_routes_q_when_D_zero`,
`t11_46_enqueue_adl_k_add_overflow_still_routes_quantity`,
`t4_17_enqueue_adl_preserves_oi_balance_qty_only`.
Engine Kani 360 → 363 (+3). All 335 host tests pass.
KL-FORK-ENGINE-BANKRUPT-CLOSE-1 fully REVOKED (was: PARTIALLY REVOKED
since Wave 11d Phase 1).
Drive-by fixes (pre-existing Kani-build breakages from prior waves)
-------------------------------------------------------------------
These prevented `cargo kani` from running on main; necessary to verify
Wave 11e's harnesses.
* `tests/common/mod.rs` — typo `max_max_max_trading_fee_bps` →
`max_trading_fee_bps` (introduced by an earlier auto-rename, never tested
under Kani at lines 110, 210).
* `tests/proofs_audit.rs:756` — `validate_execute_trade_entry` updated from
9-arg to 10-arg call (signature added separate `admit_h_max` in Wave
11a-ii; test was never updated). Inserted `admit_h_min = 0`.
* `test_visible!`-wrapped three fns broken by Wave 11d Phase 1 (commit
d0fae02): `assert_public_postconditions`, `settle_losses_with_context`,
`resolve_flat_negative_with_context`. The Wave 11d Phase 1 commit added
Kani tests that call these methods but never wrapped the methods
themselves. Kani-on-main has been silently broken since Wave 11d Phase 1.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
📝 WalkthroughWalkthroughThis PR implements Wave 11e B-residual routing in the ADL engine, introducing phantom-dust certified/potential split logic, a new overflow-safe ceil-mul-div helper, and replacing coefficient-based deficit accounting with explicit loss and bankruptcy-close state machine routing. All proof harnesses are updated to validate the new behavior. ChangesWave 11e ADL B-Residual Routing Implementation
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
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. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (1)
tests/proofs_instructions.rs (1)
823-861: ⚡ Quick winAlso pin
active_close_presenton the other two routing harnesses.Lines 824-827 and Lines 910-916 describe "no state-machine startup", but only the uncertified-gap proof actually asserts that. As written, these two proofs would still pass if
enqueue_adlspuriously started bankrupt-close state while preserving the loss buckets. Since this PR is explicitly restoring bankrupt-close parity, I'd snapshotactive_close_presenthere too.Suggested diff
fn proof_d_phantom_routes_to_uninsured_protocol_loss() { @@ let protocol_loss_before = engine.explicit_unallocated_protocol_loss.get(); let explicit_long_before = engine.explicit_unallocated_loss_long.get(); let k_before = engine.adl_coeff_long; + let active_close_before = engine.active_close_present; @@ assert!( engine.adl_coeff_long == k_before, "K must not be modified on the certified-saturated path" ); + assert!( + engine.active_close_present == active_close_before, + "phantom-only routing must not start bankrupt-close state" + ); } @@ fn proof_d_social_books_residual_when_uncertified_gap_zero() { @@ let protocol_loss_before = engine.explicit_unallocated_protocol_loss.get(); let explicit_long_before = engine.explicit_unallocated_loss_long.get(); + let active_close_before = engine.active_close_present; @@ assert!( engine.bankruptcy_hmax_lock_active, "Step 2 must arm the bankruptcy h_max lock when d > 0" ); + assert!( + engine.active_close_present == active_close_before, + "fully absorbed residual must not start bankrupt-close state" + ); }Also applies to: 909-955
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/proofs_instructions.rs` around lines 823 - 861, Snapshot the InstructionContext.active_close_present flag before calling enqueue_adl and assert it is unchanged after in the proof_d_phantom_routes_to_uninsured_protocol_loss test (and the other two routing-harness tests mentioned) so a spurious bankrupt-close start is detected; specifically, capture ctx.active_close_present into a local (e.g., let active_close_before = ctx.active_close_present) prior to calling RiskEngine::enqueue_adl, then add an assertion after the call that ctx.active_close_present == active_close_before; apply the same change to the other two routing harness functions that exercise enqueue_adl so all three pin active_close_present.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/percolator.rs`:
- Around line 4096-4109: The branch handling d_social must ensure B-side loss
weights are populated before deciding between record_uninsured_protocol_loss and
book_or_start_active_close_residual_to_side: populate loss_weight_sum_<side> and
each account's loss_weight / b_* on the live attach/trade/liquidation paths so
loss_weight_sum_* > 0 when appropriate; specifically, wire/update those
per-account and aggregate B-loss weight fields prior to the d_social routing
here (so book_or_start_active_close_residual_to_side sees correct weights)
rather than only relying on test pre-seeding — if there is an existing helper
that computes loss weights, call it before this branch, otherwise implement the
wiring logic and ensure record_uninsured_protocol_loss remains the fallback when
weights are truly zero.
---
Nitpick comments:
In `@tests/proofs_instructions.rs`:
- Around line 823-861: Snapshot the InstructionContext.active_close_present flag
before calling enqueue_adl and assert it is unchanged after in the
proof_d_phantom_routes_to_uninsured_protocol_loss test (and the other two
routing-harness tests mentioned) so a spurious bankrupt-close start is detected;
specifically, capture ctx.active_close_present into a local (e.g., let
active_close_before = ctx.active_close_present) prior to calling
RiskEngine::enqueue_adl, then add an assertion after the call that
ctx.active_close_present == active_close_before; apply the same change to the
other two routing harness functions that exercise enqueue_adl so all three pin
active_close_present.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 2b460abf-5258-43d9-9e8c-5eb4d71f8753
📒 Files selected for processing (5)
src/percolator.rstests/common/mod.rstests/proofs_audit.rstests/proofs_instructions.rstests/proofs_liveness.rs
Comment on lines
+4096
to
+4109
| if d_social != 0 { | ||
| if uncertified_potential != 0 { | ||
| self.record_uninsured_protocol_loss(d_social); | ||
| } else { | ||
| let (_booked, _recorded) = self.book_or_start_active_close_residual_to_side( | ||
| ctx, | ||
| u16::MAX, | ||
| opp, | ||
| self.last_oracle_price, | ||
| self.current_slot, | ||
| q_close_q, | ||
| d_social, | ||
| PUBLIC_B_CHUNK_ATOMS, | ||
| )?; |
There was a problem hiding this comment.
Wire the B-loss weights before routing d_social here.
This branch only reaches real B-booking when loss_weight_sum_<side> > 0, but this file still never populates non-zero loss_weight_sum_* or per-account loss_weight/b_* on the live attach/trade/liquidation paths. In normal engine state, book_or_start_active_close_residual_to_side() will therefore collapse to explicit loss recording instead of socializing or opening the active-close residual flow, so the advertised Wave 11e behavior is only reachable in tests that pre-seed those fields.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/percolator.rs` around lines 4096 - 4109, The branch handling d_social
must ensure B-side loss weights are populated before deciding between
record_uninsured_protocol_loss and book_or_start_active_close_residual_to_side:
populate loss_weight_sum_<side> and each account's loss_weight / b_* on the live
attach/trade/liquidation paths so loss_weight_sum_* > 0 when appropriate;
specifically, wire/update those per-account and aggregate B-loss weight fields
prior to the d_social routing here (so
book_or_start_active_close_residual_to_side sees correct weights) rather than
only relying on test pre-seeding — if there is an existing helper that computes
loss weights, call it before this branch, otherwise implement the wiring logic
and ensure record_uninsured_protocol_loss remains the fallback when weights are
truly zero.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
enqueue_adlStep 7/8/10/11. K is no longer modified for bankruptcy residual.D_remroutes. Engine Kani 360 → 363 (+3).Algorithmic change
K_opp -= ceil(D_rem * A_old * POS_SCALE / OI)with headroom checkD_remsplits intod_phantom(→ uninsured) +d_social(→ B-residual booking OR uninsured)adl_coeff_<opp>active_close_present+active_close_residual_*+explicit_unallocated_loss_<side>Both algorithms preserve global conservation.
Kani harnesses
3 rewritten (old K-adjust assertions replaced with B-residual equivalents):
t11_54_worked_example_regression— replacesadl_coeff_long != 0i128withbankruptcy_hmax_lock_active+explicit_unallocated_loss_long == 500.t11_49_pure_pnl_bankruptcy_path— replacesadl_coeff_long != k_beforewithbankruptcy_hmax_lock_active+explicit_unallocated_loss_long == 1000.proof_adl_pipeline_trade_liquidate_reopen— replacesadl_coeff_short < k_short_beforewithbankruptcy_hmax_lock_active+explicit_unallocated_loss_short == 1000.3 new:
proof_d_phantom_routes_to_uninsured_protocol_loss—old_certified >= oi→ fullD_remtorecord_uninsured_protocol_loss.proof_d_social_routes_to_uninsured_when_uncertified_gap_nonzero—uncertified_potential != 0→ both shares to uninsured.proof_d_social_books_residual_when_uncertified_gap_zero—uncertified_potential == 0→ social share tobook_or_start_active_close_residual_to_side.Drive-by fixes (pre-existing Kani-build breakages)
Kani-on-main has been silently broken since Wave 11d Phase 1. Necessary to fix to verify Wave 11e's harnesses:
tests/common/mod.rs:110,210— typomax_max_max_trading_fee_bps→max_trading_fee_bps.tests/proofs_audit.rs:756—validate_execute_trade_entry9-arg → 10-arg call (missingadmit_h_min = 0).assert_public_postconditions,settle_losses_with_context,resolve_flat_negative_with_contextwrapped intest_visible!macro (Wave 11d Phase 1 added Kani tests calling these but never wrapped them).Test plan
cargo build --release --tests --features test— clean.cargo test --release --features test --tests— 335 passed, 0 failed.verify-engine-preservation.sh,verify-engine-deferred-absent.sh,verify-eng-port-preservation.sh,verify-wrapper-preservation.sh— all silent.🤖 Generated with Claude Code
Summary by CodeRabbit