From 7ef8be769db7c908d1b210694c8ffb53016f5be7 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:23:38 +0100 Subject: [PATCH 1/9] =?UTF-8?q?sync(engine):=20port=20withdraw=5Flive=5Fin?= =?UTF-8?q?surance=5Fnot=5Fatomic=20empty-market=20gate=20=E2=80=94=20clos?= =?UTF-8?q?es=20ENG-PORT-1=20(CRITICAL-5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Empty-market gate from toly upstream (toly-engine:10250-10292) — refuses live insurance withdrawal unless market is provably empty + fully accrued. ADAPTED port: 3 toly-only conditions (active_close_present, stress_consumed_bps_e9_since_envelope, bankruptcy_hmax_lock_active) SKIPPED per KL-FORK-ENGINE-BANKRUPT-CLOSE-1 + KL-FORK-ENGINE-STRESS-ENVELOPE-1 (fork has no such fields). 8 surviving conditions all map to existing fork RiskEngine fields: - oi_eff_long_q == 0 && oi_eff_short_q == 0 (no live OI) - stored_pos_count_long == 0 && stored_pos_count_short == 0 (no stored positions) - stale_account_count_long == 0 && stale_account_count_short == 0 (no stale accounts) - neg_pnl_account_count == 0 (no negative-PnL accounts) - current_slot == last_market_slot (market accrued) Without this gate, an admin holding insurance_authority can drain the live insurance fund while users hold positions whose maintenance margin assumes that insurance is there. With 8 conditions enforced, the fund is only drainable when the market has no live obligations. Cross-ref: ENGINE_BODY_DIFF.md §Vault accounting Hunk 1 (CRITICAL severity), AUDIT_WORK_PRESERVATION.md row 1. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index e502de3b6..f4d82d40d 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -7051,6 +7051,26 @@ impl RiskEngine { return Err(RiskError::Overflow); } self.check_live_accrual_envelope(now_slot)?; + // PORT (ENG-PORT-1 / CRITICAL-5 — empty-market gate): toly upstream + // refuses live-insurance withdrawal unless the market is provably + // empty + fully accrued. ADAPTED port — the 3 toly-only conditions + // (active_close_present, stress_consumed_bps_e9_since_envelope, + // bankruptcy_hmax_lock_active) are SKIPPED per + // KL-FORK-ENGINE-BANKRUPT-CLOSE-1 + KL-FORK-ENGINE-STRESS-ENVELOPE-1 + // — fork has no such fields. The 8 surviving conditions all map to + // existing fork fields and prove the same empty-market invariant + // for fork's narrower schema. + if self.oi_eff_long_q != 0 + || self.oi_eff_short_q != 0 + || self.stored_pos_count_long != 0 + || self.stored_pos_count_short != 0 + || self.stale_account_count_long != 0 + || self.stale_account_count_short != 0 + || self.neg_pnl_account_count != 0 + || self.current_slot != self.last_market_slot + { + return Err(RiskError::Undercollateralized); + } let ins = self.insurance_fund.balance.get(); if amount > ins { return Err(RiskError::InsufficientBalance); From 486381dac0aa72033cdcd44b6256de58a2f66674 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:24:50 +0100 Subject: [PATCH 2/9] =?UTF-8?q?sync(engine):=20port=20account=5Fhas=5Funse?= =?UTF-8?q?ttled=5Flive=5Feffects=20helper=20(ADAPTED=204-predicate=20form?= =?UTF-8?q?)=20=E2=80=94=20ENG-PORT-3=20prerequisite?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds toly's account_has_unsettled_live_effects predicate (toly-engine:4884) as a post-touch invariant detector for sync_account_fee_to_slot_not_atomic, execute_trade, withdraw, convert_released_pnl, and close_account. ADAPTED port per KL-FORK-ENGINE-B-TRACKING-1: toly's 5th predicate (B-snap mismatch via b_target_for_account) is SKIPPED — fork has no B-tracking subsystem. The 4 retained predicates (epoch / A / K / F) catch K/F/A_basis/epoch staleness; the residual narrow case (B drift with epoch/A/K/F in sync) is documented in KL-FORK-ENGINE-B-TRACKING-1. This is the helper-definition commit; callsite wiring (4 callsites) follows in subsequent commits as Port 2 (sync_account_fee) and Port 3-callsites lands on the 4 trade/withdraw/ convert/close paths. Cross-ref: ENGINE_BODY_DIFF.md §execute_trade_not_atomic Hunk 2; AUDIT_WORK_PRESERVATION.md row 3. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index f4d82d40d..be9c0ca9b 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -4903,6 +4903,40 @@ impl RiskEngine { } + test_visible! { + /// PORT (ENG-PORT-3 / CRITICAL-7): post-touch invariant predicate. + /// Returns `Ok(true)` if the account at `idx` carries a non-zero position + /// basis whose epoch / A / K / F snapshots disagree with the side's + /// current aggregates — i.e., touch_account_live_local left the account + /// stale and any downstream mutation (trade, withdraw, close, convert) + /// would operate on inconsistent state. + /// + /// ADAPTED port (KL-FORK-ENGINE-B-TRACKING-1): toly's 5th predicate + /// (`b_snap`/`b_epoch_snap` mismatch via `b_target_for_account`) is + /// SKIPPED here — fork has no B-tracking subsystem. The 4 retained + /// predicates (epoch / A / K / F) catch K/F/A_basis/epoch staleness in + /// every path; the residual narrow case (B drift only, with epoch/A/K/F + /// in sync) is documented in KL-FORK-ENGINE-B-TRACKING-1 as a bounded + /// gap that closes when the B-tracking subsystem ports. + /// + /// Cross-ref: ENGINE_BODY_DIFF.md §execute_trade_not_atomic Hunk 2; + /// AUDIT_WORK_PRESERVATION.md row 3. + fn account_has_unsettled_live_effects(&self, idx: usize) -> Result { + let account = &self.accounts[idx]; + if account.position_basis_q == 0 { + return Ok(false); + } + let side = side_of_i128(account.position_basis_q).ok_or(RiskError::CorruptState)?; + if account.adl_epoch_snap != self.get_epoch_side(side) { + return Ok(true); + } + Ok(account.adl_a_basis != self.get_a_side(side) + || account.adl_k_snap != self.get_k_side(side) + || account.f_snap != self.get_f_side(side)) + } + + } + // ======================================================================== // Account Management // ======================================================================== From 60bedc6395ea4dc8e9c8011617ca97854866f4b9 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:26:01 +0100 Subject: [PATCH 3/9] =?UTF-8?q?sync(engine):=20port=20sync=5Faccount=5Ffee?= =?UTF-8?q?=20loss-safe=20anchor=20+=20ensure=5Ffee=5Fdraw=5Fdoes=5Fnot=5F?= =?UTF-8?q?precede=5Floss=20helper=20=E2=80=94=20closes=20ENG-PORT-2=20(CR?= =?UTF-8?q?ITICAL-6)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the loss-juniority bug in sync_account_fee_to_slot_not_atomic. Without these changes, the fee cursor could advance past last_market_slot and charge fees for slots the market hasn't accrued through, ranking the fee draw senior to losses that should have been booked first. Three sub-changes: 1. New helper ensure_fee_draw_does_not_precede_loss (toly-engine equivalent): - Rejects with Undercollateralized if pnl < 0 (realized loss already on the account) - On Live, also rejects if account_has_unsettled_live_effects (epoch/A/K/F drift — unrealized loss not yet booked). ADAPTED 4-predicate form per KL-FORK-ENGINE-B-TRACKING-1; B-snap predicate dropped (no fork B-tracking subsystem). 2. live_loss_safe_anchor block in sync_account_fee_to_slot_not_atomic: - When Live + now_slot > last_market_slot + account holds position basis, anchor to last_market_slot instead of now_slot. - Threaded through both shape_anchor (validation) and the final commit anchor. 3. Loss-juniority guard call when fee_rate_per_slot > 0 && shape_anchor > last_fee_slot. Plus a defensive narrowing of the live envelope check to fire only on now_slot > current_slot (avoids redundant envelope check on repeated same-slot fee syncs). Cross-ref: ENGINE_BODY_DIFF.md §sync_account_fee_to_slot_not_atomic (CRITICAL severity); AUDIT_WORK_PRESERVATION.md row 2. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 53 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 50 insertions(+), 3 deletions(-) diff --git a/src/percolator.rs b/src/percolator.rs index be9c0ca9b..a09ed772a 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -4937,6 +4937,28 @@ impl RiskEngine { } + test_visible! { + /// PORT (ENG-PORT-2 / CRITICAL-6): rejects a fee-draw that would rank + /// senior to an unrealized loss on the same account. Two checks: + /// (a) account already has realized negative PnL — fees must wait, + /// (b) on Live, the account has unsettled K/F/A_basis/epoch state — + /// a fee draw at the current cursor would assume settled losses + /// that haven't yet been booked. + /// + /// Pure SF port — no schema dependency. Toly source: toly-engine + /// (within sync_account_fee_to_slot_not_atomic body). + fn ensure_fee_draw_does_not_precede_loss(&self, idx: usize) -> Result<()> { + if self.accounts[idx].pnl < 0 { + return Err(RiskError::Undercollateralized); + } + if self.market_mode == MarketMode::Live && self.account_has_unsettled_live_effects(idx)? { + return Err(RiskError::Undercollateralized); + } + Ok(()) + } + + } + // ======================================================================== // Account Management // ======================================================================== @@ -7286,22 +7308,47 @@ impl RiskEngine { if now_slot < self.current_slot { return Err(RiskError::Overflow); } + // PORT (ENG-PORT-2 / CRITICAL-6): loss-safe fee anchor. + // When market is Live, now_slot is ahead of last_market_slot, and the + // account holds a non-zero position basis, the fee draw must use + // last_market_slot (not now_slot) as its shape/anchor — otherwise the + // fee would charge for slots the market hasn't accrued through, ranking + // ahead of unrealized losses on those same slots. + let live_loss_safe_anchor = if self.market_mode == MarketMode::Live + && now_slot > self.last_market_slot + && (idx as usize) < MAX_ACCOUNTS + && self.accounts[idx as usize].position_basis_q != 0 + { + self.last_market_slot + } else { + now_slot + }; let shape_anchor = match self.market_mode { - MarketMode::Live => now_slot, + MarketMode::Live => live_loss_safe_anchor, MarketMode::Resolved => self.resolved_slot, }; self.validate_touched_account_shape_at_fee_slot(idx as usize, shape_anchor)?; + // PORT (ENG-PORT-2 / CRITICAL-6): loss-juniority guard. + // Whenever the fee cursor would advance past the account's last_fee_slot + // and we're charging a non-zero rate, refuse if the account holds either + // realized negative PnL OR (on Live) unsettled K/F/A_basis/epoch state. + if fee_rate_per_slot > 0 && shape_anchor > self.accounts[idx as usize].last_fee_slot { + self.ensure_fee_draw_does_not_precede_loss(idx as usize)?; + } // Reject time jumps that would brick subsequent accrue_market_to. // Only meaningful on Live; on Resolved the envelope is moot because // accrue_market_to is no longer reachable, but the check is safe // (last_market_slot is frozen to resolved_slot). - if self.market_mode == MarketMode::Live { + // PORT: gate the envelope check on now_slot > current_slot — if no + // time advance, no envelope to check (avoids a redundant call when + // sync_account_fee is invoked at the same slot multiple times). + if self.market_mode == MarketMode::Live && now_slot > self.current_slot { self.check_live_accrual_envelope(now_slot)?; } let anchor = match self.market_mode { MarketMode::Live => { self.current_slot = now_slot; - self.current_slot + live_loss_safe_anchor } MarketMode::Resolved => { // Resolved fee sync is anchored at resolution. From 61938f2d1c4531934df3de65fd0df3f8bf5f4e31 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:28:12 +0100 Subject: [PATCH 4/9] =?UTF-8?q?sync(engine):=20wire=20account=5Fhas=5Funse?= =?UTF-8?q?ttled=5Flive=5Feffects=20at=204=20callsites=20=E2=80=94=20close?= =?UTF-8?q?s=20ENG-PORT-3=20(CRITICAL-7)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the post-touch invariant guard at 4 fork-engine entrypoints that mutate account state through touch_account_live_local. Each guard rejects with Undercollateralized before any downstream mutation that would otherwise operate on stale K/F/A_basis/epoch. - execute_trade_not_atomic: both counterparties checked after the dual touch (Step 11). Prevents trade attaching at stale basis when a side mode change post-touch leaves K/F drifted. - withdraw_not_atomic: post-touch, before finalize_touched (which sweeps fees against capital using current K/F). - convert_released_pnl_not_atomic: post-touch, before convert_released_pnl_core mutates released-PnL bookkeeping. - close_account_not_atomic: post-touch, before effective_pos_q_checked (which derives from A_basis/K snaps) is used in the position==0 check. Defense-in-depth post-touch invariant — does not fire on any current happy-path because touch_account_live_local correctly settles snaps. Catches regressions in the touch machinery before they propagate to the trade/withdraw/convert/close mutation paths. ADAPTED 4-predicate form per KL-FORK-ENGINE-B-TRACKING-1; B-snap predicate absent (no fork B-tracking subsystem). Residual narrow case (B drift with epoch/A/K/F in sync) closes when the B-tracking subsystem ports. Cross-ref: ENGINE_BODY_DIFF.md §execute_trade_not_atomic Hunk 2 (HIGH severity); AUDIT_WORK_PRESERVATION.md row 3. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index a09ed772a..8d30ad3d8 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -5121,6 +5121,14 @@ impl RiskEngine { // Step 3: live local touch self.touch_account_live_local(idx as usize, &mut ctx)?; + // PORT (ENG-PORT-3 / CRITICAL-7): post-touch invariant guard. + // Withdraw must reject if the account's snaps disagree with the side's + // current aggregates after touch — finalize_touched would otherwise + // sweep fees against capital based on stale K/F. + if self.account_has_unsettled_live_effects(idx as usize)? { + return Err(RiskError::Undercollateralized); + } + // Finalize touched (whole-only conversion + fee sweep) self.finalize_touched_accounts_post_live(&ctx)?; @@ -5335,6 +5343,16 @@ impl RiskEngine { self.touch_account_live_local(first as usize, &mut ctx)?; self.touch_account_live_local(second as usize, &mut ctx)?; + // PORT (ENG-PORT-3 / CRITICAL-7): post-touch invariant guard. + // Verify both counterparties are settled (epoch / A / K / F snaps + // match side aggregates) before any trade-body mutation. ADAPTED + // 4-predicate form per KL-FORK-ENGINE-B-TRACKING-1. + if self.account_has_unsettled_live_effects(a as usize)? + || self.account_has_unsettled_live_effects(b as usize)? + { + return Err(RiskError::Undercollateralized); + } + // Step 12a: flush dust-only empty sides before computing // bilateral_oi_after. A touch that hits the "q_eff_new == 0" dust // branch zeros the account basis and decrements stored_pos_count @@ -6410,6 +6428,13 @@ impl RiskEngine { // Step 3: live local touch (no auto-convert, no finalize yet) self.touch_account_live_local(idx as usize, &mut ctx)?; + // PORT (ENG-PORT-3 / CRITICAL-7): post-touch invariant guard. + // Reject if convert would mutate released-PnL bookkeeping based on + // stale K/F/A_basis/epoch. + if self.account_has_unsettled_live_effects(idx as usize)? { + return Err(RiskError::Undercollateralized); + } + // Steps 4-10 happen before finalize so auto-convert cannot consume // the user's released PnL before they can request it. self.convert_released_pnl_core(idx as usize, x_req, oracle_price)?; @@ -6458,6 +6483,15 @@ impl RiskEngine { self.accrue_market_to(now_slot, oracle_price, funding_rate_e9)?; self.current_slot = now_slot; self.touch_account_live_local(idx as usize, &mut ctx)?; + + // PORT (ENG-PORT-3 / CRITICAL-7): post-touch invariant guard. + // Close must reject if effective_pos_q would be computed from stale + // A_basis/K/F (the next line uses effective_pos_q_checked which derives + // from those snaps). + if self.account_has_unsettled_live_effects(idx as usize)? { + return Err(RiskError::Undercollateralized); + } + self.finalize_touched_accounts_post_live(&ctx)?; // Position must be zero From 0206a590f8d60beb7e46573b84575cc456b9caec Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:30:50 +0100 Subject: [PATCH 5/9] =?UTF-8?q?sync(engine):=20port=20enforce=5Fside=5Fmod?= =?UTF-8?q?e=5Foi=5Fgate=20per-account=20widening=20+=20new=20account=5Fga?= =?UTF-8?q?te=20helper=20=E2=80=94=20closes=20ENG-PORT-4=20(CRITICAL-8)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the maker-replaces-taker hazard in enforce_side_mode_oi_gate. The pre-port aggregate-OI gate alone admits a trade where one counterparty closes long (releasing OI) while the other opens long (consuming the same OI) — net aggregate OI change is zero, so the side-mode (DrainOnly / ResetPending) check passes, even though a NEW account just landed on a side mid-reset. Three sub-changes (toly-engine equivalent at toly-engine:8021-8063): 1. New helper enforce_side_mode_account_gate(old_eff, new_eff). Verbatim port. Rejects any new entrant onto a ResetPending side regardless of OI movement; on DrainOnly, rejects unless the account is reducing its existing same-side basis. 2. enforce_side_mode_oi_gate widens to 6-arg signature with per-account positions (old_eff_a, new_eff_a, old_eff_b, new_eff_b, oi_long_after, oi_short_after). Body keeps the existing aggregate-OI checks AND adds the account-gate calls for both counterparties. 3. The single execute_trade_not_atomic callsite now passes the per-account positions captured earlier in the trade flow. The gate is additive: it widens what gets rejected without weakening what gets accepted. All happy paths are unaffected. Test callsites in tests/proofs_*.rs (#![cfg(kani)]-gated) need the 4-arg expansion — follow-up commit "ENG-PORT-4 fixup" updates them. Cross-ref: ENGINE_BODY_DIFF.md §enforce_side_mode_oi_gate Hunk 1 (HIGH severity); AUDIT_WORK_PRESERVATION.md row 4. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 54 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 52 insertions(+), 2 deletions(-) diff --git a/src/percolator.rs b/src/percolator.rs index 8d30ad3d8..e7de9c3fe 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -5447,8 +5447,18 @@ impl RiskEngine { return Err(RiskError::Overflow); } - // Reject if trade would increase OI on a blocked side. - self.enforce_side_mode_oi_gate(oi_long_after, oi_short_after)?; + // Reject if trade would increase OI on a blocked side OR land a fresh + // entrant on a gated side. PORT (ENG-PORT-4 / CRITICAL-8) — widened + // 6-arg signature threads per-account positions through to the + // account-gate, closing the maker-replaces-taker hazard. + self.enforce_side_mode_oi_gate( + old_eff_a, + new_eff_a, + old_eff_b, + new_eff_b, + oi_long_after, + oi_short_after, + )?; // Spec §1.4: per-side active-position cap. Pre-validate the NET // delta across BOTH legs so a valid position swap at the cap @@ -5672,8 +5682,46 @@ impl RiskEngine { } test_visible! { + /// PORT (ENG-PORT-4 / CRITICAL-8): per-account side-mode entrant gate. + /// Rejects any new entrant onto a ResetPending side regardless of OI + /// movement; on DrainOnly, rejects unless the account is reducing its + /// existing same-side basis. Closes the maker-replaces-taker hazard + /// where aggregate OI is flat but a fresh OI lands on a gated side. + fn enforce_side_mode_account_gate(&self, old_eff: i128, new_eff: i128) -> Result<()> { + if new_eff == 0 { + return Ok(()); + } + let side = side_of_i128(new_eff).ok_or(RiskError::CorruptState)?; + match self.get_side_mode(side) { + SideMode::Normal => Ok(()), + SideMode::ResetPending => Err(RiskError::SideBlocked), + SideMode::DrainOnly => { + let old_same_side = side_of_i128(old_eff) == Some(side); + if old_same_side && new_eff.unsigned_abs() <= old_eff.unsigned_abs() { + Ok(()) + } else { + Err(RiskError::SideBlocked) + } + } + } + } + } + + test_visible! { + /// PORT (ENG-PORT-4 / CRITICAL-8): widened to 6-arg signature with + /// per-account positions. The pre-port aggregate-OI gate alone admits + /// a trade where one counterparty closes long (releasing OI) while + /// the other opens long (consuming the same OI) — net aggregate OI + /// change is zero, so the side-mode (DrainOnly / ResetPending) check + /// passes, even though a NEW account just landed on a side mid-reset. + /// Threading per-account old/new effective positions into the gate + /// closes that hazard via enforce_side_mode_account_gate. fn enforce_side_mode_oi_gate( &self, + old_eff_a: i128, + new_eff_a: i128, + old_eff_b: i128, + new_eff_b: i128, oi_long_after: u128, oi_short_after: u128, ) -> Result<()> { @@ -5687,6 +5735,8 @@ impl RiskEngine { { return Err(RiskError::SideBlocked); } + self.enforce_side_mode_account_gate(old_eff_a, new_eff_a)?; + self.enforce_side_mode_account_gate(old_eff_b, new_eff_b)?; Ok(()) } } From e2f1c67c9b94ad174770975a9ffbcfc65084c3b3 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:32:24 +0100 Subject: [PATCH 6/9] =?UTF-8?q?test(audit):=20update=209=20enforce=5Fside?= =?UTF-8?q?=5Fmode=5Foi=5Fgate=20callsites=20for=206-arg=20signature=20?= =?UTF-8?q?=E2=80=94=20ENG-PORT-4=20fixup?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mechanical update — ENG-PORT-4 widened the gate signature from 2-arg (oi_long_after, oi_short_after) to 6-arg (old_eff_a, new_eff_a, old_eff_b, new_eff_b, oi_long_after, oi_short_after). Without these test updates the engine library still builds clean, but proofs_*.rs Kani harnesses fail to compile. - proofs_invariants.rs:580/585/594/599/607 (proof_side_mode_gating): pass 0i128 per-account positions; the test isolates the aggregate-OI gate, and the per-account gate is a no-op when new_eff == 0. - proofs_instructions.rs:596: pass per-account positions in (b, a) order matching the bilateral_oi_after call directly above. - proofs_liveness.rs:69, 79: pass (old_a, new_a, old_b, new_b) in scope. - proofs_checklist.rs:393: pass (eff_a_before, new_eff_a, eff_b_before, new_eff_b) in scope. Verification: - cargo build --release: clean (lib unchanged from ENG-PORT-4 production commit). - Kani build verification deferred to the post-port verification gate (cargo kani --workspace, run after all 7 ports + cleanup commit). Cross-ref: AUDIT_WORK_PRESERVATION.md row 5 (the original 38b551e fixup commit had a 4-file pattern; this fixup matches plus adds proofs_checklist.rs:393 which the prior session also touched). Co-Authored-By: Claude Opus 4.7 (1M context) --- tests/proofs_checklist.rs | 4 +++- tests/proofs_instructions.rs | 4 +++- tests/proofs_invariants.rs | 13 ++++++++----- tests/proofs_liveness.rs | 5 +++-- 4 files changed, 17 insertions(+), 9 deletions(-) diff --git a/tests/proofs_checklist.rs b/tests/proofs_checklist.rs index 608474114..a44601b04 100644 --- a/tests/proofs_checklist.rs +++ b/tests/proofs_checklist.rs @@ -390,7 +390,9 @@ fn proof_g4_drain_only_blocks_oi_increase() { "G4 setup must be an OI-increasing long-side trade" ); - let result = engine.enforce_side_mode_oi_gate(oi_long_after, oi_short_after); + // ENG-PORT-4 fixup: 6-arg signature. Pass (eff_a_before, new_eff_a, eff_b_before, + // new_eff_b) in scope, matching the bilateral_oi_after call earlier in the test. + let result = engine.enforce_side_mode_oi_gate(eff_a_before, new_eff_a, eff_b_before, new_eff_b, oi_long_after, oi_short_after); match result { Err(RiskError::SideBlocked) => {} _ => assert!( diff --git a/tests/proofs_instructions.rs b/tests/proofs_instructions.rs index da5d3dece..8bdb21e81 100644 --- a/tests/proofs_instructions.rs +++ b/tests/proofs_instructions.rs @@ -592,8 +592,10 @@ fn t11_50_execute_trade_atomic_oi_update_sign_flip() { .unwrap(); assert!(oi_long_after == POS_SCALE); assert!(oi_short_after == POS_SCALE); + // ENG-PORT-4 fixup: 6-arg signature. Pass per-account positions in + // (b, a) order to match the bilateral_oi_after call directly above. engine - .enforce_side_mode_oi_gate(oi_long_after, oi_short_after) + .enforce_side_mode_oi_gate(old_eff_b, new_eff_b, old_eff_a, new_eff_a, oi_long_after, oi_short_after) .unwrap(); engine .attach_effective_position(b as usize, new_eff_b) diff --git a/tests/proofs_invariants.rs b/tests/proofs_invariants.rs index e07fd99d9..79def6c95 100644 --- a/tests/proofs_invariants.rs +++ b/tests/proofs_invariants.rs @@ -576,13 +576,16 @@ fn proof_side_mode_gating() { engine.oi_eff_short_q = oi; // DrainOnly blocks OI increases on its side but permits non-increasing candidates. + // ENG-PORT-4 fixup: 6-arg signature. Pass 0i128 per-account positions — + // the per-account gate is a no-op when new_eff == 0; this proof isolates + // the aggregate-OI gate. engine.side_mode_long = SideMode::DrainOnly; - let long_inc = engine.enforce_side_mode_oi_gate(oi + POS_SCALE, oi); + let long_inc = engine.enforce_side_mode_oi_gate(0, 0, 0, 0, oi + POS_SCALE, oi); assert!( long_inc == Err(RiskError::SideBlocked), "DrainOnly long side must block long OI increases" ); - let long_same = engine.enforce_side_mode_oi_gate(oi, oi); + let long_same = engine.enforce_side_mode_oi_gate(0, 0, 0, 0, oi, oi); assert!( long_same.is_ok(), "DrainOnly long side must permit non-increasing long OI" @@ -591,12 +594,12 @@ fn proof_side_mode_gating() { // ResetPending has the same OI-increase gate. engine.side_mode_long = SideMode::Normal; engine.side_mode_short = SideMode::ResetPending; - let short_inc = engine.enforce_side_mode_oi_gate(oi, oi + POS_SCALE); + let short_inc = engine.enforce_side_mode_oi_gate(0, 0, 0, 0, oi, oi + POS_SCALE); assert!( short_inc == Err(RiskError::SideBlocked), "ResetPending short side must block short OI increases" ); - let short_same = engine.enforce_side_mode_oi_gate(oi, oi); + let short_same = engine.enforce_side_mode_oi_gate(0, 0, 0, 0, oi, oi); assert!( short_same.is_ok(), "ResetPending short side must permit non-increasing short OI" @@ -604,7 +607,7 @@ fn proof_side_mode_gating() { // Normal mode does not block side OI increases at this gate. engine.side_mode_short = SideMode::Normal; - let normal_inc = engine.enforce_side_mode_oi_gate(oi + POS_SCALE, oi + POS_SCALE); + let normal_inc = engine.enforce_side_mode_oi_gate(0, 0, 0, 0, oi + POS_SCALE, oi + POS_SCALE); assert!( normal_inc.is_ok(), "Normal side mode must not block OI increases at the side-mode gate" diff --git a/tests/proofs_liveness.rs b/tests/proofs_liveness.rs index c0b998e96..8342787bc 100644 --- a/tests/proofs_liveness.rs +++ b/tests/proofs_liveness.rs @@ -66,7 +66,8 @@ fn t11_44_trade_path_reopens_ready_reset_side() { assert!( engine - .enforce_side_mode_oi_gate(oi_long_after, oi_short_after) + // ENG-PORT-4 fixup: 6-arg signature. Per-account positions in scope. + .enforce_side_mode_oi_gate(old_a, new_a, old_b, new_b, oi_long_after, oi_short_after) .is_err(), "ready ResetPending side must block OI increase before preflight finalization" ); @@ -76,7 +77,7 @@ fn t11_44_trade_path_reopens_ready_reset_side() { assert!(engine.side_mode_long == SideMode::Normal); assert!( engine - .enforce_side_mode_oi_gate(oi_long_after, oi_short_after) + .enforce_side_mode_oi_gate(old_a, new_a, old_b, new_b, oi_long_after, oi_short_after) .is_ok(), "trade preflight must reopen a fully ready ResetPending side before OI gating" ); From fe1d6fded104513b8b2dde0ac877c9610e86c141 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:33:50 +0100 Subject: [PATCH 7/9] =?UTF-8?q?sync(engine):=20port=20resolve=5Fmarket=5Fn?= =?UTF-8?q?ot=5Fatomic=204=20SF=20hunks=20(pre-state,=20K-zero,=20dust-zer?= =?UTF-8?q?o=20ADAPTED,=20drain-guard)=20=E2=80=94=20closes=20ENG-PORT-5a?= =?UTF-8?q?=20(CRITICAL-9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 4 SF hunks from toly upstream's resolve_market_not_atomic body (toly-engine:9518-9674). 2 sibling toly hunks (ensure_no_active_bankrupt_close, clear_stress_envelope) are SKIPPED per KL parents — fork has neither subsystem. Hunks ported: 1. Hunk 2 — pre-state snapshot. 8 locals (pre_mode_long/short, pre_a_long/short, pre_oi_long/short, pre_stored_long/short) capture the pre-resolve view BEFORE any mutation. Downstream gates read snapshots so per-side decisions reflect the pre-resolve state. 2. Hunk 3 — K-terminal-delta zero-on-zero-OI. A side with no pre-resolve OI cannot accumulate a non-zero terminal delta (would attribute a settlement shift to non-existent positions). Forces delta to 0 when pre_oi_ == 0. 3. Hunk 5 — phantom-dust zero on pre_stored_ == 0. ADAPTED to fork's single-bound schema per KL-PHANTOM-DUST-SCHEMA-1 (toly uses certified+ potential pair; fork uses single-bound phantom_dust_bound__q). Semantically equivalent: no stored positions ⇒ no dust to track. 4. Hunk 6 — drain-reset pre_stored guard. Only enter drain reset when pre_stored_ > 0. The pre-port code unconditionally entered drain even on sides with zero stored positions, performing spurious side-mode transitions. Hunks SKIPPED (per parent KL — see KEEP_LIST): - Hunk 1 (ensure_no_active_bankrupt_close) — KL-FORK-ENGINE-BANKRUPT-CLOSE-1 (no fork bankrupt-close subsystem; deferred to ENG-PORT-5b). - Hunk 4 (clear_stress_envelope) — KL-FORK-ENGINE-STRESS-ENVELOPE-1 (no fork stress-envelope subsystem; deferred to ENG-PORT-5b). Cross-ref: ENGINE_BODY_DIFF.md §resolve_market_not_atomic Hunks 2/3/5/6 (SECURITY-FORWARD HIGH/MEDIUM); AUDIT_WORK_PRESERVATION.md row 6. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 50 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/src/percolator.rs b/src/percolator.rs index e7de9c3fe..b373db9bd 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -6682,21 +6682,39 @@ impl RiskEngine { } } + // PORT (ENG-PORT-5a / CRITICAL-9 — Hunk 2): pre-state snapshot. + // Capture the pre-resolve view BEFORE any mutation. The K-terminal-delta + // gate, phantom-dust zero predicate, and drain-finalize gates below all + // read these snapshots so per-side decisions reflect the pre-resolve + // state, not the in-mutation state. + let pre_mode_long = self.side_mode_long; + let pre_mode_short = self.side_mode_short; + let pre_a_long = self.adl_mult_long; + let pre_a_short = self.adl_mult_short; + let pre_oi_long = self.oi_eff_long_q; + let pre_oi_short = self.oi_eff_short_q; + let pre_stored_long = self.stored_pos_count_long; + let pre_stored_short = self.stored_pos_count_short; + // Step 8: compute resolved terminal mark deltas in exact signed arithmetic. // These deltas carry the settlement shift WITHOUT adding to persistent K_side, // so resolution can succeed even near K headroom (spec §9.7 step 8). + // PORT (ENG-PORT-5a / CRITICAL-9 — Hunk 3): K-terminal-delta zero-on-zero-OI. + // A side with no pre-resolve OI cannot accumulate a non-zero terminal delta — + // it would attribute a settlement shift to non-existent positions. Forces + // the delta to 0 when pre_oi_ == 0, regardless of side mode. let price_diff = resolved_price as i128 - live_oracle_price as i128; - let resolved_k_long_td = if self.side_mode_long == SideMode::ResetPending { + let resolved_k_long_td = if pre_mode_long == SideMode::ResetPending || pre_oi_long == 0 { 0i128 } else { - checked_u128_mul_i128(self.adl_mult_long, price_diff)? + checked_u128_mul_i128(pre_a_long, price_diff)? }; - let resolved_k_short_td = if self.side_mode_short == SideMode::ResetPending { + let resolved_k_short_td = if pre_mode_short == SideMode::ResetPending || pre_oi_short == 0 { 0i128 } else { // Short side: negative of price_diff let neg_price_diff = price_diff.checked_neg().ok_or(RiskError::Overflow)?; - checked_u128_mul_i128(self.adl_mult_short, neg_price_diff)? + checked_u128_mul_i128(pre_a_short, neg_price_diff)? }; // Steps 8-13: set resolved state @@ -6720,11 +6738,31 @@ impl RiskEngine { self.oi_eff_long_q = 0; 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. + if pre_stored_long == 0 { + self.phantom_dust_bound_long_q = 0u128; + } + if pre_stored_short == 0 { + self.phantom_dust_bound_short_q = 0u128; + } + // Steps 17-20: drain/finalize sides - if self.side_mode_long != SideMode::ResetPending { + // PORT (ENG-PORT-5a / CRITICAL-9 — Hunk 6): drain-reset pre_stored guard. + // Only enter drain reset when pre_stored_ > 0 — i.e. there are + // positions to drain. The pre-port code unconditionally entered drain + // even on sides with zero stored positions, performing spurious side-mode + // transitions and bumping sweep_generation. + if pre_mode_long != SideMode::ResetPending && pre_stored_long > 0 { self.begin_full_drain_reset(Side::Long)?; } - if self.side_mode_short != SideMode::ResetPending { + if pre_mode_short != SideMode::ResetPending && pre_stored_short > 0 { self.begin_full_drain_reset(Side::Short)?; } if self.side_mode_long == SideMode::ResetPending From 7d7689f0ba0c4aa329e8ff9cee5bda0dc3f19844 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:35:28 +0100 Subject: [PATCH 8/9] =?UTF-8?q?sync(engine):=20port=20force=5Fclose=5Freso?= =?UTF-8?q?lved=5Fnot=5Fatomic=20position-basis=20early-return=20=E2=80=94?= =?UTF-8?q?=20closes=20Port=206?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SF guard from toly upstream's force_close_resolved_with_fee_not_atomic body. Refuses terminal close when reconcile_resolved_not_atomic left position_basis_q non-zero — guards against partial-progress reconcile (e.g., social loss spread that didn't fully unwind basis). Without this guard, close_resolved_terminal_not_atomic silently mis-accounts the residual, OR fails later in a less recoverable way. Toly's matching fee-charging line (sync_account_fee_to_slot at resolved_slot) is FEATURE-DIVERGENCE per ENGINE_BODY_DIFF Hunk 3 — SKIPPED. Fork doesn't charge maintenance fees at resolved close. Cross-ref: ENGINE_BODY_DIFF.md §force_close_resolved_not_atomic Hunk 2 (SECURITY-FORWARD HIGH); audit-validated independent of bankruptcy/stress/active-close subsystems. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/percolator.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/percolator.rs b/src/percolator.rs index b373db9bd..82558b6bc 100644 --- a/src/percolator.rs +++ b/src/percolator.rs @@ -6802,6 +6802,24 @@ impl RiskEngine { // Finalize any sides that are fully ready for reopening self.maybe_finalize_ready_reset_sides(); + + // PORT (ENG-PORT-6 / Port 6 — SF guard): position-basis early-return. + // Refuse to attempt terminal close when the account still has non-zero + // position_basis_q after reconcile_resolved_not_atomic ran — guards + // against the case where reconcile partially progressed (e.g., social + // loss spread didn't fully unwind basis). Without this, the next call + // (close_resolved_terminal_not_atomic) expects basis == 0 and may fail + // later in a less recoverable way, OR silently mis-account because the + // close path zeros basis without realizing the residual. + // The matching toly-side fee-charging line + // (sync_account_fee_to_slot(i, resolved_slot, fee_rate_per_slot)) + // is FEATURE-DIVERGENCE — fork doesn't charge maintenance fees at + // resolved close. SKIP per ENGINE_BODY_DIFF §force_close_resolved_not_atomic + // Hunk 3 (FEATURE-DIVERGENCE MEDIUM). + if self.accounts[i].position_basis_q != 0 { + return Ok(ResolvedCloseResult::ProgressOnly); + } + self.assert_public_postconditions()?; // pnl <= 0: can close immediately (loser/zero — no payout gate) From dac8bf61fe949ebc609a660b4e356a4315a37ec0 Mon Sep 17 00:00:00 2001 From: dcccrypto Date: Sun, 10 May 2026 01:37:33 +0100 Subject: [PATCH 9/9] =?UTF-8?q?chore(engine):=20remove=20last=5Fcrank=5Fsl?= =?UTF-8?q?ot=20+=20gc=5Fcursor=20refs=20from=20detailed=5Foffsets.rs=20ex?= =?UTF-8?q?ample=20=E2=80=94=20restore=20cargo=20test=20clean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pre-existing build break in fork-only example examples/detailed_offsets.rs (added in 9340977 "chore: add detailed_offsets example for layout verification"). Both fields were removed without rename in the v12.1 sync (9a1c627 + 84a9293): - last_crank_slot retired; conceptually replaced by last_market_slot (already printed on a separate line in this file) - gc_cursor retired in 84a9293 ("Simplify ADL: replace windowed crank with full-scan") Cleanest fix per Phase 0 baseline analysis: delete the 2 broken lines, leaving the rest of the example intact (it correctly references current RiskEngine fields incl. fork-only phantom_dust_bound__q, materialized_account_count, etc.). Restores `cargo test --features test` to clean (was failing at compile due to E0609 errors in the example), so the post-Phase-1 verification gate uses the standard SESSION_START_CHECKLIST baseline command without the --lib --tests workaround. Per BULK_SYNC_PLAN.md Phase 0 finding #3: applied as final cleanup commit on the sync branch before push. Co-Authored-By: Claude Opus 4.7 (1M context) --- examples/detailed_offsets.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/detailed_offsets.rs b/examples/detailed_offsets.rs index 7880e6d85..8ce62e381 100644 --- a/examples/detailed_offsets.rs +++ b/examples/detailed_offsets.rs @@ -41,11 +41,11 @@ fn main() { println!("resolved_k_long_terminal_delta:{}", offset_of!(RiskEngine, resolved_k_long_terminal_delta)); println!("resolved_k_short_terminal_delta:{}", offset_of!(RiskEngine, resolved_k_short_terminal_delta)); println!("resolved_live_price:{}", offset_of!(RiskEngine, resolved_live_price)); - println!("last_crank_slot:{}", offset_of!(RiskEngine, last_crank_slot)); + // last_crank_slot was renamed → see last_market_slot lower in this file. + // gc_cursor was retired in v12.1 (84a9293 "Simplify ADL: replace windowed crank with full-scan"). println!("c_tot:{}", offset_of!(RiskEngine, c_tot)); println!("pnl_pos_tot:{}", offset_of!(RiskEngine, pnl_pos_tot)); println!("pnl_matured_pos_tot:{}", offset_of!(RiskEngine, pnl_matured_pos_tot)); - println!("gc_cursor:{}", offset_of!(RiskEngine, gc_cursor)); println!("adl_mult_long:{}", offset_of!(RiskEngine, adl_mult_long)); println!("adl_mult_short:{}", offset_of!(RiskEngine, adl_mult_short)); println!("adl_coeff_long:{}", offset_of!(RiskEngine, adl_coeff_long));