audit: engine critical bundle (closes C-5/6/7/8/9) - #89
Closed
dcccrypto wants to merge 9 commits into
Closed
Conversation
…delta + adapted phantom-dust zero (ENG-PORT-5a) ENG-PORT-5a — engine-side completion of CRITICAL-9, paired with PORT-1 wrapper bundle. Closes the four security gaps the deep audit identified in `resolve_market_not_atomic`: 1. Pre-state snapshots (toly-engine:9590-9597). 8 locals capture the pre-resolve view BEFORE any mutation; K-terminal-delta and drain-finalize gates now read snapshots so per-side decisions reflect the pre-resolve state. 2. K-terminal-delta zero-on-zero-OI (toly-engine:9603). A side with no pre-resolve OI cannot accumulate a non-zero terminal delta (would attribute a settlement shift to non-existent positions). 3. Phantom-dust zero on `pre_stored_<side> == 0` (toly-engine:9637-9644). ADAPTED to fork's single-bound schema per KL-PHANTOM-DUST-SCHEMA-1 — fork has `phantom_dust_bound_<side>_q` (one field), toly has certified/potential pair (four fields). Semantically equivalent: no stored positions ⇒ no dust to track. 4. Drain guard `pre_stored_<side> > 0` on `begin_full_drain_reset` (toly-engine:9647-9652). A side that already had no stored positions never enters the drain path. Out of scope (deferred to ENG-PORT-5b): - `ensure_no_active_bankrupt_close()` — fork-engine has no `active_close_present` field (KL-FORK-ENGINE-BANKRUPT-CLOSE-1). - `clear_stress_envelope()` — fork-engine has only `stress_reset_pending: u8`, not the full stress-envelope subsystem (KL-FORK-ENGINE-STRESS-ENVELOPE-1). Both deferral sites are documented inline. Tests: - 2 new Kani harnesses in tests/proofs_audit.rs: - `kani_resolve_market_terminal_drain` (Ordinary path) - `kani_resolve_market_terminal_drain_degenerate` (Degenerate path) Both verified SUCCESSFUL: 0 of 3524 checks failed, 4.77s. - 287/287 unit tests still pass (incl. all 9 existing resolve_market_*). - Regression-checked existing resolve harnesses: - proof_force_close_resolved_with_position_conserves: 0/4722 failures - proof_force_close_resolved_flat_returns_capital: 0/4700 failures KEEP_LIST entries added in `~/wrapper-engine-deep-audit/KEEP_LIST.md`: - KL-PHANTOM-DUST-SCHEMA-1 - KL-FORK-ENGINE-BANKRUPT-CLOSE-1 - KL-FORK-ENGINE-STRESS-ENVELOPE-1 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…mic (ENG-PORT-1, CRITICAL-5) Closes the admin-callable insurance siphon. Without this gate the wrapper- authorized live insurance withdrawal accepts any amount the wrapper signs off on, even while open positions, stale accounts, or pending negative PnL exists — the engine's vault accounting trusts the wrapper's "is the market exposed" judgment. That trust is misplaced because the wrapper authorization in tag 22/23 (insurance_operator + cooldown + bps mask) operates on rate-limit semantics, not exposure semantics. Ports the SUBSET of toly's 11-condition gate that maps onto existing fork-engine state (8 of 11): - oi_eff_long_q / oi_eff_short_q - stored_pos_count_long / stored_pos_count_short - stale_account_count_long / stale_account_count_short - neg_pnl_account_count - current_slot == last_market_slot Deferred (toly-only state, gated by KEEP_LIST entries): - active_close_present (KL-FORK-ENGINE-BANKRUPT-CLOSE-1) - bankruptcy_hmax_lock_active (KL-FORK-ENGINE-BANKRUPT-CLOSE-1) - stress_consumed_bps_e9_since_envelope (KL-FORK-ENGINE-STRESS-ENVELOPE-1) Until those subsystems land (ENG-PORT-1b, paired with the ENG-PORT-5b family), the wrapper-side authorization gate carries the residual checks. Tests: - New Kani harness `kani_withdraw_live_insurance_empty_market_gate`: symbolic pick over the 8 gate fields + a baseline. Each nonzero exposure marker causes rejection; the empty baseline accepts. Verified SUCCESSFUL: 0 of 989 checks failed, 2.47s. - 287/287 unit tests still pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ede_loss helper (ENG-PORT-2, CRITICAL-6)
Closes the loss-juniority bug in recurring fee accounting. Without this
fix `sync_account_fee_to_slot_not_atomic` would charge fee debt over the
interval `[last_fee_slot, now_slot]` even when `now_slot` is ahead of
`last_market_slot` — i.e., for slots the market hasn't accrued mark/funding
through. The fee debt then ranks ahead of those unrealized losses on the
account's capital ledger, ranking maintenance fees senior to losses they
were meant to be junior to.
Three sub-changes (toly-engine:10458-10504 + 4858-4866):
1. New helper `account_has_unsettled_live_effects` (4-predicate
ADAPTED port — fork lacks B-tracking subsystem per
KL-FORK-ENGINE-B-TRACKING-1, so the toly hunk's b_snap /
b_target_for_account / b_epoch_snap checks are dropped). Detects
when an account's epoch/A/K/F snap differs from its side's current
aggregates.
2. New helper `ensure_fee_draw_does_not_precede_loss` rejects with
Undercollateralized when (a) account.pnl < 0 OR (b) market is Live
AND the account has unsettled live effects.
3. `sync_account_fee_to_slot_not_atomic` (public entrypoint) now:
- Computes a `live_loss_safe_anchor` that clamps Live nonflat
accounts to `last_market_slot` when `now_slot` is ahead.
- Calls `ensure_fee_draw_does_not_precede_loss` as a front-stop
when the call would actually advance the fee anchor.
- Skips the live-accrual envelope check when `now_slot` doesn't
advance current_slot (no-op idempotent calls).
4. Internal `sync_account_fee_to_slot` belt-and-suspenders: also calls
`ensure_fee_draw_does_not_precede_loss` when fee_abs > 0, so any
future internal callers (e.g., a future `force_close_resolved_with_fee`
port) inherit the guarantee.
Tests:
- New Kani harnesses (both 0/2943 failures, 3.71s + 2.99s):
- `kani_sync_account_fee_rejects_negative_pnl`
- `kani_sync_account_fee_zero_rate_skips_loss_check` (regression
catch — the front-stop must NOT fire on a no-draw call)
- 287/287 unit tests still pass.
KEEP_LIST entry added: KL-FORK-ENGINE-B-TRACKING-1 documents the
B-snap subsystem absence as the rationale for the ADAPTED port.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…at 4 callsites (ENG-PORT-3, CRITICAL-7) Wires the predicate added in ENG-PORT-2 as a post-touch invariant assertion at four engine entrypoints that mutate account state through `touch_account_live_local`: - `execute_trade_not_atomic` (toly-engine:7688-7691): both counterparties checked after the dual touch; either side leaving stale snap state rejects with Undercollateralized before the trade body proceeds. - `withdraw_not_atomic` (toly-engine:9325-9328): post-touch, before finalize-touched (which sweeps fees against capital). - `convert_released_pnl_not_atomic` (toly-engine:9260-9263): post-touch, before `convert_released_pnl_core` mutates released-PnL bookkeeping. - `close_account_not_atomic` (toly-engine:7464-7467): post-touch, before `effective_pos_q == 0` check that would use stale A/K reference. Without this guard, a `touch_account_live_local` regression OR a specific edge case where touch fails to settle one of K/F/A/epoch would leave downstream computations operating on inconsistent account state. The guard is a belt-and-suspenders post-touch invariant: it does not fire on any current happy-path; it catches regressions in the touch machinery before they propagate. Tests: - All 287 unit tests still pass — the guard is a no-op on every existing test path because `touch_account_live_local` correctly settles the snaps. - Predicate correctness verified by the ENG-PORT-2 harnesses which exercise `account_has_unsettled_live_effects` through the public `sync_account_fee_to_slot_not_atomic` entrypoint. - The B-tracking gap (KL-FORK-ENGINE-B-TRACKING-1) means the guard catches K/F/A/epoch staleness but not B-snap drift; documented in KEEP_LIST.md as a residual narrow case. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes the maker-replaces-taker gap 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 that's mid-reset. Three sub-changes (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` signature widens with `(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 per-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. Tests: - All 287 unit tests still pass — existing happy paths don't fall into the maker-replaces-taker hazard. The gate is additive: it widens what gets rejected without weakening what gets accepted. - The fix is mechanical (signature + helper + callsite); a focused Kani harness for the maker-replaces-taker scenario would require multi- account symbolic setup that's tractable in unit tests but expensive in Kani; deferred to wrapper Bundle 4 cargo extensions. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… signature (ENG-PORT-4 fixup) Mechanical update: thread per-account old/new effective positions through the 5 existing test callsites. ENG-PORT-4 widened the gate signature to (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 binaries fail to compile. - proofs_invariants.rs:580-607 (proof_side_mode_gating): pass 0 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 the (b,a)-ordered per-account positions already in scope; matches 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: - 287/287 unit tests pass. - proof_side_mode_gating Kani harness (the most affected): 0 failures. - All Bundle 1 new harnesses still SUCCESSFUL. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
📝 WalkthroughWalkthroughThis PR refactors the keeper crank phase-2 scan from a fixed window size to a deterministic greedy touch-budget model, adds slot-bounded stress-reset pending semantics to enforce safe generation resets, strengthens side-mode OI gating, and adds fee-draw and post-touch invariant guards across multiple workflows. Specification and proof coverage are expanded to validate the new behaviors. ChangesStress-Reset & Touch-Budget Keeper Crank Refactor
Estimated code review effort🎯 4 (Complex) | ⏱️ ~75 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
⚔️ Resolve merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
src/percolator.rs (1)
6197-6223:⚠️ Potential issue | 🟠 Major | ⚡ Quick winReject
rr_touch_limit == 0or Phase 2 can stall forever.With
rr_touch_limit == 0, the Phase 2 loop never runs,rr_cursor_positionnever advances, andcomplete_cursor_wrap()never executes. A caller can then indefinitely starvesweep_generationadvancement and delayed stress clearing, which undercuts the mandatory sweep/liveness semantics this rewrite is introducing.Suggested fix
if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE { return Err(RiskError::Overflow); } + if rr_touch_limit == 0 { + return Err(RiskError::Overflow); + } if self.market_mode != MarketMode::Live { return Err(RiskError::Unauthorized); }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/percolator.rs` around lines 6197 - 6223, Add an explicit rejection for rr_touch_limit == 0 in this method (the function taking rr_touch_limit: u64) so Phase 2 cannot be skipped: after input validation (after Self::validate_admission_pair / Self::validate_threshold_opt and market_mode check) insert a guard if rr_touch_limit == 0 { return Err(RiskError::InvalidArgument); } (or another appropriate RiskError variant used by this crate) to prevent infinite stalling; keep the existing combined_touch_budget check with MAX_TOUCHED_PER_INSTRUCTION unchanged.
🧹 Nitpick comments (4)
tests/proofs_admission.rs (2)
1414-1434: ⚡ Quick winSecond crank's preconditions aren't pinned — at-most-once invariant may be vacuously satisfied.
After the first
keeper_crank_not_atomicat slot 1 advancessweep_generationand (presumably) wrapsrr_cursor_positionback to 0, the second call at slot 1 is expected to not advance generation again. However, the second call's input state is whatever the first call left behind, so if the first call also clearsstress_reset_pending/ drops back into a state where the wrap branch is unreachable (e.g., cursor not at the last slot), the equalityengine.sweep_generation == after_firstholds trivially without exercising the at-most-once guard.To strengthen this, after the first crank explicitly re-stage the stress-wrap pre-state (e.g., reset
rr_cursor_positionback tomax_accounts - 1, re-setstress_reset_pendingif relevant) before the second invocation, so the second call would try to advance generation and is rejected solely by the same-slot guard (last_sweep_generation_advance_slot == 1).♻️ Suggested setup for the second crank
let first = engine.keeper_crank_not_atomic(1, DEFAULT_ORACLE, &[], 0, 0, 1, 100, None, 1); assert!(first.is_ok()); let after_first = engine.sweep_generation; assert_eq!(after_first, generation_before as u64 + 1); + // Re-stage a state where Phase 2 *would* try to advance the + // generation again, so the at-most-once guard is the sole reason + // generation does not move. + engine.rr_cursor_position = engine.params.max_accounts - 1; let second = engine.keeper_crank_not_atomic(1, DEFAULT_ORACLE, &[], 0, 0, 1, 100, None, 1); assert!(second.is_ok()); assert_eq!(engine.sweep_generation, after_first); assert_eq!(engine.last_sweep_generation_advance_slot, 1); }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/proofs_admission.rs` around lines 1414 - 1434, The test currently calls keeper_crank_not_atomic twice but the second call's preconditions are not re-created, so the at-most-once check can be vacuously true; after the first successful call, explicitly reset the pre-state that would trigger a generation advance before invoking keeper_crank_not_atomic a second time by setting engine.rr_cursor_position = params.max_accounts - 1 (so the wrap branch is reachable) and re-assert any relevant flags such as engine.stress_reset_pending = true (if used by the wrap path), keep the second call at the same slot (1) and then assert sweep_generation did not change and last_sweep_generation_advance_slot == 1. Ensure these adjustments reference keeper_crank_not_atomic, rr_cursor_position, stress_reset_pending, sweep_generation, last_sweep_generation_advance_slot and params.max_accounts.
1327-1355: ⚖️ Poor tradeoffGreedy Phase 2 model proof is decoupled from the engine implementation.
v19_greedy_phase2_model_respects_touch_budget_and_boundsverifies properties of a hand-rolled greedy loop defined inside the proof body itself, not againstRiskEngine::keeper_crank_not_atomicor any engine helper. As written, this harness can pass even if the engine's actual Phase 2 scan diverges from the modeled semantics (e.g., scanning pastsweep_limit, mis-counting touched-vs-skipped, or mishandlingrr_touch_limit == 0). The companion harnesses (v19_rr_touch_zero_no_cursor_advance,v19_same_slot_stress_wrap_defers_generation_reset, etc.) anchor specific cases through the engine, but there is no harness that drives the engine through a multi-account scan and asserts the bound/touch-budget invariants directly.Consider either (a) renaming this to make its model-only nature explicit (e.g.,
v19_greedy_phase2_spec_model_self_consistent) and adding a second harness that asserts the same invariants on the engine over a small symbolic account population, or (b) replacing it with an engine-level harness usingparams.max_accounts = Nfor a small N and a symbolicusedmask.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/proofs_admission.rs` around lines 1327 - 1355, The test v19_greedy_phase2_model_respects_touch_budget_and_bounds is currently a standalone model and should be made explicit or replaced with an engine-level harness: either rename the function to v19_greedy_phase2_spec_model_self_consistent to indicate it's a pure model, and then add a new harness function that constructs a RiskEngine, sets params.max_accounts = 8 (matching sweep_limit), makes rr_touch_limit and the per-slot used mask symbolic, invokes RiskEngine::keeper_crank_not_atomic (or the appropriate Phase 2 helper) to drive a multi-account scan, and asserts the same invariants (touched <= rr_touch_limit, i <= sweep_limit, cursor_after < sweep_limit, and behavior when rr_touch_limit == 0); or replace the existing function with that engine-level harness directly. Use the existing variable names (rr_touch_limit, used_mask, sweep_limit) when mapping symbolic inputs to the engine setup so the assertions correspond to the modeled properties.tests/proofs_audit.rs (2)
1534-1541: ⚡ Quick winENG-PORT-3 has no dedicated Kani harness; the inline comment understates the gap.
The trailing comment justifies skipping ENG-PORT-3 coverage by pointing at the ENG-PORT-2 harnesses (
kani_sync_account_fee_rejects_negative_pnl,..._zero_rate_skips_loss_check) and "287 unit tests". Those ENG-PORT-2 harnesses verifyensure_fee_draw_does_not_precede_lossonly along thesync_account_fee_to_slot_not_atomicpath — they do not exerciseaccount_has_unsettled_live_effectsnor confirm it is invoked at the four ENG-PORT-3 callsites (execute_trade_not_atomic,withdraw_not_atomic,convert_released_pnl_not_atomic,close_account_not_atomic). A single trivial harness per callsite that builds an account in an unsettled-live-effects state and asserts each public entrypoint returnsErrwould close this gap without much effort, and would catch regressions where one of the four guard insertions is later removed or skipped.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/proofs_audit.rs` around lines 1534 - 1541, Missing dedicated Kani harnesses for ENG-PORT-3: add one small Kani harness per guarded callsite to guarantee the account_has_unsettled_live_effects check is actually exercised. For each of execute_trade_not_atomic, withdraw_not_atomic, convert_released_pnl_not_atomic and close_account_not_atomic create a harness (e.g., kani_account_has_unsettled_live_effects_execute_trade_harness) that constructs an Account in an “unsettled live effects” state (reuse the same setup helpers used by the ENG-PORT-2 harnesses like kani_sync_account_fee_rejects_negative_pnl), calls the public entrypoint (execute_trade, withdraw, convert_released_pnl, close_account respectively) and asserts the call returns Err; this will ensure the account_has_unsettled_live_effects predicate is invoked at each of the four callsites and will catch regressions if any guard is removed.
1448-1471: 💤 Low valueConsider adding an inline reference to the gate list to improve harness maintainability.
The harness's
pick-to-corruption mapping correctly covers all 7 individually-checkable gate fields (oi_eff_long_q,oi_eff_short_q,stored_pos_count_long/short,stale_account_count_long/short,neg_pnl_account_count) plus the slot mismatch case (current_slot != last_market_slot), matching the gate enforced at lines 7301–7309 ofwithdraw_live_insurance_not_atomic. Thepick == 7case correctly relies ontop_up_insurance_fundadvancingcurrent_slotwhile leavinglast_market_slotunchanged.However, adding a brief inline comment or extracting the gate field enumeration to a shared constant would help prevent silent gaps if new fields are added to the gate in the future (e.g.,
pending_close_present,stress_envelope,bankruptcy_hmax_lockcurrently deferred per ENG-PORT-1b, or any others added later).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/proofs_audit.rs` around lines 1448 - 1471, The harness maps the fuzz `pick` values to specific gate-corrupting fields (oi_eff_long_q, oi_eff_short_q, stored_pos_count_long/short, stale_account_count_long/short, neg_pnl_account_count, and the slot-mismatch via engine.current_slot) but has no explicit in-code reference to the gate enforced in withdraw_live_insurance_not_atomic; add a short inline comment above the `pick` mapping that enumerates the exact gate fields (matching withdraw_live_insurance_not_atomic) and/or extract those field names into a shared constant/enum (e.g., GATE_FIELDS or GateCorruptionKind) used by the harness so future gate additions must be updated in one place, and ensure the kani::assume(pick <= 8) bound is derived from that constant rather than a magic number; also mention the dependency on top_up_insurance_fund for the slot-mismatch case so maintainers see the coupling.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@README.md`:
- Around line 44-47: Markdown fenced code blocks are unlabeled and cause MD040
lint failures; update the three unlabeled fences containing the formulas for
ReleasedPos_i/effective_pnl_i, effective_pos(i)/pnl_delta(i), and the price-move
inequality (P_new, P_last, max_price_move_bps_per_slot) to include a language
label (e.g., add "text" after the opening ```). Edit the blocks that include the
symbols ReleasedPos_i, effective_pnl_i, effective_pos(i), pnl_delta(i), P_new,
P_last, and max_price_move_bps_per_slot to start with ```text so the linter
accepts them.
In `@src/percolator.rs`:
- Around line 5736-5744: The block comment before the test_visible! macro is
using Rust doc comments (///) which triggers an unused doc warning because it
doesn't attach to the generated item; replace the leading /// lines with regular
line comments (//) or move the explanatory text into the test_visible! macro
input so it becomes part of the macro payload; locate the comment immediately
preceding the test_visible! invocation in percolator.rs (the ENG-PORT-4
description) and change the comment style accordingly.
- Around line 3141-3146: The check treats Account::adl_a_basis like a stale-bit
but it is an attachment snapshot; instead rebase adl_a_basis on touch so the
stale-test remains correct. In settle_side_effects_live, when touching an
account whose account.adl_epoch_snap == self.get_epoch_side(side) update
account.adl_a_basis to the current value from self.get_a_side(side) (i.e.,
assign account.adl_a_basis = self.get_a_side(side)) so later comparisons in this
function (which already bail when adl_epoch_snap differs) no longer incorrectly
see adl_a_basis as stale.
In `@tests/proofs_audit.rs`:
- Around line 1337-1376: The test currently guards all terminal-drain
post-conditions behind "if r.is_ok()" which allows the harness to be vacuous
when resolve_market_not_atomic returns Err; change the conditional to an
unconditional assertion by replacing "if r.is_ok() { ... }" with
"assert!(r.is_ok());" immediately after calling resolve_market_not_atomic in
kani_resolve_market_terminal_drain so the subsequent assertions always run, and
make the identical change in kani_resolve_market_terminal_drain_degenerate;
reference the call site "let r = engine.resolve_market_not_atomic(...)" and the
result variable "r" when locating where to replace the conditional with an
assert.
---
Outside diff comments:
In `@src/percolator.rs`:
- Around line 6197-6223: Add an explicit rejection for rr_touch_limit == 0 in
this method (the function taking rr_touch_limit: u64) so Phase 2 cannot be
skipped: after input validation (after Self::validate_admission_pair /
Self::validate_threshold_opt and market_mode check) insert a guard if
rr_touch_limit == 0 { return Err(RiskError::InvalidArgument); } (or another
appropriate RiskError variant used by this crate) to prevent infinite stalling;
keep the existing combined_touch_budget check with MAX_TOUCHED_PER_INSTRUCTION
unchanged.
---
Nitpick comments:
In `@tests/proofs_admission.rs`:
- Around line 1414-1434: The test currently calls keeper_crank_not_atomic twice
but the second call's preconditions are not re-created, so the at-most-once
check can be vacuously true; after the first successful call, explicitly reset
the pre-state that would trigger a generation advance before invoking
keeper_crank_not_atomic a second time by setting engine.rr_cursor_position =
params.max_accounts - 1 (so the wrap branch is reachable) and re-assert any
relevant flags such as engine.stress_reset_pending = true (if used by the wrap
path), keep the second call at the same slot (1) and then assert
sweep_generation did not change and last_sweep_generation_advance_slot == 1.
Ensure these adjustments reference keeper_crank_not_atomic, rr_cursor_position,
stress_reset_pending, sweep_generation, last_sweep_generation_advance_slot and
params.max_accounts.
- Around line 1327-1355: The test
v19_greedy_phase2_model_respects_touch_budget_and_bounds is currently a
standalone model and should be made explicit or replaced with an engine-level
harness: either rename the function to
v19_greedy_phase2_spec_model_self_consistent to indicate it's a pure model, and
then add a new harness function that constructs a RiskEngine, sets
params.max_accounts = 8 (matching sweep_limit), makes rr_touch_limit and the
per-slot used mask symbolic, invokes RiskEngine::keeper_crank_not_atomic (or the
appropriate Phase 2 helper) to drive a multi-account scan, and asserts the same
invariants (touched <= rr_touch_limit, i <= sweep_limit, cursor_after <
sweep_limit, and behavior when rr_touch_limit == 0); or replace the existing
function with that engine-level harness directly. Use the existing variable
names (rr_touch_limit, used_mask, sweep_limit) when mapping symbolic inputs to
the engine setup so the assertions correspond to the modeled properties.
In `@tests/proofs_audit.rs`:
- Around line 1534-1541: Missing dedicated Kani harnesses for ENG-PORT-3: add
one small Kani harness per guarded callsite to guarantee the
account_has_unsettled_live_effects check is actually exercised. For each of
execute_trade_not_atomic, withdraw_not_atomic, convert_released_pnl_not_atomic
and close_account_not_atomic create a harness (e.g.,
kani_account_has_unsettled_live_effects_execute_trade_harness) that constructs
an Account in an “unsettled live effects” state (reuse the same setup helpers
used by the ENG-PORT-2 harnesses like
kani_sync_account_fee_rejects_negative_pnl), calls the public entrypoint
(execute_trade, withdraw, convert_released_pnl, close_account respectively) and
asserts the call returns Err; this will ensure the
account_has_unsettled_live_effects predicate is invoked at each of the four
callsites and will catch regressions if any guard is removed.
- Around line 1448-1471: The harness maps the fuzz `pick` values to specific
gate-corrupting fields (oi_eff_long_q, oi_eff_short_q,
stored_pos_count_long/short, stale_account_count_long/short,
neg_pnl_account_count, and the slot-mismatch via engine.current_slot) but has no
explicit in-code reference to the gate enforced in
withdraw_live_insurance_not_atomic; add a short inline comment above the `pick`
mapping that enumerates the exact gate fields (matching
withdraw_live_insurance_not_atomic) and/or extract those field names into a
shared constant/enum (e.g., GATE_FIELDS or GateCorruptionKind) used by the
harness so future gate additions must be updated in one place, and ensure the
kani::assume(pick <= 8) bound is derived from that constant rather than a magic
number; also mention the dependency on top_up_insurance_fund for the
slot-mismatch case so maintainers see the coupling.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 4084c41a-28f7-4789-8073-d40dade49f86
📒 Files selected for processing (12)
README.mdkani-list.jsonscripts/proof-strength-audit-results.mdspec.mdsrc/percolator.rstests/proofs_admission.rstests/proofs_audit.rstests/proofs_checklist.rstests/proofs_instructions.rstests/proofs_invariants.rstests/proofs_liveness.rstests/unit_tests.rs
Comment on lines
44
to
47
| ``` | ||
| ReleasedPos_i = max(PNL_i, 0) - R_i | ||
| effective_pnl_i = floor(ReleasedPos_i * h) | ||
| ``` |
There was a problem hiding this comment.
Add fence languages to satisfy markdown linting
Line 44, Line 80, and Line 116 use unlabeled fenced blocks. Add a language (e.g., text) to avoid MD040 lint failures in docs checks.
Proposed doc-lint fix
-```
+```text
ReleasedPos_i = max(PNL_i, 0) - R_i
effective_pnl_i = floor(ReleasedPos_i * h)
```diff
-```
+```text
effective_pos(i) = floor(basis_i * A / a_basis_i)
pnl_delta(i) =
floor(|basis_i| * ((K - k_snap_i) * FUNDING_DEN + (F - f_snap_i))
/ (a_basis_i * POS_SCALE * FUNDING_DEN))
```diff
-```
+```text
abs(P_new - P_last) * 10_000
<= max_price_move_bps_per_slot * dt * P_last
</details>
Also applies to: 80-85, 116-119
<details>
<summary>🧰 Tools</summary>
<details>
<summary>🪛 markdownlint-cli2 (0.22.1)</summary>
[warning] 44-44: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
</details>
</details>
<details>
<summary>🤖 Prompt for AI Agents</summary>
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In @README.md around lines 44 - 47, Markdown fenced code blocks are unlabeled
and cause MD040 lint failures; update the three unlabeled fences containing the
formulas for ReleasedPos_i/effective_pnl_i, effective_pos(i)/pnl_delta(i), and
the price-move inequality (P_new, P_last, max_price_move_bps_per_slot) to
include a language label (e.g., add "text" after the opening ). Edit the blocks that include the symbols ReleasedPos_i, effective_pnl_i, effective_pos(i), pnl_delta(i), P_new, P_last, and max_price_move_bps_per_slot to start with text so the linter accepts them.
</details>
<!-- fingerprinting:phantom:poseidon:hawk -->
<!-- d98c2f50 -->
<!-- This is an auto-generated comment by CodeRabbit -->
Comment on lines
+3141
to
+3146
| 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)) |
There was a problem hiding this comment.
adl_a_basis is treated like a stale bit here, but it is still an attachment snapshot elsewhere.
settle_side_effects_live() does not rebase Account::adl_a_basis on touch, so after an ADL shrink a fully-touched same-epoch account can still satisfy account.adl_a_basis != self.get_a_side(side). That makes the new guards reject fee sync / withdraw / convert / close for accounts that are already current under this fork’s existing semantics.
Suggested fix
- Ok(account.adl_a_basis != self.get_a_side(side)
- || account.adl_k_snap != self.get_k_side(side)
+ Ok(account.adl_k_snap != self.get_k_side(side)
|| account.f_snap != self.get_f_side(side))🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/percolator.rs` around lines 3141 - 3146, The check treats
Account::adl_a_basis like a stale-bit but it is an attachment snapshot; instead
rebase adl_a_basis on touch so the stale-test remains correct. In
settle_side_effects_live, when touching an account whose account.adl_epoch_snap
== self.get_epoch_side(side) update account.adl_a_basis to the current value
from self.get_a_side(side) (i.e., assign account.adl_a_basis =
self.get_a_side(side)) so later comparisons in this function (which already bail
when adl_epoch_snap differs) no longer incorrectly see adl_a_basis as stale.
Comment on lines
+5736
to
+5744
| /// ENG-PORT-4 (CRITICAL-8): aggregate-OI + per-account side-mode gate. | ||
| /// | ||
| /// The aggregate OI checks alone miss the maker-replaces-taker case: | ||
| /// a trade where one counterparty closes long while the other opens | ||
| /// long net-zeros side OI but still admits a new entrant onto a side | ||
| /// in DrainOnly/ResetPending. Toly v12.20.6 widened the gate | ||
| /// (toly-engine:8021-8043) to also check per-account old/new effective | ||
| /// positions, so any new arrival on a blocked side is rejected even | ||
| /// when aggregate OI doesn't grow. |
There was a problem hiding this comment.
Use a normal comment here to avoid the rustdoc warning.
This /// block sits in front of test_visible!, so it does not attach to the generated function and Clippy reports unused doc comment. Convert it to // comments, or move the docs inside the macro input.
🧰 Tools
🪛 Clippy (1.95.0)
[warning] 5736-5736: unused doc comment
(warning)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/percolator.rs` around lines 5736 - 5744, The block comment before the
test_visible! macro is using Rust doc comments (///) which triggers an unused
doc warning because it doesn't attach to the generated item; replace the leading
/// lines with regular line comments (//) or move the explanatory text into the
test_visible! macro input so it becomes part of the macro payload; locate the
comment immediately preceding the test_visible! invocation in percolator.rs (the
ENG-PORT-4 description) and change the comment style accordingly.
Comment on lines
+1337
to
+1376
| let r = engine.resolve_market_not_atomic( | ||
| ResolveMode::Ordinary, | ||
| DEFAULT_ORACLE, | ||
| DEFAULT_ORACLE, | ||
| DEFAULT_SLOT + 1, | ||
| 0, | ||
| ); | ||
|
|
||
| if r.is_ok() { | ||
| // Steps 13 / 14 / 15-16 / 21 post-conditions (all share the | ||
| // single-engine-call atomicity claim — none of these can be | ||
| // partially applied). | ||
| assert!(engine.market_mode == MarketMode::Resolved); | ||
| assert!(engine.oi_eff_long_q == 0); | ||
| assert!(engine.oi_eff_short_q == 0); | ||
| assert!(engine.resolved_payout_h_num == 0); | ||
| assert!(engine.resolved_payout_h_den == 0); | ||
| assert!(engine.resolved_payout_ready == 0); | ||
| assert!(engine.pnl_matured_pos_tot == pre_pnl_pos_tot); | ||
|
|
||
| // ENG-PORT-5a phantom-dust invariant (KL-PHANTOM-DUST-SCHEMA-1). | ||
| if pre_stored_long == 0 { | ||
| assert!(engine.phantom_dust_bound_long_q == 0); | ||
| } | ||
| if pre_stored_short == 0 { | ||
| assert!(engine.phantom_dust_bound_short_q == 0); | ||
| } | ||
|
|
||
| // ENG-PORT-5a K-terminal-delta-zero-on-zero-OI predicate. A side | ||
| // with no pre-resolve OI cannot accumulate a non-zero terminal | ||
| // delta — the delta would attribute a settlement shift to | ||
| // positions that don't exist. | ||
| if pre_oi_long == 0 { | ||
| assert!(engine.resolved_k_long_terminal_delta == 0); | ||
| } | ||
| if pre_oi_short == 0 { | ||
| assert!(engine.resolved_k_short_terminal_delta == 0); | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
Conditional if r.is_ok() makes the terminal-drain post-conditions vacuous when the engine rejects.
kani_resolve_market_terminal_drain only asserts the post-conditions inside if r.is_ok() { ... }. If the symbolic pre_dust_long/pre_dust_short (or any other state) causes resolve_market_not_atomic to consistently return Err(..) along all reachable paths, the harness passes without verifying anything — which directly defeats the stated purpose of CRITICAL-9 / ENG-PORT-5a (terminal-drain atomicity). The same pattern is in kani_resolve_market_terminal_drain_degenerate (Line 1412).
Given this fixture (fresh engine, one deposited but flat account, OI = 0, current slot = DEFAULT_SLOT + 1), an Ordinary resolve at the live oracle should always succeed, so the conditional masks any future regression that turns this harness vacuous. Convert it to an unconditional success assertion (and propagate to the Degenerate twin):
🛡️ Replace conditional check with unconditional success
- let r = engine.resolve_market_not_atomic(
+ engine.resolve_market_not_atomic(
ResolveMode::Ordinary,
DEFAULT_ORACLE,
DEFAULT_ORACLE,
DEFAULT_SLOT + 1,
0,
- );
-
- if r.is_ok() {
- // Steps 13 / 14 / 15-16 / 21 post-conditions ...
- assert!(engine.market_mode == MarketMode::Resolved);
- ...
- }
+ ).expect("flat-account, no-OI Ordinary resolve must succeed");
+
+ // Steps 13 / 14 / 15-16 / 21 post-conditions ...
+ assert!(engine.market_mode == MarketMode::Resolved);
+ ...Apply the same change to kani_resolve_market_terminal_drain_degenerate.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@tests/proofs_audit.rs` around lines 1337 - 1376, The test currently guards
all terminal-drain post-conditions behind "if r.is_ok()" which allows the
harness to be vacuous when resolve_market_not_atomic returns Err; change the
conditional to an unconditional assertion by replacing "if r.is_ok() { ... }"
with "assert!(r.is_ok());" immediately after calling resolve_market_not_atomic
in kani_resolve_market_terminal_drain so the subsequent assertions always run,
and make the identical change in kani_resolve_market_terminal_drain_degenerate;
reference the call site "let r = engine.resolve_market_not_atomic(...)" and the
result variable "r" when locating where to replace the conditional with an
assert.
Owner
Author
|
Superseded by bulk-sync strategy. Closing unmerged. Branch preserved at feat/audit-engine-critical-bundle for reference; the 5 audit-validated fixes will be cross-checked against bulk-sync output to confirm parity or improvement. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Bundle 1 of the wrapper-engine deep-audit Phase 2 execution. Closes 5 CRITICAL findings on the engine side (C-5 through C-9, anchoring C-1/2 wrapper changes that follow in Bundle 2).
This PR also brings in 10 Toly upstream cherry-picks (authored by Anatoly Yakovenko) that were already merged into the working branch HEAD as part of the v12.18.5+ track. They appear first in the commit graph; the 6 audit-port commits sit on top.
Audit-port commits (6, authored as part of this work)
a911643ENG-PORT-5aresolve_market_not_atomicpre-state snapshots + zero-OI K-delta + fork-adapted phantom-dust zero + drainpre_stored > 0guardf460a2aENG-PORT-1withdraw_live_insurance_not_atomic(8 of 11 toly conditions; 3 deferred to ENG-PORT-1b)099ad75ENG-PORT-2ensure_fee_draw_does_not_precede_losshelper + newaccount_has_unsettled_live_effectspredicate9b51dd0ENG-PORT-3execute_trade_not_atomic,withdraw_not_atomic,convert_released_pnl_not_atomic,close_account_not_atomicba3f41aENG-PORT-4enforce_side_mode_oi_gatewidened: per-account(old_eff_*, new_eff_*)plumbed alongside aggregate OI; newenforce_side_mode_account_gatehelper closes the maker-replaces-taker gap38b551etest fixupToly upstream cherry-picks (10, pre-existing on the branch base)
a559c76 .. 33c2b04- read-only set of Anatoly-authored commits. Most relevant ones for this PR's scope:a559c76Support sparse keeper stress sweepsbabfe83Harden engine state invariants1299bbdHarden account-local fee state checksbc88671Bound solvency and harden fee credits33c2b04Fail closed on corrupt engine stateThese should land regardless of the audit work; they are independent Toly upstream improvements that the working branch was already carrying.
Adapted ports and deferred sub-work
Inline + KEEP_LIST.md documented:
active_close_present+bankruptcy_hmax_lock_activeDEFERRED to ENG-PORT-1b/5b. Same gate also defersclear_stress_envelope.account_has_unsettled_live_effectsADAPTED to drop toly's B-component snap predicates (fork lacksb_snap/b_target_for_account/b_epoch_snap). 4 remaining predicates (epoch / A / K / F) catch staleness in every path.9d849bb"Support dynamic trade fees" SKIPPED as FEATURE divergence.FIX-2 (LpCollateralLedger PDA struct) is NOT in this engine bundle - the struct is wrapper-side type (Pubkey-typed PDA, no engine fit) and lands in Bundle 2 alongside FIX-1 + FIX-3.
Test plan
Cross-program follow-up
dcccrypto/percolator-prog feat/audit-wrapper-critical-bundle): pins to this engine SHA in Cargo.toml; wires up PORT-1 / PORT-2 / PORT-3 / PORT-12 wrapper changes.dcccrypto/percolator-sdk feat/audit-sdk-wire-format-bundle): paired SDK release for tag 19 mode-byte; one beta cycle before Bundle 2 wrapper opens.origin/main's independent v12.17-core sync line into a single linear history.🤖 Generated with Claude Code
Summary by CodeRabbit
Release Notes
Documentation
Bug Fixes & Safety
Tests