From 6149b0382c526462c61159221cc5289ec78d0b38 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 23:11:49 +0100 Subject: [PATCH] =?UTF-8?q?sync(engine):=20Wave=206a=20=E2=80=94=20phantom?= =?UTF-8?q?-dust=204-field=20schema=20(KL-PHANTOM-DUST-SCHEMA-1=20REVOKED)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adopts toly's 4-field phantom-dust schema (certified + potential per side, toly:783-786). Closes the long-standing single-bound vs split divergence flagged in Phase 2. Schema: - `phantom_dust_bound__q` → `phantom_dust_potential__q` (renamed; semantically identical upper-bound tracking) - Added `phantom_dust_certified__q` per side — lower-bound dust certified by B-tracking-aware liquidation step 7 (toly:5030-5118). Always 0 on this branch: B-tracking subsystem isn't ported, so the certified fields exist purely for wire-format alignment with toly + NFT vendored-bytes mirroring (Wave 6c). When B-tracking lands, the certified field starts receiving non-zero values from the new liquidation logic with no schema break. - Net RiskEngine growth: +32 bytes (2 × u128 → 4 × u128). Helpers: - `inc_phantom_dust_bound` → `inc_phantom_dust_potential` (rename only) - `inc_phantom_dust_bound_by` → `inc_phantom_dust_potential_by` (fork-only liquidation step-10 helper, kept; toly inlines the equivalent at toly:5099 but uses a different post-state formula) - New toly-aligned: `get/set_phantom_dust_certified`, `get/set_phantom_dust_potential` (toly:3353-3378). Setters are grounded in resolve_market zeroing; getters in the new `assert_public_postconditions` invariant. Callsites updated: - `sync_account_fee_to_slot_not_atomic` precision-boundary increment - `try_close_position_at_oracle` step-10 dust bump (uses _by helper) - `begin_full_drain_reset` full-drain side zeroing (now clears both certified + potential per side, matching toly's `begin_terminal_epoch_exhaustion_reset` semantics) - `schedule_end_of_instruction_resets` §5.7 A/B/C — OI-cap uses `phantom_dust_potential__q` (renamed bound) - `resolve_market_not_atomic` clears all 4 fields per side on `pre_stored_ == 0` (matches toly:9637-9644) New invariant: - `assert_public_postconditions` now asserts `certified <= potential` per side as a forward-looking defense-in-depth gate. Trivially holds on this branch (certified always 0); guards against off-by-one / step-ordering bugs once B-tracking lands. Kani: - 2 new harnesses in proofs_invariants.rs: - `proof_phantom_dust_certified_le_potential_at_genesis` - `proof_phantom_dust_certified_gt_potential_rejects` - Total engine Kani proof count: 311 → 313. KEEP_LIST: - KL-PHANTOM-DUST-SCHEMA-1 marked REVOKED. Verify scripts: - verify-engine-preservation.sh: §A.1/§A.2 entries removed (fields renamed); §F.4 updated to track inc_phantom_dust_potential; §F.5 updated to track inc_phantom_dust_potential_by (still fork-only). - verify-engine-deferred-absent.sh: phantom_dust_{certified,potential} EXPECT_ABSENT entries removed (fields now legitimately present). Migration: - Path B per Wave 6 pre-decision: force-resolve + rebuild J51cB2 during deployment prep, no on-chain migration instruction in code. Only 1 mainnet market live + closed beta. Operationally trivial. Tests: 335 passing, 0 regressions. Build: cargo build --release clean. Verify: both engine verify scripts silent. Follow-ups (Wave 6 sub-PRs): - Wave 6b: dynamic-fee API rename + per-call threading - Wave 6c: percolator-nft slab_types mirror update for 4-field schema - Wave 6d: wrapper integration + SLAB_LEN bump (includes the 2-line wrapper offset-print rename — already coupled to this engine PR via path = "../percolator") Co-Authored-By: Claude Opus 4.7 (1M context) --- examples/detailed_offsets.rs | 4 +- src/percolator.rs | 180 +++++++++++++++++++++++++++-------- tests/proofs_instructions.rs | 58 +++++------ tests/proofs_invariants.rs | 56 +++++++++++ tests/proofs_liveness.rs | 2 +- tests/proofs_safety.rs | 10 +- 6 files changed, 231 insertions(+), 79 deletions(-) diff --git a/examples/detailed_offsets.rs b/examples/detailed_offsets.rs index 8ce62e381..fcf286373 100644 --- a/examples/detailed_offsets.rs +++ b/examples/detailed_offsets.rs @@ -62,8 +62,8 @@ fn main() { println!("stored_pos_count_short:{}", offset_of!(RiskEngine, stored_pos_count_short)); println!("stale_account_count_long:{}", offset_of!(RiskEngine, stale_account_count_long)); println!("stale_account_count_short:{}", offset_of!(RiskEngine, stale_account_count_short)); - println!("phantom_dust_bound_long_q:{}", offset_of!(RiskEngine, phantom_dust_bound_long_q)); - println!("phantom_dust_bound_short_q:{}", offset_of!(RiskEngine, phantom_dust_bound_short_q)); + println!("phantom_dust_potential_long_q:{}", offset_of!(RiskEngine, phantom_dust_potential_long_q)); + println!("phantom_dust_potential_short_q:{}", offset_of!(RiskEngine, phantom_dust_potential_short_q)); println!("materialized_account_count:{}", offset_of!(RiskEngine, materialized_account_count)); println!("neg_pnl_account_count:{}", offset_of!(RiskEngine, neg_pnl_account_count)); println!("last_oracle_price:{}", offset_of!(RiskEngine, last_oracle_price)); diff --git a/src/percolator.rs b/src/percolator.rs index c05f51dd5..e24999cf2 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -665,9 +665,27 @@ pub struct RiskEngine { pub stale_account_count_long: u64, pub stale_account_count_short: u64, - /// Dynamic phantom dust bounds (spec §4.6, §5.7) - pub phantom_dust_bound_long_q: u128, - pub phantom_dust_bound_short_q: u128, + /// Wave 6a / KL-PHANTOM-DUST-SCHEMA-1 (REVOKED): adopt toly's 4-field + /// phantom-dust schema (certified + potential per side, toly:783-786). + /// + /// `potential__q` is the upper bound — the maximum representable + /// dust on `` given account-floor slack and the OI-cap math. + /// Semantically identical to the fork's prior `phantom_dust_bound__q` + /// (renamed; see `inc_phantom_dust_potential` / `_by`). + /// + /// `certified__q` is the lower bound — dust that's been certified + /// by the B-tracking-aware liquidation step 7 (toly:5030-5118). The fork + /// hasn't ported B-tracking, so `certified__q` is always 0 on this + /// branch: it exists purely for wire-format alignment with toly + NFT + /// vendored-bytes mirroring (Wave 6c). When B-tracking is ported in a + /// future wave, the certified field will start receiving non-zero values + /// from the new liquidation logic with no schema break. + /// + /// Spec §4.6, §5.7. Toly engine ref: src/percolator.rs:783-786. + pub phantom_dust_certified_long_q: u128, + pub phantom_dust_certified_short_q: u128, + pub phantom_dust_potential_long_q: u128, + pub phantom_dust_potential_short_q: u128, /// Materialized account count (spec §2.2) pub materialized_account_count: u64, @@ -1550,8 +1568,12 @@ impl RiskEngine { stored_pos_count_short: 0, stale_account_count_long: 0, stale_account_count_short: 0, - phantom_dust_bound_long_q: 0u128, - phantom_dust_bound_short_q: 0u128, + // Wave 6a: 4-field phantom-dust schema. `certified` always 0 on + // this branch (no B-tracking-aware certification logic). + phantom_dust_certified_long_q: 0u128, + phantom_dust_certified_short_q: 0u128, + phantom_dust_potential_long_q: 0u128, + phantom_dust_potential_short_q: 0u128, materialized_account_count: 0, neg_pnl_account_count: 0, // Wave 4a: bankrupt-close gate variables — see init_in_place @@ -1678,8 +1700,11 @@ impl RiskEngine { self.stored_pos_count_short = 0; self.stale_account_count_long = 0; self.stale_account_count_short = 0; - self.phantom_dust_bound_long_q = 0; - self.phantom_dust_bound_short_q = 0; + // Wave 6a: 4-field phantom-dust schema. See struct comment. + self.phantom_dust_certified_long_q = 0; + self.phantom_dust_certified_short_q = 0; + self.phantom_dust_potential_long_q = 0; + self.phantom_dust_potential_short_q = 0; self.materialized_account_count = 0; self.neg_pnl_account_count = 0; // Wave 4a: bankrupt-close gate variables init to no-active state. @@ -2503,7 +2528,7 @@ impl RiskEngine { let rem = p.checked_rem(U256::from_u128(a_basis)); if let Some(r) = rem { if !r.is_zero() { - self.inc_phantom_dust_bound(old_side)?; + self.inc_phantom_dust_potential(old_side)?; } } } @@ -2823,18 +2848,23 @@ impl RiskEngine { } } - /// Spec §4.6: increment phantom dust bound by 1 q-unit (checked). - fn inc_phantom_dust_bound(&mut self, s: Side) -> Result<()> { + /// Spec §4.6: increment phantom dust potential by 1 q-unit (checked). + /// + /// Wave 6a (KL-PHANTOM-DUST-SCHEMA-1 REVOKED): renamed from + /// `inc_phantom_dust_bound`. Semantically identical; the field rename + /// is `phantom_dust_bound__q` → `phantom_dust_potential__q`. + /// Mirrors toly `inc_phantom_dust_potential` (toly:3335-3352). + fn inc_phantom_dust_potential(&mut self, s: Side) -> Result<()> { match s { Side::Long => { - self.phantom_dust_bound_long_q = self - .phantom_dust_bound_long_q + self.phantom_dust_potential_long_q = self + .phantom_dust_potential_long_q .checked_add(1u128) .ok_or(RiskError::Overflow)?; } Side::Short => { - self.phantom_dust_bound_short_q = self - .phantom_dust_bound_short_q + self.phantom_dust_potential_short_q = self + .phantom_dust_potential_short_q .checked_add(1u128) .ok_or(RiskError::Overflow)?; } @@ -2842,18 +2872,25 @@ impl RiskEngine { Ok(()) } - /// Spec §4.6.1: increment phantom dust bound by amount_q (checked). - fn inc_phantom_dust_bound_by(&mut self, s: Side, amount_q: u128) -> Result<()> { + /// 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_bound_long_q = self - .phantom_dust_bound_long_q + 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_bound_short_q = self - .phantom_dust_bound_short_q + self.phantom_dust_potential_short_q = self + .phantom_dust_potential_short_q .checked_add(amount_q) .ok_or(RiskError::Overflow)?; } @@ -2861,6 +2898,40 @@ impl RiskEngine { Ok(()) } + /// Wave 6a / KL-PHANTOM-DUST-SCHEMA-1 (REVOKED): toly get/set helpers + /// for the 4-field schema. Mirrors toly:3353-3378. + /// + /// `certified` is always 0 on this branch (see field doc); the setters + /// exist so future B-tracking liquidation logic can be ported in place + /// without re-shaping helper call sites. + fn get_phantom_dust_certified(&self, s: Side) -> u128 { + match s { + Side::Long => self.phantom_dust_certified_long_q, + Side::Short => self.phantom_dust_certified_short_q, + } + } + + fn set_phantom_dust_certified(&mut self, s: Side, v: u128) { + match s { + Side::Long => self.phantom_dust_certified_long_q = v, + Side::Short => self.phantom_dust_certified_short_q = v, + } + } + + fn get_phantom_dust_potential(&self, s: Side) -> u128 { + match s { + Side::Long => self.phantom_dust_potential_long_q, + Side::Short => self.phantom_dust_potential_short_q, + } + } + + fn set_phantom_dust_potential(&mut self, s: Side, v: u128) { + match s { + Side::Long => self.phantom_dust_potential_long_q = v, + Side::Short => self.phantom_dust_potential_short_q = v, + } + } + // ======================================================================== // effective_pos_q (spec §5.2) // ======================================================================== @@ -2962,7 +3033,7 @@ impl RiskEngine { self.set_pnl_with_reserve(idx, new_pnl, ReserveMode::UseAdmissionPair(ctx.admit_h_min_shared, ctx.admit_h_max_shared), Some(ctx))?; if q_eff_new == 0 { - self.inc_phantom_dust_bound(side)?; + self.inc_phantom_dust_potential(side)?; self.set_position_basis_q(idx, 0i128)?; self.accounts[idx].adl_a_basis = ADL_ONE; self.accounts[idx].adl_k_snap = 0i128; @@ -3588,7 +3659,7 @@ impl RiskEngine { 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_bound_by(opp, bound_u128)?; + self.inc_phantom_dust_potential_by(opp, bound_u128)?; } if a_new < MIN_A_SIDE { self.set_side_mode(opp, SideMode::DrainOnly); @@ -3672,10 +3743,17 @@ impl RiskEngine { let spc = self.get_stored_pos_count(side); self.set_stale_count(side, spc); - // phantom_dust_bound_side_q = 0 (spec §2.5 step 6) + // phantom_dust = 0 on full-drain side reset (spec §2.5 step 6). + // Wave 6a: zero both certified and potential for the 4-field schema. match side { - Side::Long => self.phantom_dust_bound_long_q = 0u128, - Side::Short => self.phantom_dust_bound_short_q = 0u128, + Side::Long => { + self.phantom_dust_certified_long_q = 0u128; + self.phantom_dust_potential_long_q = 0u128; + } + Side::Short => { + self.phantom_dust_certified_short_q = 0u128; + self.phantom_dust_potential_short_q = 0u128; + } } // mode = ResetPending @@ -3709,15 +3787,21 @@ impl RiskEngine { test_visible! { fn schedule_end_of_instruction_resets(&mut self, ctx: &mut InstructionContext) -> Result<()> { + // Wave 6a: OI-cap uses `phantom_dust_potential__q` (the upper + // bound) — renamed from `phantom_dust_bound__q`, semantically + // identical. `certified__q` is the lower bound and is always 0 + // on this branch (no B-tracking-aware certification), so it doesn't + // participate in the cap. + // // §5.7.A: Bilateral-empty dust clearance if self.stored_pos_count_long == 0 && self.stored_pos_count_short == 0 { - let clear_bound_q = self.phantom_dust_bound_long_q - .checked_add(self.phantom_dust_bound_short_q) + let clear_bound_q = self.phantom_dust_potential_long_q + .checked_add(self.phantom_dust_potential_short_q) .ok_or(RiskError::CorruptState)?; let has_residual = self.oi_eff_long_q != 0 || self.oi_eff_short_q != 0 - || self.phantom_dust_bound_long_q != 0 - || self.phantom_dust_bound_short_q != 0; + || self.phantom_dust_potential_long_q != 0 + || self.phantom_dust_potential_short_q != 0; if has_residual { if self.oi_eff_long_q != self.oi_eff_short_q { return Err(RiskError::CorruptState); @@ -3736,12 +3820,12 @@ impl RiskEngine { else if self.stored_pos_count_long == 0 && self.stored_pos_count_short > 0 { let has_residual = self.oi_eff_long_q != 0 || self.oi_eff_short_q != 0 - || self.phantom_dust_bound_long_q != 0; + || self.phantom_dust_potential_long_q != 0; if has_residual { if self.oi_eff_long_q != self.oi_eff_short_q { return Err(RiskError::CorruptState); } - if self.oi_eff_long_q <= self.phantom_dust_bound_long_q { + if self.oi_eff_long_q <= self.phantom_dust_potential_long_q { self.oi_eff_long_q = 0u128; self.oi_eff_short_q = 0u128; ctx.pending_reset_long = true; @@ -3755,12 +3839,12 @@ impl RiskEngine { else if self.stored_pos_count_short == 0 && self.stored_pos_count_long > 0 { let has_residual = self.oi_eff_long_q != 0 || self.oi_eff_short_q != 0 - || self.phantom_dust_bound_short_q != 0; + || self.phantom_dust_potential_short_q != 0; if has_residual { if self.oi_eff_long_q != self.oi_eff_short_q { return Err(RiskError::CorruptState); } - if self.oi_eff_short_q <= self.phantom_dust_bound_short_q { + if self.oi_eff_short_q <= self.phantom_dust_potential_short_q { self.oi_eff_long_q = 0u128; self.oi_eff_short_q = 0u128; ctx.pending_reset_long = true; @@ -4352,6 +4436,19 @@ impl RiskEngine { if self.market_mode == MarketMode::Live && self.pnl_pos_tot > MAX_PNL_POS_TOT { return Err(RiskError::CorruptState); } + // Wave 6a / KL-PHANTOM-DUST-SCHEMA-1 (REVOKED): certified is a lower + // bound, potential is the upper bound; certified must never exceed + // potential on either side. On this branch certified is always 0 + // (see field doc), so the invariant is `0 <= potential` — trivially + // true — but the explicit check grounds the get helpers and matches + // toly's defense-in-depth posture once B-tracking lands. + if self.get_phantom_dust_certified(Side::Long) + > self.get_phantom_dust_potential(Side::Long) + || self.get_phantom_dust_certified(Side::Short) + > self.get_phantom_dust_potential(Side::Short) + { + return Err(RiskError::CorruptState); + } if self.materialized_account_count > self.params.max_accounts { return Err(RiskError::CorruptState); } @@ -7170,18 +7267,17 @@ impl RiskEngine { self.oi_eff_short_q = 0; // PORT (ENG-PORT-5a / CRITICAL-9 — Hunk 5): phantom-dust zero on - // pre_stored_ == 0. ADAPTED to fork's single-bound phantom_dust - // schema per KL-PHANTOM-DUST-SCHEMA-1 (toly uses the certified+potential - // pair phantom_dust_certified__q + phantom_dust_potential__q; - // fork uses the single-bound phantom_dust_bound__q). Semantically - // equivalent: no stored positions ⇒ no dust to track. - // Without this, fork-resolved markets carry stale phantom-dust into the - // resolved-payout-h-num/den ratio. + // pre_stored_ == 0. Wave 6a (KL-PHANTOM-DUST-SCHEMA-1 REVOKED): + // now clears all 4 fields of the toly-aligned schema (certified + + // potential per side, toly:9637-9644). Without this, resolved markets + // carry stale phantom-dust into the resolved-payout h-num/den ratio. if pre_stored_long == 0 { - self.phantom_dust_bound_long_q = 0u128; + self.set_phantom_dust_certified(Side::Long, 0); + self.set_phantom_dust_potential(Side::Long, 0); } if pre_stored_short == 0 { - self.phantom_dust_bound_short_q = 0u128; + self.set_phantom_dust_certified(Side::Short, 0); + self.set_phantom_dust_potential(Side::Short, 0); } // Steps 17-20: drain/finalize sides diff --git a/tests/proofs_instructions.rs b/tests/proofs_instructions.rs index 8bdb21e81..0eddd1237 100644 --- a/tests/proofs_instructions.rs +++ b/tests/proofs_instructions.rs @@ -114,8 +114,8 @@ fn t3_17_clean_empty_engine_no_retrigger() { assert!(engine.stored_pos_count_short == 0); assert!(engine.oi_eff_long_q == 0); assert!(engine.oi_eff_short_q == 0); - assert!(engine.phantom_dust_bound_long_q == 0); - assert!(engine.phantom_dust_bound_short_q == 0); + assert!(engine.phantom_dust_potential_long_q == 0); + assert!(engine.phantom_dust_potential_short_q == 0); let result = engine.schedule_end_of_instruction_resets(&mut ctx); assert!(result.is_ok()); @@ -130,14 +130,14 @@ fn t3_17_clean_empty_engine_no_retrigger() { fn t3_18_dust_bound_reset_in_begin_full_drain() { let mut engine = RiskEngine::new(zero_fee_params()); - engine.phantom_dust_bound_long_q = 5u128; + engine.phantom_dust_potential_long_q = 5u128; engine.oi_eff_long_q = 0u128; engine.begin_full_drain_reset(Side::Long); assert!( - engine.phantom_dust_bound_long_q == 0, - "phantom_dust_bound must be zeroed by begin_full_drain_reset" + engine.phantom_dust_potential_long_q == 0, + "phantom_dust_potential must be zeroed by begin_full_drain_reset" ); } @@ -493,13 +493,13 @@ fn t11_41_attach_effective_position_remainder_accounting() { engine.adl_mult_long = 6; engine.stored_pos_count_long = 1; - let dust_before = engine.phantom_dust_bound_long_q; + let dust_before = engine.phantom_dust_potential_long_q; let new_pos = (2 * POS_SCALE) as i128; engine.attach_effective_position(idx as usize, new_pos); assert!( - engine.phantom_dust_bound_long_q > dust_before, + engine.phantom_dust_potential_long_q > dust_before, "dust bound must increment on nonzero remainder" ); @@ -508,11 +508,11 @@ fn t11_41_attach_effective_position_remainder_accounting() { engine.accounts[idx as usize].adl_a_basis = ADL_ONE; engine.adl_mult_long = ADL_ONE; - let dust_before2 = engine.phantom_dust_bound_long_q; + let dust_before2 = engine.phantom_dust_potential_long_q; engine.attach_effective_position(idx as usize, (3 * POS_SCALE) as i128); assert!( - engine.phantom_dust_bound_long_q == dust_before2, + engine.phantom_dust_potential_long_q == dust_before2, "dust bound must not increment on zero remainder" ); } @@ -546,14 +546,14 @@ fn t11_42_dynamic_dust_bound_inductive() { engine.settle_side_effects_live(a as usize, &mut _ctx) }; assert!(engine.accounts[a as usize].position_basis_q == 0); - assert!(engine.phantom_dust_bound_long_q == 1u128); + assert!(engine.phantom_dust_potential_long_q == 1u128); let _ = { let mut _ctx = InstructionContext::new_with_admission(0, 100); engine.settle_side_effects_live(b as usize, &mut _ctx) }; assert!(engine.accounts[b as usize].position_basis_q == 0); - assert!(engine.phantom_dust_bound_long_q == 2u128); + assert!(engine.phantom_dust_potential_long_q == 2u128); } #[kani::proof] @@ -802,13 +802,13 @@ fn t5_24_dynamic_dust_bound_sufficient() { let mut _ctx = InstructionContext::new_with_admission(0, 100); engine.settle_side_effects_live(a as usize, &mut _ctx) }; - assert!(engine.phantom_dust_bound_long_q == 1u128); + assert!(engine.phantom_dust_potential_long_q == 1u128); let _ = { let mut _ctx = InstructionContext::new_with_admission(0, 100); engine.settle_side_effects_live(b as usize, &mut _ctx) }; - assert!(engine.phantom_dust_bound_long_q == 2u128); + assert!(engine.phantom_dust_potential_long_q == 2u128); } // ############################################################################ @@ -907,7 +907,7 @@ fn t13_56_unilateral_empty_orphan_resolution() { let mut ctx = InstructionContext::new(); engine.stored_pos_count_long = 0; - engine.phantom_dust_bound_long_q = 100u128; + engine.phantom_dust_potential_long_q = 100u128; engine.oi_eff_long_q = 50u128; engine.stored_pos_count_short = 2; @@ -930,7 +930,7 @@ fn t13_57_unilateral_empty_corruption_guard() { let mut ctx = InstructionContext::new(); engine.stored_pos_count_long = 0; - engine.phantom_dust_bound_long_q = 100u128; + engine.phantom_dust_potential_long_q = 100u128; engine.oi_eff_long_q = 50u128; engine.stored_pos_count_short = 2; @@ -948,7 +948,7 @@ fn t13_58_unilateral_empty_short_side() { let mut ctx = InstructionContext::new(); engine.stored_pos_count_short = 0; - engine.phantom_dust_bound_short_q = 200u128; + engine.phantom_dust_potential_short_q = 200u128; engine.oi_eff_short_q = 75u128; engine.stored_pos_count_long = 3; @@ -978,7 +978,7 @@ fn t13_60_unconditional_dust_bound_on_any_a_decay() { engine.oi_eff_short_q = 4 * POS_SCALE; engine.stored_pos_count_long = 1; - let dust_before = engine.phantom_dust_bound_long_q; + let dust_before = engine.phantom_dust_potential_long_q; let result = engine.enqueue_adl(&mut ctx, Side::Short, 2 * POS_SCALE, 0u128); assert!(result.is_ok()); @@ -986,7 +986,7 @@ fn t13_60_unconditional_dust_bound_on_any_a_decay() { // Unconditional: dust ALWAYS increments by at least 1 on A decay assert!( - engine.phantom_dust_bound_long_q >= dust_before + 1, + engine.phantom_dust_potential_long_q >= dust_before + 1, "dust must increment unconditionally on any A_side decay" ); } @@ -1048,9 +1048,9 @@ fn t12_53_adl_truncation_dust_must_not_deadlock() { .checked_sub(eff_a.unsigned_abs()) .unwrap_or(0); - // Verify phantom_dust_bound covers the A-truncation dust + // Verify phantom_dust_potential covers the A-truncation dust assert!( - engine.phantom_dust_bound_long_q >= dust, + engine.phantom_dust_potential_long_q >= dust, "dust bound must cover A-truncation phantom OI" ); @@ -1120,7 +1120,7 @@ fn t14_61_dust_bound_adl_a_truncation_sufficient() { } /// Same-epoch zeroing: when settle_side_effects zeros a position (q_eff_new == 0), -/// the engine must increment phantom_dust_bound by 1. +/// the engine must increment phantom_dust_potential by 1. #[kani::proof] #[kani::solver(cadical)] fn t14_62_dust_bound_same_epoch_zeroing() { @@ -1140,7 +1140,7 @@ fn t14_62_dust_bound_same_epoch_zeroing() { // A_side=1 so floor(1 * 1 / 3) = 0 engine.adl_mult_long = 1; - let dust_before = engine.phantom_dust_bound_long_q; + let dust_before = engine.phantom_dust_potential_long_q; let result = { let mut _ctx = InstructionContext::new_with_admission(0, 100); @@ -1151,10 +1151,10 @@ fn t14_62_dust_bound_same_epoch_zeroing() { // Position must be zeroed assert!(engine.accounts[idx as usize].position_basis_q == 0); // Dust bound must have incremented by 1 - let dust_after = engine.phantom_dust_bound_long_q; + let dust_after = engine.phantom_dust_potential_long_q; assert!( dust_after == dust_before + 1u128, - "same-epoch zeroing must increment phantom_dust_bound by 1" + "same-epoch zeroing must increment phantom_dust_potential by 1" ); } @@ -1203,14 +1203,14 @@ fn t14_63_dust_bound_position_reattach_remainder() { fn t14_64_dust_bound_full_drain_reset_zeroes() { let mut engine = RiskEngine::new(zero_fee_params()); - engine.phantom_dust_bound_long_q = 42u128; + engine.phantom_dust_potential_long_q = 42u128; engine.oi_eff_long_q = 0u128; engine.stored_pos_count_long = 0; engine.adl_epoch_long = 0; engine.begin_full_drain_reset(Side::Long); - assert!(engine.phantom_dust_bound_long_q == 0u128); + assert!(engine.phantom_dust_potential_long_q == 0u128); assert!(engine.oi_eff_long_q == 0u128); } @@ -1265,7 +1265,7 @@ fn t14_65_dust_bound_end_to_end_clearance() { assert!(engine.adl_mult_long == 9); assert!(engine.oi_eff_long_q == 9 * POS_SCALE); assert!(engine.oi_eff_short_q == 9 * POS_SCALE); - assert!(engine.phantom_dust_bound_long_q != 0); + assert!(engine.phantom_dust_potential_long_q != 0); // Settle long accounts to get actual effective positions under new A let sa = { @@ -1287,9 +1287,9 @@ fn t14_65_dust_bound_end_to_end_clearance() { // Dust = tracked OI - actual sum of effective positions let dust = engine.oi_eff_long_q.checked_sub(sum_eff).unwrap_or(0); - // Verify phantom_dust_bound covers the multi-account A-truncation dust + // Verify phantom_dust_potential covers the multi-account A-truncation dust assert!( - engine.phantom_dust_bound_long_q >= dust, + engine.phantom_dust_potential_long_q >= dust, "dust bound must cover A-truncation phantom OI for multiple accounts" ); diff --git a/tests/proofs_invariants.rs b/tests/proofs_invariants.rs index 435627be6..84f9d01c8 100644 --- a/tests/proofs_invariants.rs +++ b/tests/proofs_invariants.rs @@ -1092,3 +1092,59 @@ fn proof_bankrupt_close_state_machine_schema() { "bankrupt-close state-machine schema clear/validate/codec invariants" ); } + +// ============================================================================ +// Wave 6a — phantom-dust 4-field schema (KL-PHANTOM-DUST-SCHEMA-1 REVOKED) +// ============================================================================ + +/// Schema-level invariant `certified <= potential` holds at market genesis +/// and is consumed by `assert_public_postconditions`. On this branch +/// `certified__q` is always 0 (no B-tracking-aware liquidation logic), +/// so the gate trivially passes; when B-tracking lands, this harness will +/// detect any setter that violates the lower-bound ≤ upper-bound contract. +#[kani::proof] +#[kani::unwind(2)] +#[kani::solver(cadical)] +fn proof_phantom_dust_certified_le_potential_at_genesis() { + let engine = RiskEngine::new(zero_fee_params()); + + assert!(engine.phantom_dust_certified_long_q <= engine.phantom_dust_potential_long_q); + assert!(engine.phantom_dust_certified_short_q <= engine.phantom_dust_potential_short_q); + + // On this branch certified is always 0 at genesis. + assert_eq!(engine.phantom_dust_certified_long_q, 0); + assert_eq!(engine.phantom_dust_certified_short_q, 0); + + assert!(engine.assert_public_postconditions().is_ok()); +} + +/// `assert_public_postconditions` rejects any state where certified exceeds +/// potential on either side. Forward-looking: once B-tracking sets +/// `certified` from liquidation step 7, this guards against off-by-one or +/// step-ordering bugs. +#[kani::proof] +#[kani::unwind(2)] +#[kani::solver(cadical)] +fn proof_phantom_dust_certified_gt_potential_rejects() { + let mut engine = RiskEngine::new(zero_fee_params()); + + let side: u8 = kani::any(); + kani::assume(side < 2); + + let certified: u8 = kani::any(); + let potential: u8 = kani::any(); + kani::assume(certified as u128 > potential as u128); + + if side == 0 { + engine.phantom_dust_certified_long_q = certified as u128; + engine.phantom_dust_potential_long_q = potential as u128; + } else { + engine.phantom_dust_certified_short_q = certified as u128; + engine.phantom_dust_potential_short_q = potential as u128; + } + + assert_eq!( + engine.assert_public_postconditions(), + Err(RiskError::CorruptState) + ); +} diff --git a/tests/proofs_liveness.rs b/tests/proofs_liveness.rs index 8ccc0a2fd..db12c29d6 100644 --- a/tests/proofs_liveness.rs +++ b/tests/proofs_liveness.rs @@ -426,7 +426,7 @@ fn proof_unilateral_empty_orphan_dust_clearance() { // Phantom dust: OI == dust bound (should clear) let dust = 42u128; - engine.phantom_dust_bound_long_q = dust; + engine.phantom_dust_potential_long_q = dust; engine.oi_eff_long_q = dust; // OI <= dust bound engine.oi_eff_short_q = dust; // balanced (required by spec) diff --git a/tests/proofs_safety.rs b/tests/proofs_safety.rs index 19eecc070..664c77d0b 100644 --- a/tests/proofs_safety.rs +++ b/tests/proofs_safety.rs @@ -746,7 +746,7 @@ fn t5_23_dust_clearance_guard_safe() { let max_total_dust_base = max_total_dust_fp / (S_POS_SCALE as u16); assert!( max_total_dust_base < n as u16, - "total OI dust < phantom_dust_bound" + "total OI dust < phantom_dust_potential" ); assert!(dust_bound == n, "dust_bound tracks exact zeroing count"); } @@ -2361,8 +2361,8 @@ fn proof_audit4_init_in_place_canonical() { engine.stored_pos_count_short = 11; engine.stale_account_count_long = 3; engine.stale_account_count_short = 4; - engine.phantom_dust_bound_long_q = 50; - engine.phantom_dust_bound_short_q = 60; + engine.phantom_dust_potential_long_q = 50; + engine.phantom_dust_potential_short_q = 60; engine.num_used_accounts = 10; engine.materialized_account_count = 5; engine.last_oracle_price = 9999; @@ -2405,8 +2405,8 @@ fn proof_audit4_init_in_place_canonical() { assert!(engine.stored_pos_count_short == 0); assert!(engine.stale_account_count_long == 0); assert!(engine.stale_account_count_short == 0); - assert!(engine.phantom_dust_bound_long_q == 0); - assert!(engine.phantom_dust_bound_short_q == 0); + assert!(engine.phantom_dust_potential_long_q == 0); + assert!(engine.phantom_dust_potential_short_q == 0); // ---- Account tracking ---- assert!(engine.num_used_accounts == 0);