From e53116ea0d44c99ef6bd39c3275ca1bf94f82ff0 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Mon, 11 May 2026 11:10:34 +0100 Subject: [PATCH] =?UTF-8?q?sync(engine):=20Wave=2011e=20=E2=80=94=20v12.20?= =?UTF-8?q?.6=20enqueue=5Fadl=20B-residual=20algorithm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces fork's K-adjust ADL (`delta_K_abs = ceil(D_rem * A_old * POS_SCALE / OI)` written to `adl_coeff_`) 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_ / 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_` + `phantom_dust_potential_` 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_ == 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) --- src/percolator.rs | 233 ++++++++++++++++++++--------------- tests/common/mod.rs | 4 +- tests/proofs_audit.rs | 1 + tests/proofs_instructions.rs | 189 +++++++++++++++++++++++++++- tests/proofs_liveness.rs | 30 +++-- 5 files changed, 349 insertions(+), 108 deletions(-) diff --git a/src/percolator.rs b/src/percolator.rs index 7b067fa7b..72e4003ba 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -225,9 +225,8 @@ pub use i128::{I128, U128}; // ============================================================================ pub mod wide_math; use wide_math::{ - ceil_div_positive_checked, fee_debt_u128_checked, mul_div_ceil_u128, mul_div_floor_u128, - mul_div_floor_u256_with_rem, wide_mul_div_ceil_u128_or_over_i128max, wide_mul_div_floor_u128, - OverI128Magnitude, I256, U256, + ceil_div_positive_checked, fee_debt_u128_checked, mul_div_ceil_u128, mul_div_ceil_u256, + mul_div_floor_u128, mul_div_floor_u256_with_rem, wide_mul_div_floor_u128, I256, U256, }; // ============================================================================ @@ -1351,6 +1350,43 @@ impl RiskEngine { .checked_div(d) } + /// Kani-visible ceil(a * b / d) with U256 overflow fallback. + /// + /// Returns `Err(RiskError::Overflow)` when `d == 0` or when the wide + /// product overflows u128 even after the U256 path. Under `cfg(kani)` + /// the U256 fallback is skipped (returns `Err` on u128 overflow) to + /// keep harness time bounded. + /// + /// Mirrors toly engine `ceil_mul_div_u128_or_wide` (toly:3398-3424). + /// Used by `enqueue_adl` Step 7 (`d_phantom` certified-share split). + fn ceil_mul_div_u128_or_wide(a: u128, b: u128, d: u128) -> Result { + if d == 0 { + return Err(RiskError::Overflow); + } + if a == 0 || b == 0 { + return Ok(0); + } + if let Some(prod) = a.checked_mul(b) { + let q = prod / d; + let r = prod % d; + return if r == 0 { + Ok(q) + } else { + q.checked_add(1).ok_or(RiskError::Overflow) + }; + } + #[cfg(kani)] + { + Err(RiskError::Overflow) + } + #[cfg(not(kani))] + { + mul_div_ceil_u256(U256::from_u128(a), U256::from_u128(b), U256::from_u128(d)) + .try_into_u128() + .ok_or(RiskError::Overflow) + } + } + #[cfg(not(kani))] fn solvency_envelope_total_for_notional( params: &RiskParams, @@ -3200,32 +3236,6 @@ impl RiskEngine { Ok(()) } - /// Spec §4.6.1: increment phantom dust potential by amount_q (checked). - /// - /// Wave 6a: renamed from `inc_phantom_dust_bound_by`. Fork-only helper — - /// toly does the equivalent inline in liquidation step 10 (toly:5099). - /// Kept as a helper because the fork's liquidation step 10 formula - /// (`global_a_dust_bound = N_opp + ceil((OI + N_opp) / A_old)`) differs - /// from toly's `aggregate_gap + account_floor_bound` formula and reuses - /// this helper at one call site (try_close_position_at_oracle). - fn inc_phantom_dust_potential_by(&mut self, s: Side, amount_q: u128) -> Result<()> { - match s { - Side::Long => { - self.phantom_dust_potential_long_q = self - .phantom_dust_potential_long_q - .checked_add(amount_q) - .ok_or(RiskError::Overflow)?; - } - Side::Short => { - self.phantom_dust_potential_short_q = self - .phantom_dust_potential_short_q - .checked_add(amount_q) - .ok_or(RiskError::Overflow)?; - } - } - Ok(()) - } - /// Wave 6a / KL-PHANTOM-DUST-SCHEMA-1 (REVOKED): toly get/set helpers /// for the 4-field schema. Mirrors toly:3353-3378. /// @@ -4032,6 +4042,10 @@ impl RiskEngine { } self.set_oi_eff(opp, oi_post); if oi_post == 0 { + // Wave 11e: mirror toly:5012-5013 — fully drained side zeroes + // both phantom-dust accumulators (certified + potential). + self.set_phantom_dust_certified(opp, 0); + self.set_phantom_dust_potential(opp, 0); // Unconditionally reset the drained opp side (fixes phantom dust revert). set_pending_reset(ctx, opp); // Also reset liq_side only if it too has zero OI @@ -4047,65 +4061,52 @@ impl RiskEngine { return Err(RiskError::CorruptState); } - let a_old = self.get_a_side(opp); let oi_post = oi.checked_sub(q_close_q).ok_or(RiskError::Overflow)?; + let old_certified = core::cmp::min(self.get_phantom_dust_certified(opp), oi); + let old_potential = core::cmp::min(self.get_phantom_dust_potential(opp), oi); + let uncertified_potential = old_potential.saturating_sub(old_certified); - // Step 7 (§5.6 step 7): handle D_rem > 0 (quote deficit after insurance) - // Fused delta_K_abs = ceil(D_rem * A_old * POS_SCALE / OI) - // Per §1.5 Rule 14: if the quotient doesn't fit in i128, route to - // record_uninsured_protocol_loss instead of panicking. + // Step 7 (Wave 11e: v12.20.6 B-residual routing). + // + // K is no longer adjusted for bankruptcy residual; instead the deficit + // splits into a phantom-share (proportional to certified phantom dust) + // and a social-share. The phantom-share routes to non-claim audit loss + // (phantom-dust units cannot absorb claims). The social-share routes + // to the bankrupt-close residual state machine when the certified mass + // is pinned (uncertified_potential == 0), otherwise to uninsured loss + // (the certified mass isn't pinned, so socialization would be unfair). + // + // Mirrors toly engine `enqueue_adl` Step 7 (toly:5034-5069). if d_rem != 0 { - let a_ps = a_old.checked_mul(POS_SCALE).ok_or(RiskError::Overflow)?; - match wide_mul_div_ceil_u128_or_over_i128max(d_rem, a_ps, oi) { - Ok(delta_k_abs) => { - let delta_k = -(delta_k_abs as i128); - let k_opp = self.get_k_side(opp); - // Two-step headroom check (spec §5.6 clause 7): - // (a) the K add itself must fit i128 (checked_add) - // (b) the resulting K must leave room for any valid - // future mark-to-market step at MAX_ORACLE_PRICE - // on the same side: for side s with multiplier A_s, - // |new_k| + A_s * MAX_ORACLE_PRICE <= i128::MAX - // Without (b), a K value technically inside i128 - // can still make the next accrue_market_to overflow - // when the oracle moves, bricking live accrual. - // A_s cannot grow post-ADL (new A <= old A), so using - // a_old for the headroom budget is conservative. - let headroom_ok = match k_opp.checked_add(delta_k) { - Some(new_k) => { - let max_mark = U256::from_u128(a_old) - .checked_mul(U256::from_u128(MAX_ORACLE_PRICE as u128)); - match max_mark { - Some(mark) => { - // i128::MAX - |new_k| must be >= mark. - let abs_new_k = U256::from_u128(new_k.unsigned_abs()); - let i128_max_u = U256::from_u128(i128::MAX as u128); - match i128_max_u.checked_sub(abs_new_k) { - Some(budget) => { - if mark <= budget { Some(new_k) } else { None } - } - None => None, - } - } - None => None, - } - } - None => None, - }; - match headroom_ok { - Some(new_k) => { - self.set_k_side(opp, new_k)?; - } - None => { - // K-space overflow OR insufficient future mark headroom: - // route D_rem through record_uninsured (spec §1.7 clause 12). - self.record_uninsured_protocol_loss(d_rem); - } - } + let d_social = if old_certified >= oi { + self.record_uninsured_protocol_loss(d_rem); + 0 + } else { + let d_phantom = if old_certified == 0 { + 0 + } else { + Self::ceil_mul_div_u128_or_wide(d_rem, old_certified, oi)? + }; + let d_phantom = core::cmp::min(d_phantom, d_rem); + if d_phantom > 0 { + self.record_uninsured_protocol_loss(d_phantom); } - Err(OverI128Magnitude) => { - // Quotient overflow: route D_rem through record_uninsured (spec §1.7 clause 12). - self.record_uninsured_protocol_loss(d_rem); + d_rem - d_phantom + }; + 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, + )?; } } } @@ -4113,12 +4114,16 @@ impl RiskEngine { // Step 8 (§5.6 step 8): if OI_post == 0, both flags are set. if oi_post == 0 { self.set_oi_eff(opp, 0u128); + // Wave 11e: zero phantom-dust on full drain (toly:5074-5075). + self.set_phantom_dust_certified(opp, 0); + self.set_phantom_dust_potential(opp, 0); set_pending_reset(ctx, opp); set_pending_reset(ctx, liq_side); return Ok(()); } // Steps 8-9: compute A_candidate and A_trunc_rem using U256 intermediates + let a_old = self.get_a_side(opp); let a_old_u256 = U256::from_u128(a_old); let oi_post_u256 = U256::from_u128(oi_post); let oi_u256 = U256::from_u128(oi); @@ -4133,18 +4138,43 @@ impl RiskEngine { let a_new = a_candidate_u256.try_into_u128().ok_or(RiskError::Overflow)?; self.set_a_side(opp, a_new); self.set_oi_eff(opp, oi_post); - // Spec §5.6 step 10: increment phantom dust when OI actually decreased - if oi_post < oi { - let n_opp = self.get_stored_pos_count(opp) as u128; - let n_opp_u256 = U256::from_u128(n_opp); - // global_a_dust_bound = N_opp + ceil((OI_before + N_opp) / A_old) - let oi_plus_n = oi_u256.checked_add(n_opp_u256).unwrap_or(U256::MAX); - let ceil_term = ceil_div_positive_checked(oi_plus_n, a_old_u256); - let global_a_dust_bound = n_opp_u256.checked_add(ceil_term) - .unwrap_or(U256::MAX); - let bound_u128 = global_a_dust_bound.try_into_u128().unwrap_or(u128::MAX); - self.inc_phantom_dust_potential_by(opp, bound_u128)?; - } + // Wave 11e (v12.20.6): maintain phantom-dust certified+potential + // via represented_after / aggregate_gap arithmetic (toly:5097-5120). + // + // represented_source_lower = oi - old_potential (lower bound on + // represented mass before this step). + // represented_after = floor(represented_source_lower * a_new / a_old) + // (mass surviving the A shrink, clamped to oi_post). + // aggregate_gap = oi_post - represented_after (worst-case + // uncertified mass remaining). + // post_potential = min(oi_post, aggregate_gap + N_opp) (account-floor + // bound applied so the bound shrinks with stored_pos_count_opp). + // post_certified = min(oi_post, old_certified - q_close_q) + // (close pinned mass first, never above oi_post). + let represented_source_lower = oi + .checked_sub(old_potential) + .ok_or(RiskError::CorruptState)?; + let represented_after = U256::from_u128(represented_source_lower) + .checked_mul(U256::from_u128(a_new)) + .ok_or(RiskError::Overflow)? + .checked_div(U256::from_u128(a_old)) + .ok_or(RiskError::Overflow)? + .try_into_u128() + .ok_or(RiskError::Overflow)?; + let represented_after = core::cmp::min(oi_post, represented_after); + let aggregate_gap = oi_post + .checked_sub(represented_after) + .ok_or(RiskError::CorruptState)?; + let account_floor_bound = self.get_stored_pos_count(opp) as u128; + let post_potential = core::cmp::min( + oi_post, + aggregate_gap + .checked_add(account_floor_bound) + .ok_or(RiskError::Overflow)?, + ); + let post_certified = core::cmp::min(oi_post, old_certified.saturating_sub(q_close_q)); + self.set_phantom_dust_certified(opp, post_certified); + self.set_phantom_dust_potential(opp, post_potential); if a_new < MIN_A_SIDE { self.set_side_mode(opp, SideMode::DrainOnly); } @@ -4154,6 +4184,11 @@ impl RiskEngine { // Step 11: precision exhaustion terminal drain self.set_oi_eff(opp, 0u128); self.set_oi_eff(liq_side, 0u128); + // Wave 11e: zero phantom-dust on terminal drain (toly:5130-5133). + self.set_phantom_dust_certified(opp, 0); + self.set_phantom_dust_potential(opp, 0); + self.set_phantom_dust_certified(liq_side, 0); + self.set_phantom_dust_potential(liq_side, 0); set_pending_reset(ctx, opp); set_pending_reset(ctx, liq_side); @@ -4936,6 +4971,7 @@ impl RiskEngine { Ok(()) } + test_visible! { fn assert_public_postconditions(&self) -> Result<()> { self.assert_public_postconditions_fast()?; #[cfg(all( @@ -4945,6 +4981,7 @@ impl RiskEngine { self.validate_public_account_postconditions()?; Ok(()) } + } fn assert_public_postconditions_fast(&self) -> Result<()> { Self::validate_params_fast_shape(&self.params).map_err(|_| RiskError::CorruptState)?; @@ -5668,6 +5705,7 @@ impl RiskEngine { /// `positive_pnl_usability_mutated` admission gate); pass `None` from /// internal/contextless call sites to use the unguarded /// `_without_context` writer. + test_visible! { fn settle_losses_with_context( &mut self, idx: usize, @@ -5704,6 +5742,7 @@ impl RiskEngine { } Ok(()) } + } fn settle_losses(&mut self, idx: usize) -> Result<()> { self.settle_losses_with_context(idx, None) @@ -5717,6 +5756,7 @@ impl RiskEngine { /// (toly:7123-7149). The lock fires BEFORE `absorb_protocol_loss` so the /// envelope sees the pre-loss equity (so subsequent gates inside the same /// instruction observe the lock). + test_visible! { fn resolve_flat_negative_with_context( &mut self, idx: usize, @@ -5744,6 +5784,7 @@ impl RiskEngine { } Ok(()) } + } fn resolve_flat_negative(&mut self, idx: usize) -> Result<()> { self.resolve_flat_negative_with_context(idx, None) diff --git a/tests/common/mod.rs b/tests/common/mod.rs index abd9a8e61..b3fc91fc6 100644 --- a/tests/common/mod.rs +++ b/tests/common/mod.rs @@ -107,7 +107,7 @@ pub fn zero_fee_params() -> RiskParams { RiskParams { maintenance_margin_bps: 500, initial_margin_bps: 1000, - max_max_max_trading_fee_bps: 0, + max_trading_fee_bps: 0, max_accounts: MAX_ACCOUNTS as u64, liquidation_fee_bps: 0, liquidation_fee_cap: U128::ZERO, @@ -207,7 +207,7 @@ pub fn default_params() -> RiskParams { RiskParams { maintenance_margin_bps: 500, initial_margin_bps: 1000, - max_max_max_trading_fee_bps: 10, + max_trading_fee_bps: 10, max_accounts: MAX_ACCOUNTS as u64, liquidation_fee_bps: 100, liquidation_fee_cap: U128::new(1_000_000), diff --git a/tests/proofs_audit.rs b/tests/proofs_audit.rs index a672f5b1b..992aa8f3a 100644 --- a/tests/proofs_audit.rs +++ b/tests/proofs_audit.rs @@ -761,6 +761,7 @@ fn proof_trade_no_crank_gate() { size, DEFAULT_ORACLE, 0, + 0, 100, None, ); diff --git a/tests/proofs_instructions.rs b/tests/proofs_instructions.rs index 29f98b083..b48852d79 100644 --- a/tests/proofs_instructions.rs +++ b/tests/proofs_instructions.rs @@ -724,6 +724,27 @@ fn t11_52_touch_account_full_restart_fee_seniority() { #[kani::proof] #[kani::solver(cadical)] fn t11_54_worked_example_regression() { + // Wave 11e (v12.20.6 ADL): the K-adjust post-state (`adl_coeff_long != + // 0i128`) is gone — `enqueue_adl` no longer mutates K for bankruptcy + // residual. The deficit instead splits into the certified-phantom-share + // (uninsured loss) and the social share (B-residual booking or explicit + // non-claim loss when `loss_weight_sum_ == 0`). + // + // This setup leaves both phantom-dust accumulators at zero and never + // initializes loss_weight_sum_, so the social share (d_rem = 500) + // routes entirely through `add_explicit_unallocated_loss_side` via + // `book_or_start_active_close_residual_to_side`. + // + // Pinned invariants (algorithm-agnostic, still valid): + // - A_opp was reduced (Step 10 shrank `adl_mult_long`). + // - OI_opp was reduced by `q_close`. + // - Lazy K-snap sync still works (both engine and account K stay 0). + // - Conservation holds. + // Pinned invariants (new under v12.20.6): + // - Bankruptcy h_max lock was armed (Step 2). + // - Exactly d_social = 500 atoms routed to the long-side explicit + // non-claim loss bucket (since loss_weight_sum_long == 0, the entire + // chunk records explicit and no state-machine startup is needed). let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, 100); let a = add_user_test(&mut engine, 0).unwrap(); @@ -758,9 +779,17 @@ fn t11_54_worked_example_regression() { let r2 = engine.enqueue_adl(&mut ctx, Side::Short, q_close, d); assert!(r2.is_ok()); - assert!(engine.adl_mult_long < ADL_ONE); - assert!(engine.oi_eff_long_q == POS_SCALE); - assert!(engine.adl_coeff_long != 0i128); + assert!(engine.adl_mult_long < ADL_ONE, "A_opp must shrink"); + assert!(engine.oi_eff_long_q == POS_SCALE, "OI_opp must shrink by q_close"); + assert!( + engine.bankruptcy_hmax_lock_active, + "v12.20.6: Step 2 must arm the bankruptcy h_max lock when d > 0" + ); + assert!( + engine.explicit_unallocated_loss_long.get() == d, + "v12.20.6: d_social == d must be recorded as explicit non-claim loss \ + on opp side when loss_weight_sum_ == 0 (no holders to absorb)" + ); let _ = { let mut _ctx = InstructionContext::new_with_admission(0, 100); @@ -771,6 +800,160 @@ fn t11_54_worked_example_regression() { assert!(engine.check_conservation()); } +// ============================================================================ +// Wave 11e: v12.20.6 enqueue_adl B-residual routing harnesses +// +// Pins the three observable routes of `D_rem` under the new algorithm: +// 1. Certified-phantom-dust share routes to `record_uninsured_protocol_loss` +// (the `explicit_unallocated_protocol_loss` bucket), because phantom-dust +// units cannot absorb claims. +// 2. Social share routes to `record_uninsured_protocol_loss` when +// `uncertified_potential != 0` (gap between certified and potential +// means the certified mass isn't pinned, so socialization would be +// unfair). +// 3. Social share routes to `book_or_start_active_close_residual_to_side` +// when `uncertified_potential == 0` (certified mass is pinned). +// Without B-tracking holders (`loss_weight_sum_ == 0`), this +// degenerates to `add_explicit_unallocated_loss_side` (records_explicit +// path in `plan_bankruptcy_residual_chunk_to_side`). +// ============================================================================ + +#[kani::proof] +#[kani::solver(cadical)] +fn proof_d_phantom_routes_to_uninsured_protocol_loss() { + // Pre-state: opp side has `old_certified == oi`. Step 7 takes the + // `old_certified >= oi` shortcut and routes the entire d_rem through + // `record_uninsured_protocol_loss` — no B-residual booking attempted, + // no K modification. + let mut engine = RiskEngine::new(zero_fee_params()); + let mut ctx = InstructionContext::new(); + + engine.adl_mult_long = POS_SCALE; + engine.oi_eff_long_q = 2 * POS_SCALE; + engine.oi_eff_short_q = 2 * POS_SCALE; + engine.stored_pos_count_long = 1; + // Saturate certified phantom dust on the opp (long) side. + engine.phantom_dust_certified_long_q = 2 * POS_SCALE; + engine.phantom_dust_potential_long_q = 2 * POS_SCALE; + + 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 d = 700u128; + let q_close = 0u128; + + let result = engine.enqueue_adl(&mut ctx, Side::Short, q_close, d); + assert!(result.is_ok()); + + assert!( + engine.explicit_unallocated_protocol_loss.get() == protocol_loss_before + d, + "fully-certified opp side routes entire d_rem to uninsured loss" + ); + assert!( + engine.explicit_unallocated_loss_long.get() == explicit_long_before, + "no explicit non-claim loss recorded on the certified-saturated path" + ); + assert!( + engine.adl_coeff_long == k_before, + "K must not be modified on the certified-saturated path" + ); +} + +#[kani::proof] +#[kani::solver(cadical)] +fn proof_d_social_routes_to_uninsured_when_uncertified_gap_nonzero() { + // Pre-state: opp side has 0 < old_certified < oi AND + // old_potential > old_certified (so uncertified_potential != 0). + // d_phantom proportional to certified routes to uninsured; d_social + // (the remainder) ALSO routes to uninsured because the certified mass + // isn't pinned (socializing would be unfair). + let mut engine = RiskEngine::new(zero_fee_params()); + let mut ctx = InstructionContext::new(); + + engine.adl_mult_long = POS_SCALE; + engine.oi_eff_long_q = 4 * POS_SCALE; + engine.oi_eff_short_q = 4 * POS_SCALE; + engine.stored_pos_count_long = 1; + // Half-certified + uncertified gap. + engine.phantom_dust_certified_long_q = 2 * POS_SCALE; + engine.phantom_dust_potential_long_q = 3 * POS_SCALE; + + 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; + + let d = 400u128; + let q_close = 0u128; + + let result = engine.enqueue_adl(&mut ctx, Side::Short, q_close, d); + assert!(result.is_ok()); + + assert!( + engine.explicit_unallocated_protocol_loss.get() == protocol_loss_before + d, + "uncertified-gap-nonzero path routes the entire d_rem to uninsured \ + (d_phantom + d_social both increment protocol_loss)" + ); + assert!( + engine.explicit_unallocated_loss_long.get() == explicit_long_before, + "no explicit non-claim loss on the uncertified-gap path" + ); + assert!( + engine.active_close_present == active_close_before, + "no bankrupt-close state machine startup on the uncertified-gap path" + ); +} + +#[kani::proof] +#[kani::solver(cadical)] +fn proof_d_social_books_residual_when_uncertified_gap_zero() { + // Pre-state: opp side has old_certified == old_potential (and both < + // oi). uncertified_potential == 0 → d_social routes through + // `book_or_start_active_close_residual_to_side`. With no B-tracking + // holders (loss_weight_sum_ == 0), the chunk plan records explicit + // and `add_explicit_unallocated_loss_side` writes the full d_social to + // the opp side's explicit non-claim bucket. No state-machine startup + // since the entire residual is absorbed in one chunk. + let mut engine = RiskEngine::new(zero_fee_params()); + let mut ctx = InstructionContext::new(); + + engine.adl_mult_long = POS_SCALE; + engine.oi_eff_long_q = 4 * POS_SCALE; + engine.oi_eff_short_q = 4 * POS_SCALE; + engine.stored_pos_count_long = 1; + // Half-certified, no uncertified gap. + engine.phantom_dust_certified_long_q = 2 * POS_SCALE; + engine.phantom_dust_potential_long_q = 2 * POS_SCALE; + + let protocol_loss_before = engine.explicit_unallocated_protocol_loss.get(); + let explicit_long_before = engine.explicit_unallocated_loss_long.get(); + + let d = 400u128; + let q_close = 0u128; + + let result = engine.enqueue_adl(&mut ctx, Side::Short, q_close, d); + assert!(result.is_ok()); + + // d_phantom = ceil(400 * 2*POS_SCALE / 4*POS_SCALE) = 200. + // d_social = 400 - 200 = 200. + let expected_d_phantom = 200u128; + let expected_d_social = d - expected_d_phantom; + + assert!( + engine.explicit_unallocated_protocol_loss.get() == protocol_loss_before + expected_d_phantom, + "d_phantom must route to uninsured protocol loss" + ); + assert!( + engine.explicit_unallocated_loss_long.get() == explicit_long_before + expected_d_social, + "d_social must route to explicit non-claim loss on opp side \ + (no holders → records_explicit path)" + ); + assert!( + engine.bankruptcy_hmax_lock_active, + "Step 2 must arm the bankruptcy h_max lock when d > 0" + ); +} + #[kani::proof] #[kani::unwind(34)] #[kani::solver(cadical)] diff --git a/tests/proofs_liveness.rs b/tests/proofs_liveness.rs index db12c29d6..8d6fb347b 100644 --- a/tests/proofs_liveness.rs +++ b/tests/proofs_liveness.rs @@ -207,6 +207,10 @@ fn t11_48_bankruptcy_liquidation_routes_q_when_D_zero() { #[kani::proof] #[kani::solver(cadical)] fn t11_49_pure_pnl_bankruptcy_path() { + // Wave 11e (v12.20.6 ADL): pure-PnL bankruptcy (q_close = 0, D > 0) + // socializes the deficit via the B-residual path now, not via K-adjust. + // Asserts the new post-state: lock armed + entire D recorded as explicit + // non-claim loss on the opposing side (no holders → records_explicit). let mut engine = RiskEngine::new(zero_fee_params()); let mut ctx = InstructionContext::new(); @@ -217,7 +221,6 @@ fn t11_49_pure_pnl_bankruptcy_path() { engine.stored_pos_count_long = 1; let a_before = engine.adl_mult_long; - let k_before = engine.adl_coeff_long; let d = 1_000u128; let q_close = 0u128; @@ -230,8 +233,13 @@ fn t11_49_pure_pnl_bankruptcy_path() { "A must be unchanged for pure PnL bankruptcy" ); assert!( - engine.adl_coeff_long != k_before, - "K must change when D > 0" + engine.bankruptcy_hmax_lock_active, + "v12.20.6: Step 2 must arm the bankruptcy h_max lock when D > 0" + ); + assert!( + engine.explicit_unallocated_loss_long.get() == d, + "v12.20.6: full d_social == D must record as explicit non-claim loss \ + on opp side when loss_weight_sum_ == 0" ); assert!(engine.oi_eff_long_q == 2 * POS_SCALE); } @@ -490,8 +498,8 @@ fn proof_adl_pipeline_trade_liquidate_reopen() { assert!(engine.check_conservation()); let mut ctx = InstructionContext::new(); - let k_short_before = engine.adl_coeff_short; - let result = engine.enqueue_adl(&mut ctx, Side::Long, size, 1_000u128); + let d = 1_000u128; + let result = engine.enqueue_adl(&mut ctx, Side::Long, size, d); assert!(result.is_ok(), "ADL enqueue must succeed for balanced OI"); assert!( engine.oi_eff_long_q == engine.oi_eff_short_q, @@ -507,9 +515,17 @@ fn proof_adl_pipeline_trade_liquidate_reopen() { ctx.pending_reset_short, "ADL full drain must schedule short reset" ); + // Wave 11e (v12.20.6 ADL): deficit is socialized to opp side via the + // B-residual booking path, not via K-adjust. With no loss-weight on + // opp side, the full d records as explicit non-claim loss. + assert!( + engine.bankruptcy_hmax_lock_active, + "Step 2 must arm the bankruptcy h_max lock when d > 0" + ); assert!( - engine.adl_coeff_short < k_short_before, - "deficit must be socialized to the opposing short side K" + engine.explicit_unallocated_loss_short.get() == d, + "v12.20.6: d_social == d must record as explicit non-claim loss \ + on opp (short) side when loss_weight_sum_short == 0" ); assert!(engine.check_conservation());